Theory BigStep

(*  Title:       CoreC++
    ID:          $Id: BigStep.thy,v 1.17 2007-07-19 21:23:08 makarius Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

    Based on the Jinja theory J/BigStep.thy by Tobias Nipkow
*)


header {* \isaheader{Big Step Semantics} *}

theory BigStep imports Syntax State begin


section {* The rules *}

inductive
  eval :: "prog => env => expr => state => expr => state => bool"
          ("_,_ \<turnstile> ((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  and evals :: "prog => env => expr list => state => expr list => state => bool"
           ("_,_ \<turnstile> ((1⟨_,/_⟩) [=>]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  for P :: prog
where

  New:
  "[| new_Addr h = Some a; h' = h(a\<mapsto>(C,Collect (init_obj P C))) |]
  ==> P,E \<turnstile> ⟨new C,(h,l)⟩ => ⟨ref (a,[C]),(h',l)⟩"

| NewFail:
  "new_Addr h = None ==>
  P,E \<turnstile> ⟨new C, (h,l)⟩ => ⟨THROW OutOfMemory,(h,l)⟩"

| StaticUpCast:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs),s1⟩; P \<turnstile> Path last Cs to C via Cs'; Ds = Cs@pCs' |]
  ==> P,E \<turnstile> ⟨(|C|)),e,s0⟩ => ⟨ref (a,Ds),s1⟩"

| StaticDownCast:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs@[C]@Cs'),s1⟩
   ==> P,E \<turnstile> ⟨(|C|)),e,s0⟩ => ⟨ref (a,Cs@[C]),s1⟩"

| StaticCastNull:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P,E \<turnstile> ⟨(|C|)),e,s0⟩ => ⟨null,s1⟩"

| StaticCastFail:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs),s1⟩; ¬ P \<turnstile> (last Cs) \<preceq>* C; C ∉ set Cs |]
  ==> P,E \<turnstile> ⟨(|C|)),e,s0⟩ => ⟨THROW ClassCast,s1⟩"

| StaticCastThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨(|C|)),e,s0⟩ => ⟨throw e',s1⟩"

| StaticUpDynCast:(* path uniqueness not necessary for type proof but for determinism *)
  "[|P,E \<turnstile> ⟨e,s0⟩ => ⟨ref(a,Cs),s1⟩; P \<turnstile> Path last Cs to C unique;
    P \<turnstile> Path last Cs to C via Cs'; Ds = Cs@pCs' |]
  ==> P,E \<turnstile> ⟨Cast C e,s0⟩ => ⟨ref(a,Ds),s1⟩"

| StaticDownDynCast:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs@[C]@Cs'),s1⟩
   ==> P,E \<turnstile> ⟨Cast C e,s0⟩ => ⟨ref (a,Cs@[C]),s1⟩"

| DynCast: (* path uniqueness not necessary for type proof but for determinism *)
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs),(h,l)⟩; h a = Some(D,S);
    P \<turnstile> Path D to C via Cs'; P \<turnstile> Path D to C unique |]
  ==> P,E \<turnstile> ⟨Cast C e,s0⟩ => ⟨ref (a,Cs'),(h,l)⟩"

| DynCastNull:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P,E \<turnstile> ⟨Cast C e,s0⟩ => ⟨null,s1⟩"

| DynCastFail: (* fourth premise not necessary for type proof but for determinism *)
  "[| P,E \<turnstile> ⟨e,s0⟩=> ⟨ref (a,Cs),(h,l)⟩; h a = Some(D,S); ¬ P \<turnstile> Path D to C unique;
    ¬ P \<turnstile> Path last Cs to C unique; C ∉ set Cs |]
  ==> P,E \<turnstile> ⟨Cast C e,s0⟩ => ⟨null,(h,l)⟩"

| DynCastThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨Cast C e,s0⟩ => ⟨throw e',s1⟩"

| Val:
  "P,E \<turnstile> ⟨Val v,s⟩ => ⟨Val v,s⟩"

| BinOp:
  "[| P,E \<turnstile> ⟨e1,s0⟩ => ⟨Val v1,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ => ⟨Val v2,s2⟩; 
    binop(bop,v1,v2) = Some v |]
  ==> P,E \<turnstile> ⟨e1 «bop» e2,s0⟩=>⟨Val v,s2⟩"

| BinOpThrow1:
  "P,E \<turnstile> ⟨e1,s0⟩ => ⟨throw e,s1⟩ ==>
  P,E \<turnstile> ⟨e1 «bop» e2, s0⟩ => ⟨throw e,s1⟩"

| BinOpThrow2:
  "[| P,E \<turnstile> ⟨e1,s0⟩ => ⟨Val v1,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ => ⟨throw e,s2⟩ |]
  ==> P,E \<turnstile> ⟨e1 «bop» e2,s0⟩ => ⟨throw e,s2⟩"

