Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)
(* *)
(* 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" ("Var _" [100] 100)
| Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
| App "trm" "trm" ("App _ _" [110,110] 100)
| 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.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.induct) (auto)
instantiation ty :: size
begin
nominal_primrec size_ty
where
"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)+
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 \<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)
nominal_primrec
psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [100,100] 130)
where
"\<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.strong_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.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\<sharp>t" "z\<sharp>\<theta>"
shows "z\<sharp>(\<theta><t>)"
using a
by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_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.strong_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.strong_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.strong_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.strong_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.strong_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.strong_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.strong_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 *}
inductive
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_cases
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]:
fixes \<Gamma> \<Gamma>' :: Ctxt
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)
inductive
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_cases typing_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 *}
inductive
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 *}
inductive
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_cases 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)"
inductive
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_cases 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 *}
inductive
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_cases alg_equiv_inv_auto[elim]:
"\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
"\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
"\<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 by lexicographic_order
lemma logical_monotonicity:
fixes \<Gamma> \<Gamma>' :: Ctxt
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.strong_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.strong_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.strong_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.strong_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.strong_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 :
fixes \<Gamma> \<Gamma>' \<Gamma>'' :: Ctxt
assumes a: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and b: "\<Gamma>' \<subseteq> \<Gamma>''"
and c: "valid \<Gamma>''"
shows "\<Gamma>'' \<turnstile> \<theta> is \<theta>' 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 a1: "\<Gamma> \<turnstile> t : T"
and a2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
and a3: "valid \<Gamma>'"
shows "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T"
using a1 a2 a3
proof (nominal_induct \<Gamma> t T avoiding: \<theta> \<theta>' arbitrary: \<Gamma>' rule: typing.strong_induct)
case (T_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<theta> \<theta>' \<Gamma>')
have vc: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+
have asm1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
have ih:"\<And>\<theta> \<theta>' \<Gamma>'. \<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
show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using vc
proof (simp, intro strip)
fix \<Gamma>'' s' t'
assume sub: "\<Gamma>' \<subseteq> \<Gamma>''"
and asm2: "\<Gamma>''\<turnstile> s' is t' : T\<^isub>1"
and val: "valid \<Gamma>''"
from asm1 val sub have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity by blast
with asm2 vc have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext by blast
with ih val have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<t\<^isub>2> is ((x,t')#\<theta>')<t\<^isub>2> : T\<^isub>2" by auto
with vc have "\<Gamma>''\<turnstile>\<theta><t\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" by (simp add: psubst_subst_psubst)
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 show "\<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
qed
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>'" by fact
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>'" by fact
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