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