# Theory FJAux

```(*  Title:       A theory of Featherweight Java in Isabelle/HOL
Author:      Nate Foster <jnfoster at cis.upenn.edu>,
Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>, 2006
Maintainer:  Nate Foster <jnfoster at cis.upenn.edu>,
Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>

Auxiliary lemmas
*)

section ‹{\tt FJAux}: Auxiliary Lemmas›

theory FJAux imports FJDefs
begin

subsection‹Non-FJ Lemmas›

subsubsection‹Lists›
lemma mem_ith:
assumes "ei ∈ set es"
shows "∃ el er. es = el@ei#er"
using assms
proof(induct es)
case Nil thus ?case by auto
next
case (Cons esh est)
{ assume "esh = ei"
with Cons have ?case by blast
} moreover {
assume "esh ≠ ei"
with Cons have "ei ∈ set est" by auto
with Cons obtain el er where "esh # est = (esh#el) @ (ei#er)" by auto
hence ?case by blast }
ultimately show ?case by blast
qed

lemma ith_mem: "⋀i. ⟦ i < length es ⟧ ⟹ es!i ∈ set es"
proof(induct es)
case Nil thus ?case by auto
next
case (Cons h t) thus ?case by(cases "i", auto)
qed

subsubsection‹Maps›

lemma map_shuffle:
assumes "length xs = length ys"
shows "[xs[↦]ys,x↦y] = [(xs@[x])[↦](ys@[y])]"
using assms
by (induct "xs" "ys" rule:list_induct2) (auto simp add:map_upds_append1)

lemma map_upds_index:
assumes "length xs = length As"
and "[xs[↦]As]x = Some Ai"
shows "∃i.(As!i = Ai)
∧ (i < length As)
∧ (∀(Bs::'c list).((length Bs = length As)
⟶ ([xs[↦]Bs] x = Some (Bs !i))))"
(is "∃i. ?P i xs As"
is "∃i.(?P1 i As) ∧ (?P2 i As) ∧ (∀Bs::('c list).(?P3 i xs As Bs))")
using assms
proof(induct "xs" "As" rule:list_induct2)
assume "[[][↦][]] x = Some Ai"
moreover have "¬[[][↦][]] x = Some Ai" by auto
ultimately show "∃i. ?P i [] []" by contradiction
next
fix xa xs y ys
assume length_xs_ys: "length xs = length ys"
and IH: "[xs [↦] ys] x = Some Ai ⟹ ∃i. ?P i xs ys"
and map_eq_Some: "[xa # xs [↦] y # ys] x = Some Ai"
then have map_decomp: "[xa#xs [↦] y#ys] = [xa↦y] ++ [xs[↦]ys]" by fastforce
show "∃i. ?P i (xa#xs) (y # ys)"
proof(cases "[xs[↦]ys]x")
case(Some Ai')
hence "([xa ↦y] ++ [xs[↦]ys]) x = Some Ai'" by(rule map_add_find_right)
hence P: "[xs[↦]ys] x = Some Ai" using map_eq_Some Some by simp
from IH[OF P] obtain i where
R1: "ys ! i = Ai"
and R2: "i < length ys"
and pre_r3: "∀(Bs::'c list). ?P3 i xs ys Bs" by fastforce
{ fix Bs::"'c list"
assume length_Bs: "length Bs = length (y#ys)"
then obtain n where "length (y#ys) = Suc n" by auto
with length_Bs obtain b bs where Bs_def: "Bs = b#bs" by (auto simp add:length_Suc_conv)
with length_Bs have "length ys = length bs" by simp
with pre_r3 have "([xa↦b] ++ [xs[↦]bs]) x = Some (bs!i)" by(auto simp only:map_add_find_right)
with pre_r3 Bs_def length_Bs have "?P3 (i+1) (xa#xs) (y#ys) Bs" by simp }
with R1 R2 have "?P (i+1) (xa#xs) (y#ys)" by auto
thus ?thesis ..
next
case None
with map_decomp map_eq_Some have "[xa↦y] x = Some Ai" by (auto simp only:map_add_SomeD)
hence ai_def: "y = Ai" and x_eq_xa:"x=xa" by (auto simp only:map_upd_Some_unfold)
{ fix Bs::"'c list"
assume length_Bs: "length Bs = length (y#ys)"
then obtain n where "length (y#ys) = Suc n" by auto
with length_Bs obtain b bs where Bs_def: "Bs = b#bs" by (auto simp add:length_Suc_conv)
with length_Bs have "length ys = length bs" by simp
hence "dom([xs[↦]ys]) = dom([xs[↦]bs])" by auto
with None have "[xs[↦]bs] x = None" by (auto simp only:domIff)
moreover from x_eq_xa have sing_map: "[xa↦b] x = Some b" by (auto simp only:map_upd_Some_unfold)
ultimately have "([xa↦b] ++ [xs[↦]bs]) x = Some b" by (auto simp only:map_add_Some_iff)
with Bs_def have "?P3 0 (xa#xs) (y#ys) Bs" by simp }
with ai_def have "?P 0 (xa#xs) (y#ys)" by auto
thus ?thesis ..
qed
qed

subsection‹FJ Lemmas›

subsubsection‹Substitution›

lemma subst_list1_eq_map_substs :
"∀σ. subst_list1 σ l = map (substs σ) l"
by (induct l, simp_all)

lemma subst_list2_eq_map_substs :
"∀σ. subst_list2 σ l = map (substs σ) l"
by (induct l, simp_all)

subsubsection‹Lookup›

lemma lookup_functional:
assumes "lookup l f = o1"
and "lookup l f = o2"
shows "o1 = o2"
using assms by (induct l) auto

lemma lookup_true:
"lookup l f = Some r ⟹ f r"
proof(induct l)
case Nil thus ?case by simp
next
case(Cons h t) thus ?case by(cases "f h") (auto simp add:lookup.simps)
qed

lemma lookup_hd:
"⟦ length l > 0; f (l!0) ⟧ ⟹ lookup l f = Some (l!0)"
by (induct l) auto

lemma lookup_split: "lookup l f = None ∨ (∃h. lookup l f = Some h)"
by (induct l) simp_all

lemma lookup_index:
assumes "lookup l1 f = Some e"
shows " ⋀l2. ∃i < (length l1). e = l1!i ∧ ((length l1 = length l2) ⟶ lookup2 l1 l2 f = Some (l2!i))"
using assms
proof(induct l1)
case Nil thus ?case by auto
next
case (Cons h1 t1)
{ assume asm:"f h1"
hence "0<length (h1 # t1) ∧ e = (h1 # t1) ! 0"
using Cons by (auto simp add:lookup.simps)
moreover {
assume "length (h1 # t1) = length l2"
hence "length l2 = Suc (length t1)" by auto
then obtain h2 t2 where l2_def:"l2 = h2#t2" by (auto simp add: length_Suc_conv)
hence "lookup2 (h1 # t1) l2 f = Some (l2 ! 0)" using asm by(auto simp add: lookup2.simps)
}
ultimately have ?case by auto
} moreover {
assume asm:"¬ (f h1)"
hence "lookup t1 f = Some e"
using Cons by (auto simp add:lookup.simps)
then obtain i where
"i<length t1"
and "e = t1 ! i"
and  ih:"(length t1 = length (tl l2) ⟶ lookup2 t1 (tl l2) f = Some ((tl l2) ! i))"
using Cons by blast
hence "Suc i < length (h1#t1) ∧ e = (h1#t1)!(Suc i)" using Cons by auto
moreover {
assume "length (h1 # t1) = length l2"
hence lens:"length l2 = Suc (length t1)" by auto
then obtain h2 t2 where l2_def:"l2 = h2#t2" by (auto simp add: length_Suc_conv)
hence "lookup2 t1 t2 f = Some (t2 ! i)" using ih l2_def lens by auto
hence "lookup2 (h1 # t1) l2 f = Some (l2!(Suc i))"
using asm l2_def by(auto simp add: lookup2.simps)
}
ultimately have ?case by auto
}
ultimately show ?case by auto
qed

lemma lookup2_index:
"⋀l2. ⟦ lookup2 l1 l2 f = Some e;
length l1 = length l2 ⟧ ⟹ ∃i < (length l2). e = (l2!i) ∧ lookup l1 f = Some (l1!i)"
proof(induct l1)
case Nil thus ?case by auto
next
case (Cons h1 t1)
hence "length l2 = Suc (length t1)" by auto
then obtain h2 t2 where l2_def:"l2 = h2#t2" by (auto simp add: length_Suc_conv)
{ assume asm:"f h1"
hence "e = h2" using Cons l2_def by (auto simp add:lookup2.simps)
hence "0<length (h2#t2) ∧ e = (h2#t2) ! 0 ∧ lookup (h1 # t1) f = Some ((h1 # t1) ! 0)"
using asm by (auto simp add:lookup.simps)
hence ?case using l2_def by auto
} moreover {
assume asm:"¬ (f h1)"
hence "∃i<length t2. e = t2 ! i ∧ lookup t1 f = Some (t1 ! i)" using Cons l2_def by auto
then obtain i where "i<length t2 ∧  e = t2 ! i ∧ lookup t1 f = Some (t1 ! i)" by auto
hence "(Suc i) < length(h2#t2) ∧ e = ((h2#t2) ! (Suc i)) ∧ lookup (h1#t1) f = Some ((h1#t1) ! (Suc i))"
using asm by (force simp add: lookup.simps)
hence ?case using l2_def by auto
}
ultimately show ?case by auto
qed

lemma lookup_append:
assumes "lookup l f = Some r"
shows "lookup (l@l') f = Some r"
using assms by(induct l) auto

lemma method_typings_lookup:
assumes lookup_eq_Some: "lookup M f = Some mDef"
and M_ok: "CT ⊢+ M OK IN C"
shows "CT ⊢ mDef OK IN C"
using lookup_eq_Some M_ok
proof(induct M)
case Nil thus ?case by fastforce
next
case (Cons h t) thus ?case by(cases "f h", auto elim:method_typings.cases simp add:lookup.simps)
qed

subsubsection‹Functional›

text ‹These lemmas prove that several relations are actually functions›

lemma mtype_functional:
assumes "mtype(CT,m,C) = Cs → C0"
and     "mtype(CT,m,C) = Ds → D0"
shows "Ds=Cs ∧ D0=C0"
using assms by induct (auto elim:mtype.cases)

lemma mbody_functional:
assumes mb1: "mbody(CT,m,C) = xs . e0"
and     mb2: "mbody(CT,m,C) = ys . d0"
shows "xs = ys ∧ e0 = d0"
using assms by induct (auto elim:mbody.cases)

lemma fields_functional:
assumes "fields(CT,C) = Cf"
and "CT OK"
shows "⋀Cf'. ⟦ fields(CT,C) = Cf'⟧ ⟹ Cf = Cf'"
using assms
proof induct
case (f_obj CT)
hence "CT(Object) = None" by (auto elim: ct_typing.cases)
thus ?case using f_obj by (auto elim: fields.cases)
next
case (f_class CT C CDef D Cf Dg DgCf DgCf')
hence f_class_inv:
"(CT C = Some CDef) ∧ (cSuper CDef = D) ∧ (cFields CDef = Cf)"
and "CT OK" by fastforce+
hence c_not_obj:"C ≠ Object" by (force elim:ct_typing.cases)
from f_class have flds:"fields(CT,C) = DgCf'" by fastforce
then obtain Dg' where
"fields(CT,D) = Dg'"
and "DgCf' = Dg' @ Cf"
using f_class_inv c_not_obj by (auto elim:fields.cases)
hence "Dg' = Dg" using f_class by auto
thus ?case using ‹DgCf = Dg @ Cf› and ‹DgCf' = Dg' @ Cf› by force
qed

subsubsection‹Subtyping and Typing›

lemma typings_lengths: assumes "CT;Γ ⊢+ es:Cs" shows "length es = length Cs"
using assms by(induct "es" "Cs") (auto elim:typings.cases)

lemma typings_index:
assumes "CT;Γ ⊢+ es:Cs"
shows "⋀i. ⟦ i < length es ⟧ ⟹ CT;Γ ⊢ (es!i) : (Cs!i)"
proof -
have "length es = length Cs" using assms by (auto simp: typings_lengths)
thus "⋀i. ⟦ i < length es ⟧ ⟹ CT;Γ ⊢ (es!i) : (Cs!i)"
using assms
proof(induct es Cs rule:list_induct2)
case Nil thus ?case by auto
next
case (Cons esh est hCs tCs i)
thus ?case by(cases i) (auto elim:typings.cases)
qed
qed

lemma subtypings_index:
assumes "CT ⊢+ Cs <: Ds"
shows "⋀i. ⟦ i < length Cs ⟧ ⟹ CT ⊢ (Cs!i) <: (Ds!i)"
using assms
proof induct
case ss_nil thus ?case by auto
next
case (ss_cons hCs CT tCs hDs tDs i)
thus ?case by(cases "i", auto)
qed

lemma subtyping_append:
assumes "CT ⊢+ Cs <: Ds"
and "CT ⊢ C <: D"
shows "CT ⊢+ (Cs@[C]) <: (Ds@[D])"
using assms
by (induct rule:subtypings.induct) (auto simp add:subtypings.intros elim:subtypings.cases)

lemma typings_append:
assumes "CT;Γ ⊢+ es : Cs"
and "CT;Γ ⊢ e : C"
shows "CT;Γ ⊢+ (es@[e]) : (Cs@[C])"
proof -
have "length es = length Cs" using assms by(simp_all add:typings_lengths)
thus "CT;Γ ⊢+ (es@[e]) : (Cs@[C])" using assms
proof(induct "es" "Cs" rule:list_induct2)
have "CT;Γ ⊢+ []:[]" by(simp add:typings_typing.ts_nil)
moreover from assms have "CT;Γ ⊢ e : C" by simp
ultimately show "CT;Γ ⊢+ ([]@[e]) : ([]@[C])" by (auto simp add:typings_typing.ts_cons)
next
fix x xs y ys
assume "length xs = length ys"
and IH: "⟦CT;Γ ⊢+ xs : ys; CT;Γ ⊢ e : C⟧ ⟹ CT;Γ ⊢+ (xs @ [e]) : (ys @ [C])"
and x_xs_typs: "CT;Γ ⊢+ (x # xs) : (y # ys)"
and e_typ: "CT;Γ ⊢ e : C"
from x_xs_typs have x_typ: "CT;Γ ⊢ x : y" and "CT;Γ ⊢+ xs : ys" by(auto elim:typings.cases)
with IH e_typ have "CT;Γ ⊢+ (xs@[e]) : (ys@[C])" by simp
with x_typ have "CT;Γ ⊢+ ((x#xs)@[e]) : ((y#ys)@[C])" by (auto simp add:typings_typing.ts_cons)
thus "CT;Γ ⊢+ ((x # xs) @ [e]) : ((y # ys) @ [C])" by(auto simp add:typings_typing.ts_cons)
qed
qed

lemma ith_typing: "⋀Cs. ⟦ CT;Γ ⊢+ (es@(h#t)) : Cs ⟧ ⟹ CT;Γ ⊢ h : (Cs!(length es))"
proof(induct "es", auto elim:typings.cases)
qed

lemma ith_subtyping: "⋀Ds. ⟦ CT ⊢+ (Cs@(h#t)) <: Ds ⟧ ⟹ CT ⊢ h <: (Ds!(length Cs))"
proof(induct "Cs", auto elim:subtypings.cases)
qed

lemma subtypings_refl: "CT ⊢+ Cs <: Cs"
by(induct "Cs", auto simp add: subtyping.s_refl subtypings.intros)

lemma subtypings_trans: "⋀Ds Es. ⟦ CT ⊢+ Cs <: Ds;  CT ⊢+ Ds <: Es ⟧ ⟹ CT ⊢+ Cs <: Es"
proof(induct "Cs")
case Nil thus ?case
next
case (Cons hCs tCs)
then obtain hDs tDs
where h1:"CT ⊢ hCs <: hDs" and t1:"CT ⊢+ tCs <: tDs" and "Ds = hDs#tDs"
by (auto elim:subtypings.cases)
then obtain hEs tEs
where h2:"CT ⊢ hDs <: hEs" and t2:"CT ⊢+ tDs <: tEs" and "Es = hEs#tEs"
using Cons by (auto elim:subtypings.cases)
moreover from subtyping.s_trans[OF h1 h2] have "CT ⊢ hCs <: hEs" by fastforce
moreover with t1 t2 have "CT ⊢+ tCs <: tEs" using Cons by simp_all
ultimately show ?case by (auto simp add:subtypings.intros)
qed

lemma ith_typing_sub:
"⋀Cs. ⟦ CT;Γ ⊢+ (es@(h#t)) : Cs;
CT;Γ ⊢ h' : Ci';
CT ⊢ Ci' <: (Cs!(length es)) ⟧
⟹ ∃Cs'. (CT;Γ ⊢+ (es@(h'#t)) : Cs' ∧ CT ⊢+ Cs' <: Cs)"
proof(induct es)
case Nil
then obtain hCs tCs
where ts: "CT;Γ ⊢+ t : tCs"
and Cs_def: "Cs = hCs # tCs" by(auto elim:typings.cases)
from Cs_def Nil have "CT ⊢ Ci' <: hCs" by auto
with Cs_def have "CT ⊢+ (Ci'#tCs) <: Cs" by(auto simp add:subtypings.ss_cons subtypings_refl)
moreover from ts Nil have "CT;Γ ⊢+ (h'#t) : (Ci'#tCs)" by(auto simp add:typings_typing.ts_cons)
ultimately show ?case by auto
next
case (Cons eh et)
then obtain hCs tCs
where "CT;Γ ⊢ eh : hCs"
and "CT;Γ ⊢+ (et@(h#t)) : tCs"
and Cs_def: "Cs = hCs # tCs"
by(auto elim:typings.cases)
moreover with Cons obtain tCs'
where "CT;Γ ⊢+ (et@(h'#t)) : tCs'"
and "CT ⊢+ tCs' <: tCs"
by auto
ultimately have
"CT;Γ ⊢+ (eh#(et@(h'#t))) : (hCs#tCs')"
and "CT ⊢+ (hCs#tCs') <: Cs"
thus ?case by auto
qed

lemma mem_typings:
"⋀Cs. ⟦ CT;Γ ⊢+ es:Cs; ei ∈ set es⟧ ⟹ ∃Ci. CT;Γ ⊢ ei:Ci"
proof(induct es)
case Nil thus ?case by auto
next
case (Cons eh et) thus ?case
by(cases "ei=eh", auto elim:typings.cases)
qed

lemma typings_proj:
assumes "CT;Γ ⊢+ ds : As"
and "CT ⊢+ As <: Bs"
and "length ds = length As"
and "length ds = length Bs"
and "i < length ds"
shows "CT;Γ ⊢ ds!i : As!i" and "CT ⊢ As!i <: Bs!i"
using assms by (auto simp add:typings_index subtypings_index)

lemma subtypings_length:
"CT ⊢+ As <: Bs ⟹ length As = length Bs"
by(induct rule:subtypings.induct) simp_all

lemma not_subtypes_aux:
assumes "CT ⊢ C <: Da"
and "C ≠ Da"
and "CT C = Some CDef"
and "cSuper CDef = D"
shows "CT ⊢ D <: Da"
using assms
by (induct rule:subtyping.induct) (auto intro:subtyping.intros)

lemma not_subtypes:
assumes "CT ⊢ A <: C"
shows "⋀D. ⟦ CT ⊢ D ¬<: C;  CT ⊢ C ¬<: D⟧ ⟹ CT ⊢ A ¬<: D"
using assms
proof(induct rule:subtyping.induct)
case s_refl thus ?case by auto
next
case (s_trans CT C D E Da)
have da_nsub_d:"CT ⊢ Da ¬<: D"
proof(rule ccontr)
assume "¬ CT ⊢ Da ¬<: D"
hence da_sub_d:"CT ⊢ Da <: D" by auto
have d_sub_e:"CT ⊢ D <: E" using s_trans by fastforce
thus "False" using s_trans by (force simp add:subtyping.s_trans[OF da_sub_d d_sub_e])
qed
have d_nsub_da:"CT ⊢ D ¬<: Da" using s_trans by auto
from da_nsub_d d_nsub_da s_trans show "CT ⊢ C ¬<: Da" by auto
next
case (s_super CT C CDef D Da)
have "C ≠ Da" proof(rule ccontr)
assume "¬ C ≠ Da"
hence "C = Da" by auto
hence "CT ⊢ Da <: D" using s_super by(auto simp add: subtyping.s_super)
thus "False" using s_super by auto
qed
thus ?case using s_super by (auto simp add: not_subtypes_aux)
qed

subsubsection‹Sub-Expressions›

lemma isubexpr_typing:
assumes "e1 ∈ isubexprs(e0)"
shows "⋀C. ⟦ CT;Map.empty ⊢ e0 : C ⟧ ⟹ ∃D. CT;Map.empty ⊢ e1 : D"
using assms
by (induct rule:isubexprs.induct) (auto elim:typing.cases simp add:mem_typings)

lemma subexpr_typing:
assumes "e1 ∈ subexprs(e0)"
shows "⋀C. ⟦ CT;Map.empty ⊢ e0 : C ⟧ ⟹ ∃D. CT;Map.empty ⊢ e1 : D"
using assms
by (induct rule:rtrancl.induct) (auto, force simp add:isubexpr_typing)

lemma isubexpr_reduct:
assumes "d1 ∈ isubexprs(e1)"
shows "⋀d2. ⟦ CT ⊢ d1 → d2 ⟧ ⟹ ∃e2. CT ⊢ e1 → e2"
using assms mem_ith
by induct
(auto elim:isubexprs.cases intro:reduction.intros,
force intro:reduction.intros,
force intro:reduction.intros)

lemma subexpr_reduct:
assumes "d1 ∈ subexprs(e1)"
shows "⋀d2. ⟦ CT ⊢ d1 → d2 ⟧ ⟹ ∃e2. CT ⊢ e1 → e2"
using assms
by (induct rule:rtrancl.induct) (auto, force simp add: isubexpr_reduct)

end
```