Quelle  Crary.thy   Sprache: Isabelle

(*                                                    *)
(* 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\<^sub>1 T\<^sub>2. T=T\<^sub>1\T\<^sub>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\<^sub>1\T\<^sub>2) = size T\<^sub>1 + size T\<^sub>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: 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: fresh_list_cons)

lemma lookup_fresh':
  assumes a: "z\\"
  shows "lookup \ z = Var z"
using a
by (induct rule: lookup.induct)
   (auto simp: fresh_list_cons fresh_prod fresh_atm)
 
nominal_primrec
  psubst :: "Subst \ trm \ trm"  (‹_<_>› [100,100] 130)
where
  "\<(Var x)> = (lookup \ x)"
| "\<(App t\<^sub>1 t\<^sub>2)> = App \1> \2>"
| "x\\ \ \<(Lam [x].t)> = Lam [x].(\)"
| "\<(Const n)> = Const n"
| "\<(Unit)> = Unit"
  by(finite_guess | simp add: abs_fresh | fresh_guess)+

abbreviation 
 subst :: "trm \ name \ trm \ trm" (‹_[_::=_]› [100,100,100] 100)
where
  "t[x::=t'] \ ([(x,t')])" 

lemma subst[simp]:
  shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
  and   "(App t\<^sub>1 t\<^sub>2)[y::=t'] = App (t\<^sub>1[y::=t']) (t\<^sub>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\<^sub>1"
  shows "t\<^sub>1[a::=t\<^sub>2] = ([(c,a)]\t\<^sub>1)[c::=t\<^sub>2]"
using a
  by (nominal_induct t🚫1 avoiding: a c t🚫2 rule: trm.strong_induct)
     (auto simp: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)

lemma fresh_psubst: 
  fixes z::"name"
  assumes a: "z\t" "z\\"
  shows "z\(\)"
using a
by (nominal_induct t avoiding: z θ t rule: trm.strong_induct)
   (auto simp: abs_fresh lookup_fresh)

lemma fresh_subst'':
  fixes z::"name"
  assumes "z\t\<^sub>2"
  shows "z\t\<^sub>1[z::=t\<^sub>2]"
using assms 
by (nominal_induct t🚫1 avoiding: t🚫2 z rule: trm.strong_induct)
   (auto simp: abs_fresh fresh_nat fresh_atm)

lemma fresh_subst':
  fixes z::"name"
  assumes "z\[y].t\<^sub>1" "z\t\<^sub>2"
  shows "z\t\<^sub>1[y::=t\<^sub>2]"
using assms 
by (nominal_induct t🚫1 avoiding: y t🚫2 z rule: trm.strong_induct)
   (auto simp: abs_fresh fresh_nat fresh_atm)

lemma fresh_subst:
  fixes z::"name"
  assumes a: "z\t\<^sub>1" "z\t\<^sub>2"
  shows "z\t\<^sub>1[y::=t\<^sub>2]"
using a 
by (auto simp: fresh_subst' abs_fresh)

lemma fresh_psubst_simp:
  assumes "x\t"
  shows "((x,u)#\) = \" 
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)#\) = \" by fact
  ultimately have "((x,u)#\) = \" by auto
  moreover have "((x,u)#\) = Lam [y].(((x,u)#\))" using fs 
    by (simp add: fresh_list_cons fresh_prod)
  moreover have " \ = Lam [y]. (\)" using fs by simp
  ultimately show "((x,u)#\) = \" by auto
qed (auto simp: 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: fresh_atm abs_fresh)

lemma subst_fun_eq:
  fixes u::trm
  assumes h:"[x].t\<^sub>1 = [y].t\<^sub>2"
  shows "t\<^sub>1[x::=u] = t\<^sub>2[y::=u]"
