# Theory Exception_Tables

```(*  Title:      JinjaThreads/Compiler/Exception_Tables.thy
Author:     Andreas Lochbihler
*)

section ‹Various Operations for Exception Tables›

theory Exception_Tables imports
Compiler2
"../Common/ExternalCallWF"
"../JVM/JVMExceptions"
begin

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

lemma pcs_subset:
shows "pcs(compxE2 e pc d) ⊆ {pc..<pc+size(compE2 e)}"
and "pcs(compxEs2 es pc d) ⊆ {pc..<pc+size(compEs2 es)}"
apply(induct e pc d and es pc d rule: compxE2_compxEs2_induct)
apply (fastforce)+
done

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

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

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

lemma [simp]: "pc < pc⇩0 ∨ pc⇩0+size(compE2 e) ≤ pc ⟹ pc ∉ pcs(compxE2 e pc⇩0 d)"
using pcs_subset by fastforce

lemma [simp]: "pc < pc0 ∨ pc0+size(compEs2 es) ≤ pc ⟹ pc ∉ pcs(compxEs2 es pc0 d)"
using pcs_subset by fastforce

lemma [simp]: "pc1 + size(compE2 e1) ≤ pc2 ⟹ pcs(compxE2 e1 pc1 d1) ∩ pcs(compxE2 e2 pc2 d2) = {}"
using pcs_subset by fastforce

lemma [simp]: "pc⇩1 + size(compE2 e) ≤ pc⇩2 ⟹ pcs(compxE2 e pc⇩1 d⇩1) ∩ pcs(compxEs2 es pc⇩2 d⇩2) = {}"
using pcs_subset by fastforce

lemma match_ex_table_append_not_pcs [simp]:
"pc ∉ pcs xt0 ⟹ match_ex_table P C pc (xt0 @ xt1) = match_ex_table P C pc xt1"
by (induct xt0) (auto simp: matches_ex_entry_def)

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

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

lemma outside_pcs_compxEs2_not_matches_entry [simp]:
assumes xe: "xe ∈ set(compxEs2 es pc d)"
and outside: "pc' < pc ∨ pc+size(compEs2 es) ≤ pc'"
shows "¬ matches_ex_entry P C pc' xe"
proof
assume "matches_ex_entry P C pc' xe"
with xe have "pc' ∈ pcs(compxEs2 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 match_ex_table_eq_NoneI [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_table_not_pcs_None:
"pc ∉ pcs xt ⟹ match_ex_table P C pc xt = None"
by(auto intro: match_ex_table_eq_NoneI)

lemma match_ex_entry:
fixes start shows
"matches_ex_entry P C pc (start, end, catch_type, handler) =
(start ≤ pc ∧ pc < end ∧ (case catch_type of None ⇒ True | ⌊C'⌋ ⇒ P ⊢ C ≼⇧* C'))"

lemma pcs_compxE2D [dest]:
"pc ∈ pcs (compxE2 e pc' d) ⟹ pc' ≤ pc ∧ pc < pc' + length (compE2 e)"
using pcs_subset by(fastforce)

lemma pcs_compxEs2D [dest]:
"pc ∈ pcs (compxEs2 es pc' d) ⟹ pc' ≤ pc ∧ pc < pc' + length (compEs2 es)"
using pcs_subset by(fastforce)

definition shift :: "nat ⇒ ex_table ⇒ ex_table"
where
"shift n xt ≡ map (λ(from,to,C,handler,depth). (n+from,n+to,C,n+handler,depth)) xt"

lemma shift_0 [simp]: "shift 0 xt = xt"
by(induct xt)(auto simp:shift_def)

lemma shift_Nil [simp]: "shift n [] = []"

lemma shift_Cons_tuple [simp]:
"shift n ((from, to, C, handler, depth) # xt) = (from + n, to + n, C, handler + n, depth) # shift n xt"

lemma shift_append [simp]: "shift n (xt⇩1 @ xt⇩2) = shift n xt⇩1 @ shift n xt⇩2"

lemma shift_shift [simp]: "shift m (shift n xt) = shift (m+n) xt"

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
shows shift_compxE2: "shift pc (compxE2 e pc' d) = compxE2 e (pc' + pc) d"
and  shift_compxEs2: "shift pc (compxEs2 es pc' d) = compxEs2 es (pc' + pc) d"
by(induct e and es arbitrary: pc pc' d and pc pc' d rule: compE2.induct compEs2.induct)
(auto simp:shift_def ac_simps)

lemma compxE2_size_convs [simp]: "n ≠ 0 ⟹ compxE2 e n d = shift n (compxE2 e 0 d)"
and compxEs2_size_convs: "n ≠ 0 ⟹ compxEs2 es n d = shift n (compxEs2 es 0 d)"

lemma pcs_shift_conv [simp]: "pcs (shift n xt) = (+) n ` pcs xt"
apply(rule_tac x="x-n" in image_eqI)
apply(auto)
apply(rule bexI)
prefer 2
apply(assumption)
apply(auto)
done

