Theory J1

Up to index of Isabelle/HOL/Jinja

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

header {* \chapter{Compilation}\label{cha:comp}
          \isaheader{An Intermediate Language} *}

theory J1 = BigStep:

types
  expr1 = "nat exp"
  J1_prog = "expr1 prog"

  state1 = "heap × (val list)"

consts
  max_vars:: "'a exp => nat"
  max_varss:: "'a exp list => nat"
primrec
"max_vars(new C) = 0"
"max_vars(Cast C e) = max_vars e"
"max_vars(Val v) = 0"
"max_vars(e1 «bop» e2) = max (max_vars e1) (max_vars e2)"
"max_vars(Var V) = 0"
"max_vars(V:=e) = max_vars e"
"max_vars(e\<bullet>F{D}) = max_vars e"
"max_vars(FAss e1 F D e2) = max (max_vars e1) (max_vars e2)"
"max_vars(e\<bullet>M(es)) = max (max_vars e) (max_varss es)"
"max_vars({V:T; e}) = max_vars e + 1"
"max_vars(e1;;e2) = max (max_vars e1) (max_vars e2)"
"max_vars(if (e) e1 else e2) =
   max (max_vars e) (max (max_vars e1) (max_vars e2))"
"max_vars(while (b) e) = max (max_vars b) (max_vars e)"
"max_vars(throw e) = max_vars e"
"max_vars(try e1 catch(C V) e2) = max (max_vars e1) (max_vars e2 + 1)"

"max_varss [] = 0"
"max_varss (e#es) = max (max_vars e) (max_varss es)"

consts
  eval1  :: "J1_prog => ((expr1 × state1) × (expr1 × state1)) set"
  evals1  :: "J1_prog => ((expr1 list × state1) × (expr1 list × state1)) set"