proof -
  { 
    assume "x=y" and "t\<^sub>1=t\<^sub>2"
    then have ?thesis using h by simp
  }
  moreover 
  {
    assume h1:"x \ y" and h2:"t\<^sub>1=[(x,y)] \ t\<^sub>2" and h3:"x \ t\<^sub>2"
    then have "([(x,y)] \ t\<^sub>2)[x::=u] = t\<^sub>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"
by (nominal_induct t rule: trm.strong_induct) 
   (auto simp: fresh_list_nil)

lemma psubst_subst_psubst:
  assumes h:"c\\"
  shows "\[c::=s] = ((c,s)#\)"
  using h
by (nominal_induct t avoiding: θ c s rule: trm.strong_induct)
   (auto simp: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)

lemma subst_fresh_simp:
  assumes a: "x\\"
  shows "\ = Var x"
using a
by (induct θ arbitrary: x) (auto simp:fresh_list_cons fresh_prod fresh_atm)

lemma psubst_subst_propagate: 
  assumes "x\\" 
  shows "\ = \[x::=\]"
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 "\ = \[x::=\]" using subst_fresh_simp by auto
  }
  moreover 
  { assume h:"x\n"
    then have "x\Var n" by (auto simp: fresh_atm) 
    moreover have "x\\" by fact
    ultimately have "x\\" using fresh_psubst by blast
    then have " \[x::=\] = \" using forget by auto
    then have "\ = \[x::=\]" 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])>) = ((\)[y::=(\)]))" by fact
  have "\ <(Lam [n].t)[x::=u]> = \" using fs by auto
  then have "\ <(Lam [n].t)[x::=u]> = Lam [n]. \" using fs by auto
  moreover have "\ = \[x::=\]" using ih fs by blast
  ultimately have "\ <(Lam [n].t)[x::=u]> = Lam [n].(\[x::=\])" by auto
  moreover have "Lam [n].(\[x::=\]) = (Lam [n].\)[x::=\]" using fs fresh_psubst by auto
  ultimately have "\<(Lam [n].t)[x::=u]> = (Lam [n].\)[x::=\]" using fs by auto
  then show "\<(Lam [n].t)[x::=u]> = \[x::=\]" 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
  "\\<^sub>1 \ \\<^sub>2 \ \a T. (a,T)\set \\<^sub>1 \ (a,T)\set \\<^sub>2"

lemma valid_monotonicity[elim]:
 fixes Γ Γ' :: Ctxt
 assumes a: "\ \ \'" 
 and     b: "x\\'"
 shows "(x,T\<^sub>1)#\ \ (x,T\<^sub>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: fresh_prod fresh_list_cons fresh_atm)

lemma type_unicity_in_context:
  assumes a: "valid \" 
  and     b: "(x,T\<^sub>1) \ set \" 
  and     c: "(x,T\<^sub>2) \ set \"
  shows "T\<^sub>1=T\<^sub>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\<^sub>1 : T\<^sub>1\T\<^sub>2; \ \ e\<^sub>2 : T\<^sub>1\ \ \ \ App e\<^sub>1 e\<^sub>2 : T\<^sub>2"
| T_Lam[intro]:   "\x\\; (x,T\<^sub>1)#\ \ t : T\<^sub>2\ \ \ \ Lam [x].t : T\<^sub>1\T\<^sub>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\<^sub>1)#\ \ s\<^sub>2 \ t\<^sub>2 : T\<^sub>2\ \ \ \ Lam [x]. s\<^sub>2 \ Lam [x]. t\<^sub>2 : T\<^sub>1 \ T\<^sub>2"
| Q_App[intro]:   "\\ \ s\<^sub>1 \ t\<^sub>1 : T\<^sub>1 \ T\<^sub>2 ; \ \ s\<^sub>2 \ t\<^sub>2 : T\<^sub>1\ \ \ \ App s\<^sub>1 s\<^sub>2 \ App t\<^sub>1 t\<^sub>2 : T\<^sub>2"
| Q_Beta[intro]:  "\x\(\,s\<^sub>2,t\<^sub>2); (x,T\<^sub>1)#\ \ s\<^sub>1 \ t\<^sub>1 : T\<^sub>2 ; \ \ s\<^sub>2 \ t\<^sub>2 : T\<^sub>1\
                   ==>  Γ ⊨ App (Lam [x]. s🚫1) s🚫2 ≡ t🚫1[x::=t🚫2] : T🚫2"
