# Theory Correctness2

```(*  Title:      Jinja/Compiler/Correctness2.thy
Author:     Tobias Nipkow
*)

section ‹Correctness of Stage 2›

theory Correctness2
imports "HOL-Library.Sublist" Compiler2
begin

(*<*)hide_const (open) Throw(*>*)

subsection‹Instruction sequences›

text‹How to select individual instructions and subsequences of
instructions from a program given the class, method and program
counter.›

definition before :: "jvm_prog ⇒ cname ⇒ mname ⇒ nat ⇒ instr list ⇒ bool"
("(_,_,_,_/ ⊳ _)" [51,0,0,0,51] 50) where
"P,C,M,pc ⊳ is ⟷ prefix is (drop pc (instrs_of P C M))"

definition at :: "jvm_prog ⇒ cname ⇒ mname ⇒ nat ⇒ instr ⇒ bool"
("(_,_,_,_/ ▹ _)" [51,0,0,0,51] 50) where
"P,C,M,pc ▹ i ⟷ (∃is. drop pc (instrs_of P C M) = i#is)"

lemma [simp]: "P,C,M,pc ⊳ []"

lemma [simp]: "P,C,M,pc ⊳ (i#is) = (P,C,M,pc ▹ i ∧ P,C,M,pc + 1 ⊳ is)"
(*<*)by(fastforce simp add:before_def at_def prefix_def drop_Suc drop_tl)(*>*)

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

lemma [simp]: "P,C,M,pc ⊳ (is⇩1 @ is⇩2) = (P,C,M,pc ⊳ is⇩1 ∧ P,C,M,pc + size is⇩1 ⊳ is⇩2)"
(*<*)
(*>*)

(*<*)
declare drop_drop[simp]
(*>*)

lemma [simp]: "P,C,M,pc ▹ i ⟹ instrs_of P C M ! pc = i"

lemma beforeM:
"P ⊢ C sees M: Ts→T = body in D ⟹
compP⇩2 P,D,M,0 ⊳ compE⇩2 body @ [Return]"
(*<*)
by(drule sees_method_idemp)
(*>*)

text‹This lemma executes a single instruction by rewriting:›

lemma [simp]:
"P,C,M,pc ▹ instr ⟹
(P ⊢ (None, h, (vs,ls,C,M,pc) # frs) -jvm→ σ') =
((None, h, (vs,ls,C,M,pc) # frs) = σ' ∨
(∃σ. exec(P,(None, h, (vs,ls,C,M,pc) # frs)) = Some σ ∧ P ⊢ σ -jvm→ σ'))"
(*<*)
by(simp only: exec_all_def)
(blast intro: converse_rtranclE converse_rtrancl_into_rtrancl)
(*>*)

subsection‹Exception tables›

definition pcs :: "ex_table ⇒ nat set"
where
"pcs xt  ≡  ⋃(f,t,C,h,d) ∈ set xt. {f ..< t}"

lemma pcs_subset:
shows "⋀pc d. pcs(compxE⇩2 e pc d) ⊆ {pc..<pc+size(compE⇩2 e)}"
and "⋀pc d. pcs(compxEs⇩2 es pc d) ⊆ {pc..<pc+size(compEs⇩2 es)}"
(*<*)
proof(induct e and es rule: compxE⇩2.induct compxEs⇩2.induct)
case Cast then show ?case by (fastforce simp:pcs_def)
next
case BinOp then show ?case by (fastforce simp:pcs_def split:bop.splits)
next
case LAss then show ?case by (fastforce simp: pcs_def)
next
case FAcc then show ?case by (fastforce simp: pcs_def)
next
case FAss then show ?case by (fastforce simp: pcs_def)
next
case Call then show ?case by (fastforce simp: pcs_def)
next
case Seq then show ?case by (fastforce simp: pcs_def)
next
case Cond then show ?case by (fastforce simp: pcs_def)
next
case While then show ?case by (fastforce simp: pcs_def)
next
case throw then show ?case by (fastforce simp: pcs_def)
next
case TryCatch then show ?case by (fastforce simp: pcs_def)
next
case Cons_exp then show ?case by (fastforce simp: pcs_def)
(*>*)

lemma [simp]: "pcs [] = {}"

lemma [simp]: "pcs (x#xt) = {fst x ..< fst(snd x)} ∪ pcs xt"

lemma [simp]: "pcs(xt⇩1 @ xt⇩2) = pcs xt⇩1 ∪ pcs xt⇩2"

lemma [simp]: "pc < pc⇩0 ∨ pc⇩0+size(compE⇩2 e) ≤ pc ⟹ pc ∉ pcs(compxE⇩2 e pc⇩0 d)"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]: "pc < pc⇩0 ∨ pc⇩0+size(compEs⇩2 es) ≤ pc ⟹ pc ∉ pcs(compxEs⇩2 es pc⇩0 d)"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]: "pc⇩1 + size(compE⇩2 e⇩1) ≤ pc⇩2 ⟹ pcs(compxE⇩2 e⇩1 pc⇩1 d⇩1) ∩ pcs(compxE⇩2 e⇩2 pc⇩2 d⇩2) = {}"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]: "pc⇩1 + size(compE⇩2 e) ≤ pc⇩2 ⟹ pcs(compxE⇩2 e pc⇩1 d⇩1) ∩ pcs(compxEs⇩2 es pc⇩2 d⇩2) = {}"
(*<*)using pcs_subset by fastforce(*>*)

lemma [simp]:
"pc ∉ pcs xt⇩0 ⟹ match_ex_table P C pc (xt⇩0 @ xt⇩1) = match_ex_table P C pc xt⇩1"
(*<*)by (induct xt⇩0) (auto simp: matches_ex_entry_def)(*>*)

lemma [simp]: "⟦ x ∈ set xt; pc ∉ pcs xt ⟧ ⟹ ¬ matches_ex_entry P D pc x"
(*<*)by(auto simp:matches_ex_entry_def pcs_def)(*>*)

lemma [simp]:
assumes xe: "xe ∈ set(compxE⇩2 e pc d)" and outside: "pc' < pc ∨ pc+size(compE⇩2 e) ≤ pc'"
shows "¬ matches_ex_entry P C pc' xe"
(*<*)
proof
assume "matches_ex_entry P C pc' xe"
with xe have "pc' ∈ pcs(compxE⇩2 e pc d)"
with outside show False by simp
qed
(*>*)

lemma [simp]:
assumes xe: "xe ∈ set(compxEs⇩2 es pc d)" and outside: "pc' < pc ∨ pc+size(compEs⇩2 es) ≤ pc'"
shows "¬ matches_ex_entry P C pc' xe"
(*<*)
proof
assume "matches_ex_entry P C pc' xe"
with xe have "pc' ∈ pcs(compxEs⇩2 es pc d)"
with outside show False by simp
qed
(*>*)

lemma match_ex_table_app[simp]:
"∀xte ∈ set xt⇩1. ¬ matches_ex_entry P D pc xte ⟹
match_ex_table P D pc (xt⇩1 @ xt) = match_ex_table P D pc xt"
(*<*)by(induct xt⇩1) simp_all(*>*)

lemma [simp]:
"∀x ∈ set xtab. ¬ matches_ex_entry P C pc x ⟹
match_ex_table P C pc xtab = None"
(*<*)using match_ex_table_app[where ?xt = "[]"] by fastforce(*>*)

lemma match_ex_entry:
"matches_ex_entry P C pc (start, end, catch_type, handler) =
(start ≤ pc ∧ pc < end ∧  P ⊢ C ≼⇧* catch_type)"

definition caught :: "jvm_prog ⇒ pc ⇒ heap ⇒ addr ⇒ ex_table ⇒ bool" where
"caught P pc h a xt ⟷
(∃entry ∈ set xt. matches_ex_entry P (cname_of h a) pc entry)"

definition beforex :: "jvm_prog ⇒ cname ⇒ mname ⇒ ex_table ⇒ nat set ⇒ nat ⇒ bool"
("(2_,/_,/_ ⊳/ _ /'/ _,/_)" [51,0,0,0,0,51] 50) where
"P,C,M ⊳ xt / I,d ⟷
(∃xt⇩0 xt⇩1. ex_table_of P C M = xt⇩0 @ xt @ xt⇩1 ∧ pcs xt⇩0 ∩ I = {} ∧ pcs xt ⊆ I ∧
(∀pc ∈ I. ∀C pc' d'. match_ex_table P C pc xt⇩1 = ⌊(pc',d')⌋ ⟶ d' ≤ d))"

definition dummyx :: "jvm_prog ⇒ cname ⇒ mname ⇒ ex_table ⇒ nat set ⇒ nat ⇒ bool"  ("(2_,_,_ ▹/ _ '/_,_)" [51,0,0,0,0,51] 50) where
"P,C,M ▹ xt/I,d ⟷ P,C,M ⊳ xt/I,d"

abbreviation
"beforex⇩0 P C M d I xt xt⇩0 xt⇩1
≡ ex_table_of P C M = xt⇩0 @ xt @ xt⇩1 ∧ pcs xt⇩0 ∩ I = {}
∧ pcs xt ⊆ I ∧ (∀pc ∈ I. ∀C pc' d'. match_ex_table P C pc xt⇩1 = ⌊(pc',d')⌋ ⟶ d' ≤ d)"

lemma beforex_beforex⇩0_eq:
"P,C,M ⊳ xt / I,d ≡ ∃xt⇩0 xt⇩1. beforex⇩0 P C M d I xt xt⇩0 xt⇩1"
using beforex_def by auto

lemma beforexD1: "P,C,M ⊳ xt / I,d ⟹ pcs xt ⊆ I"

lemma beforex_mono: "⟦ P,C,M ⊳ xt/I,d'; d' ≤ d ⟧ ⟹ P,C,M ⊳ xt/I,d"
(*<*)by(fastforce simp:beforex_def)(*>*)

lemma [simp]: "P,C,M ⊳ xt/I,d ⟹ P,C,M ⊳ xt/I,Suc d"
(*<*)by(fastforce intro:beforex_mono)(*>*)

lemma beforex_append[simp]:
"pcs xt⇩1 ∩ pcs xt⇩2 = {} ⟹
P,C,M ⊳ xt⇩1 @ xt⇩2/I,d =
(P,C,M ⊳ xt⇩1/I-pcs xt⇩2,d  ∧  P,C,M ⊳ xt⇩2/I-pcs xt⇩1,d ∧ P,C,M ▹ xt⇩1@xt⇩2/I,d)"
(*<*)(is "?Q ⟹ ?P = (?P1 ∧ ?P2 ∧ ?P3)" is "?Q ⟹ ?P = ?P123")
proof -
assume pcs: ?Q
show ?thesis proof(rule iffI)
assume "?P123" then show ?P by(simp add:dummyx_def)
next
assume hyp: ?P
let ?xt = "xt⇩1 @ xt⇩2"
let ?beforex = "beforex⇩0 P C M d"
obtain xt⇩0 xt⇩1' where beforex: "?beforex I ?xt xt⇩0 xt⇩1'"
using hyp by(clarsimp simp: beforex_def)
have "∃xt⇩0 xt⇩1'. ?beforex (I - pcs xt⇩2) xt⇩1 xt⇩0 xt⇩1'" ― ‹?P1›
using pcs beforex by(rule_tac x=xt⇩0 in exI) auto
moreover have "∃xt⇩0 xt⇩1'. ?beforex (I - pcs xt⇩1) xt⇩2 xt⇩0 xt⇩1'"  ― ‹?P2›
using pcs beforex by(rule_tac x="xt⇩0@xt⇩1" in exI) auto
moreover have ?P3 using hyp by(simp add: dummyx_def)
ultimately show ?P123 by (simp add: beforex_def)
qed
qed
(*>*)

lemma beforex_appendD1:
assumes bx: "P,C,M ⊳ xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)] / I,d"
and pcs: "pcs xt⇩1 ⊆ J" and JI: "J ⊆ I" and Jpcs: "J ∩ pcs xt⇩2 = {}"
shows "P,C,M ⊳ xt⇩1 / J,d"
(*<*)
proof -
let ?beforex = "beforex⇩0 P C M d"
obtain xt⇩0 xt⇩1' where bx': "?beforex I (xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)]) xt⇩0 xt⇩1'"
using bx by(clarsimp simp:beforex_def)
let ?xt0 = xt⇩0 and ?xt1 = "xt⇩2 @ (f, t, D, h, d) # xt⇩1'"
have "pcs xt⇩0 ∩ J = {}" using bx' JI by blast
moreover {
fix pc C pc' d' assume pcJ: "pc∈J"
then have "pc ∉ pcs xt⇩2" using bx' Jpcs by blast
then have "match_ex_table P C pc (xt⇩2 @ (f, t, D, h, d) # xt⇩1')
= ⌊(pc', d')⌋ ⟶ d' ≤ d"
using bx' JI pcJ by (auto split:if_split_asm)
}
ultimately have "?beforex J xt⇩1 ?xt0 ?xt1" using bx' pcs by simp
then show ?thesis using beforex_def by blast
qed
(*>*)

lemma beforex_appendD2:
assumes bx: "P,C,M ⊳ xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)] / I,d"
and pcs: "pcs xt⇩2 ⊆ J" and JI: "J ⊆ I" and Jpcs: "J ∩ pcs xt⇩1 = {}"
shows "P,C,M ⊳ xt⇩2 / J,d"
(*<*)
proof -
let ?beforex = "beforex⇩0 P C M d"
obtain xt⇩0 xt⇩1' where bx': "?beforex I (xt⇩1 @ xt⇩2 @ [(f,t,D,h,d)]) xt⇩0 xt⇩1'"
using bx by(clarsimp simp:beforex_def)
then have "∃xt⇩1''. beforex⇩0 P C M d J xt⇩2 (xt⇩0 @ xt⇩1) xt⇩1''"
using assms by fastforce
then show ?thesis using beforex_def by blast
qed
(*>*)

lemma beforexM:
"P ⊢ C sees M: Ts→T = body in D ⟹
compP⇩2 P,D,M ⊳ compxE⇩2 body 0 0/{..<size(compE⇩2 body)},0"
(*<*)
proof -
assume cM: "P ⊢ C sees M: Ts→T = body in D"
let ?xt0 = "[]"
have "∃xt1. beforex⇩0 (compP⇩2 P) D M 0 ({..<size(compE⇩2 body)}) (compxE⇩2 body 0 0) ?xt0 xt1"
using sees_method_compP[where f = compMb⇩2, OF sees_method_idemp[OF cM]]
pcs_subset by(fastforce simp add: compP⇩2_def compMb⇩2_def)
then show ?thesis using beforex_def by blast
qed
(*>*)

lemma match_ex_table_SomeD2:
assumes met: "match_ex_table P D pc (ex_table_of P C M) = ⌊(pc',d')⌋"
and bx: "P,C,M ⊳ xt/I,d"
and nmet: "∀x ∈ set xt. ¬ matches_ex_entry P D pc x" and pcI: "pc ∈ I"
shows "d' ≤ d"
(*<*)
proof -
obtain xt⇩0 xt⇩1 where bx': "beforex⇩0 P C M d I xt xt⇩0 xt⇩1"
using bx by(clarsimp simp:beforex_def)
then have "pc ∉ pcs xt⇩0" using pcI by blast
then show ?thesis using bx' met nmet pcI by simp
qed
(*>*)

lemma match_ex_table_SomeD1:
"⟦ match_ex_table P D pc (ex_table_of P C M) = ⌊(pc',d')⌋;
P,C,M ⊳ xt / I,d; pc ∈ I; pc ∉ pcs xt ⟧ ⟹ d' ≤ d"
(*<*)by(auto elim: match_ex_table_SomeD2)(*>*)

subsection‹The correctness proof›

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

definition
handle :: "jvm_prog ⇒ cname ⇒ mname ⇒ addr ⇒ heap ⇒ val list ⇒ val list ⇒ nat ⇒ frame list
⇒ jvm_state" where
"handle P C M a h vs ls pc frs = find_handler P a h ((vs,ls,C,M,pc) # frs)"

lemma handle_Cons:
"⟦ P,C,M ⊳ xt/I,d; d ≤ size vs; pc ∈ I;
∀x ∈ set xt. ¬ matches_ex_entry P (cname_of h xa) pc x ⟧ ⟹
handle P C M xa h (v # vs) ls pc frs = handle P C M xa h vs ls pc frs"
(*<*)by(auto simp:handle_def Suc_diff_le dest: match_ex_table_SomeD2)(*>*)

lemma handle_append:
assumes bx: "P,C,M ⊳ xt/I,d" and d: "d ≤ size vs"
and pcI: "pc ∈ I" and pc_not: "pc ∉ pcs xt"
shows "handle P C M xa h (ws @ vs) ls pc frs = handle P C M xa h vs ls pc frs"
(*<*)
proof -
{ fix pc' d'
assume "match_ex_table P (cname_of h xa) pc (ex_table_of P C M) = ⌊(pc', d')⌋"
then have "length ws ≤ length ws + length vs - d'"
using assms by(fastforce dest:match_ex_table_SomeD2 split:nat_diff_split)
}
then show ?thesis by(simp add: handle_def)
qed
(*>*)

lemma aux_isin[simp]: "⟦ B ⊆ A; a ∈ B ⟧ ⟹ a ∈ A"
(*<*)by blast(*>*)

lemma fixes P⇩1 defines [simp]: "P ≡ compP⇩2 P⇩1"
shows Jcc:
"P⇩1 ⊢⇩1 ⟨e,(h⇩0,ls⇩0)⟩ ⇒ ⟨ef,(h⇩1,ls⇩1)⟩ ⟹
(⋀C M pc v xa vs frs I.
⟦ P,C,M,pc ⊳ compE⇩2 e; P,C,M ⊳ compxE⇩2 e pc (size vs)/I,size vs;
{pc..<pc+size(compE⇩2 e)} ⊆ I ⟧ ⟹
(ef = Val v ⟶
P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(v#vs,ls⇩1,C,M,pc+size(compE⇩2 e))#frs))
∧
(ef = Throw xa ⟶
(∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compE⇩2 e) ∧
¬ caught P pc⇩1 h⇩1 xa (compxE⇩2 e pc (size vs)) ∧
P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ handle P C M xa h⇩1 vs ls⇩1 pc⇩1 frs)))"
(*<*)
(is "_ ⟹ (⋀C M pc v xa vs frs I.
PROP ?P e h⇩0 ls⇩0 ef h⇩1 ls⇩1 C M pc v xa vs frs I)")
(*>*)

and "P⇩1 ⊢⇩1 ⟨es,(h⇩0,ls⇩0)⟩ [⇒] ⟨fs,(h⇩1,ls⇩1)⟩ ⟹
(⋀C M pc ws xa es' vs frs I.
⟦ P,C,M,pc ⊳ compEs⇩2 es; P,C,M ⊳ compxEs⇩2 es pc (size vs)/I,size vs;
{pc..<pc+size(compEs⇩2 es)} ⊆ I ⟧ ⟹
(fs = map Val ws ⟶
P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(rev ws @ vs,ls⇩1,C,M,pc+size(compEs⇩2 es))#frs))
∧
(fs = map Val ws @ Throw xa # es' ⟶
(∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < pc + size(compEs⇩2 es) ∧
¬ caught P pc⇩1 h⇩1 xa (compxEs⇩2 es pc (size vs)) ∧
P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ handle P C M xa h⇩1 vs ls⇩1 pc⇩1 frs)))"
(*<*)
(is "_ ⟹ (⋀C M pc ws xa es' vs frs I.
PROP ?Ps es h⇩0 ls⇩0 fs h⇩1 ls⇩1 C M pc ws xa es' vs frs I)")
proof (induct rule:eval⇩1_evals⇩1_inducts)
case New⇩1 thus ?case by (clarsimp simp add:blank_def fun_eq_iff)
next
case NewFail⇩1 thus ?case by(auto simp: handle_def pcs_def)
next
case (Cast⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs C')
let ?pc = "pc + length(compE⇩2 e)"
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc)#frs)" using Cast⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc+1)#frs)"
using Cast⇩1 by (auto simp add:cast_ok_def)
finally show ?case by auto
next
case (CastNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 C')
let ?pc = "pc + length(compE⇩2 e)"
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Null#vs,ls⇩1,C,M,?pc)#frs)"
using CastNull⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩1,(Null#vs,ls⇩1,C,M,?pc+1)#frs)"
using CastNull⇩1 by (auto simp add:cast_ok_def)
finally show ?case by auto
next
case (CastFail⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs C')
let ?pc = "pc + length(compE⇩2 e)"
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
using CastFail⇩1 by fastforce
also have "P ⊢ … -jvm→ handle P C M ?xa h⇩1 (Addr a#vs) ls⇩1 ?pc frs"
using CastFail⇩1 by (auto simp add:handle_def cast_ok_def)
also have "handle P C M ?xa h⇩1 (Addr a#vs) ls⇩1 ?pc frs =
handle P C M ?xa h⇩1 vs ls⇩1 ?pc frs"
using CastFail⇩1.prems by(auto simp:handle_Cons)
finally have exec: "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ …".
show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩1. ?H pc⇩1))")
proof
show ?N by simp
next
have "?eq ⟶ ?H ?pc" using exec by auto
thus "?eq ⟶ (∃pc⇩1. ?H pc⇩1)" by blast
qed
next
case CastThrow⇩1 thus ?case by fastforce
next
case Val⇩1 thus ?case by simp
next
case Var⇩1 thus ?case by auto
next
case (BinOp⇩1 e⇩1 h⇩0 ls⇩0 v⇩1 h⇩1 ls⇩1 e⇩2 v⇩2 h⇩2 ls⇩2 bop w)
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?pc⇩2 = "?pc⇩1 + length(compE⇩2 e⇩2)"
have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 (Val v⇩2) h⇩2 ls⇩2 C M ?pc⇩1 v⇩2 xa (v⇩1#vs) frs
(I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc⇩1)#frs)" using BinOp⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩2,(v⇩2#v⇩1#vs,ls⇩2,C,M,?pc⇩2)#frs)"
using BinOp⇩1.prems IH⇩2 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩2,(w#vs,ls⇩2,C,M,?pc⇩2+1)#frs)"
using BinOp⇩1 by(cases bop) auto
finally show ?case by (auto split: bop.splits simp:add.assoc)
next
case BinOpThrow⇩1⇩1 thus ?case by(fastforce)
next
case (BinOpThrow⇩2⇩1 e⇩1 h⇩0 ls⇩0 v⇩1 h⇩1 ls⇩1 e⇩2 e h⇩2 ls⇩2 bop)
let ?pc = "pc + length(compE⇩2 e⇩1)"
let ?σ⇩1 = "(None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc)#frs)"
have 1: "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ ?σ⇩1"
using BinOpThrow⇩2⇩1 by fastforce
show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
proof
show ?N by simp
next
{ assume ?eq
moreover
have "PROP ?P e⇩2 h⇩1 ls⇩1 (throw e) h⇩2 ls⇩2 C M ?pc v xa (v⇩1#vs) frs
(I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
ultimately obtain pc⇩2 where
pc⇩2: "?pc ≤ pc⇩2 ∧ pc⇩2 < ?pc + size(compE⇩2 e⇩2) ∧
¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc (size vs + 1))" and
2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (v⇩1#vs) ls⇩2 pc⇩2 frs"
using BinOpThrow⇩2⇩1.prems by fastforce
have 3: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
using 2 BinOpThrow⇩2⇩1.prems pc⇩2 by(auto simp:handle_Cons)
have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 3] by auto
hence "∃pc⇩2. ?H pc⇩2" by iprover
}
thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
qed
next
case (FAcc⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 C fs F D w)
let ?pc = "pc + length(compE⇩2 e)"
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc)#frs)" using FAcc⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩1,(w#vs,ls⇩1,C,M,?pc+1)#frs)"
using FAcc⇩1 by auto
finally show ?case by auto
next
case (FAccNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 F D)
let ?pc = "pc + length(compE⇩2 e)"
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Null#vs,ls⇩1,C,M,?pc)#frs)" using FAccNull⇩1 by fastforce
also have "P ⊢ … -jvm→ handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs"
using FAccNull⇩1.prems
by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
also have "handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs =
handle P C M ?xa h⇩1 vs ls⇩1 ?pc frs"
finally show ?case by (auto intro: exI[where x = ?pc])
next
case FAccThrow⇩1 thus ?case by fastforce
next
case (LAss⇩1 e h⇩0 ls⇩0 w h⇩1 ls⇩1 i ls⇩2)
let ?pc = "pc + length(compE⇩2 e)"
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(w#vs,ls⇩1,C,M,?pc)#frs)" using LAss⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩1,(Unit#vs,ls⇩2,C,M,?pc+2)#frs)"
using LAss⇩1 by auto
finally show ?case using LAss⇩1 by auto
next
case LAssThrow⇩1 thus ?case by fastforce
next
case (FAss⇩1 e⇩1 h⇩0 ls⇩0 a h⇩1 ls⇩1 e⇩2 w h⇩2 ls⇩2 C fs fs' F D h⇩2')
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?pc⇩2 = "?pc⇩1 + length(compE⇩2 e⇩2)"
have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 (Val w) h⇩2 ls⇩2 C M ?pc⇩1 w xa (Addr a#vs) frs
(I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Addr a#vs,ls⇩1,C,M,?pc⇩1)#frs)" using FAss⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩2,(w#Addr a#vs,ls⇩2,C,M,?pc⇩2)#frs)"
using FAss⇩1.prems IH⇩2 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩2',(Unit#vs,ls⇩2,C,M,?pc⇩2+2)#frs)"
using FAss⇩1 by auto
finally show ?case using FAss⇩1 by (auto simp:add.assoc)
next
case (FAssNull⇩1 e⇩1 h⇩0 ls⇩0 h⇩1 ls⇩1 e⇩2 w h⇩2 ls⇩2 F D)
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?pc⇩2 = "?pc⇩1 + length(compE⇩2 e⇩2)"
have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 (Val w) h⇩2 ls⇩2 C M ?pc⇩1 w xa (Null#vs) frs
(I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Null#vs,ls⇩1,C,M,?pc⇩1)#frs)" using FAssNull⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩2,(w#Null#vs,ls⇩2,C,M,?pc⇩2)#frs)"
using FAssNull⇩1.prems IH⇩2 by fastforce
also have "P ⊢ … -jvm→ handle P C M ?xa h⇩2 (w#Null#vs) ls⇩2 ?pc⇩2 frs"
using FAssNull⇩1.prems
by(fastforce simp:split_beta handle_def simp del: split_paired_Ex)
also have "handle P C M ?xa h⇩2 (w#Null#vs) ls⇩2 ?pc⇩2 frs =
handle P C M ?xa h⇩2 vs ls⇩2 ?pc⇩2 frs"
finally show ?case by (auto intro: exI[where x = ?pc⇩2])
next
case (FAssThrow⇩2⇩1 e⇩1 h⇩0 ls⇩0 w h⇩1 ls⇩1 e⇩2 e' h⇩2 ls⇩2 F D)
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?σ⇩1 = "(None,h⇩1,(w#vs,ls⇩1,C,M,?pc⇩1)#frs)"
have 1: "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→ ?σ⇩1"
using FAssThrow⇩2⇩1 by fastforce
show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
proof
show ?N by simp
next
{ assume ?eq
moreover
have "PROP ?P e⇩2 h⇩1 ls⇩1 (throw e') h⇩2 ls⇩2 C M ?pc⇩1 v xa (w#vs) frs
(I - pcs (compxE⇩2 e⇩1 pc (length vs)))" by fact
ultimately obtain pc⇩2 where
pc⇩2: "?pc⇩1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1 + size(compE⇩2 e⇩2) ∧
¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc⇩1 (size vs + 1))" and
2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (w#vs) ls⇩2 pc⇩2 frs"
using FAssThrow⇩2⇩1.prems by fastforce
have 3: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
using 2 FAssThrow⇩2⇩1.prems pc⇩2 by(auto simp:handle_Cons)
have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 3] by auto
hence "∃pc⇩2. ?H pc⇩2" by iprover
}
thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
qed
next
case FAssThrow⇩1⇩1 thus ?case by fastforce
next
case (Call⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1 es pvs h⇩2 ls⇩2 Ca fs M' Ts T body D ls⇩2' f h⇩3 ls⇩3)
have "P⇩1 ⊢⇩1 ⟨es,(h⇩1, ls⇩1)⟩ [⇒] ⟨map Val pvs,(h⇩2, ls⇩2)⟩" by fact
hence [simp]: "length es = length pvs" by(auto dest:evals⇩1_preserves_elen)
let ?σ⇩0 = "(None,h⇩0,(vs, ls⇩0, C,M,pc)#frs)"
let ?pc⇩1 = "pc + length(compE⇩2 e)"
let ?σ⇩1 = "(None,h⇩1,(Addr a # vs, ls⇩1, C,M,?pc⇩1)#frs)"
let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
let ?frs⇩2 = "(rev pvs @ Addr a # vs, ls⇩2, C,M,?pc⇩2)#frs"
let ?σ⇩2 = "(None,h⇩2,?frs⇩2)"
let ?frs⇩2' = "([], ls⇩2', D,M',0) # ?frs⇩2"
let ?σ⇩2' = "(None, h⇩2, ?frs⇩2')"
have IH_es: "PROP ?Ps es h⇩1 ls⇩1 (map Val pvs) h⇩2 ls⇩2 C M ?pc⇩1 pvs xa
(map Val pvs) (Addr a # vs) frs (I - pcs(compxE⇩2 e pc (size vs)))" by fact
have "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" using Call⇩1 by fastforce
also have "P ⊢ … -jvm→ ?σ⇩2" using IH_es Call⇩1.prems by fastforce
also have "P ⊢ … -jvm→ ?σ⇩2'"
using Call⇩1 by(auto simp add: nth_append compMb⇩2_def)
finally have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩2'".
have "P⇩1 ⊢ Ca sees M': Ts→T = body in D" by fact
then have M'_in_D: "P⇩1 ⊢ D sees M': Ts→T = body in D"
by(rule sees_method_idemp)
hence M'_code: "compP⇩2 P⇩1,D,M',0 ⊳ compE⇩2 body @ [Return]"
and M'_xtab: "compP⇩2 P⇩1,D,M' ⊳ compxE⇩2 body 0 0/{..<size(compE⇩2 body)},0"
by(rule beforeM, rule beforexM)
have IH_body: "PROP ?P body h⇩2 ls⇩2' f h⇩3 ls⇩3 D M' 0 v xa [] ?frs⇩2 ({..<size(compE⇩2 body)})" by fact
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm (is "?val ⟶ ?trans")
proof
assume val: ?val
note 1
also have "P ⊢ ?σ⇩2' -jvm→
(None,h⇩3,([v],ls⇩3,D,M',size(compE⇩2 body))#?frs⇩2)"
using val IH_body Call⇩1.prems M'_code M'_xtab
by (fastforce simp del:split_paired_Ex)
also have "P ⊢ … -jvm→ (None, h⇩3, (v # vs, ls⇩2, C,M,?pc⇩2+1)#frs)"
using Call⇩1 M'_code M'_in_D by(auto simp: nth_append compMb⇩2_def)
qed
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
assume throw: ?throw
with IH_body obtain pc⇩2 where
pc⇩2: "0 ≤ pc⇩2 ∧ pc⇩2 < size(compE⇩2 body) ∧
¬ caught P pc⇩2 h⇩3 xa (compxE⇩2 body 0 0)" and
2: "P ⊢ ?σ⇩2' -jvm→ handle P D M' xa h⇩3 [] ls⇩3 pc⇩2 ?frs⇩2"
using Call⇩1.prems M'_code M'_xtab
by (fastforce simp del:split_paired_Ex)
have "handle P D M' xa h⇩3 [] ls⇩3 pc⇩2 ?frs⇩2 =
handle P C M xa h⇩3 (rev pvs @ Addr a # vs) ls⇩2 ?pc⇩2 frs"
using pc⇩2 M'_in_D by(auto simp add:handle_def)
also have "… = handle P C M xa h⇩3 vs ls⇩2 ?pc⇩2 frs"
using Call⇩1.prems by(auto simp add:handle_append handle_Cons)
finally have "?H ?pc⇩2" using pc⇩2 jvm_trans[OF 1 2] by auto
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case (CallParamsThrow⇩1 e h⇩0 ls⇩0 w h⇩1 ls⇩1 es es' h⇩2 ls⇩2 pvs ex es'' M')
let ?σ⇩0 = "(None,h⇩0,(vs, ls⇩0, C,M,pc)#frs)"
let ?pc⇩1 = "pc + length(compE⇩2 e)"
let ?σ⇩1 = "(None,h⇩1,(w # vs, ls⇩1, C,M,?pc⇩1)#frs)"
let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" using CallParamsThrow⇩1 by fastforce
show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
proof
show ?N by simp
next
{ assume ?eq
moreover
have "PROP ?Ps es h⇩1 ls⇩1 es' h⇩2 ls⇩2 C M ?pc⇩1 pvs xa es'' (w#vs) frs
(I - pcs (compxE⇩2 e pc (length vs)))" by fact
ultimately have "∃pc⇩2.
(?pc⇩1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1 + size(compEs⇩2 es) ∧
¬ caught P pc⇩2 h⇩2 xa (compxEs⇩2 es ?pc⇩1 (size vs + 1))) ∧
P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (w#vs) ls⇩2 pc⇩2 frs"
(is "∃pc⇩2. ?PC pc⇩2 ∧ ?Exec pc⇩2")
using CallParamsThrow⇩1 by force
then obtain pc⇩2 where pc⇩2: "?PC pc⇩2" and 2: "?Exec pc⇩2" by iprover
have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 2] CallParamsThrow⇩1
by(auto simp:handle_Cons)
hence "∃pc⇩2. ?H pc⇩2" by iprover
}
thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
qed
next
case (CallNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 es pvs h⇩2 ls⇩2 M')
have "P⇩1 ⊢⇩1 ⟨es,(h⇩1, ls⇩1)⟩ [⇒] ⟨map Val pvs,(h⇩2, ls⇩2)⟩" by fact
hence [simp]: "length es = length pvs" by(auto dest:evals⇩1_preserves_elen)
let ?pc⇩1 = "pc + length(compE⇩2 e)"
let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
have IH_es: "PROP ?Ps es h⇩1 ls⇩1 (map Val pvs) h⇩2 ls⇩2 C M ?pc⇩1 pvs xa
(map Val pvs) (Null#vs) frs (I - pcs(compxE⇩2 e pc (size vs)))" by fact
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Null#vs,ls⇩1,C,M,?pc⇩1)#frs)" using CallNull⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩2,(rev pvs@Null#vs,ls⇩2,C,M,?pc⇩2)#frs)"
using CallNull⇩1 IH_es by fastforce
also have "P ⊢ … -jvm→ handle P C M ?xa h⇩2 (rev pvs@Null#vs) ls⇩2 ?pc⇩2 frs"
using CallNull⇩1.prems
by(auto simp:split_beta handle_def nth_append simp del: split_paired_Ex)
also have "handle P C M ?xa h⇩2 (rev pvs@Null#vs) ls⇩2 ?pc⇩2 frs =
handle P C M ?xa h⇩2 vs ls⇩2 ?pc⇩2 frs"
using CallNull⇩1.prems by(auto simp:handle_Cons handle_append)
finally show ?case by (auto intro: exI[where x = ?pc⇩2])
next
case CallObjThrow⇩1 thus ?case by fastforce
next
case Block⇩1 thus ?case by auto
next
case (Seq⇩1 e⇩1 h⇩0 ls⇩0 w h⇩1 ls⇩1 e⇩2 e⇩2' h⇩2 ls⇩2)
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩1+1)#frs)"
have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(w#vs,ls⇩1,C,M,?pc⇩1)#frs)"
using Seq⇩1 by fastforce
also have "P ⊢ … -jvm→ ?σ⇩1" using Seq⇩1 by auto
finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
let ?pc⇩2 = "?pc⇩1 + 1 + length(compE⇩2 e⇩2)"
have IH⇩2: "PROP ?P e⇩2 h⇩1 ls⇩1 e⇩2' h⇩2 ls⇩2 C M (?pc⇩1+1) v xa vs frs
(I - pcs(compxE⇩2 e⇩1 pc (size vs)))" by fact
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm (is "?val ⟶ ?trans")
proof
assume val: ?val
note eval⇩1
also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2)#frs)"
using val Seq⇩1.prems IH⇩2 by fastforce
qed
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
assume throw: ?throw
then obtain pc⇩2 where
pc⇩2: "?pc⇩1+1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2 ∧
¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 (?pc⇩1+1) (size vs))" and
eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
using IH⇩2 Seq⇩1.prems by fastforce
have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case SeqThrow⇩1 thus ?case by fastforce
next
case (CondT⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 e⇩1 e' h⇩2 ls⇩2 e⇩2)
let ?pc⇩1 = "pc + length(compE⇩2 e)"
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩1+1)#frs)"
have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool(True)#vs,ls⇩1,C,M,?pc⇩1)#frs)"
using CondT⇩1 by (fastforce simp add: Int_Un_distrib)
also have "P ⊢ … -jvm→ ?σ⇩1" using CondT⇩1 by auto
finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
let ?pc⇩1' = "?pc⇩1 + 1 + length(compE⇩2 e⇩1)"
let ?pc⇩2' = "?pc⇩1' + 1 + length(compE⇩2 e⇩2)"
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm (is "?val ⟶ ?trans")
proof
assume val: ?val
note eval⇩1
also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩1')#frs)"
using val CondT⇩1 by(fastforce simp:Int_Un_distrib)
also have "P ⊢ … -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2')#frs)"
qed
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
let ?d = "size vs"
let ?I = "I - pcs(compxE⇩2 e pc ?d) - pcs(compxE⇩2 e⇩2 (?pc⇩1'+1) ?d)"
assume throw: ?throw
moreover
have "PROP ?P e⇩1 h⇩1 ls⇩1 e' h⇩2 ls⇩2 C M (?pc⇩1+1) v xa vs frs ?I" by fact
ultimately obtain pc⇩2 where
pc⇩2: "?pc⇩1+1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1' ∧
¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩1 (?pc⇩1+1) (size vs))" and
eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
using CondT⇩1.prems by (fastforce simp:Int_Un_distrib)
have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case (CondF⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 e⇩2 e' h⇩2 ls⇩2 e⇩1)
let ?pc⇩1 = "pc + length(compE⇩2 e)"
let ?pc⇩2 = "?pc⇩1 + 1 + length(compE⇩2 e⇩1)+ 1"
let ?pc⇩2' = "?pc⇩2 + length(compE⇩2 e⇩2)"
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩2)#frs)"
have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool(False)#vs,ls⇩1,C,M,?pc⇩1)#frs)"
using CondF⇩1 by (fastforce simp add: Int_Un_distrib)
also have "P ⊢ … -jvm→ ?σ⇩1" using CondF⇩1 by auto
finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm (is "?val ⟶ ?trans")
proof
assume val: ?val
note eval⇩1
also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2')#frs)"
using val CondF⇩1 by(fastforce simp:Int_Un_distrib)
qed
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
let ?d = "size vs"
let ?I = "I - pcs(compxE⇩2 e pc ?d) - pcs(compxE⇩2 e⇩1 (?pc⇩1+1) ?d)"
assume throw: ?throw
moreover
have "PROP ?P e⇩2 h⇩1 ls⇩1 e' h⇩2 ls⇩2 C M ?pc⇩2 v xa vs frs ?I" by fact
ultimately obtain pc⇩2 where
pc⇩2: "?pc⇩2 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2' ∧
¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc⇩2 ?d)" and
eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
using CondF⇩1.prems by(fastforce simp:Int_Un_distrib)
have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case (CondThrow⇩1 e h⇩0 ls⇩0 f h⇩1 ls⇩1 e⇩1 e⇩2)
let ?d = "size vs"
let ?xt⇩1 = "compxE⇩2 e⇩1 (pc+size(compE⇩2 e)+1) ?d"
let ?xt⇩2 = "compxE⇩2 e⇩2 (pc+size(compE⇩2 e)+size(compE⇩2 e⇩1)+2) ?d"
let ?I = "I - (pcs ?xt⇩1 ∪ pcs ?xt⇩2)"
have "pcs(compxE⇩2 e pc ?d) ∩ pcs(?xt⇩1 @ ?xt⇩2) = {}"
moreover have "PROP ?P e h⇩0 ls⇩0 (throw f) h⇩1 ls⇩1 C M pc v xa vs frs ?I" by fact
ultimately show ?case using CondThrow⇩1.prems by fastforce
next
case (WhileF⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 c)
let ?pc = "pc + length(compE⇩2 e)"
let ?pc' = "?pc + length(compE⇩2 c) + 3"
have "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(Bool False#vs,ls⇩1,C,M,?pc)#frs)"
using WhileF⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩1,(vs,ls⇩1,C,M,?pc')#frs)"
also have "P ⊢ … -jvm→ (None,h⇩1,(Unit#vs,ls⇩1,C,M,?pc'+1)#frs)"
using WhileF⇩1.prems by (auto simp:eval_nat_numeral)
next
case (WhileT⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 c v⇩1 h⇩2 ls⇩2 e⇩3 h⇩3 ls⇩3)
let ?pc = "pc + length(compE⇩2 e)"
let ?pc' = "?pc + length(compE⇩2 c) + 1"
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?σ⇩2 = "(None,h⇩2,(vs,ls⇩2,C,M,pc)#frs)"
have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool True#vs,ls⇩1,C,M,?pc)#frs)"
using WhileT⇩1 by fastforce
also have "P ⊢ … -jvm→ (None,h⇩1,(vs,ls⇩1,C,M,?pc+1)#frs)"
using WhileT⇩1.prems by auto
also have "P ⊢ … -jvm→ (None,h⇩2,(v⇩1#vs,ls⇩2,C,M,?pc')#frs)"
using WhileT⇩1 by(fastforce)
also have "P ⊢ … -jvm→ ?σ⇩2" using WhileT⇩1.prems by auto
finally have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩2".
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm (is "?val ⟶ ?trans")
proof
assume val: ?val
note 1
also have "P ⊢ ?σ⇩2 -jvm→ (None,h⇩3,(v#vs,ls⇩3,C,M,?pc'+3)#frs)"
qed
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
assume throw: ?throw
moreover
have "PROP ?P (while (e) c) h⇩2 ls⇩2 e⇩3 h⇩3 ls⇩3 C M pc v xa vs frs I" by fact
ultimately obtain pc⇩2 where
pc⇩2: "pc ≤ pc⇩2 ∧ pc⇩2 < ?pc'+3 ∧
¬ caught P pc⇩2 h⇩3 xa (compxE⇩2 (while (e) c) pc (size vs))" and
2: "P ⊢ ?σ⇩2 -jvm→ handle P C M xa h⇩3 vs ls⇩3 pc⇩2 frs"
using WhileT⇩1.prems by (auto simp:add.assoc eval_nat_numeral)
have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 2] by auto
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case WhileCondThrow⇩1 thus ?case by fastforce
next
case (WhileBodyThrow⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1 c e' h⇩2 ls⇩2)
let ?pc⇩1 = "pc + length(compE⇩2 e)"
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?σ⇩1 = "(None,h⇩1,(vs,ls⇩1,C,M,?pc⇩1+1)#frs)"
have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,(Bool(True)#vs,ls⇩1,C,M,?pc⇩1)#frs)"
using WhileBodyThrow⇩1 by (fastforce simp add: Int_Un_distrib)
also have "P ⊢ … -jvm→ ?σ⇩1" using  WhileBodyThrow⇩1 by auto
finally have eval⇩1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1".
let ?pc⇩1' = "?pc⇩1 + 1 + length(compE⇩2 c)"
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm by simp
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
assume throw: ?throw
moreover
have "PROP ?P c h⇩1 ls⇩1 (throw e') h⇩2 ls⇩2 C M (?pc⇩1+1) v xa vs frs
(I - pcs (compxE⇩2 e pc (size vs)))" by fact
ultimately obtain pc⇩2 where
pc⇩2: "?pc⇩1+1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩1' ∧
¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 c (?pc⇩1+1) (size vs))" and
eval⇩2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
using WhileBodyThrow⇩1.prems by (fastforce simp:Int_Un_distrib)
have "?H pc⇩2" using pc⇩2 jvm_trans[OF eval⇩1 eval⇩2] by auto
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case (Throw⇩1 e h⇩0 ls⇩0 a h⇩1 ls⇩1)
let ?pc = "pc + size(compE⇩2 e)"
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm by simp
next
show ?Err (is "?throw ⟶ (∃pc⇩1. ?H pc⇩1)")
proof
assume ?throw
hence "P ⊢ (None, h⇩0, (vs, ls⇩0, C, M, pc) # frs) -jvm→
(None, h⇩1, (Addr xa#vs, ls⇩1, C, M, ?pc) # frs)"
using Throw⇩1 by fastforce
also have "P ⊢ … -jvm→ handle P C M xa h⇩1 (Addr xa#vs) ls⇩1 ?pc frs"
also have "handle P C M xa h⇩1 (Addr xa#vs) ls⇩1 ?pc frs =
handle P C M xa h⇩1 vs ls⇩1 ?pc frs"
finally have "?H ?pc" by simp
thus "∃pc⇩1. ?H pc⇩1" by iprover
qed
qed
next
case (ThrowNull⇩1 e h⇩0 ls⇩0 h⇩1 ls⇩1)
let ?pc = "pc + size(compE⇩2 e)"
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm by simp
next
show ?Err (is "?throw ⟶ (∃pc⇩1. ?H pc⇩1)")
proof
assume throw: ?throw
have "P ⊢ (None, h⇩0, (vs, ls⇩0, C, M, pc) # frs) -jvm→
(None, h⇩1, (Null#vs, ls⇩1, C, M, ?pc) # frs)"
using ThrowNull⇩1 by fastforce
also have "P ⊢ … -jvm→  handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs"
also have "handle P C M ?xa h⇩1 (Null#vs) ls⇩1 ?pc frs =
handle P C M ?xa h⇩1 vs ls⇩1 ?pc frs"
finally have "?H ?pc" using throw by simp
thus "∃pc⇩1. ?H pc⇩1" by iprover
qed
qed
next
case ThrowThrow⇩1 thus ?case by fastforce
next
case (Try⇩1 e⇩1 h⇩0 ls⇩0 v⇩1 h⇩1 ls⇩1 Ci i e⇩2)
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?pc⇩1' = "?pc⇩1 + 2 + length(compE⇩2 e⇩2)"
have "P,C,M ⊳ compxE⇩2 (try e⇩1 catch(Ci i) e⇩2) pc (size vs) / I,size vs" by fact
hence "P,C,M ⊳ compxE⇩2 e⇩1 pc (size vs) /
{pc..<pc + length (compE⇩2 e⇩1)},size vs"
using Try⇩1.prems by (fastforce simp:beforex_def split:if_split_asm)
hence "P ⊢ (None,h⇩0,(vs,ls⇩0,C,M,pc)#frs) -jvm→
(None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc⇩1)#frs)" using Try⇩1 by auto
also have "P ⊢ … -jvm→ (None,h⇩1,(v⇩1#vs,ls⇩1,C,M,?pc⇩1')#frs)"
using Try⇩1.prems by auto
finally show ?case by (auto simp:add.assoc)
next
case (TryCatch⇩1 e⇩1 h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs Ci i e⇩2 e⇩2' h⇩2 ls⇩2)
let ?e = "try e⇩1 catch(Ci i) e⇩2"
let ?xt = "compxE⇩2 ?e pc (size vs)"
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?ls⇩1 = "ls⇩1[i := Addr a]"
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?pc⇩1' = "?pc⇩1 + 2"
let ?σ⇩1 = "(None,h⇩1,(vs,?ls⇩1,C,M, ?pc⇩1') # frs)"
have I: "{pc..<pc + length (compE⇩2 (try e⇩1 catch(Ci i) e⇩2))} ⊆ I"
and beforex: "P,C,M ⊳ ?xt/I,size vs" by fact+
have "P ⊢ ?σ⇩0 -jvm→ (None,h⇩1,((Addr a)#vs,ls⇩1,C,M, ?pc⇩1+1) # frs)"
proof -
have "PROP ?P e⇩1 h⇩0 ls⇩0 (Throw a) h⇩1 ls⇩1 C M pc w a vs frs {pc..<pc + length (compE⇩2 e⇩1)}"
by fact
moreover have "P,C,M ⊳ compxE⇩2 e⇩1 pc (size vs)/{pc..<?pc⇩1},size vs"
using beforex I pcs_subset by(force elim!: beforex_appendD1)
ultimately have
"∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < ?pc⇩1 ∧
¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs)) ∧
P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs"
using  TryCatch⇩1.prems by auto
then obtain pc⇩1 where
pc⇩1_in_e⇩1: "pc ≤ pc⇩1" "pc⇩1 < ?pc⇩1" and
pc⇩1_not_caught: "¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs))" and
0: "P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs" by iprover
from beforex obtain xt⇩0 xt⇩1
where ex_tab: "ex_table_of P C M = xt⇩0 @ ?xt @ xt⇩1"
and disj: "pcs xt⇩0 ∩ I = {}" by(auto simp:beforex_def)
have hp: "h⇩1 a = Some (D, fs)" "P⇩1 ⊢ D ≼⇧* Ci" by fact+
have "pc⇩1 ∉ pcs xt⇩0" using pc⇩1_in_e⇩1 I disj by auto
with pc⇩1_in_e⇩1 pc⇩1_not_caught hp
show ?thesis using ex_tab 0 by(simp add:handle_def matches_ex_entry_def)
qed
also have "P ⊢ … -jvm→ ?σ⇩1" using TryCatch⇩1 by auto
finally have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" .
let ?pc⇩2 = "?pc⇩1' + length(compE⇩2 e⇩2)"
let ?I⇩2 = "{?pc⇩1' ..< ?pc⇩2}"
have "P,C,M ⊳ compxE⇩2 ?e pc (size vs) / I,size vs" by fact
hence beforex⇩2: "P,C,M ⊳ compxE⇩2 e⇩2 ?pc⇩1' (size vs) / ?I⇩2, size vs"
using I pcs_subset[of _ ?pc⇩1'] by(auto elim!:beforex_appendD2)
have IH⇩2: "PROP ?P e⇩2 h⇩1 ?ls⇩1 e⇩2' h⇩2 ls⇩2 C M ?pc⇩1' v xa vs frs ?I⇩2" by fact
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm (is "?val ⟶ ?trans")
proof
assume val: ?val
note 1 also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(v#vs,ls⇩2,C,M,?pc⇩2)#frs)"
using val beforex⇩2 IH⇩2 TryCatch⇩1.prems by auto
qed
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
assume throw: ?throw
then obtain pc⇩2 where
pc⇩2: "?pc⇩1+2 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2 ∧
¬ caught P pc⇩2 h⇩2 xa (compxE⇩2 e⇩2 ?pc⇩1' (size vs))" and
2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 vs ls⇩2 pc⇩2 frs"
using IH⇩2 beforex⇩2 TryCatch⇩1.prems by auto
have "?H pc⇩2" using pc⇩2 jvm_trans[OF 1 2]
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case (TryThrow⇩1 e⇩1 h⇩0 ls⇩0 a h⇩1 ls⇩1 D fs Ci i e⇩2)
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?pc⇩1 = "pc + length(compE⇩2 e⇩1)"
let ?e = "try e⇩1 catch(Ci i) e⇩2"
let ?xt = "compxE⇩2 ?e pc (size vs)"
have I: "{pc..<pc + length (compE⇩2 (try e⇩1 catch(Ci i) e⇩2))} ⊆ I"
and beforex: "P,C,M ⊳ ?xt/I,size vs" by fact+
have "PROP ?P e⇩1 h⇩0 ls⇩0 (Throw a) h⇩1 ls⇩1 C M pc w a vs frs {pc..<pc + length (compE⇩2 e⇩1)}" by fact
moreover have "P,C,M ⊳ compxE⇩2 e⇩1 pc (size vs)/{pc..<?pc⇩1},size vs"
using beforex I pcs_subset by(force elim!: beforex_appendD1)
ultimately have
"∃pc⇩1. pc ≤ pc⇩1 ∧ pc⇩1 < ?pc⇩1 ∧
¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs)) ∧
P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs"
using TryThrow⇩1.prems by auto
then obtain pc⇩1 where
pc⇩1_in_e⇩1: "pc ≤ pc⇩1" "pc⇩1 < ?pc⇩1" and
pc⇩1_not_caught: "¬ caught P pc⇩1 h⇩1 a (compxE⇩2 e⇩1 pc (size vs))" and
0: "P ⊢ ?σ⇩0 -jvm→ handle P C M a h⇩1 vs ls⇩1 pc⇩1 frs" by iprover
show ?case (is "?N ∧ (?eq ⟶ (∃pc⇩2. ?H pc⇩2))")
proof
show ?N by simp
next
{ assume ?eq
with TryThrow⇩1 pc⇩1_in_e⇩1 pc⇩1_not_caught 0
have "?H pc⇩1" by (simp add:match_ex_entry) auto
hence "∃pc⇩2. ?H pc⇩2" by iprover
}
thus "?eq ⟶ (∃pc⇩2. ?H pc⇩2)" by iprover
qed
next
case Nil⇩1 thus ?case by simp
next
case (Cons⇩1 e h⇩0 ls⇩0 v h⇩1 ls⇩1 es fs h⇩2 ls⇩2)
let ?pc⇩1 = "pc + length(compE⇩2 e)"
let ?σ⇩0 = "(None,h⇩0,(vs,ls⇩0,C,M,pc)#frs)"
let ?σ⇩1 = "(None,h⇩1,(v#vs,ls⇩1,C,M,?pc⇩1)#frs)"
have 1: "P ⊢ ?σ⇩0 -jvm→ ?σ⇩1" using Cons⇩1 by fastforce
let ?pc⇩2 = "?pc⇩1 + length(compEs⇩2 es)"
have IHs: "PROP ?Ps es h⇩1 ls⇩1 fs h⇩2 ls⇩2 C M ?pc⇩1 (tl ws) xa es' (v#vs) frs
(I - pcs (compxE⇩2 e pc (length vs)))" by fact
show ?case (is "?Norm ∧ ?Err")
proof
show ?Norm (is "?val ⟶ ?trans")
proof
assume val: ?val
note 1
also have "P ⊢ ?σ⇩1 -jvm→ (None,h⇩2,(rev(ws) @ vs,ls⇩2,C,M,?pc⇩2)#frs)"
using val IHs Cons⇩1.prems by fastforce
qed
next
show ?Err (is "?throw ⟶ (∃pc⇩2. ?H pc⇩2)")
proof
assume throw: ?throw
then obtain pc⇩2 where
pc⇩2: "?pc⇩1 ≤ pc⇩2 ∧ pc⇩2 < ?pc⇩2 ∧
¬ caught P pc⇩2 h⇩2 xa (compxEs⇩2 es ?pc⇩1 (size vs + 1))" and
2: "P ⊢ ?σ⇩1 -jvm→ handle P C M xa h⇩2 (v#vs) ls⇩2 pc⇩2 frs"
using IHs Cons⇩1.prems
by(fastforce simp:Cons_eq_append_conv neq_Nil_conv)
have "?H pc⇩2" using Cons⇩1.prems pc⇩2 jvm_trans[OF 1 2]
thus "∃pc⇩2. ?H pc⇩2" by iprover
qed
qed
next
case ConsThrow⇩1 thus ?case by (fastforce simp:Cons_eq_append_conv)
qed
(*>*)

(*FIXME move! *)
lemma atLeast0AtMost[simp]: "{0::nat..n} = {..n}"
by auto

lemma atLeast0LessThan[simp]: "{0::nat..<n} = {..<n}"
by auto

fun exception :: "'a exp ⇒ addr option" where
"exception (Throw a) = Some a"
| "exception e = None"

lemma comp⇩2_correct:
assumes "method": "P⇩1 ⊢ C sees M:Ts→T = body in C"
and eval:   "P⇩1 ⊢⇩1 ⟨body,(h,ls)⟩ ⇒ ⟨e',(h',ls')⟩"
shows "compP⇩2 P⇩1 ⊢ (None,h,[([],ls,C,M,0)]) -jvm→ (exception e',h',[])"
(*<*)
(is "_ ⊢ ?σ⇩0 -jvm→ ?σ⇩1")
proof -
let ?P = "compP⇩2 P⇩1"
have code: "?P,C,M,0 ⊳ compE⇩2 body" using beforeM[OF "method"] by auto
have xtab: "?P,C,M ⊳ compxE⇩2 body 0 (size[])/{..<size(compE⇩2 body)},size[]"
using beforexM[OF "method"] by auto
― ‹Distinguish if e' is a value or an exception›
{ fix v assume [simp]: "e' = Val v"
have "?P ⊢ ?σ⇩0 -jvm→ (None,h',[([v],ls',C,M,size(compE⇩2 body))])"
using Jcc[OF eval code xtab] by auto
also have "?P ⊢ … -jvm→ ?σ⇩1" using beforeM[OF "method"] by auto
finally have ?thesis .
}
moreover
{ fix a assume [simp]: "e' = Throw a"
obtain pc where pc: "0 ≤ pc ∧ pc < size(compE⇩2 body) ∧
¬ caught ?P pc h' a (compxE⇩2 body 0 0)"
and 1: "?P ⊢ ?σ⇩0 -jvm→ handle ?P C M a h' [] ls' pc []"
using Jcc[OF eval code xtab] by fastforce
from pc have "handle ?P C M a h' [] ls' pc [] = ?σ⇩1" using xtab "method"
by(auto simp:handle_def compMb⇩2_def)
with 1 have ?thesis by simp
}
ultimately show ?thesis using eval⇩1_final[OF eval] by(auto simp:final_def)
qed
(*>*)

end
```