(* 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 *) section ‹{\tt FJSound}: Type Soundness› theory FJSound imports FJAux begin text‹Type soundness is proved using the standard technique of progress and subject reduction. The numbered lemmas and theorems in this section correspond to the same results in the ACM TOPLAS paper. › subsection‹Method Type and Body Connection› lemma mtype_mbody: fixes Cs :: "nat list" assumes "mtype(CT,m,C) = Cs → C0" shows "∃xs e. mbody(CT,m,C) = xs . e ∧ length xs = length Cs" using assms proof(induct rule:mtype.induct) case(mt_class C0 Cs C CDef CT m mDef) thus ?case by (force simp add:varDefs_types_def varDefs_names_def elim:mtype.cases intro:mbody.mb_class) next case(mt_super CT C0 CDef m D Cs C) then obtain xs e where "mbody(CT,m,D) = xs . e" and "length xs = length Cs" by auto thus ?case using mt_super by (auto intro:mbody.mb_super) qed lemma mtype_mbody_length: assumes mt:"mtype(CT,m,C) = Cs → C0" and mb:"mbody(CT,m,C) = xs . e" shows "length xs = length Cs" proof - from mtype_mbody[OF mt] obtain xs' e' where mb2: "mbody(CT,m,C) = xs' . e'" and "length xs' = length Cs" by auto with mbody_functional[OF mb mb2] show ?thesis by auto qed subsection‹Method Types and Field Declarations of Subtypes› lemma A_1_1: assumes "CT ⊢ C <: D" and "CT OK" shows "(mtype(CT,m,D) = Cs → C0) ⟹ (mtype(CT,m,C) = Cs → C0)" using assms proof (induct rule:subtyping.induct) case (s_refl C CT) show ?case by fact next case (s_trans C CT D E) thus ?case by auto next case (s_super CT C CDef D) hence "CT ⊢ CDef OK" and "cName CDef = C" by(auto elim:ct_typing.cases) with s_super obtain M where M: "CT ⊢+ M OK IN C" and cMethods: "cMethods CDef = M" by(auto elim:class_typing.cases) let ?lookup_m = "lookup M (λmd. (mName md =m))" show ?case proof(cases "∃mDef. ?lookup_m = Some mDef") case True then obtain mDef where m: "?lookup_m = Some mDef" by(rule exE) hence mDef_name: "mName mDef = m" by (rule lookup_true) have "CT ⊢ mDef OK IN C" using M m by(auto simp add:method_typings_lookup) then obtain CDef' m' D' Cs' C0' where CT: "CT C = Some CDef'" and "cSuper CDef' = D'" and "mName mDef = m'" and mReturn: "mReturn mDef = C0'" and varDefs_types: "varDefs_types (mParams mDef) = Cs'" and "∀Ds D0. (mtype(CT,m',D') = Ds → D0) ⟶ Cs'=Ds ∧ C0'=D0" by (auto elim: method_typing.cases) with s_super mDef_name have "CDef=CDef'" and "D=D'" and "m=m'" and "∀Ds D0. (mtype(CT,m,D) = Ds → D0) ⟶ Cs'=Ds ∧ C0' = D0" by auto thus ?thesis using s_super cMethods m CT mReturn varDefs_types by (auto intro:mtype.intros) next case False hence "?lookup_m = None" by (simp add: lookup_split) then show ?thesis using s_super cMethods by (auto simp add:mtype.intros) qed qed lemma sub_fields: assumes "CT ⊢ C <: D" shows "⋀Dg. fields(CT,D) = Dg ⟹ ∃Cf. fields(CT,C) = (Dg@Cf)" using assms proof induct case (s_refl CT C) hence "fields(CT,C) = (Dg@[])" by simp thus ?case .. next case (s_trans CT C D E) then obtain Df Cf where "fields(CT,C) = ((Dg@Df)@Cf)" by force thus ?case by auto next case (s_super CT C CDef D Dg) then obtain Cf where "cFields CDef = Cf" by force with s_super have "fields(CT,C) = (Dg@Cf)" by(simp add:f_class) thus ?case .. qed subsection‹Substitution Lemma› lemma A_1_2: assumes "CT OK" and "Γ = Γ1 ++ Γ2" and "Γ2 = [xs [↦] Bs]" and "length xs = length ds" and "length Bs = length ds" and "∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs" shows "CT;Γ ⊢+ es:Ds ⟹ ∃Cs. (CT;Γ1 ⊢+ ([ds/xs]es):Cs ∧ CT ⊢+ Cs <: Ds)" (is "?TYPINGS ⟹ ?P1") and "CT;Γ ⊢ e:D ⟹ ∃C. (CT;Γ1 ⊢ ((ds/xs)e):C ∧ CT ⊢ C <: D)" (is "?TYPING ⟹ ?P2") proof - let ?COMMON_ASMS = "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" have RESULT:" (?TYPINGS ⟶ ?COMMON_ASMS ⟶ ?P1) ∧ (?TYPING ⟶ ?COMMON_ASMS ⟶ ?P2)" proof(induct rule:typings_typing.induct) case (ts_nil CT Γ) show ?case proof (rule impI) have "(CT;Γ1 ⊢+ ([ds/xs][]):[]) ∧ (CT ⊢+ [] <: [])" by (auto simp add: typings_typing.intros subtypings.intros) then show "∃Cs.(CT;Γ1 ⊢+ ([ds/xs][]):Cs) ∧ (CT ⊢+ Cs <: [])" by auto qed next case(ts_cons CT Γ e0 C0 es Cs') show ?case proof (rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" with ts_cons have e0_typ: "CT;Γ ⊢ e0 : C0" by fastforce with ts_cons asms have "∃C.(CT;Γ1 ⊢ (ds/xs) e0 : C) ∧ (CT ⊢ C <: C0)" and "∃Cs.(CT;Γ1 ⊢+ [ds/xs]es : Cs) ∧ (CT ⊢+ Cs <: Cs')" by auto then obtain C Cs where "(CT;Γ1 ⊢ (ds/xs) e0 : C) ∧ (CT ⊢ C <: C0)" and "(CT;Γ1 ⊢+ [ds/xs]es : Cs) ∧ (CT ⊢+ Cs <: Cs')" by auto hence "CT;Γ1 ⊢+ [ds/xs](e0#es) : (C#Cs)" and "CT ⊢+ (C#Cs) <: (C0#Cs')" by (auto simp add: typings_typing.intros subtypings.intros) then show "∃Cs. CT;Γ1 ⊢+ map (substs [xs [↦] ds]) (e0 # es) : Cs ∧ CT ⊢+ Cs <: (C0 # Cs')" by auto qed next case (t_var Γ x C' CT) show ?case proof (rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" hence lengths: "length ds = length Bs" and G_def: "Γ = Γ1 ++ Γ2" and G2_def : "Γ2 = [xs[↦]Bs]" by auto from lengths G2_def have same_doms: "dom([xs[↦]ds]) = dom(Γ2)" by auto from asms show "∃C. CT;Γ1 ⊢ substs [xs [↦] ds] (Var x) : C ∧ CT ⊢ C <: C'" proof (cases "Γ2 x") case None with G_def t_var have G1_x: "Γ1 x = Some C'" by(simp add:map_add_Some_iff) from None same_doms have "x ∉ dom([xs[↦]ds])" by (auto simp only:domIff) hence "[xs[↦]ds]x = None" by(auto simp only:map_add_Some_iff) hence "(ds/xs)(Var x) = (Var x)" by auto with G1_x have "CT;Γ1 ⊢ (ds/xs)(Var x) : C'" and "CT ⊢ C' <: C'" by (auto simp add:typings_typing.intros subtyping.intros) thus ?thesis by auto next case (Some Bi) with G_def t_var have c'_eq_bi: "C' = Bi" by (auto simp add: map_add_SomeD) from ‹length xs = length ds› asms have "length xs = length Bs" by simp with Some G2_def have "∃i.(Bs!i = Bi) ∧ (i < length Bs) ∧ (∀l.((length l = length Bs) ⟶ ([xs[↦]l] x = Some (l!i))))" by (auto simp add: map_upds_index) then obtain i where bs_i_proj: "(Bs!i = Bi)" and i_len: "i < length Bs" and P: "(⋀(l::exp list).((length l = length Bs) ⟶ ([xs[↦]l] x = Some (l!i))))" by fastforce from lengths P have subst_x: "([xs[↦]ds]x = Some (ds!i))" by auto from asms obtain As where as_ex:"CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs" by fastforce hence "length As = length Bs" by (auto simp add: subtypings_length) hence proj_i:"CT;Γ1 ⊢ ds!i : As!i ∧ CT ⊢ As!i <: Bs!i" using i_len lengths as_ex by (auto simp add: typings_proj) hence "CT;Γ1 ⊢ (ds/xs)(Var x) : As!i ∧ CT ⊢ As!i <: C'" using c'_eq_bi bs_i_proj subst_x by auto thus ?thesis .. qed qed next case(t_field CT Γ e0 C0 Cf fi fDef Ci) show ?case proof(rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" from t_field have flds: "fields(CT,C0) = Cf" by fastforce from t_field asms obtain C where e0_typ: "CT;Γ1 ⊢ (ds/xs)e0 : C" and sub: "CT ⊢ C <: C0" by auto from sub_fields[OF sub flds] obtain Dg where flds_C: "fields(CT,C) = (Cf@Dg)" .. from t_field have lookup_CfDg: "lookup (Cf@Dg) (λfd. vdName fd = fi) = Some fDef" by(simp add:lookup_append) from e0_typ flds_C lookup_CfDg t_field have "CT;Γ1 ⊢ (ds/xs)(FieldProj e0 fi) : Ci" by(simp add:typings_typing.intros) moreover have "CT ⊢ Ci <: Ci" by (simp add:subtyping.intros) ultimately show "∃C. CT;Γ1 ⊢ (ds/xs)(FieldProj e0 fi) : C ∧ CT ⊢ C <: Ci" by auto qed next case(t_invk CT Γ e0 C0 m Ds C es Cs) show ?case proof(rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" hence ct_ok: "CT OK" .. from t_invk have mtyp: "mtype(CT,m,C0) = Ds → C" and subs: "CT ⊢+ Cs <: Ds" and lens: "length es = length Ds" by auto from t_invk asms obtain C' where e0_typ: "CT;Γ1 ⊢ (ds/xs)e0 : C'" and sub': "CT ⊢ C' <: C0" by auto from t_invk asms obtain Cs' where es_typ: "CT;Γ1 ⊢+ [ds/xs]es : Cs'" and subs': "CT ⊢+ Cs' <: Cs" by auto have subst_e: "(ds/xs)(MethodInvk e0 m es) = MethodInvk ((ds/xs)e0) m ([ds/xs]es)" by(auto simp add: subst_list1_eq_map_substs) from e0_typ A_1_1[OF sub' ct_ok mtyp] es_typ subtypings_trans[OF subs' subs] lens subst_e have "CT;Γ1 ⊢ (ds/xs)(MethodInvk e0 m es) : C" by(auto simp add:typings_typing.intros) moreover have "CT ⊢ C <: C" by(simp add:subtyping.intros) ultimately show "∃C'. CT;Γ1 ⊢ (ds/xs)(MethodInvk e0 m es) : C' ∧ CT ⊢ C' <: C" by auto qed next case(t_new CT C Df es Ds Γ Cs) show ?case proof(rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" hence ct_ok: "CT OK" .. from t_new have subs: "CT ⊢+ Cs <: Ds" and flds: "fields(CT,C) = Df" and len: "length es = length Df" and vdts: "varDefs_types Df = Ds" by auto from t_new asms obtain Cs' where es_typ: "CT;Γ1 ⊢+ [ds/xs]es : Cs'" and subs': "CT ⊢+ Cs' <: Cs" by auto have subst_e: "(ds/xs)(New C es) = New C ([ds/xs]es)" by(auto simp add: subst_list2_eq_map_substs) from es_typ subtypings_trans[OF subs' subs] flds subst_e len vdts have "CT;Γ1 ⊢ (ds/xs)(New C es) : C" by(auto simp add:typings_typing.intros) moreover have "CT ⊢ C <: C" by(simp add:subtyping.intros) ultimately show "∃C'. CT;Γ1 ⊢ (ds/xs)(New C es) : C' ∧ CT ⊢ C' <: C" by auto qed next case(t_ucast CT Γ e0 D C) show ?case proof(rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" from t_ucast asms obtain C' where e0_typ: "CT;Γ1 ⊢ (ds/xs)e0 : C'" and sub1:"CT ⊢ C' <: D" and sub2:"CT ⊢ D <: C" by auto from sub1 sub2 have "CT ⊢ C' <: C" by (rule s_trans) with e0_typ have "CT;Γ1 ⊢ (ds/xs)(Cast C e0) : C" by(auto simp add: typings_typing.intros) moreover have "CT ⊢ C <: C" by (rule s_refl) ultimately show "∃C'. CT;Γ1 ⊢ (ds/xs)(Cast C e0) : C' ∧ CT ⊢ C' <: C" by auto qed next case(t_dcast CT Γ e0 D C) show ?case proof(rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" from t_dcast asms obtain C' where e0_typ:"CT;Γ1 ⊢ (ds/xs)e0 : C'" by auto have "(CT ⊢ C' <: C) ∨ (C ≠ C' ∧ CT ⊢ C <: C') ∨ (CT ⊢ C ¬<: C' ∧ CT ⊢ C' ¬<: C)" by blast moreover { assume "CT ⊢ C' <: C" with e0_typ have "CT;Γ1 ⊢ (ds/xs) (Cast C e0) : C" by (auto simp add: typings_typing.intros) } moreover { assume "(C ≠ C' ∧ CT ⊢ C <: C')" with e0_typ have "CT;Γ1 ⊢ (ds/xs) (Cast C e0) : C" by (auto simp add: typings_typing.intros) } moreover { assume "(CT ⊢ C ¬<: C' ∧ CT ⊢ C' ¬<: C)" with e0_typ have "CT;Γ1 ⊢ (ds/xs) (Cast C e0) : C" by (auto simp add: typings_typing.intros) } ultimately have "CT;Γ1 ⊢ (ds/xs) (Cast C e0) : C" by auto moreover have "CT ⊢ C <: C" by(rule s_refl) ultimately show "∃C'. CT;Γ1 ⊢ (ds/xs)(Cast C e0) : C' ∧ CT ⊢ C' <: C" by auto qed next case(t_scast CT Γ e0 D C) show ?case proof(rule impI) assume asms: "(CT OK) ∧ (Γ = Γ1 ++ Γ2) ∧ (Γ2 = [xs [↦] Bs]) ∧ (length Bs = length ds) ∧ (∃As. CT;Γ1 ⊢+ ds : As ∧ CT ⊢+ As <: Bs)" from t_scast asms obtain C' where e0_typ:"CT;Γ1 ⊢ (ds/xs)e0 : C'" and sub1: "CT ⊢ C' <: D" and nsub1: "CT ⊢ C ¬<: D" and nsub2: "CT ⊢ D ¬<: C" by auto from not_subtypes[OF sub1 nsub1 nsub2] have "CT ⊢ C' ¬<: C" by fastforce moreover have "CT ⊢ C ¬<: C'" proof(rule ccontr) assume "¬ CT ⊢ C ¬<: C'" hence "CT ⊢ C <: C'" by auto hence "CT ⊢ C <: D" using sub1 by(rule s_trans) with nsub1 show "False" by auto qed ultimately have "CT;Γ1 ⊢ (ds/xs) (Cast C e0) : C" using e0_typ by (auto simp add: typings_typing.intros) thus "∃C'. CT;Γ1 ⊢ (ds/xs)(Cast C e0) : C' ∧ CT ⊢ C' <: C" by (auto simp add: s_refl) qed qed thus "?TYPINGS ⟹ ?P1" and "?TYPING ⟹ ?P2" using assms by auto qed subsection‹Weakening Lemma› text ‹This lemma is not in the same form as in TOPLAS, but rather as we need it in subject reduction› lemma A_1_3: shows "(CT;Γ2 ⊢+ es : Cs) ⟹ (CT;Γ1++Γ2 ⊢+ es : Cs)" (is "?P1 ⟹ ?P2") and "CT;Γ2 ⊢ e : C ⟹ CT;Γ1++Γ2 ⊢ e : C" (is "?Q1 ⟹ ?Q2") proof - have "(?P1 ⟶ ?P2) ∧ (?Q1 ⟶ ?Q2)" by(induct rule:typings_typing.induct, auto simp add: map_add_find_right typings_typing.intros) thus "?P1 ⟹ ?P2" and "?Q1 ⟹ ?Q2" by auto qed subsection ‹Method Body Typing Lemma› lemma A_1_4: assumes ct_ok: "CT OK" and mb:"mbody(CT,m,C) = xs . e" and mt:"mtype(CT,m,C) = Ds → D" shows "∃D0 C0. (CT ⊢ C <: D0) ∧ (CT ⊢ C0 <: D) ∧ (CT;[xs[↦]Ds](this ↦ D0) ⊢ e : C0)" using mb ct_ok mt proof(induct rule: mbody.induct) case (mb_class CT C CDef m mDef xs e) hence m_param:"varDefs_types (mParams mDef) = Ds" and m_ret:"mReturn mDef = D" and "CT ⊢ CDef OK" and "cName CDef = C" by (auto elim:mtype.cases ct_typing.cases) hence "CT ⊢+ (cMethods CDef) OK IN C" by (auto elim:class_typing.cases) hence "CT ⊢ mDef OK IN C" using mb_class by(auto simp add:method_typings_lookup) hence "∃ E0. ((CT;[xs[↦]Ds,this↦C] ⊢ e : E0) ∧ (CT ⊢ E0 <: D))" using mb_class m_param m_ret by(auto elim:method_typing.cases) then obtain E0 where "CT;[xs[↦]Ds,this↦C] ⊢ e : E0" and "CT ⊢ E0 <: D" and "CT ⊢ C <: C" by (auto simp add: s_refl) thus ?case by blast next case (mb_super CT C CDef m Da xs e) hence ct: "CT OK" and IH: "⟦CT OK; mtype(CT,m,Da) = Ds → D⟧ ⟹ ∃D0 C0. (CT ⊢ Da <: D0) ∧ (CT ⊢ C0 <: D) ∧ (CT;[xs [↦] Ds, this ↦ D0] ⊢ e:C0)" by fastforce+ from mb_super have c_sub_da: "CT ⊢ C <: Da" by (auto simp add:s_super) from mb_super have mt:"mtype(CT,m,Da) = Ds → D" by (auto elim: mtype.cases) from IH[OF ct mt] obtain D0 C0 where s1: "CT ⊢ Da <: D0" and "CT ⊢ C0 <: D" and "CT;[xs [↦] Ds, this ↦ D0] ⊢ e : C0" by auto thus ?case using s_trans[OF c_sub_da s1] by blast qed subsection ‹Subject Reduction Theorem› theorem Thm_2_4_1: assumes "CT ⊢ e → e'" and "CT OK" shows "⋀C. ⟦ CT;Γ ⊢ e : C ⟧ ⟹ ∃C'. (CT;Γ ⊢ e' : C' ∧ CT ⊢ C' <: C)" using assms proof(induct rule: reduction.induct) case (r_field CT Ca Cf es fi e') hence "CT;Γ ⊢ FieldProj (New Ca es) fi : C" and ct_ok: "CT OK" and flds: "fields(CT,Ca) = Cf" and lkup2: "lookup2 Cf es (λfd. vdName fd = fi) = Some e'" by fastforce+ then obtain Ca' Cf' fDef where new_typ: "CT;Γ ⊢ New Ca es : Ca'" and flds':"fields(CT,Ca') = Cf'" and lkup: "lookup Cf' (λfd. vdName fd = fi) = Some fDef" and C_def: "vdType fDef = C" by (auto elim: typing.cases) hence Ca_Ca': "Ca = Ca'" by (auto elim:typing.cases) with flds' have Cf_Cf': "Cf = Cf'" by(simp add:fields_functional[OF flds ct_ok]) from new_typ obtain Cs Ds Cf'' where "fields(CT,Ca') = Cf''" and es_typs: "CT;Γ ⊢+ es:Cs" and Ds_def: "varDefs_types Cf'' = Ds" and length_Cf_es: "length Cf'' = length es" and subs: "CT ⊢+ Cs <: Ds" by(auto elim:typing.cases) with Ca_Ca' have Cf_Cf'': "Cf = Cf''" by(auto simp add:fields_functional[OF flds ct_ok]) from length_Cf_es Cf_Cf'' lookup2_index[OF lkup2] obtain i where i_bound: "i < length es" and "e' = es!i" and "lookup Cf (λfd. vdName fd = fi) = Some (Cf!i)" by auto moreover with C_def Ds_def lkup lkup2 have "Ds!i = C" using Ca_Ca' Cf_Cf' Cf_Cf'' i_bound length_Cf_es flds' by (auto simp add:nth_map varDefs_types_def fields_functional[OF flds ct_ok]) moreover with subs es_typs have "CT;Γ ⊢ (es!i):(Cs!i)" and "CT ⊢ (Cs!i) <: (Ds!i)" using i_bound by(auto simp add:typings_index subtypings_index typings_lengths) ultimately show ?case by auto next case(r_invk CT m Ca xs e ds es e') from r_invk have mb: "mbody(CT,m,Ca) = xs . e" by fastforce from r_invk obtain Ca' Ds Cs where "CT;Γ ⊢ New Ca es : Ca'" and "mtype(CT,m,Ca') = Cs → C" and ds_typs: "CT;Γ ⊢+ ds : Ds" and Ds_subs: "CT ⊢+ Ds <: Cs" and l1: "length ds = length Cs" by(auto elim:typing.cases) hence new_typ: "CT;Γ ⊢ New Ca es : Ca" and mt: "mtype(CT,m,Ca) = Cs → C" by (auto elim:typing.cases) from ds_typs new_typ have "CT;Γ ⊢+ (ds @[New Ca es]) : (Ds @[Ca])" by (simp add:typings_append) moreover from A_1_4[OF _ mb mt] r_invk obtain Da E where "CT ⊢ Ca <: Da" and E_sub_C: "CT ⊢ E <: C" and e0_typ1: "CT;[xs[↦]Cs,this↦Da] ⊢ e : E" by auto moreover with Ds_subs have "CT ⊢+ (Ds@[Ca]) <: (Cs@[Da])" by(auto simp add:subtyping_append) ultimately have ex: "∃As. CT;Γ ⊢+ (ds @[New Ca es]) : As ∧ CT ⊢+ As <: (Cs@[Da])" by auto from e0_typ1 have e0_typ2: "CT;(Γ ++ [xs[↦]Cs,this↦Da]) ⊢ e : E" by(simp only:A_1_3) from e0_typ2 mtype_mbody_length[OF mt mb] have e0_typ3: "CT;(Γ ++ [(xs@[this])[↦](Cs@[Da])]) ⊢ e : E" by(force simp only:map_shuffle) let ?Γ1 = "Γ" and ?Γ2 = "[(xs@[this])[↦](Cs@[Da])]" have g_def: "(?Γ1 ++ ?Γ2) = (?Γ1 ++ ?Γ2)" and g2_def: "?Γ2 = ?Γ2" by auto from A_1_2[OF _ g_def g2_def _ _ ex] e0_typ3 r_invk l1 mtype_mbody_length[OF mt mb] obtain E' where e'_typ: "CT;Γ ⊢ substs [(xs@[this])[↦](ds@[New Ca es])] e : E'" and E'_sub_E: "CT ⊢ E' <: E" by force moreover from e'_typ l1 mtype_mbody_length[OF mt mb] have "CT;Γ ⊢ substs [xs[↦]ds,this↦(New Ca es)] e : E'" by(auto simp only:map_shuffle) moreover from E'_sub_E E_sub_C have "CT ⊢ E' <: C" by (rule subtyping.s_trans) ultimately show ?case using r_invk by auto next case (r_cast CT Ca D es) then obtain Ca' where "C = D" and "CT;Γ ⊢ New Ca es : Ca'" by (auto elim: typing.cases) thus ?case using r_cast by (auto elim: typing.cases) next case (rc_field CT e0 e0' f) then obtain C0 Cf fd where "CT;Γ ⊢ e0 : C0" and Cf_def: "fields(CT,C0) = Cf" and fd_def:"lookup Cf (λfd. (vdName fd = f)) = Some fd" and "vdType fd = C" by (auto elim:typing.cases) moreover with rc_field obtain C' where "CT;Γ ⊢ e0' : C'" and "CT ⊢ C' <: C0" by auto moreover from sub_fields[OF _ Cf_def] obtain Cf' where "fields(CT,C') = (Cf@Cf')" by rule (rule ‹CT ⊢ C' <: C0›) moreover with fd_def have "lookup (Cf@Cf') (λfd. (vdName fd = f)) = Some fd" by(simp add:lookup_append) ultimately have "CT;Γ ⊢ FieldProj e0' f : C" by(auto simp add:typings_typing.t_field) thus ?case by (auto simp add:subtyping.s_refl) next case (rc_invk_recv CT e0 e0' m es C) then obtain C0 Ds Cs where ct_ok:"CT OK" and "CT;Γ ⊢ e0 : C0" and mt:"mtype(CT,m,C0) = Ds → C" and "CT;Γ ⊢+ es : Cs" and "length es = length Ds" and "CT ⊢+ Cs <: Ds" by (auto elim:typing.cases) moreover with rc_invk_recv obtain C0' where "CT;Γ ⊢ e0' : C0'" and "CT ⊢ C0' <: C0" by auto moreover with A_1_1[OF _ ct_ok mt] have "mtype(CT,m,C0') = Ds → C" by simp ultimately have "CT;Γ ⊢ MethodInvk e0' m es : C" by(auto simp add:typings_typing.t_invk) thus ?case by (auto simp add:subtyping.s_refl) next case (rc_invk_arg CT ei ei' e0 m el er C) then obtain Cs Ds C0 where typs: "CT;Γ ⊢+ (el@(ei#er)) : Cs" and e0_typ: "CT;Γ ⊢ e0 : C0" and mt: "mtype(CT,m,C0) = Ds → C" and Cs_sub_Ds: "CT ⊢+ Cs <: Ds" and len: "length (el@(ei#er)) = length Ds" by(auto elim:typing.cases) hence "CT;Γ ⊢ ei:(Cs!(length el))" by (simp add:ith_typing) with rc_invk_arg obtain Ci' where ei_typ: "CT;Γ ⊢ ei':Ci'" and Ci_sub: "CT ⊢ Ci' <: (Cs!(length el))" by auto from ith_typing_sub[OF typs ei_typ Ci_sub] obtain Cs' where es'_typs: "CT;Γ ⊢+ (el@(ei'#er)) : Cs'" and Cs'_sub_Cs: "CT ⊢+ Cs' <: Cs" by auto from len have "length (el@(ei'#er)) = length Ds" by simp with es'_typs subtypings_trans[OF Cs'_sub_Cs Cs_sub_Ds] e0_typ mt have "CT;Γ ⊢ MethodInvk e0 m (el@(ei'#er)) : C" by(auto simp add:typings_typing.t_invk) thus ?case by (auto simp add:subtyping.s_refl) next case (rc_new_arg CT ei ei' Ca el er C) then obtain Cs Df Ds where typs: "CT;Γ ⊢+ (el@(ei#er)) : Cs" and flds: "fields(CT,C) = Df" and len: "length (el@(ei#er)) = length Df" and Ds_def: "varDefs_types Df = Ds" and Cs_sub_Ds: "CT ⊢+ Cs <: Ds" and C_def: "Ca = C" by(auto elim:typing.cases) hence "CT;Γ ⊢ ei:(Cs!(length el))" by (simp add:ith_typing) with rc_new_arg obtain Ci' where ei_typ: "CT;Γ ⊢ ei':Ci'" and Ci_sub: "CT ⊢ Ci' <: (Cs!(length el))" by auto from ith_typing_sub[OF typs ei_typ Ci_sub] obtain Cs' where es'_typs: "CT;Γ ⊢+ (el@(ei'#er)) : Cs'" and Cs'_sub_Cs: "CT ⊢+ Cs' <: Cs" by auto from len have "length (el@(ei'#er)) = length Df" by simp with es'_typs subtypings_trans[OF Cs'_sub_Cs Cs_sub_Ds] flds Ds_def C_def have "CT;Γ ⊢ New Ca (el@(ei'#er)) : C" by(auto simp add:typings_typing.t_new) thus ?case by (auto simp add:subtyping.s_refl) next case (rc_cast CT e0 e0' C Ca) then obtain D where "CT;Γ ⊢ e0 : D" and Ca_def: "Ca = C" by(auto elim:typing.cases) with rc_cast obtain D' where e0'_typ: "CT;Γ ⊢ e0':D'" and "CT ⊢ D' <: D" by auto have "(CT ⊢ D' <: C) ∨ (C ≠ D' ∧ CT ⊢ C <: D') ∨ (CT ⊢ C ¬<: D' ∧ CT ⊢ D' ¬<: C)" by blast moreover { assume "CT ⊢ D' <: C" with e0'_typ have "CT;Γ ⊢ Cast C e0' : C" by (auto simp add: typings_typing.t_ucast) } moreover { assume "(C ≠ D' ∧ CT ⊢ C <: D')" with e0'_typ have "CT;Γ ⊢ Cast C e0' : C" by (auto simp add: typings_typing.t_dcast) } moreover { assume "(CT ⊢ C ¬<: D' ∧ CT ⊢ D' ¬<: C)" with e0'_typ have "CT;Γ ⊢ Cast C e0' : C" by (auto simp add: typings_typing.t_scast) } ultimately have "CT;Γ ⊢ Cast C e0' : C" by auto thus ?case using Ca_def by (auto simp add:subtyping.s_refl) qed subsection ‹Multi-Step Subject Reduction Theorem› corollary Cor_2_4_1_multi: assumes "CT ⊢ e →* e'" and "CT OK" shows "⋀C. ⟦ CT;Γ ⊢ e : C ⟧ ⟹ ∃C'. (CT;Γ ⊢ e' : C' ∧ CT ⊢ C' <: C)" using assms proof induct case (rs_refl CT e C) thus ?case by (auto simp add:subtyping.s_refl) next case(rs_trans CT e e' e'' C) hence e_typ: "CT;Γ ⊢ e : C" and e_step: "CT ⊢ e → e'" and ct_ok: "CT OK" and IH: "⋀D. ⟦CT;Γ ⊢ e' : D; CT OK⟧ ⟹ ∃E. CT;Γ ⊢ e'' : E ∧ CT ⊢ E <: D" by auto from Thm_2_4_1[OF e_step ct_ok e_typ] obtain D where e'_typ: "CT;Γ ⊢ e' : D" and D_sub_C: "CT ⊢ D <: C" by auto with IH[OF e'_typ ct_ok] obtain E where "CT;Γ ⊢ e'': E" and E_sub_D: "CT ⊢ E <: D" by auto moreover from s_trans[OF E_sub_D D_sub_C] have "CT ⊢ E <: C" by auto ultimately show ?case by auto qed subsection ‹Progress› text ‹The two "progress lemmas" proved in the TOPLAS paper alone are not quite enough to prove type soundness. We prove an additional lemma showing that every well-typed expression is either a value or contains a potential redex as a sub-expression.› theorem Thm_2_4_2_1: assumes "CT;Map.empty ⊢ e : C" and "FieldProj (New C0 es) fi ∈ subexprs(e)" shows "∃Cf fDef. fields(CT, C0) = Cf ∧ lookup Cf (λfd. (vdName fd = fi)) = Some fDef" proof - obtain Ci where "CT;Map.empty ⊢ (FieldProj (New C0 es) fi) : Ci" using assms by (force simp add:subexpr_typing) then obtain Cf fDef C0' where "CT;Map.empty ⊢ (New C0 es) : C0'" and "fields(CT,C0') = Cf" and "lookup Cf (λfd. (vdName fd = fi)) = Some fDef" by (auto elim:typing.cases) thus ?thesis by (auto elim:typing.cases) qed lemma Thm_2_4_2_2: fixes es ds :: "exp list" assumes "CT;Map.empty ⊢ e : C" and "MethodInvk (New C0 es) m ds ∈ subexprs(e)" shows "∃xs e0. mbody(CT,m,C0) = xs . e0 ∧ length xs = length ds" proof - obtain D where "CT;Map.empty ⊢ MethodInvk (New C0 es) m ds : D" using assms by (force simp add:subexpr_typing) then obtain C0' Cs where "CT;Map.empty ⊢ (New C0 es) : C0'" and mt:"mtype(CT,m,C0') = Cs → D" and "length ds = length Cs" by (auto elim:typing.cases) with mtype_mbody[OF mt] show ?thesis by (force elim:typing.cases) qed lemma closed_subterm_split: assumes "CT;Γ ⊢ e : C" and "Γ = Map.empty" shows " ((∃C0 es fi. (FieldProj (New C0 es) fi) ∈ subexprs(e)) ∨ (∃C0 es m ds. (MethodInvk (New C0 es) m ds) ∈ subexprs(e)) ∨ (∃C0 D es. (Cast D (New C0 es)) ∈ subexprs(e)) ∨ val(e))" (is "?F e ∨ ?M e ∨ ?C e ∨ ?V e" is "?IH e") using assms proof(induct CT Γ e C rule:typing_induct) case 1 thus ?case using assms by auto next case (2 C CT Γ x) thus ?case by auto next case (3 C0 Ct Cf Ci Γ e0 fDef fi) have s1: "e0 ∈ subexprs(FieldProj e0 fi)" by(auto simp add:isubexprs.intros) from 3 have "?IH e0" by auto moreover { assume "?F e0" then obtain C0 es fi' where s2: "FieldProj (New C0 es) fi' ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?M e0" then obtain C0 es m ds where s2: "MethodInvk (New C0 es) m ds ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?C e0" then obtain C0 D es where s2: "Cast D (New C0 es) ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?V e0" then obtain C0 es where "e0 = (New C0 es)" and "vals(es)" by (force elim:val.cases) hence ?case by(force intro:isubexprs.intros) } ultimately show ?case by blast next case (4 C C0 CT Cs Ds Γ e0 es m) have s1: "e0 ∈ subexprs(MethodInvk e0 m es)" by(auto simp add:isubexprs.intros) from 4 have "?IH e0" by auto moreover { assume "?F e0" then obtain C0 es fi where s2: "FieldProj (New C0 es) fi ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?M e0" then obtain C0 es' m' ds where s2: "MethodInvk (New C0 es') m' ds ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?C e0" then obtain C0 D es where s2: "Cast D (New C0 es) ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?V e0" then obtain C0 es' where "e0 = (New C0 es')" and "vals(es')" by (force elim:val.cases) hence ?case by(force intro:isubexprs.intros) } ultimately show ?case by blast next case (5 C CT Cs Df Ds Γ es) hence "length es = length Cs" "⋀ i. ⟦i < length es; CT;Γ ⊢ (es!i) : (Cs!i); Γ = Map.empty⟧ ⟹ ?IH (es!i)" and "CT;Γ ⊢+ es : Cs" by (auto simp add:typings_lengths) hence "(∃i < length es. (?F (es!i) ∨ ?M (es!i) ∨ ?C (es!i))) ∨ (vals(es))" (is "?Q es") proof(induct "es" "Cs" rule:list_induct2) case Nil thus "?Q []" by(auto intro:vals_val.intros) next case (Cons h t Ch Ct) with 5 have h_t_typs: "CT;Γ ⊢+ (h#t) : (Ch#Ct)" and OIH: "⋀ i. ⟦i < length (h#t); CT;Γ ⊢ ((h#t)!i) : ((Ch#Ct)!i); Γ = Map.empty⟧ ⟹ ?IH ((h#t)!i)" and G_def: "Γ = Map.empty" by auto from h_t_typs have h_typ: "CT;Γ ⊢ (h#t)!0 : (Ch#Ct)!0" and t_typs: "CT;Γ ⊢+ t : Ct" by(auto elim:typings.cases) { fix i assume "i < length t" hence s_i: "Suc i < length (h#t)" by auto from OIH[OF s_i] have "⟦i < length t; CT;Γ ⊢ (t!i) : (Ct!i); Γ = Map.empty⟧ ⟹ ?IH (t!i)" by auto } with t_typs have "?Q t" using Cons by auto moreover { assume "∃i < length t. (?F (t!i) ∨ ?M (t!i) ∨ ?C (t!i))" then obtain i where "i < length t" and "?F (t!i) ∨ ?M (t!i) ∨ ?C (t!i)" by force hence "(Suc i < length (h#t)) ∧ (?F ((h#t)!(Suc i)) ∨ ?M ((h#t)!(Suc i)) ∨ ?C ((h#t)!(Suc i)))" by auto hence "∃i < length (h#t). (?F ((h#t)!i) ∨ ?M ((h#t)!i) ∨ ?C ((h#t)!i))" .. hence "?Q (h#t)" by auto } moreover { assume v_t: "vals(t)" from OIH[OF _ h_typ G_def] have "?IH h" by auto moreover { assume "?F h ∨ ?M h ∨ ?C h" hence "?F ((h#t)!0) ∨ ?M ((h#t)!0) ∨ ?C ((h#t)!0)" by auto hence "?Q (h#t)" by force } moreover { assume "?V h" with v_t have "vals((h#t))" by (force intro:vals_val.intros) hence "?Q(h#t)" by auto } ultimately have "?Q(h#t)" by blast } ultimately show "?Q(h#t)" by blast qed moreover { assume "∃i<length es. ?F (es!i) ∨ ?M (es!i) ∨ ?C(es!i)" then obtain i where i_len: "i < length es" and r: "?F (es!i) ∨ ?M (es!i) ∨ ?C(es!i)" by force from ith_mem[OF i_len] have s1:"es!i ∈ subexprs(New C es)" by(auto intro:isubexprs.se_newarg) { assume "?F (es!i)" then obtain C0 es' fi where s2: "FieldProj (New C0 es') fi ∈ subexprs(es!i)" by auto from rtrancl_trans[OF s2 s1] have "?F(New C es) ∨ ?M(New C es) ∨ ?C(New C es)" by auto } moreover { assume "?M (es!i)" then obtain C0 es' m' ds where s2: "MethodInvk (New C0 es') m' ds ∈ subexprs(es!i)" by force from rtrancl_trans[OF s2 s1] have "?F(New C es) ∨ ?M(New C es) ∨ ?C(New C es)" by auto } moreover { assume "?C (es!i)" then obtain C0 D es' where s2: "Cast D (New C0 es') ∈ subexprs(es!i)" by auto from rtrancl_trans[OF s2 s1] have "?F(New C es) ∨ ?M(New C es) ∨ ?C(New C es)" by auto } ultimately have "?F(New C es) ∨ ?M(New C es) ∨ ?C(New C es)" using r by blast hence ?case by auto } moreover { assume "vals(es)" hence ?case by(auto intro:vals_val.intros) } ultimately show ?case by blast next case (6 C CT D Γ e0) have s1: "e0 ∈ subexprs(Cast C e0)" by(auto simp add:isubexprs.intros) from 6 have "?IH e0" by auto moreover { assume "?F e0" then obtain C0 es fi where s2: "FieldProj (New C0 es) fi ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?M e0" then obtain C0 es m ds where s2: "MethodInvk (New C0 es) m ds ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?C e0" then obtain C0 D' es where s2: "Cast D' (New C0 es) ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?V e0" then obtain C0 es' where "e0 = (New C0 es')" and "vals(es')" by (force elim:val.cases) hence ?case by(force intro:isubexprs.intros) } ultimately show ?case by blast next case (7 C CT D Γ e0) have s1: "e0 ∈ subexprs(Cast C e0)" by(auto simp add:isubexprs.intros) from 7 have "?IH e0" by auto moreover { assume "?F e0" then obtain C0 es fi where s2: "FieldProj (New C0 es) fi ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?M e0" then obtain C0 es m ds where s2: "MethodInvk (New C0 es) m ds ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?C e0" then obtain C0 D' es where s2: "Cast D' (New C0 es) ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?V e0" then obtain C0 es' where "e0 = (New C0 es')" and "vals(es')" by (force elim:val.cases) hence ?case by(force intro:isubexprs.intros) } ultimately show ?case by blast next case (8 C CT D Γ e0) have s1: "e0 ∈ subexprs(Cast C e0)" by(auto simp add:isubexprs.intros) from 8 have "?IH e0" by auto moreover { assume "?F e0" then obtain C0 es fi where s2: "FieldProj (New C0 es) fi ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?M e0" then obtain C0 es m ds where s2: "MethodInvk (New C0 es) m ds ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?C e0" then obtain C0 D' es where s2: "Cast D' (New C0 es) ∈ subexprs(e0)" by auto from rtrancl_trans[OF s2 s1] have ?case by auto } moreover { assume "?V e0" then obtain C0 es' where "e0 = (New C0 es')" and "vals(es')" by (force elim:val.cases) hence ?case by(force intro:isubexprs.intros) } ultimately show ?case by blast qed subsection ‹Type Soundness Theorem› theorem Thm_2_4_3: assumes e_typ: "CT;Map.empty ⊢ e : C" and ct_ok: "CT OK" and multisteps: "CT ⊢ e →* e1" and no_step: "¬(∃e2. CT ⊢ e1 → e2)" shows "(val(e1) ∧ (∃D. CT;Map.empty ⊢ e1 : D ∧ CT ⊢ D <: C)) ∨ (∃D C es. (Cast D (New C es) ∈ subexprs(e1) ∧ CT ⊢ C ¬<: D))" proof - from assms Cor_2_4_1_multi[OF multisteps ct_ok e_typ] obtain C1 where e1_typ: "CT;Map.empty ⊢ e1 : C1" and C1_sub_C: "CT ⊢ C1 <: C" by auto from e1_typ have "((∃C0 es fi. (FieldProj (New C0 es) fi) ∈ subexprs(e1)) ∨ (∃C0 es m ds. (MethodInvk (New C0 es) m ds) ∈ subexprs(e1)) ∨ (∃C0 D es. (Cast D (New C0 es)) ∈ subexprs(e1)) ∨ val(e1))" (is "?F e1 ∨ ?M e1 ∨ ?C e1 ∨ ?V e1") by (simp add: closed_subterm_split) moreover { assume "?F e1" then obtain C0 es fi where fp: "FieldProj (New C0 es) fi ∈ subexprs(e1)" by auto then obtain Ci where "CT;Map.empty ⊢ FieldProj (New C0 es) fi : Ci" using e1_typ by(force simp add:subexpr_typing) then obtain C0' where new_typ: "CT;Map.empty ⊢ New C0 es : C0'" by (force elim: typing.cases) hence "C0 = C0'" by (auto elim:typing.cases) with new_typ obtain Df where f1: "fields(CT,C0) = Df" and lens: "length es = length Df" by(auto elim:typing.cases) from Thm_2_4_2_1[OF e1_typ fp] obtain Cf fDef where f2: "fields(CT,C0) = Cf" and lkup: "lookup Cf (λfd. vdName fd = fi) = Some(fDef)" by force moreover from fields_functional[OF f1 ct_ok f2] lens have "length es = length Cf" by auto moreover from lookup_index[OF lkup] obtain i where "i<length Cf" and "fDef = Cf ! i" and "(length Cf = length es) ⟶ lookup2 Cf es (λfd. vdName fd = fi) = Some (es ! i)" by auto ultimately have "lookup2 Cf es (λfd. vdName fd = fi) = Some (es!i)" by auto with f2 have "CT ⊢ FieldProj(New C0 es) fi → (es!i)" by(auto intro:reduction.intros) with fp have "∃e2. CT ⊢ e1 → e2" by(simp add:subexpr_reduct) with no_step have ?thesis by auto } moreover { assume "?M e1" then obtain C0 es m ds where mi:"MethodInvk (New C0 es) m ds ∈ subexprs(e1)" by auto then obtain D where "CT;Map.empty ⊢ MethodInvk (New C0 es) m ds : D" using e1_typ by(force simp add:subexpr_typing) then obtain C0' Es E where m_typ: "CT;Map.empty ⊢ New C0 es : C0'" and "mtype(CT,m,C0') = Es → E" and "length ds = length Es" by (auto elim:typing.cases) from Thm_2_4_2_2[OF e1_typ mi] obtain xs e0 where mb: "mbody(CT, m, C0) = xs . e0" and "length xs = length ds" by auto hence "CT ⊢ (MethodInvk (New C0 es) m ds) → (substs[xs[↦]ds,this↦(New C0 es)]e0)" by(auto simp add:reduction.intros) with mi have "∃e2. CT ⊢ e1 → e2" by(simp add:subexpr_reduct) with no_step have ?thesis by auto } moreover { assume "?C e1" then obtain C0 D es where c_def: "Cast D (New C0 es) ∈ subexprs(e1)" by auto then obtain D' where "CT;Map.empty ⊢ Cast D (New C0 es) : D'" using e1_typ by (force simp add:subexpr_typing) then obtain C0' where new_typ: "CT;Map.empty ⊢ New C0 es : C0'" and D_eq_D': "D = D'" by (auto elim:typing.cases) hence C0_eq_C0': "C0 = C0'" by(auto elim:typing.cases) hence ?thesis proof(cases "CT ⊢ C0 <: D") case True hence "CT ⊢ Cast D (New C0 es) → (New C0 es)" by(auto simp add:reduction.intros) with c_def have "∃e2. CT ⊢ e1 → e2" by (simp add:subexpr_reduct) with no_step show ?thesis by auto next case False with c_def show ?thesis by auto qed } moreover { assume "?V e1" hence ?thesis using assms by(auto simp add:Cor_2_4_1_multi) } ultimately show ?thesis by blast qed end