| Q_Ext[intro]:   "\x\(\,s,t); (x,T\<^sub>1)#\ \ App s (Var x) \ App t (Var x) : T\<^sub>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\<^sub>1) t\<^sub>2 \ t\<^sub>1[x::=t\<^sub>2]"
| QAR_App[intro]:  "t\<^sub>1 \ t\<^sub>1' \ App t\<^sub>1 t\<^sub>2 \ App t\<^sub>1' t\<^sub>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
by (induct arbitrary: b) (use subst_fun_eq in blast)+

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
  obtain t' where "x \ t'" and hl:"t' \ b" using h \x \ b\ 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\<^sub>1)#\ \ App s (Var x) \ App t (Var x) : T\<^sub>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\<^sub>1 \ T\<^sub>2; \ \ s \ t : T\<^sub>1\ \ \ \ App p s \ App q t : T\<^sub>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\<^sub>1 \ T\<^sub>2"
  "\ \ s\t : TBase"
  "\ \ s\t : TUnit"
  "\ \ s\t : T\<^sub>1 \ T\<^sub>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\<^sub>1\T\<^sub>2"
  shows "(x,T\<^sub>1)#\ \ App t (Var x) \ App u (Var x) : T\<^sub>2"
proof -
  obtain y where fs2: "y\(\,t,u)" and "(y,T\<^sub>1)#\ \ App t (Var y) \ App u (Var y) : T\<^sub>2" 
    using h by auto
  then have "([(x,y)]\((y,T\<^sub>1)#\)) \ [(x,y)]\ App t (Var y) \ [(x,y)]\ App u (Var y) : T\<^sub>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 "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"

Here is the counter example : 
\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> 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\<^sub>1\T\<^sub>2 = T" by fact
  have "\ \ App p s \ u : T\<^sub>2'" by fact
  then obtain r t T🚫1' where "u = App r t" "\ \ p \ r : T\<^sub>1' → T🚫2'" by auto
  with ih have "T\<^sub>1\T\<^sub>2 = T\<^sub>1' \ T\<^sub>2'" by auto
  then show "T\<^sub>2=T\<^sub>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: 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\<^sub>1)#\ \ App t (Var x) \ App u (Var x) : T\<^sub>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\<^sub>1\T\<^sub>2" by fact
  then have "(x,T\<^sub>1)#\ \ App t (Var x) \ App u (Var x) : T\<^sub>2" using fs 
    by (simp add: Q_Arrow_strong_inversion)
  with ih have "(x,T\<^sub>1)#\ \ App s (Var x) \ App u (Var x) : T\<^sub>2" by simp
  then show "\ \ s \ u : T\<^sub>1\T\<^sub>2" using fs by (auto simp: fresh_prod)
next
  case (QAP_App Γ p q T🚫1 T🚫2 s t u)
  have "\ \ App q t \ u : T\<^sub>2" by fact
  then obtain r T🚫1' v where ha: "\ \ q \ r : T\<^sub>1'→T🚫2" and hb: "Γ ⊨ t ⇔ v : T🚫1'" and eq: "u = App r v"
    by auto
  have ih1: "\ \ q \ r : T\<^sub>1\T\<^sub>2 \ \ \ p \ r : T\<^sub>1\T\<^sub>2" by fact
  have ih2:"\ \ t \ v : T\<^sub>1 \ \ \ s \ v : T\<^sub>1" by fact
  have "\ \ p \ q : T\<^sub>1\T\<^sub>2" by fact
  then have "\ \ q \ p : T\<^sub>1\T\<^sub>2" by (simp add: algorithmic_symmetry)
  with ha have "T\<^sub>1'\T\<^sub>2 = T\<^sub>1\T\<^sub>2" using algorithmic_path_type_unicity by simp
  then have "T\<^sub>1' = T\<^sub>1" by (simp add: ty.inject) 
  then have "\ \ s \ v : T\<^sub>1" "\ \ p \ r : T\<^sub>1\T\<^sub>2" using ih1 ih2 ha hb by auto
  then show "\ \ App p s \ u : T\<^sub>2" using eq by auto
qed (auto)

lemma algorithmic_weak_head_closure:
  shows "\ \ s \ t : T \ s' \ s \ t' \ t \ \ \ s' \ t' : T"
proof (nominal_induct Γ s t T avoiding: s' t'  
    rule: alg_equiv_alg_path_equiv.strong_inducts(1) [of _ _ _ _ "\a b c d e. True"])
