theory CR imports Lam_Funs begin text ‹The Church-Rosser proof from Barendregt's book› lemma forget: assumes asm: "x♯L" shows "L[x::=P] = L" using asm proof (nominal_induct L avoiding: x P rule: lam.strong_induct) case (Var z) have "x♯Var z" by fact thus "(Var z)[x::=P] = (Var z)" by (simp add: fresh_atm) next case (App M1 M2) have "x♯App M1 M2" by fact moreover have ih1: "x♯M1 ⟹ M1[x::=P] = M1" by fact moreover have ih1: "x♯M2 ⟹ M2[x::=P] = M2" by fact ultimately show "(App M1 M2)[x::=P] = (App M1 M2)" by simp next case (Lam z M) have vc: "z♯x" "z♯P" by fact+ have ih: "x♯M ⟹ M[x::=P] = M" by fact have asm: "x♯Lam [z].M" by fact then have "x♯M" using vc by (simp add: fresh_atm abs_fresh) then have "M[x::=P] = M" using ih by simp then show "(Lam [z].M)[x::=P] = Lam [z].M" using vc by simp qed lemma forget_automatic: assumes asm: "x♯L" shows "L[x::=P] = L" using asm by (nominal_induct L avoiding: x P rule: lam.strong_induct) (auto simp add: abs_fresh fresh_atm) lemma fresh_fact: fixes z::"name" assumes asms: "z♯N" "z♯L" shows "z♯(N[y::=L])" using asms proof (nominal_induct N avoiding: z y L rule: lam.strong_induct) case (Var u) have "z♯(Var u)" "z♯L" by fact+ thus "z♯((Var u)[y::=L])" by simp next case (App N1 N2) have ih1: "⟦z♯N1; z♯L⟧ ⟹ z♯N1[y::=L]" by fact moreover have ih2: "⟦z♯N2; z♯L⟧ ⟹ z♯N2[y::=L]" by fact moreover have "z♯App N1 N2" "z♯L" by fact+ ultimately show "z♯((App N1 N2)[y::=L])" by simp next case (Lam u N1) have vc: "u♯z" "u♯y" "u♯L" by fact+ have "z♯Lam [u].N1" by fact hence "z♯N1" using vc by (simp add: abs_fresh fresh_atm) moreover have ih: "⟦z♯N1; z♯L⟧ ⟹ z♯(N1[y::=L])" by fact moreover have "z♯L" by fact ultimately show "z♯(Lam [u].N1)[y::=L]" using vc by (simp add: abs_fresh) qed lemma fresh_fact_automatic: fixes z::"name" assumes asms: "z♯N" "z♯L" shows "z♯(N[y::=L])" using asms by (nominal_induct N avoiding: z y L rule: lam.strong_induct) (auto simp add: abs_fresh fresh_atm) lemma fresh_fact': fixes a::"name" assumes a: "a♯t2" shows "a♯t1[a::=t2]" using a by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) (auto simp add: abs_fresh fresh_atm) lemma substitution_lemma: assumes a: "x≠y" and b: "x♯L" shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" using a b proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct) case (Var z) (* case 1: Variables*) have "x≠y" by fact have "x♯L" by fact show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS") proof - { (*Case 1.1*) assume "z=x" have "(1)": "?LHS = N[y::=L]" using ‹z=x› by simp have "(2)": "?RHS = N[y::=L]" using ‹z=x› ‹x≠y› by simp from "(1)" "(2)" have "?LHS = ?RHS" by simp } moreover { (*Case 1.2*) assume "z=y" and "z≠x" have "(1)": "?LHS = L" using ‹z≠x› ‹z=y› by simp have "(2)": "?RHS = L[x::=N[y::=L]]" using ‹z=y› by simp have "(3)": "L[x::=N[y::=L]] = L" using ‹x♯L› by (simp add: forget) from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp } moreover { (*Case 1.3*) assume "z≠x" and "z≠y" have "(1)": "?LHS = Var z" using ‹z≠x› ‹z≠y› by simp have "(2)": "?RHS = Var z" using ‹z≠x› ‹z≠y› by simp from "(1)" "(2)" have "?LHS = ?RHS" by simp } ultimately show "?LHS = ?RHS" by blast qed next case (Lam z M1) (* case 2: lambdas *) have ih: "⟦x≠y; x♯L⟧ ⟹ M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact have "x≠y" by fact have "x♯L" by fact have fs: "z♯x" "z♯y" "z♯N" "z♯L" by fact+ hence "z♯N[y::=L]" by (simp add: fresh_fact) show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") proof - have "?LHS = Lam [z].(M1[x::=N][y::=L])" using ‹z♯x› ‹z♯y› ‹z♯N› ‹z♯L› by simp also from ih have "… = Lam [z].(M1[y::=L][x::=N[y::=L]])" using ‹x≠y› ‹x♯L› by simp also have "… = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using ‹z♯x› ‹z♯N[y::=L]› by simp also have "… = ?RHS" using ‹z♯y› ‹z♯L› by simp finally show "?LHS = ?RHS" . qed next case (App M1 M2) (* case 3: applications *) thus "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp qed lemma substitution_lemma_automatic: assumes asm: "x≠y" "x♯L" shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" using asm by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) (auto simp add: fresh_fact forget) section ‹Beta Reduction› inductive "Beta" :: "lam⇒lam⇒bool" (" _ ⟶⇩_{β}_" [80,80] 80) where b1[intro]: "s1⟶⇩_{β}s2 ⟹ (App s1 t)⟶⇩_{β}(App s2 t)" | b2[intro]: "s1⟶⇩_{β}s2 ⟹ (App t s1)⟶⇩_{β}(App t s2)" | b3[intro]: "s1⟶⇩_{β}s2 ⟹ (Lam [a].s1)⟶⇩_{β}(Lam [a].s2)" | b4[intro]: "a♯s2 ⟹ (App (Lam [a].s1) s2)⟶⇩_{β}(s1[a::=s2])" equivariance Beta nominal_inductive Beta by (simp_all add: abs_fresh fresh_fact') inductive "Beta_star" :: "lam⇒lam⇒bool" (" _ ⟶⇩_{β}⇧^{*}_" [80,80] 80) where bs1[intro, simp]: "M ⟶⇩_{β}⇧^{*}M" | bs2[intro]: "⟦M1⟶⇩_{β}⇧^{*}M2; M2 ⟶⇩_{β}M3⟧ ⟹ M1 ⟶⇩_{β}⇧^{*}M3" equivariance Beta_star lemma beta_star_trans: assumes a1: "M1⟶⇩_{β}⇧^{*}M2" and a2: "M2⟶⇩_{β}⇧^{*}M3" shows "M1 ⟶⇩_{β}⇧^{*}M3" using a2 a1 by (induct) (auto) section ‹One-Reduction› inductive One :: "lam⇒lam⇒bool" (" _ ⟶⇩_{1}_" [80,80] 80) where o1[intro!]: "M⟶⇩_{1}M" | o2[simp,intro!]: "⟦t1⟶⇩_{1}t2;s1⟶⇩_{1}s2⟧ ⟹ (App t1 s1)⟶⇩_{1}(App t2 s2)" | o3[simp,intro!]: "s1⟶⇩_{1}s2 ⟹ (Lam [a].s1)⟶⇩_{1}(Lam [a].s2)" | o4[simp,intro!]: "⟦a♯(s1,s2); s1⟶⇩_{1}s2;t1⟶⇩_{1}t2⟧ ⟹ (App (Lam [a].t1) s1)⟶⇩_{1}(t2[a::=s2])" equivariance One nominal_inductive One by (simp_all add: abs_fresh fresh_fact') inductive "One_star" :: "lam⇒lam⇒bool" (" _ ⟶⇩_{1}⇧^{*}_" [80,80] 80) where os1[intro, simp]: "M ⟶⇩_{1}⇧^{*}M" | os2[intro]: "⟦M1⟶⇩_{1}⇧^{*}M2; M2 ⟶⇩_{1}M3⟧ ⟹ M1 ⟶⇩_{1}⇧^{*}M3" equivariance One_star lemma one_star_trans: assumes a1: "M1⟶⇩_{1}⇧^{*}M2" and a2: "M2⟶⇩_{1}⇧^{*}M3" shows "M1⟶⇩_{1}⇧^{*}M3" using a2 a1 by (induct) (auto) lemma one_fresh_preserv: fixes a :: "name" assumes a: "t⟶⇩_{1}s" and b: "a♯t" shows "a♯s" using a b proof (induct) case o1 thus ?case by simp next case o2 thus ?case by simp next case (o3 s1 s2 c) have ih: "a♯s1 ⟹ a♯s2" by fact have c: "a♯Lam [c].s1" by fact show ?case proof (cases "a=c") assume "a=c" thus "a♯Lam [c].s2" by (simp add: abs_fresh) next assume d: "a≠c" with c have "a♯s1" by (simp add: abs_fresh) hence "a♯s2" using ih by simp thus "a♯Lam [c].s2" using d by (simp add: abs_fresh) qed next case (o4 c t1 t2 s1 s2) have i1: "a♯t1 ⟹ a♯t2" by fact have i2: "a♯s1 ⟹ a♯s2" by fact have as: "a♯App (Lam [c].s1) t1" by fact hence c1: "a♯Lam [c].s1" and c2: "a♯t1" by (simp add: fresh_prod)+ from c2 i1 have c3: "a♯t2" by simp show "a♯s2[c::=t2]" proof (cases "a=c") assume "a=c" thus "a♯s2[c::=t2]" using c3 by (simp add: fresh_fact') next assume d1: "a≠c" from c1 d1 have "a♯s1" by (simp add: abs_fresh) hence "a♯s2" using i2 by simp thus "a♯s2[c::=t2]" using c3 by (simp add: fresh_fact) qed qed lemma one_fresh_preserv_automatic: fixes a :: "name" assumes a: "t⟶⇩_{1}s" and b: "a♯t" shows "a♯s" using a b apply(nominal_induct avoiding: a rule: One.strong_induct) apply(auto simp add: abs_fresh fresh_atm fresh_fact) done lemma subst_rename: assumes a: "c♯t1" shows "t1[a::=t2] = ([(c,a)]∙t1)[c::=t2]" using a by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct) (auto simp add: calc_atm fresh_atm abs_fresh) lemma one_abs: assumes a: "Lam [a].t⟶⇩_{1}t'" shows "∃t''. t'=Lam [a].t'' ∧ t⟶⇩_{1}t''" proof - have "a♯Lam [a].t" by (simp add: abs_fresh) with a have "a♯t'" by (simp add: one_fresh_preserv) with a show ?thesis by (cases rule: One.strong_cases[where a="a" and aa="a"]) (auto simp add: lam.inject abs_fresh alpha) qed lemma one_app: assumes a: "App t1 t2 ⟶⇩_{1}t'" shows "(∃s1 s2. t' = App s1 s2 ∧ t1 ⟶⇩_{1}s1 ∧ t2 ⟶⇩_{1}s2) ∨ (∃a s s1 s2. t1 = Lam [a].s ∧ t' = s1[a::=s2] ∧ s ⟶⇩_{1}s1 ∧ t2 ⟶⇩_{1}s2 ∧ a♯(t2,s2))" using a by (erule_tac One.cases) (auto simp add: lam.inject) lemma one_red: assumes a: "App (Lam [a].t1) t2 ⟶⇩_{1}M" "a♯(t2,M)" shows "(∃s1 s2. M = App (Lam [a].s1) s2 ∧ t1 ⟶⇩_{1}s1 ∧ t2 ⟶⇩_{1}s2) ∨ (∃s1 s2. M = s1[a::=s2] ∧ t1 ⟶⇩_{1}s1 ∧ t2 ⟶⇩_{1}s2)" using a by (cases rule: One.strong_cases [where a="a" and aa="a"]) (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod) text ‹first case in Lemma 3.2.4› lemma one_subst_aux: assumes a: "N⟶⇩_{1}N'" shows "M[x::=N] ⟶⇩_{1}M[x::=N']" using a proof (nominal_induct M avoiding: x N N' rule: lam.strong_induct) case (Var y) thus "Var y[x::=N] ⟶⇩_{1}Var y[x::=N']" by (cases "x=y") auto next case (App P Q) (* application case - third line *) thus "(App P Q)[x::=N] ⟶⇩_{1}(App P Q)[x::=N']" using o2 by simp next case (Lam y P) (* abstraction case - fourth line *) thus "(Lam [y].P)[x::=N] ⟶⇩_{1}(Lam [y].P)[x::=N']" using o3 by simp qed lemma one_subst_aux_automatic: assumes a: "N⟶⇩_{1}N'" shows "M[x::=N] ⟶⇩_{1}M[x::=N']" using a by (nominal_induct M avoiding: x N N' rule: lam.strong_induct) (auto simp add: fresh_prod fresh_atm) lemma one_subst: assumes a: "M⟶⇩_{1}M'" and b: "N⟶⇩_{1}N'" shows "M[x::=N]⟶⇩_{1}M'[x::=N']" using a b proof (nominal_induct M M' avoiding: N N' x rule: One.strong_induct) case (o1 M) thus ?case by (simp add: one_subst_aux) next case (o2 M1 M2 N1 N2) thus ?case by simp next case (o3 a M1 M2) thus ?case by simp next case (o4 a N1 N2 M1 M2 N N' x) have vc: "a♯N" "a♯N'" "a♯x" "a♯N1" "a♯N2" by fact+ have asm: "N⟶⇩_{1}N'" by fact show ?case proof - have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using vc by simp moreover have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) ⟶⇩_{1}M2[x::=N'][a::=N2[x::=N']]" using o4 asm by (simp add: fresh_fact) moreover have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" using vc by (simp add: substitution_lemma fresh_atm) ultimately show "(App (Lam [a].M1) N1)[x::=N] ⟶⇩_{1}M2[a::=N2][x::=N']" by simp qed qed lemma one_subst_automatic: assumes a: "M⟶⇩_{1}M'" and b: "N⟶⇩_{1}N'" shows "M[x::=N]⟶⇩_{1}M'[x::=N']" using a b by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct) (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact) lemma diamond[rule_format]: fixes M :: "lam" and M1:: "lam" assumes a: "M⟶⇩_{1}M1" and b: "M⟶⇩_{1}M2" shows "∃M3. M1⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" using a b proof (nominal_induct avoiding: M1 M2 rule: One.strong_induct) case (o1 M) (* case 1 --- M1 = M *) thus "∃M3. M⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" by blast next case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*) have vc: "x♯Q" "x♯Q'" "x♯M2" by fact+ have i1: "⋀M2. Q ⟶⇩_{1}M2 ⟹ (∃M3. Q'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3)" by fact have i2: "⋀M2. P ⟶⇩_{1}M2 ⟹ (∃M3. P'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3)" by fact have "App (Lam [x].P) Q ⟶⇩_{1}M2" by fact hence "(∃P' Q'. M2 = App (Lam [x].P') Q' ∧ P⟶⇩_{1}P' ∧ Q⟶⇩_{1}Q') ∨ (∃P' Q'. M2 = P'[x::=Q'] ∧ P⟶⇩_{1}P' ∧ Q⟶⇩_{1}Q')" using vc by (simp add: one_red) moreover (* subcase 2.1 *) { assume "∃P' Q'. M2 = App (Lam [x].P') Q' ∧ P⟶⇩_{1}P' ∧ Q⟶⇩_{1}Q'" then obtain P'' and Q'' where b1: "M2=App (Lam [x].P'') Q''" and b2: "P⟶⇩_{1}P''" and b3: "Q⟶⇩_{1}Q''" by blast from b2 i2 have "(∃M3. P'⟶⇩_{1}M3 ∧ P''⟶⇩_{1}M3)" by simp then obtain P''' where c1: "P'⟶⇩_{1}P'''" and c2: "P''⟶⇩_{1}P'''" by force from b3 i1 have "(∃M3. Q'⟶⇩_{1}M3 ∧ Q''⟶⇩_{1}M3)" by simp then obtain Q''' where d1: "Q'⟶⇩_{1}Q'''" and d2: "Q''⟶⇩_{1}Q'''" by force from c1 c2 d1 d2 have "P'[x::=Q']⟶⇩_{1}P'''[x::=Q'''] ∧ App (Lam [x].P'') Q'' ⟶⇩_{1}P'''[x::=Q''']" using vc b3 by (auto simp add: one_subst one_fresh_preserv) hence "∃M3. P'[x::=Q']⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" using b1 by blast } moreover (* subcase 2.2 *) { assume "∃P' Q'. M2 = P'[x::=Q'] ∧ P⟶⇩_{1}P' ∧ Q⟶⇩_{1}Q'" then obtain P'' Q'' where b1: "M2=P''[x::=Q'']" and b2: "P⟶⇩_{1}P''" and b3: "Q⟶⇩_{1}Q''" by blast from b2 i2 have "(∃M3. P'⟶⇩_{1}M3 ∧ P''⟶⇩_{1}M3)" by simp then obtain P''' where c1: "P'⟶⇩_{1}P'''" and c2: "P''⟶⇩_{1}P'''" by blast from b3 i1 have "(∃M3. Q'⟶⇩_{1}M3 ∧ Q''⟶⇩_{1}M3)" by simp then obtain Q''' where d1: "Q'⟶⇩_{1}Q'''" and d2: "Q''⟶⇩_{1}Q'''" by blast from c1 c2 d1 d2 have "P'[x::=Q']⟶⇩_{1}P'''[x::=Q'''] ∧ P''[x::=Q'']⟶⇩_{1}P'''[x::=Q''']" by (force simp add: one_subst) hence "∃M3. P'[x::=Q']⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" using b1 by blast } ultimately show "∃M3. P'[x::=Q']⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" by blast next case (o2 P P' Q Q') (* case 3 *) have i0: "P⟶⇩_{1}P'" by fact have i0': "Q⟶⇩_{1}Q'" by fact have i1: "⋀M2. Q ⟶⇩_{1}M2 ⟹ (∃M3. Q'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3)" by fact have i2: "⋀M2. P ⟶⇩_{1}M2 ⟹ (∃M3. P'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3)" by fact assume "App P Q ⟶⇩_{1}M2" hence "(∃P'' Q''. M2 = App P'' Q'' ∧ P⟶⇩_{1}P'' ∧ Q⟶⇩_{1}Q'') ∨ (∃x P' P'' Q'. P = Lam [x].P' ∧ M2 = P''[x::=Q'] ∧ P'⟶⇩_{1}P'' ∧ Q⟶⇩_{1}Q' ∧ x♯(Q,Q'))" by (simp add: one_app[simplified]) moreover (* subcase 3.1 *) { assume "∃P'' Q''. M2 = App P'' Q'' ∧ P⟶⇩_{1}P'' ∧ Q⟶⇩_{1}Q''" then obtain P'' and Q'' where b1: "M2=App P'' Q''" and b2: "P⟶⇩_{1}P''" and b3: "Q⟶⇩_{1}Q''" by blast from b2 i2 have "(∃M3. P'⟶⇩_{1}M3 ∧ P''⟶⇩_{1}M3)" by simp then obtain P''' where c1: "P'⟶⇩_{1}P'''" and c2: "P''⟶⇩_{1}P'''" by blast from b3 i1 have "∃M3. Q'⟶⇩_{1}M3 ∧ Q''⟶⇩_{1}M3" by simp then obtain Q''' where d1: "Q'⟶⇩_{1}Q'''" and d2: "Q''⟶⇩_{1}Q'''" by blast from c1 c2 d1 d2 have "App P' Q'⟶⇩_{1}App P''' Q''' ∧ App P'' Q'' ⟶⇩_{1}App P''' Q'''" by blast hence "∃M3. App P' Q'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" using b1 by blast } moreover (* subcase 3.2 *) { assume "∃x P1 P'' Q''. P = Lam [x].P1 ∧ M2 = P''[x::=Q''] ∧ P1⟶⇩_{1}P'' ∧ Q⟶⇩_{1}Q'' ∧ x♯(Q,Q'')" then obtain x P1 P1'' Q'' where b0: "P = Lam [x].P1" and b1: "M2 = P1''[x::=Q'']" and b2: "P1⟶⇩_{1}P1''" and b3: "Q⟶⇩_{1}Q''" and vc: "x♯(Q,Q'')" by blast from b0 i0 have "∃P1'. P'=Lam [x].P1' ∧ P1⟶⇩_{1}P1'" by (simp add: one_abs) then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1⟶⇩_{1}P1'" by blast from g1 b0 b2 i2 have "(∃M3. (Lam [x].P1')⟶⇩_{1}M3 ∧ (Lam [x].P1'')⟶⇩_{1}M3)" by simp then obtain P1''' where c1: "(Lam [x].P1')⟶⇩_{1}P1'''" and c2: "(Lam [x].P1'')⟶⇩_{1}P1'''" by blast from c1 have "∃R1. P1'''=Lam [x].R1 ∧ P1'⟶⇩_{1}R1" by (simp add: one_abs) then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'⟶⇩_{1}R1" by blast from c2 have "∃R2. P1'''=Lam [x].R2 ∧ P1''⟶⇩_{1}R2" by (simp add: one_abs) then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''⟶⇩_{1}R2" by blast from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) from b3 i1 have "(∃M3. Q'⟶⇩_{1}M3 ∧ Q''⟶⇩_{1}M3)" by simp then obtain Q''' where d1: "Q'⟶⇩_{1}Q'''" and d2: "Q''⟶⇩_{1}Q'''" by blast from g1 r2 d1 r4 r5 d2 have "App P' Q'⟶⇩_{1}R1[x::=Q'''] ∧ P1''[x::=Q'']⟶⇩_{1}R1[x::=Q''']" using vc i0' by (simp add: one_subst one_fresh_preserv) hence "∃M3. App P' Q'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" using b1 by blast } ultimately show "∃M3. App P' Q'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" by blast next case (o3 P P' x) (* case 4 *) have i1: "P⟶⇩_{1}P'" by fact have i2: "⋀M2. P ⟶⇩_{1}M2 ⟹ (∃M3. P'⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3)" by fact have "(Lam [x].P)⟶⇩_{1}M2" by fact hence "∃P''. M2=Lam [x].P'' ∧ P⟶⇩_{1}P''" by (simp add: one_abs) then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P⟶⇩_{1}P''" by blast from i2 b1 b2 have "∃M3. (Lam [x].P')⟶⇩_{1}M3 ∧ (Lam [x].P'')⟶⇩_{1}M3" by blast then obtain M3 where c1: "(Lam [x].P')⟶⇩_{1}M3" and c2: "(Lam [x].P'')⟶⇩_{1}M3" by blast from c1 have "∃R1. M3=Lam [x].R1 ∧ P'⟶⇩_{1}R1" by (simp add: one_abs) then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'⟶⇩_{1}R1" by blast from c2 have "∃R2. M3=Lam [x].R2 ∧ P''⟶⇩_{1}R2" by (simp add: one_abs) then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''⟶⇩_{1}R2" by blast from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) from r2 r4 have "(Lam [x].P')⟶⇩_{1}(Lam [x].R1) ∧ (Lam [x].P'')⟶⇩_{1}(Lam [x].R2)" by (simp add: one_subst) thus "∃M3. (Lam [x].P')⟶⇩_{1}M3 ∧ M2⟶⇩_{1}M3" using b1 r5 by blast qed lemma one_lam_cong: assumes a: "t1⟶⇩_{β}⇧^{*}t2" shows "(Lam [a].t1)⟶⇩_{β}⇧^{*}(Lam [a].t2)" using a proof induct case bs1 thus ?case by simp next case (bs2 y z) thus ?case by (blast dest: b3) qed lemma one_app_congL: assumes a: "t1⟶⇩_{β}⇧^{*}t2" shows "App t1 s⟶⇩_{β}⇧^{*}App t2 s" using a proof induct case bs1 thus ?case by simp next case bs2 thus ?case by (blast dest: b1) qed lemma one_app_congR: assumes a: "t1⟶⇩_{β}⇧^{*}t2" shows "App s t1 ⟶⇩_{β}⇧^{*}App s t2" using a proof induct case bs1 thus ?case by simp next case bs2 thus ?case by (blast dest: b2) qed lemma one_app_cong: assumes a1: "t1⟶⇩_{β}⇧^{*}t2" and a2: "s1⟶⇩_{β}⇧^{*}s2" shows "App t1 s1⟶⇩_{β}⇧^{*}App t2 s2" proof - have "App t1 s1 ⟶⇩_{β}⇧^{*}App t2 s1" using a1 by (rule one_app_congL) moreover have "App t2 s1 ⟶⇩_{β}⇧^{*}App t2 s2" using a2 by (rule one_app_congR) ultimately show ?thesis by (rule beta_star_trans) qed lemma one_beta_star: assumes a: "(t1⟶⇩_{1}t2)" shows "(t1⟶⇩_{β}⇧^{*}t2)" using a proof(nominal_induct rule: One.strong_induct) case o1 thus ?case by simp next case o2 thus ?case by (blast intro!: one_app_cong) next case o3 thus ?case by (blast intro!: one_lam_cong) next case (o4 a s1 s2 t1 t2) have vc: "a♯s1" "a♯s2" by fact+ have a1: "t1⟶⇩_{β}⇧^{*}t2" and a2: "s1⟶⇩_{β}⇧^{*}s2" by fact+ have c1: "(App (Lam [a].t2) s2) ⟶⇩_{β}(t2 [a::= s2])" using vc by (simp add: b4) from a1 a2 have c2: "App (Lam [a].t1 ) s1 ⟶⇩_{β}⇧^{*}App (Lam [a].t2 ) s2" by (blast intro!: one_app_cong one_lam_cong) show ?case using c2 c1 by (blast intro: beta_star_trans) qed lemma one_star_lam_cong: assumes a: "t1⟶⇩_{1}⇧^{*}t2" shows "(Lam [a].t1)⟶⇩_{1}⇧^{*}(Lam [a].t2)" using a proof induct case os1 thus ?case by simp next case os2 thus ?case by (blast intro: one_star_trans) qed lemma one_star_app_congL: assumes a: "t1⟶⇩_{1}⇧^{*}t2" shows "App t1 s⟶⇩_{1}⇧^{*}App t2 s" using a proof induct case os1 thus ?case by simp next case os2 thus ?case by (blast intro: one_star_trans) qed lemma one_star_app_congR: assumes a: "t1⟶⇩_{1}⇧^{*}t2" shows "App s t1 ⟶⇩_{1}⇧^{*}App s t2" using a proof induct case os1 thus ?case by simp next case os2 thus ?case by (blast intro: one_star_trans) qed lemma beta_one_star: assumes a: "t1⟶⇩_{β}t2" shows "t1⟶⇩_{1}⇧^{*}t2" using a proof(induct) case b1 thus ?case by (blast intro!: one_star_app_congL) next case b2 thus ?case by (blast intro!: one_star_app_congR) next case b3 thus ?case by (blast intro!: one_star_lam_cong) next case b4 thus ?case by auto qed lemma trans_closure: shows "(M1⟶⇩_{1}⇧^{*}M2) = (M1⟶⇩_{β}⇧^{*}M2)" proof assume "M1 ⟶⇩_{1}⇧^{*}M2" then show "M1⟶⇩_{β}⇧^{*}M2" proof induct case (os1 M1) thus "M1⟶⇩_{β}⇧^{*}M1" by simp next case (os2 M1 M2 M3) have "M2⟶⇩_{1}M3" by fact then have "M2⟶⇩_{β}⇧^{*}M3" by (rule one_beta_star) moreover have "M1⟶⇩_{β}⇧^{*}M2" by fact ultimately show "M1⟶⇩_{β}⇧^{*}M3" by (auto intro: beta_star_trans) qed next assume "M1 ⟶⇩_{β}⇧^{*}M2" then show "M1⟶⇩_{1}⇧^{*}M2" proof induct case (bs1 M1) thus "M1⟶⇩_{1}⇧^{*}M1" by simp next case (bs2 M1 M2 M3) have "M2⟶⇩_{β}M3" by fact then have "M2⟶⇩_{1}⇧^{*}M3" by (rule beta_one_star) moreover have "M1⟶⇩_{1}⇧^{*}M2" by fact ultimately show "M1⟶⇩_{1}⇧^{*}M3" by (auto intro: one_star_trans) qed qed lemma cr_one: assumes a: "t⟶⇩_{1}⇧^{*}t1" and b: "t⟶⇩_{1}t2" shows "∃t3. t1⟶⇩_{1}t3 ∧ t2⟶⇩_{1}⇧^{*}t3" using a b proof (induct arbitrary: t2) case os1 thus ?case by force next case (os2 t s1 s2 t2) have b: "s1 ⟶⇩_{1}s2" by fact have h: "⋀t2. t ⟶⇩_{1}t2 ⟹ (∃t3. s1 ⟶⇩_{1}t3 ∧ t2 ⟶⇩_{1}⇧^{*}t3)" by fact have c: "t ⟶⇩_{1}t2" by fact show "∃t3. s2 ⟶⇩_{1}t3 ∧ t2 ⟶⇩_{1}⇧^{*}t3" proof - from c h have "∃t3. s1 ⟶⇩_{1}t3 ∧ t2 ⟶⇩_{1}⇧^{*}t3" by blast then obtain t3 where c1: "s1 ⟶⇩_{1}t3" and c2: "t2 ⟶⇩_{1}⇧^{*}t3" by blast have "∃t4. s2 ⟶⇩_{1}t4 ∧ t3 ⟶⇩_{1}t4" using b c1 by (blast intro: diamond) thus ?thesis using c2 by (blast intro: one_star_trans) qed qed lemma cr_one_star: assumes a: "t⟶⇩_{1}⇧^{*}t2" and b: "t⟶⇩_{1}⇧^{*}t1" shows "∃t3. t1⟶⇩_{1}⇧^{*}t3∧t2⟶⇩_{1}⇧^{*}t3" using a b proof (induct arbitrary: t1) case (os1 t) then show ?case by force next case (os2 t s1 s2 t1) have c: "t ⟶⇩_{1}⇧^{*}s1" by fact have c': "t ⟶⇩_{1}⇧^{*}t1" by fact have d: "s1 ⟶⇩_{1}s2" by fact have "t ⟶⇩_{1}⇧^{*}t1 ⟹ (∃t3. t1 ⟶⇩_{1}⇧^{*}t3 ∧ s1 ⟶⇩_{1}⇧^{*}t3)" by fact then obtain t3 where f1: "t1 ⟶⇩_{1}⇧^{*}t3" and f2: "s1 ⟶⇩_{1}⇧^{*}t3" using c' by blast from cr_one d f2 have "∃t4. t3⟶⇩_{1}t4 ∧ s2⟶⇩_{1}⇧^{*}t4" by blast then obtain t4 where g1: "t3⟶⇩_{1}t4" and g2: "s2⟶⇩_{1}⇧^{*}t4" by blast have "t1⟶⇩_{1}⇧^{*}t4" using f1 g1 by (blast intro: one_star_trans) thus ?case using g2 by blast qed lemma cr_beta_star: assumes a1: "t⟶⇩_{β}⇧^{*}t1" and a2: "t⟶⇩_{β}⇧^{*}t2" shows "∃t3. t1⟶⇩_{β}⇧^{*}t3∧t2⟶⇩_{β}⇧^{*}t3" proof - from a1 have "t⟶⇩_{1}⇧^{*}t1" by (simp only: trans_closure) moreover from a2 have "t⟶⇩_{1}⇧^{*}t2" by (simp only: trans_closure) ultimately have "∃t3. t1⟶⇩_{1}⇧^{*}t3 ∧ t2⟶⇩_{1}⇧^{*}t3" by (blast intro: cr_one_star) then obtain t3 where "t1⟶⇩_{1}⇧^{*}t3" and "t2⟶⇩_{1}⇧^{*}t3" by blast hence "t1⟶⇩_{β}⇧^{*}t3" and "t2⟶⇩_{β}⇧^{*}t3" by (simp_all only: trans_closure) then show "∃t3. t1⟶⇩_{β}⇧^{*}t3∧t2⟶⇩_{β}⇧^{*}t3" by blast qed end