# Theory Compiler1

Author:     Andreas Lochbihler, Tobias Nipkow

Based on Jinja/Compiler/Compiler1
*)

section ‹Compilation Stage 1›

theory Compiler1 imports
PCompiler
J1State
ListIndex
begin

definition fresh_var ::
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.›

where
"compE1 Vs (new C) = new C"
| "compE1 Vs (newA Te) = newA TcompE1 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 (ai) = (compE1 Vs a)compE1 Vs i"
| "compE1 Vs (ai:=e) = (compE1 Vs a)compE1 Vs i:=compE1 Vs e"
| "compE1 Vs (a∙length) = compE1 Vs a∙length"
| "compE1 Vs (eF{D}) = compE1 Vs eF{D}"
| "compE1 Vs (eF{D}:=e') = compE1 Vs eF{D}:=compE1 Vs e'"
| "compE1 Vs (e∙compareAndSwap(DF, e', e'')) = compE1 Vs e∙compareAndSwap(DF, compE1 Vs e', compE1 Vs e'')"
| "compE1 Vs (eM(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 = objM(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]:
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)"
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"