lemma image_plus_const_conv [simp]:
fixes m :: nat
shows "m ∈ (+) n ` A ⟷ m ≥ n ∧ m - n ∈ A"
by(force)

lemma match_ex_table_shift_eq_None_conv [simp]:
"match_ex_table P C pc (shift n xt) = None ⟷ pc < n ∨ match_ex_table P C (pc - n) xt = None"
by(induct xt)(auto simp add: match_ex_entry split: if_split_asm)

lemma match_ex_table_shift_pc_None:
"pc ≥ n ⟹ match_ex_table P C pc (shift n xt) = None ⟷ match_ex_table P C (pc - n) xt = None"

lemma match_ex_table_shift_eq_Some_conv [simp]:
"match_ex_table P C pc (shift n xt) = ⌊(pc', d)⌋ ⟷
pc ≥ n ∧ pc' ≥ n ∧ match_ex_table P C (pc - n) xt = ⌊(pc' - n, d)⌋"
by(induct xt)(auto simp add: match_ex_entry split: if_split_asm)

lemma match_ex_table_shift:
"match_ex_table P C pc xt = ⌊(pc', d)⌋ ⟹ match_ex_table P C (n + pc) (shift n xt) = ⌊(n + pc', d)⌋"

lemma match_ex_table_shift_pcD:
"match_ex_table P C pc (shift n xt) = ⌊(pc', d)⌋ ⟹ pc ≥ n ∧ pc' ≥ n ∧ match_ex_table P C (pc - n) xt = ⌊(pc' - n, d)⌋"

lemma match_ex_table_pcsD: "match_ex_table P C pc xt = ⌊(pc', D)⌋ ⟹ pc ∈ pcs xt"
by(induct xt)(auto split: if_split_asm simp add: match_ex_entry)

definition stack_xlift :: "nat ⇒ ex_table ⇒ ex_table"
where "stack_xlift n xt ≡ map (λ(from,to,C,handler,depth). (from, to, C, handler, n + depth)) xt"

lemma stack_xlift_0 [simp]: "stack_xlift 0 xt = xt"
by(induct xt, auto simp add: stack_xlift_def)

lemma stack_xlift_Nil [simp]: "stack_xlift n [] = []"

lemma stack_xlift_Cons_tuple [simp]:
"stack_xlift n ((from, to, C, handler, depth) # xt) = (from, to, C, handler, depth + n) # stack_xlift n xt"

lemma stack_xlift_append [simp]: "stack_xlift n (xt @ xt') = stack_xlift n xt @ stack_xlift n xt'"

lemma stack_xlift_stack_xlift [simp]: "stack_xlift n (stack_xlift m xt) = stack_xlift (n + m) xt"

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
shows stack_xlift_compxE2: "stack_xlift n (compxE2 e pc d) = compxE2 e pc (n + d)"
and stack_xlift_compxEs2: "stack_xlift n (compxEs2 es pc d) = compxEs2 es pc (n + d)"
by(induct e and es arbitrary: d pc and d pc rule: compE2.induct compEs2.induct)
(auto simp add: shift_compxE2 simp del: compxE2_size_convs)

