header {* \chapter{Compilation}\label{cha:comp}
\isaheader{An Intermediate Language} *}
theory J1 imports "../J/BigStep" begin
type_synonym expr⇣1 = "nat exp"
type_synonym J⇣1_prog = "expr⇣1 prog"
type_synonym state⇣1 = "heap × (val list)"
primrec
max_vars :: "'a exp => nat"
and max_varss :: "'a exp list => nat"
where
"max_vars(new C) = 0"
| "max_vars(Cast C e) = max_vars e"
| "max_vars(Val v) = 0"
| "max_vars(e⇣1 «bop» e⇣2) = max (max_vars e⇣1) (max_vars e⇣2)"
| "max_vars(Var V) = 0"
| "max_vars(V:=e) = max_vars e"
| "max_vars(e•F{D}) = max_vars e"
| "max_vars(FAss e⇣1 F D e⇣2) = max (max_vars e⇣1) (max_vars e⇣2)"
| "max_vars(e•M(es)) = max (max_vars e) (max_varss es)"
| "max_vars({V:T; e}) = max_vars e + 1"
| "max_vars(e⇣1;;e⇣2) = max (max_vars e⇣1) (max_vars e⇣2)"
| "max_vars(if (e) e⇣1 else e⇣2) =
max (max_vars e) (max (max_vars e⇣1) (max_vars e⇣2))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e⇣1 catch(C V) e⇣2) = max (max_vars e⇣1) (max_vars e⇣2 + 1)"
| "max_varss [] = 0"
| "max_varss (e#es) = max (max_vars e) (max_varss es)"
inductive
eval⇣1 :: "J⇣1_prog => expr⇣1 => state⇣1 => expr⇣1 => state⇣1 => bool"
("_ \<turnstile>⇩1 ((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
and evals⇣1 :: "J⇣1_prog => expr⇣1 list => state⇣1 => expr⇣1 list => state⇣1 => bool"
("_ \<turnstile>⇩1 ((1⟨_,/_⟩) [=>]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
for P :: J⇣1_prog
where
New⇣1:
"[| new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>(C,init_fields FDTs)) |]
==> P \<turnstile>⇩1 ⟨new C,(h,l)⟩ => ⟨addr a,(h',l)⟩"
| NewFail⇣1:
"new_Addr h = None ==>
P \<turnstile>⇩1 ⟨new C, (h,l)⟩ => ⟨THROW OutOfMemory,(h,l)⟩"
| Cast⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨addr a,(h,l)⟩; h a = Some(D,fs); P \<turnstile> D \<preceq>⇧* C |]
==> P \<turnstile>⇩1 ⟨Cast C e,s⇣0⟩ => ⟨addr a,(h,l)⟩"
| CastNull⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨null,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨Cast C e,s⇣0⟩ => ⟨null,s⇣1⟩"
| CastFail⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P \<turnstile> D \<preceq>⇧* C |]
==> P \<turnstile>⇩1 ⟨Cast C e,s⇣0⟩ => ⟨THROW ClassCast,(h,l)⟩"
| CastThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨Cast C e,s⇣0⟩ => ⟨throw e',s⇣1⟩"
| Val⇣1:
"P \<turnstile>⇩1 ⟨Val v,s⟩ => ⟨Val v,s⟩"
| BinOp⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨Val v⇣1,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣2,s⇣1⟩ => ⟨Val v⇣2,s⇣2⟩; binop(bop,v⇣1,v⇣2) = Some v |]
==> P \<turnstile>⇩1 ⟨e⇣1 «bop» e⇣2,s⇣0⟩ => ⟨Val v,s⇣2⟩"
| BinOpThrow⇣1⇣1:
"P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨throw e,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨e⇣1 «bop» e⇣2, s⇣0⟩ => ⟨throw e,s⇣1⟩"
| BinOpThrow⇣2⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨Val v⇣1,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣2,s⇣1⟩ => ⟨throw e,s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨e⇣1 «bop» e⇣2,s⇣0⟩ => ⟨throw e,s⇣2⟩"
| Var⇣1:
"[| ls!i = v; i < size ls |] ==>
P \<turnstile>⇩1 ⟨Var i,(h,ls)⟩ => ⟨Val v,(h,ls)⟩"
| LAss⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨Val v,(h,ls)⟩; i < size ls; ls' = ls[i := v] |]
==> P \<turnstile>⇩1 ⟨i:= e,s⇣0⟩ => ⟨unit,(h,ls')⟩"
| LAssThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨i:= e,s⇣0⟩ => ⟨throw e',s⇣1⟩"
| FAcc⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨addr a,(h,ls)⟩; h a = Some(C,fs); fs(F,D) = Some v |]
==> P \<turnstile>⇩1 ⟨e•F{D},s⇣0⟩ => ⟨Val v,(h,ls)⟩"
| FAccNull⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨null,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨e•F{D},s⇣0⟩ => ⟨THROW NullPointer,s⇣1⟩"
| FAccThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨e•F{D},s⇣0⟩ => ⟨throw e',s⇣1⟩"
| FAss⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨addr a,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣2,s⇣1⟩ => ⟨Val v,(h⇣2,l⇣2)⟩;
h⇣2 a = Some(C,fs); fs' = fs((F,D)\<mapsto>v); h⇣2' = h⇣2(a\<mapsto>(C,fs')) |]
==> P \<turnstile>⇩1 ⟨e⇣1•F{D}:= e⇣2,s⇣0⟩ => ⟨unit,(h⇣2',l⇣2)⟩"
| FAssNull⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨null,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣2,s⇣1⟩ => ⟨Val v,s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨e⇣1•F{D}:= e⇣2,s⇣0⟩ => ⟨THROW NullPointer,s⇣2⟩"
| FAssThrow⇣1⇣1:
"P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨e⇣1•F{D}:= e⇣2,s⇣0⟩ => ⟨throw e',s⇣1⟩"
| FAssThrow⇣2⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨Val v,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣2,s⇣1⟩ => ⟨throw e',s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨e⇣1•F{D}:= e⇣2,s⇣0⟩ => ⟨throw e',s⇣2⟩"
| CallObjThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨e•M(es),s⇣0⟩ => ⟨throw e',s⇣1⟩"
| CallNull⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨null,s⇣1⟩; P \<turnstile>⇩1 ⟨es,s⇣1⟩ [=>] ⟨map Val vs,s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨e•M(es),s⇣0⟩ => ⟨THROW NullPointer,s⇣2⟩"
| Call⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨addr a,s⇣1⟩; P \<turnstile>⇩1 ⟨es,s⇣1⟩ [=>] ⟨map Val vs,(h⇣2,ls⇣2)⟩;
h⇣2 a = Some(C,fs); P \<turnstile> C sees M:Ts->T = body in D;
size vs = size Ts; ls⇣2' = (Addr a) # vs @ replicate (max_vars body) undefined;
P \<turnstile>⇩1 ⟨body,(h⇣2,ls⇣2')⟩ => ⟨e',(h⇣3,ls⇣3)⟩ |]
==> P \<turnstile>⇩1 ⟨e•M(es),s⇣0⟩ => ⟨e',(h⇣3,ls⇣2)⟩"
| CallParamsThrow⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨Val v,s⇣1⟩; P \<turnstile>⇩1 ⟨es,s⇣1⟩ [=>] ⟨es',s⇣2⟩;
es' = map Val vs @ throw ex # es⇣2 |]
==> P \<turnstile>⇩1 ⟨e•M(es),s⇣0⟩ => ⟨throw ex,s⇣2⟩"
| Block⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨e',s⇣1⟩ ==> P \<turnstile>⇩1 ⟨Block i T e,s⇣0⟩ => ⟨e',s⇣1⟩"
| Seq⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣0,s⇣0⟩ => ⟨Val v,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣1,s⇣1⟩ => ⟨e⇣2,s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨e⇣0;;e⇣1,s⇣0⟩ => ⟨e⇣2,s⇣2⟩"
| SeqThrow⇣1:
"P \<turnstile>⇩1 ⟨e⇣0,s⇣0⟩ => ⟨throw e,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨e⇣0;;e⇣1,s⇣0⟩ => ⟨throw e,s⇣1⟩"
| CondT⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨true,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣1,s⇣1⟩ => ⟨e',s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨if (e) e⇣1 else e⇣2,s⇣0⟩ => ⟨e',s⇣2⟩"
| CondF⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨false,s⇣1⟩; P \<turnstile>⇩1 ⟨e⇣2,s⇣1⟩ => ⟨e',s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨if (e) e⇣1 else e⇣2,s⇣0⟩ => ⟨e',s⇣2⟩"
| CondThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨if (e) e⇣1 else e⇣2, s⇣0⟩ => ⟨throw e',s⇣1⟩"
| WhileF⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨false,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨while (e) c,s⇣0⟩ => ⟨unit,s⇣1⟩"
| WhileT⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨true,s⇣1⟩; P \<turnstile>⇩1 ⟨c,s⇣1⟩ => ⟨Val v⇣1,s⇣2⟩;
P \<turnstile>⇩1 ⟨while (e) c,s⇣2⟩ => ⟨e⇣3,s⇣3⟩ |]
==> P \<turnstile>⇩1 ⟨while (e) c,s⇣0⟩ => ⟨e⇣3,s⇣3⟩"
| WhileCondThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨while (e) c,s⇣0⟩ => ⟨throw e',s⇣1⟩"
| WhileBodyThrow⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨true,s⇣1⟩; P \<turnstile>⇩1 ⟨c,s⇣1⟩ => ⟨throw e',s⇣2⟩|]
==> P \<turnstile>⇩1 ⟨while (e) c,s⇣0⟩ => ⟨throw e',s⇣2⟩"
| Throw⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨addr a,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨throw e,s⇣0⟩ => ⟨Throw a,s⇣1⟩"
| ThrowNull⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨null,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨throw e,s⇣0⟩ => ⟨THROW NullPointer,s⇣1⟩"
| ThrowThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨throw e,s⇣0⟩ => ⟨throw e',s⇣1⟩"
| Try⇣1:
"P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨Val v⇣1,s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨try e⇣1 catch(C i) e⇣2,s⇣0⟩ => ⟨Val v⇣1,s⇣1⟩"
| TryCatch⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨Throw a,(h⇣1,ls⇣1)⟩;
h⇣1 a = Some(D,fs); P \<turnstile> D \<preceq>⇧* C; i < length ls⇣1;
P \<turnstile>⇩1 ⟨e⇣2,(h⇣1,ls⇣1[i:=Addr a])⟩ => ⟨e⇣2',(h⇣2,ls⇣2)⟩ |]
==> P \<turnstile>⇩1 ⟨try e⇣1 catch(C i) e⇣2,s⇣0⟩ => ⟨e⇣2',(h⇣2,ls⇣2)⟩"
| TryThrow⇣1:
"[| P \<turnstile>⇩1 ⟨e⇣1,s⇣0⟩ => ⟨Throw a,(h⇣1,ls⇣1)⟩; h⇣1 a = Some(D,fs); ¬ P \<turnstile> D \<preceq>⇧* C |]
==> P \<turnstile>⇩1 ⟨try e⇣1 catch(C i) e⇣2,s⇣0⟩ => ⟨Throw a,(h⇣1,ls⇣1)⟩"
| Nil⇣1:
"P \<turnstile>⇩1 ⟨[],s⟩ [=>] ⟨[],s⟩"
| Cons⇣1:
"[| P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨Val v,s⇣1⟩; P \<turnstile>⇩1 ⟨es,s⇣1⟩ [=>] ⟨es',s⇣2⟩ |]
==> P \<turnstile>⇩1 ⟨e#es,s⇣0⟩ [=>] ⟨Val v # es',s⇣2⟩"
| ConsThrow⇣1:
"P \<turnstile>⇩1 ⟨e,s⇣0⟩ => ⟨throw e',s⇣1⟩ ==>
P \<turnstile>⇩1 ⟨e#es,s⇣0⟩ [=>] ⟨throw e' # es, s⇣1⟩"
lemmas eval⇣1_evals⇣1_induct = eval⇣1_evals⇣1.induct [split_format (complete)]
and eval⇣1_evals⇣1_inducts = eval⇣1_evals⇣1.inducts [split_format (complete)]
lemma eval⇣1_preserves_len:
"P \<turnstile>⇩1 ⟨e⇣0,(h⇣0,ls⇣0)⟩ => ⟨e⇣1,(h⇣1,ls⇣1)⟩ ==> length ls⇣0 = length ls⇣1"
and evals⇣1_preserves_len:
"P \<turnstile>⇩1 ⟨es⇣0,(h⇣0,ls⇣0)⟩ [=>] ⟨es⇣1,(h⇣1,ls⇣1)⟩ ==> length ls⇣0 = length ls⇣1"
by (induct rule:eval⇣1_evals⇣1_inducts, simp_all)
lemma evals⇣1_preserves_elen:
"!!es' s s'. P \<turnstile>⇩1 ⟨es,s⟩ [=>] ⟨es',s'⟩ ==> length es = length es'"
apply(induct es type:list)
apply (auto elim:evals⇣1.cases)
done
lemma eval⇣1_final: "P \<turnstile>⇩1 ⟨e,s⟩ => ⟨e',s'⟩ ==> final e'"
and evals⇣1_final: "P \<turnstile>⇩1 ⟨es,s⟩ [=>] ⟨es',s'⟩ ==> finals es'"
by(induct rule:eval⇣1_evals⇣1.inducts, simp_all)
end