(*<*)
syntax (xsymbols)
  eval1 :: "J1_prog => expr => state1 => nat => expr => state1 => bool"
          ("_ \<turnstile>1 ((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  evals1 :: "J1_prog => expr list => state1 => nat => expr list => state1 => bool"
           ("_ \<turnstile>1 ((1⟨_,/_⟩) [=>]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
(*>*)

translations
  "P \<turnstile>1 ⟨e,s⟩ => ⟨e',s'⟩" == "((e,s), e',s') ∈ eval1 P"
  "P \<turnstile>1 ⟨e,s⟩ [=>] ⟨e',s'⟩" == "((e,s), e',s') ∈ evals1 P"
(*<*)
  "P \<turnstile>1 ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩" <= "((e,h,l), e',h',l') ∈ eval1 P"
  "P \<turnstile>1 ⟨e,s⟩ => ⟨e',(h',l')⟩" <= "((e,s), e',h',l') ∈ eval1 P"
  "P \<turnstile>1 ⟨e,(h,l)⟩ => ⟨e',s'⟩" <= "((e,h,l), e',s') ∈ eval1 P"
  "P \<turnstile>1 ⟨e,(h,l)⟩ [=>] ⟨e',(h',l')⟩" <= "((e,h,l), e',h',l') ∈ evals1 P"
  "P \<turnstile>1 ⟨e,s⟩ [=>] ⟨e',(h',l')⟩" <= "((e,s), e',h',l') ∈ evals1 P"
  "P \<turnstile>1 ⟨e,(h,l)⟩ [=>] ⟨e',s'⟩" <= "((e,h,l), e',s') ∈ evals1 P"
(*>*)


inductive "eval1 P" "evals1 P"
intros

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

Cast1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨addr a,(h,l)⟩; h a = Some(D,fs); P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile>1 ⟨Cast C e,s0⟩ => ⟨addr a,(h,l)⟩"
CastNull1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P \<turnstile>1 ⟨Cast C e,s0⟩ => ⟨null,s1⟩"
CastFail1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile>1 ⟨Cast C e,s0⟩ => ⟨THROW ClassCast,(h,l)⟩"
CastThrow1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨Cast C e,s0⟩ => ⟨throw e',s1⟩"

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

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

Var1:
  "[| ls!i = v; i < size ls |] ==>
  P \<turnstile>1 ⟨Var i,(h,ls)⟩ => ⟨Val v,(h,ls)⟩"

LAss1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨Val v,(h,ls)⟩; i < size ls; ls' = ls[i := v] |]
  ==> P \<turnstile>1 ⟨i:= e,s0⟩ => ⟨unit,(h,ls')⟩"
LAssThrow1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨i:= e,s0⟩ => ⟨throw e',s1⟩"

FAcc1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨addr a,(h,ls)⟩; h a = Some(C,fs); fs(F,D) = Some v |]
  ==> P \<turnstile>1 ⟨e\<bullet>F{D},s0⟩ => ⟨Val v,(h,ls)⟩"
FAccNull1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P \<turnstile>1 ⟨e\<bullet>F{D},s0⟩ => ⟨THROW NullPointer,s1⟩"
FAccThrow1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨e\<bullet>F{D},s0⟩ => ⟨throw e',s1⟩"

FAss1:
  "[| P \<turnstile>1 ⟨e1,s0⟩ => ⟨addr a,s1⟩; P \<turnstile>1 ⟨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>1 ⟨e1\<bullet>F{D}:= e2,s0⟩ => ⟨unit,(h2',l2)⟩"
FAssNull1:
  "[| P \<turnstile>1 ⟨e1,s0⟩ => ⟨null,s1⟩;  P \<turnstile>1 ⟨e2,s1⟩ => ⟨Val v,s2⟩ |]
  ==> P \<turnstile>1 ⟨e1\<bullet>F{D}:= e2,s0⟩ => ⟨THROW NullPointer,s2⟩"
FAssThrow11:
  "P \<turnstile>1 ⟨e1,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨e1\<bullet>F{D}:= e2,s0⟩ => ⟨throw e',s1⟩"
FAssThrow21:
  "[| P \<turnstile>1 ⟨e1,s0⟩ => ⟨Val v,s1⟩; P \<turnstile>1 ⟨e2,s1⟩ => ⟨throw e',s2⟩ |]
  ==> P \<turnstile>1 ⟨e1\<bullet>F{D}:= e2,s0⟩ => ⟨throw e',s2⟩"

CallObjThrow1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨e\<bullet>M(es),s0⟩ => ⟨throw e',s1⟩"
CallNull1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨null,s1⟩; P \<turnstile>1 ⟨es,s1⟩ [=>] ⟨map Val vs,s2⟩ |]
  ==> P \<turnstile>1 ⟨e\<bullet>M(es),s0⟩ => ⟨THROW NullPointer,s2⟩"
Call1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨addr a,s1⟩; P \<turnstile>1 ⟨es,s1⟩ [=>] ⟨map Val vs,(h2,ls2)⟩;
    h2 a = Some(C,fs); P \<turnstile> C sees M:Ts->T = body in D;
    size vs = size Ts; ls2' = (Addr a) # vs @ replicate (max_vars body) arbitrary;
    P \<turnstile>1 ⟨body,(h2,ls2')⟩ => ⟨e',(h3,ls3)⟩ |]
  ==> P \<turnstile>1 ⟨e\<bullet>M(es),s0⟩ => ⟨e',(h3,ls2)⟩"
CallParamsThrow1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨Val v,s1⟩; P \<turnstile>1 ⟨es,s1⟩ [=>] ⟨es',s2⟩;
     es' = map Val vs @ throw ex # es2 |]
   ==> P \<turnstile>1 ⟨e\<bullet>M(es),s0⟩ => ⟨throw ex,s2⟩"

Block1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨f,s1⟩ ==> P \<turnstile>1 ⟨Block i T e,s0⟩ => ⟨f,s1⟩"

Seq1:
  "[| P \<turnstile>1 ⟨e0,s0⟩ => ⟨Val v,s1⟩; P \<turnstile>1 ⟨e1,s1⟩ => ⟨e2,s2⟩ |]
  ==> P \<turnstile>1 ⟨e0;;e1,s0⟩ => ⟨e2,s2⟩"
SeqThrow1:
  "P \<turnstile>1 ⟨e0,s0⟩ => ⟨throw e,s1⟩ ==>
  P \<turnstile>1 ⟨e0;;e1,s0⟩ => ⟨throw e,s1⟩"

CondT1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨true,s1⟩; P \<turnstile>1 ⟨e1,s1⟩ => ⟨e',s2⟩ |]
  ==> P \<turnstile>1 ⟨if (e) e1 else e2,s0⟩ => ⟨e',s2⟩"
CondF1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨false,s1⟩; P \<turnstile>1 ⟨e2,s1⟩ => ⟨e',s2⟩ |]
  ==> P \<turnstile>1 ⟨if (e) e1 else e2,s0⟩ => ⟨e',s2⟩"
CondThrow1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨if (e) e1 else e2, s0⟩ => ⟨throw e',s1⟩"

WhileF1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨false,s1⟩ ==>
  P \<turnstile>1 ⟨while (e) c,s0⟩ => ⟨unit,s1⟩"
WhileT1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨true,s1⟩; P \<turnstile>1 ⟨c,s1⟩ => ⟨Val v1,s2⟩;
    P \<turnstile>1 ⟨while (e) c,s2⟩ => ⟨e3,s3⟩ |]
  ==> P \<turnstile>1 ⟨while (e) c,s0⟩ => ⟨e3,s3⟩"