| Var:
  "l V = Some v ==>
  P,E \<turnstile> ⟨Var V,(h,l)⟩ => ⟨Val v,(h,l)⟩"

| LAss:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨Val v,(h,l)⟩; E V = Some T;
     P \<turnstile> T casts v to v'; l' = l(V\<mapsto>v') |]
  ==> P,E \<turnstile> ⟨V:=e,s0⟩ => ⟨Val v',(h,l')⟩"

| LAssThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨V:=e,s0⟩ => ⟨throw e',s1⟩"

| FAcc:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs'),(h,l)⟩; h a = Some(D,S);
     Ds = Cs'@pCs; (Ds,fs) ∈ S; fs F = Some v |]
  ==> P,E \<turnstile> ⟨e•F{Cs},s0⟩ => ⟨Val v,(h,l)⟩"

| FAccNull:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P,E \<turnstile> ⟨e•F{Cs},s0⟩ => ⟨THROW NullPointer,s1⟩" 

| FAccThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨e•F{Cs},s0⟩ => ⟨throw e',s1⟩"

| FAss:
  "[| P,E \<turnstile> ⟨e1,s0⟩ => ⟨ref (a,Cs'),s1⟩; P,E \<turnstile> ⟨e2,s1⟩ => ⟨Val v,(h2,l2)⟩;
     h2 a = Some(D,S); P \<turnstile> (last Cs') has least F:T via Cs; P \<turnstile> T casts v to v';
     Ds = Cs'@pCs; (Ds,fs) ∈ S; fs' = fs(F\<mapsto>v'); 
     S' = S - {(Ds,fs)} ∪ {(Ds,fs')}; h2' = h2(a\<mapsto>(D,S'))|]
  ==> P,E \<turnstile> ⟨e1•F{Cs}:=e2,s0⟩ => ⟨Val v',(h2',l2)⟩"

| FAssNull:
  "[| P,E \<turnstile> ⟨e1,s0⟩ => ⟨null,s1⟩;  P,E \<turnstile> ⟨e2,s1⟩ => ⟨Val v,s2⟩ |] ==>
  P,E \<turnstile> ⟨e1•F{Cs}:=e2,s0⟩ => ⟨THROW NullPointer,s2⟩" 

| FAssThrow1:
  "P,E \<turnstile> ⟨e1,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨e1•F{Cs}:=e2,s0⟩ => ⟨throw e',s1⟩"

| FAssThrow2:
  "[| P,E \<turnstile> ⟨e1,s0⟩ => ⟨Val v,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ => ⟨throw e',s2⟩ |]
  ==> P,E \<turnstile> ⟨e1•F{Cs}:=e2,s0⟩ => ⟨throw e',s2⟩"

| CallObjThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨Call e Copt M es,s0⟩ => ⟨throw e',s1⟩"

| CallParamsThrow:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨Val v,s1⟩; P,E \<turnstile> ⟨es,s1⟩ [=>] ⟨map Val vs @ throw ex # es',s2⟩ |]
   ==> P,E \<turnstile> ⟨Call e Copt M es,s0⟩ => ⟨throw ex,s2⟩"

