1theory CR 2imports Lam_Funs 3begin 4 5text \<open>The Church-Rosser proof from Barendregt's book\<close> 6 7lemma forget: 8 assumes asm: "x\<sharp>L" 9 shows "L[x::=P] = L" 10using asm 11proof (nominal_induct L avoiding: x P rule: lam.strong_induct) 12 case (Var z) 13 have "x\<sharp>Var z" by fact 14 thus "(Var z)[x::=P] = (Var z)" by (simp add: fresh_atm) 15next 16 case (App M1 M2) 17 have "x\<sharp>App M1 M2" by fact 18 moreover 19 have ih1: "x\<sharp>M1 \<Longrightarrow> M1[x::=P] = M1" by fact 20 moreover 21 have ih1: "x\<sharp>M2 \<Longrightarrow> M2[x::=P] = M2" by fact 22 ultimately show "(App M1 M2)[x::=P] = (App M1 M2)" by simp 23next 24 case (Lam z M) 25 have vc: "z\<sharp>x" "z\<sharp>P" by fact+ 26 have ih: "x\<sharp>M \<Longrightarrow> M[x::=P] = M" by fact 27 have asm: "x\<sharp>Lam [z].M" by fact 28 then have "x\<sharp>M" using vc by (simp add: fresh_atm abs_fresh) 29 then have "M[x::=P] = M" using ih by simp 30 then show "(Lam [z].M)[x::=P] = Lam [z].M" using vc by simp 31qed 32 33lemma forget_automatic: 34 assumes asm: "x\<sharp>L" 35 shows "L[x::=P] = L" 36 using asm 37by (nominal_induct L avoiding: x P rule: lam.strong_induct) 38 (auto simp add: abs_fresh fresh_atm) 39 40lemma fresh_fact: 41 fixes z::"name" 42 assumes asms: "z\<sharp>N" "z\<sharp>L" 43 shows "z\<sharp>(N[y::=L])" 44using asms 45proof (nominal_induct N avoiding: z y L rule: lam.strong_induct) 46 case (Var u) 47 have "z\<sharp>(Var u)" "z\<sharp>L" by fact+ 48 thus "z\<sharp>((Var u)[y::=L])" by simp 49next 50 case (App N1 N2) 51 have ih1: "\<lbrakk>z\<sharp>N1; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N1[y::=L]" by fact 52 moreover 53 have ih2: "\<lbrakk>z\<sharp>N2; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N2[y::=L]" by fact 54 moreover 55 have "z\<sharp>App N1 N2" "z\<sharp>L" by fact+ 56 ultimately show "z\<sharp>((App N1 N2)[y::=L])" by simp 57next 58 case (Lam u N1) 59 have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact+ 60 have "z\<sharp>Lam [u].N1" by fact 61 hence "z\<sharp>N1" using vc by (simp add: abs_fresh fresh_atm) 62 moreover 63 have ih: "\<lbrakk>z\<sharp>N1; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>(N1[y::=L])" by fact 64 moreover 65 have "z\<sharp>L" by fact 66 ultimately show "z\<sharp>(Lam [u].N1)[y::=L]" using vc by (simp add: abs_fresh) 67qed 68 69lemma fresh_fact_automatic: 70 fixes z::"name" 71 assumes asms: "z\<sharp>N" "z\<sharp>L" 72 shows "z\<sharp>(N[y::=L])" 73 using asms 74by (nominal_induct N avoiding: z y L rule: lam.strong_induct) 75 (auto simp add: abs_fresh fresh_atm) 76 77lemma fresh_fact': 78 fixes a::"name" 79 assumes a: "a\<sharp>t2" 80 shows "a\<sharp>t1[a::=t2]" 81using a 82by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) 83 (auto simp add: abs_fresh fresh_atm) 84 85lemma substitution_lemma: 86 assumes a: "x\<noteq>y" 87 and b: "x\<sharp>L" 88 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" 89using a b 90proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct) 91 case (Var z) (* case 1: Variables*) 92 have "x\<noteq>y" by fact 93 have "x\<sharp>L" by fact 94 show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS") 95 proof - 96 { (*Case 1.1*) 97 assume "z=x" 98 have "(1)": "?LHS = N[y::=L]" using \<open>z=x\<close> by simp 99 have "(2)": "?RHS = N[y::=L]" using \<open>z=x\<close> \<open>x\<noteq>y\<close> by simp 100 from "(1)" "(2)" have "?LHS = ?RHS" by simp 101 } 102 moreover 103 { (*Case 1.2*) 104 assume "z=y" and "z\<noteq>x" 105 have "(1)": "?LHS = L" using \<open>z\<noteq>x\<close> \<open>z=y\<close> by simp 106 have "(2)": "?RHS = L[x::=N[y::=L]]" using \<open>z=y\<close> by simp 107 have "(3)": "L[x::=N[y::=L]] = L" using \<open>x\<sharp>L\<close> by (simp add: forget) 108 from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp 109 } 110 moreover 111 { (*Case 1.3*) 112 assume "z\<noteq>x" and "z\<noteq>y" 113 have "(1)": "?LHS = Var z" using \<open>z\<noteq>x\<close> \<open>z\<noteq>y\<close> by simp 114 have "(2)": "?RHS = Var z" using \<open>z\<noteq>x\<close> \<open>z\<noteq>y\<close> by simp 115 from "(1)" "(2)" have "?LHS = ?RHS" by simp 116 } 117 ultimately show "?LHS = ?RHS" by blast 118 qed 119next 120 case (Lam z M1) (* case 2: lambdas *) 121 have ih: "\<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact 122 have "x\<noteq>y" by fact 123 have "x\<sharp>L" by fact 124 have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact+ 125 hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact) 126 show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 127 proof - 128 have "?LHS = Lam [z].(M1[x::=N][y::=L])" using \<open>z\<sharp>x\<close> \<open>z\<sharp>y\<close> \<open>z\<sharp>N\<close> \<open>z\<sharp>L\<close> by simp 129 also from ih have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])" using \<open>x\<noteq>y\<close> \<open>x\<sharp>L\<close> by simp 130 also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using \<open>z\<sharp>x\<close> \<open>z\<sharp>N[y::=L]\<close> by simp 131 also have "\<dots> = ?RHS" using \<open>z\<sharp>y\<close> \<open>z\<sharp>L\<close> by simp 132 finally show "?LHS = ?RHS" . 133 qed 134next 135 case (App M1 M2) (* case 3: applications *) 136 thus "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp 137qed 138 139lemma substitution_lemma_automatic: 140 assumes asm: "x\<noteq>y" "x\<sharp>L" 141 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" 142 using asm 143by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) 144 (auto simp add: fresh_fact forget) 145 146section \<open>Beta Reduction\<close> 147 148inductive 149 "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta> _" [80,80] 80) 150where 151 b1[intro]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^sub>\<beta>(App s2 t)" 152 | b2[intro]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^sub>\<beta>(App t s2)" 153 | b3[intro]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^sub>\<beta> (Lam [a].s2)" 154 | b4[intro]: "a\<sharp>s2 \<Longrightarrow> (App (Lam [a].s1) s2)\<longrightarrow>\<^sub>\<beta>(s1[a::=s2])" 155 156equivariance Beta 157 158nominal_inductive Beta 159 by (simp_all add: abs_fresh fresh_fact') 160 161inductive 162 "Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta>\<^sup>* _" [80,80] 80) 163where 164 bs1[intro, simp]: "M \<longrightarrow>\<^sub>\<beta>\<^sup>* M" 165 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^sub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^sub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^sub>\<beta>\<^sup>* M3" 166 167equivariance Beta_star 168 169lemma beta_star_trans: 170 assumes a1: "M1\<longrightarrow>\<^sub>\<beta>\<^sup>* M2" 171 and a2: "M2\<longrightarrow>\<^sub>\<beta>\<^sup>* M3" 172 shows "M1 \<longrightarrow>\<^sub>\<beta>\<^sup>* M3" 173using a2 a1 174by (induct) (auto) 175 176section \<open>One-Reduction\<close> 177 178inductive 179 One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>1 _" [80,80] 80) 180where 181 o1[intro!]: "M\<longrightarrow>\<^sub>1M" 182 | o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^sub>1t2;s1\<longrightarrow>\<^sub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^sub>1(App t2 s2)" 183 | o3[simp,intro!]: "s1\<longrightarrow>\<^sub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^sub>1(Lam [a].s2)" 184 | o4[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1\<longrightarrow>\<^sub>1s2;t1\<longrightarrow>\<^sub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^sub>1(t2[a::=s2])" 185 186equivariance One 187 188nominal_inductive One 189 by (simp_all add: abs_fresh fresh_fact') 190 191inductive 192 "One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>1\<^sup>* _" [80,80] 80) 193where 194 os1[intro, simp]: "M \<longrightarrow>\<^sub>1\<^sup>* M" 195 | os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^sub>1\<^sup>* M2; M2 \<longrightarrow>\<^sub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^sub>1\<^sup>* M3" 196 197equivariance One_star 198 199lemma one_star_trans: 200 assumes a1: "M1\<longrightarrow>\<^sub>1\<^sup>* M2" 201 and a2: "M2\<longrightarrow>\<^sub>1\<^sup>* M3" 202 shows "M1\<longrightarrow>\<^sub>1\<^sup>* M3" 203using a2 a1 204by (induct) (auto) 205 206lemma one_fresh_preserv: 207 fixes a :: "name" 208 assumes a: "t\<longrightarrow>\<^sub>1s" 209 and b: "a\<sharp>t" 210 shows "a\<sharp>s" 211using a b 212proof (induct) 213 case o1 thus ?case by simp 214next 215 case o2 thus ?case by simp 216next 217 case (o3 s1 s2 c) 218 have ih: "a\<sharp>s1 \<Longrightarrow> a\<sharp>s2" by fact 219 have c: "a\<sharp>Lam [c].s1" by fact 220 show ?case 221 proof (cases "a=c") 222 assume "a=c" thus "a\<sharp>Lam [c].s2" by (simp add: abs_fresh) 223 next 224 assume d: "a\<noteq>c" 225 with c have "a\<sharp>s1" by (simp add: abs_fresh) 226 hence "a\<sharp>s2" using ih by simp 227 thus "a\<sharp>Lam [c].s2" using d by (simp add: abs_fresh) 228 qed 229next 230 case (o4 c t1 t2 s1 s2) 231 have i1: "a\<sharp>t1 \<Longrightarrow> a\<sharp>t2" by fact 232 have i2: "a\<sharp>s1 \<Longrightarrow> a\<sharp>s2" by fact 233 have as: "a\<sharp>App (Lam [c].s1) t1" by fact 234 hence c1: "a\<sharp>Lam [c].s1" and c2: "a\<sharp>t1" by (simp add: fresh_prod)+ 235 from c2 i1 have c3: "a\<sharp>t2" by simp 236 show "a\<sharp>s2[c::=t2]" 237 proof (cases "a=c") 238 assume "a=c" 239 thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact') 240 next 241 assume d1: "a\<noteq>c" 242 from c1 d1 have "a\<sharp>s1" by (simp add: abs_fresh) 243 hence "a\<sharp>s2" using i2 by simp 244 thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact) 245 qed 246qed 247 248lemma one_fresh_preserv_automatic: 249 fixes a :: "name" 250 assumes a: "t\<longrightarrow>\<^sub>1s" 251 and b: "a\<sharp>t" 252 shows "a\<sharp>s" 253using a b 254apply(nominal_induct avoiding: a rule: One.strong_induct) 255apply(auto simp add: abs_fresh fresh_atm fresh_fact) 256done 257 258lemma subst_rename: 259 assumes a: "c\<sharp>t1" 260 shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]" 261using a 262by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct) 263 (auto simp add: calc_atm fresh_atm abs_fresh) 264 265lemma one_abs: 266 assumes a: "Lam [a].t\<longrightarrow>\<^sub>1t'" 267 shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^sub>1t''" 268proof - 269 have "a\<sharp>Lam [a].t" by (simp add: abs_fresh) 270 with a have "a\<sharp>t'" by (simp add: one_fresh_preserv) 271 with a show ?thesis 272 by (cases rule: One.strong_cases[where a="a" and aa="a"]) 273 (auto simp add: lam.inject abs_fresh alpha) 274qed 275 276lemma one_app: 277 assumes a: "App t1 t2 \<longrightarrow>\<^sub>1 t'" 278 shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2) \<or> 279 (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2 \<and> a\<sharp>(t2,s2))" 280using a by (erule_tac One.cases) (auto simp add: lam.inject) 281 282lemma one_red: 283 assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^sub>1 M" "a\<sharp>(t2,M)" 284 shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2) \<or> 285 (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2)" 286using a 287by (cases rule: One.strong_cases [where a="a" and aa="a"]) 288 (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod) 289 290text \<open>first case in Lemma 3.2.4\<close> 291 292lemma one_subst_aux: 293 assumes a: "N\<longrightarrow>\<^sub>1N'" 294 shows "M[x::=N] \<longrightarrow>\<^sub>1 M[x::=N']" 295using a 296proof (nominal_induct M avoiding: x N N' rule: lam.strong_induct) 297 case (Var y) 298 thus "Var y[x::=N] \<longrightarrow>\<^sub>1 Var y[x::=N']" by (cases "x=y") auto 299next 300 case (App P Q) (* application case - third line *) 301 thus "(App P Q)[x::=N] \<longrightarrow>\<^sub>1 (App P Q)[x::=N']" using o2 by simp 302next 303 case (Lam y P) (* abstraction case - fourth line *) 304 thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^sub>1 (Lam [y].P)[x::=N']" using o3 by simp 305qed 306 307lemma one_subst_aux_automatic: 308 assumes a: "N\<longrightarrow>\<^sub>1N'" 309 shows "M[x::=N] \<longrightarrow>\<^sub>1 M[x::=N']" 310using a 311by (nominal_induct M avoiding: x N N' rule: lam.strong_induct) 312 (auto simp add: fresh_prod fresh_atm) 313 314lemma one_subst: 315 assumes a: "M\<longrightarrow>\<^sub>1M'" 316 and b: "N\<longrightarrow>\<^sub>1N'" 317 shows "M[x::=N]\<longrightarrow>\<^sub>1M'[x::=N']" 318using a b 319proof (nominal_induct M M' avoiding: N N' x rule: One.strong_induct) 320 case (o1 M) 321 thus ?case by (simp add: one_subst_aux) 322next 323 case (o2 M1 M2 N1 N2) 324 thus ?case by simp 325next 326 case (o3 a M1 M2) 327 thus ?case by simp 328next 329 case (o4 a N1 N2 M1 M2 N N' x) 330 have vc: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" "a\<sharp>N1" "a\<sharp>N2" by fact+ 331 have asm: "N\<longrightarrow>\<^sub>1N'" by fact 332 show ?case 333 proof - 334 have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using vc by simp 335 moreover have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^sub>1 M2[x::=N'][a::=N2[x::=N']]" 336 using o4 asm by (simp add: fresh_fact) 337 moreover have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" 338 using vc by (simp add: substitution_lemma fresh_atm) 339 ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^sub>1 M2[a::=N2][x::=N']" by simp 340 qed 341qed 342 343lemma one_subst_automatic: 344 assumes a: "M\<longrightarrow>\<^sub>1M'" 345 and b: "N\<longrightarrow>\<^sub>1N'" 346 shows "M[x::=N]\<longrightarrow>\<^sub>1M'[x::=N']" 347using a b 348by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct) 349 (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact) 350 351lemma diamond[rule_format]: 352 fixes M :: "lam" 353 and M1:: "lam" 354 assumes a: "M\<longrightarrow>\<^sub>1M1" 355 and b: "M\<longrightarrow>\<^sub>1M2" 356 shows "\<exists>M3. M1\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" 357 using a b 358proof (nominal_induct avoiding: M1 M2 rule: One.strong_induct) 359 case (o1 M) (* case 1 --- M1 = M *) 360 thus "\<exists>M3. M\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" by blast 361next 362 case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*) 363 have vc: "x\<sharp>Q" "x\<sharp>Q'" "x\<sharp>M2" by fact+ 364 have i1: "\<And>M2. Q \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact 365 have i2: "\<And>M2. P \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact 366 have "App (Lam [x].P) Q \<longrightarrow>\<^sub>1 M2" by fact 367 hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q') \<or> 368 (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q')" using vc by (simp add: one_red) 369 moreover (* subcase 2.1 *) 370 { assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q'" 371 then obtain P'' and Q'' where 372 b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^sub>1P''" and b3: "Q\<longrightarrow>\<^sub>1Q''" by blast 373 from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> P''\<longrightarrow>\<^sub>1M3)" by simp 374 then obtain P''' where 375 c1: "P'\<longrightarrow>\<^sub>1P'''" and c2: "P''\<longrightarrow>\<^sub>1P'''" by force 376 from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3)" by simp 377 then obtain Q''' where 378 d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by force 379 from c1 c2 d1 d2 380 have "P'[x::=Q']\<longrightarrow>\<^sub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^sub>1 P'''[x::=Q''']" 381 using vc b3 by (auto simp add: one_subst one_fresh_preserv) 382 hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast 383 } 384 moreover (* subcase 2.2 *) 385 { assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q'" 386 then obtain P'' Q'' where 387 b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^sub>1P''" and b3: "Q\<longrightarrow>\<^sub>1Q''" by blast 388 from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> P''\<longrightarrow>\<^sub>1M3)" by simp 389 then obtain P''' where 390 c1: "P'\<longrightarrow>\<^sub>1P'''" and c2: "P''\<longrightarrow>\<^sub>1P'''" by blast 391 from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3)" by simp 392 then obtain Q''' where 393 d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by blast 394 from c1 c2 d1 d2 395 have "P'[x::=Q']\<longrightarrow>\<^sub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^sub>1P'''[x::=Q''']" 396 by (force simp add: one_subst) 397 hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast 398 } 399 ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" by blast 400next 401 case (o2 P P' Q Q') (* case 3 *) 402 have i0: "P\<longrightarrow>\<^sub>1P'" by fact 403 have i0': "Q\<longrightarrow>\<^sub>1Q'" by fact 404 have i1: "\<And>M2. Q \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact 405 have i2: "\<And>M2. P \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact 406 assume "App P Q \<longrightarrow>\<^sub>1 M2" 407 hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^sub>1P'' \<and> Q\<longrightarrow>\<^sub>1Q'') \<or> 408 (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^sub>1 P'' \<and> Q\<longrightarrow>\<^sub>1Q' \<and> x\<sharp>(Q,Q'))" 409 by (simp add: one_app[simplified]) 410 moreover (* subcase 3.1 *) 411 { assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^sub>1P'' \<and> Q\<longrightarrow>\<^sub>1Q''" 412 then obtain P'' and Q'' where 413 b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^sub>1P''" and b3: "Q\<longrightarrow>\<^sub>1Q''" by blast 414 from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> P''\<longrightarrow>\<^sub>1M3)" by simp 415 then obtain P''' where 416 c1: "P'\<longrightarrow>\<^sub>1P'''" and c2: "P''\<longrightarrow>\<^sub>1P'''" by blast 417 from b3 i1 have "\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3" by simp 418 then obtain Q''' where 419 d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by blast 420 from c1 c2 d1 d2 421 have "App P' Q'\<longrightarrow>\<^sub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^sub>1 App P''' Q'''" by blast 422 hence "\<exists>M3. App P' Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast 423 } 424 moreover (* subcase 3.2 *) 425 { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^sub>1 P'' \<and> Q\<longrightarrow>\<^sub>1Q'' \<and> x\<sharp>(Q,Q'')" 426 then obtain x P1 P1'' Q'' where 427 b0: "P = Lam [x].P1" and b1: "M2 = P1''[x::=Q'']" and 428 b2: "P1\<longrightarrow>\<^sub>1P1''" and b3: "Q\<longrightarrow>\<^sub>1Q''" and vc: "x\<sharp>(Q,Q'')" by blast 429 from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^sub>1P1'" by (simp add: one_abs) 430 then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^sub>1P1'" by blast 431 from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^sub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^sub>1M3)" by simp 432 then obtain P1''' where 433 c1: "(Lam [x].P1')\<longrightarrow>\<^sub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^sub>1P1'''" by blast 434 from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^sub>1R1" by (simp add: one_abs) 435 then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^sub>1R1" by blast 436 from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^sub>1R2" by (simp add: one_abs) 437 then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^sub>1R2" by blast 438 from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) 439 from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3)" by simp 440 then obtain Q''' where 441 d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by blast 442 from g1 r2 d1 r4 r5 d2 443 have "App P' Q'\<longrightarrow>\<^sub>1R1[x::=Q'''] \<and> P1''[x::=Q'']\<longrightarrow>\<^sub>1R1[x::=Q''']" 444 using vc i0' by (simp add: one_subst one_fresh_preserv) 445 hence "\<exists>M3. App P' Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast 446 } 447 ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" by blast 448next 449 case (o3 P P' x) (* case 4 *) 450 have i1: "P\<longrightarrow>\<^sub>1P'" by fact 451 have i2: "\<And>M2. P \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact 452 have "(Lam [x].P)\<longrightarrow>\<^sub>1 M2" by fact 453 hence "\<exists>P''. M2=Lam [x].P'' \<and> P\<longrightarrow>\<^sub>1P''" by (simp add: one_abs) 454 then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P\<longrightarrow>\<^sub>1P''" by blast 455 from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^sub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^sub>1M3" by blast 456 then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^sub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^sub>1M3" by blast 457 from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^sub>1R1" by (simp add: one_abs) 458 then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^sub>1R1" by blast 459 from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^sub>1R2" by (simp add: one_abs) 460 then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^sub>1R2" by blast 461 from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) 462 from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^sub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^sub>1(Lam [x].R2)" 463 by (simp add: one_subst) 464 thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 r5 by blast 465qed 466 467lemma one_lam_cong: 468 assumes a: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 469 shows "(Lam [a].t1)\<longrightarrow>\<^sub>\<beta>\<^sup>*(Lam [a].t2)" 470 using a 471proof induct 472 case bs1 thus ?case by simp 473next 474 case (bs2 y z) 475 thus ?case by (blast dest: b3) 476qed 477 478lemma one_app_congL: 479 assumes a: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 480 shows "App t1 s\<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s" 481 using a 482proof induct 483 case bs1 thus ?case by simp 484next 485 case bs2 thus ?case by (blast dest: b1) 486qed 487 488lemma one_app_congR: 489 assumes a: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 490 shows "App s t1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App s t2" 491using a 492proof induct 493 case bs1 thus ?case by simp 494next 495 case bs2 thus ?case by (blast dest: b2) 496qed 497 498lemma one_app_cong: 499 assumes a1: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 500 and a2: "s1\<longrightarrow>\<^sub>\<beta>\<^sup>*s2" 501 shows "App t1 s1\<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s2" 502proof - 503 have "App t1 s1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL) 504 moreover 505 have "App t2 s1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR) 506 ultimately show ?thesis by (rule beta_star_trans) 507qed 508 509lemma one_beta_star: 510 assumes a: "(t1\<longrightarrow>\<^sub>1t2)" 511 shows "(t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2)" 512 using a 513proof(nominal_induct rule: One.strong_induct) 514 case o1 thus ?case by simp 515next 516 case o2 thus ?case by (blast intro!: one_app_cong) 517next 518 case o3 thus ?case by (blast intro!: one_lam_cong) 519next 520 case (o4 a s1 s2 t1 t2) 521 have vc: "a\<sharp>s1" "a\<sharp>s2" by fact+ 522 have a1: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^sub>\<beta>\<^sup>*s2" by fact+ 523 have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^sub>\<beta> (t2 [a::= s2])" using vc by (simp add: b4) 524 from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 525 by (blast intro!: one_app_cong one_lam_cong) 526 show ?case using c2 c1 by (blast intro: beta_star_trans) 527qed 528 529lemma one_star_lam_cong: 530 assumes a: "t1\<longrightarrow>\<^sub>1\<^sup>*t2" 531 shows "(Lam [a].t1)\<longrightarrow>\<^sub>1\<^sup>* (Lam [a].t2)" 532 using a 533proof induct 534 case os1 thus ?case by simp 535next 536 case os2 thus ?case by (blast intro: one_star_trans) 537qed 538 539lemma one_star_app_congL: 540 assumes a: "t1\<longrightarrow>\<^sub>1\<^sup>*t2" 541 shows "App t1 s\<longrightarrow>\<^sub>1\<^sup>* App t2 s" 542 using a 543proof induct 544 case os1 thus ?case by simp 545next 546 case os2 thus ?case by (blast intro: one_star_trans) 547qed 548 549lemma one_star_app_congR: 550 assumes a: "t1\<longrightarrow>\<^sub>1\<^sup>*t2" 551 shows "App s t1 \<longrightarrow>\<^sub>1\<^sup>* App s t2" 552 using a 553proof induct 554 case os1 thus ?case by simp 555next 556 case os2 thus ?case by (blast intro: one_star_trans) 557qed 558 559lemma beta_one_star: 560 assumes a: "t1\<longrightarrow>\<^sub>\<beta>t2" 561 shows "t1\<longrightarrow>\<^sub>1\<^sup>*t2" 562 using a 563proof(induct) 564 case b1 thus ?case by (blast intro!: one_star_app_congL) 565next 566 case b2 thus ?case by (blast intro!: one_star_app_congR) 567next 568 case b3 thus ?case by (blast intro!: one_star_lam_cong) 569next 570 case b4 thus ?case by auto 571qed 572 573lemma trans_closure: 574 shows "(M1\<longrightarrow>\<^sub>1\<^sup>*M2) = (M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M2)" 575proof 576 assume "M1 \<longrightarrow>\<^sub>1\<^sup>* M2" 577 then show "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M2" 578 proof induct 579 case (os1 M1) thus "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M1" by simp 580 next 581 case (os2 M1 M2 M3) 582 have "M2\<longrightarrow>\<^sub>1M3" by fact 583 then have "M2\<longrightarrow>\<^sub>\<beta>\<^sup>*M3" by (rule one_beta_star) 584 moreover have "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M2" by fact 585 ultimately show "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M3" by (auto intro: beta_star_trans) 586 qed 587next 588 assume "M1 \<longrightarrow>\<^sub>\<beta>\<^sup>* M2" 589 then show "M1\<longrightarrow>\<^sub>1\<^sup>*M2" 590 proof induct 591 case (bs1 M1) thus "M1\<longrightarrow>\<^sub>1\<^sup>*M1" by simp 592 next 593 case (bs2 M1 M2 M3) 594 have "M2\<longrightarrow>\<^sub>\<beta>M3" by fact 595 then have "M2\<longrightarrow>\<^sub>1\<^sup>*M3" by (rule beta_one_star) 596 moreover have "M1\<longrightarrow>\<^sub>1\<^sup>*M2" by fact 597 ultimately show "M1\<longrightarrow>\<^sub>1\<^sup>*M3" by (auto intro: one_star_trans) 598 qed 599qed 600 601lemma cr_one: 602 assumes a: "t\<longrightarrow>\<^sub>1\<^sup>*t1" 603 and b: "t\<longrightarrow>\<^sub>1t2" 604 shows "\<exists>t3. t1\<longrightarrow>\<^sub>1t3 \<and> t2\<longrightarrow>\<^sub>1\<^sup>*t3" 605 using a b 606proof (induct arbitrary: t2) 607 case os1 thus ?case by force 608next 609 case (os2 t s1 s2 t2) 610 have b: "s1 \<longrightarrow>\<^sub>1 s2" by fact 611 have h: "\<And>t2. t \<longrightarrow>\<^sub>1 t2 \<Longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^sub>1 t3 \<and> t2 \<longrightarrow>\<^sub>1\<^sup>* t3)" by fact 612 have c: "t \<longrightarrow>\<^sub>1 t2" by fact 613 show "\<exists>t3. s2 \<longrightarrow>\<^sub>1 t3 \<and> t2 \<longrightarrow>\<^sub>1\<^sup>* t3" 614 proof - 615 from c h have "\<exists>t3. s1 \<longrightarrow>\<^sub>1 t3 \<and> t2 \<longrightarrow>\<^sub>1\<^sup>* t3" by blast 616 then obtain t3 where c1: "s1 \<longrightarrow>\<^sub>1 t3" and c2: "t2 \<longrightarrow>\<^sub>1\<^sup>* t3" by blast 617 have "\<exists>t4. s2 \<longrightarrow>\<^sub>1 t4 \<and> t3 \<longrightarrow>\<^sub>1 t4" using b c1 by (blast intro: diamond) 618 thus ?thesis using c2 by (blast intro: one_star_trans) 619 qed 620qed 621 622lemma cr_one_star: 623 assumes a: "t\<longrightarrow>\<^sub>1\<^sup>*t2" 624 and b: "t\<longrightarrow>\<^sub>1\<^sup>*t1" 625 shows "\<exists>t3. t1\<longrightarrow>\<^sub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^sub>1\<^sup>*t3" 626using a b 627proof (induct arbitrary: t1) 628 case (os1 t) then show ?case by force 629next 630 case (os2 t s1 s2 t1) 631 have c: "t \<longrightarrow>\<^sub>1\<^sup>* s1" by fact 632 have c': "t \<longrightarrow>\<^sub>1\<^sup>* t1" by fact 633 have d: "s1 \<longrightarrow>\<^sub>1 s2" by fact 634 have "t \<longrightarrow>\<^sub>1\<^sup>* t1 \<Longrightarrow> (\<exists>t3. t1 \<longrightarrow>\<^sub>1\<^sup>* t3 \<and> s1 \<longrightarrow>\<^sub>1\<^sup>* t3)" by fact 635 then obtain t3 where f1: "t1 \<longrightarrow>\<^sub>1\<^sup>* t3" 636 and f2: "s1 \<longrightarrow>\<^sub>1\<^sup>* t3" using c' by blast 637 from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^sub>1t4 \<and> s2\<longrightarrow>\<^sub>1\<^sup>*t4" by blast 638 then obtain t4 where g1: "t3\<longrightarrow>\<^sub>1t4" 639 and g2: "s2\<longrightarrow>\<^sub>1\<^sup>*t4" by blast 640 have "t1\<longrightarrow>\<^sub>1\<^sup>*t4" using f1 g1 by (blast intro: one_star_trans) 641 thus ?case using g2 by blast 642qed 643 644lemma cr_beta_star: 645 assumes a1: "t\<longrightarrow>\<^sub>\<beta>\<^sup>*t1" 646 and a2: "t\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 647 shows "\<exists>t3. t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^sub>\<beta>\<^sup>*t3" 648proof - 649 from a1 have "t\<longrightarrow>\<^sub>1\<^sup>*t1" by (simp only: trans_closure) 650 moreover 651 from a2 have "t\<longrightarrow>\<^sub>1\<^sup>*t2" by (simp only: trans_closure) 652 ultimately have "\<exists>t3. t1\<longrightarrow>\<^sub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^sub>1\<^sup>*t3" by (blast intro: cr_one_star) 653 then obtain t3 where "t1\<longrightarrow>\<^sub>1\<^sup>*t3" and "t2\<longrightarrow>\<^sub>1\<^sup>*t3" by blast 654 hence "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t3" and "t2\<longrightarrow>\<^sub>\<beta>\<^sup>*t3" by (simp_all only: trans_closure) 655 then show "\<exists>t3. t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^sub>\<beta>\<^sup>*t3" by blast 656qed 657 658end 659 660