WhileCondThrow1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨while (e) c,s0⟩ => ⟨throw e',s1⟩"
WhileBodyThrow1:
  "[| P \<turnstile>1 ⟨e,s0⟩ => ⟨true,s1⟩; P \<turnstile>1 ⟨c,s1⟩ => ⟨throw e',s2⟩|]
  ==> P \<turnstile>1 ⟨while (e) c,s0⟩ => ⟨throw e',s2⟩"

Throw1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨addr a,s1⟩ ==>
  P \<turnstile>1 ⟨throw e,s0⟩ => ⟨Throw a,s1⟩"
ThrowNull1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P \<turnstile>1 ⟨throw e,s0⟩ => ⟨THROW NullPointer,s1⟩"
ThrowThrow1:
  "P \<turnstile>1 ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile>1 ⟨throw e,s0⟩ => ⟨throw e',s1⟩"

Try1:
  "P \<turnstile>1 ⟨e1,s0⟩ => ⟨Val v1,s1⟩ ==>
  P \<turnstile>1 ⟨try e1 catch(C i) e2,s0⟩ => ⟨Val v1,s1⟩"
TryCatch1:
  "[| P \<turnstile>1 ⟨e1,s0⟩ => ⟨Throw a,(h1,ls1)⟩;
    h1 a = Some(D,fs); P \<turnstile> D \<preceq>* C; i < length ls1;
    P \<turnstile>1 ⟨e2,(h1,ls1[i:=Addr a])⟩ => ⟨e2',(h2,ls2)⟩ |]
  ==> P \<turnstile>1 ⟨try e1 catch(C i) e2,s0⟩ => ⟨e2',(h2,ls2)⟩"
TryThrow1:
  "[| P \<turnstile>1 ⟨e1,s0⟩ => ⟨Throw a,(h1,ls1)⟩; h1 a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile>1 ⟨try e1 catch(C i) e2,s0⟩ => ⟨Throw a,(h1,ls1)⟩"

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

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

(*<*)
lemmas eval1_evals1_induct = eval1_evals1.induct [split_format (complete)]
(*>*)

lemma eval1_preserves_len:
  "P \<turnstile>1 ⟨e0,(h0,ls0)⟩ => ⟨e1,(h1,ls1)⟩ ==> length ls0 = length ls1"
and evals1_preserves_len:
  "P \<turnstile>1 ⟨es0,(h0,ls0)⟩ [=>] ⟨es1,(h1,ls1)⟩ ==> length ls0 = length ls1"
(*<*)by (induct rule:eval1_evals1_induct, simp_all)(*>*)


lemma evals1_preserves_elen:
  "!!es' s s'. P \<turnstile>1 ⟨es,s⟩ [=>] ⟨es',s'⟩ ==> length es = length es'"
(*<*)
apply(induct es type:list)
apply (auto elim:eval1_evals1.elims)
done
(*>*)


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


end

