# Theory Crary

theory Crary
imports Nominal
```(*                                                    *)
(* 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"

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)

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(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"

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)

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)

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
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)

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)

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

lemma typing_implies_valid:
assumes a: "Γ ⊢ t : T"
shows "valid Γ"
using a by (induct) (auto)

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

lemma def_equiv_implies_valid:
assumes a: "Γ ⊢ t ≡ s : T"
shows "valid Γ"
using a by (induct) (auto elim: typing_implies_valid)

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"

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

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

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)

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
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)

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 (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)

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)

assumes a: "Γ ⊢ s is t : T"
and     b: "s' ↝ s"
and     c: "t' ↝ t"
shows "Γ ⊢ s' is t' : T"
by (nominal_induct arbitrary: Γ s t s' t' rule: ty.strong_induct)
(auto, blast)

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"
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"
}
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"
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

```