(* *) (* Formalisation of the chapter on Logical Relations *) (* and a Case Study in Equivalence Checking *) (* by Karl Crary from the book on Advanced Topics in *) (* Types and Programming Languages, MIT Press 2005 *) (* The formalisation was done by Julien Narboux and *) (* Christian Urban. *) theory Crary imports "HOL-Nominal.Nominal" begin atom_decl name nominal_datatype ty = TBase | TUnit | Arrow "ty" "ty" ("_→_" [100,100] 100) nominal_datatype trm = Unit | Var "name" ("Var _" [100] 100) | Lam "«name»trm" ("Lam [_]._" [100,100] 100) | App "trm" "trm" ("App _ _" [110,110] 100) | Const "nat" type_synonym Ctxt = "(name×ty) list" type_synonym Subst = "(name×trm) list" lemma perm_ty[simp]: fixes T::"ty" and pi::"name prm" shows "pi∙T = T" by (induct T rule: ty.induct) (simp_all) lemma fresh_ty[simp]: fixes x::"name" and T::"ty" shows "x♯T" by (simp add: fresh_def supp_def) lemma ty_cases: fixes T::ty shows "(∃ T⇩_{1}T⇩_{2}. T=T⇩_{1}→T⇩_{2}) ∨ T=TUnit ∨ T=TBase" by (induct T rule:ty.induct) (auto) instantiation ty :: size begin nominal_primrec size_ty where "size (TBase) = 1" | "size (TUnit) = 1" | "size (T⇩_{1}→T⇩_{2}) = size T⇩_{1}+ size T⇩_{2}" by (rule TrueI)+ instance .. end lemma ty_size_greater_zero[simp]: fixes T::"ty" shows "size T > 0" by (nominal_induct rule: ty.strong_induct) (simp_all) section ‹Substitutions› fun lookup :: "Subst ⇒ name ⇒ trm" where "lookup [] x = Var x" | "lookup ((y,T)#θ) x = (if x=y then T else lookup θ x)" lemma lookup_eqvt[eqvt]: fixes pi::"name prm" shows "pi∙(lookup θ x) = lookup (pi∙θ) (pi∙x)" by (induct θ) (auto simp add: perm_bij) lemma lookup_fresh: fixes z::"name" assumes a: "z♯θ" "z♯x" shows "z♯ lookup θ x" using a by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) lemma lookup_fresh': assumes a: "z♯θ" shows "lookup θ z = Var z" using a by (induct rule: lookup.induct) (auto simp add: fresh_list_cons fresh_prod fresh_atm) nominal_primrec psubst :: "Subst ⇒ trm ⇒ trm" ("_<_>" [100,100] 130) where "θ<(Var x)> = (lookup θ x)" | "θ<(App t⇩_{1}t⇩_{2})> = App θ<t⇩_{1}> θ<t⇩_{2}>" | "x♯θ ⟹ θ<(Lam [x].t)> = Lam [x].(θ<t>)" | "θ<(Const n)> = Const n" | "θ<(Unit)> = Unit" apply(finite_guess)+ apply(rule TrueI)+ apply(simp add: abs_fresh)+ apply(fresh_guess)+ done abbreviation subst :: "trm ⇒ name ⇒ trm ⇒ trm" ("_[_::=_]" [100,100,100] 100) where "t[x::=t'] ≡ ([(x,t')])<t>" lemma subst[simp]: shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" and "(App t⇩_{1}t⇩_{2})[y::=t'] = App (t⇩_{1}[y::=t']) (t⇩_{2}[y::=t'])" and "x♯(y,t') ⟹ (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" and "Const n[y::=t'] = Const n" and "Unit [y::=t'] = Unit" by (simp_all add: fresh_list_cons fresh_list_nil) lemma subst_eqvt[eqvt]: fixes pi::"name prm" shows "pi∙(t[x::=t']) = (pi∙t)[(pi∙x)::=(pi∙t')]" by (nominal_induct t avoiding: x t' rule: trm.strong_induct) (perm_simp add: fresh_bij)+ lemma subst_rename: fixes c::"name" assumes a: "c♯t⇩_{1}" shows "t⇩_{1}[a::=t⇩_{2}] = ([(c,a)]∙t⇩_{1})[c::=t⇩_{2}]" using a apply(nominal_induct t⇩_{1}avoiding: a c t⇩_{2}rule: trm.strong_induct) apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+ done lemma fresh_psubst: fixes z::"name" assumes a: "z♯t" "z♯θ" shows "z♯(θ<t>)" using a by (nominal_induct t avoiding: z θ t rule: trm.strong_induct) (auto simp add: abs_fresh lookup_fresh) lemma fresh_subst'': fixes z::"name" assumes "z♯t⇩_{2}" shows "z♯t⇩_{1}[z::=t⇩_{2}]" using assms by (nominal_induct t⇩_{1}avoiding: t⇩_{2}z rule: trm.strong_induct) (auto simp add: abs_fresh fresh_nat fresh_atm) lemma fresh_subst': fixes z::"name" assumes "z♯[y].t⇩_{1}" "z♯t⇩_{2}" shows "z♯t⇩_{1}[y::=t⇩_{2}]" using assms by (nominal_induct t⇩_{1}avoiding: y t⇩_{2}z rule: trm.strong_induct) (auto simp add: abs_fresh fresh_nat fresh_atm) lemma fresh_subst: fixes z::"name" assumes a: "z♯t⇩_{1}" "z♯t⇩_{2}" shows "z♯t⇩_{1}[y::=t⇩_{2}]" using a by (auto simp add: fresh_subst' abs_fresh) lemma fresh_psubst_simp: assumes "x♯t" shows "((x,u)#θ)<t> = θ<t>" using assms proof (nominal_induct t avoiding: x u θ rule: trm.strong_induct) case (Lam y t x u) have fs: "y♯θ" "y♯x" "y♯u" by fact+ moreover have "x♯ Lam [y].t" by fact ultimately have "x♯t" by (simp add: abs_fresh fresh_atm) moreover have ih:"⋀n T. n♯t ⟹ ((n,T)#θ)<t> = θ<t>" by fact ultimately have "((x,u)#θ)<t> = θ<t>" by auto moreover have "((x,u)#θ)<Lam [y].t> = Lam [y].(((x,u)#θ)<t>)" using fs by (simp add: fresh_list_cons fresh_prod) moreover have " θ<Lam [y].t> = Lam [y]. (θ<t>)" using fs by simp ultimately show "((x,u)#θ)<Lam [y].t> = θ<Lam [y].t>" by auto qed (auto simp add: fresh_atm abs_fresh) lemma forget: fixes x::"name" assumes a: "x♯t" shows "t[x::=t'] = t" using a by (nominal_induct t avoiding: x t' rule: trm.strong_induct) (auto simp add: fresh_atm abs_fresh) lemma subst_fun_eq: fixes u::trm assumes h:"[x].t⇩_{1}= [y].t⇩_{2}" shows "t⇩_{1}[x::=u] = t⇩_{2}[y::=u]" proof - { assume "x=y" and "t⇩_{1}=t⇩_{2}" then have ?thesis using h by simp } moreover { assume h1:"x ≠ y" and h2:"t⇩_{1}=[(x,y)] ∙ t⇩_{2}" and h3:"x ♯ t⇩_{2}" then have "([(x,y)] ∙ t⇩_{2})[x::=u] = t⇩_{2}[y::=u]" by (simp add: subst_rename) then have ?thesis using h2 by simp } ultimately show ?thesis using alpha h by blast qed lemma psubst_empty[simp]: shows "[]<t> = t" by (nominal_induct t rule: trm.strong_induct) (auto simp add: fresh_list_nil) lemma psubst_subst_psubst: assumes h:"c♯θ" shows "θ<t>[c::=s] = ((c,s)#θ)<t>" using h by (nominal_induct t avoiding: θ c s rule: trm.strong_induct) (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst) lemma subst_fresh_simp: assumes a: "x♯θ" shows "θ<Var x> = Var x" using a by (induct θ arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm) lemma psubst_subst_propagate: assumes "x♯θ" shows "θ<t[x::=u]> = θ<t>[x::=θ<u>]" using assms proof (nominal_induct t avoiding: x u θ rule: trm.strong_induct) case (Var n x u θ) { assume "x=n" moreover have "x♯θ" by fact ultimately have "θ<Var n[x::=u]> = θ<Var n>[x::=θ<u>]" using subst_fresh_simp by auto } moreover { assume h:"x≠n" then have "x♯Var n" by (auto simp add: fresh_atm) moreover have "x♯θ" by fact ultimately have "x♯θ<Var n>" using fresh_psubst by blast then have " θ<Var n>[x::=θ<u>] = θ<Var n>" using forget by auto then have "θ<Var n[x::=u]> = θ<Var n>[x::=θ<u>]" using h by auto } ultimately show ?case by auto next case (Lam n t x u θ) have fs:"n♯x" "n♯u" "n♯θ" "x♯θ" by fact+ have ih:"⋀ y s θ. y♯θ ⟹ ((θ<(t[y::=s])>) = ((θ<t>)[y::=(θ<s>)]))" by fact have "θ <(Lam [n].t)[x::=u]> = θ<Lam [n]. (t [x::=u])>" using fs by auto then have "θ <(Lam [n].t)[x::=u]> = Lam [n]. θ<t [x::=u]>" using fs by auto moreover have "θ<t[x::=u]> = θ<t>[x::=θ<u>]" using ih fs by blast ultimately have "θ <(Lam [n].t)[x::=u]> = Lam [n].(θ<t>[x::=θ<u>])" by auto moreover have "Lam [n].(θ<t>[x::=θ<u>]) = (Lam [n].θ<t>)[x::=θ<u>]" using fs fresh_psubst by auto ultimately have "θ<(Lam [n].t)[x::=u]> = (Lam [n].θ<t>)[x::=θ<u>]" using fs by auto then show "θ<(Lam [n].t)[x::=u]> = θ<Lam [n].t>[x::=θ<u>]" using fs by auto qed (auto) section ‹Typing› inductive valid :: "Ctxt ⇒ bool" where v_nil[intro]: "valid []" | v_cons[intro]: "⟦valid Γ;a♯Γ⟧ ⟹ valid ((a,T)#Γ)" equivariance valid inductive_cases valid_cons_elim_auto[elim]:"valid ((x,T)#Γ)" abbreviation "sub_context" :: "Ctxt ⇒ Ctxt ⇒ bool" (" _ ⊆ _ " [55,55] 55) where "Γ⇩_{1}⊆ Γ⇩_{2}≡ ∀a T. (a,T)∈set Γ⇩_{1}⟶ (a,T)∈set Γ⇩_{2}" lemma valid_monotonicity[elim]: fixes Γ Γ' :: Ctxt assumes a: "Γ ⊆ Γ'" and b: "x♯Γ'" shows "(x,T⇩_{1})#Γ ⊆ (x,T⇩_{1})#Γ'" using a b by auto lemma fresh_context: fixes Γ :: "Ctxt" and a :: "name" assumes "a♯Γ" shows "¬(∃τ::ty. (a,τ)∈set Γ)" using assms by (induct Γ) (auto simp add: fresh_prod fresh_list_cons fresh_atm) lemma type_unicity_in_context: assumes a: "valid Γ" and b: "(x,T⇩_{1}) ∈ set Γ" and c: "(x,T⇩_{2}) ∈ set Γ" shows "T⇩_{1}=T⇩_{2}" using a b c by (induct Γ) (auto dest!: fresh_context) inductive typing :: "Ctxt⇒trm⇒ty⇒bool" (" _ ⊢ _ : _ " [60,60,60] 60) where T_Var[intro]: "⟦valid Γ; (x,T)∈set Γ⟧ ⟹ Γ ⊢ Var x : T" | T_App[intro]: "⟦Γ ⊢ e⇩_{1}: T⇩_{1}→T⇩_{2}; Γ ⊢ e⇩_{2}: T⇩_{1}⟧ ⟹ Γ ⊢ App e⇩_{1}e⇩_{2}: T⇩_{2}" | T_Lam[intro]: "⟦x♯Γ; (x,T⇩_{1})#Γ ⊢ t : T⇩_{2}⟧ ⟹ Γ ⊢ Lam [x].t : T⇩_{1}→T⇩_{2}" | T_Const[intro]: "valid Γ ⟹ Γ ⊢ Const n : TBase" | T_Unit[intro]: "valid Γ ⟹ Γ ⊢ Unit : TUnit" equivariance typing nominal_inductive typing by (simp_all add: abs_fresh) lemma typing_implies_valid: assumes a: "Γ ⊢ t : T" shows "valid Γ" using a by (induct) (auto) declare trm.inject [simp add] declare ty.inject [simp add] inductive_cases typing_inv_auto[elim]: "Γ ⊢ Lam [x].t : T" "Γ ⊢ Var x : T" "Γ ⊢ App x y : T" "Γ ⊢ Const n : T" "Γ ⊢ Unit : TUnit" "Γ ⊢ s : TUnit" declare trm.inject [simp del] declare ty.inject [simp del] section ‹Definitional Equivalence› inductive def_equiv :: "Ctxt⇒trm⇒trm⇒ty⇒bool" ("_ ⊢ _ ≡ _ : _" [60,60] 60) where Q_Refl[intro]: "Γ ⊢ t : T ⟹ Γ ⊢ t ≡ t : T" | Q_Symm[intro]: "Γ ⊢ t ≡ s : T ⟹ Γ ⊢ s ≡ t : T" | Q_Trans[intro]: "⟦Γ ⊢ s ≡ t : T; Γ ⊢ t ≡ u : T⟧ ⟹ Γ ⊢ s ≡ u : T" | Q_Abs[intro]: "⟦x♯Γ; (x,T⇩_{1})#Γ ⊢ s⇩_{2}≡ t⇩_{2}: T⇩_{2}⟧ ⟹ Γ ⊢ Lam [x]. s⇩_{2}≡ Lam [x]. t⇩_{2}: T⇩_{1}→ T⇩_{2}" | Q_App[intro]: "⟦Γ ⊢ s⇩_{1}≡ t⇩_{1}: T⇩_{1}→ T⇩_{2}; Γ ⊢ s⇩_{2}≡ t⇩_{2}: T⇩_{1}⟧ ⟹ Γ ⊢ App s⇩_{1}s⇩_{2}≡ App t⇩_{1}t⇩_{2}: T⇩_{2}" | Q_Beta[intro]: "⟦x♯(Γ,s⇩_{2},t⇩_{2}); (x,T⇩_{1})#Γ ⊢ s⇩_{1}≡ t⇩_{1}: T⇩_{2}; Γ ⊢ s⇩_{2}≡ t⇩_{2}: T⇩_{1}⟧ ⟹ Γ ⊢ App (Lam [x]. s⇩_{1}) s⇩_{2}≡ t⇩_{1}[x::=t⇩_{2}] : T⇩_{2}" | Q_Ext[intro]: "⟦x♯(Γ,s,t); (x,T⇩_{1})#Γ ⊢ App s (Var x) ≡ App t (Var x) : T⇩_{2}⟧ ⟹ Γ ⊢ s ≡ t : T⇩_{1}→ T⇩_{2}" | Q_Unit[intro]: "⟦Γ ⊢ s : TUnit; Γ ⊢ t: TUnit⟧ ⟹ Γ ⊢ s ≡ t : TUnit" equivariance def_equiv nominal_inductive def_equiv by (simp_all add: abs_fresh fresh_subst'') lemma def_equiv_implies_valid: assumes a: "Γ ⊢ t ≡ s : T" shows "valid Γ" using a by (induct) (auto elim: typing_implies_valid) section ‹Weak Head Reduction› inductive whr_def :: "trm⇒trm⇒bool" ("_ ↝ _" [80,80] 80) where QAR_Beta[intro]: "App (Lam [x]. t⇩_{1}) t⇩_{2}↝ t⇩_{1}[x::=t⇩_{2}]" | QAR_App[intro]: "t⇩_{1}↝ t⇩_{1}' ⟹ App t⇩_{1}t⇩_{2}↝ App t⇩_{1}' t⇩_{2}" declare trm.inject [simp add] declare ty.inject [simp add] inductive_cases whr_inv_auto[elim]: "t ↝ t'" "Lam [x].t ↝ t'" "App (Lam [x].t12) t2 ↝ t" "Var x ↝ t" "Const n ↝ t" "App p q ↝ t" "t ↝ Const n" "t ↝ Var x" "t ↝ App p q" declare trm.inject [simp del] declare ty.inject [simp del] equivariance whr_def section ‹Weak Head Normalisation› abbreviation nf :: "trm ⇒ bool" ("_ ↝|" [100] 100) where "t↝| ≡ ¬(∃ u. t ↝ u)" inductive whn_def :: "trm⇒trm⇒bool" ("_ ⇓ _" [80,80] 80) where QAN_Reduce[intro]: "⟦s ↝ t; t ⇓ u⟧ ⟹ s ⇓ u" | QAN_Normal[intro]: "t↝| ⟹ t ⇓ t" declare trm.inject[simp] inductive_cases whn_inv_auto[elim]: "t ⇓ t'" declare trm.inject[simp del] equivariance whn_def lemma red_unicity : assumes a: "x ↝ a" and b: "x ↝ b" shows "a=b" using a b apply (induct arbitrary: b) apply (erule whr_inv_auto(3)) apply (clarify) apply (rule subst_fun_eq) apply (simp) apply (force) apply (erule whr_inv_auto(6)) apply (blast)+ done lemma nf_unicity : assumes "x ⇓ a" and "x ⇓ b" shows "a=b" using assms proof (induct arbitrary: b) case (QAN_Reduce x t a b) have h:"x ↝ t" "t ⇓ a" by fact+ have ih:"⋀b. t ⇓ b ⟹ a = b" by fact have "x ⇓ b" by fact then obtain t' where "x ↝ t'" and hl:"t' ⇓ b" using h by auto then have "t=t'" using h red_unicity by auto then show "a=b" using ih hl by auto qed (auto) section ‹Algorithmic Term Equivalence and Algorithmic Path Equivalence› inductive alg_equiv :: "Ctxt⇒trm⇒trm⇒ty⇒bool" ("_ ⊢ _ ⇔ _ : _" [60,60,60,60] 60) and alg_path_equiv :: "Ctxt⇒trm⇒trm⇒ty⇒bool" ("_ ⊢ _ ↔ _ : _" [60,60,60,60] 60) where QAT_Base[intro]: "⟦s ⇓ p; t ⇓ q; Γ ⊢ p ↔ q : TBase⟧ ⟹ Γ ⊢ s ⇔ t : TBase" | QAT_Arrow[intro]: "⟦x♯(Γ,s,t); (x,T⇩_{1})#Γ ⊢ App s (Var x) ⇔ App t (Var x) : T⇩_{2}⟧ ⟹ Γ ⊢ s ⇔ t : T⇩_{1}→ T⇩_{2}" | QAT_One[intro]: "valid Γ ⟹ Γ ⊢ s ⇔ t : TUnit" | QAP_Var[intro]: "⟦valid Γ;(x,T) ∈ set Γ⟧ ⟹ Γ ⊢ Var x ↔ Var x : T" | QAP_App[intro]: "⟦Γ ⊢ p ↔ q : T⇩_{1}→ T⇩_{2}; Γ ⊢ s ⇔ t : T⇩_{1}⟧ ⟹ Γ ⊢ App p s ↔ App q t : T⇩_{2}" | QAP_Const[intro]: "valid Γ ⟹ Γ ⊢ Const n ↔ Const n : TBase" equivariance alg_equiv nominal_inductive alg_equiv avoids QAT_Arrow: x by simp_all declare trm.inject [simp add] declare ty.inject [simp add] inductive_cases alg_equiv_inv_auto[elim]: "Γ ⊢ s⇔t : TBase" "Γ ⊢ s⇔t : T⇩_{1}→ T⇩_{2}" "Γ ⊢ s↔t : TBase" "Γ ⊢ s↔t : TUnit" "Γ ⊢ s↔t : T⇩_{1}→ T⇩_{2}" "Γ ⊢ Var x ↔ t : T" "Γ ⊢ Var x ↔ t : T'" "Γ ⊢ s ↔ Var x : T" "Γ ⊢ s ↔ Var x : T'" "Γ ⊢ Const n ↔ t : T" "Γ ⊢ s ↔ Const n : T" "Γ ⊢ App p s ↔ t : T" "Γ ⊢ s ↔ App q t : T" "Γ ⊢ Lam[x].s ↔ t : T" "Γ ⊢ t ↔ Lam[x].s : T" declare trm.inject [simp del] declare ty.inject [simp del] lemma Q_Arrow_strong_inversion: assumes fs: "x♯Γ" "x♯t" "x♯u" and h: "Γ ⊢ t ⇔ u : T⇩_{1}→T⇩_{2}" shows "(x,T⇩_{1})#Γ ⊢ App t (Var x) ⇔ App u (Var x) : T⇩_{2}" proof - obtain y where fs2: "y♯(Γ,t,u)" and "(y,T⇩_{1})#Γ ⊢ App t (Var y) ⇔ App u (Var y) : T⇩_{2}" using h by auto then have "([(x,y)]∙((y,T⇩_{1})#Γ)) ⊢ [(x,y)]∙ App t (Var y) ⇔ [(x,y)]∙ App u (Var y) : T⇩_{2}" using alg_equiv.eqvt[simplified] by blast then show ?thesis using fs fs2 by (perm_simp) qed (* Warning this lemma is false: lemma algorithmic_type_unicity: shows "⟦ Γ ⊢ s ⇔ t : T ; Γ ⊢ s ⇔ u : T' ⟧ ⟹ T = T'" and "⟦ Γ ⊢ s ↔ t : T ; Γ ⊢ s ↔ u : T' ⟧ ⟹ T = T'" Here is the counter example : Γ ⊢ Const n ⇔ Const n : Tbase and Γ ⊢ Const n ⇔ Const n : TUnit *) lemma algorithmic_path_type_unicity: shows "Γ ⊢ s ↔ t : T ⟹ Γ ⊢ s ↔ u : T' ⟹ T = T'" proof (induct arbitrary: u T' rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _ "%a b c d . True" ]) case (QAP_Var Γ x T u T') have "Γ ⊢ Var x ↔ u : T'" by fact then have "u=Var x" and "(x,T') ∈ set Γ" by auto moreover have "valid Γ" "(x,T) ∈ set Γ" by fact+ ultimately show "T=T'" using type_unicity_in_context by auto next case (QAP_App Γ p q T⇩_{1}T⇩_{2}s t u T⇩_{2}') have ih:"⋀u T. Γ ⊢ p ↔ u : T ⟹ T⇩_{1}→T⇩_{2}= T" by fact have "Γ ⊢ App p s ↔ u : T⇩_{2}'" by fact then obtain r t T⇩_{1}' where "u = App r t" "Γ ⊢ p ↔ r : T⇩_{1}' → T⇩_{2}'" by auto with ih have "T⇩_{1}→T⇩_{2}= T⇩_{1}' → T⇩_{2}'" by auto then show "T⇩_{2}=T⇩_{2}'" using ty.inject by auto qed (auto) lemma alg_path_equiv_implies_valid: shows "Γ ⊢ s ⇔ t : T ⟹ valid Γ" and "Γ ⊢ s ↔ t : T ⟹ valid Γ" by (induct rule : alg_equiv_alg_path_equiv.inducts) auto lemma algorithmic_symmetry: shows "Γ ⊢ s ⇔ t : T ⟹ Γ ⊢ t ⇔ s : T" and "Γ ⊢ s ↔ t : T ⟹ Γ ⊢ t ↔ s : T" by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto simp add: fresh_prod) lemma algorithmic_transitivity: shows "Γ ⊢ s ⇔ t : T ⟹ Γ ⊢ t ⇔ u : T ⟹ Γ ⊢ s ⇔ u : T" and "Γ ⊢ s ↔ t : T ⟹ Γ ⊢ t ↔ u : T ⟹ Γ ⊢ s ↔ u : T" proof (nominal_induct Γ s t T and Γ s t T avoiding: u rule: alg_equiv_alg_path_equiv.strong_inducts) case (QAT_Base s p t q Γ u) have "Γ ⊢ t ⇔ u : TBase" by fact then obtain r' q' where b1: "t ⇓ q'" and b2: "u ⇓ r'" and b3: "Γ ⊢ q' ↔ r' : TBase" by auto have ih: "Γ ⊢ q ↔ r' : TBase ⟹ Γ ⊢ p ↔ r' : TBase" by fact have "t ⇓ q" by fact with b1 have eq: "q=q'" by (simp add: nf_unicity) with ih b3 have "Γ ⊢ p ↔ r' : TBase" by simp moreover have "s ⇓ p" by fact ultimately show "Γ ⊢ s ⇔ u : TBase" using b2 by auto next case (QAT_Arrow x Γ s t T⇩_{1}T⇩_{2}u) have ih:"(x,T⇩_{1})#Γ ⊢ App t (Var x) ⇔ App u (Var x) : T⇩_{2}⟹ (x,T⇩_{1})#Γ ⊢ App s (Var x) ⇔ App u (Var x) : T⇩_{2}" by fact have fs: "x♯Γ" "x♯s" "x♯t" "x♯u" by fact+ have "Γ ⊢ t ⇔ u : T⇩_{1}→T⇩_{2}" by fact then have "(x,T⇩_{1})#Γ ⊢ App t (Var x) ⇔ App u (Var x) : T⇩_{2}" using fs by (simp add: Q_Arrow_strong_inversion) with ih have "(x,T⇩_{1})#Γ ⊢ App s (Var x) ⇔ App u (Var x) : T⇩_{2}" by simp then show "Γ ⊢ s ⇔ u : T⇩_{1}→T⇩_{2}" using fs by (auto simp add: fresh_prod) next case (QAP_App Γ p q T⇩_{1}T⇩_{2}s t u) have "Γ ⊢ App q t ↔ u : T⇩_{2}" by fact then obtain r T⇩_{1}' v where ha: "Γ ⊢ q ↔ r : T⇩_{1}'→T⇩_{2}" and hb: "Γ ⊢ t ⇔ v : T⇩_{1}'" and eq: "u = App r v" by auto have ih1: "Γ ⊢ q ↔ r : T⇩_{1}→T⇩_{2}⟹ Γ ⊢ p ↔ r : T⇩_{1}→T⇩_{2}" by fact have ih2:"Γ ⊢ t ⇔ v : T⇩_{1}⟹ Γ ⊢ s ⇔ v : T⇩_{1}" by fact have "Γ ⊢ p ↔ q : T⇩_{1}→T⇩_{2}" by fact then have "Γ ⊢ q ↔ p : T⇩_{1}→T⇩_{2}" by (simp add: algorithmic_symmetry) with ha have "T⇩_{1}'→T⇩_{2}= T⇩_{1}→T⇩_{2}" using algorithmic_path_type_unicity by simp then have "T⇩_{1}' = T⇩_{1}" by (simp add: ty.inject) then have "Γ ⊢ s ⇔ v : T⇩_{1}" "Γ ⊢ p ↔ r : T⇩_{1}→T⇩_{2}" using ih1 ih2 ha hb by auto then show "Γ ⊢ App p s ↔ u : T⇩_{2}" using eq by auto qed (auto) lemma algorithmic_weak_head_closure: shows "Γ ⊢ s ⇔ t : T ⟹ s' ↝ s ⟹ t' ↝ t ⟹ Γ ⊢ s' ⇔ t' : T" apply (nominal_induct Γ s t T avoiding: s' t' rule: alg_equiv_alg_path_equiv.strong_inducts(1) [of _ _ _ _ "%a b c d e. True"]) apply(auto intro!: QAT_Arrow) done lemma algorithmic_monotonicity: shows "Γ ⊢ s ⇔ t : T ⟹ Γ ⊆ Γ' ⟹ valid Γ' ⟹ Γ' ⊢ s ⇔ t : T" and "Γ ⊢ s ↔ t : T ⟹ Γ ⊆ Γ' ⟹ valid Γ' ⟹ Γ' ⊢ s ↔ t : T" proof (nominal_induct Γ s t T and Γ s t T avoiding: Γ' rule: alg_equiv_alg_path_equiv.strong_inducts) case (QAT_Arrow x Γ s t T⇩_{1}T⇩_{2}Γ') have fs:"x♯Γ" "x♯s" "x♯t" "x♯Γ'" by fact+ have h2:"Γ ⊆ Γ'" by fact have ih:"⋀Γ'. ⟦(x,T⇩_{1})#Γ ⊆ Γ'; valid Γ'⟧ ⟹ Γ' ⊢ App s (Var x) ⇔ App t (Var x) : T⇩_{2}" by fact have "valid Γ'" by fact then have "valid ((x,T⇩_{1})#Γ')" using fs by auto moreover have sub: "(x,T⇩_{1})#Γ ⊆ (x,T⇩_{1})#Γ'" using h2 by auto ultimately have "(x,T⇩_{1})#Γ' ⊢ App s (Var x) ⇔ App t (Var x) : T⇩_{2}" using ih by simp then show "Γ' ⊢ s ⇔ t : T⇩_{1}→T⇩_{2}" using fs by (auto simp add: fresh_prod) qed (auto) lemma path_equiv_implies_nf: assumes "Γ ⊢ s ↔ t : T" shows "s ↝|" and "t ↝|" using assms by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto) section ‹Logical Equivalence› function log_equiv :: "(Ctxt ⇒ trm ⇒ trm ⇒ ty ⇒ bool)" ("_ ⊢ _ is _ : _" [60,60,60,60] 60) where "Γ ⊢ s is t : TUnit = True" | "Γ ⊢ s is t : TBase = Γ ⊢ s ⇔ t : TBase" | "Γ ⊢ s is t : (T⇩_{1}→ T⇩_{2}) = (∀Γ' s' t'. Γ⊆Γ' ⟶ valid Γ' ⟶ Γ' ⊢ s' is t' : T⇩_{1}⟶ (Γ' ⊢ (App s s') is (App t t') : T⇩_{2}))" apply (auto simp add: ty.inject) apply (subgoal_tac "(∃T⇩_{1}T⇩_{2}. b=T⇩_{1}→ T⇩_{2}) ∨ b=TUnit ∨ b=TBase" ) apply (force) apply (rule ty_cases) done termination by lexicographic_order lemma logical_monotonicity: fixes Γ Γ' :: Ctxt assumes a1: "Γ ⊢ s is t : T" and a2: "Γ ⊆ Γ'" and a3: "valid Γ'" shows "Γ' ⊢ s is t : T" using a1 a2 a3 proof (induct arbitrary: Γ' rule: log_equiv.induct) case (2 Γ s t Γ') then show "Γ' ⊢ s is t : TBase" using algorithmic_monotonicity by auto next case (3 Γ s t T⇩_{1}T⇩_{2}Γ') have "Γ ⊢ s is t : T⇩_{1}→T⇩_{2}" and "Γ ⊆ Γ'" and "valid Γ'" by fact+ then show "Γ' ⊢ s is t : T⇩_{1}→T⇩_{2}" by simp qed (auto) lemma main_lemma: shows "Γ ⊢ s is t : T ⟹ valid Γ ⟹ Γ ⊢ s ⇔ t : T" and "Γ ⊢ p ↔ q : T ⟹ Γ ⊢ p is q : T" proof (nominal_induct T arbitrary: Γ s t p q rule: ty.strong_induct) case (Arrow T⇩_{1}T⇩_{2}) { case (1 Γ s t) have ih1:"⋀Γ s t. ⟦Γ ⊢ s is t : T⇩_{2}; valid Γ⟧ ⟹ Γ ⊢ s ⇔ t : T⇩_{2}" by fact have ih2:"⋀Γ s t. Γ ⊢ s ↔ t : T⇩_{1}⟹ Γ ⊢ s is t : T⇩_{1}" by fact have h:"Γ ⊢ s is t : T⇩_{1}→T⇩_{2}" by fact obtain x::name where fs:"x♯(Γ,s,t)" by (erule exists_fresh[OF fs_name1]) have "valid Γ" by fact then have v: "valid ((x,T⇩_{1})#Γ)" using fs by auto then have "(x,T⇩_{1})#Γ ⊢ Var x ↔ Var x : T⇩_{1}" by auto then have "(x,T⇩_{1})#Γ ⊢ Var x is Var x : T⇩_{1}" using ih2 by auto then have "(x,T⇩_{1})#Γ ⊢ App s (Var x) is App t (Var x) : T⇩_{2}" using h v by auto then have "(x,T⇩_{1})#Γ ⊢ App s (Var x) ⇔ App t (Var x) : T⇩_{2}" using ih1 v by auto then show "Γ ⊢ s ⇔ t : T⇩_{1}→T⇩_{2}" using fs by (auto simp add: fresh_prod) next case (2 Γ p q) have h: "Γ ⊢ p ↔ q : T⇩_{1}→T⇩_{2}" by fact have ih1:"⋀Γ s t. Γ ⊢ s ↔ t : T⇩_{2}⟹ Γ ⊢ s is t : T⇩_{2}" by fact have ih2:"⋀Γ s t. ⟦Γ ⊢ s is t : T⇩_{1}; valid Γ⟧ ⟹ Γ ⊢ s ⇔ t : T⇩_{1}" by fact { fix Γ' s t assume "Γ ⊆ Γ'" and hl:"Γ' ⊢ s is t : T⇩_{1}" and hk: "valid Γ'" then have "Γ' ⊢ p ↔ q : T⇩_{1}→ T⇩_{2}" using h algorithmic_monotonicity by auto moreover have "Γ' ⊢ s ⇔ t : T⇩_{1}" using ih2 hl hk by auto ultimately have "Γ' ⊢ App p s ↔ App q t : T⇩_{2}" by auto then have "Γ' ⊢ App p s is App q t : T⇩_{2}" using ih1 by auto } then show "Γ ⊢ p is q : T⇩_{1}→T⇩_{2}" by simp } next case TBase { case 2 have h:"Γ ⊢ s ↔ t : TBase" by fact then have "s ↝|" and "t ↝|" using path_equiv_implies_nf by auto then have "s ⇓ s" and "t ⇓ t" by auto then have "Γ ⊢ s ⇔ t : TBase" using h by auto then show "Γ ⊢ s is t : TBase" by auto } qed (auto elim: alg_path_equiv_implies_valid) corollary corollary_main: assumes a: "Γ ⊢ s ↔ t : T" shows "Γ ⊢ s ⇔ t : T" using a main_lemma alg_path_equiv_implies_valid by blast lemma logical_symmetry: assumes a: "Γ ⊢ s is t : T" shows "Γ ⊢ t is s : T" using a by (nominal_induct arbitrary: Γ s t rule: ty.strong_induct) (auto simp add: algorithmic_symmetry) lemma logical_transitivity: assumes "Γ ⊢ s is t : T" "Γ ⊢ t is u : T" shows "Γ ⊢ s is u : T" using assms proof (nominal_induct arbitrary: Γ s t u rule:ty.strong_induct) case TBase then show "Γ ⊢ s is u : TBase" by (auto elim: algorithmic_transitivity) next case (Arrow T⇩_{1}T⇩_{2}Γ s t u) have h1:"Γ ⊢ s is t : T⇩_{1}→ T⇩_{2}" by fact have h2:"Γ ⊢ t is u : T⇩_{1}→ T⇩_{2}" by fact have ih1:"⋀Γ s t u. ⟦Γ ⊢ s is t : T⇩_{1}; Γ ⊢ t is u : T⇩_{1}⟧ ⟹ Γ ⊢ s is u : T⇩_{1}" by fact have ih2:"⋀Γ s t u. ⟦Γ ⊢ s is t : T⇩_{2}; Γ ⊢ t is u : T⇩_{2}⟧ ⟹ Γ ⊢ s is u : T⇩_{2}" by fact { fix Γ' s' u' assume hsub:"Γ ⊆ Γ'" and hl:"Γ' ⊢ s' is u' : T⇩_{1}" and hk: "valid Γ'" then have "Γ' ⊢ u' is s' : T⇩_{1}" using logical_symmetry by blast then have "Γ' ⊢ u' is u' : T⇩_{1}" using ih1 hl by blast then have "Γ' ⊢ App t u' is App u u' : T⇩_{2}" using h2 hsub hk by auto moreover have "Γ' ⊢ App s s' is App t u' : T⇩_{2}" using h1 hsub hl hk by auto ultimately have "Γ' ⊢ App s s' is App u u' : T⇩_{2}" using ih2 by blast } then show "Γ ⊢ s is u : T⇩_{1}→ T⇩_{2}" by auto qed (auto) lemma logical_weak_head_closure: assumes a: "Γ ⊢ s is t : T" and b: "s' ↝ s" and c: "t' ↝ t" shows "Γ ⊢ s' is t' : T" using a b c algorithmic_weak_head_closure by (nominal_induct arbitrary: Γ s t s' t' rule: ty.strong_induct) (auto, blast) lemma logical_weak_head_closure': assumes "Γ ⊢ s is t : T" and "s' ↝ s" shows "Γ ⊢ s' is t : T" using assms proof (nominal_induct arbitrary: Γ s t s' rule: ty.strong_induct) case (TBase Γ s t s') then show ?case by force next case (TUnit Γ s t s') then show ?case by auto next case (Arrow T⇩_{1}T⇩_{2}Γ s t s') have h1:"s' ↝ s" by fact have ih:"⋀Γ s t s'. ⟦Γ ⊢ s is t : T⇩_{2}; s' ↝ s⟧ ⟹ Γ ⊢ s' is t : T⇩_{2}" by fact have h2:"Γ ⊢ s is t : T⇩_{1}→T⇩_{2}" by fact then have hb:"∀Γ' s' t'. Γ⊆Γ' ⟶ valid Γ' ⟶ Γ' ⊢ s' is t' : T⇩_{1}⟶ (Γ' ⊢ (App s s') is (App t t') : T⇩_{2})" by auto { fix Γ' s⇩_{2}t⇩_{2}assume "Γ ⊆ Γ'" and "Γ' ⊢ s⇩_{2}is t⇩_{2}: T⇩_{1}" and "valid Γ'" then have "Γ' ⊢ (App s s⇩_{2}) is (App t t⇩_{2}) : T⇩_{2}" using hb by auto moreover have "(App s' s⇩_{2}) ↝ (App s s⇩_{2})" using h1 by auto ultimately have "Γ' ⊢ App s' s⇩_{2}is App t t⇩_{2}: T⇩_{2}" using ih by auto } then show "Γ ⊢ s' is t : T⇩_{1}→T⇩_{2}" by auto qed abbreviation log_equiv_for_psubsts :: "Ctxt ⇒ Subst ⇒ Subst ⇒ Ctxt ⇒ bool" ("_ ⊢ _ is _ over _" [60,60] 60) where "Γ' ⊢ θ is θ' over Γ ≡ ∀x T. (x,T) ∈ set Γ ⟶ Γ' ⊢ θ<Var x> is θ'<Var x> : T" lemma logical_pseudo_reflexivity: assumes "Γ' ⊢ t is s over Γ" shows "Γ' ⊢ s is s over Γ" proof - from assms have "Γ' ⊢ s is t over Γ" using logical_symmetry by blast with assms show "Γ' ⊢ s is s over Γ" using logical_transitivity by blast qed lemma logical_subst_monotonicity : fixes Γ Γ' Γ'' :: Ctxt assumes a: "Γ' ⊢ θ is θ' over Γ" and b: "Γ' ⊆ Γ''" and c: "valid Γ''" shows "Γ'' ⊢ θ is θ' over Γ" using a b c logical_monotonicity by blast lemma equiv_subst_ext : assumes h1: "Γ' ⊢ θ is θ' over Γ" and h2: "Γ' ⊢ s is t : T" and fs: "x♯Γ" shows "Γ' ⊢ (x,s)#θ is (x,t)#θ' over (x,T)#Γ" using assms proof - { fix y U assume "(y,U) ∈ set ((x,T)#Γ)" moreover { assume "(y,U) ∈ set [(x,T)]" with h2 have "Γ' ⊢ ((x,s)#θ)<Var y> is ((x,t)#θ')<Var y> : U" by auto } moreover { assume hl:"(y,U) ∈ set Γ" then have "¬ y♯Γ" by (induct Γ) (auto simp add: fresh_list_cons fresh_atm fresh_prod) then have hf:"x♯ Var y" using fs by (auto simp add: fresh_atm) then have "((x,s)#θ)<Var y> = θ<Var y>" "((x,t)#θ')<Var y> = θ'<Var y>" using fresh_psubst_simp by blast+ moreover have "Γ' ⊢ θ<Var y> is θ'<Var y> : U" using h1 hl by auto ultimately have "Γ' ⊢ ((x,s)#θ)<Var y> is ((x,t)#θ')<Var y> : U" by auto } ultimately have "Γ' ⊢ ((x,s)#θ)<Var y> is ((x,t)#θ')<Var y> : U" by auto } then show "Γ' ⊢ (x,s)#θ is (x,t)#θ' over (x,T)#Γ" by auto qed theorem fundamental_theorem_1: assumes a1: "Γ ⊢ t : T" and a2: "Γ' ⊢ θ is θ' over Γ" and a3: "valid Γ'" shows "Γ' ⊢ θ<t> is θ'<t> : T" using a1 a2 a3 proof (nominal_induct Γ t T avoiding: θ θ' arbitrary: Γ' rule: typing.strong_induct) case (T_Lam x Γ T⇩_{1}t⇩_{2}T⇩_{2}θ θ' Γ') have vc: "x♯θ" "x♯θ'" "x♯Γ" by fact+ have asm1: "Γ' ⊢ θ is θ' over Γ" by fact have ih:"⋀θ θ' Γ'. ⟦Γ' ⊢ θ is θ' over (x,T⇩_{1})#Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<t⇩_{2}> is θ'<t⇩_{2}> : T⇩_{2}" by fact show "Γ' ⊢ θ<Lam [x].t⇩_{2}> is θ'<Lam [x].t⇩_{2}> : T⇩_{1}→T⇩_{2}" using vc proof (simp, intro strip) fix Γ'' s' t' assume sub: "Γ' ⊆ Γ''" and asm2: "Γ''⊢ s' is t' : T⇩_{1}" and val: "valid Γ''" from asm1 val sub have "Γ'' ⊢ θ is θ' over Γ" using logical_subst_monotonicity by blast with asm2 vc have "Γ'' ⊢ (x,s')#θ is (x,t')#θ' over (x,T⇩_{1})#Γ" using equiv_subst_ext by blast with ih val have "Γ'' ⊢ ((x,s')#θ)<t⇩_{2}> is ((x,t')#θ')<t⇩_{2}> : T⇩_{2}" by auto with vc have "Γ''⊢θ<t⇩_{2}>[x::=s'] is θ'<t⇩_{2}>[x::=t'] : T⇩_{2}" by (simp add: psubst_subst_psubst) moreover have "App (Lam [x].θ<t⇩_{2}>) s' ↝ θ<t⇩_{2}>[x::=s']" by auto moreover have "App (Lam [x].θ'<t⇩_{2}>) t' ↝ θ'<t⇩_{2}>[x::=t']" by auto ultimately show "Γ''⊢ App (Lam [x].θ<t⇩_{2}>) s' is App (Lam [x].θ'<t⇩_{2}>) t' : T⇩_{2}" using logical_weak_head_closure by auto qed qed (auto) theorem fundamental_theorem_2: assumes h1: "Γ ⊢ s ≡ t : T" and h2: "Γ' ⊢ θ is θ' over Γ" and h3: "valid Γ'" shows "Γ' ⊢ θ<s> is θ'<t> : T" using h1 h2 h3 proof (nominal_induct Γ s t T avoiding: Γ' θ θ' rule: def_equiv.strong_induct) case (Q_Refl Γ t T Γ' θ θ') have "Γ ⊢ t : T" and "valid Γ'" by fact+ moreover have "Γ' ⊢ θ is θ' over Γ" by fact ultimately show "Γ' ⊢ θ<t> is θ'<t> : T" using fundamental_theorem_1 by blast next case (Q_Symm Γ t s T Γ' θ θ') have "Γ' ⊢ θ is θ' over Γ" and "valid Γ'" by fact+ moreover have ih: "⋀ Γ' θ θ'. ⟦Γ' ⊢ θ is θ' over Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<t> is θ'<s> : T" by fact ultimately show "Γ' ⊢ θ<s> is θ'<t> : T" using logical_symmetry by blast next case (Q_Trans Γ s t T u Γ' θ θ') have ih1: "⋀ Γ' θ θ'. ⟦Γ' ⊢ θ is θ' over Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<s> is θ'<t> : T" by fact have ih2: "⋀ Γ' θ θ'. ⟦Γ' ⊢ θ is θ' over Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<t> is θ'<u> : T" by fact have h: "Γ' ⊢ θ is θ' over Γ" and v: "valid Γ'" by fact+ then have "Γ' ⊢ θ' is θ' over Γ" using logical_pseudo_reflexivity by auto then have "Γ' ⊢ θ'<t> is θ'<u> : T" using ih2 v by auto moreover have "Γ' ⊢ θ<s> is θ'<t> : T" using ih1 h v by auto ultimately show "Γ' ⊢ θ<s> is θ'<u> : T" using logical_transitivity by blast next case (Q_Abs x Γ T⇩_{1}s⇩_{2}t⇩_{2}T⇩_{2}Γ' θ θ') have fs:"x♯Γ" by fact have fs2: "x♯θ" "x♯θ'" by fact+ have h2: "Γ' ⊢ θ is θ' over Γ" and h3: "valid Γ'" by fact+ have ih:"⋀Γ' θ θ'. ⟦Γ' ⊢ θ is θ' over (x,T⇩_{1})#Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<s⇩_{2}> is θ'<t⇩_{2}> : T⇩_{2}" by fact { fix Γ'' s' t' assume "Γ' ⊆ Γ''" and hl:"Γ''⊢ s' is t' : T⇩_{1}" and hk: "valid Γ''" then have "Γ'' ⊢ θ is θ' over Γ" using h2 logical_subst_monotonicity by blast then have "Γ'' ⊢ (x,s')#θ is (x,t')#θ' over (x,T⇩_{1})#Γ" using equiv_subst_ext hl fs by blast then have "Γ'' ⊢ ((x,s')#θ)<s⇩_{2}> is ((x,t')#θ')<t⇩_{2}> : T⇩_{2}" using ih hk by blast then have "Γ''⊢ θ<s⇩_{2}>[x::=s'] is θ'<t⇩_{2}>[x::=t'] : T⇩_{2}" using fs2 psubst_subst_psubst by auto moreover have "App (Lam [x]. θ<s⇩_{2}>) s' ↝ θ<s⇩_{2}>[x::=s']" and "App (Lam [x].θ'<t⇩_{2}>) t' ↝ θ'<t⇩_{2}>[x::=t']" by auto ultimately have "Γ'' ⊢ App (Lam [x]. θ<s⇩_{2}>) s' is App (Lam [x].θ'<t⇩_{2}>) t' : T⇩_{2}" using logical_weak_head_closure by auto } moreover have "valid Γ'" by fact ultimately have "Γ' ⊢ Lam [x].θ<s⇩_{2}> is Lam [x].θ'<t⇩_{2}> : T⇩_{1}→T⇩_{2}" by auto then show "Γ' ⊢ θ<Lam [x].s⇩_{2}> is θ'<Lam [x].t⇩_{2}> : T⇩_{1}→T⇩_{2}" using fs2 by auto next case (Q_App Γ s⇩_{1}t⇩_{1}T⇩_{1}T⇩_{2}s⇩_{2}t⇩_{2}Γ' θ θ') then show "Γ' ⊢ θ<App s⇩_{1}s⇩_{2}> is θ'<App t⇩_{1}t⇩_{2}> : T⇩_{2}" by auto next case (Q_Beta x Γ s⇩_{2}t⇩_{2}T⇩_{1}s12 t12 T⇩_{2}Γ' θ θ') have h: "Γ' ⊢ θ is θ' over Γ" and h': "valid Γ'" by fact+ have fs: "x♯Γ" by fact have fs2: " x♯θ" "x♯θ'" by fact+ have ih1: "⋀Γ' θ θ'. ⟦Γ' ⊢ θ is θ' over Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<s⇩_{2}> is θ'<t⇩_{2}> : T⇩_{1}" by fact have ih2: "⋀Γ' θ θ'. ⟦Γ' ⊢ θ is θ' over (x,T⇩_{1})#Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<s12> is θ'<t12> : T⇩_{2}" by fact have "Γ' ⊢ θ<s⇩_{2}> is θ'<t⇩_{2}> : T⇩_{1}" using ih1 h' h by auto then have "Γ' ⊢ (x,θ<s⇩_{2}>)#θ is (x,θ'<t⇩_{2}>)#θ' over (x,T⇩_{1})#Γ" using equiv_subst_ext h fs by blast then have "Γ' ⊢ ((x,θ<s⇩_{2}>)#θ)<s12> is ((x,θ'<t⇩_{2}>)#θ')<t12> : T⇩_{2}" using ih2 h' by auto then have "Γ' ⊢ θ<s12>[x::=θ<s⇩_{2}>] is θ'<t12>[x::=θ'<t⇩_{2}>] : T⇩_{2}" using fs2 psubst_subst_psubst by auto then have "Γ' ⊢ θ<s12>[x::=θ<s⇩_{2}>] is θ'<t12[x::=t⇩_{2}]> : T⇩_{2}" using fs2 psubst_subst_propagate by auto moreover have "App (Lam [x].θ<s12>) (θ<s⇩_{2}>) ↝ θ<s12>[x::=θ<s⇩_{2}>]" by auto ultimately have "Γ' ⊢ App (Lam [x].θ<s12>) (θ<s⇩_{2}>) is θ'<t12[x::=t⇩_{2}]> : T⇩_{2}" using logical_weak_head_closure' by auto then show "Γ' ⊢ θ<App (Lam [x].s12) s⇩_{2}> is θ'<t12[x::=t⇩_{2}]> : T⇩_{2}" using fs2 by simp next case (Q_Ext x Γ s t T⇩_{1}T⇩_{2}Γ' θ θ') have h2: "Γ' ⊢ θ is θ' over Γ" and h2': "valid Γ'" by fact+ have fs:"x♯Γ" "x♯s" "x♯t" by fact+ have ih:"⋀Γ' θ θ'. ⟦Γ' ⊢ θ is θ' over (x,T⇩_{1})#Γ; valid Γ'⟧ ⟹ Γ' ⊢ θ<App s (Var x)> is θ'<App t (Var x)> : T⇩_{2}" by fact { fix Γ'' s' t' assume hsub: "Γ' ⊆ Γ''" and hl: "Γ''⊢ s' is t' : T⇩_{1}" and hk: "valid Γ''" then have "Γ'' ⊢ θ is θ' over Γ" using h2 logical_subst_monotonicity by blast then have "Γ'' ⊢ (x,s')#θ is (x,t')#θ' over (x,T⇩_{1})#Γ" using equiv_subst_ext hl fs by blast then have "Γ'' ⊢ ((x,s')#θ)<App s (Var x)> is ((x,t')#θ')<App t (Var x)> : T⇩_{2}" using ih hk by blast then have "Γ'' ⊢ App (((x,s')#θ)<s>) (((x,s')#θ)<(Var x)>) is App (((x,t')#θ')<t>) (((x,t')#θ')<(Var x)>) : T⇩_{2}" by auto then have "Γ'' ⊢ App ((x,s')#θ)<s> s' is App ((x,t')#θ')<t> t' : T⇩_{2}" by auto then have "Γ'' ⊢ App (θ<s>) s' is App (θ'<t>) t' : T⇩_{2}" using fs fresh_psubst_simp by auto } moreover have "valid Γ'" by fact ultimately show "Γ' ⊢ θ<s> is θ'<t> : T⇩_{1}→T⇩_{2}" by auto next case (Q_Unit Γ s t Γ' θ θ') then show "Γ' ⊢ θ<s> is θ'<t> : TUnit" by auto qed theorem completeness: assumes asm: "Γ ⊢ s ≡ t : T" shows "Γ ⊢ s ⇔ t : T" proof - have val: "valid Γ" using def_equiv_implies_valid asm by simp moreover { fix x T assume "(x,T) ∈ set Γ" "valid Γ" then have "Γ ⊢ Var x is Var x : T" using main_lemma(2) by blast } ultimately have "Γ ⊢ [] is [] over Γ" by auto then have "Γ ⊢ []<s> is []<t> : T" using fundamental_theorem_2 val asm by blast then have "Γ ⊢ s is t : T" by simp then show "Γ ⊢ s ⇔ t : T" using main_lemma(1) val by simp qed text ‹We leave soundness as an exercise - just like Crary in the ATS book :-) \\ @{prop[mode=IfThen] "⟦Γ ⊢ s ⇔ t : T; Γ ⊢ t : T; Γ ⊢ s : T⟧ ⟹ Γ ⊢ s ≡ t : T"} \\ @{prop "⟦Γ ⊢ s ↔ t : T; Γ ⊢ t : T; Γ ⊢ s : T⟧ ⟹ Γ ⊢ s ≡ t : T"} › end