header {* {\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[\<mapsto>]ys,x\<mapsto>y] = [(xs@[x])[\<mapsto>](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[\<mapsto>]As]x = Some Ai"
shows "∃i.(As!i = Ai)
∧ (i < length As)
∧ (∀(Bs::'c list).((length Bs = length As)
--> ([xs[\<mapsto>]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 "[[][\<mapsto>][]] x = Some Ai"
moreover have "¬[[][\<mapsto>][]] 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 [\<mapsto>] ys] x = Some Ai ==> ∃i. ?P i xs ys"
and map_eq_Some: "[xa # xs [\<mapsto>] y # ys] x = Some Ai"
from prems have map_decomp: "[xa#xs [\<mapsto>] y#ys] = [xa\<mapsto>y] ++ [xs[\<mapsto>]ys]" by fastsimp
from length_xs_ys IH map_eq_Some show "∃i. ?P i (xa#xs) (y # ys)"
proof(cases "[xs[\<mapsto>]ys]x")
case(Some Ai')
hence "([xa \<mapsto>y] ++ [xs[\<mapsto>]ys]) x = Some Ai'" by(rule map_add_find_right)
hence P: "[xs[\<mapsto>]ys] x = Some Ai" using prems 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 fastsimp
{ 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\<mapsto>b] ++ [xs[\<mapsto>]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 have "[xa\<mapsto>y] x = Some Ai" using prems 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[\<mapsto>]ys]) = dom([xs[\<mapsto>]bs])" by auto
with None have "[xs[\<mapsto>]bs] x = None" by (auto simp only:domIff)
moreover from x_eq_xa have sing_map: "[xa\<mapsto>b] x = Some b" by (auto simp only:map_upd_Some_unfold)
ultimately have "([xa\<mapsto>b] ++ [xs[\<mapsto>]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 prems 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 prems 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 prems by blast
hence "Suc i < length (h1#t1) ∧ e = (h1#t1)!(Suc i)" using prems 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 prems 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 prems 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 \<turnstile>+ M OK IN C"
shows "CT \<turnstile> mDef OK IN C"
using lookup_eq_Some M_ok
proof(induct M)
case Nil thus ?case by fastsimp
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 fastsimp+
hence c_not_obj:"C ≠ Object" by (force elim:ct_typing.cases)
from f_class have flds:"fields(CT,C) = DgCf'" by fastsimp
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 prems by force
qed
subsubsection{* Subtyping and Typing *}
lemma typings_lengths: assumes "CT;Γ \<turnstile>+ es:Cs" shows "length es = length Cs"
using assms by(induct "es" "Cs") (auto elim:typings.cases)
lemma typings_index:
assumes "CT;Γ \<turnstile>+ es:Cs"
shows "!!i. [| i < length es |] ==> CT;Γ \<turnstile> (es!i) : (Cs!i)"
proof -
have "length es = length Cs" using assms by (auto simp: typings_lengths)
thus "!!i. [| i < length es |] ==> CT;Γ \<turnstile> (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 \<turnstile>+ Cs <: Ds"
shows "!!i. [| i < length Cs |] ==> CT \<turnstile> (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 \<turnstile>+ Cs <: Ds"
and "CT \<turnstile> C <: D"
shows "CT \<turnstile>+ (Cs@[C]) <: (Ds@[D])"
using assms
by (induct rule:subtypings.induct) (auto simp add:subtypings.intros elim:subtypings.cases)
lemma typings_append:
assumes "CT;Γ \<turnstile>+ es : Cs"
and "CT;Γ \<turnstile> e : C"
shows "CT;Γ \<turnstile>+ (es@[e]) : (Cs@[C])"
proof -
have "length es = length Cs" using assms by(simp_all add:typings_lengths)
thus "CT;Γ \<turnstile>+ (es@[e]) : (Cs@[C])" using prems
proof(induct "es" "Cs" rule:list_induct2)
have "CT;Γ \<turnstile>+ []:[]" by(simp add:typings_typing.ts_nil)
moreover from assms have "CT;Γ \<turnstile> e : C" by simp
ultimately show "CT;Γ \<turnstile>+ ([]@[e]) : ([]@[C])" by (auto simp add:typings_typing.ts_cons)
next
fix x xs y ys
assume "length xs = length ys"
and IH: "[|CT;Γ \<turnstile>+ xs : ys; CT;Γ \<turnstile> e : C|] ==> CT;Γ \<turnstile>+ (xs @ [e]) : (ys @ [C])"
and x_xs_typs: "CT;Γ \<turnstile>+ (x # xs) : (y # ys)"
and e_typ: "CT;Γ \<turnstile> e : C"
from x_xs_typs have x_typ: "CT;Γ \<turnstile> x : y" and "CT;Γ \<turnstile>+ xs : ys" by(auto elim:typings.cases)
with IH e_typ have "CT;Γ \<turnstile>+ (xs@[e]) : (ys@[C])" by simp
with x_typ have "CT;Γ \<turnstile>+ ((x#xs)@[e]) : ((y#ys)@[C])" by (auto simp add:typings_typing.ts_cons)
thus "CT;Γ \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])" by(auto simp add:typings_typing.ts_cons)
qed
qed
lemma ith_typing: "!!Cs. [| CT;Γ \<turnstile>+ (es@(h#t)) : Cs |] ==> CT;Γ \<turnstile> h : (Cs!(length es))"
proof(induct "es", auto elim:typings.cases)
qed
lemma ith_subtyping: "!!Ds. [| CT \<turnstile>+ (Cs@(h#t)) <: Ds |] ==> CT \<turnstile> h <: (Ds!(length Cs))"
proof(induct "Cs", auto elim:subtypings.cases)
qed
lemma subtypings_refl: "CT \<turnstile>+ Cs <: Cs"
by(induct "Cs", auto simp add: subtyping.s_refl subtypings.intros)
lemma subtypings_trans: "!!Ds Es. [| CT \<turnstile>+ Cs <: Ds; CT \<turnstile>+ Ds <: Es |] ==> CT \<turnstile>+ Cs <: Es"
proof(induct "Cs")
case Nil thus ?case
by (auto elim:subtypings.cases simp add:subtypings.ss_nil)
next
case (Cons hCs tCs)
then obtain hDs tDs
where h1:"CT \<turnstile> hCs <: hDs" and t1:"CT \<turnstile>+ tCs <: tDs" and "Ds = hDs#tDs"
by (auto elim:subtypings.cases)
then obtain hEs tEs
where h2:"CT \<turnstile> hDs <: hEs" and t2:"CT \<turnstile>+ tDs <: tEs" and "Es = hEs#tEs"
using Cons by (auto elim:subtypings.cases)
moreover from subtyping.s_trans[OF h1 h2] have "CT \<turnstile> hCs <: hEs" by fastsimp
moreover with t1 t2 have "CT \<turnstile>+ tCs <: tEs" using Cons by simp_all
ultimately show ?case by (auto simp add:subtypings.intros)
qed
lemma ith_typing_sub:
"!!Cs. [| CT;Γ \<turnstile>+ (es@(h#t)) : Cs;
CT;Γ \<turnstile> h' : Ci';
CT \<turnstile> Ci' <: (Cs!(length es)) |]
==> ∃Cs'. (CT;Γ \<turnstile>+ (es@(h'#t)) : Cs' ∧ CT \<turnstile>+ Cs' <: Cs)"
proof(induct es)
case Nil
then obtain hCs tCs
where ts: "CT;Γ \<turnstile>+ t : tCs"
and Cs_def: "Cs = hCs # tCs" by(auto elim:typings.cases)
from Cs_def Nil have "CT \<turnstile> Ci' <: hCs" by auto
with Cs_def have "CT \<turnstile>+ (Ci'#tCs) <: Cs" by(auto simp add:subtypings.ss_cons subtypings_refl)
moreover from ts Nil have "CT;Γ \<turnstile>+ (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;Γ \<turnstile> eh : hCs"
and "CT;Γ \<turnstile>+ (et@(h#t)) : tCs"
and Cs_def: "Cs = hCs # tCs"
by(auto elim:typings.cases)
moreover with Cons obtain tCs'
where "CT;Γ \<turnstile>+ (et@(h'#t)) : tCs'"
and "CT \<turnstile>+ tCs' <: tCs"
by auto
ultimately have
"CT;Γ \<turnstile>+ (eh#(et@(h'#t))) : (hCs#tCs')"
and "CT \<turnstile>+ (hCs#tCs') <: Cs"
by(auto simp add:typings_typing.ts_cons subtypings.ss_cons subtyping.s_refl)
thus ?case by auto
qed
lemma mem_typings:
"!!Cs. [| CT;Γ \<turnstile>+ es:Cs; ei ∈ set es|] ==> ∃Ci. CT;Γ \<turnstile> 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;Γ \<turnstile>+ ds : As"
and "CT \<turnstile>+ As <: Bs"
and "length ds = length As"
and "length ds = length Bs"
and "i < length ds"
shows "CT;Γ \<turnstile> ds!i : As!i" and "CT \<turnstile> As!i <: Bs!i"
using assms by (auto simp add:typings_index subtypings_index)
lemma subtypings_length:
"CT \<turnstile>+ As <: Bs ==> length As = length Bs"
by(induct rule:subtypings.induct) simp_all
lemma not_subtypes_aux:
assumes "CT \<turnstile> C <: Da"
and "C ≠ Da"
and "CT C = Some CDef"
and "cSuper CDef = D"
shows "CT \<turnstile> D <: Da"
using assms
by (induct rule:subtyping.induct) (auto intro:subtyping.intros)
lemma not_subtypes:
assumes "CT \<turnstile> A <: C"
shows "!!D. [| CT \<turnstile> D ¬<: C; CT \<turnstile> C ¬<: D|] ==> CT \<turnstile> 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 \<turnstile> Da ¬<: D" proof(rule ccontr)
assume "¬ CT \<turnstile> Da ¬<: D"
hence da_sub_d:"CT \<turnstile> Da <: D" by auto
have d_sub_e:"CT \<turnstile> D <: E" using prems by fastsimp
thus "False" using prems by (force simp add:subtyping.s_trans[OF da_sub_d d_sub_e])
qed
have d_nsub_da:"CT \<turnstile> D ¬<: Da" using s_trans by auto
from da_nsub_d d_nsub_da s_trans show "CT \<turnstile> 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 \<turnstile> Da <: D" using prems by(auto simp add: subtyping.s_super)
thus "False" using prems by auto
qed
thus ?case using prems by (auto simp add: not_subtypes_aux)
qed
subsubsection{* Sub-Expressions *}
lemma isubexpr_typing:
assumes "e1 ∈ isubexprs(e0)"
shows "!!C. [| CT;empty \<turnstile> e0 : C |] ==> ∃D. CT;empty \<turnstile> 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;empty \<turnstile> e0 : C |] ==> ∃D. CT;empty \<turnstile> 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 \<turnstile> d1 -> d2 |] ==> ∃e2. CT \<turnstile> 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 \<turnstile> d1 -> d2 |] ==> ∃e2. CT \<turnstile> e1 -> e2"
using assms
by (induct rule:rtrancl.induct) (auto, force simp add: isubexpr_reduct)
end