lemmas eval1_evals1_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.
        [| eval1 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.
        [| eval1 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.
        [| eval1 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.
        [| eval1 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.
        [| eval1 P e1 (a, b) (Val v1) (aa, ba); P1 e1 a b (Val v1) aa ba;
           eval1 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.
        [| eval1 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.
        [| eval1 P e1 (a, b) (Val v1) (aa, ba); P1 e1 a b (Val v1) aa ba;
           eval1 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;
     !!h i ls v. [| ls ! i = v; i < length ls |] ==> P1 (Var i) h ls (Val v) h ls;
     !!e h i ls ls' a b v.
        [| eval1 P e (a, b) (Val v) (h, ls); P1 e a b (Val v) h ls; i < length ls;
           ls' = ls[i := v] |]
        ==> P1 (i:=e) a b unit h ls';
     !!e e' i a b aa ba.
        [| eval1 P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (i:=e) a b (throw e') aa ba;
     !!C D F a e fs h ls aa b v.
        [| eval1 P e (aa, b) (addr a) (h, ls); P1 e aa b (addr a) h ls;
           h a = ⌊(C, fs)⌋; fs (F, D) = ⌊v⌋ |]
        ==> P1 (e\<bullet>F{D}) aa b (Val v) h ls;
     !!D F e a b aa ba.
        [| eval1 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.
        [| eval1 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.
        [| eval1 P e1 (aa, b) (addr a) (ab, ba); P1 e1 aa b (addr a) ab ba;
           eval1 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.
        [| eval1 P e1 (a, b) null (aa, ba); P1 e1 a b null aa ba;
           eval1 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.
        [| eval1 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.
        [| eval1 P e1 (a, b) (Val v) (aa, ba); P1 e1 a b (Val v) aa ba;
           eval1 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' es a b aa ba.
        [| eval1 P e (a, b) (throw e') (aa, ba); P1 e a b (throw e') aa ba |]
        ==> P1 (e\<bullet>M(es)) a b (throw e') aa ba;
     !!M e es a b aa ba ab bb vs.
        [| eval1 P e (a, b) null (aa, ba); P1 e a b null aa ba;
           evals1 P es (aa, ba) (map Val vs) (ab, bb);
           P2 es aa ba (map Val vs) ab bb |]
        ==> P1 (e\<bullet>M(es)) a b (THROW NullPointer) ab bb;
     !!C D M T Ts a body e e' es fs h2 h3 ls2 ls2' ls3 aa b ab ba vs.
        [| eval1 P e (aa, b) (addr a) (ab, ba); P1 e aa b (addr a) ab ba;
           evals1 P es (ab, ba) (map Val vs) (h2, ls2);
           P2 es ab ba (map Val vs) h2 ls2; h2 a = ⌊(C, fs)⌋;
           P \<turnstile> C sees M: Ts->T = body in D; length vs = length Ts;
           ls2' = Addr a # vs @ replicate (max_vars body) arbitrary;
           eval1 P body (h2, ls2') e' (h3, ls3); P1 body h2 ls2' e' h3 ls3 |]
        ==> P1 (e\<bullet>M(es)) aa b e' h3 ls2;
     !!M e es es' es2 ex a b aa ba ab bb v vs.
        [| eval1 P e (a, b) (Val v) (aa, ba); P1 e a b (Val v) aa ba;
           evals1 P es (aa, ba) es' (ab, bb); P2 es aa ba es' ab bb;
           es' = map Val vs @ throw ex # es2 |]
        ==> P1 (e\<bullet>M(es)) a b (throw ex) ab bb;
     !!T e f i a b aa ba.
        [| eval1 P e (a, b) f (aa, ba); P1 e a b f aa ba |]
        ==> P1 {i:T; e} a b f aa ba;
     !!e0 e1 e2 a b aa ba ab bb v.
        [| eval1 P e0 (a, b) (Val v) (aa, ba); P1 e0 a b (Val v) aa ba;
           eval1 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.
        [| eval1 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.
        [| eval1 P e (a, b) true (aa, ba); P1 e a b true aa ba;
           eval1 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.
        [| eval1 P e (a, b) false (aa, ba); P1 e a b false aa ba;
           eval1 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.
        [| eval1 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.
        [| eval1 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.
        [| eval1 P e (a, b) true (aa, ba); P1 e a b true aa ba;
           eval1 P c (aa, ba) (Val v1) (ab, bb); P1 c aa ba (Val v1) ab bb;
           eval1 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.
        [| eval1 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.
        [| eval1 P e (a, b) true (aa, ba); P1 e a b true aa ba;
           eval1 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.
        [| eval1 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.
        [| eval1 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.
        [| eval1 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 e1 e2 i a b aa ba v1.
        [| eval1 P e1 (a, b) (Val v1) (aa, ba); P1 e1 a b (Val v1) aa ba |]
        ==> P1 (try e1 catch(C i) e2) a b (Val v1) aa ba;
     !!C D a e1 e2 e2' fs h1 h2 i ls1 ls2 aa b.
        [| eval1 P e1 (aa, b) (Throw a) (h1, ls1); P1 e1 aa b (Throw a) h1 ls1;
           h1 a = ⌊(D, fs)⌋; subcls P D C; i < length ls1;
           eval1 P e2 (h1, ls1[i := Addr a]) e2' (h2, ls2);
           P1 e2 h1 (ls1[i := Addr a]) e2' h2 ls2 |]
        ==> P1 (try e1 catch(C i) e2) aa b e2' h2 ls2;
     !!C D a e1 e2 fs h1 i ls1 aa b.
        [| eval1 P e1 (aa, b) (Throw a) (h1, ls1); P1 e1 aa b (Throw a) h1 ls1;
           h1 a = ⌊(D, fs)⌋; ¬ subcls P D C |]
        ==> P1 (try e1 catch(C i) e2) aa b (Throw a) h1 ls1;
     !!a b. P2 [] a b [] a b;
     !!e es es' a b aa ba ab bb v.
        [| eval1 P e (a, b) (Val v) (aa, ba); P1 e a b (Val v) aa ba;
           evals1 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.
        [| eval1 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 |]
  ==> (eval1 P xha (xga, xgb) xfa (xea, xeb) --> P1 xha xga xgb xfa xea xeb) &
      (evals1 P xda (xca, xcb) xba (xaa, xab) --> P2 xda xca xcb xba xaa xab)

lemma eval1_preserves_len: 

  eval1 P e0 (h0, ls0) e1 (h1, ls1) ==> length ls0 = length ls1

and evals1_preserves_len: 

  evals1 P es0 (h0, ls0) es1 (h1, ls1) ==> length ls0 = length ls1

lemma evals1_preserves_elen: 

  evals1 P es s es' s' ==> length es = length es'

lemma eval1_final: 

  eval1 P e s e' s' ==> final e'

and evals1_final: 

  evals1 P es s es' s' ==> finals es'