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