qed(auto intro!: QAT_Arrow)

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\<^sub>1)#\ \ \'; valid \'\ \ \' \ App s (Var x) \ App t (Var x) : T\<^sub>2" by fact
  have "valid \'" by fact
  then have "valid ((x,T\<^sub>1)#\')" using fs by auto
  moreover
  have sub: "(x,T\<^sub>1)#\ \ (x,T\<^sub>1)#\'" using h2 by auto
  ultimately have "(x,T\<^sub>1)#\' \ App s (Var x) \ App t (Var x) : T\<^sub>2" using ih by simp
  then show "\' \ s \ t : T\<^sub>1\T\<^sub>2" using fs by (auto simp: 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\<^sub>1 \ T\<^sub>2) =
    (∀Γ' s' t'. \\\' ⟶ valid Γ' \ \' ⊨ s' is t' : T🚫1 ⟶  (Γ' \ (App s s') is (App t t') : T\<^sub>2))"
using ty_cases by (force simp: ty.inject)+

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\<^sub>1\T\<^sub>2" 
  and  "\ \ \'" 
  and  "valid \'" by fact+
  then show "\' \ s is t : T\<^sub>1\T\<^sub>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\<^sub>2; valid \\ \ \ \ s \ t : T\<^sub>2" by fact
    have ih2:"\\ s t. \ \ s \ t : T\<^sub>1 \ \ \ s is t : T\<^sub>1" by fact
    have h:"\ \ s is t : T\<^sub>1\T\<^sub>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\<^sub>1)#\)" using fs by auto
    then have "(x,T\<^sub>1)#\ \ Var x \ Var x : T\<^sub>1" by auto
    then have "(x,T\<^sub>1)#\ \ Var x is Var x : T\<^sub>1" using ih2 by auto
    then have "(x,T\<^sub>1)#\ \ App s (Var x) is App t (Var x) : T\<^sub>2" using h v by auto
    then have "(x,T\<^sub>1)#\ \ App s (Var x) \ App t (Var x) : T\<^sub>2" using ih1 v by auto
    then show "\ \ s \ t : T\<^sub>1\T\<^sub>2" using fs by (auto simp: fresh_prod)
  next
    case (2 Γ p q)
    have h: "\ \ p \ q : T\<^sub>1\T\<^sub>2" by fact
    have ih1:"\\ s t. \ \ s \ t : T\<^sub>2 \ \ \ s is t : T\<^sub>2" by fact
    have ih2:"\\ s t. \\ \ s is t : T\<^sub>1; valid \\ \ \ \ s \ t : T\<^sub>1" by fact
    {
      fix Γ' s t
      assume "\ \ \'" and hl:"\' \ s is t : T\<^sub>1" and hk: "valid \'"
      then have "\' \ p \ q : T\<^sub>1 \ T\<^sub>2" using h algorithmic_monotonicity by auto
      moreover have "\' \ s \ t : T\<^sub>1" using ih2 hl hk by auto
      ultimately have "\' \ App p s \ App q t : T\<^sub>2" by auto
      then have "\' \ App p s is App q t : T\<^sub>2" using ih1 by auto
    }
    then show "\ \ p is q : T\<^sub>1\T\<^sub>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: 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\<^sub>1 \ T\<^sub>2" by fact
  have h2:"\ \ t is u : T\<^sub>1 \ T\<^sub>2" by fact
  have ih1:"\\ s t u. \\ \ s is t : T\<^sub>1; \ \ t is u : T\<^sub>1\ \ \ \ s is u : T\<^sub>1" by fact
  have ih2:"\\ s t u. \\ \ s is t : T\<^sub>2; \ \ t is u : T\<^sub>2\ \ \ \ s is u : T\<^sub>2" by fact
  {
    fix Γ' s' u'
    assume hsub:"\ \ \'" and hl:"\' \ s' is u' : T\<^sub>1" and hk: "valid \'"
    then have "\' \ u' is s' : T\<^sub>1" using logical_symmetry by blast
    then have "\' \ u' is u' : T\<^sub>1" using ih1 hl by blast
    then have "\' \ App t u' is App u u' : T\<^sub>2" using h2 hsub hk by auto
    moreover have "\' \ App s s' is App t u' : T\<^sub>2" using h1 hsub hl hk by auto
    ultimately have "\' \ App s s' is App u u' : T\<^sub>2" using ih2 by blast
  }
  then show "\ \ s is u : T\<^sub>1 \ T\<^sub>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 
