# Theory Correctness1

(*  Title:      JinjaDCI/Compiler/Correctness1.thy
Author:     Tobias Nipkow, Susannah Mansky
Copyright   TUM 2003, UIUC 2019-20

Based on the Jinja theory Compiler/Correctness1.thy by Tobias Nipkow
*)

section ‹ Correctness of Stage 1 ›

theory Correctness1
imports J1WellForm Compiler1
begin

subsection‹Correctness of program compilation ›

primrec unmod :: "expr⇩1 ⇒ nat ⇒ bool"
and unmods :: "expr⇩1 list ⇒ nat ⇒ bool" where
"unmod (new C) i = True" |
"unmod (Cast C e) i = unmod e i" |
"unmod (Val v) i = True" |
"unmod (e⇩1 «bop» e⇩2) i = (unmod e⇩1 i ∧ unmod e⇩2 i)" |
"unmod (Var i) j = True" |
"unmod (i:=e) j = (i ≠ j ∧ unmod e j)" |
"unmod (e∙F{D}) i = unmod e i" |
"unmod (C∙⇩sF{D}) i = True" |
"unmod (e⇩1∙F{D}:=e⇩2) i = (unmod e⇩1 i ∧ unmod e⇩2 i)" |
"unmod (C∙⇩sF{D}:=e⇩2) i = unmod e⇩2 i" |
"unmod (e∙M(es)) i = (unmod e i ∧ unmods es i)" |
"unmod (C∙⇩sM(es)) i = unmods es i" |
"unmod {j:T; e} i = unmod e i" |
"unmod (e⇩1;;e⇩2) i = (unmod e⇩1 i ∧  unmod e⇩2 i)" |
"unmod (if (e) e⇩1 else e⇩2) i = (unmod e i ∧ unmod e⇩1 i ∧ unmod e⇩2 i)" |
"unmod (while (e) c) i = (unmod e i ∧ unmod c i)" |
"unmod (throw e) i = unmod e i" |
"unmod (try e⇩1 catch(C i) e⇩2) j = (unmod e⇩1 j ∧ (if i=j then False else unmod e⇩2 j))" |
"unmod (INIT C (Cs,b) ← e) i = unmod e i" |
"unmod (RI(C,e);Cs ← e') i = (unmod e i ∧ unmod e' i)" |

"unmods ([]) i = True" |
"unmods (e#es) i = (unmod e i ∧ unmods es i)"

lemma hidden_unmod: "⋀Vs. hidden Vs i ⟹ unmod (compE⇩1 Vs e) i" and
"⋀Vs. hidden Vs i ⟹ unmods (compEs⇩1 Vs es) i"
(*<*)
proof(induct e and es rule: compE⇩1.induct compEs⇩1.induct)
case TryCatch
then show ?case by(simp add:hidden_inacc)(auto simp add:hidden_def)
qed (simp_all add:hidden_inacc)
(*>*)

