(* 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> License: LGPL 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 by (auto elim:subtypings.cases simp add:subtypings.ss_nil) 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" by(auto simp add:typings_typing.ts_cons subtypings.ss_cons subtyping.s_refl) 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