proof (nominal_induct arbitrary: Γ s t s' t' rule: ty.strong_induct)
next
  case (Arrow ty1 ty2)
  then show ?case
    by (smt (verit, ccfv_threshold) QAR_App log_equiv.simps(3))
qed auto
   

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\<^sub>2; s' \ s\ \ \ \ s' is t : T\<^sub>2" by fact
  have h2:"\ \ s is t : T\<^sub>1\T\<^sub>2" by fact
  then 
  have hb:"\\' s' t'. \\\' \ valid \' \ \' \ s' is t' : T\<^sub>1 \ (\' \ (App s s') is (App t t') : T\<^sub>2)" 
    by auto
  {
    fix Γ' s\<^sub>2 t\<^sub>2
    assume "\ \ \'" and "\' \ s\<^sub>2 is t\<^sub>2 : T\<^sub>1" and "valid \'"
    then have "\' \ (App s s\<^sub>2) is (App t t\<^sub>2) : T\<^sub>2" using hb by auto
    moreover have "(App s' s\<^sub>2) \ (App s s\<^sub>2)" using h1 by auto  
    ultimately have "\' \ App s' s\<^sub>2 is App t t\<^sub>2 : T\<^sub>2" using ih by auto
  }
  then show "\ \ s' is t : T\<^sub>1\T\<^sub>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 \ \ \' \ \ is \' : T"

