theory SN
imports Lam_Funs
begin
text \<open>Strong Normalisation proof from the Proofs and Types book\<close>
section \<open>Beta Reduction\<close>
lemma subst_rename:
assumes a: "c\t1"
shows "t1[a::=t2] = ([(c,a)]\t1)[c::=t2]"
using a
by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
(auto simp add: calc_atm fresh_atm abs_fresh)
lemma forget:
assumes a: "a\t1"
shows "t1[a::=t2] = t1"
using a
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_atm)
lemma fresh_fact:
fixes a::"name"
assumes a: "a\t1" "a\t2"
shows "a\t1[b::=t2]"
using a
by (nominal_induct t1 avoiding: a b t2 rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_atm)
lemma fresh_fact':
fixes a::"name"
assumes a: "a\t2"
shows "a\t1[a::=t2]"
using a
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_atm)
lemma subst_lemma:
assumes a: "x\y"
and b: "x\L"
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a b
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
(auto simp add: fresh_fact forget)
lemma id_subs:
shows "t[x::=Var x] = t"
by (nominal_induct t avoiding: x rule: lam.strong_induct)
(simp_all add: fresh_atm)
lemma lookup_fresh:
fixes z::"name"
assumes "z\\" "z\x"
shows "z\ lookup \ x"
using assms
by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)
lemma lookup_fresh':
assumes "z\\"
shows "lookup \ z = Var z"
using assms
by (induct rule: lookup.induct)
(auto simp add: fresh_list_cons fresh_prod fresh_atm)
lemma psubst_subst:
assumes h:"c\\"
shows "(\)[c::=s] = ((c,s)#\)"
using h
by (nominal_induct t avoiding: \<theta> c s rule: lam.strong_induct)
(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')
inductive
Beta :: "lam\lam\bool" (" _ \\<^sub>\ _" [80,80] 80)
where
b1[intro!]: "s1 \\<^sub>\ s2 \ App s1 t \\<^sub>\ App s2 t"
| b2[intro!]: "s1\\<^sub>\s2 \ App t s1 \\<^sub>\ App t s2"
| b3[intro!]: "s1\\<^sub>\s2 \ Lam [a].s1 \\<^sub>\ Lam [a].s2"
| b4[intro!]: "a\s2 \ App (Lam [a].s1) s2\\<^sub>\ (s1[a::=s2])"
equivariance Beta
nominal_inductive Beta
by (simp_all add: abs_fresh fresh_fact')
lemma beta_preserves_fresh:
fixes a::"name"
assumes a: "t\\<^sub>\ s"
shows "a\t \ a\s"
using a
apply(nominal_induct t s avoiding: a rule: Beta.strong_induct)
apply(auto simp add: abs_fresh fresh_fact fresh_atm)
done
lemma beta_abs:
assumes a: "Lam [a].t\\<^sub>\ t'"
shows "\t''. t'=Lam [a].t'' \ t\\<^sub>\ t''"
proof -
have "a\Lam [a].t" by (simp add: abs_fresh)
with a have "a\t'" by (simp add: beta_preserves_fresh)
with a show ?thesis
by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
(auto simp add: lam.inject abs_fresh alpha)
qed
lemma beta_subst:
assumes a: "M \\<^sub>\ M'"
shows "M[x::=N]\\<^sub>\ M'[x::=N]"
using a
by (nominal_induct M M' avoiding: x N rule: Beta.strong_induct)
(auto simp add: fresh_atm subst_lemma fresh_fact)
section \<open>types\<close>
nominal_datatype ty =
TVar "nat"
| TArr "ty" "ty" (infix "\" 200)
lemma fresh_ty:
fixes a ::"name"
and \<tau> ::"ty"
shows "a\\"
by (nominal_induct \<tau> rule: ty.strong_induct)
(auto simp add: fresh_nat)
(* valid contexts *)
inductive
valid :: "(name\ty) list \ bool"
where
v1[intro]: "valid []"
| v2[intro]: "\valid \;a\\\\ valid ((a,\)#\)"
equivariance valid
(* typing judgements *)
lemma fresh_context:
fixes \<Gamma> :: "(name\<times>ty)list"
and a :: "name"
assumes a: "a\\"
shows "\(\\::ty. (a,\)\set \)"
using a
by (induct \<Gamma>)
(auto simp add: fresh_prod fresh_list_cons fresh_atm)
inductive
typing :: "(name\ty) list\lam\ty\bool" ("_ \ _ : _" [60,60,60] 60)
where
t1[intro]: "\valid \; (a,\)\set \\ \ \ \ Var a : \"
| t2[intro]: "\\ \ t1 : \\\; \ \ t2 : \\ \ \ \ App t1 t2 : \"
| t3[intro]: "\a\\;((a,\)#\) \ t : \\ \ \ \ Lam [a].t : \\\"
equivariance typing
nominal_inductive typing
by (simp_all add: abs_fresh fresh_ty)
subsection \<open>a fact about beta\<close>
definition "NORMAL" :: "lam \ bool" where
"NORMAL t \ \(\t'. t\\<^sub>\ t')"
lemma NORMAL_Var:
shows "NORMAL (Var a)"
proof -
{ assume "\t'. (Var a) \\<^sub>\ t'"
then obtain t' where "(Var a) \\<^sub>\ t'" by blast
hence False by (cases) (auto)
}
thus "NORMAL (Var a)" by (auto simp add: NORMAL_def)
qed
text \<open>Inductive version of Strong Normalisation\<close>
inductive
SN :: "lam \ bool"
where
SN_intro: "(\t'. t \\<^sub>\ t' \ SN t') \ SN t"
lemma SN_preserved:
assumes a: "SN t1" "t1\\<^sub>\ t2"
shows "SN t2"
using a
by (cases) (auto)
lemma double_SN_aux:
assumes a: "SN a"
and b: "SN b"
and hyp: "\x z.
\<lbrakk>\<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> SN y; \<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> P y z;
\<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> SN u; \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z"
shows "P a b"
proof -
from a
have r: "\b. SN b \ P a b"
proof (induct a rule: SN.SN.induct)
case (SN_intro x)
note SNI' = SN_intro
have "SN b" by fact
thus ?case
proof (induct b rule: SN.SN.induct)
case (SN_intro y)
show ?case
apply (rule hyp)
apply (erule SNI')
apply (erule SNI')
apply (rule SN.SN_intro)
apply (erule SN_intro)+
done
qed
qed
from b show ?thesis by (rule r)
qed
lemma double_SN[consumes 2]:
assumes a: "SN a"
and b: "SN b"
and c: "\x z. \\y. x \\<^sub>\ y \ P y z; \u. z \\<^sub>\ u \ P x u\ \ P x z"
shows "P a b"
using a b c
apply(rule_tac double_SN_aux)
apply(assumption)+
apply(blast)
done
section \<open>Candidates\<close>
nominal_primrec
RED :: "ty \ lam set"
where
"RED (TVar X) = {t. SN(t)}"
| "RED (\\\) = {t. \u. (u\RED \ \ (App t u)\RED \)}"
by (rule TrueI)+
text \<open>neutral terms\<close>
definition NEUT :: "lam \ bool" where
"NEUT t \ (\a. t = Var a) \ (\t1 t2. t = App t1 t2)"
(* a slight hack to get the first element of applications *)
(* this is needed to get (SN t) from SN (App t s) *)
inductive
FST :: "lam\lam\bool" (" _ \ _" [80,80] 80)
where
fst[intro!]: "(App t s) \ t"
nominal_primrec
fst_app_aux::"lam\lam option"
where
"fst_app_aux (Var a) = None"
| "fst_app_aux (App t1 t2) = Some t1"
| "fst_app_aux (Lam [x].t) = None"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: fresh_none)
apply(fresh_guess)+
done
definition
fst_app_def[simp]: "fst_app t = the (fst_app_aux t)"
lemma SN_of_FST_of_App:
assumes a: "SN (App t s)"
shows "SN (fst_app (App t s))"
using a
proof -
from a have "\z. (App t s \ z) \ SN z"
by (induct rule: SN.SN.induct)
(blast elim: FST.cases intro: SN_intro)
then have "SN t" by blast
then show "SN (fst_app (App t s))" by simp
qed
section \<open>Candidates\<close>
definition "CR1" :: "ty \ bool" where
"CR1 \ \ \t. (t\RED \ \ SN t)"
definition "CR2" :: "ty \ bool" where
"CR2 \ \ \t t'. (t\RED \ \ t \\<^sub>\ t') \ t'\RED \"
definition "CR3_RED" :: "lam \ ty \ bool" where
"CR3_RED t \ \ \t'. t\\<^sub>\ t' \ t'\RED \"
definition "CR3" :: "ty \ bool" where
"CR3 \ \ \t. (NEUT t \ CR3_RED t \) \ t\RED \"
definition "CR4" :: "ty \ bool" where
"CR4 \ \ \t. (NEUT t \ NORMAL t) \t\RED \"
lemma CR3_implies_CR4:
assumes a: "CR3 \"
shows "CR4 \"
using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def)
(* sub_induction in the arrow-type case for the next proof *)
lemma sub_induction:
assumes a: "SN(u)"
and b: "u\RED \"
and c1: "NEUT t"
and c2: "CR2 \"
and c3: "CR3 \"
and c4: "CR3_RED t (\\\)"
shows "(App t u)\RED \"
using a b
proof (induct)
fix u
assume as: "u\RED \"
assume ih: " \u'. \u \\<^sub>\ u'; u' \ RED \\ \ App t u' \ RED \"
have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def)
moreover
have "CR3_RED (App t u) \" unfolding CR3_RED_def
proof (intro strip)
fix r
assume red: "App t u \\<^sub>\ r"
moreover
{ assume "\t'. t \\<^sub>\ t' \ r = App t' u"
then obtain t' where a1: "t \\<^sub>\ t'" and a2: "r = App t' u" by blast
have "t'\RED (\\\)" using c4 a1 by (simp add: CR3_RED_def)
then have "App t' u\RED \" using as by simp
then have "r\RED \" using a2 by simp
}
moreover
{ assume "\u'. u \\<^sub>\ u' \ r = App t u'"
then obtain u' where b1: "u \\<^sub>\ u'" and b2: "r = App t u'" by blast
have "u'\RED \" using as b1 c2 by (auto simp add: CR2_def)
with ih have "App t u' \ RED \" using b1 by simp
then have "r\RED \" using b2 by simp
}
moreover
{ assume "\x t'. t = Lam [x].t'"
then obtain x t' where "t = Lam [x].t'" by blast
then have "NEUT (Lam [x].t')" using c1 by simp
then have "False" by (simp add: NEUT_def)
then have "r\RED \" by simp
}
ultimately show "r \ RED \" by (cases) (auto simp add: lam.inject)
qed
ultimately show "App t u \ RED \" using c3 by (simp add: CR3_def)
qed
text \<open>properties of the candiadates\<close>
lemma RED_props:
shows "CR1 \" and "CR2 \" and "CR3 \"
proof (nominal_induct \<tau> rule: ty.strong_induct)
case (TVar a)
{ case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
next
case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def)
next
case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def)
}
next
case (TArr \<tau>1 \<tau>2)
{ case 1
have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
have "\t. t \ RED (\1 \ \2) \ SN t"
proof -
fix t
assume "t \ RED (\1 \ \2)"
then have a: "\u. u \ RED \1 \ App t u \ RED \2" by simp
from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4)
moreover
fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
moreover
have "NORMAL (Var a)" by (rule NORMAL_Var)
ultimately have "(Var a)\ RED \1" by (simp add: CR4_def)
with a have "App t (Var a) \ RED \2" by simp
hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
thus "SN t" by (auto dest: SN_of_FST_of_App)
qed
then show "CR1 (\1 \ \2)" unfolding CR1_def by simp
next
case 2
have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
then show "CR2 (\1 \ \2)" unfolding CR2_def by auto
next
case 3
have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
show "CR3 (\1 \ \2)" unfolding CR3_def
proof (simp, intro strip)
fix t u
assume a1: "u \ RED \1"
assume a2: "NEUT t \ CR3_RED t (\1 \ \2)"
have "SN(u)" using a1 ih_CR1_\<tau>1 by (simp add: CR1_def)
then show "(App t u)\RED \2" using ih_CR2_\1 ih_CR3_\2 a1 a2 by (blast intro: sub_induction)
qed
}
qed
text \<open>
the next lemma not as simple as on paper, probably because of
the stronger double_SN induction
\<close>
lemma abs_RED:
assumes asm: "\s\RED \. t[x::=s]\RED \"
shows "Lam [x].t\RED (\\\)"
proof -
have b1: "SN t"
proof -
have "Var x\RED \"
proof -
have "CR4 \" by (simp add: RED_props CR3_implies_CR4)
moreover
have "NEUT (Var x)" by (auto simp add: NEUT_def)
moreover
have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def)
ultimately show "Var x\RED \" by (simp add: CR4_def)
qed
then have "t[x::=Var x]\RED \" using asm by simp
then have "t\RED \" by (simp add: id_subs)
moreover
have "CR1 \" by (simp add: RED_props)
ultimately show "SN t" by (simp add: CR1_def)
qed
show "Lam [x].t\RED (\\\)"
proof (simp, intro strip)
fix u
assume b2: "u\RED \"
then have b3: "SN u" using RED_props by (auto simp add: CR1_def)
show "App (Lam [x].t) u \ RED \" using b1 b3 b2 asm
proof(induct t u rule: double_SN)
fix t u
assume ih1: "\t'. \t \\<^sub>\ t'; u\RED \; \s\RED \. t'[x::=s]\RED \\ \ App (Lam [x].t') u \ RED \"
assume ih2: "\u'. \u \\<^sub>\ u'; u'\RED \; \s\RED \. t[x::=s]\RED \\ \ App (Lam [x].t) u' \ RED \"
assume as1: "u \ RED \"
assume as2: "\s\RED \. t[x::=s]\RED \"
have "CR3_RED (App (Lam [x].t) u) \" unfolding CR3_RED_def
proof(intro strip)
fix r
assume red: "App (Lam [x].t) u \\<^sub>\ r"
moreover
{ assume "\t'. t \\<^sub>\ t' \ r = App (Lam [x].t') u"
then obtain t' where a1: "t \\<^sub>\ t'" and a2: "r = App (Lam [x].t') u" by blast
have "App (Lam [x].t') u\RED \" using ih1 a1 as1 as2
apply(auto)
apply(drule_tac x="t'" in meta_spec)
apply(simp)
apply(drule meta_mp)
prefer 2
apply(auto)[1]
apply(rule ballI)
apply(drule_tac x="s" in bspec)
apply(simp)
apply(subgoal_tac "CR2 \")(*A*)
apply(unfold CR2_def)[1]
apply(drule_tac x="t[x::=s]" in spec)
apply(drule_tac x="t'[x::=s]" in spec)
apply(simp add: beta_subst)
(*A*)
apply(simp add: RED_props)
done
then have "r\RED \" using a2 by simp
}
moreover
{ assume "\u'. u \\<^sub>\ u' \ r = App (Lam [x].t) u'"
then obtain u' where b1: "u \\<^sub>\ u'" and b2: "r = App (Lam [x].t) u'" by blast
have "App (Lam [x].t) u'\RED \" using ih2 b1 as1 as2
apply(auto)
apply(drule_tac x="u'" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(subgoal_tac "CR2 \")
apply(unfold CR2_def)[1]
apply(drule_tac x="u" in spec)
apply(drule_tac x="u'" in spec)
apply(simp)
apply(simp add: RED_props)
apply(simp)
done
then have "r\RED \" using b2 by simp
}
moreover
{ assume "r = t[x::=u]"
then have "r\RED \" using as1 as2 by auto
}
ultimately show "r \ RED \"
(* one wants to use the strong elimination principle; for this one
has to know that x\<sharp>u *)
apply(cases)
apply(auto simp add: lam.inject)
apply(drule beta_abs)
apply(auto)[1]
apply(auto simp add: alpha subst_rename)
done
qed
moreover
have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto)
ultimately show "App (Lam [x].t) u \ RED \" using RED_props by (simp add: CR3_def)
qed
qed
qed
abbreviation
mapsto :: "(name\lam) list \ name \ lam \ bool" ("_ maps _ to _" [55,55,55] 55)
where
"\ maps x to e \ (lookup \ x) = e"
abbreviation
closes :: "(name\lam) list \ (name\ty) list \ bool" ("_ closes _" [55,55] 55)
where
"\ closes \ \ \x T. ((x,T) \ set \ \ (\t. \ maps x to t \ t \ RED T))"
lemma all_RED:
assumes a: "\ \ t : \"
and b: "\ closes \"
shows "\ \ RED \"
using a b
proof(nominal_induct avoiding: \<theta> rule: typing.strong_induct)
case (t3 a \<Gamma> \<sigma> t \<tau> \<theta>) \<comment> \<open>lambda case\<close>
have ih: "\\. \ closes ((a,\)#\) \ \ \ RED \" by fact
have \<theta>_cond: "\<theta> closes \<Gamma>" by fact
have fresh: "a\\" "a\\" by fact+
from ih have "\s\RED \. ((a,s)#\) \ RED \" using fresh \_cond fresh_context by simp
then have "\s\RED \. \[a::=s] \ RED \" using fresh by (simp add: psubst_subst)
then have "Lam [a].(\) \ RED (\ \ \)" by (simp only: abs_RED)
then show "\<(Lam [a].t)> \ RED (\ \ \)" using fresh by simp
qed auto
section \<open>identity substitution generated from a context \<Gamma>\<close>
fun
"id" :: "(name\ty) list \ (name\lam) list"
where
"id [] = []"
| "id ((x,\)#\) = (x,Var x)#(id \)"
lemma id_maps:
shows "(id \) maps a to (Var a)"
by (induct \<Gamma>) (auto)
lemma id_fresh:
fixes a::"name"
assumes a: "a\\"
shows "a\(id \)"
using a
by (induct \<Gamma>)
(auto simp add: fresh_list_nil fresh_list_cons)
lemma id_apply:
shows "(id \) = t"
by (nominal_induct t avoiding: \<Gamma> rule: lam.strong_induct)
(auto simp add: id_maps id_fresh)
lemma id_closes:
shows "(id \) closes \"
apply(auto)
apply(simp add: id_maps)
apply(subgoal_tac "CR3 T") \<comment> \<open>A\<close>
apply(drule CR3_implies_CR4)
apply(simp add: CR4_def)
apply(drule_tac x="Var x" in spec)
apply(force simp add: NEUT_def NORMAL_Var)
\<comment> \<open>A\<close>
apply(rule RED_props)
done
lemma typing_implies_RED:
assumes a: "\ \ t : \"
shows "t \ RED \"
proof -
have "(id \)\RED \"
proof -
have "(id \) closes \" by (rule id_closes)
with a show ?thesis by (rule all_RED)
qed
thus"t \ RED \" by (simp add: id_apply)
qed
lemma typing_implies_SN:
assumes a: "\ \ t : \"
shows "SN(t)"
proof -
from a have "t \ RED \" by (rule typing_implies_RED)
moreover
have "CR1 \" by (rule RED_props)
ultimately show "SN(t)" by (simp add: CR1_def)
qed
end
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