lemma compxE2_stack_xlift_convs [simp]: "d > 0 ⟹ compxE2 e pc d = stack_xlift d (compxE2 e pc 0)"
and compxEs2_stack_xlift_convs [simp]: "d > 0 ⟹ compxEs2 es pc d = stack_xlift d (compxEs2 es pc 0)"

lemma stack_xlift_shift [simp]: "stack_xlift d (shift n xt) = shift n (stack_xlift d xt)"
by(induct xt)(auto)

lemma pcs_stack_xlift_conv [simp]: "pcs (stack_xlift n xt) = pcs xt"

lemma match_ex_table_stack_xlift_eq_None_conv [simp]:
"match_ex_table P C pc (stack_xlift d xt) = None ⟷ match_ex_table P C pc xt = None"

lemma match_ex_table_stack_xlift_eq_Some_conv [simp]:
"match_ex_table P C pc (stack_xlift n xt) = ⌊(pc', d)⌋ ⟷ d ≥ n ∧ match_ex_table P C pc xt = ⌊(pc', d - n)⌋"

lemma match_ex_table_stack_xliftD:
"match_ex_table P C pc (stack_xlift n xt) = ⌊(pc', d)⌋ ⟹ d ≥ n ∧ match_ex_table P C pc xt = ⌊(pc', d - n)⌋"
by(simp)

lemma match_ex_table_stack_xlift:
"match_ex_table P C pc xt = ⌊(pc', d)⌋ ⟹ match_ex_table P C pc (stack_xlift n xt) = ⌊(pc', n + d)⌋"
by simp

lemma pcs_stack_xlift: "pcs (stack_xlift n xt) = pcs xt"

lemma match_ex_table_None_append [simp]:
"match_ex_table P C pc xt = None
⟹ match_ex_table P C pc (xt @ xt') = match_ex_table P C pc xt'"
by(induct xt, auto)

lemma match_ex_table_Some_append [simp]:
"match_ex_table P C pc xt = ⌊(pc', d)⌋ ⟹ match_ex_table P C pc (xt @ xt') = ⌊(pc', d)⌋"
by(induct xt)(auto)

lemma match_ex_table_append:
"match_ex_table P C pc (xt @ xt') = (case match_ex_table P C pc xt of None ⇒ match_ex_table P C pc xt'
| Some pcd ⇒ Some pcd)"
by(auto)

lemma match_ex_table_pc_length_compE2:
"match_ex_table P a pc (compxE2 e pc' d) = ⌊pcd⌋ ⟹ pc' ≤ pc ∧ pc < length (compE2 e) + pc'"

and match_ex_table_pc_length_compEs2:
"match_ex_table P a pc (compxEs2 es pc' d) = ⌊pcd⌋ ⟹ pc' ≤ pc ∧ pc < length (compEs2 es) + pc'"
using pcs_subset by(cases pcd, fastforce dest!: match_ex_table_pcsD)+

lemma match_ex_table_compxE2_shift_conv:
"f > 0 ⟹ match_ex_table P C pc (compxE2 e f d) = ⌊(pc', d')⌋ ⟷ pc ≥ f ∧ pc' ≥ f ∧ match_ex_table P C (pc - f) (compxE2 e 0 d) = ⌊(pc' - f, d')⌋"
by simp

lemma match_ex_table_compxEs2_shift_conv:
"f > 0 ⟹ match_ex_table P C pc (compxEs2 es f d) = ⌊(pc', d')⌋ ⟷ pc ≥ f ∧ pc' ≥ f ∧ match_ex_table P C (pc - f) (compxEs2 es 0 d) = ⌊(pc' - f, d')⌋"

lemma match_ex_table_compxE2_stack_conv:
"d > 0 ⟹ match_ex_table P C pc (compxE2 e 0 d) = ⌊(pc', d')⌋ ⟷ d' ≥ d ∧ match_ex_table P C pc (compxE2 e 0 0) = ⌊(pc', d' - d)⌋"
by simp

lemma match_ex_table_compxEs2_stack_conv:
"d > 0 ⟹ match_ex_table P C pc (compxEs2 es 0 d) = ⌊(pc', d')⌋ ⟷ d' ≥ d ∧ match_ex_table P C pc (compxEs2 es 0 0) = ⌊(pc', d' - d)⌋"