(* "$Id$" *)
(* *)
(* 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 "../Nominal"
begin
atom_decl name
nominal_datatype ty =
TBase
| TUnit
| Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
nominal_datatype trm =
Unit
| Var "name"
| Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
| App "trm" "trm"
| Const "nat"
types Ctxt = "(name\<times>ty) list"
types Subst = "(name\<times>trm) list"
lemma perm_ty[simp]:
fixes T::"ty"
and pi::"name prm"
shows "pi\<bullet>T = T"
by (induct T rule: ty.weak_induct) (simp_all)
lemma fresh_ty[simp]:
fixes x::"name"
and T::"ty"
shows "x\<sharp>T"
by (simp add: fresh_def supp_def)
lemma ty_cases:
fixes T::ty
shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
by (induct T rule:ty.weak_induct) (auto)
instance ty :: size ..
nominal_primrec
"size (TBase) = 1"
"size (TUnit) = 1"
"size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
by (rule TrueI)+
lemma ty_size_greater_zero[simp]:
fixes T::"ty"
shows "size T > 0"
by (nominal_induct rule:ty.induct) (simp_all)
section {* Substitutions *}
fun
lookup :: "Subst \<Rightarrow> name \<Rightarrow> trm"
where
"lookup [] x = Var x"
| "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)"
lemma lookup_eqvt[eqvt]:
fixes pi::"name prm"
shows "pi\<bullet>(lookup \<theta> x) = lookup (pi\<bullet>\<theta>) (pi\<bullet>x)"
by (induct \<theta>) (auto simp add: perm_bij)
lemma lookup_fresh:
fixes z::"name"
assumes a: "z\<sharp>\<theta>" "z\<sharp>x"
shows "z\<sharp> lookup \<theta> x"
using a
by (induct rule: lookup.induct)
(auto simp add: fresh_list_cons)
lemma lookup_fresh':
assumes a: "z\<sharp>\<theta>"
shows "lookup \<theta> z = Var z"
using a
by (induct rule: lookup.induct)
(auto simp add: fresh_list_cons fresh_prod fresh_atm)
consts
psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [60,100] 100)
nominal_primrec
"\<theta><(Var x)> = (lookup \<theta> x)"
"\<theta><(App t\<^isub>1 t\<^isub>2)> = App (\<theta><t\<^isub>1>) (\<theta><t\<^isub>2>)"
"x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
"\<theta><(Const n)> = Const n"
"\<theta><(Unit)> = Unit"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)+
apply(fresh_guess)+
done
abbreviation
subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
where
"t[x::=t'] \<equiv> ([(x,t')])<t>"
lemma subst[simp]:
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
and "(App t\<^isub>1 t\<^isub>2)[y::=t'] = App (t\<^isub>1[y::=t']) (t\<^isub>2[y::=t'])"
and "x\<sharp>(y,t') \<Longrightarrow> (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\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
by (nominal_induct t avoiding: x t' rule: trm.induct)
(perm_simp add: fresh_bij)+
lemma subst_rename:
fixes c::"name"
assumes a: "c\<sharp>t\<^isub>1"
shows "t\<^isub>1[a::=t\<^isub>2] = ([(c,a)]\<bullet>t\<^isub>1)[c::=t\<^isub>2]"
using a
apply(nominal_induct t\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.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\<sharp>t" "z\<sharp>\<theta>"
shows "z\<sharp>(\<theta><t>)"
using a
by (nominal_induct t avoiding: z \<theta> t rule: trm.induct)
(auto simp add: abs_fresh lookup_fresh)
lemma fresh_subst'':
fixes z::"name"
assumes "z\<sharp>t\<^isub>2"
shows "z\<sharp>t\<^isub>1[z::=t\<^isub>2]"
using assms
by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.induct)
(auto simp add: abs_fresh fresh_nat fresh_atm)
lemma fresh_subst':
fixes z::"name"
assumes "z\<sharp>[y].t\<^isub>1" "z\<sharp>t\<^isub>2"
shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
using assms
by (nominal_induct t\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.induct)
(auto simp add: abs_fresh fresh_nat fresh_atm)
lemma fresh_subst:
fixes z::"name"
assumes a: "z\<sharp>t\<^isub>1" "z\<sharp>t\<^isub>2"
shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
using a
by (auto simp add: fresh_subst' abs_fresh)
lemma fresh_psubst_simp:
assumes "x\<sharp>t"
shows "(x,u)#\<theta><t> = \<theta><t>"
using assms
proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct)
case (Lam y t x u)
have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+
moreover have "x\<sharp> Lam [y].t" by fact
ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm)
moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact
ultimately have "(x,u)#\<theta><t> = \<theta><t>" by auto
moreover have "(x,u)#\<theta><Lam [y].t> = Lam [y]. ((x,u)#\<theta><t>)" using fs
by (simp add: fresh_list_cons fresh_prod)
moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp
ultimately show "(x,u)#\<theta><Lam [y].t> = \<theta><Lam [y].t>" by auto
qed (auto simp add: fresh_atm abs_fresh)
lemma forget:
fixes x::"name"
assumes a: "x\<sharp>t"
shows "t[x::=t'] = t"
using a
by (nominal_induct t avoiding: x t' rule: trm.induct)
(auto simp add: fresh_atm abs_fresh)
lemma subst_fun_eq:
fixes u::trm
assumes h:"[x].t\<^isub>1 = [y].t\<^isub>2"
shows "t\<^isub>1[x::=u] = t\<^isub>2[y::=u]"
proof -
{
assume "x=y" and "t\<^isub>1=t\<^isub>2"
then have ?thesis using h by simp
}
moreover
{
assume h1:"x \<noteq> y" and h2:"t\<^isub>1=[(x,y)] \<bullet> t\<^isub>2" and h3:"x \<sharp> t\<^isub>2"
then have "([(x,y)] \<bullet> t\<^isub>2)[x::=u] = t\<^isub>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.induct)
(auto simp add: fresh_list_nil)
lemma psubst_subst_psubst:
assumes h:"c\<sharp>\<theta>"
shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>"
using h
by (nominal_induct t avoiding: \<theta> c s rule: trm.induct)
(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
lemma subst_fresh_simp:
assumes a: "x\<sharp>\<theta>"
shows "\<theta><Var x> = Var x"
using a
by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm)
lemma psubst_subst_propagate:
assumes "x\<sharp>\<theta>"
shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]"
using assms
proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct)
case (Var n x u \<theta>)
{ assume "x=n"
moreover have "x\<sharp>\<theta>" by fact
ultimately have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using subst_fresh_simp by auto
}
moreover
{ assume h:"x\<noteq>n"
then have "x\<sharp>Var n" by (auto simp add: fresh_atm)
moreover have "x\<sharp>\<theta>" by fact
ultimately have "x\<sharp>\<theta><Var n>" using fresh_psubst by blast
then have " \<theta><Var n>[x::=\<theta><u>] = \<theta><Var n>" using forget by auto
then have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using h by auto
}
ultimately show ?case by auto
next
case (Lam n t x u \<theta>)
have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact+
have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact
have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto
then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto
moreover have "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" using ih fs by blast
ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto
moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto
ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto
then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto
qed (auto)
section {* Typing *}
inductive2
valid :: "Ctxt \<Rightarrow> bool"
where
v_nil[intro]: "valid []"
| v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,T)#\<Gamma>)"
equivariance valid
inductive_cases2
valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
abbreviation
"sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<subseteq> _ " [55,55] 55)
where
"\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^isub>2"
lemma valid_monotonicity[elim]:
assumes a: "\<Gamma> \<subseteq> \<Gamma>'"
and b: "x\<sharp>\<Gamma>'"
shows "(x,T\<^isub>1)#\<Gamma> \<subseteq> (x,T\<^isub>1)#\<Gamma>'"
using a b by auto
lemma fresh_context:
fixes \<Gamma> :: "Ctxt"
and a :: "name"
assumes "a\<sharp>\<Gamma>"
shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
using assms
by (induct \<Gamma>)
(auto simp add: fresh_prod fresh_list_cons fresh_atm)
lemma type_unicity_in_context:
assumes a: "valid \<Gamma>"
and b: "(x,T\<^isub>1) \<in> set \<Gamma>"
and c: "(x,T\<^isub>2) \<in> set \<Gamma>"
shows "T\<^isub>1=T\<^isub>2"
using a b c
by (induct \<Gamma>)
(auto dest!: fresh_context)
inductive2
typing :: "Ctxt\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60)
where
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2"
| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
| t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
| t_Unit[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
equivariance typing
nominal_inductive typing
by (simp_all add: abs_fresh)
lemma typing_implies_valid:
assumes a: "\<Gamma> \<turnstile> t : T"
shows "valid \<Gamma>"
using a by (induct) (auto)
declare trm.inject [simp add]
declare ty.inject [simp add]
inductive_cases2 t_inv_auto[elim]:
"\<Gamma> \<turnstile> Lam [x].t : T"
"\<Gamma> \<turnstile> Var x : T"
"\<Gamma> \<turnstile> App x y : T"
"\<Gamma> \<turnstile> Const n : T"
"\<Gamma> \<turnstile> Unit : TUnit"
"\<Gamma> \<turnstile> s : TUnit"
declare trm.inject [simp del]
declare ty.inject [simp del]
section {* Definitional Equivalence *}
inductive2
def_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60)
where
Q_Refl[intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<equiv> t : T"
| Q_Symm[intro]: "\<Gamma> \<turnstile> t \<equiv> s : T \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"
| Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s \<equiv> t : T; \<Gamma> \<turnstile> t \<equiv> u : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> u : T"
| Q_Abs[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s\<^isub>2 \<equiv> Lam [x]. t\<^isub>2 : T\<^isub>1 \<rightarrow> T\<^isub>2"
| Q_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> s\<^isub>1 \<equiv> t\<^isub>1 : T\<^isub>1 \<rightarrow> T\<^isub>2 ; \<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App s\<^isub>1 s\<^isub>2 \<equiv> App t\<^isub>1 t\<^isub>2 : T\<^isub>2"
| Q_Beta[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s\<^isub>2,t\<^isub>2); (x,T\<^isub>1)#\<Gamma> \<turnstile> s\<^isub>1 \<equiv> t\<^isub>1 : T\<^isub>2 ; \<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1\<rbrakk>
\<Longrightarrow> \<Gamma> \<turnstile> App (Lam [x]. s\<^isub>1) s\<^isub>2 \<equiv> t\<^isub>1[x::=t\<^isub>2] : T\<^isub>2"
| Q_Ext[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2\<rbrakk>
\<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
| Q_Unit[intro]: "\<lbrakk>\<Gamma> \<turnstile> s : TUnit; \<Gamma> \<turnstile> t: TUnit\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : TUnit"
equivariance def_equiv
nominal_inductive def_equiv
by (simp_all add: abs_fresh fresh_subst'')
lemma def_equiv_implies_valid:
assumes a: "\<Gamma> \<turnstile> t \<equiv> s : T"
shows "valid \<Gamma>"
using a by (induct) (auto elim: typing_implies_valid)
section {* Weak Head Reduction *}
inductive2
whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80)
where
QAR_Beta[intro]: "App (Lam [x]. t\<^isub>1) t\<^isub>2 \<leadsto> t\<^isub>1[x::=t\<^isub>2]"
| QAR_App[intro]: "t\<^isub>1 \<leadsto> t\<^isub>1' \<Longrightarrow> App t\<^isub>1 t\<^isub>2 \<leadsto> App t\<^isub>1' t\<^isub>2"
declare trm.inject [simp add]
declare ty.inject [simp add]
inductive_cases2 whr_inv_auto[elim]:
"t \<leadsto> t'"
"Lam [x].t \<leadsto> t'"
"App (Lam [x].t12) t2 \<leadsto> t"
"Var x \<leadsto> t"
"Const n \<leadsto> t"
"App p q \<leadsto> t"
"t \<leadsto> Const n"
"t \<leadsto> Var x"
"t \<leadsto> App p q"
declare trm.inject [simp del]
declare ty.inject [simp del]
equivariance whr_def
section {* Weak Head Normalisation *}
abbreviation
nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100)
where
"t\<leadsto>| \<equiv> \<not>(\<exists> u. t \<leadsto> u)"
inductive2
whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
where
QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u"
| QAN_Normal[intro]: "t\<leadsto>| \<Longrightarrow> t \<Down> t"
declare trm.inject[simp]
inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'"
declare trm.inject[simp del]
lemma whn_eqvt[eqvt]:
fixes pi::"name prm"
assumes a: "t \<Down> t'"
shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
using a
apply(induct)
apply(rule QAN_Reduce)
apply(rule whr_def.eqvt)
apply(assumption)+
apply(rule QAN_Normal)
apply(auto)
apply(drule_tac pi="rev pi" in whr_def.eqvt)
apply(perm_simp)
done
lemma red_unicity :
assumes a: "x \<leadsto> a"
and b: "x \<leadsto> 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 \<Down> a" and "x \<Down> b"
shows "a=b"
using assms
proof (induct arbitrary: b)
case (QAN_Reduce x t a b)
have h:"x \<leadsto> t" "t \<Down> a" by fact+
have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact
have "x \<Down> b" by fact
then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> 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 *}
inductive2
alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60,60,60] 60)
and
alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60,60,60] 60)
where
QAT_Base[intro]: "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
| QAT_Arrow[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2\<rbrakk>
\<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
| QAT_One[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TUnit"
| QAP_Var[intro]: "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T"
| QAP_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2"
| QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> 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_cases2 alg_equiv_inv_auto[elim]:
"\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
"\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
inductive_cases2 alg_path_equiv_inv_auto[elim]:
"\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
"\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
"\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
"\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
"\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
"\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
"\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
"\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
"\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
"\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
"\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
"\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
"\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
declare trm.inject [simp del]
declare ty.inject [simp del]
lemma Q_Arrow_strong_inversion:
assumes fs: "x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u"
and h: "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2"
shows "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2"
proof -
obtain y where fs2: "y\<sharp>(\<Gamma>,t,u)" and "(y,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>2"
using h by auto
then have "([(x,y)]\<bullet>((y,T\<^isub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^isub>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 "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<Longrightarrow> T = T'"
proof (induct arbitrary: u T'
rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _ "%a b c d . True" ])
case (QAP_Var \<Gamma> x T u T')
have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact+
ultimately show "T=T'" using type_unicity_in_context by auto
next
case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u T\<^isub>2')
have ih: "\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2'" by fact
then obtain r t T\<^isub>1' where "u = App r t" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
with ih have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
then show "T\<^isub>2=T\<^isub>2'" using ty.inject by auto
qed (auto)
lemma alg_path_equiv_implies_valid:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
by (induct rule : alg_equiv_alg_path_equiv.inducts, auto)
lemma algorithmic_symmetry:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T"
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T"
by (induct rule: alg_equiv_alg_path_equiv.inducts)
(auto simp add: fresh_prod)
lemma algorithmic_transitivity:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T"
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T"
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv.strong_inducts)
case (QAT_Base s p t q \<Gamma> u)
have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : TBase" by fact
then obtain r' q' where b1: "t \<Down> q'" and b2: "u \<Down> r'" and b3: "\<Gamma> \<turnstile> q' \<leftrightarrow> r' : TBase" by auto
have ih: "\<Gamma> \<turnstile> q \<leftrightarrow> r' : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by fact
have "t \<Down> q" by fact
with b1 have eq: "q=q'" by (simp add: nf_unicity)
with ih b3 have "\<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by simp
moreover
have "s \<Down> p" by fact
ultimately show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : TBase" using b2 by auto
next
case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 u)
have ih:"(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2
\<Longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by fact
have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact+
have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" using fs
by (simp add: Q_Arrow_strong_inversion)
with ih have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by simp
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
next
case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u)
have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^isub>2" by fact
then obtain r T\<^isub>1' v where ha: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^isub>1'\<rightarrow>T\<^isub>2" and hb: "\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^isub>1'" and eq: "u = App r v"
by auto
have ih1: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^isub>1\<rightarrow>T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
have ih2:"\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^isub>1" by fact
have "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
then have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^isub>1\<rightarrow>T\<^isub>2" by (simp add: algorithmic_symmetry)
with ha have "T\<^isub>1'\<rightarrow>T\<^isub>2 = T\<^isub>1\<rightarrow>T\<^isub>2" using algorithmic_path_type_unicity by simp
then have "T\<^isub>1' = T\<^isub>1" by (simp add: ty.inject)
then have "\<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^isub>1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1\<rightarrow>T\<^isub>2" using ih1 ih2 ha hb by auto
then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2" using eq by auto
qed (auto)
lemma algorithmic_weak_head_closure:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> s' \<leadsto> s \<Longrightarrow> t' \<leadsto> t \<Longrightarrow> \<Gamma> \<turnstile> s' \<Leftrightarrow> t' : T"
apply (nominal_induct \<Gamma> 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 "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts)
case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact+
have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact
have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
have "valid \<Gamma>'" by fact
then have "valid ((x,T\<^isub>1)#\<Gamma>')" using fs by auto
moreover
have sub: "(x,T\<^isub>1)#\<Gamma> \<subseteq> (x,T\<^isub>1)#\<Gamma>'" using h2 by auto
ultimately have "(x,T\<^isub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih by simp
then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
qed (auto)
lemma path_equiv_implies_nf:
assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
shows "s \<leadsto>|" and "t \<leadsto>|"
using assms
by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto)
section {* Logical Equivalence *}
function log_equiv :: "(Ctxt \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)" ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60)
where
"\<Gamma> \<turnstile> s is t : TUnit = True"
| "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
| "\<Gamma> \<turnstile> s is t : (T\<^isub>1 \<rightarrow> T\<^isub>2) =
(\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2))"
apply (auto simp add: ty.inject)
apply (subgoal_tac "(\<exists>T\<^isub>1 T\<^isub>2. b=T\<^isub>1 \<rightarrow> T\<^isub>2) \<or> b=TUnit \<or> b=TBase" )
apply (force)
apply (rule ty_cases)
done
termination
apply(relation "measure (\<lambda>(_,_,_,T). size T)")
apply(auto)
done
lemma logical_monotonicity :
assumes a1: "\<Gamma> \<turnstile> s is t : T"
and a2: "\<Gamma> \<subseteq> \<Gamma>'"
and a3: "valid \<Gamma>'"
shows "\<Gamma>' \<turnstile> s is t : T"
using a1 a2 a3
proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct)
case (2 \<Gamma> s t \<Gamma>')
then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto
next
case (3 \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
have "\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2"
and "\<Gamma> \<subseteq> \<Gamma>'"
and "valid \<Gamma>'" by fact+
then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by simp
qed (auto)
lemma main_lemma:
shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T"
proof (nominal_induct T arbitrary: \<Gamma> s t p q rule: ty.induct)
case (Arrow T\<^isub>1 T\<^isub>2)
{
case (1 \<Gamma> s t)
have ih1:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>2" by fact
have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^isub>1" by fact
have h:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1])
have "valid \<Gamma>" by fact
then have v: "valid ((x,T\<^isub>1)#\<Gamma>)" using fs by auto
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T\<^isub>1" by auto
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x is Var x : T\<^isub>1" using ih2 by auto
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T\<^isub>2" using h v by auto
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih1 v by auto
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
next
case (2 \<Gamma> p q)
have h: "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^isub>2" by fact
have ih2:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>1; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact
{
fix \<Gamma>' s t
assume "\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^isub>1" and hk: "valid \<Gamma>'"
then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2" using h algorithmic_monotonicity by auto
moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" using ih2 hl hk by auto
ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2" by auto
then have "\<Gamma>' \<turnstile> App p s is App q t : T\<^isub>2" using ih1 by auto
}
then show "\<Gamma> \<turnstile> p is q : T\<^isub>1\<rightarrow>T\<^isub>2" by simp
}
next
case TBase
{ case 2
have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact
then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto
then have "s \<Down> s" and "t \<Down> t" by auto
then have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" using h by auto
then show "\<Gamma> \<turnstile> s is t : TBase" by auto
}
qed (auto elim: alg_path_equiv_implies_valid)
corollary corollary_main:
assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
using a main_lemma alg_path_equiv_implies_valid by blast
lemma logical_symmetry:
assumes a: "\<Gamma> \<turnstile> s is t : T"
shows "\<Gamma> \<turnstile> t is s : T"
using a
by (nominal_induct arbitrary: \<Gamma> s t rule: ty.induct)
(auto simp add: algorithmic_symmetry)
lemma logical_transitivity:
assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T"
shows "\<Gamma> \<turnstile> s is u : T"
using assms
proof (nominal_induct arbitrary: \<Gamma> s t u rule:ty.induct)
case TBase
then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim: algorithmic_transitivity)
next
case (Arrow T\<^isub>1 T\<^isub>2 \<Gamma> s t u)
have h1:"\<Gamma> \<turnstile> s is t : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact
have h2:"\<Gamma> \<turnstile> t is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact
have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>1; \<Gamma> \<turnstile> t is u : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^isub>1" by fact
have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; \<Gamma> \<turnstile> t is u : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^isub>2" by fact
{
fix \<Gamma>' s' u'
assume hsub:"\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^isub>1" and hk: "valid \<Gamma>'"
then have "\<Gamma>' \<turnstile> u' is s' : T\<^isub>1" using logical_symmetry by blast
then have "\<Gamma>' \<turnstile> u' is u' : T\<^isub>1" using ih1 hl by blast
then have "\<Gamma>' \<turnstile> App t u' is App u u' : T\<^isub>2" using h2 hsub hk by auto
moreover have "\<Gamma>' \<turnstile> App s s' is App t u' : T\<^isub>2" using h1 hsub hl hk by auto
ultimately have "\<Gamma>' \<turnstile> App s s' is App u u' : T\<^isub>2" using ih2 by blast
}
then show "\<Gamma> \<turnstile> s is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
qed (auto)
lemma logical_weak_head_closure:
assumes a: "\<Gamma> \<turnstile> s is t : T"
and b: "s' \<leadsto> s"
and c: "t' \<leadsto> t"
shows "\<Gamma> \<turnstile> s' is t' : T"
using a b c algorithmic_weak_head_closure
by (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.induct)
(auto, blast)
lemma logical_weak_head_closure':
assumes "\<Gamma> \<turnstile> s is t : T" and "s' \<leadsto> s"
shows "\<Gamma> \<turnstile> s' is t : T"
using assms
proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.induct)
case (TBase \<Gamma> s t s')
then show ?case by force
next
case (TUnit \<Gamma> s t s')
then show ?case by auto
next
case (Arrow T\<^isub>1 T\<^isub>2 \<Gamma> s t s')
have h1:"s' \<leadsto> s" by fact
have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T\<^isub>2" by fact
have h2:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
then
have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2)"
by auto
{
fix \<Gamma>' s\<^isub>2 t\<^isub>2
assume "\<Gamma> \<subseteq> \<Gamma>'" and "\<Gamma>' \<turnstile> s\<^isub>2 is t\<^isub>2 : T\<^isub>1" and "valid \<Gamma>'"
then have "\<Gamma>' \<turnstile> (App s s\<^isub>2) is (App t t\<^isub>2) : T\<^isub>2" using hb by auto
moreover have "(App s' s\<^isub>2) \<leadsto> (App s s\<^isub>2)" using h1 by auto
ultimately have "\<Gamma>' \<turnstile> App s' s\<^isub>2 is App t t\<^isub>2 : T\<^isub>2" using ih by auto
}
then show "\<Gamma> \<turnstile> s' is t : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
qed
abbreviation
log_equiv_for_psubsts :: "Ctxt \<Rightarrow> Subst \<Rightarrow> Subst \<Rightarrow> Ctxt \<Rightarrow> bool" ("_ \<turnstile> _ is _ over _" [60,60] 60)
where
"\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma> \<equiv> \<forall>x T. (x,T) \<in> set \<Gamma> \<longrightarrow> \<Gamma>' \<turnstile> \<theta><Var x> is \<theta>'<Var x> : T"
lemma logical_pseudo_reflexivity:
assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>"
shows "\<Gamma>' \<turnstile> s is s over \<Gamma>"
proof -
have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact
moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
qed
lemma logical_subst_monotonicity :
assumes a: "\<Gamma>' \<turnstile> s is t over \<Gamma>"
and b: "\<Gamma>' \<subseteq> \<Gamma>''"
and c: "valid \<Gamma>''"
shows "\<Gamma>'' \<turnstile> s is t over \<Gamma>"
using a b c logical_monotonicity by blast
lemma equiv_subst_ext :
assumes h1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and h2: "\<Gamma>' \<turnstile> s is t : T"
and fs: "x\<sharp>\<Gamma>"
shows "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>"
using assms
proof -
{
fix y U
assume "(y,U) \<in> set ((x,T)#\<Gamma>)"
moreover
{
assume "(y,U) \<in> set [(x,T)]"
with h2 have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
}
moreover
{
assume hl:"(y,U) \<in> set \<Gamma>"
then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_atm fresh_prod)
then have hf:"x\<sharp> Var y" using fs by (auto simp add: fresh_atm)
then have "(x,s)#\<theta><Var y> = \<theta><Var y>" "(x,t)#\<theta>'<Var y> = \<theta>'<Var y>" using fresh_psubst_simp by blast+
moreover have "\<Gamma>' \<turnstile> \<theta><Var y> is \<theta>'<Var y> : U" using h1 hl by auto
ultimately have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
}
ultimately have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
}
then show "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" by auto
qed
theorem fundamental_theorem_1:
assumes h1: "\<Gamma> \<turnstile> t : T"
and h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and h3: "valid \<Gamma>'"
shows "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T"
using h1 h2 h3
proof (nominal_induct \<Gamma> t T avoiding: \<Gamma>' \<theta> \<theta>' rule: typing.strong_induct)
case (t_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
have fs:"x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+
have h:"\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
have ih:"\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
{
fix \<Gamma>'' s' t'
assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and v: "valid \<Gamma>''"
then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity h by blast
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><t\<^isub>2> is (x,t')#\<theta>'<t\<^isub>2> : T\<^isub>2" using ih v by auto
then have "\<Gamma>''\<turnstile>\<theta><t\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" using psubst_subst_psubst fs by simp
moreover have "App (Lam [x].\<theta><t\<^isub>2>) s' \<leadsto> \<theta><t\<^isub>2>[x::=s']" by auto
moreover have "App (Lam [x].\<theta>'<t\<^isub>2>) t' \<leadsto> \<theta>'<t\<^isub>2>[x::=t']" by auto
ultimately have "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2"
using logical_weak_head_closure by auto
}
then show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by simp
qed (auto)
theorem fundamental_theorem_2:
assumes h1: "\<Gamma> \<turnstile> s \<equiv> t : T"
and h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and h3: "valid \<Gamma>'"
shows "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T"
using h1 h2 h3
proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<theta> \<theta>' rule: def_equiv.strong_induct)
case (Q_Refl \<Gamma> t T \<Gamma>' \<theta> \<theta>')
have "\<Gamma> \<turnstile> t : T"
and "valid \<Gamma>'" by fact+
moreover
have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
ultimately show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1 by blast
next
case (Q_Symm \<Gamma> t s T \<Gamma>' \<theta> \<theta>')
have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and "valid \<Gamma>'" by fact+
moreover
have ih: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<s> : T" by fact
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast
next
case (Q_Trans \<Gamma> s t T u \<Gamma>' \<theta> \<theta>')
have ih1: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" by fact
have ih2: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<u> : T" by fact
have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and v: "valid \<Gamma>'" by fact+
then have "\<Gamma>' \<turnstile> \<theta>' is \<theta>' over \<Gamma>" using logical_pseudo_reflexivity by auto
then have "\<Gamma>' \<turnstile> \<theta>'<t> is \<theta>'<u> : T" using ih2 v by auto
moreover have "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using ih1 h v by auto
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<u> : T" using logical_transitivity by blast
next
case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
have fs:"x\<sharp>\<Gamma>" by fact
have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and h3: "valid \<Gamma>'" by fact+
have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
{
fix \<Gamma>'' s' t'
assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><s\<^isub>2> is (x,t')#\<theta>'<t\<^isub>2> : T\<^isub>2" using ih hk by blast
then have "\<Gamma>''\<turnstile> \<theta><s\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
moreover have "App (Lam [x]. \<theta><s\<^isub>2>) s' \<leadsto> \<theta><s\<^isub>2>[x::=s']"
and "App (Lam [x].\<theta>'<t\<^isub>2>) t' \<leadsto> \<theta>'<t\<^isub>2>[x::=t']" by auto
ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2"
using logical_weak_head_closure by auto
}
moreover have "valid \<Gamma>'" using h3 by auto
ultimately have "\<Gamma>' \<turnstile> Lam [x].\<theta><s\<^isub>2> is Lam [x].\<theta>'<t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs2 by auto
next
case (Q_App \<Gamma> s\<^isub>1 t\<^isub>1 T\<^isub>1 T\<^isub>2 s\<^isub>2 t\<^isub>2 \<Gamma>' \<theta> \<theta>')
then show "\<Gamma>' \<turnstile> \<theta><App s\<^isub>1 s\<^isub>2> is \<theta>'<App t\<^isub>1 t\<^isub>2> : T\<^isub>2" by auto
next
case (Q_Beta x \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1 s12 t12 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and h': "valid \<Gamma>'" by fact+
have fs: "x\<sharp>\<Gamma>" by fact
have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
have ih1: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" by fact
have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^isub>2" by fact
have "\<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" using ih1 h' h by auto
then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^isub>2>)#\<theta> is (x,\<theta>'<t\<^isub>2>)#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext h fs by blast
then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^isub>2>)#\<theta><s12> is (x,\<theta>'<t\<^isub>2>)#\<theta>'<t12> : T\<^isub>2" using ih2 h' by auto
then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^isub>2>] is \<theta>'<t12>[x::=\<theta>'<t\<^isub>2>] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^isub>2>] is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 psubst_subst_propagate by auto
moreover have "App (Lam [x].\<theta><s12>) (\<theta><s\<^isub>2>) \<leadsto> \<theta><s12>[x::=\<theta><s\<^isub>2>]" by auto
ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<theta><s12>) (\<theta><s\<^isub>2>) is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2"
using logical_weak_head_closure' by auto
then show "\<Gamma>' \<turnstile> \<theta><App (Lam [x].s12) s\<^isub>2> is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 by simp
next
case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and h2': "valid \<Gamma>'" by fact+
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact+
have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk>
\<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^isub>2" by fact
{
fix \<Gamma>'' s' t'
assume hsub: "\<Gamma>' \<subseteq> \<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><App s (Var x)> is (x,t')#\<theta>'<App t (Var x)> : T\<^isub>2" using ih hk by blast
then
have "\<Gamma>'' \<turnstile> App (((x,s')#\<theta>)<s>) (((x,s')#\<theta>)<(Var x)>) is App ((x,t')#\<theta>'<t>) ((x,t')#\<theta>'<(Var x)>) : T\<^isub>2"
by auto
then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta><s>) s' is App ((x,t')#\<theta>'<t>) t' : T\<^isub>2" by auto
then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^isub>2" using fs fresh_psubst_simp by auto
}
moreover have "valid \<Gamma>'" using h2' by auto
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
next
case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>')
then show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : TUnit" by auto
qed
theorem completeness:
assumes asm: "\<Gamma> \<turnstile> s \<equiv> t : T"
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
proof -
have val: "valid \<Gamma>" using def_equiv_implies_valid asm by simp
moreover
{
fix x T
assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>"
then have "\<Gamma> \<turnstile> Var x is Var x : T" using main_lemma(2) by blast
}
ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto
then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 val asm by blast
then have "\<Gamma> \<turnstile> s is t : T" by simp
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp
qed
text {* We leave soundness as an exercise - like in the book :-) \\
@{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\
@{prop "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"}
*}
end