# Theory Compiler1

```(*  Title:      JinjaThreads/Compiler/Compiler1.thy
Author:     Andreas Lochbihler, Tobias Nipkow

Based on Jinja/Compiler/Compiler1
*)

section ‹Compilation Stage 1›

theory Compiler1 imports
PCompiler
J1State
ListIndex
begin

definition fresh_var :: "vname list ⇒ vname"
where "fresh_var Vs = sum_list (STR ''V'' # Vs)"

lemma fresh_var_fresh: "fresh_var Vs ∉ set Vs"
proof -
have "V ∈ set Vs ⟹ length (String.explode V) < length (String.explode (fresh_var Vs))" for V
by (induction Vs) (auto simp add: fresh_var_def Literal.rep_eq)
then show ?thesis
by auto
qed

text‹Replacing variable names by indices.›

and compEs1 :: "vname list ⇒ 'addr expr list ⇒ 'addr expr1 list"
where
"compE1 Vs (new C) = new C"
| "compE1 Vs (newA T⌊e⌉) = newA T⌊compE1 Vs e⌉"
| "compE1 Vs (Cast T e) = Cast T (compE1 Vs e)"
| "compE1 Vs (e instanceof T) = (compE1 Vs e) instanceof T"
| "compE1 Vs (Val v) = Val v"
| "compE1 Vs (Var V) = Var(index Vs V)"
| "compE1 Vs (e«bop»e') = (compE1 Vs e)«bop»(compE1 Vs e')"
| "compE1 Vs (V:=e) = (index Vs V):= (compE1 Vs e)"
| "compE1 Vs (a⌊i⌉) = (compE1 Vs a)⌊compE1 Vs i⌉"
| "compE1 Vs (a⌊i⌉:=e) = (compE1 Vs a)⌊compE1 Vs i⌉:=compE1 Vs e"
| "compE1 Vs (a∙length) = compE1 Vs a∙length"
| "compE1 Vs (e∙F{D}) = compE1 Vs e∙F{D}"
| "compE1 Vs (e∙F{D}:=e') = compE1 Vs e∙F{D}:=compE1 Vs e'"
| "compE1 Vs (e∙compareAndSwap(D∙F, e', e'')) = compE1 Vs e∙compareAndSwap(D∙F, compE1 Vs e', compE1 Vs e'')"
| "compE1 Vs (e∙M(es)) = (compE1 Vs e)∙M(compEs1 Vs es)"
| "compE1 Vs {V:T=vo; e} = {(size Vs):T=vo; compE1 (Vs@[V]) e}"
| "compE1 Vs (sync⇘U⇙ (o') e) = sync⇘length Vs⇙ (compE1 Vs o') (compE1 (Vs@[fresh_var Vs]) e)"
| "compE1 Vs (insync⇘U⇙ (a) e) = insync⇘length Vs⇙ (a) (compE1 (Vs@[fresh_var Vs]) e)"
| "compE1 Vs (e1;;e2) = (compE1 Vs e1);;(compE1 Vs e2)"
| "compE1 Vs (if (b) e1 else e2) = (if (compE1 Vs b) (compE1 Vs e1) else (compE1 Vs e2))"
| "compE1 Vs (while (b) e) = (while (compE1 Vs b) (compE1 Vs e))"
| "compE1 Vs (throw e) = throw (compE1 Vs e)"
| "compE1 Vs (try e1 catch(C V) e2) = try(compE1 Vs e1) catch(C (size Vs)) (compE1 (Vs@[V]) e2)"

| "compEs1 Vs []     = []"
| "compEs1 Vs (e#es) = compE1 Vs e # compEs1 Vs es"
by pat_completeness auto
termination
apply(relation "case_sum (λp. size (snd p)) (λp. size_list size (snd p)) <*mlex*> {}")
apply(rule wf_mlex[OF wf_empty])
apply(rule mlex_less, simp)+
done

lemmas compE1_compEs1_induct =
compE1_compEs1.induct[case_names New NewArray Cast InstanceOf Val Var BinOp LAss AAcc AAss ALen FAcc FAss CAS Call Block Synchronized InSynchronized Seq Cond While throw TryCatch Nil Cons]

lemma compEs1_conv_map [simp]: "compEs1 Vs es = map (compE1 Vs) es"
by(induct es) simp_all

lemmas compEs1_map_Val = compEs1_conv_map

lemma compE1_eq_Val [simp]: "compE1 Vs e = Val v ⟷ e = Val v"
apply(cases e, auto)
done

lemma Val_eq_compE1 [simp]: "Val v = compE1 Vs e ⟷ e = Val v"
apply(cases e, auto)
done

lemma compEs1_eq_map_Val [simp]: "compEs1 Vs es = map Val vs ⟷ es = map Val vs"
apply(induct es arbitrary: vs)
apply(auto, blast)
done

lemma compE1_eq_Var [simp]: "compE1 Vs e = Var V ⟷ (∃V'. e = Var V' ∧ V = index Vs V')"
by(cases e, auto)

lemma compE1_eq_Call [simp]:
"compE1 Vs e = obj∙M(params) ⟷ (∃obj' params'. e = obj'∙M(params') ∧ compE1 Vs obj' = obj ∧ compEs1 Vs params' = params)"
by(cases e, auto)

lemma length_compEs2 [simp]:
"length (compEs1 Vs es) = length es"

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
shows expr_locks_compE1 [simp]: "expr_locks (compE1 Vs e) = expr_locks e"
and expr_lockss_compEs1 [simp]: "expr_lockss (compEs1 Vs es) = expr_lockss es"
by(induct Vs e and Vs es rule: compE1_compEs1.induct)(auto intro: ext)

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
shows contains_insync_compE1 [simp]: "contains_insync (compE1 Vs e) = contains_insync e"
and contains_insyncs_compEs1 [simp]: "contains_insyncs (compEs1 Vs es) = contains_insyncs es"
by(induct Vs e and Vs es rule: compE1_compEs1.induct)simp_all

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
shows max_vars_compE1: "max_vars (compE1 Vs e) = max_vars e"
apply(induct Vs e and Vs es rule: compE1_compEs1.induct)
apply(auto)
done

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
shows ℬ: "size Vs = n ⟹ ℬ (compE1 Vs e) n"
and ℬs: "size Vs = n ⟹ ℬs (compEs1 Vs es) n"
apply(induct Vs e and Vs es arbitrary: n and n rule: compE1_compEs1.induct)
apply auto
done

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
shows fv_compE1: "fv e ⊆ set Vs ⟹ fv (compE1 Vs e) = (index Vs) ` (fv e)"
and fvs_compEs1: "fvs es ⊆ set Vs ⟹ fvs (compEs1 Vs es) = (index Vs) ` (fvs es)"
proof(induct Vs e and Vs es rule: compE1_compEs1_induct)
case (Block Vs V ty vo exp)
have IH: "fv exp ⊆ set (Vs @ [V]) ⟹ fv (compE1 (Vs @ [V]) exp) = index (Vs @ [V]) ` fv exp" by fact
from ‹fv {V:ty=vo; exp} ⊆ set Vs› have fv': "fv exp ⊆ set (Vs @ [V])" by auto
from IH[OF this] have IH': "fv (compE1 (Vs @ [V]) exp) = index (Vs @ [V]) ` fv exp" .
have "fv (compE1 (Vs @ [V]) exp) - {length Vs} = index Vs ` (fv exp - {V})"
proof(rule equalityI[OF subsetI subsetI])
fix x
assume x: "x ∈ fv (compE1 (Vs @ [V]) exp) - {length Vs}"
hence "x ≠ length Vs" by simp
from x IH' have "x ∈ index (Vs @ [V]) ` fv exp" by simp
thus "x ∈ index Vs ` (fv exp - {V})"
proof(rule imageE)
fix y
assume [simp]: "x = index (Vs @ [V]) y"
and y: "y ∈ fv exp"
have "y ≠ V"
proof
assume [simp]: "y = V"
hence "x = length Vs" by simp
with ‹x ≠ length Vs› show False by contradiction
qed
moreover with fv' y have "y ∈ set Vs" by auto
ultimately have "index (Vs @ [V]) y = index Vs y" by(simp)
thus ?thesis using y ‹y ≠ V› by auto
qed
next
fix x
assume x: "x ∈ index Vs ` (fv exp - {V})"
thus "x ∈ fv (compE1 (Vs @ [V]) exp) - {length Vs}"
proof(rule imageE)
fix y
assume [simp]: "x = index Vs y"
and y: "y ∈ fv exp - {V}"
with fv' have "y ∈ set Vs" "y ≠ V" by auto
hence "index Vs y = index (Vs @ [V]) y" by simp
with y have "x ∈ index (Vs @ [V]) ` fv exp" by auto
thus ?thesis using IH' ‹y ∈ set Vs› by simp
qed
qed
thus ?case by simp
next
case (Synchronized Vs V exp1 exp2)
have IH1: "fv exp1 ⊆ set Vs ⟹ fv (compE1 Vs exp1) = index Vs ` fv exp1"
and IH2: "fv exp2 ⊆ set (Vs @ [fresh_var Vs]) ⟹ fv (compE1 (Vs @ [fresh_var Vs]) exp2) = index (Vs @ [fresh_var Vs]) ` fv exp2"
by fact+
from ‹fv (sync⇘V⇙ (exp1) exp2) ⊆ set Vs› have fv1: "fv exp1 ⊆ set Vs"
and fv2: "fv exp2 ⊆ set Vs" by auto
from fv2 have fv2': "fv exp2 ⊆ set (Vs @ [fresh_var Vs])" by auto
have "index (Vs @ [fresh_var Vs]) ` fv exp2 = index Vs ` fv exp2"
proof(rule equalityI[OF subsetI subsetI])
fix x
assume x: "x ∈ index (Vs @ [fresh_var Vs]) ` fv exp2"
thus "x ∈ index Vs ` fv exp2"
proof(rule imageE)
fix y
assume [simp]: "x = index (Vs @ [fresh_var Vs]) y"
and y: "y ∈ fv exp2"
from y fv2 have "y ∈ set Vs" by auto
moreover hence "y ≠ (fresh_var Vs)" by(auto simp add: fresh_var_fresh)
ultimately show ?thesis using y by(auto)
qed
next
fix x
assume x: "x ∈ index Vs ` fv exp2"
thus "x ∈ index (Vs @ [fresh_var Vs]) ` fv exp2"
proof(rule imageE)
fix y
assume [simp]: "x = index Vs y"
and y: "y ∈ fv exp2"
from y fv2 have "y ∈ set Vs" by auto
moreover hence "y ≠ (fresh_var Vs)" by(auto simp add: fresh_var_fresh)
ultimately have "index Vs y = index (Vs @ [fresh_var Vs]) y" by simp
thus ?thesis using y by(auto)
qed
qed
with IH1[OF fv1] IH2[OF fv2'] show ?case by(auto)
next
case (InSynchronized Vs V a exp)
have IH: "fv exp ⊆ set (Vs @ [fresh_var Vs]) ⟹ fv (compE1 (Vs @ [fresh_var Vs]) exp) = index (Vs @ [fresh_var Vs]) ` fv exp"
by fact
from ‹fv (insync⇘V⇙ (a) exp) ⊆ set Vs› have fv: "fv exp ⊆ set Vs" by simp
hence fv': "fv exp ⊆ set (Vs @ [fresh_var Vs])" by auto
have "index (Vs @ [fresh_var Vs]) ` fv exp = index Vs ` fv exp"
proof(rule equalityI[OF subsetI subsetI])
fix x
assume "x ∈ index (Vs @ [fresh_var Vs]) ` fv exp"
thus "x ∈ index Vs ` fv exp"
proof(rule imageE)
fix y
assume [simp]: "x = index (Vs @ [fresh_var Vs]) y"
and y: "y ∈ fv exp"
from y fv have "y ∈ set Vs" by auto
moreover hence "y ≠ (fresh_var Vs)" by(auto simp add: fresh_var_fresh)
ultimately have "index (Vs @ [fresh_var Vs]) y = index Vs y" by simp
thus ?thesis using y by simp
qed
next
fix x
assume "x ∈ index Vs ` fv exp"
thus "x ∈ index (Vs @ [fresh_var Vs]) ` fv exp"
proof(rule imageE)
fix y
assume [simp]: "x = index Vs y"
and y: "y ∈ fv exp"
from y fv have "y ∈ set Vs" by auto
moreover hence "y ≠ (fresh_var Vs)" by(auto simp add: fresh_var_fresh)
ultimately have "index Vs y = index (Vs @ [fresh_var Vs]) y" by simp
thus ?thesis using y by auto
qed
qed
with IH[OF fv'] show ?case by simp
next
case (TryCatch Vs exp1 C V exp2)
have IH1: "fv exp1 ⊆ set Vs ⟹ fv (compE1 Vs exp1) = index Vs ` fv exp1"
and IH2: "fv exp2 ⊆ set (Vs @ [V]) ⟹ fv (compE1 (Vs @ [V]) exp2) = index (Vs @ [V]) ` fv exp2"
by fact+
from ‹fv (try exp1 catch(C V) exp2) ⊆ set Vs› have fv1: "fv exp1 ⊆ set Vs"
and fv2: "fv exp2 ⊆ set (Vs @ [V])" by auto
have "index (Vs @ [V]) ` fv exp2 - {length Vs} = index Vs ` (fv exp2 - {V})"
proof(rule equalityI[OF subsetI subsetI])
fix x
assume x: "x ∈ index (Vs @ [V]) ` fv exp2 - {length Vs}"
hence "x ≠ length Vs" by simp
from x have "x ∈ index (Vs @ [V]) ` fv exp2" by auto
thus "x ∈ index Vs ` (fv exp2 - {V})"
proof(rule imageE)
fix y
assume [simp]: "x = index (Vs @ [V]) y"
and y: "y ∈ fv exp2"
have "y ≠ V"
proof
assume [simp]: "y = V"
hence "x = length Vs" by simp
with ‹x ≠ length Vs› show False by contradiction
qed
moreover with fv2 y have "y ∈ set Vs" by auto
ultimately have "index (Vs @ [V]) y = index Vs y" by(simp)
thus ?thesis using y ‹y ≠ V› by auto
qed
next
fix x
assume x: "x ∈ index Vs ` (fv exp2 - {V})"
thus "x ∈ index (Vs @ [V]) ` fv exp2 - {length Vs}"
proof(rule imageE)
fix y
assume [simp]: "x = index Vs y"
and y: "y ∈ fv exp2 - {V}"
with fv2 have "y ∈ set Vs" "y ≠ V" by auto
hence "index Vs y = index (Vs @ [V]) y" by simp
with y have "x ∈ index (Vs @ [V]) ` fv exp2" by auto
thus ?thesis using ‹y ∈ set Vs› by simp
qed
qed
with IH1[OF fv1] IH2[OF fv2] show ?case by auto
qed(auto)

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
shows syncvars_compE1: "fv e ⊆ set Vs ⟹ syncvars (compE1 Vs e)"
and syncvarss_compEs1: "fvs es ⊆ set Vs ⟹ syncvarss (compEs1 Vs es)"
proof(induct Vs e and Vs es rule: compE1_compEs1_induct)
case (Block Vs V ty vo exp)
from ‹fv {V:ty=vo; exp} ⊆ set Vs› have "fv exp ⊆ set (Vs @ [V])" by auto
from ‹fv exp ⊆ set (Vs @ [V]) ⟹ syncvars (compE1 (Vs @ [V]) exp)›[OF this] show ?case by(simp)
next
case (Synchronized Vs V exp1 exp2)
note IH1 = ‹fv exp1 ⊆ set Vs ⟹ syncvars (compE1 Vs exp1)›
note IH2 = ‹fv exp2 ⊆ set (Vs @ [fresh_var Vs]) ⟹ syncvars (compE1 (Vs @ [fresh_var Vs]) exp2)›
from ‹fv (sync⇘V⇙ (exp1) exp2) ⊆ set Vs› have fv1: "fv exp1 ⊆ set Vs"
and fv2: "fv exp2 ⊆ set Vs" and fv2': "fv exp2 ⊆ set (Vs @ [fresh_var Vs])" by auto
have "length Vs ∉ index (Vs @ [fresh_var Vs]) ` fv exp2"
proof
assume "length Vs ∈ index (Vs @ [fresh_var Vs]) ` fv exp2"
thus False
proof(rule imageE)
fix x
assume x: "length Vs = index (Vs @ [fresh_var Vs]) x"
and x': "x ∈ fv exp2"
from x' fv2 have "x ∈ set Vs" "x ≠ (fresh_var Vs)" by(auto simp add: fresh_var_fresh)
with x show ?thesis by(simp)
qed
qed
with IH1[OF fv1] IH2[OF fv2'] fv2' show ?case by(simp add: fv_compE1)
next
case (InSynchronized Vs V a exp)
note IH = ‹fv exp ⊆ set (Vs @ [fresh_var Vs]) ⟹ syncvars (compE1 (Vs @ [fresh_var Vs]) exp)›
from ‹fv (insync⇘V⇙ (a) exp) ⊆ set Vs› have fv: "fv exp ⊆ set Vs"
and fv': "fv exp ⊆ set (Vs @ [fresh_var Vs])" by auto
have "length Vs ∉ index (Vs @ [fresh_var Vs]) ` fv exp"
proof
assume "length Vs ∈ index (Vs @ [fresh_var Vs]) ` fv exp"
thus False
proof(rule imageE)
fix x
assume x: "length Vs = index (Vs @ [fresh_var Vs]) x"
and x': "x ∈ fv exp"
from x' fv have "x ∈ set Vs" "x ≠ (fresh_var Vs)" by(auto simp add: fresh_var_fresh)
with x show ?thesis by(simp)
qed
qed
with IH[OF fv'] fv' show ?case by(simp add: fv_compE1)
next
case (TryCatch Vs exp1 C V exp2)
note IH1 = ‹fv exp1 ⊆ set Vs ⟹ syncvars (compE1 Vs exp1)›
note IH2 = ‹fv exp2 ⊆ set (Vs @ [V]) ⟹ syncvars (compE1 (Vs @ [V]) exp2)›
from ‹fv (try exp1 catch(C V) exp2) ⊆ set Vs› have fv1: "fv exp1 ⊆ set Vs"
and fv2: "fv exp2 ⊆ set (Vs @ [V])" by auto
from IH1[OF fv1] IH2[OF fv2] show ?case by auto
qed auto

lemma (in heap_base) synthesized_call_compP [simp]:
"synthesized_call (compP f P) h aMvs = synthesized_call P h aMvs"

where
"fin1 (Val v) = Val v"
| "fin1 (throw e) = throw (fin1 e)"

lemma comp_final: "final e ⟹ compE1 Vs e = fin1 e"
by(erule finalE, simp_all)

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
shows [simp]: "max_vars (compE1 Vs e) = max_vars e"