Theory BigStep

(*  Title:      Jinja/J/BigStep.thy
    ID:         $Id: BigStep.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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

theory BigStep = Expr + State:

consts
  eval  :: "J_prog => ((expr × state) × (expr × state)) set"
  evals  :: "J_prog => ((expr list × state) × (expr list × state)) set"

(*<*)
syntax (xsymbols)
  eval :: "J_prog => expr => state => expr => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  evals :: "J_prog => expr list => state => expr list => state => bool"
           ("_ \<turnstile> ((1⟨_,/_⟩) [=>]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
(*>*)

translations
  "P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩"  ==  "((e,s), e',s') ∈ eval P"
  "P \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩"  ==  "((es,s), es',s') ∈ evals P"
(*<*)
  "P \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩" <= "((e,h,l), e',h',l') ∈ eval P"
  "P \<turnstile> ⟨e,s⟩ => ⟨e',(h',l')⟩" <= "((e,s), e',h',l') ∈ eval P"
  "P \<turnstile> ⟨e,(h,l)⟩ => ⟨e',s'⟩" <= "((e,h,l), e',s') ∈ eval P"
  "P \<turnstile> ⟨e,(h,l)⟩ [=>] ⟨e',(h',l')⟩" <= "((e,h,l), e',h',l') ∈ evals P"
  "P \<turnstile> ⟨e,s⟩ [=>] ⟨e',(h',l')⟩" <= "((e,s), e',h',l') ∈ evals P"
  "P \<turnstile> ⟨e,(h,l)⟩ [=>] ⟨e',s'⟩" <= "((e,h,l), e',s') ∈ evals P"
(*>*)


inductive "eval P" "evals P"
intros

New:
  "[| new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>(C,init_fields FDTs)) |]
  ==> P \<turnstile> ⟨new C,(h,l)⟩ => ⟨addr a,(h',l)⟩"

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

Cast:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨addr a,(h,l)⟩; h a = Some(D,fs); P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨Cast C e,s0⟩ => ⟨addr a,(h,l)⟩"

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

CastFail:
  "[| P \<turnstile> ⟨e,s0⟩=> ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨Cast C e,s0⟩ => ⟨THROW ClassCast,(h,l)⟩"

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

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

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

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

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

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

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

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

FAcc:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨addr a,(h,l)⟩; h a = Some(C,fs); fs(F,D) = Some v |]
  ==> P \<turnstile> ⟨e\<bullet>F{D},s0⟩ => ⟨Val v,(h,l)⟩"

FAccNull:
  "P \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P \<turnstile> ⟨e\<bullet>F{D},s0⟩ => ⟨THROW NullPointer,s1⟩"

FAccThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨e\<bullet>F{D},s0⟩ => ⟨throw e',s1⟩"

FAss:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨addr a,s1⟩; P \<turnstile> ⟨e2,s1⟩ => ⟨Val v,(h2,l2)⟩;
     h2 a = Some(C,fs); fs' = fs((F,D)\<mapsto>v); h2' = h2(a\<mapsto>(C,fs')) |]
  ==> P \<turnstile> ⟨e1\<bullet>F{D}:=e2,s0⟩ => ⟨unit,(h2',l2)⟩"

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

FAssThrow1:
  "P \<turnstile> ⟨e1,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨e1\<bullet>F{D}:=e2,s0⟩ => ⟨throw e',s1⟩"

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

CallObjThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨e\<bullet>M(ps),s0⟩ => ⟨throw e',s1⟩"

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

CallNull:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩;  P \<turnstile> ⟨ps,s1⟩ [=>] ⟨map Val vs,s2⟩ |]
  ==> P \<turnstile> ⟨e\<bullet>M(ps),s0⟩ => ⟨THROW NullPointer,s2⟩"

Call:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨addr a,s1⟩;  P \<turnstile> ⟨ps,s1⟩ [=>] ⟨map Val vs,(h2,l2)⟩;
     h2 a = Some(C,fs);  P \<turnstile> C sees M:Ts->T = (pns,body) in D;
     length vs = length pns;  l2' = [this\<mapsto>Addr a, pns[\<mapsto>]vs];
     P \<turnstile> ⟨body,(h2,l2')⟩ => ⟨e',(h3,l3)⟩ |]
  ==> P \<turnstile> ⟨e\<bullet>M(ps),s0⟩ => ⟨e',(h3,l2)⟩"

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

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

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

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

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

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

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

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

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

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

Throw:
  "P \<turnstile> ⟨e,s0⟩ => ⟨addr a,s1⟩ ==>
  P \<turnstile> ⟨throw e,s0⟩ => ⟨Throw a,s1⟩"

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

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

Try:
  "P \<turnstile> ⟨e1,s0⟩ => ⟨Val v1,s1⟩ ==>
  P \<turnstile> ⟨try e1 catch(C V) e2,s0⟩ => ⟨Val v1,s1⟩"

TryCatch:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨Throw a,(h1,l1)⟩;  h1 a = Some(D,fs);  P \<turnstile> D \<preceq>* C;
     P \<turnstile> ⟨e2,(h1,l1(V\<mapsto>Addr a))⟩ => ⟨e2',(h2,l2)⟩ |]
  ==> P \<turnstile> ⟨try e1 catch(C V) e2,s0⟩ => ⟨e2',(h2,l2(V:=l1 V))⟩"

TryThrow:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨Throw a,(h1,l1)⟩;  h1 a = Some(D,fs);  ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨try e1 catch(C V) e2,s0⟩ => ⟨Throw a,(h1,l1)⟩"

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

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

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

(*<*)
lemmas eval_evals_induct = eval_evals.induct [split_format (complete)]

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


subsection"Final expressions"

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

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

lemma [simp]: "final(throw e) = (∃a. e = addr a)"
(*<*)by(simp add:final_def)(*>*)

lemma finalE: "[| final e;  !!v. e = Val v ==> R;  !!a. e = Throw a ==> R |] ==> R"
(*<*)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 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) = (∃a. e = addr a)"
(*<*)
apply(simp add:finals_def)
apply(rule iffI)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastsimp
apply clarsimp
apply(rule_tac x = "[]" in exI)
apply simp
done
(*>*)

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


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


lemma eval_lcl_incr: "P \<turnstile> ⟨e,(h0,l0)⟩ => ⟨e',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
 and evals_lcl_incr: "P \<turnstile> ⟨es,(h0,l0)⟩ [=>] ⟨es',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
(*<*)
proof (induct rule: eval_evals_induct)
  case BinOp show ?case by(rule subset_trans)
next
  case Call thus ?case
    by(simp del: fun_upd_apply) 
next
  case Seq show ?case by(rule subset_trans)
next
  case CondT show ?case by(rule subset_trans)
next
  case CondF show ?case by(rule subset_trans)
next
  case WhileT thus ?case by(blast)
next
  case TryCatch thus ?case by(clarsimp simp:dom_def split:split_if_asm) blast
next
  case Cons show ?case by(rule subset_trans)
next
  case Block thus ?case by(auto simp del:fun_upd_apply)
qed auto
(*>*)

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

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


lemma eval_finalsId:
assumes finals: "finals es" shows "P \<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 \<turnstile> ⟨es,s⟩ [=>] ⟨es,s⟩"
   and finals: "finals (e # es)".
  show "P \<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 \<turnstile> ⟨Val v,s⟩ => ⟨Val v,s⟩" by (simp add: eval_finalId)
      moreover from finals e have "P \<turnstile> ⟨es,s⟩ [=>] ⟨es,s⟩" by(fast intro:hyp)
      ultimately have "P \<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 \<turnstile> ⟨Throw a,s⟩ => ⟨Throw a,s⟩" by (simp add: eval_finalId)
      hence "P \<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
(*>*)


theorem eval_hext: "P \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> h \<unlhd> h'"
and evals_hext:  "P \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩ ==> h \<unlhd> h'"
(*<*)
proof (induct rule:eval_evals_induct)
  case New thus ?case
    by(fastsimp intro!: hext_new intro:someI simp:new_Addr_def
                split:split_if_asm simp del:fun_upd_apply)
next
  case BinOp thus ?case by (fast elim!:hext_trans)
next
  case BinOpThrow2 thus ?case by(fast elim!: hext_trans)
next
  case FAss thus ?case
    by(auto simp:sym[THEN hext_upd_obj] simp del:fun_upd_apply
            elim!: hext_trans)
next
  case FAssNull thus ?case by (fast elim!:hext_trans)
next
  case FAssThrow2 thus ?case by (fast elim!:hext_trans)
next
  case CallParamsThrow thus ?case by(fast elim!: hext_trans)
next
  case CallNull thus ?case by(fast elim!: hext_trans)
next
  case Call thus ?case by(fast elim!: hext_trans)
next
  case Seq thus ?case by(fast elim!: hext_trans)
next
  case CondT thus ?case by(fast elim!: hext_trans)
next
  case CondF thus ?case by(fast elim!: hext_trans)
next
  case WhileT thus ?case by(fast elim!: hext_trans)
next
  case WhileBodyThrow thus ?case by (fast elim!: hext_trans)
next
  case TryCatch thus ?case  by(fast elim!: hext_trans)
next
  case Cons thus ?case by (fast intro: hext_trans)
qed auto
(*>*)


end

lemmas eval_evals_induct:

  [| !!C FDTs a h h' l.
        [| new_Addr h = ⌊a⌋; P \<turnstile> C has_fields FDTs;
           h' = h(a |-> (C, init_fields FDTs)) |]
        ==> P1 (new C) h l (addr a) h' l;
     !!C h l. new_Addr h = None ==> P1 (new C) h l (THROW OutOfMemory) h l;
     !!C D a e fs h l aa b.
        [| eval P e (aa, b) (addr a) (h, l); P1 e aa b (addr a) h l;
           h a = ⌊(D, fs)⌋; subcls P D C |]
        ==> P1 (Cast C e) aa b (addr a) h l;
     !!C e a b aa ba.
        [| eval P e (a, b) null (aa, ba); P1 e a b null aa ba |]
        ==> P1 (Cast C e) a b null aa ba;
     !!C D a e fs h l aa b.
        [| eval P e (aa, b) (addr a) (h, l); P1 e aa b (addr a) h l;
           h a = ⌊(D, fs)⌋; ¬ subcls P D C |]
        ==> P1 (Cast C e) aa b (THROW ClassCast) h l;
     !!C e e' a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (Cast C e) a b (throw e') aa ba;
     !!a b v. P1 (Val v) a b (Val v) a b;
     !!bop e1 e2 a b aa ba ab bb v v1 v2.
        [| eval P e1 (a, b) (Val v1) (aa, ba); P1 e1 a b (Val v1) aa ba;
           eval P e2 (aa, ba) (Val v2) (ab, bb); P1 e2 aa ba (Val v2) ab bb;
           binop (bop, v1, v2) = ⌊v⌋ |]
        ==> P1 (e1 «bop» e2) a b (Val v) ab bb;
     !!bop e e1 e2 a b aa ba.
        [| eval P e1 (a, b) (throw e) (aa, ba); P1 e1 a b (throw e) aa ba |]
        ==> P1 (e1 «bop» e2) a b (throw e) aa ba;
     !!bop e e1 e2 a b aa ba ab bb v1.
        [| eval P e1 (a, b) (Val v1) (aa, ba); P1 e1 a b (Val v1) aa ba;
           eval P e2 (aa, ba) (throw e) (ab, bb); P1 e2 aa ba (throw e) ab bb |]
        ==> P1 (e1 «bop» e2) a b (throw e) ab bb;
     !!V h l v. l V = ⌊v⌋ ==> P1 (Var V) h l (Val v) h l;
     !!V e h l l' a b v.
        [| eval P e (a, b) (Val v) (h, l); P1 e a b (Val v) h l;
           l' = l(V |-> v) |]
        ==> P1 (V:=e) a b unit h l';
     !!V e e' a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (V:=e) a b (throw e') aa ba;
     !!C D F a e fs h l aa b v.
        [| eval P e (aa, b) (addr a) (h, l); P1 e aa b (addr a) h l;
           h a = ⌊(C, fs)⌋; fs (F, D) = ⌊v⌋ |]
        ==> P1 (e\<bullet>F{D}) aa b (Val v) h l;
     !!D F e a b aa ba.
        [| eval P e (a, b) null (aa, ba); P1 e a b null aa ba |]
        ==> P1 (e\<bullet>F{D}) a b (THROW NullPointer) aa ba;
     !!D F e e' a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (e\<bullet>F{D}) a b (throw e') aa ba;
     !!C D F a e1 e2 fs fs' h2 h2' l2 aa b ab ba v.
        [| eval P e1 (aa, b) (addr a) (ab, ba); P1 e1 aa b (addr a) ab ba;
           eval P e2 (ab, ba) (Val v) (h2, l2); P1 e2 ab ba (Val v) h2 l2;
           h2 a = ⌊(C, fs)⌋; fs' = fs((F, D) |-> v); h2' = h2(a |-> (C, fs')) |]
        ==> P1 (e1\<bullet>F{D} := e2) aa b unit h2' l2;
     !!D F e1 e2 a b aa ba ab bb v.
        [| eval P e1 (a, b) null (aa, ba); P1 e1 a b null aa ba;
           eval P e2 (aa, ba) (Val v) (ab, bb); P1 e2 aa ba (Val v) ab bb |]
        ==> P1 (e1\<bullet>F{D} := e2) a b (THROW NullPointer) ab bb;
     !!D F e' e1 e2 a b aa ba.
        [| eval P e1 (a, b) (throw e') (aa, ba); P1 e1 a b (throw e') aa ba |]
        ==> P1 (e1\<bullet>F{D} := e2) a b (throw e') aa ba;
     !!D F e' e1 e2 a b aa ba ab bb v.
        [| eval P e1 (a, b) (Val v) (aa, ba); P1 e1 a b (Val v) aa ba;
           eval P e2 (aa, ba) (throw e') (ab, bb); P1 e2 aa ba (throw e') ab bb |]
        ==> P1 (e1\<bullet>F{D} := e2) a b (throw e') ab bb;
     !!M e e' ps a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (e\<bullet>M(ps)) a b (throw e') aa ba;
     !!M e es es' ex a b aa ba ab bb v vs.
        [| eval P e (a, b) (Val v) (aa, ba); P1 e a b (Val v) aa ba;
           evals P es (aa, ba) (map Val vs @ throw ex # es') (ab, bb);
           P2 es aa ba (map Val vs @ throw ex # es') ab bb |]
        ==> P1 (e\<bullet>M(es)) a b (throw ex) ab bb;
     !!M e ps a b aa ba ab bb vs.
        [| eval P e (a, b) null (aa, ba); P1 e a b null aa ba;
           evals P ps (aa, ba) (map Val vs) (ab, bb);
           P2 ps aa ba (map Val vs) ab bb |]
        ==> P1 (e\<bullet>M(ps)) a b (THROW NullPointer) ab bb;
     !!C D M T Ts a body e e' fs h2 h3 l2 l2' l3 pns ps aa b ab ba vs.
        [| eval P e (aa, b) (addr a) (ab, ba); P1 e aa b (addr a) ab ba;
           evals P ps (ab, ba) (map Val vs) (h2, l2);
           P2 ps ab ba (map Val vs) h2 l2; h2 a = ⌊(C, fs)⌋;
           P \<turnstile> C sees M: Ts->T = (pns, body) in D;
           length vs = length pns; l2' = [this |-> Addr a, pns [|->] vs];
           eval P body (h2, l2') e' (h3, l3); P1 body h2 l2' e' h3 l3 |]
        ==> P1 (e\<bullet>M(ps)) aa b e' h3 l2;
     !!T V e0 e1 h0 h1 l0 l1.
        [| eval P e0 (h0, l0(V := None)) e1 (h1, l1);
           P1 e0 h0 (l0(V := None)) e1 h1 l1 |]
        ==> P1 {V:T; e0} h0 l0 e1 h1 (l1(V := l0 V));
     !!e0 e1 e2 a b aa ba ab bb v.
        [| eval P e0 (a, b) (Val v) (aa, ba); P1 e0 a b (Val v) aa ba;
           eval P e1 (aa, ba) e2 (ab, bb); P1 e1 aa ba e2 ab bb |]
        ==> P1 (e0;; e1) a b e2 ab bb;
     !!e e0 e1 a b aa ba.
        [| eval P e0 (a, b) (throw e) (aa, ba); P1 e0 a b (throw e) aa ba |]
        ==> P1 (e0;; e1) a b (throw e) aa ba;
     !!e e' e1 e2 a b aa ba ab bb.
        [| eval P e (a, b) true (aa, ba); P1 e a b true aa ba;
           eval P e1 (aa, ba) e' (ab, bb); P1 e1 aa ba e' ab bb |]
        ==> P1 (if (e) e1 else e2) a b e' ab bb;
     !!e e' e1 e2 a b aa ba ab bb.
        [| eval P e (a, b) false (aa, ba); P1 e a b false aa ba;
           eval P e2 (aa, ba) e' (ab, bb); P1 e2 aa ba e' ab bb |]
        ==> P1 (if (e) e1 else e2) a b e' ab bb;
     !!e e' e1 e2 a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (if (e) e1 else e2) a b (throw e') aa ba;
     !!c e a b aa ba.
        [| eval P e (a, b) false (aa, ba); P1 e a b false aa ba |]
        ==> P1 (while (e) c) a b unit aa ba;
     !!c e e3 a b aa ba ab bb ac bc v1.
        [| eval P e (a, b) true (aa, ba); P1 e a b true aa ba;
           eval P c (aa, ba) (Val v1) (ab, bb); P1 c aa ba (Val v1) ab bb;
           eval P (while (e) c) (ab, bb) e3 (ac, bc);
           P1 (while (e) c) ab bb e3 ac bc |]
        ==> P1 (while (e) c) a b e3 ac bc;
     !!c e e' a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (while (e) c) a b (throw e') aa ba;
     !!c e e' a b aa ba ab bb.
        [| eval P e (a, b) true (aa, ba); P1 e a b true aa ba;
           eval P c (aa, ba) (throw e') (ab, bb); P1 c aa ba (throw e') ab bb |]
        ==> P1 (while (e) c) a b (throw e') ab bb;
     !!a e aa b ab ba.
        [| eval P e (aa, b) (addr a) (ab, ba); P1 e aa b (addr a) ab ba |]
        ==> P1 (throw e) aa b (Throw a) ab ba;
     !!e a b aa ba.
        [| eval P e (a, b) null (aa, ba); P1 e a b null aa ba |]
        ==> P1 (throw e) a b (THROW NullPointer) aa ba;
     !!e e' a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (throw e) a b (throw e') aa ba;
     !!C V e1 e2 a b aa ba v1.
        [| eval P e1 (a, b) (Val v1) (aa, ba); P1 e1 a b (Val v1) aa ba |]
        ==> P1 (try e1 catch(C V) e2) a b (Val v1) aa ba;
     !!C D V a e1 e2 e2' fs h1 h2 l1 l2 aa b.
        [| eval P e1 (aa, b) (Throw a) (h1, l1); P1 e1 aa b (Throw a) h1 l1;
           h1 a = ⌊(D, fs)⌋; subcls P D C;
           eval P e2 (h1, l1(V |-> Addr a)) e2' (h2, l2);
           P1 e2 h1 (l1(V |-> Addr a)) e2' h2 l2 |]
        ==> P1 (try e1 catch(C V) e2) aa b e2' h2 (l2(V := l1 V));
     !!C D V a e1 e2 fs h1 l1 aa b.
        [| eval P e1 (aa, b) (Throw a) (h1, l1); P1 e1 aa b (Throw a) h1 l1;
           h1 a = ⌊(D, fs)⌋; ¬ subcls P D C |]
        ==> P1 (try e1 catch(C V) e2) aa b (Throw a) h1 l1;
     !!a b. P2 [] a b [] a b;
     !!e es es' a b aa ba ab bb v.
        [| eval P e (a, b) (Val v) (aa, ba); P1 e a b (Val v) aa ba;
           evals P es (aa, ba) es' (ab, bb); P2 es aa ba es' ab bb |]
        ==> P2 (e # es) a b (Val v # es') ab bb;
     !!e e' es a b aa ba.
        [| eval P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P2 (e # es) a b (throw e' # es) aa ba |]
  ==> (eval P xha (xga, xgb) xfa (xea, xeb) --> P1 xha xga xgb xfa xea xeb) &
      (evals P xda (xca, xcb) xba (xaa, xab) --> P2 xda xca xcb xba xaa xab)

lemmas eval_cases:

  [| eval P (Cast C e) s e' s';
     !!D a fs h l.
        [| eval P e s (addr a) (h, l); h a = ⌊(D, fs)⌋; subcls P D C; e' = addr a;
           s' = (h, l) |]
        ==> Pa;
     [| eval P e s null s'; e' = null |] ==> Pa;
     !!D a fs h l.
        [| eval P e s (addr a) (h, l); h a = ⌊(D, fs)⌋; ¬ subcls P D C;
           e' = THROW ClassCast; s' = (h, l) |]
        ==> Pa;
     !!e'a. [| eval P e s (throw e'a) s'; e' = throw e'a |] ==> Pa |]
  ==> Pa

  [| eval P (Val v) s e' s'; [| e' = Val v; s' = s |] ==> Pa |] ==> Pa

  [| eval P (e1 «bop» e2) s e' s';
     !!s1 v v1 v2.
        [| eval P e1 s (Val v1) s1; eval P e2 s1 (Val v2) s';
           binop (bop, v1, v2) = ⌊v⌋; e' = Val v |]
        ==> Pa;
     !!e. [| eval P e1 s (throw e) s'; e' = throw e |] ==> Pa;
     !!e s1 v1.
        [| eval P e1 s (Val v1) s1; eval P e2 s1 (throw e) s'; e' = throw e |]
        ==> Pa |]
  ==> Pa

  [| eval P (V:=e) s e' s';
     !!h l v.
        [| eval P e s (Val v) (h, l); e' = unit; s' = (h, l(V |-> v)) |] ==> Pa;
     !!e'a. [| eval P e s (throw e'a) s'; e' = throw e'a |] ==> Pa |]
  ==> Pa

  [| eval P (e\<bullet>F{D}) s e' s';
     !!C a fs h l v.
        [| eval P e s (addr a) (h, l); h a = ⌊(C, fs)⌋; fs (F, D) = ⌊v⌋;
           e' = Val v; s' = (h, l) |]
        ==> Pa;
     [| eval P e s null s'; e' = THROW NullPointer |] ==> Pa;
     !!e'a. [| eval P e s (throw e'a) s'; e' = throw e'a |] ==> Pa |]
  ==> Pa

  [| eval P (e1\<bullet>F{D} := e2) s e' s';
     !!C a fs h2 l2 s1 v.
        [| eval P e1 s (addr a) s1; eval P e2 s1 (Val v) (h2, l2);
           h2 a = ⌊(C, fs)⌋; e' = unit;
           s' = (h2(a |-> (C, fs((F, D) |-> v))), l2) |]
        ==> Pa;
     !!s1 v.
        [| eval P e1 s null s1; eval P e2 s1 (Val v) s'; e' = THROW NullPointer |]
        ==> Pa;
     !!e'a. [| eval P e1 s (throw e'a) s'; e' = throw e'a |] ==> Pa;
     !!e'a s1 v.
        [| eval P e1 s (Val v) s1; eval P e2 s1 (throw e'a) s'; e' = throw e'a |]
        ==> Pa |]
  ==> Pa

  [| eval P (e\<bullet>M {D}(es)) s e' s';
     !!e'a. [| eval P e s (throw e'a) s'; e' = throw e'a |] ==> Pa;
     !!es' ex s1 v vs.
        [| eval P e s (Val v) s1; evals P es s1 (map Val vs @ throw ex # es') s';
           e' = throw ex |]
        ==> Pa;
     !!s1 vs.
        [| eval P e s null s1; evals P es s1 (map Val vs) s';
           e' = THROW NullPointer |]
        ==> Pa;
     !!C Da T Ts a body fs h2 h3 l2 l3 pns s1 vs.
        [| eval P e s (addr a) s1; evals P es s1 (map Val vs) (h2, l2);
           h2 a = ⌊(C, fs)⌋;
           P \<turnstile> C sees M {D}: Ts->T = (pns, body) in Da;
           length vs = length pns;
           eval P body (h2, [this |-> Addr a, pns [|->] vs]) e' (h3, l3);
           s' = (h3, l2) |]
        ==> Pa |]
  ==> Pa

  [| eval P {V:T; e1} s e' s';
     !!h0 h1 l0 l1.
        [| eval P e1 (h0, l0(V := None)) e' (h1, l1); s = (h0, l0);
           s' = (h1, l1(V := l0 V)) |]
        ==> Pa |]
  ==> Pa

  [| eval P (e1;; e2) s e' s';
     !!s1 v. [| eval P e1 s (Val v) s1; eval P e2 s1 e' s' |] ==> Pa;
     !!e. [| eval P e1 s (throw e) s'; e' = throw e |] ==> Pa |]
  ==> Pa

  [| eval P (if (e) e1 else e2) s e' s';
     !!s1. [| eval P e s true s1; eval P e1 s1 e' s' |] ==> Pa;
     !!s1. [| eval P e s false s1; eval P e2 s1 e' s' |] ==> Pa;
     !!e'a. [| eval P e s (throw e'a) s'; e' = throw e'a |] ==> Pa |]
  ==> Pa

  [| eval P (while (b) c) s e' s'; [| eval P b s false s'; e' = unit |] ==> Pa;
     !!s1 s2 v1.
        [| eval P b s true s1; eval P c s1 (Val v1) s2;
           eval P (while (b) c) s2 e' s' |]
        ==> Pa;
     !!e'a. [| eval P b s (throw e'a) s'; e' = throw e'a |] ==> Pa;
     !!e'a s1.
        [| eval P b s true s1; eval P c s1 (throw e'a) s'; e' = throw e'a |]
        ==> Pa |]
  ==> Pa

  [| eval P (throw e) s e' s';
     !!a. [| eval P e s (addr a) s'; e' = Throw a |] ==> Pa;
     [| eval P e s null s'; e' = THROW NullPointer |] ==> Pa;
     !!e'a. [| eval P e s (throw e'a) s'; e' = throw e'a |] ==> Pa |]
  ==> Pa

  [| eval P (try e1 catch(C V) e2) s e' s';
     !!v1. [| eval P e1 s (Val v1) s'; e' = Val v1 |] ==> Pa;
     !!D a fs h1 h2 l1 l2.
        [| eval P e1 s (Throw a) (h1, l1); h1 a = ⌊(D, fs)⌋; subcls P D C;
           eval P e2 (h1, l1(V |-> Addr a)) e' (h2, l2);
           s' = (h2, l2(V := l1 V)) |]
        ==> Pa;
     !!D a fs h1 l1.
        [| eval P e1 s (Throw a) (h1, l1); h1 a = ⌊(D, fs)⌋; ¬ subcls P D C;
           e' = Throw a; s' = (h1, l1) |]
        ==> Pa |]
  ==> Pa

lemmas evals_cases:

  [| evals P [] s e' s'; [| e' = []; s' = s |] ==> Pa |] ==> Pa

  [| evals P (e # es) s e' s';
     !!es' s1 v.
        [| eval P e s (Val v) s1; evals P es s1 es' s'; e' = Val v # es' |]
        ==> Pa;
     !!e'a. [| eval P e s (throw e'a) s'; e' = throw e'a # es |] ==> Pa |]
  ==> Pa

Final expressions

lemma

  final (Val v)

lemma

  final (throw e) = (EX a. e = addr a)

lemma finalE:

  [| final e; !!v. e = Val v ==> R; !!a. e = Throw a ==> R |] ==> R

lemma

  finals []

lemma

  finals (Val v # es) = finals es

lemma finals_app_map:

  finals (map Val vs @ es) = finals es

lemma

  finals (map Val vs)

lemma

  finals (throw e # es) = (EX a. e = addr a)

lemma not_finals_ConsI:

  ¬ final e ==> ¬ finals (e # es)

lemma eval_final:

  eval P e s e' s' ==> final e'

and evals_final:

  evals P es s es' s' ==> finals es'

lemma eval_lcl_incr:

  eval P e (h0, l0) e' (h1, l1) ==> dom l0 <= dom l1

and evals_lcl_incr:

  evals P es (h0, l0) es' (h1, l1) ==> dom l0 <= dom l1

lemma eval_finalId:

  final e ==> eval P e s e s

lemma

  finals es ==> evals P es s es s

theorem eval_hext:

  eval P e (h, l) e' (h', l') ==> h \<unlhd> h'

and evals_hext:

  evals P es (h, l) es' (h', l') ==> h \<unlhd> h'