lemma logical_pseudo_reflexivity:
  assumes "\' \ t is s over \"
  shows "\' \ s is s over \"
  by (meson assms logical_symmetry logical_transitivity) 

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)#\) is ((x,t)#\') : U" by auto 
    }
    moreover
    {
      assume hl:"(y,U) \ set \"
      then have "\ y\\" by (induct Γ) (auto simp: fresh_list_cons fresh_atm fresh_prod)
      then have hf:"x\ Var y" using fs by (auto simp: fresh_atm)
      then have "((x,s)#\) = \" "((x,t)#\') = \'" 
        using fresh_psubst_simp by blast+ 
      moreover have  "\' \ \ is \' : U" using h1 hl by auto
      ultimately have "\' \ ((x,s)#\) is ((x,t)#\') : U" by auto
    }
    ultimately have "\' \ ((x,s)#\) is ((x,t)#\') : 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 "\' \ \ is \' : 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\<^sub>1)#\; valid \'\ \ \' \ \2> is \'2> : T\<^sub>2" by fact
  show "\' \ \2> is \'2> : T\<^sub>1\T\<^sub>2" using vc
  proof (simp, intro strip)
    fix Γ'' s' t'
    assume sub: "\' \ \''" 
    and    asm2: "\''\ s' is t' : T\<^sub>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\<^sub>1)#\" using equiv_subst_ext by blast
    with ih val have "\'' \ ((x,s')#\)2> is ((x,t')#\')2> : T\<^sub>2" by auto
    with vc have "\''\\2>[x::=s'] is \'2>[x::=t'] : T\<^sub>2" by (simp add: psubst_subst_psubst)
    moreover 
    have "App (Lam [x].\2>) s' \ \2>[x::=s']" by auto
    moreover 
    have "App (Lam [x].\'2>) t' \ \'2>[x::=t']" by auto
    ultimately show "\''\ App (Lam [x].\2>) s' is App (Lam [x].\'2>) t' : T\<^sub>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 "\' \ \ is \' : T"
using h1 h2 h3
proof (nominal_induct Γ s t T avoiding: Γ' \ \' rule: def_equiv.strong_induct)
  case (Q_Refl Γ t T Γ' \ \')
  then show "\' \ \ is \' : T" using fundamental_theorem_1
    by blast
next
  case (Q_Symm Γ t s T Γ' \ \')
  then show "\' \ \ is \' : T" using logical_symmetry by blast
next
  case (Q_Trans Γ s t T u Γ' \ \')
  have ih1: "\ \' \ \'. \\' \ \ is \' over \; valid \'\ \ \' \ \ is \' : T" by fact
  have ih2: "\ \' \ \'. \\' \ \ is \' over \; valid \'\ \ \' \ \ is \' : T" by fact
  have h: "\' \ \ is \' over \" 
  and  v: "valid \'" by fact+
  then have "\' \ \' is \' over \" using logical_pseudo_reflexivity by auto
  then have "\' \ \' is \' : T" using ih2 v by auto
  moreover have "\' \ \ is \' : T" using ih1 h v by auto
  ultimately show "\' \ \ is \' : 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\<^sub>1)#\; valid \'\ \ \' \ \2> is \'2> : T\<^sub>2" by fact
  {
    fix Γ'' s' t'
    assume "\' \ \''" and hl:"\''\ s' is t' : T\<^sub>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\<^sub>1)#\" using equiv_subst_ext hl fs by blast
    then have "\'' \ ((x,s')#\)2> is ((x,t')#\')2> : T\<^sub>2" using ih hk by blast
    then have "\''\ \2>[x::=s'] is \'2>[x::=t'] : T\<^sub>2" using fs2 psubst_subst_psubst by auto
    moreover have "App (Lam [x]. \2>) s' \ \2>[x::=s']" 
              and "App (Lam [x].\'2>) t' \ \'2>[x::=t']" by auto
    ultimately have "\'' \ App (Lam [x]. \2>) s' is App (Lam [x].\'2>) t' : T\<^sub>2" 
      using logical_weak_head_closure by auto
  }
  moreover have "valid \'" by fact
  ultimately have "\' \ Lam [x].\2> is Lam [x].\'2> : T\<^sub>1\T\<^sub>2" by auto
  then show "\' \ \2> is \'2> : T\<^sub>1\T\<^sub>2" using fs2 by auto
next
  case (Q_App Γ s🚫1 t🚫1 T🚫1 T🚫2 s🚫2 t🚫2 Γ' \ \')
  then show "\' \ \1 s\<^sub>2> is \'1 t\<^sub>2> : T\<^sub>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 \'\ \ \' \ \2> is \'2> : T\<^sub>1" by fact
  have ih2: "\\' \ \'. \\' \ \ is \' over (x,T\<^sub>1)#\; valid \'\ \ \' \ \ is \' : T\<^sub>2" by fact
  have "\' \ \2> is \'2> : T\<^sub>1" using ih1 h' h by auto
  then have "\' \ (x,\2>)#\ is (x,\'2>)#\' over (x,T\<^sub>1)#\" using equiv_subst_ext h fs by blast
  then have "\' \ ((x,\2>)#\) is ((x,\'2>)#\') : T\<^sub>2" using ih2 h' by auto
  then have "\' \ \[x::=\2>] is \'[x::=\'2>] : T\<^sub>2" using fs2 psubst_subst_psubst by auto
  then have "\' \ \[x::=\2>] is \'2]> : T\<^sub>2" using fs2 psubst_subst_propagate by auto
  moreover have "App (Lam [x].\) (\2>) \ \[x::=\2>]" by auto 
  ultimately have "\' \ App (Lam [x].\) (\2>) is \'2]> : T\<^sub>2" 
    using logical_weak_head_closure' by auto
  then show "\' \ \2> is \'2]> : T\<^sub>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\<^sub>1)#\; valid \'\
                          ==> Γ' \ \ is \'<App t (Var x)> : T🚫2" by fact
   {
    fix Γ'' s' t'
    assume hsub: "\' \ \''" and hl: "\''\ s' is t' : T\<^sub>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\<^sub>1)#\" using equiv_subst_ext hl fs by blast
    then have "\'' \ ((x,s')#\) is ((x,t')#\') : T\<^sub>2" using ih hk by blast
    then 
    have "\'' \ App (((x,s')#\)) (((x,s')#\)<(Var x)>) is App (((x,t')#\')) (((x,t')#\')<(Var x)>) : T\<^sub>2"
      by auto
    then have "\'' \ App ((x,s')#\) s' is App ((x,t')#\') t' : T\<^sub>2" by auto
    then have "\'' \ App (\) s' is App (\') t' : T\<^sub>2" using fs fresh_psubst_simp by auto
  }
  moreover have "valid \'" by fact
  ultimately show "\' \ \ is \' : T\<^sub>1\T\<^sub>2" by auto
next
  case (Q_Unit Γ s t Γ' \ \')  
  then show "\' \ \ is \' : 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
  then have "\ \ [] is [] over \"
    by (simp add: QAP_Var main_lemma(2)) 
  then have "\ \ [] is [] : 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"} \\
 🍋‹[Γ ⊨ s ↔ t : T; Γ ⊨ t : T; Γ ⊨ s : T] ==> Γ ⊨ s ≡ t : T› 
›

end