| Call:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs),s1⟩;  P,E \<turnstile> ⟨ps,s1⟩ [=>] ⟨map Val vs,(h2,l2)⟩;
     h2 a = Some(C,S);  P \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds;
     P \<turnstile> (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'; length vs = length pns; 
     P \<turnstile> Ts Casts vs to vs'; l2' = [this\<mapsto>Ref (a,Cs'), pns[\<mapsto>]vs'];
     new_body = (case T' of Class D => (|D|)),body   | _  => body);  
     P,E(this\<mapsto>Class(last Cs'), pns[\<mapsto>]Ts) \<turnstile> ⟨new_body,(h2,l2')⟩ => ⟨e',(h3,l3)⟩ |]
  ==> P,E \<turnstile> ⟨e•M(ps),s0⟩ => ⟨e',(h3,l2)⟩"

| StaticCall:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨ref (a,Cs),s1⟩;  P,E \<turnstile> ⟨ps,s1⟩ [=>] ⟨map Val vs,(h2,l2)⟩;
     P \<turnstile> Path (last Cs) to C unique; P \<turnstile> Path (last Cs) to C via Cs'';
     P \<turnstile> C has least M = (Ts,T,pns,body) via Cs'; Ds = (Cs@pCs'')@pCs';
     length vs = length pns; P \<turnstile> Ts Casts vs to vs'; 
     l2' = [this\<mapsto>Ref (a,Ds), pns[\<mapsto>]vs'];
     P,E(this\<mapsto>Class(last Ds), pns[\<mapsto>]Ts) \<turnstile> ⟨body,(h2,l2')⟩ => ⟨e',(h3,l3)⟩ |]
  ==> P,E \<turnstile> ⟨e•(C::)M(ps),s0⟩ => ⟨e',(h3,l2)⟩"

| CallNull:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩;  P,E \<turnstile> ⟨es,s1⟩ [=>] ⟨map Val vs,s2⟩ |]
  ==> P,E \<turnstile> ⟨Call e Copt M es,s0⟩ => ⟨THROW NullPointer,s2⟩"

| Block:
  "[|P,E(V \<mapsto> T) \<turnstile> ⟨e0,(h0,l0(V:=None))⟩ => ⟨e1,(h1,l1)⟩ |] ==>
  P,E \<turnstile> ⟨{V:T; e0},(h0,l0)⟩ => ⟨e1,(h1,l1(V:=l0 V))⟩"

| Seq:
  "[| P,E \<turnstile> ⟨e0,s0⟩ => ⟨Val v,s1⟩; P,E \<turnstile> ⟨e1,s1⟩ => ⟨e2,s2⟩ |]
  ==> P,E \<turnstile> ⟨e0;;e1,s0⟩ => ⟨e2,s2⟩"

| SeqThrow:
  "P,E \<turnstile> ⟨e0,s0⟩ => ⟨throw e,s1⟩ ==>
  P,E \<turnstile> ⟨e0;;e1,s0⟩=>⟨throw e,s1⟩"

| CondT:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨true,s1⟩; P,E \<turnstile> ⟨e1,s1⟩ => ⟨e',s2⟩ |]
  ==> P,E \<turnstile> ⟨if (e) e1 else e2,s0⟩ => ⟨e',s2⟩"

| CondF:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨false,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ => ⟨e',s2⟩ |]
  ==> P,E \<turnstile> ⟨if (e) e1 else e2,s0⟩ => ⟨e',s2⟩"

| CondThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨if (e) e1 else e2, s0⟩ => ⟨throw e',s1⟩"

| WhileF:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨false,s1⟩ ==>
  P,E \<turnstile> ⟨while (e) c,s0⟩ => ⟨unit,s1⟩"

| WhileT:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨true,s1⟩; P,E \<turnstile> ⟨c,s1⟩ => ⟨Val v1,s2⟩; 
     P,E \<turnstile> ⟨while (e) c,s2⟩ => ⟨e3,s3⟩ |]
  ==> P,E \<turnstile> ⟨while (e) c,s0⟩ => ⟨e3,s3⟩"

| WhileCondThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨ throw e',s1⟩ ==>
  P,E \<turnstile> ⟨while (e) c,s0⟩ => ⟨throw e',s1⟩"

| WhileBodyThrow:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨true,s1⟩; P,E \<turnstile> ⟨c,s1⟩ => ⟨throw e',s2⟩|]
  ==> P,E \<turnstile> ⟨while (e) c,s0⟩ => ⟨throw e',s2⟩"

| Throw:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨ref r,s1⟩ ==>
  P,E \<turnstile> ⟨throw e,s0⟩ => ⟨Throw r,s1⟩"

| ThrowNull:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P,E \<turnstile> ⟨throw e,s0⟩ => ⟨THROW NullPointer,s1⟩"

| ThrowThrow:
  "P,E \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P,E \<turnstile> ⟨throw e,s0⟩ => ⟨throw e',s1⟩"

| Nil:
  "P,E \<turnstile> ⟨[],s⟩ [=>] ⟨[],s⟩"

| Cons:
  "[| P,E \<turnstile> ⟨e,s0⟩ => ⟨Val v,s1⟩; P,E \<turnstile> ⟨es,s1⟩ [=>] ⟨es',s2⟩ |]
  ==> P,E \<turnstile> ⟨e#es,s0⟩ [=>] ⟨Val v # es',s2⟩"

| ConsThrow:
  "P,E \<turnstile> ⟨e, s0⟩ => ⟨throw e', s1⟩ ==>
  P,E \<turnstile> ⟨e#es, s0⟩ [=>] ⟨throw e' # es, s1⟩"

lemmas eval_evals_induct = eval_evals.induct [split_format (complete)]
  and eval_evals_inducts = eval_evals.inducts [split_format (complete)]

inductive_cases eval_cases [cases set]:
 "P,E \<turnstile> ⟨new C,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨Cast C e,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨(|C|)),e,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨Val v,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e1 «bop» e2,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨Var V,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨V:=e,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e•F{Cs},s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e1•F{Cs}:=e2,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e•M(es),s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e•(C::)M(es),s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨{V:T;e1},s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e1;;e2,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨if (e) e1 else e2,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨while (b) c,s⟩ => ⟨e',s'⟩"
 "P,E \<turnstile> ⟨throw e,s⟩ => ⟨e',s'⟩"
  
inductive_cases evals_cases [cases set]:
 "P,E \<turnstile> ⟨[],s⟩ [=>] ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e#es,s⟩ [=>] ⟨e',s'⟩"



section {*Final expressions*}

constdefs
  final :: "expr => bool"
  "final e  ≡  (∃v. e = Val v) ∨ (∃r. e = Throw r)"
  finals:: "expr list => bool"
  "finals es  ≡  (∃vs. es = map Val vs) ∨ (∃vs r es'. es = map Val vs @ Throw r # es')"

lemma [simp]: "final(Val v)"
by(simp add:final_def)

lemma [simp]: "final(throw e) = (∃r. e = ref r)"
by(simp add:final_def)

lemma finalE: "[| final e;  !!v. e = Val v ==> Q;  !!r. e = Throw r ==> Q |] ==> Q"
by(auto simp:final_def)

lemma [iff]: "finals []"
by(simp add:finals_def)

lemma [iff]: "finals (Val v # es) = finals es"

apply(clarsimp simp add:finals_def)
apply(rule iffI)
 apply(erule disjE)
  apply simp
 apply(rule disjI2)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastsimp
apply(erule disjE)
 apply (rule disjI1)
 apply clarsimp
apply(rule disjI2)
apply clarsimp
apply(rule_tac x = "v#vs" in exI)
apply simp
done


lemma finals_app_map[iff]: "finals (map Val vs @ es) = finals es"
by(induct_tac vs, auto)

lemma [iff]: "finals (map Val vs)"
using finals_app_map[of vs "[]"]by(simp)

lemma [iff]: "finals (throw e # es) = (∃r. e = ref r)"

apply(simp add:finals_def)
apply(rule iffI)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastsimp
apply fastsimp
done


lemma not_finals_ConsI: "¬ final e ==> ¬ finals(e#es)"
 
apply(auto simp add:finals_def final_def)
apply(case_tac vs)
apply auto
done


lemma eval_final: "P,E \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩ ==> final e'"
 and evals_final: "P,E \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩ ==> finals es'"
by(induct rule:eval_evals.inducts, simp_all)


lemma eval_lcl_incr: "P,E \<turnstile> ⟨e,(h0,l0)⟩ => ⟨e',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
 and evals_lcl_incr: "P,E \<turnstile> ⟨es,(h0,l0)⟩ [=>] ⟨es',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
by (induct rule:eval_evals_inducts) (auto simp del:fun_upd_apply)


text{* Only used later, in the small to big translation, but is already a
good sanity check: *}

lemma eval_finalId:  "final e ==> P,E \<turnstile> ⟨e,s⟩ => ⟨e,s⟩"
by (erule finalE) (fastsimp intro: eval_evals.intros)+


lemma eval_finalsId:
assumes finals: "finals es" shows "P,E \<turnstile> ⟨es,s⟩ [=>] ⟨es,s⟩"

  using finals
proof (induct es type: list)
  case Nil show ?case by (rule eval_evals.intros)
next
  case (Cons e es)
  have hyp: "finals es ==> P,E \<turnstile> ⟨es,s⟩ [=>] ⟨es,s⟩"
   and finals: "finals (e # es)" by fact+
  show "P,E \<turnstile> ⟨e # es,s⟩ [=>] ⟨e # es,s⟩"
  proof cases
    assume "final e"
    thus ?thesis
    proof (cases rule: finalE)
      fix v assume e: "e = Val v"
      have "P,E \<turnstile> ⟨Val v,s⟩ => ⟨Val v,s⟩" by (simp add: eval_finalId)
      moreover from finals e have "P,E \<turnstile> ⟨es,s⟩ [=>] ⟨es,s⟩" by(fast intro:hyp)
      ultimately have "P,E \<turnstile> ⟨Val v#es,s⟩ [=>] ⟨Val v#es,s⟩"
        by (rule eval_evals.intros)
      with e show ?thesis by simp
    next
      fix a assume e: "e = Throw a"
      have "P,E \<turnstile> ⟨Throw a,s⟩ => ⟨Throw a,s⟩" by (simp add: eval_finalId)
      hence "P,E \<turnstile> ⟨Throw a#es,s⟩ [=>] ⟨Throw a#es,s⟩" by (rule eval_evals.intros)
      with e show ?thesis by simp
    qed
  next
    assume "¬ final e"
    with not_finals_ConsI finals have False by blast
    thus ?thesis ..
  qed
qed


lemma
eval_preserves_obj:"P,E \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> (!!S. h a = Some(D,S) 
  ==> ∃S'. h' a = Some(D,S'))"
and evals_preserves_obj:"P,E \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩ 
==> (!!S. h a = Some(D,S) ==> ∃S'. h' a = Some(D,S'))"
by(induct rule:eval_evals_inducts)(fastsimp dest:new_Addr_SomeD)+

end