author | urbanc |
Mon, 11 Feb 2008 15:19:17 +0100 | |
changeset 26055 | a7a537e0413a |
parent 25867 | c24395ea4e71 |
child 26458 | 5c21ec1ff293 |
permissions | -rw-r--r-- |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
1 |
(* $Id$ *) |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
2 |
|
23159 | 3 |
(* Authors: Christian Urban and Mathilde Arnaud *) |
4 |
(* *) |
|
5 |
(* A formalisation of the Church-Rosser proof by Masako Takahashi.*) |
|
6 |
(* This formalisation follows with some very slight exceptions *) |
|
7 |
(* the version of this proof given by Randy Pollack in the paper: *) |
|
8 |
(* *) |
|
9 |
(* Polishing Up the Tait-Martin Löf Proof of the *) |
|
10 |
(* Church-Rosser Theorem (1995). *) |
|
11 |
||
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
12 |
theory CR_Takahashi |
25867 | 13 |
imports "../Nominal" |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
14 |
begin |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
15 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
16 |
atom_decl name |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
17 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
18 |
nominal_datatype lam = |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
19 |
Var "name" |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
20 |
| App "lam" "lam" |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
21 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
22 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
23 |
consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
24 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
25 |
nominal_primrec |
23159 | 26 |
"(Var x)[y::=s] = (if x=y then s else (Var x))" |
27 |
"(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])" |
|
28 |
"x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])" |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
29 |
apply(finite_guess)+ |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
30 |
apply(rule TrueI)+ |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
31 |
apply(simp add: abs_fresh) |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
32 |
apply(fresh_guess)+ |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
33 |
done |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
34 |
|
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
35 |
section {* Lemmas about Capture-Avoiding Substitution *} |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
36 |
|
23159 | 37 |
lemma subst_eqvt[eqvt]: |
38 |
fixes pi::"name prm" |
|
39 |
shows "pi\<bullet>t1[x::=t2] = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]" |
|
40 |
by (nominal_induct t1 avoiding: x t2 rule: lam.induct) |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
41 |
(auto simp add: perm_bij fresh_atm fresh_bij) |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
42 |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
43 |
lemma forget: |
23159 | 44 |
shows "x\<sharp>t \<Longrightarrow> t[x::=s] = t" |
45 |
by (nominal_induct t avoiding: x s rule: lam.induct) |
|
46 |
(auto simp add: abs_fresh fresh_atm) |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
47 |
|
26055 | 48 |
lemma fresh_fact1: |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
49 |
fixes z::"name" |
23159 | 50 |
shows "z\<sharp>(t,s) \<Longrightarrow> z\<sharp>t[y::=s]" |
51 |
by (nominal_induct t avoiding: z y s rule: lam.induct) |
|
52 |
(auto simp add: abs_fresh fresh_prod fresh_atm) |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
53 |
|
26055 | 54 |
lemma fresh_fact2: |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
55 |
fixes x::"name" |
23159 | 56 |
shows "x\<sharp>s \<Longrightarrow> x\<sharp>t[x::=s]" |
57 |
by (nominal_induct t avoiding: x s rule: lam.induct) |
|
58 |
(auto simp add: abs_fresh fresh_atm) |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
59 |
|
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
60 |
lemma substitution_lemma: |
23159 | 61 |
assumes a: "x\<noteq>y" "x\<sharp>u" |
62 |
shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]" |
|
63 |
using a by (nominal_induct t avoiding: x y s u rule: lam.induct) |
|
26055 | 64 |
(auto simp add: fresh_fact1 forget) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
65 |
|
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
66 |
lemma subst_rename: |
23159 | 67 |
assumes a: "y\<sharp>t" |
68 |
shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]" |
|
69 |
using a by (nominal_induct t avoiding: x y s rule: lam.induct) |
|
25867 | 70 |
(auto simp add: calc_atm fresh_atm abs_fresh) |
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
71 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
72 |
section {* Beta-Reduction *} |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
73 |
|
23760 | 74 |
inductive |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
75 |
"Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
76 |
where |
23159 | 77 |
b1[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^isub>\<beta> App t2 s" |
78 |
| b2[intro]: "s1 \<longrightarrow>\<^isub>\<beta> s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^isub>\<beta> App t s2" |
|
79 |
| b3[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^isub>\<beta> Lam [x].t2" |
|
80 |
| b4[intro]: "App (Lam [x].t) s \<longrightarrow>\<^isub>\<beta> t[x::=s]" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
81 |
|
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
82 |
section {* Transitive Closure of Beta *} |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
83 |
|
23760 | 84 |
inductive |
23159 | 85 |
"Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
86 |
where |
23159 | 87 |
bs1[intro]: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t" |
88 |
| bs2[intro]: "t \<longrightarrow>\<^isub>\<beta> s \<Longrightarrow> t \<longrightarrow>\<^isub>\<beta>\<^sup>* s" |
|
89 |
| bs3[intro,trans]: "\<lbrakk>t1\<longrightarrow>\<^isub>\<beta>\<^sup>* t2; t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
90 |
|
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
91 |
section {* One-Reduction *} |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
92 |
|
23760 | 93 |
inductive |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
94 |
One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80) |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
95 |
where |
22855 | 96 |
o1[intro]: "Var x\<longrightarrow>\<^isub>1 Var x" |
23159 | 97 |
| o2[intro]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2; s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>\<^isub>1 App t2 s2" |
98 |
| o3[intro]: "t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^isub>1 Lam [x].t2" |
|
99 |
| 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]" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
100 |
|
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
101 |
equivariance One |
23159 | 102 |
nominal_inductive One |
26055 | 103 |
by (simp_all add: abs_fresh fresh_fact2) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
104 |
|
22855 | 105 |
lemma One_refl: |
23159 | 106 |
shows "t \<longrightarrow>\<^isub>1 t" |
107 |
by (nominal_induct t rule: lam.induct) (auto) |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
108 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
109 |
lemma One_subst: |
23159 | 110 |
assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2" |
111 |
shows "t1[x::=s1] \<longrightarrow>\<^isub>1 t2[x::=s2]" |
|
112 |
using a by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct) |
|
26055 | 113 |
(auto simp add: substitution_lemma fresh_atm fresh_fact1) |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
114 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
115 |
lemma better_o4_intro: |
23159 | 116 |
assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2" |
117 |
shows "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2[x::=s2]" |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
118 |
proof - |
23159 | 119 |
obtain y::"name" where fs: "y\<sharp>(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp, blast) |
120 |
have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]\<bullet>t1)) s1" using fs |
|
121 |
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) |
|
122 |
also have "\<dots> \<longrightarrow>\<^isub>1 ([(y,x)]\<bullet>t2)[y::=s2]" using fs a by (auto simp add: One.eqvt) |
|
123 |
also have "\<dots> = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric]) |
|
124 |
finally show "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2[x::=s2]" by simp |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
125 |
qed |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
126 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
127 |
lemma One_Var: |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
128 |
assumes a: "Var x \<longrightarrow>\<^isub>1 M" |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
129 |
shows "M = Var x" |
26055 | 130 |
using a by (cases rule: One.cases) (simp_all) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
131 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
132 |
lemma One_Lam: |
25831 | 133 |
assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s" "x\<sharp>s" |
23159 | 134 |
shows "\<exists>t'. s = Lam [x].t' \<and> t \<longrightarrow>\<^isub>1 t'" |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
135 |
using a |
26055 | 136 |
by (cases rule: One.strong_cases) |
25831 | 137 |
(auto simp add: lam.inject abs_fresh alpha) |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
138 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
139 |
lemma One_App: |
23159 | 140 |
assumes a: "App t s \<longrightarrow>\<^isub>1 r" |
141 |
shows "(\<exists>t' s'. r = App t' s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> |
|
142 |
(\<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'))" |
|
26055 | 143 |
using a by (cases rule: One.cases) (auto simp add: lam.inject) |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
144 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
145 |
lemma One_Redex: |
25831 | 146 |
assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r" "x\<sharp>(s,r)" |
23159 | 147 |
shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> |
148 |
(\<exists>t' s'. r = t'[x::=s'] \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s')" |
|
149 |
using a |
|
26055 | 150 |
by (cases rule: One.strong_cases) |
25831 | 151 |
(auto dest: One_Lam simp add: lam.inject abs_fresh alpha fresh_prod) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
152 |
|
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
153 |
section {* Transitive Closure of One *} |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22821
diff
changeset
|
154 |
|
23760 | 155 |
inductive |
23159 | 156 |
"One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
157 |
where |
23159 | 158 |
os1[intro]: "t \<longrightarrow>\<^isub>1\<^sup>* t" |
159 |
| os2[intro]: "t \<longrightarrow>\<^isub>1 s \<Longrightarrow> t \<longrightarrow>\<^isub>1\<^sup>* s" |
|
160 |
| os3[intro]: "\<lbrakk>t1\<longrightarrow>\<^isub>1\<^sup>* t2; t2 \<longrightarrow>\<^isub>1\<^sup>* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>\<^isub>1\<^sup>* t3" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
161 |
|
23159 | 162 |
section {* Complete Development Reduction *} |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
163 |
|
23760 | 164 |
inductive |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
165 |
Dev :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>d _" [80,80]80) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
166 |
where |
23159 | 167 |
d1[intro]: "Var x \<longrightarrow>\<^isub>d Var x" |
168 |
| d2[intro]: "t \<longrightarrow>\<^isub>d s \<Longrightarrow> Lam [x].t \<longrightarrow>\<^isub>d Lam[x].s" |
|
169 |
| 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" |
|
170 |
| 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]" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
171 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
172 |
equivariance Dev |
25831 | 173 |
nominal_inductive Dev |
26055 | 174 |
by (simp_all add: abs_fresh fresh_fact2) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
175 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
176 |
lemma better_d4_intro: |
23159 | 177 |
assumes a: "t1 \<longrightarrow>\<^isub>d t2" "s1 \<longrightarrow>\<^isub>d s2" |
178 |
shows "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>d t2[x::=s2]" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
179 |
proof - |
23159 | 180 |
obtain y::"name" where fs: "y\<sharp>(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp,blast) |
181 |
have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]\<bullet>t1)) s1" using fs |
|
182 |
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) |
|
183 |
also have "\<dots> \<longrightarrow>\<^isub>d ([(y,x)]\<bullet>t2)[y::=s2]" using fs a by (auto simp add: Dev.eqvt) |
|
184 |
also have "\<dots> = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric]) |
|
185 |
finally show "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>d t2[x::=s2]" by simp |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
186 |
qed |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
187 |
|
23159 | 188 |
lemma Dev_preserves_fresh: |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
189 |
fixes x::"name" |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
190 |
assumes a: "M\<longrightarrow>\<^isub>d N" |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
191 |
shows "x\<sharp>M \<Longrightarrow> x\<sharp>N" |
26055 | 192 |
using a |
193 |
by (induct) (auto simp add: abs_fresh fresh_fact1 fresh_fact2) |
|
23159 | 194 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
195 |
lemma Dev_Lam: |
25831 | 196 |
assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N" |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
197 |
shows "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>\<^isub>d N'" |
25831 | 198 |
proof - |
199 |
from a have "x\<sharp>Lam [x].M" by (simp add: abs_fresh) |
|
200 |
with a have "x\<sharp>N" by (simp add: Dev_preserves_fresh) |
|
26055 | 201 |
with a show "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>\<^isub>d N'" |
202 |
by (cases rule: Dev.strong_cases) |
|
25831 | 203 |
(auto simp add: lam.inject abs_fresh alpha) |
204 |
qed |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
205 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
206 |
lemma Development_existence: |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
207 |
shows "\<exists>M'. M \<longrightarrow>\<^isub>d M'" |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
208 |
by (nominal_induct M rule: lam.induct) |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
209 |
(auto dest!: Dev_Lam intro: better_d4_intro) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
210 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
211 |
lemma Triangle: |
23159 | 212 |
assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2" |
213 |
shows "t2 \<longrightarrow>\<^isub>1 t1" |
|
25831 | 214 |
using a |
215 |
apply(nominal_induct avoiding: t2 rule: Dev.strong_induct) |
|
26055 | 216 |
apply(auto dest!: One_Var One_Lam One_App)[3] |
217 |
apply(auto dest!: One_Redex intro: One_subst) |
|
25831 | 218 |
done |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
219 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
220 |
lemma Diamond_for_One: |
23159 | 221 |
assumes a: "t \<longrightarrow>\<^isub>1 t1" "t \<longrightarrow>\<^isub>1 t2" |
222 |
shows "\<exists>t3. t2 \<longrightarrow>\<^isub>1 t3 \<and> t1 \<longrightarrow>\<^isub>1 t3" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
223 |
proof - |
23159 | 224 |
obtain tc where "t \<longrightarrow>\<^isub>d tc" using Development_existence by blast |
225 |
with a have "t2 \<longrightarrow>\<^isub>1 tc" and "t1 \<longrightarrow>\<^isub>1 tc" by (simp_all add: Triangle) |
|
226 |
then show "\<exists>t3. t2 \<longrightarrow>\<^isub>1 t3 \<and> t1 \<longrightarrow>\<^isub>1 t3" by blast |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
227 |
qed |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
228 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
229 |
lemma Rectangle_for_One: |
23159 | 230 |
assumes a: "t \<longrightarrow>\<^isub>1\<^sup>* t1" "t \<longrightarrow>\<^isub>1 t2" |
231 |
shows "\<exists>t3. t1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" |
|
232 |
using a Diamond_for_One by (induct arbitrary: t2) (blast)+ |
|
233 |
||
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
234 |
lemma CR_for_One_star: |
23159 | 235 |
assumes a: "t \<longrightarrow>\<^isub>1\<^sup>* t1" "t \<longrightarrow>\<^isub>1\<^sup>* t2" |
236 |
shows "\<exists>t3. t2 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t1 \<longrightarrow>\<^isub>1\<^sup>* t3" |
|
237 |
using a Rectangle_for_One by (induct arbitrary: t2) (blast)+ |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
238 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
239 |
section {* Establishing the Equivalence of Beta-star and One-star *} |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
240 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
241 |
lemma Beta_Lam_cong: |
23159 | 242 |
assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" |
243 |
shows "Lam [x].t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam [x].t2" |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
244 |
using a by (induct) (blast)+ |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
245 |
|
26055 | 246 |
lemma Beta_App_cong_aux: |
23159 | 247 |
assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" |
248 |
shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s" |
|
26055 | 249 |
and "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2" |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
250 |
using a by (induct) (blast)+ |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
251 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
252 |
lemma Beta_App_cong: |
23159 | 253 |
assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2" |
254 |
shows "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" |
|
26055 | 255 |
using a by (blast intro: Beta_App_cong_aux) |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
256 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
257 |
lemmas Beta_congs = Beta_Lam_cong Beta_App_cong |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
258 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
259 |
lemma One_implies_Beta_star: |
23159 | 260 |
assumes a: "t \<longrightarrow>\<^isub>1 s" |
261 |
shows "t \<longrightarrow>\<^isub>\<beta>\<^sup>* s" |
|
262 |
using a by (induct) (auto intro!: Beta_congs) |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
263 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
264 |
lemma One_star_Lam_cong: |
23159 | 265 |
assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" |
266 |
shows "Lam [x].t1 \<longrightarrow>\<^isub>1\<^sup>* Lam [x].t2" |
|
267 |
using a by (induct) (auto) |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
268 |
|
26055 | 269 |
lemma One_star_App_cong: |
23159 | 270 |
assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" |
26055 | 271 |
shows "App t1 s \<longrightarrow>\<^isub>1\<^sup>* App t2 s" |
272 |
and "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2" |
|
23159 | 273 |
using a by (induct) (auto intro: One_refl) |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
274 |
|
26055 | 275 |
lemmas One_congs = One_star_App_cong One_star_Lam_cong |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
276 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
277 |
lemma Beta_implies_One_star: |
23159 | 278 |
assumes a: "t1 \<longrightarrow>\<^isub>\<beta> t2" |
279 |
shows "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" |
|
22855 | 280 |
using a by (induct) (auto intro: One_refl One_congs better_o4_intro) |
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
281 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
282 |
lemma Beta_star_equals_One_star: |
23159 | 283 |
shows "t1 \<longrightarrow>\<^isub>1\<^sup>* t2 = t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" |
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
284 |
proof |
23159 | 285 |
assume "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" |
286 |
then show "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" by (induct) (auto intro: One_implies_Beta_star) |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
287 |
next |
23159 | 288 |
assume "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" |
289 |
then show "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" by (induct) (auto intro: Beta_implies_One_star) |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
290 |
qed |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
291 |
|
22833
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
292 |
section {* The Church-Rosser Theorem *} |
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
293 |
|
51a16a718820
polished all proofs and made the theory "self-contained"
urbanc
parents:
22829
diff
changeset
|
294 |
theorem CR_for_Beta_star: |
23159 | 295 |
assumes a: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t1" "t\<longrightarrow>\<^isub>\<beta>\<^sup>* t2" |
296 |
shows "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
297 |
proof - |
26055 | 298 |
from a have "t \<longrightarrow>\<^isub>1\<^sup>* t1" and "t\<longrightarrow>\<^isub>1\<^sup>* t2" by (simp_all add: Beta_star_equals_One_star) |
299 |
then have "\<exists>t3. t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (simp add: CR_for_One_star) |
|
300 |
then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp add: Beta_star_equals_One_star) |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
301 |
qed |
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
302 |
|
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
diff
changeset
|
303 |
end |