lemma eval⇩1_preserves_unmod:
"⟦ P ⊢⇩1 ⟨e,(h,ls,sh)⟩ ⇒ ⟨e',(h',ls',sh')⟩; unmod e i; i < size ls ⟧
⟹ ls ! i = ls' ! i"
and "⟦ P ⊢⇩1 ⟨es,(h,ls,sh)⟩ [⇒] ⟨es',(h',ls',sh')⟩; unmods es i; i < size ls ⟧
⟹ ls ! i = ls' ! i"
(*<*)
proof(induct rule:eval⇩1_evals⇩1_inducts)
case (RInitInitFail⇩1 e h l sh a h' l' sh' C sfs i sh'' D Cs e⇩1 h⇩1 l⇩1 sh⇩1)
have "final (throw a)" using eval⇩1_final[OF RInitInitFail⇩1.hyps(1)] by simp
then show ?case using RInitInitFail⇩1 by(auto simp: eval⇩1_preserves_len)
qed(auto dest!:eval⇩1_preserves_len evals⇩1_preserves_len split:if_split_asm)
(*>*)

lemma LAss_lem:
"⟦x ∈ set xs; size xs ≤ size ys ⟧
⟹ m⇩1 ⊆⇩m m⇩2(xs[↦]ys) ⟹ m⇩1(x↦y) ⊆⇩m m⇩2(xs[↦]ys[last_index xs x := y])"
(*<*)
by(simp add:map_le_def fun_upds_apply eq_sym_conv)
(*>*)
lemma Block_lem:
fixes l :: "'a ⇀ 'b"
assumes 0: "l ⊆⇩m [Vs [↦] ls]"
and 1: "l' ⊆⇩m [Vs [↦] ls', V↦v]"
and hidden: "V ∈ set Vs ⟹ ls ! last_index Vs V = ls' ! last_index Vs V"
and size: "size ls = size ls'"    "size Vs < size ls'"
shows "l'(V := l V) ⊆⇩m [Vs [↦] ls']"
(*<*)
proof -
have "l'(V := l V) ⊆⇩m [Vs [↦] ls', V↦v](V := l V)"
using 1 by(rule map_le_upd)
also have "… = [Vs [↦] ls'](V := l V)" by simp
also have "… ⊆⇩m [Vs [↦] ls']"
proof (cases "l V")
case None thus ?thesis by simp
next
case (Some w)
hence "[Vs [↦] ls] V = Some w"
using 0 by(force simp add: map_le_def split:if_splits)
hence VinVs: "V ∈ set Vs" and w: "w = ls ! last_index Vs V"
using size by(auto simp add:fun_upds_apply split:if_splits)
hence "w = ls' ! last_index Vs V" using hidden[OF VinVs] by simp
hence "[Vs [↦] ls'](V := l V) = [Vs [↦] ls']" using Some size VinVs
by(simp add: map_upds_upd_conv_last_index)
thus ?thesis by simp
qed
finally show ?thesis .
qed
(*>*)

(*<*)
declare fun_upd_apply[simp del]
(*>*)

text‹\noindent The main theorem: ›

theorem assumes wf: "wwf_J_prog P"
shows eval⇩1_eval: "P ⊢ ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩
⟹ (⋀Vs ls. ⟦ fv e ⊆ set Vs;  l ⊆⇩m [Vs[↦]ls]; size Vs + max_vars e ≤ size ls ⟧
⟹ ∃ls'. compP⇩1 P ⊢⇩1 ⟨compE⇩1 Vs e,(h,ls,sh)⟩ ⇒ ⟨fin⇩1 e',(h',ls',sh')⟩ ∧ l' ⊆⇩m [Vs[↦]ls'])"
(*<*)
(is "_ ⟹ (⋀Vs ls. PROP ?P e h l sh e' h' l' sh' Vs ls)"
is "_ ⟹ (⋀Vs ls. ⟦ _; _; _ ⟧ ⟹ ∃ls'. ?Post e h l sh e' h' l' sh' Vs ls ls')")
(*>*)

and evals⇩1_evals: "P ⊢ ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩
⟹ (⋀Vs ls. ⟦ fvs es ⊆ set Vs;  l ⊆⇩m [Vs[↦]ls]; size Vs + max_varss es ≤ size ls ⟧
⟹ ∃ls'. compP⇩1 P ⊢⇩1 ⟨compEs⇩1 Vs es,(h,ls,sh)⟩ [⇒] ⟨compEs⇩1 Vs es',(h',ls',sh')⟩ ∧
l' ⊆⇩m [Vs[↦]ls'])"
(*<*)
(is "_ ⟹ (⋀Vs ls. PROP ?Ps es h l sh es' h' l' sh' Vs ls)"
is "_ ⟹ (⋀Vs ls. ⟦ _; _; _⟧ ⟹ ∃ls'. ?Posts es h l sh es' h' l' sh' Vs ls ls')")
proof (induct rule:eval_evals_inducts)
case Nil thus ?case by(fastforce intro!:Nil⇩1)
next
case (Cons e h l sh v h' l' sh' es es' h⇩2 l⇩2 sh⇩2)
have "PROP ?P e h l sh (Val v) h' l' sh' Vs ls" by fact
with Cons.prems
obtain ls' where 1: "?Post e h l sh (Val v) h' l' sh' Vs ls ls'"
"size ls = size ls'" by(auto intro!:eval⇩1_preserves_len)
have "PROP ?Ps es h' l' sh' es' h⇩2 l⇩2 sh⇩2 Vs ls'" by fact
with 1 Cons.prems
obtain ls⇩2 where 2: "?Posts es h' l' sh' es' h⇩2 l⇩2 sh⇩2 Vs ls' ls⇩2" by(auto)
from 1 2 Cons show ?case by(auto intro!:Cons⇩1)
next
case ConsThrow thus ?case
by(fastforce intro!:ConsThrow⇩1 dest: eval_final)
next
case (Block e h l V sh e' h' l' sh' T)
let ?Vs = "Vs @ [V]"
have IH:
"⟦fv e ⊆ set ?Vs; l(V := None) ⊆⇩m [?Vs [↦] ls];
size ?Vs + max_vars e ≤ size ls⟧
⟹ ∃ls'. compP⇩1 P ⊢⇩1 ⟨compE⇩1 ?Vs e,(h,ls,sh)⟩ ⇒ ⟨fin⇩1 e',(h', ls',sh')⟩ ∧
l' ⊆⇩m [?Vs [↦] ls']" and
fv: "fv {V:T; e} ⊆ set Vs" and rel: "l ⊆⇩m [Vs [↦] ls]" and
len: "length Vs + max_vars {V:T; e} ≤ length ls" by fact+
have len': "length Vs < length ls" using len by auto
have "fv e ⊆ set ?Vs" using fv by auto
moreover have "l(V := None) ⊆⇩m [?Vs [↦] ls]" using rel len' by simp
moreover have "size ?Vs + max_vars e ≤ size ls" using len by simp
ultimately obtain ls' where
1: "compP⇩1 P ⊢⇩1 ⟨compE⇩1 ?Vs e,(h,ls,sh)⟩ ⇒ ⟨fin⇩1 e',(h',ls',sh')⟩"
and rel': "l' ⊆⇩m [?Vs [↦] ls']" using IH by blast
have [simp]: "length ls = length ls'" by(rule eval⇩1_preserves_len[OF 1])
show "∃ls'. compP⇩1 P ⊢⇩1 ⟨compE⇩1 Vs {V:T; e},(h,ls,sh)⟩ ⇒ ⟨fin⇩1 e',(h',ls',sh')⟩
∧ l'(V := l V) ⊆⇩m [Vs [↦] ls']" (is "∃ls'. ?R ls'")
proof
show "?R ls'"
proof
show "compP⇩1 P ⊢⇩1 ⟨compE⇩1 Vs {V:T; e},(h,ls,sh)⟩ ⇒ ⟨fin⇩1 e',(h',ls',sh')⟩"
using 1 by(simp add:Block⇩1)
next
show "l'(V := l V) ⊆⇩m [Vs [↦] ls']"
proof -
have "l' ⊆⇩m [Vs [↦] ls', V ↦ ls' ! length Vs]"
using len' rel' by simp
moreover
{ assume VinVs: "V ∈ set Vs"
hence "hidden (Vs @ [V]) (last_index Vs V)"
by(rule hidden_last_index)
hence "unmod (compE⇩1 (Vs @ [V]) e) (last_index Vs V)"
by(rule hidden_unmod)
moreover have "last_index Vs V < length ls"
using len' VinVs by simp
ultimately have "ls ! last_index Vs V = ls' ! last_index Vs V"
by(rule eval⇩1_preserves_unmod[OF 1])
}
ultimately show ?thesis using Block_lem[OF rel] len' by auto
qed
qed
qed
next
case (TryThrow e' h l sh a h' l' sh' D fs C V e⇩2)
have "PROP ?P e' h l sh (Throw a) h' l' sh' Vs ls" by fact
with TryThrow.prems
obtain ls' where 1: "?Post e' h l sh (Throw a) h' l' sh' Vs ls ls'"  by(auto)
show ?case using 1 TryThrow.hyps by(auto intro!:eval⇩1_evals⇩1.TryThrow⇩1)
next
case (TryCatch e⇩1 h l sh a h⇩1 l⇩1 sh⇩1 D fs C e⇩2 V e' h⇩2 l⇩2 sh⇩2)
let ?e = "try e⇩1 catch(C V) e⇩2"
have IH⇩1: "⟦fv e⇩1 ⊆ set Vs; l ⊆⇩m [Vs [↦] ls];
size Vs + max_vars e⇩1 ≤ length ls⟧
⟹ ∃ls⇩1. compP⇩1 P ⊢⇩1 ⟨compE⇩1 Vs e⇩1,(h,ls,sh)⟩ ⇒
⟨fin⇩1 (Throw a),(h⇩1,ls⇩1,sh⇩1)⟩ ∧
l⇩1 ⊆⇩m [Vs [↦] ls⇩1]" and
fv: "fv ?e ⊆ set Vs" and
rel: "l ⊆⇩m [Vs [↦] ls]" and
len: "length Vs + max_vars ?e ≤ length ls" by fact+
have "fv e⇩1 ⊆ set Vs" using fv by auto
moreover have "length Vs + max_vars e⇩1 ≤ length ls" using len by(auto)
ultimately obtain ls⇩1 where
1: "compP⇩1 P ⊢⇩1 ⟨compE⇩1 Vs e⇩1,(h,ls,sh)⟩ ⇒ ⟨Throw a,(h⇩1,ls⇩1,sh⇩1)⟩"
and rel⇩1: "l⇩1 ⊆⇩m [Vs [↦] ls⇩1]" using IH⇩1 rel by fastforce
from 1 have [simp]: "size ls = size ls⇩1" by(rule eval⇩1_preserves_len)
let ?Vs = "Vs @ [V]" let ?ls = "(ls⇩1[size Vs:=Addr a])"
have IH⇩2: "⟦fv e⇩2 ⊆ set ?Vs; l⇩1(V ↦ Addr a) ⊆⇩m [?Vs [↦] ?ls];
length ?Vs + max_vars e⇩2 ≤ length ?ls⟧ ⟹ ∃ls⇩2.
compP⇩1 P ⊢⇩1 ⟨compE⇩1 ?Vs e⇩2,(h⇩1,?ls,sh⇩1)⟩ ⇒ ⟨fin⇩1 e',(h⇩2, ls⇩2, sh⇩2)⟩ ∧
l⇩2 ⊆⇩m [?Vs [↦] ls⇩2]" by fact
have len⇩1: "size Vs < size ls⇩1" using len by(auto)
have "fv e⇩2 ⊆ set ?Vs" using fv by auto
moreover have "l⇩1(V ↦ Addr a) ⊆⇩m [?Vs [↦] ?ls]" using rel⇩1 len⇩1 by simp
moreover have "length ?Vs + max_vars e⇩2 ≤ length ?ls" using len by(auto)
ultimately obtain ls⇩2 where
2: "compP⇩1 P ⊢⇩1 ⟨compE⇩1 ?Vs e⇩2,(h⇩1,?ls,sh⇩1)⟩ ⇒ ⟨fin⇩1 e',(h⇩2, ls⇩2, sh⇩2)⟩"
and rel⇩2: "l⇩2 ⊆⇩m [?Vs [↦] ls⇩2]"  using IH⇩2 by blast
from 2 have [simp]: "size ls⇩1 = size ls⇩2"
by(fastforce dest: eval⇩1_preserves_len)
show "∃ls⇩2. compP⇩1 P ⊢⇩1 ⟨compE⇩1 Vs ?e,(h,ls,sh)⟩ ⇒ ⟨fin⇩1 e',(h⇩2,ls⇩2,sh⇩2)⟩ ∧
l⇩2(V := l⇩1 V) ⊆⇩m [Vs [↦] ls⇩2]"  (is "∃ls⇩2. ?R ls⇩2")
proof
show "?R ls⇩2"
proof
have hp: "h⇩1 a = Some (D, fs)" by fact
have "P ⊢ D ≼⇧* C" by fact hence caught: "compP⇩1 P ⊢ D ≼⇧* C" by simp
from TryCatch⇩1[OF 1 _ caught len⇩1 2, OF hp]
show "compP⇩1 P ⊢⇩1 ⟨compE⇩1 Vs ?e,(h,ls,sh)⟩ ⇒ ⟨fin⇩1 e',(h⇩2,ls⇩2,sh⇩2)⟩" by simp
next
show "l⇩2(V := l⇩1 V) ⊆⇩m [Vs [↦] ls⇩2]"
proof -
have "l⇩2 ⊆⇩m [Vs [↦] ls⇩2, V ↦ ls⇩2 ! length Vs]"
using len⇩1 rel⇩2 by simp
moreover
{ assume VinVs: "V ∈ set Vs"
hence "hidden (Vs @ [V]) (last_index Vs V)" by(rule hidden_last_index)
hence "unmod (compE⇩1 (Vs @ [V]) e⇩2) (last_index Vs V)"
by(rule hidden_unmod)
moreover have "last_index Vs V < length ?ls"
using len⇩1 VinVs by simp
ultimately have "?ls ! last_index Vs V = ls⇩2 ! last_index Vs V"
by(rule eval⇩1_preserves_unmod[OF 2])
moreover have "last_index Vs V < size Vs" using VinVs by simp
ultimately have "ls⇩1 ! last_index Vs V = ls⇩2 ! last_index Vs V"
using len⇩1 by(simp del:size_last_index_conv)
}
ultimately show ?thesis using Block_lem[OF rel⇩1] len⇩1  by simp
qed
qed
qed
next
case Try thus ?case by(fastforce intro!:Try⇩1)
next
case Throw thus ?case by(fastforce intro!:Throw⇩1)
next
case ThrowNull thus ?case by(fastforce intro!:ThrowNull⇩1)
next
case ThrowThrow thus ?case  by(fastforce intro!:ThrowThrow⇩1)
next
case (CondT e h l sh h⇩1 l⇩1 sh⇩1 e⇩1 e' h⇩2 l⇩2 sh⇩2 e⇩2)
have "PROP ?P e h l sh true h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with CondT.prems
obtain ls⇩1 where 1: "?Post e h l sh true h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"  by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩1 h⇩1 l⇩1 sh⇩1 e' h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 CondT.prems
obtain ls⇩2 where 2: "?Post e⇩1 h⇩1 l⇩1 sh⇩1 e' h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 show ?case by(auto intro!:CondT⇩1)
next
case (CondF e h l sh h⇩1 l⇩1 sh⇩1 e⇩2 e' h⇩2 l⇩2 sh⇩2 e⇩1 Vs ls)
have "PROP ?P e h l sh false h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with CondF.prems
obtain ls⇩1 where 1: "?Post e h l sh false h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"  by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩2 h⇩1 l⇩1 sh⇩1 e' h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 CondF.prems
obtain ls⇩2 where 2: "?Post e⇩2 h⇩1 l⇩1 sh⇩1 e' h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 show ?case by(auto intro!:CondF⇩1)
next
case CondThrow thus ?case by(fastforce intro!:CondThrow⇩1)
next
case (Seq e h l sh v h⇩1 l⇩1 sh⇩1 e⇩1 e' h⇩2 l⇩2 sh⇩2)
have "PROP ?P e h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with Seq.prems
obtain ls⇩1 where 1: "?Post e h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"  by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩1 h⇩1 l⇩1 sh⇩1 e' h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 Seq.prems
obtain ls⇩2 where 2: "?Post e⇩1 h⇩1 l⇩1 sh⇩1 e' h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 Seq show ?case by(auto intro!:Seq⇩1)
next
case SeqThrow thus ?case by(fastforce intro!:SeqThrow⇩1)
next
case WhileF thus ?case by(fastforce intro!:eval⇩1_evals⇩1.intros)
next
case (WhileT e h l sh h⇩1 l⇩1 sh⇩1 c v h⇩2 l⇩2 sh⇩2 e' h⇩3 l⇩3 sh⇩3)
have "PROP ?P e h l sh true h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with WhileT.prems
obtain ls⇩1 where 1: "?Post e h l sh true h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"   by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P c h⇩1 l⇩1 sh⇩1 (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 WhileT.prems
obtain ls⇩2 where 2: "?Post c h⇩1 l⇩1 sh⇩1 (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"
"size ls⇩1 = size ls⇩2"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P (While (e) c) h⇩2 l⇩2 sh⇩2 e' h⇩3 l⇩3 sh⇩3 Vs ls⇩2" by fact
with 1 2 WhileT.prems
obtain ls⇩3 where 3: "?Post (While (e) c) h⇩2 l⇩2 sh⇩2 e' h⇩3 l⇩3 sh⇩3 Vs ls⇩2 ls⇩3" by(auto)
from 1 2 3 show ?case by(auto intro!:WhileT⇩1)
next
case (WhileBodyThrow e h l sh h⇩1 l⇩1 sh⇩1 c e' h⇩2 l⇩2 sh⇩2)
have "PROP ?P e h l sh true h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with WhileBodyThrow.prems
obtain ls⇩1 where 1: "?Post e h l sh true h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P c h⇩1 l⇩1 sh⇩1 (throw e') h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 WhileBodyThrow.prems
obtain ls⇩2 where 2: "?Post c h⇩1 l⇩1 sh⇩1 (throw e') h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2" by auto
from 1 2 show ?case by(auto intro!:WhileBodyThrow⇩1)
next
case WhileCondThrow thus ?case by(fastforce intro!:WhileCondThrow⇩1)
next
case New thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case NewFail thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case NewInit then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case NewInitOOM then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case NewInitThrow then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case Cast thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case CastNull thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case CastThrow thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (CastFail e h l sh a h⇩1 l⇩1 sh⇩1 D fs C)
have "PROP ?P e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with CastFail.prems
obtain ls⇩1 where 1: "?Post e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1" by auto
show ?case using 1 CastFail.hyps
by(auto intro!:CastFail⇩1[where D=D])
next
case Val thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (BinOp e h l sh v⇩1 h⇩1 l⇩1 sh⇩1 e⇩1 v⇩2 h⇩2 l⇩2 sh⇩2 bop v)
have "PROP ?P e h l sh (Val v⇩1) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with BinOp.prems
obtain ls⇩1 where 1: "?Post e h l sh (Val v⇩1) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩1 h⇩1 l⇩1 sh⇩1 (Val v⇩2) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 BinOp.prems
obtain ls⇩2 where 2: "?Post e⇩1 h⇩1 l⇩1 sh⇩1 (Val v⇩2) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 BinOp show ?case by(auto intro!:BinOp⇩1)
next
case (BinOpThrow2 e⇩0 h l sh v⇩1 h⇩1 l⇩1 sh⇩1 e⇩1 e h⇩2 l⇩2 sh⇩2 bop)
have "PROP ?P e⇩0 h l sh (Val v⇩1) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with BinOpThrow2.prems
obtain ls⇩1 where 1: "?Post e⇩0 h l sh (Val v⇩1) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩1 h⇩1 l⇩1 sh⇩1 (throw e) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 BinOpThrow2.prems
obtain ls⇩2 where 2: "?Post e⇩1 h⇩1 l⇩1 sh⇩1 (throw e) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 BinOpThrow2 show ?case by(auto intro!:BinOpThrow⇩2⇩1)
next
case BinOpThrow1 thus ?case  by(fastforce intro!:eval⇩1_evals⇩1.intros)
next
case Var thus ?case
by(force intro!:Var⇩1 simp add: map_le_def fun_upds_apply)
next
case LAss thus ?case
by(fastforce simp add: LAss_lem intro:eval⇩1_evals⇩1.intros
dest:eval⇩1_preserves_len)
next
case LAssThrow thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case FAcc thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case FAccNull thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case FAccThrow thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (FAccNone e h l sh a h' l' sh' C fs F D)
have "PROP ?P e h l sh (addr a) h' l' sh' Vs ls" by fact
with FAccNone.prems
obtain ls⇩2 where 2: "?Post e h l sh (addr a) h' l' sh' Vs ls ls⇩2" by(auto)
from 2 FAccNone show ?case by(rule_tac x = ls⇩2 in exI, auto elim!: FAccNone⇩1)
next
case (FAccStatic e h l sh a h' l' sh' C fs F t D)
have "PROP ?P e h l sh (addr a) h' l' sh' Vs ls" by fact
with FAccStatic.prems
obtain ls⇩2 where 2: "?Post e h l sh (addr a) h' l' sh' Vs ls ls⇩2" by(auto)
from 2 FAccStatic show ?case by(rule_tac x = ls⇩2 in exI, auto elim!: FAccStatic⇩1)
next
case SFAcc then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (SFAccInit C F t D sh h l v' h' l' sh' sfs i v)
have "PROP ?P (INIT D ([D],False) ← unit) h l sh (Val v') h' l' sh' Vs ls" by fact
with SFAccInit.prems
obtain ls⇩2 where 1: "?Post (INIT D ([D],False) ← unit) h l sh (Val v') h' l' sh' Vs ls ls⇩2" by(auto)
from 1 SFAccInit show ?case by(rule_tac x = ls⇩2 in exI, auto intro: SFAccInit⇩1)
next
case (SFAccInitThrow C F t D sh h l a h' l' sh')
have "PROP ?P (INIT D ([D],False) ← unit) h l sh (throw a) h' l' sh' Vs ls" by fact
with SFAccInitThrow.prems
obtain ls⇩2 where 1: "?Post (INIT D ([D],False) ← unit) h l sh (throw a) h' l' sh' Vs ls ls⇩2" by(auto)
from 1 SFAccInitThrow show ?case by(rule_tac x = ls⇩2 in exI, auto intro: SFAccInitThrow⇩1)
next
case SFAccNone then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case SFAccNonStatic then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (FAss e⇩1 h l sh a h⇩1 l⇩1 sh⇩1 e⇩2 v h⇩2 l⇩2 sh⇩2 C fs fs' F D h⇩2')
have "PROP ?P e⇩1 h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with FAss.prems
obtain ls⇩1 where 1: "?Post e⇩1 h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩2 h⇩1 l⇩1 sh⇩1 (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 FAss.prems
obtain ls⇩2 where 2: "?Post e⇩2 h⇩1 l⇩1 sh⇩1 (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 FAss show ?case by(auto intro!:FAss⇩1)
next
case (FAssNull e⇩1 h l sh h⇩1 l⇩1 sh⇩1 e⇩2 v h⇩2 l⇩2 sh⇩2 F D)
have "PROP ?P e⇩1 h l sh null h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with FAssNull.prems
obtain ls⇩1 where 1: "?Post e⇩1 h l sh null h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩2 h⇩1 l⇩1 sh⇩1 (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 FAssNull.prems
obtain ls⇩2 where 2: "?Post e⇩2 h⇩1 l⇩1 sh⇩1 (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2" by(auto)
from 1 2 FAssNull show ?case by(auto intro!:FAssNull⇩1)
next
case FAssThrow1 thus ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (FAssThrow2 e⇩1 h l sh v h⇩1 l⇩1 sh⇩1 e⇩2 e h⇩2 l⇩2 sh⇩2 F D)
have "PROP ?P e⇩1 h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with FAssThrow2.prems
obtain ls⇩1 where 1: "?Post e⇩1 h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"   by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩2 h⇩1 l⇩1 sh⇩1 (throw e) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 FAssThrow2.prems
obtain ls⇩2 where 2: "?Post e⇩2 h⇩1 l⇩1 sh⇩1 (throw e) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 FAssThrow2 show ?case by(auto intro!:FAssThrow⇩2⇩1)
next
case (FAssNone e⇩1 h l sh a h' l' sh' e⇩2 v h⇩2 l⇩2 sh⇩2 C fs F D)
have "PROP ?P e⇩1 h l sh (addr a) h' l' sh' Vs ls" by fact
with FAssNone.prems
obtain ls⇩1 where 1: "?Post e⇩1 h l sh (addr a) h' l' sh' Vs ls ls⇩1"
"size ls = size ls⇩1"   by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩2 h' l' sh' (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 FAssNone.prems
obtain ls⇩2 where 2: "?Post e⇩2 h' l' sh' (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 FAssNone show ?case by(auto intro!:FAssNone⇩1)
next
case (FAssStatic e⇩1 h l sh a h' l' sh' e⇩2 v h⇩2 l⇩2 sh⇩2 C fs F t D)
have "PROP ?P e⇩1 h l sh (addr a) h' l' sh' Vs ls" by fact
with FAssStatic.prems
obtain ls⇩1 where 1: "?Post e⇩1 h l sh (addr a) h' l' sh' Vs ls ls⇩1"
"size ls = size ls⇩1"   by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P e⇩2 h' l' sh' (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 FAssStatic.prems
obtain ls⇩2 where 2: "?Post e⇩2 h' l' sh' (Val v) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"  by(auto)
from 1 2 FAssStatic show ?case by(auto intro!:FAssStatic⇩1)
next
case SFAss then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (SFAssInit e⇩2 h l sh v h⇩1 l⇩1 sh⇩1 C F t D v' h' l' sh' sfs i sfs' sh'')
have "PROP ?P e⇩2 h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with SFAssInit.prems
obtain ls⇩1 where 1: "?Post e⇩2 h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1" "length ls = length ls⇩1"
by(auto intro!:eval⇩1_preserves_len)
then have Init_size: "length Vs ≤ length ls⇩1" using SFAssInit.prems(3) by linarith
have "PROP ?P (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (Val v') h' l' sh' Vs ls⇩1" by fact
with 1 Init_size SFAssInit.prems
obtain ls⇩2 where 2: "?Post (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (Val v') h' l' sh' Vs ls⇩1 ls⇩2"
by auto
from 1 2 SFAssInit show ?case
by(auto simp add: comp_def
intro!: SFAssInit⇩1 dest!:evals_final)
next
case (SFAssInitThrow e⇩2 h l sh v h⇩1 l⇩1 sh⇩1 C F t D a h⇩2 l⇩2 sh⇩2)
have "PROP ?P e⇩2 h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with SFAssInitThrow.prems
obtain ls⇩1 where 1: "?Post e⇩2 h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1" "length ls = length ls⇩1"
by(auto intro!:eval⇩1_preserves_len)
then have Init_size: "length Vs ≤ length ls⇩1" using SFAssInitThrow.prems(3) by linarith
have "PROP ?P (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (throw a) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 Init_size SFAssInitThrow.prems
obtain ls⇩2 where 2: "?Post (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (throw a) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"
by auto
from 1 2 SFAssInitThrow show ?case
by(auto simp add: comp_def
intro!: SFAssInitThrow⇩1 dest!:evals_final)
next
case SFAssThrow then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (SFAssNone e⇩2 h l sh v h⇩2 l⇩2 sh⇩2 C F D)
have "PROP ?P e⇩2 h l sh (Val v) h⇩2 l⇩2 sh⇩2 Vs ls" by fact
with SFAssNone.prems
obtain ls⇩2 where 2: "?Post e⇩2 h l sh (Val v) h⇩2 l⇩2 sh⇩2 Vs ls ls⇩2" by(auto)
from 2 SFAssNone show ?case by(rule_tac x = ls⇩2 in exI, auto elim!: SFAssNone⇩1)
next
case SFAssNonStatic then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (CallNull e h l sh h⇩1 l⇩1 sh⇩1 es vs h⇩2 l⇩2 sh⇩2 M)
have "PROP ?P e h l sh null h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with CallNull.prems
obtain ls⇩1 where 1: "?Post e h l sh null h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?Ps es h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 CallNull.prems
obtain ls⇩2 where 2: "?Posts es h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2" by(auto)
from 1 2 CallNull show ?case
by (auto simp add: comp_def elim!: CallNull⇩1)
next
case CallObjThrow thus ?case  by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (CallParamsThrow e h l sh v h⇩1 l⇩1 sh⇩1 es vs ex es' h⇩2 l⇩2 sh⇩2 M)
have "PROP ?P e h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with CallParamsThrow.prems
obtain ls⇩1 where 1: "?Post e h l sh (Val v) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?Ps es h⇩1 l⇩1 sh⇩1 (map Val vs @ throw ex # es') h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 CallParamsThrow.prems
obtain ls⇩2 where 2: "?Posts es h⇩1 l⇩1 sh⇩1 (map Val vs @ throw ex # es') h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2" by(auto)
from 1 2 CallParamsThrow show ?case
by (auto simp add: comp_def
elim!: CallParamsThrow⇩1 dest!:evals_final)
next
case (CallNone e h l sh a h⇩1 l⇩1 sh⇩1 ps vs h⇩2 l⇩2 sh⇩2 C fs M)
have "PROP ?P e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with CallNone.prems
obtain ls⇩1 where 1: "?Post e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?Ps ps h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 CallNone.prems
obtain ls⇩2 where 2: "?Posts ps h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2" by(auto)
from 1 2 CallNone show ?case
by (auto simp add: comp_def
elim!: CallNone⇩1 dest!:evals_final sees_method_compPD)
next
case (CallStatic e h l sh a h⇩1 l⇩1 sh⇩1 ps vs h⇩2 l⇩2 sh⇩2 C fs M Ts T pns body D)
have "PROP ?P e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with CallStatic.prems
obtain ls⇩1 where 1: "?Post e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
let ?Vs = pns
have mdecl: "P ⊢ C sees M,Static: Ts→T = (pns, body) in D" by fact
have mdecl⇩1: "compP⇩1 P ⊢ C sees M,Static: Ts→T = (compE⇩1 ?Vs body) in D"
using sees_method_compP[OF mdecl, of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
by(simp)
have "PROP ?Ps ps h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 CallStatic.prems
obtain ls⇩2 where 2: "?Posts ps h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2" by(auto)
from 1 2 mdecl⇩1 CallStatic show ?case
by (auto simp add: comp_def
elim!: CallStatic⇩1 dest!:evals_final)
next
case (Call e h l sh a h⇩1 l⇩1 sh⇩1 es vs h⇩2 l⇩2 sh⇩2 C fs M Ts T pns body D l⇩2' b' h⇩3 l⇩3 sh⇩3)
have "PROP ?P e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with Call.prems
obtain ls⇩1 where 1: "?Post e h l sh (addr a) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?Ps es h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 Call.prems
obtain ls⇩2 where 2: "?Posts es h⇩1 l⇩1 sh⇩1 (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"
"size ls⇩1 = size ls⇩2"    by(auto intro!:evals⇩1_preserves_len)
let ?Vs = "this#pns"
let ?ls = "Addr a # vs @ replicate (max_vars body) undefined"
have mdecl: "P ⊢ C sees M,NonStatic: Ts→T = (pns, body) in D" by fact
have fv_body: "fv body ⊆ set ?Vs" and wf_size: "size Ts = size pns"
using wf mdecl by(auto dest!:sees_wf_mdecl simp:wf_mdecl_def)
have mdecl⇩1: "compP⇩1 P ⊢ C sees M,NonStatic: Ts→T = (compE⇩1 ?Vs body) in D"
using sees_method_compP[OF mdecl, of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
by(simp)
have [simp]: "l⇩2' = [this ↦ Addr a, pns [↦] vs]" by fact
have Call_size: "size vs = size pns" by fact
have "PROP ?P body h⇩2 l⇩2' sh⇩2 b' h⇩3 l⇩3 sh⇩3 ?Vs ?ls" by fact
with 1 2 fv_body Call_size Call.prems
obtain ls⇩3 where 3: "?Post body h⇩2 l⇩2' sh⇩2 b' h⇩3 l⇩3 sh⇩3 ?Vs ?ls ls⇩3"  by(auto)
have hp: "h⇩2 a = Some (C, fs)" by fact
from 1 2 3 hp mdecl⇩1 wf_size Call_size show ?case
by(fastforce simp add: comp_def
intro!: Call⇩1 dest!:evals_final)
next
case (SCallParamsThrow es h l sh vs ex es' h⇩2 l⇩2 sh⇩2 C M)
have "PROP ?Ps es h l sh (map Val vs @ throw ex # es') h⇩2 l⇩2 sh⇩2 Vs ls" by fact
with SCallParamsThrow.prems
obtain ls⇩2 where 2: "?Posts es h l sh (map Val vs @ throw ex # es') h⇩2 l⇩2 sh⇩2 Vs ls ls⇩2" by(auto)
from 2 SCallParamsThrow show ?case
by (fastforce simp add: comp_def
elim!: SCallParamsThrow⇩1 dest!:evals_final)
next
case (SCall ps h l sh vs h⇩2 l⇩2 sh⇩2 C M Ts T pns body D sfs l⇩2' e' h⇩3 l⇩3 sh⇩3)
have "PROP ?Ps ps h l sh (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls" by fact
with SCall.prems
obtain ls⇩2 where 2: "?Posts ps h l sh (map Val vs) h⇩2 l⇩2 sh⇩2 Vs ls ls⇩2"
"size ls = size ls⇩2"    by(auto intro!:evals⇩1_preserves_len)
let ?Vs = "pns"
let ?ls = "vs @ replicate (max_vars body) undefined"
have mdecl: "P ⊢ C sees M,Static: Ts→T = (pns, body) in D" by fact
have fv_body: "fv body ⊆ set ?Vs" and wf_size: "size Ts = size pns"
using wf mdecl by(auto dest!:sees_wf_mdecl simp:wf_mdecl_def)
have mdecl⇩1: "compP⇩1 P ⊢ C sees M,Static: Ts→T = (compE⇩1 ?Vs body) in D"
using sees_method_compP[OF mdecl, of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
by(simp)
have [simp]: "l⇩2' = [pns [↦] vs]" by fact
have SCall_size: "size vs = size pns" by fact
have "PROP ?P body h⇩2 l⇩2' sh⇩2 e' h⇩3 l⇩3 sh⇩3 ?Vs ?ls" by fact
with 2 fv_body SCall_size SCall.prems
obtain ls⇩3 where 3: "?Post body h⇩2 l⇩2' sh⇩2 e' h⇩3 l⇩3 sh⇩3 ?Vs ?ls ls⇩3"  by(auto)
have shp: "sh⇩2 D = ⌊(sfs, Done)⌋ ∨ M = clinit ∧ sh⇩2 D = ⌊(sfs, Processing)⌋" by fact
from 2 3 shp mdecl⇩1 wf_size SCall_size show ?case
by(fastforce simp add: comp_def
intro!: SCall⇩1 dest!:evals_final)
next
case (SCallNone ps h l sh vs h' l' sh' C M)
have "PROP ?Ps ps h l sh (map Val vs) h' l' sh' Vs ls" by fact
with SCallNone.prems
obtain ls⇩2 where 2: "?Posts ps h l sh (map Val vs) h' l' sh' Vs ls ls⇩2" by(auto)
from 2 SCallNone show ?case
by(rule_tac x = ls⇩2 in exI,
auto simp add: comp_def elim!: SCallNone⇩1 dest!:evals_final sees_method_compPD)
next
case (SCallNonStatic ps h l sh vs h' l' sh' C M Ts T pns body D)
let ?Vs = "this#pns"
have mdecl: "P ⊢ C sees M,NonStatic: Ts→T = (pns, body) in D" by fact
have mdecl⇩1: "compP⇩1 P ⊢ C sees M,NonStatic: Ts→T = (compE⇩1 ?Vs body) in D"
using sees_method_compP[OF mdecl, of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
by(simp)
have "PROP ?Ps ps h l sh (map Val vs) h' l' sh' Vs ls" by fact
with SCallNonStatic.prems
obtain ls⇩2 where 2: "?Posts ps h l sh (map Val vs) h' l' sh' Vs ls ls⇩2" by(auto)
from 2 mdecl⇩1 SCallNonStatic show ?case
by (auto simp add: comp_def
elim!: SCallNonStatic⇩1 dest!:evals_final)
next
case (SCallInitThrow ps h l sh vs h⇩1 l⇩1 sh⇩1 C M Ts T pns body D a h⇩2 l⇩2 sh⇩2)
have "PROP ?Ps ps h l sh (map Val vs) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with SCallInitThrow.prems
obtain ls⇩1 where 1: "?Posts ps h l sh (map Val vs) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1" "length ls = length ls⇩1"
by(auto intro!:evals⇩1_preserves_len)
then have Init_size: "length Vs ≤ length ls⇩1" using SCallInitThrow.prems(3) by linarith
have "PROP ?P (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (throw a) h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 Init_size SCallInitThrow.prems
obtain ls⇩2 where 2: "?Post (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (throw a) h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"
by auto
let ?Vs = "pns"
have mdecl: "P ⊢ C sees M,Static: Ts→T = (pns, body) in D" by fact
have mdecl⇩1: "compP⇩1 P ⊢ C sees M,Static: Ts→T = (compE⇩1 ?Vs body) in D"
using sees_method_compP[OF mdecl, of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
by(simp)
from 1 2 mdecl⇩1 SCallInitThrow show ?case
by(auto simp add: comp_def
intro!: SCallInitThrow⇩1 dest!:evals_final)
next
case (SCallInit ps h l sh vs h⇩1 l⇩1 sh⇩1 C M Ts T pns body D v' h⇩2 l⇩2 sh⇩2 l⇩2' e' h⇩3 l⇩3 sh⇩3)
have "PROP ?Ps ps h l sh (map Val vs) h⇩1 l⇩1 sh⇩1 Vs ls" by fact
with SCallInit.prems
obtain ls⇩1 where 1: "?Posts ps h l sh (map Val vs) h⇩1 l⇩1 sh⇩1 Vs ls ls⇩1" "length ls = length ls⇩1"
by(auto intro!:evals⇩1_preserves_len)
then have Init_size: "length Vs ≤ length ls⇩1" using SCallInit.prems(3) by linarith
have "PROP ?P (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (Val v') h⇩2 l⇩2 sh⇩2 Vs ls⇩1" by fact
with 1 Init_size SCallInit.prems
obtain ls⇩2 where 2: "?Post (INIT D ([D],False) ← unit) h⇩1 l⇩1 sh⇩1 (Val v') h⇩2 l⇩2 sh⇩2 Vs ls⇩1 ls⇩2"
by auto
let ?Vs = "pns"
let ?ls = "vs @ replicate (max_vars body) undefined"
have mdecl: "P ⊢ C sees M,Static: Ts→T = (pns, body) in D" by fact
have fv_body: "fv body ⊆ set ?Vs" and wf_size: "size Ts = size pns"
using wf mdecl by(auto dest!:sees_wf_mdecl simp:wf_mdecl_def)
have mdecl⇩1: "compP⇩1 P ⊢ C sees M,Static: Ts→T = (compE⇩1 ?Vs body) in D"
using sees_method_compP[OF mdecl, of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
by(simp)
have [simp]: "l⇩2' = [pns [↦] vs]" by fact
have SCall_size: "size vs = size pns" by fact
have nclinit: "M ≠ clinit" by fact
have "PROP ?P body h⇩2 l⇩2' sh⇩2 e' h⇩3 l⇩3 sh⇩3 ?Vs ?ls" by fact
with 2 fv_body SCall_size SCallInit.prems
obtain ls⇩3 where 3: "?Post body h⇩2 l⇩2' sh⇩2 e' h⇩3 l⇩3 sh⇩3 ?Vs ?ls ls⇩3"  by(auto)
have shp: "∄sfs. sh⇩1 D = ⌊(sfs, Done)⌋" by fact
from 1 2 3 shp mdecl⇩1 wf_size SCall_size nclinit show ?case
by(auto simp add: comp_def
intro!: SCallInit⇩1 dest!:evals_final)
next
― ‹ init cases ›
case InitFinal then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (InitNone sh C C' Cs e h l e' h' l' sh')
let ?sh1 = "sh(C ↦ (sblank P C, Prepared))"
have "PROP ?P (INIT C' (C # Cs,False) ← e) h l ?sh1 e' h' l' sh' Vs ls" by fact
with InitNone.prems
obtain ls⇩2 where 2: "?Post (INIT C' (C # Cs,False) ← e) h l ?sh1 e' h' l' sh' Vs ls ls⇩2" by(auto)
from 2 InitNone show ?case by (auto elim!: InitNone⇩1)
next
case InitDone then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case InitProcessing then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case InitError then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case InitObject then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (InitNonObject sh C sfs D fs ms sh' C' Cs e h l e' h1 l1 sh1)
let ?f = "(λb (pns,body). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) body)"
have cls: "class (compP ?f P) C = ⌊(D,fs,map (compM ?f) ms)⌋"
by(rule class_compP[OF InitNonObject.hyps(3)])
have "PROP ?P (INIT C' (D # C # Cs,False) ← e) h l sh' e' h1 l1 sh1 Vs ls" by fact
with InitNonObject.prems
obtain ls⇩2 where 2: "?Post (INIT C' (D # C # Cs,False) ← e) h l sh' e' h1 l1 sh1 Vs ls ls⇩2" by(auto)
from 2 cls InitNonObject show ?case by (auto elim!: InitNonObject⇩1)
next
case InitRInit then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
next
case (RInit e h l sh v h' l' sh' C sfs i sh'' C' Cs e' e⇩1 h⇩1 l⇩1 sh⇩1)
have "PROP ?P e h l sh (Val v) h' l' sh' Vs ls" by fact
with RInit.prems
obtain ls⇩1 where 1: "?Post e h l sh (Val v) h' l' sh' Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have "PROP ?P (INIT C' (Cs,True) ← e') h' l' sh'' e⇩1 h⇩1 l⇩1 sh⇩1 Vs ls⇩1" by fact
with 1 RInit.prems
obtain ls⇩2 where 2: "?Post (INIT C' (Cs,True) ← e') h' l' sh'' e⇩1 h⇩1 l⇩1 sh⇩1 Vs ls⇩1 ls⇩2" by(auto)
from 1 2 RInit show ?case by (auto elim!: RInit⇩1)
next
case (RInitInitFail e h l sh a h' l' sh' C sfs i sh'' D Cs e' e⇩1 h⇩1 l⇩1 sh⇩1)
have "PROP ?P e h l sh (throw a) h' l' sh' Vs ls" by fact
with RInitInitFail.prems
obtain ls⇩1 where 1: "?Post e h l sh (throw a) h' l' sh' Vs ls ls⇩1"
"size ls = size ls⇩1"    by(auto intro!:eval⇩1_preserves_len)
have fv: "fv (RI (D,throw a) ; Cs ← e') ⊆ set Vs"
using RInitInitFail.hyps(1) eval_final RInitInitFail.prems(1) subset_eq by fastforce
have l': "l' ⊆⇩m [Vs [↦] ls⇩1]" by (simp add: "1"(1))
have "PROP ?P (RI (D,throw a) ; Cs ← e') h' l' sh'' e⇩1 h⇩1 l⇩1 sh⇩1 Vs ls⇩1" by fact
with 1 eval_final[OF RInitInitFail.hyps(1)] RInitInitFail.prems
obtain ls⇩2 where 2: "?Post (RI (D,throw a) ; Cs ← e') h' l' sh'' e⇩1 h⇩1 l⇩1 sh⇩1 Vs ls⇩1 ls⇩2"
by fastforce
from 1 2 RInitInitFail show ?case
by(fastforce simp add: comp_def
intro!: RInitInitFail⇩1 dest!:eval_final)
next
case RInitFailFinal then show ?case by(fastforce intro:eval⇩1_evals⇩1.intros)
qed
(*>*)

subsection‹Preservation of well-formedness›

text‹ The compiler preserves well-formedness. Is less trivial than it
may appear. We start with two simple properties: preservation of
well-typedness ›

lemma compE⇩1_pres_wt: "⋀Vs Ts U.
⟦ P,[Vs[↦]Ts] ⊢ e :: U; size Ts = size Vs ⟧
⟹ compP f P,Ts ⊢⇩1 compE⇩1 Vs e :: U"
and  "⋀Vs Ts Us.
⟦ P,[Vs[↦]Ts] ⊢ es [::] Us; size Ts = size Vs ⟧
⟹ compP f P,Ts ⊢⇩1 compEs⇩1 Vs es [::] Us"
(*<*)
proof(induct e and es rule: compE⇩1.induct compEs⇩1.induct)
case Var then show ?case
by (fastforce simp:map_upds_apply_eq_Some split:if_split_asm)
next
case LAss then show ?case
by (fastforce simp:map_upds_apply_eq_Some split:if_split_asm)
next
case Call then show ?case
by (fastforce dest!: sees_method_compP[where f = f])
next
case SCall then show ?case
by (fastforce dest!: sees_method_compP[where f = f])
next
case Block then show ?case by (fastforce simp:nth_append)
next
case TryCatch then show ?case by (fastforce simp:nth_append)
qed fastforce+
(*>*)

text‹\noindent and the correct block numbering: ›

lemma ℬ: "⋀Vs n. size Vs = n ⟹ ℬ (compE⇩1 Vs e) n"
and ℬs: "⋀Vs n. size Vs = n ⟹ ℬs (compEs⇩1 Vs es) n"
(*<*)by (induct e and es rule: ℬ.induct ℬs.induct)
(force | simp,metis length_append_singleton)+(*>*)

text‹ The main complication is preservation of definite assignment
@{term"𝒟"}. ›

lemma image_last_index: "A ⊆ set(xs@[x]) ⟹ last_index (xs @ [x])  A =
(if x ∈ A then insert (size xs) (last_index xs  (A-{x})) else last_index xs  A)"
(*<*)
by(auto simp:image_def)
(*>*)

lemma A_compE⇩1_None[simp]:
"⋀Vs. 𝒜 e = None ⟹ 𝒜 (compE⇩1 Vs e) = None"
and "⋀Vs. 𝒜s es = None ⟹ 𝒜s (compEs⇩1 Vs es) = None"
(*<*)by(induct e and es rule: compE⇩1.induct compEs⇩1.induct)(auto simp:hyperset_defs)(*>*)

lemma A_compE⇩1:
"⋀A Vs. ⟦ 𝒜 e = ⌊A⌋; fv e ⊆ set Vs ⟧ ⟹ 𝒜 (compE⇩1 Vs e) = ⌊last_index Vs  A⌋"
and "⋀A Vs. ⟦ 𝒜s es = ⌊A⌋; fvs es ⊆ set Vs ⟧ ⟹ 𝒜s (compEs⇩1 Vs es) = ⌊last_index Vs  A⌋"
(*<*)
proof(induct e and es rule: fv.induct fvs.induct)
case (Block V' T e)
hence "fv e ⊆ set (Vs@[V'])" by fastforce
moreover obtain B where "𝒜 e = ⌊B⌋"
using Block.prems by(simp add: hyperset_defs)
moreover from calculation have "B ⊆ set (Vs@[V'])" by(auto dest!:A_fv)
ultimately show ?case using Block
by(auto simp add: hyperset_defs image_last_index last_index_size_conv)
next
case (TryCatch e⇩1 C V' e⇩2)
hence fve⇩2: "fv e⇩2 ⊆ set (Vs@[V'])" by auto
show ?case
proof (cases "𝒜 e⇩1")
assume A⇩1: "𝒜 e⇩1 = None"
then obtain A⇩2 where A⇩2: "𝒜 e⇩2 = ⌊A⇩2⌋" using TryCatch
by(simp add:hyperset_defs)
hence "A⇩2 ⊆ set (Vs@[V'])" using TryCatch.prems A_fv[OF A⇩2] by simp blast
thus ?thesis using TryCatch fve⇩2 A⇩1 A⇩2
by(auto simp add:hyperset_defs image_last_index last_index_size_conv)
next
fix A⇩1 assume A⇩1: "𝒜 e⇩1 =  ⌊A⇩1⌋"
show ?thesis
proof (cases  "𝒜 e⇩2")
assume A⇩2: "𝒜 e⇩2 = None"
then show ?case using TryCatch A⇩1 by(simp add:hyperset_defs)
next
fix A⇩2 assume A⇩2: "𝒜 e⇩2 = ⌊A⇩2⌋"
have "A⇩1 ⊆ set Vs" using TryCatch.prems A_fv[OF A⇩1] by simp blast
moreover
have "A⇩2 ⊆ set (Vs@[V'])" using TryCatch.prems A_fv[OF A⇩2] by simp blast
ultimately show ?thesis using TryCatch A⇩1 A⇩2
by (auto simp add: Diff_subset_conv last_index_size_conv subsetD hyperset_defs
dest!: sym [of _ A])
qed
qed
next
case (Cond e e⇩1 e⇩2)
{ assume "𝒜 e = None ∨ 𝒜 e⇩1 = None ∨ 𝒜 e⇩2 = None"
hence ?case using Cond by(auto simp add:hyperset_defs image_Un)
}
moreover
{ fix A A⇩1 A⇩2
assume "𝒜 e = ⌊A⌋" and A⇩1: "𝒜 e⇩1 = ⌊A⇩1⌋" and A⇩2: "𝒜 e⇩2 = ⌊A⇩2⌋"
moreover
have "A⇩1 ⊆ set Vs" using Cond.prems A_fv[OF A⇩1] by simp blast
moreover
have "A⇩2 ⊆ set Vs" using Cond.prems A_fv[OF A⇩2] by simp blast
ultimately have ?case using Cond
by(auto simp add:hyperset_defs image_Un
inj_on_image_Int[OF inj_on_last_index])
}
ultimately show ?case by fastforce
qed (auto simp add:hyperset_defs)
(*>*)

lemma D_None[iff]: "𝒟 (e::'a exp) None" and [iff]: "𝒟s (es::'a exp list) None"
(*<*)by(induct e and es rule: 𝒟.induct 𝒟s.induct)(simp_all)(*>*)

lemma D_last_index_compE⇩1:
"⋀A Vs. ⟦ A ⊆ set Vs; fv e ⊆ set Vs ⟧ ⟹
𝒟 e ⌊A⌋ ⟹ 𝒟 (compE⇩1 Vs e) ⌊last_index Vs  A⌋"
and "⋀A Vs. ⟦ A ⊆ set Vs; fvs es ⊆ set Vs ⟧ ⟹
𝒟s es ⌊A⌋ ⟹ 𝒟s (compEs⇩1 Vs es) ⌊last_index Vs  A⌋"
(*<*)
proof(induct e and es rule: 𝒟.induct 𝒟s.induct)
case (BinOp e⇩1 bop e⇩2)
hence IH⇩1: "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  A⌋" by simp
show ?case
proof (cases "𝒜 e⇩1")
case None thus ?thesis using BinOp by simp
next
case (Some A⇩1)
have indexA⇩1: "𝒜 (compE⇩1 Vs e⇩1) = ⌊last_index Vs  A⇩1⌋"
using A_compE⇩1[OF Some] BinOp.prems  by auto
have "A ∪ A⇩1 ⊆ set Vs" using BinOp.prems A_fv[OF Some] by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  (A ∪ A⇩1)⌋" using BinOp Some by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  A ∪ last_index Vs  A⇩1⌋"
by(simp add: image_Un)
thus ?thesis using IH⇩1 indexA⇩1 by auto
qed
next
case (FAss e⇩1 F D e⇩2)
hence IH⇩1: "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  A⌋" by simp
show ?case
proof (cases "𝒜 e⇩1")
case None thus ?thesis using FAss by simp
next
case (Some A⇩1)
have indexA⇩1: "𝒜 (compE⇩1 Vs e⇩1) = ⌊last_index Vs  A⇩1⌋"
using A_compE⇩1[OF Some] FAss.prems  by auto
have "A ∪ A⇩1 ⊆ set Vs" using FAss.prems A_fv[OF Some] by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  (A ∪ A⇩1)⌋" using FAss Some by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  A ∪ last_index Vs  A⇩1⌋"
by(simp add: image_Un)
thus ?thesis using IH⇩1 indexA⇩1 by auto
qed
next
case (Call e⇩1 M es)
hence IH⇩1: "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  A⌋" by simp
show ?case
proof (cases "𝒜 e⇩1")
case None thus ?thesis using Call by simp
next
case (Some A⇩1)
have indexA⇩1: "𝒜 (compE⇩1 Vs e⇩1) = ⌊last_index Vs  A⇩1⌋"
using A_compE⇩1[OF Some] Call.prems  by auto
have "A ∪ A⇩1 ⊆ set Vs" using Call.prems A_fv[OF Some] by auto
hence "𝒟s (compEs⇩1 Vs es) ⌊last_index Vs  (A ∪ A⇩1)⌋" using Call Some by auto
hence "𝒟s (compEs⇩1 Vs es) ⌊last_index Vs  A ∪ last_index Vs  A⇩1⌋"
by(simp add: image_Un)
thus ?thesis using IH⇩1 indexA⇩1 by auto
qed
next
case (TryCatch e⇩1 C V e⇩2)
have "⟦ A∪{V} ⊆ set(Vs@[V]); fv e⇩2 ⊆ set(Vs@[V]); 𝒟 e⇩2 ⌊A∪{V}⌋⟧ ⟹
𝒟 (compE⇩1 (Vs@[V]) e⇩2) ⌊last_index (Vs@[V])  (A∪{V})⌋" by fact
hence "𝒟 (compE⇩1 (Vs@[V]) e⇩2) ⌊last_index (Vs@[V])  (A∪{V})⌋"
using TryCatch.prems by(simp add:Diff_subset_conv)
moreover have "last_index (Vs@[V])  A ⊆ last_index Vs  A ∪ {size Vs}"
using TryCatch.prems by(auto simp add: image_last_index split:if_split_asm)
ultimately show ?case using TryCatch
by(auto simp:hyperset_defs elim!:D_mono')
next
case (Seq e⇩1 e⇩2)
hence IH⇩1: "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  A⌋" by simp
show ?case
proof (cases "𝒜 e⇩1")
case None thus ?thesis using Seq by simp
next
case (Some A⇩1)
have indexA⇩1: "𝒜 (compE⇩1 Vs e⇩1) = ⌊last_index Vs  A⇩1⌋"
using A_compE⇩1[OF Some] Seq.prems  by auto
have "A ∪ A⇩1 ⊆ set Vs" using Seq.prems A_fv[OF Some] by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  (A ∪ A⇩1)⌋" using Seq Some by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  A ∪ last_index Vs  A⇩1⌋"
by(simp add: image_Un)
thus ?thesis using IH⇩1 indexA⇩1 by auto
qed
next
case (Cond e e⇩1 e⇩2)
hence IH⇩1: "𝒟 (compE⇩1 Vs e) ⌊last_index Vs  A⌋" by simp
show ?case
proof (cases "𝒜 e")
case None thus ?thesis using Cond by simp
next
case (Some B)
have indexB: "𝒜 (compE⇩1 Vs e) = ⌊last_index Vs  B⌋"
using A_compE⇩1[OF Some] Cond.prems  by auto
have "A ∪ B ⊆ set Vs" using Cond.prems A_fv[OF Some] by auto
hence "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  (A ∪ B)⌋"
and "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  (A ∪ B)⌋"
using Cond Some by auto
hence "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  A ∪ last_index Vs  B⌋"
and "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  A ∪ last_index Vs  B⌋"
by(simp add: image_Un)+
thus ?thesis using IH⇩1 indexB by auto
qed
next
case (While e⇩1 e⇩2)
hence IH⇩1: "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  A⌋" by simp
show ?case
proof (cases "𝒜 e⇩1")
case None thus ?thesis using While by simp
next
case (Some A⇩1)
have indexA⇩1: "𝒜 (compE⇩1 Vs e⇩1) = ⌊last_index Vs  A⇩1⌋"
using A_compE⇩1[OF Some] While.prems  by auto
have "A ∪ A⇩1 ⊆ set Vs" using While.prems A_fv[OF Some] by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  (A ∪ A⇩1)⌋" using While Some by auto
hence "𝒟 (compE⇩1 Vs e⇩2) ⌊last_index Vs  A ∪ last_index Vs  A⇩1⌋"
by(simp add: image_Un)
thus ?thesis using IH⇩1 indexA⇩1 by auto
qed
next
case (Block V T e)
have "⟦ A-{V} ⊆ set(Vs@[V]); fv e ⊆ set(Vs@[V]); 𝒟 e ⌊A-{V}⌋ ⟧ ⟹
𝒟 (compE⇩1 (Vs@[V]) e) ⌊last_index (Vs@[V])  (A-{V})⌋" by fact
hence "𝒟 (compE⇩1 (Vs@[V]) e) ⌊last_index (Vs@[V])  (A-{V})⌋"
using Block.prems by(simp add:Diff_subset_conv)
moreover have "size Vs ∉ last_index Vs  A"
using Block.prems by(auto simp add:image_def size_last_index_conv)
ultimately show ?case using Block
by(auto simp add: image_last_index Diff_subset_conv hyperset_defs elim!: D_mono')
next
case (Cons_exp e⇩1 es)
hence IH⇩1: "𝒟 (compE⇩1 Vs e⇩1) ⌊last_index Vs  A⌋" by simp
show ?case
proof (cases "𝒜 e⇩1")
case None thus ?thesis using Cons_exp by simp
next
case (Some A⇩1)
have indexA⇩1: "𝒜 (compE⇩1 Vs e⇩1) = ⌊last_index Vs  A⇩1⌋"
using A_compE⇩1[OF Some] Cons_exp.prems  by auto
have "A ∪ A⇩1 ⊆ set Vs" using Cons_exp.prems A_fv[OF Some] by auto
hence "𝒟s (compEs⇩1 Vs es) ⌊last_index Vs  (A ∪ A⇩1)⌋" using Cons_exp Some by auto
hence "𝒟s (compEs⇩1 Vs es) ⌊last_index Vs  A ∪ last_index Vs  A⇩1⌋"
by(simp add: image_Un)
thus ?thesis using IH⇩1 indexA⇩1 by auto
qed
qed (simp_all add:hyperset_defs)
(*>*)

lemma last_index_image_set: "distinct xs ⟹ last_index xs  set xs = {..<size xs}"
(*<*)by(induct xs rule:rev_induct) (auto simp add: image_last_index)(*>*)

lemma D_compE⇩1:
"⟦ 𝒟 e ⌊set Vs⌋; fv e ⊆ set Vs; distinct Vs ⟧ ⟹ 𝒟 (compE⇩1 Vs e) ⌊{..<length Vs}⌋"
(*<*)by(fastforce dest!: D_last_index_compE⇩1[OF subset_refl] simp add:last_index_image_set)(*>*)

lemma D_compE⇩1':
assumes "𝒟 e ⌊set(V#Vs)⌋" and "fv e ⊆ set(V#Vs)" and "distinct(V#Vs)"
shows "𝒟 (compE⇩1 (V#Vs) e) ⌊{..length Vs}⌋"
(*<*)
proof -
have "{..size Vs} = {..<size(V#Vs)}" by auto
thus ?thesis using assms by (simp only:)(rule D_compE⇩1)
qed
(*>*)

lemma compP⇩1_pres_wf: "wf_J_prog P ⟹ wf_J⇩1_prog (compP⇩1 P)"
(*<*)
proof -
assume wf: "wf_J_prog P"
let ?f = "(λb (pns, body).
compE⇩1 (case b of Static ⇒ pns | NonStatic ⇒ this # pns) body)"
let ?wf⇩2 = "wf_J⇩1_mdecl"

{ fix C M b Ts T m
assume cM: "P ⊢ C sees M, b :  Ts→T = m in C"
and wfm: "wf_mdecl wf_J_mdecl P C (M, b, Ts, T, m)"
obtain pns body where [simp]: "m = (pns, body)" by(cases m) simp
let ?E = "λb. case b of Static ⇒ [pns [↦] Ts] | NonStatic ⇒ [pns [↦] Ts, this ↦ Class C]"
obtain T' where WT: "P,?E b ⊢ body :: T'" and subT: "P ⊢ T' ≤ T"
using wfm by(cases b) (auto simp: wf_mdecl_def)
have fv: "fv body ⊆ dom (?E b)" by(rule WT_fv[OF WT])
have "wf_mdecl ?wf⇩2 (compP ?f P) C (M, b, Ts, T, ?f b m)"
proof(cases b)
case Static then show ?thesis using cM wfm fv
by(auto simp:wf_mdecl_def wf_J⇩1_mdecl_def
intro!: compE⇩1_pres_wt D_compE⇩1 ℬ)
next
case NonStatic then show ?thesis using cM wfm fv
by(clarsimp simp add:wf_mdecl_def wf_J⇩1_mdecl_def)
(fastforce intro!: compE⇩1_pres_wt D_compE⇩1' ℬ)
qed
}
then show ?thesis by simp (rule wf_prog_compPI[OF _ wf])
qed
(*>*)

end
`