--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy Thu May 31 14:47:20 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy Thu May 31 15:23:35 2007 +0200
@@ -1,20 +1,18 @@
(* $Id$ *)
+(* Authors: Christian Urban and Mathilde Arnaud *)
+(* *)
+(* A formalisation of the Church-Rosser proof by Masako Takahashi.*)
+(* This formalisation follows with some very slight exceptions *)
+(* the version of this proof given by Randy Pollack in the paper: *)
+(* *)
+(* Polishing Up the Tait-Martin Löf Proof of the *)
+(* Church-Rosser Theorem (1995). *)
+
theory CR_Takahashi
imports "../Nominal"
begin
-text {* Authors: Mathilde Arnaud and Christian Urban
-
- The Church-Rosser proof from a paper by Masako Takahashi.
- This formalisation follows with some very slight exceptions
- the one given by Randy Pollack in the paper:
-
- Polishing Up the Tait-Martin Löf Proof of the
- Church-Rosser Theorem (1995).
-
- *}
-
atom_decl name
nominal_datatype lam =
@@ -25,9 +23,9 @@
consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100)
nominal_primrec
- "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
- "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
- "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+ "(Var x)[y::=s] = (if x=y then s else (Var x))"
+ "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
+ "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
@@ -36,109 +34,101 @@
section {* Lemmas about Capture-Avoiding Substitution *}
-lemma subst_eqvt[eqvt]:
- fixes pi:: "name prm"
- shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
-by (nominal_induct t1 avoiding: b t2 rule: lam.induct)
+lemma subst_eqvt[eqvt]:
+ fixes pi::"name prm"
+ shows "pi\<bullet>t1[x::=t2] = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
+by (nominal_induct t1 avoiding: x t2 rule: lam.induct)
(auto simp add: perm_bij fresh_atm fresh_bij)
lemma forget:
- assumes a: "x\<sharp>L"
- shows "L[x::=P] = L"
-using a by (nominal_induct L avoiding: x P rule: lam.induct)
- (auto simp add: abs_fresh fresh_atm)
+ shows "x\<sharp>t \<Longrightarrow> t[x::=s] = t"
+by (nominal_induct t avoiding: x s rule: lam.induct)
+ (auto simp add: abs_fresh fresh_atm)
lemma fresh_fact:
fixes z::"name"
- assumes a: "z\<sharp>N" "z\<sharp>L"
- shows "z\<sharp>(N[y::=L])"
-using a by (nominal_induct N avoiding: z y L rule: lam.induct)
- (auto simp add: abs_fresh fresh_atm)
+ shows "z\<sharp>(t,s) \<Longrightarrow> z\<sharp>t[y::=s]"
+by (nominal_induct t avoiding: z y s rule: lam.induct)
+ (auto simp add: abs_fresh fresh_prod fresh_atm)
lemma fresh_fact':
fixes x::"name"
- assumes a: "x\<sharp>N"
- shows "x\<sharp>M[x::=N]"
-using a by (nominal_induct M avoiding: x N rule: lam.induct)
- (auto simp add: abs_fresh fresh_atm)
+ shows "x\<sharp>s \<Longrightarrow> x\<sharp>t[x::=s]"
+by (nominal_induct t avoiding: x s rule: lam.induct)
+ (auto simp add: abs_fresh fresh_atm)
lemma substitution_lemma:
- assumes a: "x\<noteq>y" "x\<sharp>L"
- shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
-using a by (nominal_induct M avoiding: x y N L rule: lam.induct)
+ assumes a: "x\<noteq>y" "x\<sharp>u"
+ shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
+using a by (nominal_induct t avoiding: x y s u rule: lam.induct)
(auto simp add: fresh_fact forget)
lemma subst_rename:
- assumes a: "y\<sharp>M"
- shows "M[x::=N] = ([(y,x)]\<bullet>M)[y::=N]"
-using a by (nominal_induct M avoiding: x y N rule: lam.induct)
- (auto simp add: calc_atm fresh_atm abs_fresh)
+ assumes a: "y\<sharp>t"
+ shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]"
+using a by (nominal_induct t avoiding: x y s rule: lam.induct)
+ (auto simp add: calc_atm fresh_atm abs_fresh)
section {* Beta-Reduction *}
-inductive2
+inductive2
"Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
where
- b1[intro]: "M1\<longrightarrow>\<^isub>\<beta>M2 \<Longrightarrow> App M1 N \<longrightarrow>\<^isub>\<beta> App M2 N"
-| b2[intro]: "N1\<longrightarrow>\<^isub>\<beta>N2 \<Longrightarrow> App M N1 \<longrightarrow>\<^isub>\<beta> App M N2"
-| b3[intro]: "M1\<longrightarrow>\<^isub>\<beta>M2 \<Longrightarrow> Lam [x].M1 \<longrightarrow>\<^isub>\<beta> Lam [x].M2"
-| b4[intro]: "(App (Lam [x].M) N)\<longrightarrow>\<^isub>\<beta> M[x::=N]"
+ b1[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^isub>\<beta> App t2 s"
+| b2[intro]: "s1 \<longrightarrow>\<^isub>\<beta> s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^isub>\<beta> App t s2"
+| b3[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^isub>\<beta> Lam [x].t2"
+| b4[intro]: "App (Lam [x].t) s \<longrightarrow>\<^isub>\<beta> t[x::=s]"
section {* Transitive Closure of Beta *}
-inductive2
- "Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
+inductive2
+ "Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
where
- bs1[intro]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
-| bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
-
-lemma Beta_star_trans[trans]:
- assumes a1: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
- and a2: "M2\<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
- shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
-using a2 a1 by (induct) (auto)
+ bs1[intro]: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t"
+| bs2[intro]: "t \<longrightarrow>\<^isub>\<beta> s \<Longrightarrow> t \<longrightarrow>\<^isub>\<beta>\<^sup>* s"
+| bs3[intro,trans]: "\<lbrakk>t1\<longrightarrow>\<^isub>\<beta>\<^sup>* t2; t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3"
section {* One-Reduction *}
-inductive2
+inductive2
One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
where
o1[intro]: "Var x\<longrightarrow>\<^isub>1 Var x"
-| o2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1M2; N1\<longrightarrow>\<^isub>1N2\<rbrakk> \<Longrightarrow> (App M1 N1)\<longrightarrow>\<^isub>1(App M2 N2)"
-| o3[intro]: "M1\<longrightarrow>\<^isub>1M2 \<Longrightarrow> (Lam [x].M1)\<longrightarrow>\<^isub>1(Lam [x].M2)"
-| o4[intro]: "\<lbrakk>x\<sharp>(N1,N2); M1\<longrightarrow>\<^isub>1M2; N1\<longrightarrow>\<^isub>1N2\<rbrakk> \<Longrightarrow> (App (Lam [x].M1) N1)\<longrightarrow>\<^isub>1M2[x::=N2]"
+| o2[intro]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2; s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>\<^isub>1 App t2 s2"
+| o3[intro]: "t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^isub>1 Lam [x].t2"
+| o4[intro]: "\<lbrakk>x\<sharp>(s1,s2); t1\<longrightarrow>\<^isub>1t2; s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2[x::=s2]"
equivariance One
-
-nominal_inductive One by (simp_all add: abs_fresh fresh_fact')
+nominal_inductive One
+ by (simp_all add: abs_fresh fresh_fact')
lemma One_refl:
- shows "M\<longrightarrow>\<^isub>1M"
-by (nominal_induct M rule: lam.induct) (auto)
+ shows "t \<longrightarrow>\<^isub>1 t"
+by (nominal_induct t rule: lam.induct) (auto)
lemma One_subst:
- assumes a: "M\<longrightarrow>\<^isub>1M'" "N\<longrightarrow>\<^isub>1N'"
- shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']"
-using a by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
+ assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
+ shows "t1[x::=s1] \<longrightarrow>\<^isub>1 t2[x::=s2]"
+using a by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
(auto simp add: substitution_lemma fresh_atm fresh_fact)
lemma better_o4_intro:
- assumes a: "M1 \<longrightarrow>\<^isub>1 M2" "N1 \<longrightarrow>\<^isub>1 N2"
- shows "App (Lam [x].M1) N1 \<longrightarrow>\<^isub>1 M2[x::=N2]"
+ assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
+ shows "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2[x::=s2]"
proof -
- obtain y::"name" where fs: "y\<sharp>(x,M1,N1,M2,N2)" by (rule exists_fresh, rule fin_supp,blast)
- have "App (Lam [x].M1) N1 = App (Lam [y].([(y,x)]\<bullet>M1)) N1" using fs
- by (rule_tac sym, auto simp add: lam.inject alpha fresh_prod fresh_atm)
- also have "\<dots> \<longrightarrow>\<^isub>1 ([(y,x)]\<bullet>M2)[y::=N2]" using fs a by (auto simp add: One.eqvt)
- also have "\<dots> = M2[x::=N2]" using fs by (simp add: subst_rename[symmetric])
- finally show "App (Lam [x].M1) N1 \<longrightarrow>\<^isub>1 M2[x::=N2]" by simp
+ obtain y::"name" where fs: "y\<sharp>(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp, blast)
+ have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]\<bullet>t1)) s1" using fs
+ by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
+ also have "\<dots> \<longrightarrow>\<^isub>1 ([(y,x)]\<bullet>t2)[y::=s2]" using fs a by (auto simp add: One.eqvt)
+ also have "\<dots> = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric])
+ finally show "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2[x::=s2]" by simp
qed
-lemma One_fresh_preserved:
- fixes a :: "name"
- assumes a: "M\<longrightarrow>\<^isub>1N"
- shows "a\<sharp>M \<Longrightarrow> a\<sharp>N"
-using a by (nominal_induct avoiding: a rule: One.strong_induct)
+lemma One_preserves_fresh:
+ fixes x :: "name"
+ assumes a: "t \<longrightarrow>\<^isub>1 s"
+ shows "x\<sharp>t \<Longrightarrow> x\<sharp>s"
+using a by (nominal_induct t s avoiding: x rule: One.strong_induct)
(auto simp add: abs_fresh fresh_atm fresh_fact)
lemma One_Var:
@@ -147,97 +137,87 @@
using a by (erule_tac One.cases) (simp_all)
lemma One_Lam:
- assumes a: "(Lam [x].N)\<longrightarrow>\<^isub>1 M"
- shows "\<exists>M'. M = Lam [x].M' \<and> N \<longrightarrow>\<^isub>1 M'"
+ assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s"
+ shows "\<exists>t'. s = Lam [x].t' \<and> t \<longrightarrow>\<^isub>1 t'"
using a
apply(erule_tac One.cases)
apply(auto simp add: lam.inject alpha)
- apply(rule_tac x="[(x,xa)]\<bullet>M2" in exI)
- apply(perm_simp add: fresh_left calc_atm)
- apply(auto simp add: One.eqvt One_fresh_preserved)
+ apply(rule_tac x="[(x,xa)]\<bullet>t2" in exI)
+ apply(perm_simp add: fresh_left calc_atm One.eqvt One_preserves_fresh)
done
lemma One_App:
- assumes a: "App M N \<longrightarrow>\<^isub>1 R"
- shows "(\<exists>M' N'. R = App M' N' \<and> M \<longrightarrow>\<^isub>1 M' \<and> N \<longrightarrow>\<^isub>1 N') \<or>
- (\<exists>x P P' N'. M = Lam [x].P \<and> x\<sharp>(N,N') \<and> R = P'[x::=N'] \<and> P \<longrightarrow>\<^isub>1 P' \<and> N \<longrightarrow>\<^isub>1 N')"
-using a by (erule_tac One.cases) (auto simp add: lam.inject)
+ assumes a: "App t s \<longrightarrow>\<^isub>1 r"
+ shows "(\<exists>t' s'. r = App t' s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or>
+ (\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^isub>1 p' \<and> s \<longrightarrow>\<^isub>1 s' \<and> x\<sharp>(s,s'))"
+using a by (erule_tac One.cases)
+ (auto simp add: lam.inject)
lemma One_Redex:
- assumes a: "App (Lam [x].M) N \<longrightarrow>\<^isub>1 R"
- shows "(\<exists>M' N'. R = App (Lam [x].M') N' \<and> M \<longrightarrow>\<^isub>1 M' \<and> N \<longrightarrow>\<^isub>1 N') \<or>
- (\<exists>M' N'. R = M'[x::=N'] \<and> M \<longrightarrow>\<^isub>1 M' \<and> N \<longrightarrow>\<^isub>1 N')"
- using a
- apply(erule_tac One.cases)
- apply(simp_all)
- apply(rule disjI1)
- apply(auto simp add: lam.inject)[1]
- apply(drule One_Lam)
- apply(simp)
- apply(rule disjI2)
- apply(auto simp add: lam.inject alpha)
- apply(rule_tac x="[(x,xa)]\<bullet>M2" in exI)
- apply(rule_tac x="N2" in exI)
- apply(simp add: subst_rename One_fresh_preserved One.eqvt)
- done
+ assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r"
+ shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or>
+ (\<exists>t' s'. r = t'[x::=s'] \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s')"
+using a
+apply(erule_tac One.cases, simp_all)
+apply(auto dest: One_Lam simp add: lam.inject)[1]
+apply(rule disjI2)
+apply(auto simp add: lam.inject alpha)
+apply(rule_tac x="[(x,xa)]\<bullet>t2" in exI)
+apply(rule_tac x="s2" in exI)
+apply(simp add: subst_rename One_preserves_fresh One.eqvt)
+done
section {* Transitive Closure of One *}
-inductive2
- "One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
+inductive2
+ "One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
where
- os1[intro]: "M \<longrightarrow>\<^isub>1\<^sup>* M"
-| os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1\<^sup>* M2; M2 \<longrightarrow>\<^isub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>1\<^sup>* M3"
+ os1[intro]: "t \<longrightarrow>\<^isub>1\<^sup>* t"
+| os2[intro]: "t \<longrightarrow>\<^isub>1 s \<Longrightarrow> t \<longrightarrow>\<^isub>1\<^sup>* s"
+| os3[intro]: "\<lbrakk>t1\<longrightarrow>\<^isub>1\<^sup>* t2; t2 \<longrightarrow>\<^isub>1\<^sup>* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
-lemma One_star_trans:
- assumes a1: "M1\<longrightarrow>\<^isub>1\<^sup>* M2"
- and a2: "M2\<longrightarrow>\<^isub>1\<^sup>* M3"
- shows "M1\<longrightarrow>\<^isub>1\<^sup>* M3"
-using a2 a1 by (induct) (auto)
+section {* Complete Development Reduction *}
-text {* Complete Development Reduction *}
-
-inductive2
+inductive2
Dev :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>d _" [80,80]80)
where
- d1[intro]: "Var x \<longrightarrow>\<^isub>d Var x"
- | d2[intro]: "M \<longrightarrow>\<^isub>d N \<Longrightarrow> Lam [x].M \<longrightarrow>\<^isub>d Lam[x].N"
- | d3[intro]: "\<lbrakk>\<not>(\<exists>y M'. M1 = Lam [y].M'); M1 \<longrightarrow>\<^isub>d M2; N1 \<longrightarrow>\<^isub>d N2\<rbrakk> \<Longrightarrow> App M1 N1 \<longrightarrow>\<^isub>d App M2 N2"
- | d4[intro]: "\<lbrakk>x\<sharp>(N1,N2); M1 \<longrightarrow>\<^isub>d M2; N1 \<longrightarrow>\<^isub>d N2\<rbrakk> \<Longrightarrow> App (Lam [x].M1) N1 \<longrightarrow>\<^isub>d M2[x::=N2]"
+ d1[intro]: "Var x \<longrightarrow>\<^isub>d Var x"
+| d2[intro]: "t \<longrightarrow>\<^isub>d s \<Longrightarrow> Lam [x].t \<longrightarrow>\<^isub>d Lam[x].s"
+| d3[intro]: "\<lbrakk>\<not>(\<exists>y t'. t1 = Lam [y].t'); t1 \<longrightarrow>\<^isub>d t2; s1 \<longrightarrow>\<^isub>d s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>\<^isub>d App t2 s2"
+| d4[intro]: "\<lbrakk>x\<sharp>(s1,s2); t1 \<longrightarrow>\<^isub>d t2; s1 \<longrightarrow>\<^isub>d s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>\<^isub>d t2[x::=s2]"
(* FIXME: needs to be in nominal_inductive *)
declare perm_pi_simp[eqvt_force]
equivariance Dev
-
nominal_inductive Dev by (simp_all add: abs_fresh fresh_fact')
lemma better_d4_intro:
- assumes a: "M1 \<longrightarrow>\<^isub>d M2" "N1 \<longrightarrow>\<^isub>d N2"
- shows "App (Lam [x].M1) N1 \<longrightarrow>\<^isub>d M2[x::=N2]"
+ assumes a: "t1 \<longrightarrow>\<^isub>d t2" "s1 \<longrightarrow>\<^isub>d s2"
+ shows "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>d t2[x::=s2]"
proof -
- obtain y::"name" where fs: "y\<sharp>(x,M1,N1,M2,N2)" by (rule exists_fresh, rule fin_supp,blast)
- have "App (Lam [x].M1) N1 = App (Lam [y].([(y,x)]\<bullet>M1)) N1" using fs
- by (rule_tac sym, auto simp add: lam.inject alpha fresh_prod fresh_atm)
- also have "\<dots> \<longrightarrow>\<^isub>d ([(y,x)]\<bullet>M2)[y::=N2]" using fs a by (auto simp add: Dev.eqvt)
- also have "\<dots> = M2[x::=N2]" using fs by (simp add: subst_rename[symmetric])
- finally show "App (Lam [x].M1) N1 \<longrightarrow>\<^isub>d M2[x::=N2]" by simp
+ obtain y::"name" where fs: "y\<sharp>(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp,blast)
+ have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]\<bullet>t1)) s1" using fs
+ by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
+ also have "\<dots> \<longrightarrow>\<^isub>d ([(y,x)]\<bullet>t2)[y::=s2]" using fs a by (auto simp add: Dev.eqvt)
+ also have "\<dots> = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric])
+ finally show "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>d t2[x::=s2]" by simp
qed
-lemma Dev_fresh_preserved:
+lemma Dev_preserves_fresh:
fixes x::"name"
assumes a: "M\<longrightarrow>\<^isub>d N"
shows "x\<sharp>M \<Longrightarrow> x\<sharp>N"
using a by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
-
+
lemma Dev_Lam:
assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N"
shows "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>\<^isub>d N'"
using a
apply(erule_tac Dev.cases)
apply(auto simp add: lam.inject alpha)
-apply(rule_tac x="[(x,xa)]\<bullet>N" in exI)
-apply(perm_simp add: fresh_left Dev.eqvt Dev_fresh_preserved)
+apply(rule_tac x="[(x,xa)]\<bullet>s" in exI)
+apply(perm_simp add: fresh_left Dev.eqvt Dev_preserves_fresh)
done
lemma Development_existence:
@@ -246,126 +226,101 @@
(auto dest!: Dev_Lam intro: better_d4_intro)
lemma Triangle:
- assumes a: "M \<longrightarrow>\<^isub>d M1" "M \<longrightarrow>\<^isub>1 M2"
- shows "M2 \<longrightarrow>\<^isub>1 M1"
-using a by (nominal_induct avoiding: M2 rule: Dev.strong_induct)
- (auto dest!: One_Var One_App One_Redex One_Lam intro: One_subst)
-(* Remark: we could here get away with a normal induction and appealing to One_fresh_preserved *)
+ assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2"
+ shows "t2 \<longrightarrow>\<^isub>1 t1"
+using a by (nominal_induct avoiding: t2 rule: Dev.strong_induct)
+ (auto dest!: One_Var One_App One_Redex One_Lam intro: One_subst)
+(* Remark: we could here get away with a normal induction and appealing to One_preserves_fresh *)
lemma Diamond_for_One:
- assumes a: "M \<longrightarrow>\<^isub>1 M1" "M \<longrightarrow>\<^isub>1 M2"
- shows "\<exists>M3. M1 \<longrightarrow>\<^isub>1 M3 \<and> M2 \<longrightarrow>\<^isub>1 M3"
+ assumes a: "t \<longrightarrow>\<^isub>1 t1" "t \<longrightarrow>\<^isub>1 t2"
+ shows "\<exists>t3. t2 \<longrightarrow>\<^isub>1 t3 \<and> t1 \<longrightarrow>\<^isub>1 t3"
proof -
- obtain Mc where "M \<longrightarrow>\<^isub>d Mc" using Development_existence by blast
- with a have "M1 \<longrightarrow>\<^isub>1 Mc" and "M2 \<longrightarrow>\<^isub>1 Mc" by (simp_all add: Triangle)
- then show "\<exists>M3. M1 \<longrightarrow>\<^isub>1 M3 \<and> M2 \<longrightarrow>\<^isub>1 M3" by blast
+ obtain tc where "t \<longrightarrow>\<^isub>d tc" using Development_existence by blast
+ with a have "t2 \<longrightarrow>\<^isub>1 tc" and "t1 \<longrightarrow>\<^isub>1 tc" by (simp_all add: Triangle)
+ then show "\<exists>t3. t2 \<longrightarrow>\<^isub>1 t3 \<and> t1 \<longrightarrow>\<^isub>1 t3" by blast
qed
lemma Rectangle_for_One:
- assumes a: "M\<longrightarrow>\<^isub>1\<^sup>*M1" "M\<longrightarrow>\<^isub>1M2"
- shows "\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1\<^sup>*M3"
- using a
-proof (induct arbitrary: M2)
- case (os2 M1 M2 M3 M')
- have a1: "M1 \<longrightarrow>\<^isub>1 M'" by fact
- have a2: "M2 \<longrightarrow>\<^isub>1 M3" by fact
- have ih: "M1 \<longrightarrow>\<^isub>1 M' \<Longrightarrow> (\<exists>M3'. M2 \<longrightarrow>\<^isub>1 M3' \<and> M' \<longrightarrow>\<^isub>1\<^sup>* M3')" by fact
- from a1 ih obtain M3' where b1: "M2 \<longrightarrow>\<^isub>1 M3'" and b2: "M' \<longrightarrow>\<^isub>1\<^sup>* M3'" by blast
- from a2 b1 obtain M4 where c1: "M3 \<longrightarrow>\<^isub>1 M4" and c2: "M3' \<longrightarrow>\<^isub>1 M4" by (auto dest: Diamond_for_One)
- from b2 c2 have "M' \<longrightarrow>\<^isub>1\<^sup>* M4" by (blast intro: One_star.os2)
- then show "\<exists>M4. M3 \<longrightarrow>\<^isub>1 M4 \<and> M' \<longrightarrow>\<^isub>1\<^sup>* M4" using c1 by blast
-qed (auto)
-
+ assumes a: "t \<longrightarrow>\<^isub>1\<^sup>* t1" "t \<longrightarrow>\<^isub>1 t2"
+ shows "\<exists>t3. t1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3"
+using a Diamond_for_One by (induct arbitrary: t2) (blast)+
+
lemma CR_for_One_star:
- assumes a: "M\<longrightarrow>\<^isub>1\<^sup>*M1" "M\<longrightarrow>\<^isub>1\<^sup>*M2"
- shows "\<exists>M3. M1\<longrightarrow>\<^isub>1\<^sup>*M3 \<and> M2\<longrightarrow>\<^isub>1\<^sup>*M3"
-using a
-proof (induct arbitrary: M2)
- case (os2 M1 M2 M3 M')
- have a1: "M1 \<longrightarrow>\<^isub>1\<^sup>* M'" by fact
- have a2: "M2 \<longrightarrow>\<^isub>1 M3" by fact
- have ih: "M1 \<longrightarrow>\<^isub>1\<^sup>* M' \<Longrightarrow> (\<exists>M3'. M2 \<longrightarrow>\<^isub>1\<^sup>* M3' \<and> M' \<longrightarrow>\<^isub>1\<^sup>* M3')" by fact
- from a1 ih obtain M3' where b1: "M2 \<longrightarrow>\<^isub>1\<^sup>* M3'" and b2: "M' \<longrightarrow>\<^isub>1\<^sup>* M3'" by blast
- from a2 b1 obtain M4 where c1: "M3 \<longrightarrow>\<^isub>1\<^sup>* M4" and c2: "M3' \<longrightarrow>\<^isub>1 M4" by (auto dest: Rectangle_for_One)
- from b2 c2 have "M' \<longrightarrow>\<^isub>1\<^sup>* M4" by (blast intro: One_star.os2)
- then show "\<exists>M4. M3 \<longrightarrow>\<^isub>1\<^sup>* M4 \<and> M' \<longrightarrow>\<^isub>1\<^sup>* M4" using c1 by blast
-qed (auto)
+ assumes a: "t \<longrightarrow>\<^isub>1\<^sup>* t1" "t \<longrightarrow>\<^isub>1\<^sup>* t2"
+ shows "\<exists>t3. t2 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
+using a Rectangle_for_One by (induct arbitrary: t2) (blast)+
section {* Establishing the Equivalence of Beta-star and One-star *}
lemma Beta_Lam_cong:
- assumes a: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2"
- shows "(Lam [x].M1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [x].M2)"
+ assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2"
+ shows "Lam [x].t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam [x].t2"
using a by (induct) (blast)+
lemma Beta_App_congL:
- assumes a: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2"
- shows "App M1 N\<longrightarrow>\<^isub>\<beta>\<^sup>* App M2 N"
+ assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2"
+ shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
using a by (induct) (blast)+
-
+
lemma Beta_App_congR:
- assumes a: "N1\<longrightarrow>\<^isub>\<beta>\<^sup>*N2"
- shows "App M N1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App M N2"
+ assumes a: "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2"
+ shows "App t s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t s2"
using a by (induct) (blast)+
lemma Beta_App_cong:
- assumes a: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" "N1\<longrightarrow>\<^isub>\<beta>\<^sup>*N2"
- shows "App M1 N1\<longrightarrow>\<^isub>\<beta>\<^sup>* App M2 N2"
-proof -
- have "App M1 N1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App M2 N1" using a by (rule_tac Beta_App_congL)
- also have "\<dots> \<longrightarrow>\<^isub>\<beta>\<^sup>* App M2 N2" using a by (rule_tac Beta_App_congR)
- finally show "App M1 N1\<longrightarrow>\<^isub>\<beta>\<^sup>* App M2 N2" by simp
-qed
+ assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2"
+ shows "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
+using a by (blast intro: Beta_App_congL Beta_App_congR)
lemmas Beta_congs = Beta_Lam_cong Beta_App_cong
lemma One_implies_Beta_star:
- assumes a: "M\<longrightarrow>\<^isub>1N"
- shows "M\<longrightarrow>\<^isub>\<beta>\<^sup>*N"
-using a by (induct) (auto intro: Beta_congs)
+ assumes a: "t \<longrightarrow>\<^isub>1 s"
+ shows "t \<longrightarrow>\<^isub>\<beta>\<^sup>* s"
+using a by (induct) (auto intro!: Beta_congs)
lemma One_star_Lam_cong:
- assumes a: "M1\<longrightarrow>\<^isub>1\<^sup>*M2"
- shows "(Lam [x].M1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [x].M2)"
-using a by (induct) (auto intro: One_star_trans)
+ assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
+ shows "Lam [x].t1 \<longrightarrow>\<^isub>1\<^sup>* Lam [x].t2"
+using a by (induct) (auto)
lemma One_star_App_congL:
- assumes a: "M1\<longrightarrow>\<^isub>1\<^sup>*M2"
- shows "App M1 N\<longrightarrow>\<^isub>1\<^sup>* App M2 N"
-using a
-by (induct) (auto intro: One_star_trans One_refl)
+ assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
+ shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+using a by (induct) (auto intro: One_refl)
lemma One_star_App_congR:
- assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
- shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
-using a by (induct) (auto intro: One_refl One_star_trans)
+ assumes a: "s1 \<longrightarrow>\<^isub>1\<^sup>* s2"
+ shows "App t s1 \<longrightarrow>\<^isub>1\<^sup>* App t s2"
+using a by (induct) (auto intro: One_refl)
lemmas One_congs = One_star_App_congL One_star_App_congR One_star_Lam_cong
lemma Beta_implies_One_star:
- assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
- shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
+ assumes a: "t1 \<longrightarrow>\<^isub>\<beta> t2"
+ shows "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
using a by (induct) (auto intro: One_refl One_congs better_o4_intro)
lemma Beta_star_equals_One_star:
- shows "M1\<longrightarrow>\<^isub>1\<^sup>*M2 = M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2"
+ shows "t1 \<longrightarrow>\<^isub>1\<^sup>* t2 = t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2"
proof
- assume "M1 \<longrightarrow>\<^isub>1\<^sup>* M2"
- then show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" by (induct) (auto intro: One_implies_Beta_star Beta_star_trans)
+ assume "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
+ then show "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" by (induct) (auto intro: One_implies_Beta_star)
next
- assume "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
- then show "M1\<longrightarrow>\<^isub>1\<^sup>*M2" by (induct) (auto intro: Beta_implies_One_star One_star_trans)
+ assume "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2"
+ then show "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" by (induct) (auto intro: Beta_implies_One_star)
qed
section {* The Church-Rosser Theorem *}
theorem CR_for_Beta_star:
- assumes a: "M\<longrightarrow>\<^isub>\<beta>\<^sup>*M1" "M\<longrightarrow>\<^isub>\<beta>\<^sup>*M2"
- shows "\<exists>M3. M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M3 \<and> M2\<longrightarrow>\<^isub>\<beta>\<^sup>*M3"
+ assumes a: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t1" "t\<longrightarrow>\<^isub>\<beta>\<^sup>* t2"
+ shows "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3"
proof -
- from a have "M\<longrightarrow>\<^isub>1\<^sup>*M1" and "M\<longrightarrow>\<^isub>1\<^sup>*M2" by (simp_all only: Beta_star_equals_One_star)
- then have "\<exists>M3. M1\<longrightarrow>\<^isub>1\<^sup>*M3 \<and> M2\<longrightarrow>\<^isub>1\<^sup>*M3" by (rule_tac CR_for_One_star)
- then show "\<exists>M3. M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M3 \<and> M2\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (simp only: Beta_star_equals_One_star)
+ from a have "t \<longrightarrow>\<^isub>1\<^sup>* t1" and "t\<longrightarrow>\<^isub>1\<^sup>* t2" by (simp_all only: Beta_star_equals_One_star)
+ then have "\<exists>t3. t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (rule_tac CR_for_One_star)
+ then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp only: Beta_star_equals_One_star)
qed
end
--- a/src/HOL/Nominal/Nominal.thy Thu May 31 14:47:20 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu May 31 15:23:35 2007 +0200
@@ -2814,8 +2814,8 @@
and b :: "'x"
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
- shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> [(a,b)]\<bullet>x=y \<and> b\<sharp>x))"
-by (auto simp add: abs_fun_eq[OF pt, OF at] pt_swap_bij[OF pt, OF at]
+ shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> [(b,a)]\<bullet>x=y \<and> b\<sharp>x))"
+by (auto simp add: abs_fun_eq[OF pt, OF at] pt_swap_bij'[OF pt, OF at]
pt_fresh_left[OF pt, OF at]
at_calc[OF at])