lemma ty_cases: fixes T::ty shows"(∃s. T=PR s) ∨ (∃T'. T=NOT T') ∨ (∃S U. T=S OR U) ∨ (∃S U. T=S AND U) ∨ (∃S U. T=S IMP U)" by (induct T rule:ty.induct) (auto)
lemma fresh_ty: fixes a::"coname" and x::"name" and T::"ty" shows"a♯T"and"x♯T" by (nominal_induct T rule: ty.strong_induct)
(auto simp: fresh_string)
lemmas eq_bij = pt_bij[OF pt_name_inst, OF at_name_inst] pt_bij[OF pt_coname_inst, OF at_coname_inst]
lemma crename_name_eqvt[eqvt]: fixes pi::"name prm" shows"pi∙(M[d⊨c>e]) = (pi∙M)[(pi∙d)⊨c>(pi∙e)]" by (nominal_induct M avoiding: d e rule: trm.strong_induct) (auto simp: fresh_bij eq_bij)
lemma crename_coname_eqvt[eqvt]: fixes pi::"coname prm" shows"pi∙(M[d⊨c>e]) = (pi∙M)[(pi∙d)⊨c>(pi∙e)]" by (nominal_induct M avoiding: d e rule: trm.strong_induct)(auto simp: fresh_bij eq_bij)
lemma nrename_name_eqvt[eqvt]: fixes pi::"name prm" shows"pi∙(M[x⊨n>y]) = (pi∙M)[(pi∙x)⊨n>(pi∙y)]" by(nominal_induct M avoiding: x y rule: trm.strong_induct) (auto simp: fresh_bij eq_bij)
lemma nrename_coname_eqvt[eqvt]: fixes pi::"coname prm" shows"pi∙(M[x⊨n>y]) = (pi∙M)[(pi∙x)⊨n>(pi∙y)]" by(nominal_induct M avoiding: x y rule: trm.strong_induct)(auto simp: fresh_bij eq_bij)
lemmas rename_eqvts = crename_name_eqvt crename_coname_eqvt
nrename_name_eqvt nrename_coname_eqvt lemma nrename_fresh: assumes a: "x♯M" shows"M[x⊨n>y] = M" using a by (nominal_induct M avoiding: x y rule: trm.strong_induct)
(auto simp: trm.inject fresh_atm abs_fresh fin_supp abs_supp)
lemma crename_fresh: assumes a: "a♯M" shows"M[a⊨c>b] = M" using a by (nominal_induct M avoiding: a b rule: trm.strong_induct)
(auto simp: trm.inject fresh_atm abs_fresh)
lemma nrename_nfresh: fixes x::"name" shows"x♯y==>x♯M[x⊨n>y]" by (nominal_induct M avoiding: x y rule: trm.strong_induct)
(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
lemma crename_nfresh: fixes x::"name" shows"x♯M==>x♯M[a⊨c>b]" by (nominal_induct M avoiding: a b rule: trm.strong_induct)
(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
lemma crename_cfresh: fixes a::"coname" shows"a♯b==>a♯M[a⊨c>b]" by (nominal_induct M avoiding: a b rule: trm.strong_induct)
(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
lemma nrename_cfresh: fixes c::"coname" shows"c♯M==>c♯M[x⊨n>y]" by (nominal_induct M avoiding: x y rule: trm.strong_induct)
(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
lemma nrename_nfresh': fixes x::"name" shows"x♯(M,z,y)==>x♯M[z⊨n>y]" by (nominal_induct M avoiding: x z y rule: trm.strong_induct)
(auto simp: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
lemma crename_cfresh': fixes a::"coname" shows"a♯(M,b,c)==>a♯M[b⊨c>c]" by (nominal_induct M avoiding: a b c rule: trm.strong_induct)
(auto simp: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
lemma nrename_rename: assumes a: "x'♯M" shows"([(x',x)]∙M)[x'⊨n>y]= M[x⊨n>y]" using a proof (nominal_induct M avoiding: x x' y rule: trm.strong_induct) qed (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
lemma crename_rename: assumes a: "a'♯M" shows"([(a',a)]∙M)[a'⊨c>b]= M[a⊨c>b]" using a proof (nominal_induct M avoiding: a a' b rule: trm.strong_induct) qed (auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
lemma crename_id: shows"M[a⊨c>a] = M" by (nominal_induct M avoiding: a rule: trm.strong_induct) (auto)
lemma nrename_id: shows"M[x⊨n>x] = M" by (nominal_induct M avoiding: x rule: trm.strong_induct) (auto)
lemma nrename_swap: shows"x♯M ==> [(x,y)]∙M = M[y⊨n>x]" by (nominal_induct M avoiding: x y rule: trm.strong_induct)
(auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
lemma crename_swap: shows"a♯M ==> [(a,b)]∙M = M[b⊨c>a]" by (nominal_induct M avoiding: a b rule: trm.strong_induct)
(auto simp: abs_fresh abs_supp fin_supp fresh_left calc_atm fresh_atm)
lemma crename_ax: assumes a: "M[a⊨c>b] = Ax x c""c≠a""c≠b" shows"M = Ax x c" using a proof (nominal_induct M avoiding: a b x c rule: trm.strong_induct) qed (simp_all add: trm.inject split: if_splits)
lemma nrename_ax: assumes a: "M[x⊨n>y] = Ax z a""z≠x""z≠y" shows"M = Ax z a" using a proof (nominal_induct M avoiding: x y z a rule: trm.strong_induct) qed (simp_all add: trm.inject split: if_splits)
text‹substitution functions›
lemma fresh_perm_coname: fixes c::"coname" and pi::"coname prm" and M::"trm" assumes a: "c♯pi""c♯M" shows"c♯(pi∙M)" by (simp add: assms fresh_perm_app)
lemma fresh_perm_name: fixes x::"name" and pi::"name prm" and M::"trm" assumes a: "x♯pi""x♯M" shows"x♯(pi∙M)" by (simp add: assms fresh_perm_app)
lemma fresh_fun_simp_NotL: assumes a: "x'♯P""x'♯M" shows"fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x') = Cut <c>.P (x').NotL <a>.M x'" proof (rule fresh_fun_app) show"pt (TYPE(trm)::trm itself) (TYPE(name)::name itself)" by(rule pt_name_inst) show"at (TYPE(name)::name itself)" by(rule at_name_inst) show"finite (supp (λx'. Cut <c>.P (x').NotL <a>.M x')::name set)" using a by(finite_guess) obtain n::name where n: "n♯(c,P,a,M)" by (metis assms fresh_atm(3) fresh_prod) with assms have"n ♯ (λx'. Cut <c>.P (x').NotL <a>.M x')" by (fresh_guess) thenshow"∃b. b ♯ (λx'. Cut <c>.P (x').NotL <a>.M x', Cut <c>.P (b).NotL <a>.M b)" by (metis abs_fresh(1) abs_fresh(5) fresh_prod n trm.fresh(3)) show"x' ♯ (λx'. Cut <c>.P (x').NotL <a>.M x')" using assms by(fresh_guess) qed
lemma csubst_eqvt[eqvt]: fixes pi1::"name prm" and pi2::"coname prm" shows"pi1∙(M{c:=(x).N}) = (pi1∙M){(pi1∙c):=(pi1∙x).(pi1∙N)}" and"pi2∙(M{c:=(x).N}) = (pi2∙M){(pi2∙c):=(pi2∙x).(pi2∙N)}" by (nominal_induct M avoiding: c x N rule: trm.strong_induct)
(auto simp: eq_bij fresh_bij eqvts; perm_simp)+
lemma nsubst_eqvt[eqvt]: fixes pi1::"name prm" and pi2::"coname prm" shows"pi1∙(M{x:=<c>.N}) = (pi1∙M){(pi1∙x):=<(pi1∙c)>.(pi1∙N)}" and"pi2∙(M{x:=<c>.N}) = (pi2∙M){(pi2∙x):=<(pi2∙c)>.(pi2∙N)}" by (nominal_induct M avoiding: c x N rule: trm.strong_induct)
(auto simp: eq_bij fresh_bij eqvts; perm_simp)+
lemma supp_subst1: shows"supp (M{y:=<c>.P}) ⊆ ((supp M) - {y}) ∪ (supp P)" proof (nominal_induct M avoiding: y P c rule: trm.strong_induct) case (NotL coname trm name) obtain x'::name where"x'♯(trm{y:=<c>.P},P)" by (meson exists_fresh(1) fs_name1) with NotL show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast) next case (AndL1 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast) next case (AndL2 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast) next case (OrL name1 trm1 name2 trm2 name3) obtain x'::name where"x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)" by (meson exists_fresh(1) fs_name1) with OrL show ?case by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast) next case (ImpL coname trm1 name1 trm2 name2) obtain x'::name where"x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})" by (meson exists_fresh(1) fs_name1) with ImpL show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast) qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
text‹Identical to the previous proof› lemma supp_subst2: shows"supp (M{y:=<c>.P}) ⊆ supp (M) ∪ ((supp P) - {c})" proof (nominal_induct M avoiding: y P c rule: trm.strong_induct) case (NotL coname trm name) obtain x'::name where"x'♯(trm{y:=<c>.P},P)" by (meson exists_fresh(1) fs_name1) with NotL show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast) next case (AndL1 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast) next case (AndL2 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast) next case (OrL name1 trm1 name2 trm2 name3) obtain x'::name where"x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)" by (meson exists_fresh(1) fs_name1) with OrL show ?case by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast) next case (ImpL coname trm1 name1 trm2 name2) obtain x'::name where"x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})" by (meson exists_fresh(1) fs_name1) with ImpL show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast) qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
lemma supp_subst3: shows"supp (M{c:=(x).P}) ⊆ ((supp M) - {c}) ∪ (supp P)" proof (nominal_induct M avoiding: x P c rule: trm.strong_induct) case (NotR name trm coname) obtain x'::coname where"x'♯(trm{coname:=(x).P},P)" by (meson exists_fresh'(2) fs_coname1) with NotR show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR; blast) next case (AndR coname1 trm1 coname2 trm2 coname3) obtain x'::coname where x': "x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)" by (meson exists_fresh'(2) fs_coname1) with AndR show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR; blast) next case (OrR1 coname1 trm coname2) obtain x'::coname where x': "x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR1 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1; blast) next case (OrR2 coname1 trm coname2) obtain x'::coname where x': "x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR2 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2; blast) next case (ImpR name coname1 trm coname2) obtain x'::coname where x': "x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with ImpR show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpR; blast) qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
lemma supp_subst4: shows"supp (M{c:=(x).P}) ⊆ (supp M) ∪ ((supp P) - {x})" proof (nominal_induct M avoiding: x P c rule: trm.strong_induct) case (NotR name trm coname) obtain x'::coname where"x'♯(trm{coname:=(x).P},P)" by (meson exists_fresh'(2) fs_coname1) with NotR show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR; blast) next case (AndR coname1 trm1 coname2 trm2 coname3) obtain x'::coname where x': "x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)" by (meson exists_fresh'(2) fs_coname1) with AndR show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR; blast) next case (OrR1 coname1 trm coname2) obtain x'::coname where x': "x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR1 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1; blast) next case (OrR2 coname1 trm coname2) obtain x'::coname where x': "x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR2 show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2; blast) next case (ImpR name coname1 trm coname2) obtain x'::coname where x': "x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with ImpR show ?case by (auto simp: fresh_prod abs_supp supp_atm trm.supp fs_name1 fresh_fun_simp_ImpR; blast) qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
lemma supp_subst5: shows"(supp M - {y}) ⊆ supp (M{y:=<c>.P})" proof (nominal_induct M avoiding: y P c rule: trm.strong_induct) case (NotL coname trm name) obtain x'::name where"x'♯(trm{y:=<c>.P},P)" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL) apply (auto simp: fresh_def) done next case (AndL1 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1) apply (auto simp: fresh_def) done next case (AndL2 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2) apply (auto simp: fresh_def) done next case (OrL name1 trm1 name2 trm2 name3) obtain x'::name where"x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)" by (meson exists_fresh(1) fs_name1) with OrL show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL) apply (fastforce simp: fresh_def)+ done next case (ImpL coname trm1 name1 trm2 name2) obtain x'::name where"x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})" by (meson exists_fresh(1) fs_name1) with ImpL show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL) apply (fastforce simp: fresh_def)+ done qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
lemma supp_subst6: shows"(supp M) ⊆ ((supp (M{y:=<c>.P}))::coname set)" proof (nominal_induct M avoiding: y P c rule: trm.strong_induct) case (NotL coname trm name) obtain x'::name where"x'♯(trm{y:=<c>.P},P)" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL) apply (auto simp: fresh_def) done next case (AndL1 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1) apply (auto simp: fresh_def) done next case (AndL2 name1 trm name2) obtain x'::name where"x'♯(trm{y:=<c>.P},P,name1)" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2) apply (auto simp: fresh_def) done next case (OrL name1 trm1 name2 trm2 name3) obtain x'::name where"x'♯(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)" by (meson exists_fresh(1) fs_name1) with OrL show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL) apply (fastforce simp: fresh_def)+ done next case (ImpL coname trm1 name1 trm2 name2) obtain x'::name where"x'♯(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})" by (meson exists_fresh(1) fs_name1) with ImpL show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL) apply (fastforce simp: fresh_def)+ done qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
lemma supp_subst7: shows"(supp M - {c}) ⊆ supp (M{c:=(x).P})" proof (nominal_induct M avoiding: x P c rule: trm.strong_induct) case (NotR name trm coname) obtain x'::coname where"x'♯(trm{coname:=(x).P},P)" by (meson exists_fresh'(2) fs_coname1) with NotR show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR) apply (auto simp: fresh_def) done next case (AndR coname1 trm1 coname2 trm2 coname3) obtain x'::coname where"x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)" by (meson exists_fresh'(2) fs_coname1) with AndR show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR) apply (fastforce simp: fresh_def)+ done next case (OrR1 coname1 trm coname2) obtain x'::coname where"x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR1 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1) apply (auto simp: fresh_def) done next case (OrR2 coname1 trm coname2) obtain x'::coname where"x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR2 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2) apply (auto simp: fresh_def) done next case (ImpR name coname1 trm coname2) obtain x'::coname where"x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with ImpR show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpR) apply (auto simp: fresh_def) done qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
lemma supp_subst8: shows"(supp M) ⊆ ((supp (M{c:=(x).P}))::name set)" proof (nominal_induct M avoiding: x P c rule: trm.strong_induct) case (NotR name trm coname) obtain x'::coname where"x'♯(trm{coname:=(x).P},P)" by (meson exists_fresh'(2) fs_coname1) with NotR show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotR) apply (auto simp: fresh_def) done next case (AndR coname1 trm1 coname2 trm2 coname3) obtain x'::coname where"x'♯(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)" by (meson exists_fresh'(2) fs_coname1) with AndR show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndR) apply (fastforce simp: fresh_def)+ done next case (OrR1 coname1 trm coname2) obtain x'::coname where"x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR1 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR1) apply (auto simp: fresh_def) done next case (OrR2 coname1 trm coname2) obtain x'::coname where"x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with OrR2 show ?case apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrR2) apply (auto simp: fresh_def) done next case (ImpR name coname1 trm coname2) obtain x'::coname where"x'♯(trm{coname2:=(x).P},P,coname1)" by (meson exists_fresh'(2) fs_coname1) with ImpR show ?case by (force simp: fresh_prod abs_supp fs_name1 supp_atm trm.supp fresh_fun_simp_ImpR) qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+
lemma forget: shows"x♯M ==> M{x:=<c>.P} = M" and"c♯M ==> M{c:=(x).P} = M" by (nominal_induct M avoiding: x c P rule: trm.strong_induct)
(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
lemma substc_rename1: assumes a: "c♯(M,a)" shows"M{a:=(x).N} = ([(c,a)]∙M){c:=(x).N}" using a proof(nominal_induct M avoiding: c a x N rule: trm.strong_induct) case (AndR c1 M c2 M' c3) thenshow ?case apply(auto simp: fresh_prod calc_atm fresh_atm abs_fresh fresh_left) apply (metis (no_types, lifting))+ done next case ImpL thenshow ?case by (auto simp: calc_atm alpha fresh_atm abs_fresh fresh_prod fresh_left)
metis next case (Cut d M y M') thenshow ?case by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
(metis crename.simps(1) crename_id crename_rename) qed (auto simp: calc_atm alpha fresh_atm abs_fresh fresh_prod fresh_left trm.inject)
lemma substc_rename2: assumes a: "y♯(N,x)" shows"M{a:=(x).N} = M{a:=(y).([(y,x)]∙N)}" using a proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct) case (NotR y M d) obtain a::coname where"a♯(N,M{d:=(y).([(y,x)]∙N)},[(y,x)]∙N)" by (meson exists_fresh(2) fs_coname1) with NotR show ?case apply(auto simp: calc_atm alpha fresh_atm fresh_prod fresh_left) by (metis (no_types, opaque_lifting) alpha(1) trm.inject(2)) next case (AndR c1 M c2 M' c3) obtain a'::coname where"a'♯(N,M{c3:=(y).([(y,x)]∙N)},M'{c3:=(y).([(y,x)]∙N)},[(y,x)]∙N,c1,c2,c3)" by (meson exists_fresh(2) fs_coname1) with AndR show ?case apply(auto simp: calc_atm alpha fresh_atm fresh_prod fresh_left) by (metis (no_types, opaque_lifting) alpha(1) trm.inject(2)) next case (OrR1 d M e) obtain a'::coname where"a'♯(N,M{e:=(y).([(y,x)]∙N)},[(y,x)]∙N,d,e)" by (meson exists_fresh(2) fs_coname1) with OrR1 show ?case by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_OrR1) next case (OrR2 d M e) obtain a'::coname where"a'♯(N,M{e:=(y).([(y,x)]∙N)},[(y,x)]∙N,d,e)" by (meson exists_fresh(2) fs_coname1) with OrR2 show ?case by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_OrR2) next case (ImpR y d M e) obtain a'::coname where"a'♯(N,M{e:=(y).([(y,x)]∙N)},[(y,x)]∙N,d,e)" by (meson exists_fresh(2) fs_coname1) with ImpR show ?case by (auto simp: perm_swap calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left fresh_fun_simp_ImpR) qed (auto simp: calc_atm trm.inject alpha fresh_atm fresh_prod fresh_left perm_swap)
lemma substn_rename3: assumes a: "y♯(M,x)" shows"M{x:=<a>.N} = ([(y,x)]∙M){y:=<a>.N}" using a proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct) case (OrL x1 M x2 M' x3) thenshow ?case apply(auto simp add: calc_atm fresh_atm abs_fresh fresh_prod fresh_left) by (metis (mono_tags))+ next case (ImpL d M v M' u) thenshow ?case apply(auto simp add: calc_atm fresh_atm abs_fresh fresh_prod fresh_left) by (metis (mono_tags))+ next case (Cut d M y M') thenshow ?case apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left) by (metis nrename.simps(1) nrename_id nrename_rename)+ qed (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_left abs_supp fin_supp fresh_prod)
lemma substn_rename4: assumes a: "c♯(N,a)" shows"M{x:=<a>.N} = M{x:=<c>.([(c,a)]∙N)}" using a proof(nominal_induct M avoiding: x c a N rule: trm.strong_induct) case (Ax z d) thenshow ?case by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left) next case NotR thenshow ?case by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left) next case (NotL d M y) thenobtain a'::name where"a'♯(N, M{x:=<c>.([(c,a)]∙N)}, [(c,a)]∙N)" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left) by (metis (no_types, opaque_lifting) alpha(2) trm.inject(2)) next case (OrL x1 M x2 M' x3) thenobtain a'::name where"a'♯(N,M{x:=<c>.([(c,a)]∙N)},M'{x:=<c>.([(c,a)]∙N)},[(c,a)]∙N,x1,x2,x3)" by (meson exists_fresh(1) fs_name1) with OrL show ?case apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left) by (metis (no_types) alpha'(2) trm.inject(2)) next case (AndL1 u M v) thenobtain a'::name where"a'♯(N,M{x:=<c>.([(c,a)]∙N)},[(c,a)]∙N,u,v)" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left) by (metis (mono_tags, opaque_lifting) alpha'(2) trm.inject(2)) next case (AndL2 u M v) thenobtain a'::name where"a'♯(N,M{x:=<c>.([(c,a)]∙N)},[(c,a)]∙N,u,v)" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left) by (metis (mono_tags, opaque_lifting) alpha'(2) trm.inject(2)) next case (ImpL d M y M' u) thenobtain a'::name where"a'♯(N,M{u:=<c>.([(c,a)]∙N)},M'{u:=<c>.([(c,a)]∙N)},[(c,a)]∙N,y,u)" by (meson exists_fresh(1) fs_name1) with ImpL show ?case apply(auto simp: calc_atm trm.inject fresh_atm fresh_prod fresh_left) by (metis (no_types) alpha'(2) trm.inject(2)) next case (Cut d M y M') thenshow ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap) qed (auto simp: calc_atm fresh_atm fresh_left)
lemma subst_rename5: assumes a: "c'♯(c,N)""x'♯(x,M)" shows"M{x:=<c>.N} = ([(x',x)]∙M){x':=<c'>.([(c',c)]∙N)}" proof - have"M{x:=<c>.N} = ([(x',x)]∙M){x':=<c>.N}"using a by (simp add: substn_rename3) alsohave"… = ([(x',x)]∙M){x':=<c'>.([(c',c)]∙N)}"using a by (simp add: substn_rename4) finallyshow ?thesis by simp qed
lemma subst_rename6: assumes a: "c'♯(c,M)""x'♯(x,N)" shows"M{c:=(x).N} = ([(c',c)]∙M){c':=(x').([(x',x)]∙N)}" proof - have"M{c:=(x).N} = ([(c',c)]∙M){c':=(x).N}"using a by (simp add: substc_rename1) alsohave"… = ([(c',c)]∙M){c':=(x').([(x',x)]∙N)}"using a by (simp add: substc_rename2) finallyshow ?thesis by simp qed
lemma better_Cut_substn[simp]: assumes a: "a♯[c].P""x♯(y,P)" shows"(Cut <a>.M (x).N){y:=<c>.P} = (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" proof - obtain x'::"name"where fs1: "x'♯(M,N,c,P,x,y)"by (rule exists_fresh(1), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,c,P,a)"by (rule exists_fresh(2), rule fin_supp, blast) have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N))" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) have eq2: "(M=Ax y a) = (([(a',a)]∙M)=Ax y a')" by (metis perm_swap(4) swap_simps(4) swap_simps(8) trm.perm(13)) have"(Cut <a>.M (x).N){y:=<c>.P} = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N)){y:=<c>.P}" using eq1 by simp alsohave"… = (if ([(a',a)]∙M)=Ax y a' then Cut <c>.P (x').(([(x',x)]∙N){y:=<c>.P}) else Cut <a'>.(([(a',a)]∙M){y:=<c>.P}) (x').(([(x',x)]∙N){y:=<c>.P}))" using fs1 fs2 by (auto simp: fresh_prod fresh_left calc_atm fresh_atm) alsohave"… =(if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" using fs1 fs2 a unfolding eq2[symmetric] apply(auto simp: trm.inject) apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh eqvts perm_fresh_fresh calc_atm) apply (simp add: fresh_atm(2) substn_rename4) by (metis abs_fresh(2) fresh_atm(2) fresh_prod perm_fresh_fresh(2) substn_rename4) finallyshow ?thesis by simp qed
lemma better_Cut_substc[simp]: assumes a: "a♯(c,P)""x♯[y].P" shows"(Cut <a>.M (x).N){c:=(y).P} = (if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))" proof - obtain x'::"name"where fs1: "x'♯(M,N,c,P,x,y)"by (rule exists_fresh(1), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,c,P,a)"by (rule exists_fresh(2), rule fin_supp, blast) have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N))" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) have eq2: "(N=Ax x c) = (([(x',x)]∙N)=Ax x' c)" by (metis perm_dj(1) perm_swap(1) swap_simps(1) trm.perm(1)) have"(Cut <a>.M (x).N){c:=(y).P} = (Cut <a'>.([(a',a)]∙M) (x').([(x',x)]∙N)){c:=(y).P}" using eq1 by simp alsohave"… = (if ([(x',x)]∙N)=Ax x' c then Cut <a'>.(([(a',a)]∙M){c:=(y).P}) (y).P else Cut <a'>.(([(a',a)]∙M){c:=(y).P}) (x').(([(x',x)]∙N){c:=(y).P}))" using fs1 fs2 by (simp add: fresh_prod fresh_left calc_atm fresh_atm trm.inject) alsohave"… =(if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))" using fs1 fs2 a unfolding eq2[symmetric] apply(auto simp: trm.inject) apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh eqvts perm_fresh_fresh calc_atm) by (metis abs_fresh(1) fresh_atm(1) fresh_prod perm_fresh_fresh(1) substc_rename2) finallyshow ?thesis by simp qed
lemma better_Cut_substn': assumes"a♯[c].P""y♯(N,x)""M≠Ax y a" shows"(Cut <a>.M (x).N){y:=<c>.P} = Cut <a>.(M{y:=<c>.P}) (x).N" proof - obtain d::name where d: "d ♯ (M, N, P, a, c, x, y)" by (meson exists_fresh(1) fs_name1) thenhave *: "y♯([(d,x)]∙N)" by (metis assms(2) fresh_atm(1) fresh_list_cons fresh_list_nil fresh_perm_name fresh_prod) with d have"Cut <a>.M (x).N = Cut <a>.M (d).([(d,x)]∙N)" by (metis (no_types, lifting) alpha(1) fresh_prodD perm_fresh_fresh(1) trm.inject(2)) with * d assms show ?thesis apply(simp add: fresh_prod) by (smt (verit, ccfv_SIG) forget(1) trm.inject(2)) qed
lemma better_NotR_substc: assumes a: "d♯M" shows"(NotR (x).M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.NotR (x).M a' (z).P)" proof - obtain c::name where c: "c ♯ (M, P, d, x, z)" by (meson exists_fresh(1) fs_name1) obtain e::coname where e: "e ♯ (M, P, d, x, z, c)" by (meson exists_fresh'(2) fs_coname1) with c have"NotR (x).M d = NotR (c).([(c,x)]∙M) d" by (metis alpha'(1) fresh_prodD(1) nrename_id nrename_swap trm.inject(3)) with c e assms show ?thesis apply(simp add: fresh_prod) by (metis forget(2) fresh_perm_app(3) trm.inject(3)) qed
lemma better_NotL_substn: assumes a: "y♯M" shows"(NotL <a>.M y){y:=<c>.P} = fresh_fun (λx'. Cut <c>.P (x').NotL <a>.M x')" proof (generate_fresh "coname") fix ca :: coname assume d: "ca ♯ (M, P, a, c, y)" thenhave"NotL <a>.M y = NotL <ca>.([(ca,a)]∙M) y" by (metis alpha(2) fresh_prod perm_fresh_fresh(2) trm.inject(4)) with a d show ?thesis apply(simp add: fresh_left calc_atm forget) apply (metis trm.inject(4)) done qed
lemma better_AndL1_substn: assumes a: "y♯[x].M" shows"(AndL1 (x).M y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).M z')" proof (generate_fresh "name") fix d:: name assume d: "d ♯ (M, P, c, x, y)" thenhave§: "AndL1 (x).M y = AndL1 (d).([(d,x)]∙M) y" by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(6)) with d have"(λz'. Cut <c>.P (z').AndL1 (d).([(d, x)] ∙ M){x:=<c>.P} (z')) = (λz'. Cut <c>.P (z').AndL1 (x).M (z'))" by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(6)) with d have"(λz'. Cut <c>.P (z').AndL1 d.([(d, x)] ∙ M){y:=<c>.P} z') = (λz'. Cut <c>.P (z').AndL1 (x).M (z'))" apply(simp add: trm.inject alpha fresh_prod fresh_atm) by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap) with d §show ?thesis by (simp add: fresh_left calc_atm) qed
lemma better_AndL2_substn: assumes a: "y♯[x].M" shows"(AndL2 (x).M y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).M z')" proof (generate_fresh "name") fix d:: name assume d: "d ♯ (M, P, c, x, y)" thenhave§: "AndL2 (x).M y = AndL2 (d).([(d,x)]∙M) y" by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(7)) with d have"(λz'. Cut <c>.P (z').AndL2 (d).([(d, x)] ∙ M){x:=<c>.P} (z')) = (λz'. Cut <c>.P (z').AndL2 (x).M (z'))" by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(7)) with d have"(λz'. Cut <c>.P (z').AndL2 d.([(d, x)] ∙ M){y:=<c>.P} z') = (λz'. Cut <c>.P (z').AndL2 (x).M (z'))" apply(simp add: trm.inject alpha fresh_prod fresh_atm) by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap) with d §show ?thesis by (simp add: fresh_left calc_atm) qed
lemma better_AndR_substc: assumes"c♯([a].M,[b].N)" shows"(AndR <a>.M <b>.N c){c:=(z).P} = fresh_fun (λa'. Cut <a'>.(AndR <a>.M <b>.N a') (z).P)" proof (generate_fresh "coname" , generate_fresh "coname") fix d :: coname and e :: coname assume d: "d ♯ (M, N, P, a, b, c, z)" and e: "e ♯ (M, N, P, a, b, c, z, d)" thenhave"AndR <a>.M <b>.N c = AndR <d>.([(d,a)]∙M) <e>.([(e,b)]∙N) c" by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto with assms d e show ?thesis apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) by (metis (no_types, opaque_lifting) abs_fresh(2) forget(2) trm.inject(5)) qed
lemma better_OrL_substn: assumes"x♯([y].M,[z].N)" shows"(OrL (y).M (z).N x){x:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').OrL (y).M (z).N z')" proof (generate_fresh "name" , generate_fresh "name") fix d :: name and e :: name assume d: "d ♯ (M, N, P, c, x, y, z)" and e: "e ♯ (M, N, P, c, x, y, z, d)" with assms have"OrL (y).M (z).N x = OrL (d).([(d,y)]∙M) (e).([(e,z)]∙N) x" by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto with assms d e show ?thesis apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) by (metis (no_types, lifting) abs_fresh(1) forget(1) trm.inject(10)) qed
lemma better_OrR1_substc: assumes a: "d♯[a].M" shows"(OrR1 <a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.OrR1 <a>.M a' (z).P)" proof (generate_fresh "coname") fix c :: coname assume c: "c ♯ (M, P, a, d, z)" thenhave"OrR1 <a>.M d = OrR1 <c>.([(c,a)]∙M) d" by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto with assms c show ?thesis apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) by (metis abs_fresh(2) forget(2) trm.inject(8)) qed
lemma better_OrR2_substc: assumes a: "d♯[a].M" shows"(OrR2 <a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.OrR2 <a>.M a' (z).P)" proof (generate_fresh "coname") fix c :: coname assume c: "c ♯ (M, P, a, d, z)" thenhave"OrR2 <a>.M d = OrR2 <c>.([(c,a)]∙M) d" by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto with assms c show ?thesis apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) by (metis abs_fresh(2) forget(2) trm.inject(9)) qed
lemma better_ImpR_substc: assumes"d♯[a].M" shows"(ImpR (x).<a>.M d){d:=(z).P} = fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.M a' (z).P)" proof (generate_fresh "coname" , generate_fresh "name") fix c :: coname and c' :: name assume c: "c ♯ (M, P, a, d, x, z)" and c': "c' ♯ (M, P, a, d, x, z, c)" have†: "ImpR (x).<a>.M d = ImpR (c').<c>.([(c,a)]∙[(c',x)]∙M) d" apply (rule sym) using c c' apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm) done with assms c c' have"fresh_fun (λa'. Cut <a'>.ImpR (c').<c>.(([(c, a)] ∙ [(c', x)] ∙ M)){d:=(z).P} a' (z).P) = fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.M a' (z).P)" apply(intro arg_cong [where f="fresh_fun"]) by(fastforce simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh forget) with assms c c' †show ?thesis by (auto simp: fresh_left calc_atm forget abs_fresh) qed
lemma better_ImpL_substn: assumes"y♯(M,[x].N)" shows"(ImpL <a>.M (x).N y){y:=<c>.P} = fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.M (x).N z')" proof (generate_fresh "coname" , generate_fresh "name") fix ca :: coname and caa :: name assume d: "ca ♯ (M, N, P, a, c, x, y)" and e: "caa ♯ (M, N, P, a, c, x, y, ca)" have"ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]∙M) (caa).([(caa,x)]∙N) y" apply(rule sym) using d e by(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm) with d e assms show ?thesis apply(simp add: fresh_left calc_atm forget abs_fresh) apply(intro arg_cong [where f="fresh_fun"] ext) apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) by (metis forget(1) fresh_aux(1) fresh_bij(1) swap_simps(1)) qed
lemma substn_crename_comm: assumes"c≠a""c≠b" shows"M{x:=<c>.P}[a⊨c>b] = M[a⊨c>b]{x:=<c>.(P[a⊨c>b])}" using assms proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct) case (Ax name coname) thenshow ?case by(auto simp: better_crename_Cut fresh_atm) next case (Cut coname trm1 name trm2) thenshow ?case apply(simp add: rename_fresh better_crename_Cut fresh_atm) by (meson crename_ax) next case (NotL coname trm name) obtain x'::name where"x'♯(trm{x:=<c>.P},P,P[a⊨c>b],x,trm[a⊨c>b]{x:=<c>.P[a⊨c>b]})" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply (simp add: subst_fresh rename_fresh trm.inject) by (force simp: fresh_prod fresh_fun_simp_NotL better_crename_Cut fresh_atm) next case (AndL1 name1 trm name2) obtain x'::name where"x'♯(trm{x:=<c>.P},P,P[a⊨c>b],name1,trm[a⊨c>b]{x:=<c>.P[a⊨c>b]})" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case apply (simp add: subst_fresh rename_fresh trm.inject) apply (force simp: fresh_prod fresh_fun_simp_AndL1 better_crename_Cut fresh_atm) done next case (AndL2 name1 trm name2) obtain x'::name where x': "x'♯(trm{x:=<c>.P},P,P[a⊨c>b],name1,trm[a⊨c>b]{x:=<c>.P[a⊨c>b]})" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case apply (simp add: subst_fresh rename_fresh trm.inject) apply (auto simp: fresh_prod fresh_fun_simp_AndL2 better_crename_Cut fresh_atm) done next case (OrL name1 trm1 name2 trm2 name3) obtain x'::name where x': "x'♯(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a⊨c>b],name1,name2, trm1[a⊨c>b]{x:=<c>.P[a⊨c>b]},trm2[a⊨c>b]{x:=<c>.P[a⊨c>b]})" by (meson exists_fresh(1) fs_name1) with OrL show ?case apply (simp add: subst_fresh rename_fresh trm.inject) apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_OrL better_crename_Cut) done next case (ImpL coname trm1 name1 trm2 name2) obtain x'::name where x': "x'♯(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a⊨c>b],name1,name2, trm1[a⊨c>b]{x:=<c>.P[a⊨c>b]},trm2[a⊨c>b]{x:=<c>.P[a⊨c>b]})" by (meson exists_fresh(1) fs_name1) with ImpL show ?case apply (simp add: subst_fresh rename_fresh trm.inject) apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_ImpL better_crename_Cut) done qed (auto simp: subst_fresh rename_fresh)
lemma substc_crename_comm: assumes"c≠a""c≠b" shows"M{c:=(x).P}[a⊨c>b] = M[a⊨c>b]{c:=(x).(P[a⊨c>b])}" using assms proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct) case (Ax name coname) thenshow ?case by(auto simp: better_crename_Cut fresh_atm) next case (Cut coname trm1 name trm2) thenshow ?case apply(simp add: rename_fresh better_crename_Cut) by (meson crename_ax) next case (NotR name trm coname) obtain c'::coname where"c'♯(a,b,trm{coname:=(x).P},P,P[a⊨c>b],x,trm[a⊨c>b]{coname:=(x).P[a⊨c>b]})" by (meson exists_fresh' fs_coname1) with NotR show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by(auto simp: fresh_prod fresh_fun_simp_NotR better_crename_Cut fresh_atm) next case (AndR coname1 trm1 coname2 trm2 coname3) obtain c'::coname where"c'♯(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P}, P,P[a⊨c>b],x,trm1[a⊨c>b]{coname3:=(x).P[a⊨c>b]},trm2[a⊨c>b]{coname3:=(x).P[a⊨c>b]})" by (meson exists_fresh' fs_coname1) with AndR show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by (auto simp: fresh_prod fresh_fun_simp_AndR better_crename_Cut subst_fresh fresh_atm) next case (OrR1 coname1 trm coname2) obtain c'::coname where"c'♯(coname1,trm{coname2:=(x).P},P,P[a⊨c>b],a,b, trm[a⊨c>b]{coname2:=(x).P[a⊨c>b]})" by (meson exists_fresh' fs_coname1) with OrR1 show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by(auto simp: fresh_prod fresh_fun_simp_OrR1 better_crename_Cut fresh_atm) next case (OrR2 coname1 trm coname2) obtain c'::coname where"c'♯(coname1,trm{coname2:=(x).P},P,P[a⊨c>b],a,b, trm[a⊨c>b]{coname2:=(x).P[a⊨c>b]})" by (meson exists_fresh' fs_coname1) with OrR2 show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by(auto simp: fresh_prod fresh_fun_simp_OrR2 better_crename_Cut fresh_atm) next case (ImpR name coname1 trm coname2) obtain c'::coname where"c'♯(coname1,trm{coname2:=(x).P},P,P[a⊨c>b],a,b, trm[a⊨c>b]{coname2:=(x).P[a⊨c>b]})" by (meson exists_fresh' fs_coname1) with ImpR show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by(auto simp: fresh_prod fresh_fun_simp_ImpR better_crename_Cut fresh_atm) qed (auto simp: subst_fresh rename_fresh trm.inject)
lemma substn_nrename_comm: assumes"x≠y""x≠z" shows"M{x:=<c>.P}[y⊨n>z] = M[y⊨n>z]{x:=<c>.(P[y⊨n>z])}" using assms proof (nominal_induct M avoiding: x c P y z rule: trm.strong_induct) case (Ax name coname) thenshow ?case by (auto simp: better_nrename_Cut fresh_atm) next case (Cut coname trm1 name trm2) thenshow ?case apply(clarsimp simp: subst_fresh rename_fresh trm.inject better_nrename_Cut) by (meson nrename_ax) next case (NotL coname trm name) obtain x'::name where"x'♯(y,z,trm{x:=<c>.P},P,P[y⊨n>z],x,trm[y⊨n>z]{x:=<c>.P[y⊨n>z]})" by (meson exists_fresh' fs_name1) with NotL show ?case apply(clarsimp simp: rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_NotL better_nrename_Cut fresh_atm) next case (AndL1 name1 trm name2) obtain x'::name where"x'♯(trm{x:=<c>.P},P,P[y⊨n>z],name1,trm[y⊨n>z]{x:=<c>.P[y⊨n>z]},y,z)" by (meson exists_fresh' fs_name1) with AndL1 show ?case apply(clarsimp simp: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_AndL1 better_nrename_Cut fresh_atm) next case (AndL2 name1 trm name2) obtain x'::name where"x'♯(trm{x:=<c>.P},P,P[y⊨n>z],name1,trm[y⊨n>z]{x:=<c>.P[y⊨n>z]},y,z)" by (meson exists_fresh' fs_name1) with AndL2 show ?case apply(clarsimp simp: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_AndL2 better_nrename_Cut fresh_atm) next case (OrL name1 trm1 name2 trm2 name3) obtain x'::name where"x'♯(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y⊨n>z],name1,name2,y,z, trm1[y⊨n>z]{x:=<c>.P[y⊨n>z]},trm2[y⊨n>z]{x:=<c>.P[y⊨n>z]})" by (meson exists_fresh' fs_name1) with OrL show ?case apply (clarsimp simp: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_OrL better_nrename_Cut subst_fresh fresh_atm) next case (ImpL coname trm1 name1 trm2 name2) obtain x'::name where"x'♯(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y⊨n>z],name1,name2,y,z, trm1[y⊨n>z]{x:=<c>.P[y⊨n>z]},trm2[y⊨n>z]{x:=<c>.P[y⊨n>z]})" by (meson exists_fresh' fs_name1) with ImpL show ?case apply (clarsimp simp: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_ImpL better_nrename_Cut subst_fresh fresh_atm) qed (auto simp: subst_fresh rename_fresh trm.inject)
lemma substc_nrename_comm: assumes"x≠y""x≠z" shows"M{c:=(x).P}[y⊨n>z] = M[y⊨n>z]{c:=(x).(P[y⊨n>z])}" using assms proof (nominal_induct M avoiding: x c P y z rule: trm.strong_induct) case (Ax name coname) thenshow ?case by (auto simp: subst_fresh rename_fresh trm.inject better_nrename_Cut fresh_atm) next case (Cut coname trm1 name trm2) thenshow ?case apply (clarsimp simp: subst_fresh rename_fresh trm.inject better_nrename_Cut fresh_atm) by (metis nrename_ax) next case (NotR name trm coname) obtain c'::coname where"c'♯(y,z,trm{coname:=(x).P},P,P[y⊨n>z],x,trm[y⊨n>z]{coname:=(x).P[y⊨n>z]})" by (meson exists_fresh' fs_coname1) with NotR show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_NotR better_nrename_Cut fresh_atm) next case (AndR coname1 trm1 coname2 trm2 coname3) obtain c'::coname where"c'♯(coname1,coname2,y,z,trm1{coname3:=(x).P},trm2{coname3:=(x).P}, P,P[y⊨n>z],x,trm1[y⊨n>z]{coname3:=(x).P[y⊨n>z]},trm2[y⊨n>z]{coname3:=(x).P[y⊨n>z]})" by (meson exists_fresh' fs_coname1) with AndR show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_AndR better_nrename_Cut fresh_atm subst_fresh) next case (OrR1 coname1 trm coname2) obtain c'::coname where"c'♯(coname1,trm{coname2:=(x).P},P,P[y⊨n>z],y,z, trm[y⊨n>z]{coname2:=(x).P[y⊨n>z]})" by (meson exists_fresh' fs_coname1) with OrR1 show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_OrR1 better_nrename_Cut fresh_atm subst_fresh) next case (OrR2 coname1 trm coname2) obtain c'::coname where"c'♯(coname1,trm{coname2:=(x).P},P,P[y⊨n>z],y,z, trm[y⊨n>z]{coname2:=(x).P[y⊨n>z]})" by (meson exists_fresh' fs_coname1) with OrR2 show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_OrR2 better_nrename_Cut fresh_atm subst_fresh) next case (ImpR name coname1 trm coname2) obtain c'::coname where"c'♯(coname1,trm{coname2:=(x).P},P,P[y⊨n>z],y,z, trm[y⊨n>z]{coname2:=(x).P[y⊨n>z]})" by (meson exists_fresh' fs_coname1) with ImpR show ?case apply(simp add: subst_fresh rename_fresh trm.inject) by (auto simp add: fresh_prod fresh_fun_simp_ImpR better_nrename_Cut fresh_atm subst_fresh) qed (auto simp: subst_fresh rename_fresh trm.inject)
lemma substn_crename_comm': assumes"a≠c""a♯P" shows"M{x:=<c>.P}[a⊨c>b] = M[a⊨c>b]{x:=<c>.P}" proof - obtain c'::"coname"where fs2: "c'♯(c,P,a,b)"by (rule exists_fresh(2), rule fin_supp, blast) have eq: "M{x:=<c>.P} = M{x:=<c'>.([(c',c)]∙P)}" using fs2 substn_rename4 by force have eq': "M[a⊨c>b]{x:=<c>.P} = M[a⊨c>b]{x:=<c'>.([(c',c)]∙P)}" using fs2 by (simp add: substn_rename4) have eq2: "([(c',c)]∙P)[a⊨c>b] = ([(c',c)]∙P)"using fs2 assms by (metis crename_fresh fresh_atm(2) fresh_aux(2) fresh_prod) have"M{x:=<c>.P}[a⊨c>b] = M{x:=<c'>.([(c',c)]∙P)}[a⊨c>b]"using eq by simp alsohave"… = M[a⊨c>b]{x:=<c'>.(([(c',c)]∙P)[a⊨c>b])}" using fs2 by (simp add: fresh_atm(2) fresh_prod substn_crename_comm) alsohave"… = M[a⊨c>b]{x:=<c'>.(([(c',c)]∙P))}"using eq2 by simp alsohave"… = M[a⊨c>b]{x:=<c>.P}"using eq' by simp finallyshow ?thesis by simp qed
lemma substc_crename_comm': assumes"c≠a""c≠b""a♯P" shows"M{c:=(x).P}[a⊨c>b] = M[a⊨c>b]{c:=(x).P}" proof - obtain c'::"coname"where fs2: "c'♯(c,M,a,b)"by (rule exists_fresh(2), rule fin_supp, blast) have eq: "M{c:=(x).P} = ([(c',c)]∙M){c':=(x).P}" using fs2 by (simp add: substc_rename1) have eq': "([(c',c)]∙(M[a⊨c>b])){c':=(x).P} = M[a⊨c>b]{c:=(x).P}" using fs2 by (metis crename_cfresh' fresh_prod substc_rename1) have eq2: "([(c',c)]∙M)[a⊨c>b] = ([(c',c)]∙(M[a⊨c>b]))"using fs2 assms by (simp add: crename_coname_eqvt fresh_atm(2) fresh_prod swap_simps(6)) have"M{c:=(x).P}[a⊨c>b] = ([(c',c)]∙M){c':=(x).P}[a⊨c>b]"using eq by simp alsohave"… = ([(c',c)]∙M)[a⊨c>b]{c':=(x).P[a⊨c>b]}" using fs2 assms by (metis crename_fresh eq eq' eq2 substc_crename_comm) alsohave"… = ([(c',c)]∙(M[a⊨c>b])){c':=(x).P[a⊨c>b]}"using eq2 by simp alsohave"… = ([(c',c)]∙(M[a⊨c>b])){c':=(x).P}" using assms by (simp add: rename_fresh) alsohave"… = M[a⊨c>b]{c:=(x).P}"using eq' by simp finallyshow ?thesis by simp qed
lemma substn_nrename_comm': assumes"x≠y""x≠z""y♯P" shows"M{x:=<c>.P}[y⊨n>z] = M[y⊨n>z]{x:=<c>.P}" proof - obtain x'::"name"where fs2: "x'♯(x,M,y,z)"by (rule exists_fresh(1), rule fin_supp, blast) have eq: "M{x:=<c>.P} = ([(x',x)]∙M){x':=<c>.P}" using fs2 by (simp add: substn_rename3) have eq': "([(x',x)]∙(M[y⊨n>z])){x':=<c>.P} = M[y⊨n>z]{x:=<c>.P}" using fs2 by (metis fresh_prod nrename_nfresh' substn_rename3) have eq2: "([(x',x)]∙M)[y⊨n>z] = ([(x',x)]∙(M[y⊨n>z]))" using fs2 by (simp add: assms fresh_atm(1) fresh_prod nrename_name_eqvt swap_simps(5)) have"M{x:=<c>.P}[y⊨n>z] = ([(x',x)]∙M){x':=<c>.P}[y⊨n>z]"using eq by simp alsohave"… = ([(x',x)]∙M)[y⊨n>z]{x':=<c>.P[y⊨n>z]}" using fs2 by (metis assms eq eq' eq2 nrename_fresh substn_nrename_comm) alsohave"… = ([(x',x)]∙(M[y⊨n>z])){x':=<c>.P[y⊨n>z]}"using eq2 by simp alsohave"… = ([(x',x)]∙(M[y⊨n>z])){x':=<c>.P}"using assms by (simp add: rename_fresh) alsohave"… = M[y⊨n>z]{x:=<c>.P}"using eq' by simp finallyshow ?thesis by simp qed
lemma substc_nrename_comm': assumes"x≠y""y♯P" shows"M{c:=(x).P}[y⊨n>z] = M[y⊨n>z]{c:=(x).P}" proof - obtain x'::"name"where fs2: "x'♯(x,P,y,z)"by (rule exists_fresh(1), rule fin_supp, blast) have eq: "M{c:=(x).P} = M{c:=(x').([(x',x)]∙P)}" using fs2 using substc_rename2 by auto have eq': "M[y⊨n>z]{c:=(x).P} = M[y⊨n>z]{c:=(x').([(x',x)]∙P)}" using fs2 by (simp add: substc_rename2) have eq2: "([(x',x)]∙P)[y⊨n>z] = ([(x',x)]∙P)" using fs2 by (metis assms(2) fresh_atm(1) fresh_aux(1) fresh_prod nrename_fresh) have"M{c:=(x).P}[y⊨n>z] = M{c:=(x').([(x',x)]∙P)}[y⊨n>z]"using eq by simp alsohave"… = M[y⊨n>z]{c:=(x').(([(x',x)]∙P)[y⊨n>z])}" using fs2 by (simp add: fresh_atm(1) fresh_prod substc_nrename_comm) alsohave"… = M[y⊨n>z]{c:=(x').(([(x',x)]∙P))}"using eq2 by simp alsohave"… = M[y⊨n>z]{c:=(x).P}"using eq' by simp finallyshow ?thesis by simp qed
lemma fin_rest_elims: shows"fin (Cut <a>.M (x).N) y ==> False" and"fin (NotR (x).M c) y ==> False" and"fin (AndR <a>.M <b>.N c) y ==> False" and"fin (OrR1 <a>.M b) y ==> False" and"fin (OrR2 <a>.M b) y ==> False" and"fin (ImpR (x).<a>.M b) y ==> False" by (erule fin.cases, simp_all add: trm.inject)+
lemma fin_rename: shows"fin M x ==> fin ([(x',x)]∙M) x'" by (induct rule: fin.induct)
(auto simp: calc_atm simp add: fresh_left abs_fresh)
lemma not_fin_subst1: assumes"¬(fin M x)" shows"¬(fin (M{c:=(y).P}) x)" using assms proof (nominal_induct M avoiding: x c y P rule: trm.strong_induct) case (Ax name coname) thenshow ?case using fin_rest_elims(1) substc.simps(1) by presburger next case (Cut coname trm1 name trm2) thenshow ?case using fin_rest_elims(1) substc.simps(1) by simp presburger next case (NotR name trm coname) obtain a'::coname where"a'♯(trm{coname:=(y).P},P,x)" by (meson exists_fresh(2) fs_coname1) with NotR show ?case apply (simp add: fresh_prod trm.inject) using fresh_fun_simp_NotR fin_rest_elims by fastforce next case (NotL coname trm name) thenshow ?case using fin_NotL_elim freshn_after_substc by simp blast next case (AndR coname1 trm1 coname2 trm2 coname3) obtain a'::coname where"a'♯(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)" by (meson exists_fresh(2) fs_coname1) with AndR show ?case apply (simp add: fresh_prod trm.inject) using fresh_fun_simp_AndR fin_rest_elims by fastforce next case (AndL1 name1 trm name2) thenshow ?case using fin_AndL1_elim freshn_after_substc by simp (metis abs_fresh(1) fin.intros(3)) next case (AndL2 name1 trm name2) thenshow ?case using fin_AndL2_elim freshn_after_substc by simp (metis abs_fresh(1) fin.intros(4)) next case (OrR1 coname1 trm coname2) obtain a'::coname where"a'♯(trm{coname2:=(y).P},coname1,P,x)" by (meson exists_fresh(2) fs_coname1) with OrR1 show ?case apply (simp add: fresh_prod trm.inject) using fresh_fun_simp_OrR1 fin_rest_elims by fastforce next case (OrR2 coname1 trm coname2) obtain a'::coname where"a'♯(trm{coname2:=(y).P},coname1,P,x)" by (meson exists_fresh(2) fs_coname1) with OrR2 show ?case apply (simp add: fresh_prod trm.inject) using fresh_fun_simp_OrR2 fin_rest_elims by fastforce next case (OrL name1 trm1 name2 trm2 name3) thenshow ?case by simp (metis abs_fresh(1) fin.intros(5) fin_OrL_elim freshn_after_substc) next case (ImpR name coname1 trm coname2) obtain a'::coname where"a'♯(trm{coname2:=(y).P},coname1,P,x)" by (meson exists_fresh(2) fs_coname1) with ImpR show ?case apply (simp add: fresh_prod trm.inject) using fresh_fun_simp_ImpR fin_rest_elims by fastforce next case (ImpL coname trm1 name1 trm2 name2) thenshow ?case by simp (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim freshn_after_substc) qed
lemma not_fin_subst2: assumes"¬(fin M x)" shows"¬(fin (M{y:=<c>.P}) x)" using assms proof (nominal_induct M avoiding: x c y P rule: trm.strong_induct) case (Ax name coname) thenshow ?case using fin_rest_elims(1) substn.simps(1) by presburger next case (Cut coname trm1 name trm2) thenshow ?case using fin_rest_elims(1) substc.simps(1) by simp presburger next case (NotR name trm coname) with fin_rest_elims show ?case by (fastforce simp add: fresh_prod trm.inject) next case (NotL coname trm name) obtain a'::name where"a'♯(trm{y:=<c>.P},P,x)" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_NotL trm.inject) by (metis fin.intros(2) fin_NotL_elim fin_rest_elims(1) freshn_after_substn) next case (AndR coname1 trm1 coname2 trm2 coname3) obtain a'::name where"a'♯(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,coname3,x)" by (meson exists_fresh(1) fs_name1) with AndR fin_rest_elims show ?case by (fastforce simp add: fresh_prod trm.inject) next case (AndL1 name1 trm name2) obtain a'::name where"a'♯(trm{y:=<c>.P},P,name1,x)" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_AndL1 trm.inject) by (metis abs_fresh(1) fin.intros(3) fin_AndL1_elim fin_rest_elims(1) freshn_after_substn) next case (AndL2 name1 trm name2) obtain a'::name where"a'♯(trm{y:=<c>.P},P,name1,x)" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_AndL2 trm.inject) by (metis abs_fresh(1) fin.intros(4) fin_AndL2_elim fin_rest_elims(1) freshn_after_substn) next case (OrR1 coname1 trm coname2) thenshow ?case using fin_rest_elims by (fastforce simp: fresh_prod trm.inject) next case (OrR2 coname1 trm coname2) thenshow ?case using fin_rest_elims by (fastforce simp: fresh_prod trm.inject) next case (OrL name1 trm1 name2 trm2 name3) obtain a'::name where"a'♯(trm1{y:=<c>.P},trm2{y:=<c>.P},name1,name2,P,x)" by (meson exists_fresh(1) fs_name1) with OrL show ?case apply (simp add: fresh_prod trm.inject) by (metis (full_types) abs_fresh(1) fin.intros(5) fin_OrL_elim fin_rest_elims(1) fresh_fun_simp_OrL freshn_after_substn) next case (ImpR name coname1 trm coname2) with fin_rest_elims show ?case by (fastforce simp add: fresh_prod trm.inject) next case (ImpL coname trm1 name1 trm2 name2) obtain a'::name where"a'♯(trm1{name2:=<c>.P},trm2{name2:=<c>.P},name1,P,x)" by (meson exists_fresh(1) fs_name1) with ImpL show ?case apply (simp add: fresh_prod trm.inject) by (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fin_rest_elims(1) fresh_fun_simp_ImpL freshn_after_substn) qed
lemma fin_subst1: assumes"fin M x""x≠y""x♯P" shows"fin (M{y:=<c>.P}) x" using assms proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct) case (AndL1 name1 trm name2) thenshow ?case apply (clarsimp simp add: subst_fresh abs_fresh dest!: fin_AndL1_elim) by (metis abs_fresh(1) fin.intros(3) fresh_prod subst_fresh(3)) next case (AndL2 name1 trm name2) thenshow ?case apply (clarsimp simp add: subst_fresh abs_fresh dest!: fin_AndL2_elim) by (metis abs_fresh(1) fin.intros(4) fresh_prod subst_fresh(3)) next case (OrR1 coname1 trm coname2) thenshow ?case by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims) next case (OrR2 coname1 trm coname2) thenshow ?case by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims) next case (OrL name1 trm1 name2 trm2 name3) thenshow ?case apply (clarsimp simp add: subst_fresh abs_fresh) by (metis abs_fresh(1) fin.intros(5) fin_OrL_elim fresh_prod subst_fresh(3)) next case (ImpR name coname1 trm coname2) thenshow ?case by (auto simp add: subst_fresh abs_fresh dest!: fin_rest_elims) next case (ImpL coname trm1 name1 trm2 name2) thenshow ?case apply (clarsimp simp add: subst_fresh abs_fresh) by (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fresh_prod subst_fresh(3)) qed (auto dest!: fin_elims simp add: subst_fresh abs_fresh)
thm abs_fresh fresh_prod
lemma fin_subst2: assumes"fin M y""x≠y""y♯P""M≠Ax y c" shows"fin (M{c:=(x).P}) y" using assms proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct) case (Ax name coname) thenshow ?case using fin_Ax_elim by force next case (NotL coname trm name) thenshow ?case by simp (metis fin.intros(2) fin_NotL_elim fresh_prod subst_fresh(5)) next case (AndL1 name1 trm name2) thenshow ?case by simp (metis abs_fresh(1) fin.intros(3) fin_AndL1_elim fresh_prod subst_fresh(5)) next case (AndL2 name1 trm name2) thenshow ?case by simp (metis abs_fresh(1) fin.intros(4) fin_AndL2_elim fresh_prod subst_fresh(5)) next case (OrL name1 trm1 name2 trm2 name3) thenshow ?case by simp (metis abs_fresh(1) fin.intros(5) fin_OrL_elim fresh_prod subst_fresh(5)) next case (ImpL coname trm1 name1 trm2 name2) thenshow ?case by simp (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fresh_prod subst_fresh(5)) qed (use fin_rest_elims in force)+
lemma fin_substn_nrename: assumes"fin M x""x≠y""x♯P" shows"M[x⊨n>y]{y:=<c>.P} = Cut <c>.P (x).(M{y:=<c>.P})" using assms [[simproc del: defined_all]] proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct) case (Ax name coname) thenshow ?case by (metis fin_Ax_elim fresh_atm(1,3) fresh_prod nrename_swap subst_rename(3) substn.simps(1) trm.fresh(1)) next case (NotL coname trm name) obtain z::name where"z ♯ (trm,y,x,P,trm[x⊨n>y]{y:=<c>.P})" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply (clarsimp simp add: fresh_prod fresh_fun_simp_NotL trm.inject alpha fresh_atm calc_atm abs_fresh) by (metis fin_NotL_elim nrename_fresh nrename_swap substn_nrename_comm') next case (AndL1 name1 trm name2) obtain z::name where"z ♯ (name2,name1,P,trm[name2⊨n>y]{y:=<c>.P},y,P,trm)" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case using fin_AndL1_elim[OF AndL1.prems(1)] by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL1 fresh_prod nrename_fresh subst_fresh(3)) next case (AndL2 name1 trm name2) obtain z::name where"z ♯ (name2,name1,P,trm[name2⊨n>y]{y:=<c>.P},y,P,trm)" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case using fin_AndL2_elim[OF AndL2.prems(1)] by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL2 fresh_prod nrename_fresh subst_fresh(3)) next case (OrL name1 trm1 name2 trm2 name3) obtain z::name where"z ♯ (name3,name2,name1,P,trm1[name3⊨n>y]{y:=<c>.P},trm2[name3⊨n>y]{y:=<c>.P},y,P,trm1,trm2)" by (meson exists_fresh(1) fs_name1) with OrL show ?case using fin_OrL_elim[OF OrL.prems(1)] by (auto simp add: abs_fresh fresh_fun_simp_OrL fresh_atm(1) nrename_fresh subst_fresh(3)) next case (ImpL coname trm1 name1 trm2 name2) obtain z::name where"z ♯ (name1,x,P,trm1[x⊨n>y]{y:=<c>.P},trm2[x⊨n>y]{y:=<c>.P},y,P,trm1,trm2)" by (meson exists_fresh(1) fs_name1) with ImpL show ?case using fin_ImpL_elim[OF ImpL.prems(1)] by (auto simp add: abs_fresh fresh_fun_simp_ImpL fresh_atm(1) nrename_fresh subst_fresh(3)) qed (use fin_rest_elims in force)+
inductive
fic :: "trm → coname → bool" where
[intro]: "fic (Ax x a) a"
| [intro]: "a♯M ==> fic (NotR (x).M a) a"
| [intro]: "[c♯[a].M;c♯[b].N]==> fic (AndR <a>.M <b>.N c) c"
| [intro]: "b♯[a].M ==> fic (OrR1 <a>.M b) b"
| [intro]: "b♯[a].M ==> fic (OrR2 <a>.M b) b"
| [intro]: "[b♯[a].M]==> fic (ImpR (x).<a>.M b) b"
equivariance fic
lemma fic_Ax_elim: assumes"fic (Ax x a) b" shows"a=b" using assms by (auto simp: trm.inject elim!: fic.cases)
lemma fic_NotR_elim: assumes"fic (NotR (x).M a) b" shows"a=b ∧ b♯M" using assms by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6))
lemma fic_OrR1_elim: assumes"fic (OrR1 <a>.M b) c" shows"b=c ∧ c♯[a].M" using assms by (auto simp: trm.inject elim!: fic.cases)
lemma fic_OrR2_elim: assumes"fic (OrR2 <a>.M b) c" shows"b=c ∧ c♯[a].M" using assms by (auto simp: trm.inject elim!: fic.cases)
lemma fic_AndR_elim: assumes"fic (AndR <a>.M <b>.N c) d" shows"c=d ∧ d♯[a].M ∧ d♯[b].N" using assms by (auto simp: trm.inject elim!: fic.cases)
lemma fic_ImpR_elim: assumes a: "fic (ImpR (x).<a>.M b) c" shows"b=c ∧ b♯[a].M" using assms by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6))
lemma fic_rest_elims: shows"fic (Cut <a>.M (x).N) d ==> False" and"fic (NotL <a>.M x) d ==> False" and"fic (OrL (x).M (y).N z) d ==> False" and"fic (AndL1 (x).M y) d ==> False" and"fic (AndL2 (x).M y) d ==> False" and"fic (ImpL <a>.M (x).N y) d ==> False" by (erule fic.cases, simp_all add: trm.inject)+
lemma fic_rename: shows"fic M a ==> fic ([(a',a)]∙M) a'" by (induct rule: fic.induct)
(auto simp: calc_atm simp add: fresh_left abs_fresh)
lemma not_fic_subst1: assumes"¬(fic M a)" shows"¬(fic (M{y:=<c>.P}) a)" using assms proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct) case (Ax name coname) thenshow ?case using fic_rest_elims(1) substn.simps(1) by presburger next case (Cut coname trm1 name trm2) thenshow ?case by (metis abs_fresh(2) better_Cut_substn fic_rest_elims(1) fresh_prod) next case (NotR name trm coname) thenshow ?case by (metis fic.intros(2) fic_NotR_elim fresh_prod freshc_after_substn substn.simps(3)) next case (NotL coname trm name) obtain x'::name where"x' ♯ (trm{y:=<c>.P},P,a)" by (meson exists_fresh(1) fs_name1) with NotL show ?case by (simp add: fic.intros fresh_prod) (metis fic_rest_elims(1,2) fresh_fun_simp_NotL) next case (AndR coname1 trm1 coname2 trm2 coname3) thenshow ?case by simp (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substn) next case (AndL1 name1 trm name2) obtain x'::name where"x' ♯ (trm{y:=<c>.P},P,name1,a)" by (meson exists_fresh(1) fs_name1) with AndL1 fic_rest_elims show ?case by (simp add: fic.intros fresh_prod)(metis fresh_fun_simp_AndL1) next case (AndL2 name1 trm name2) obtain x'::name where"x' ♯ (trm{y:=<c>.P},P,name1,a)" by (meson exists_fresh(1) fs_name1) with AndL2 fic_rest_elims show ?case by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_AndL2) next case (OrR1 coname1 trm coname2) thenshow ?case by simp (metis abs_fresh(2) fic.simps fic_OrR1_elim freshc_after_substn) next case (OrR2 coname1 trm coname2) thenshow ?case by simp (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substn) next case (OrL name1 trm1 name2 trm2 name3) obtain x'::name where"x' ♯ (trm1{y:=<c>.P},trm2{y:=<c>.P},P,name1,name2,a)" by (meson exists_fresh(1) fs_name1) with OrL fic_rest_elims show ?case by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_OrL) next case (ImpR name coname1 trm coname2) thenshow ?case by simp (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substn) next case (ImpL coname trm1 name1 trm2 name2) obtain x'::name where"x' ♯ (trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,name1,name2,a)" by (meson exists_fresh(1) fs_name1) with ImpL fic_rest_elims fresh_fun_simp_ImpL show ?case by (simp add: fresh_prod) fastforce qed
lemma not_fic_subst2: assumes"¬(fic M a)" shows"¬(fic (M{c:=(y).P}) a)" using assms proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct) case (NotR name trm coname) obtain c'::coname where"c'♯(trm{coname:=(y).P},P,a)" by (meson exists_fresh'(2) fs_coname1) with NotR fic_rest_elims show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_NotR) by (metis fic.intros(2) fic_NotR_elim freshc_after_substc) next case (AndR coname1 trm1 coname2 trm2 coname3) obtain c'::coname where"c'♯(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,a)" by (meson exists_fresh'(2) fs_coname1) with AndR fic_rest_elims show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_AndR) by (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substc) next case (OrR1 coname1 trm coname2) obtain c'::coname where"c'♯(trm{coname2:=(y).P},P,coname1,a)" by (meson exists_fresh'(2) fs_coname1) with OrR1 fic_rest_elims show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR1) by (metis abs_fresh(2) fic.intros(4) fic_OrR1_elim freshc_after_substc) next case (OrR2 coname1 trm coname2) obtain c'::coname where"c'♯(trm{coname2:=(y).P},P,coname1,a)" by (meson exists_fresh'(2) fs_coname1) with OrR2 fic_rest_elims show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR2) by (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substc) next case (ImpR name coname1 trm coname2) obtain c'::coname where"c'♯(trm{coname2:=(y).P},P,coname1,a)" by (meson exists_fresh'(2) fs_coname1) with ImpR fic_rest_elims show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_ImpR) by (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substc) qed (use fic_rest_elims in auto)
lemma fic_subst1: assumes"fic M a""a≠b""a♯P" shows"fic (M{b:=(x).P}) a" using assms proof (nominal_induct M avoiding: x b a P rule: trm.strong_induct) case (Ax name coname) thenshow ?case using fic_Ax_elim by force next case (NotR name trm coname) with fic_NotR_elim show ?case by (fastforce simp add: fresh_prod subst_fresh) next case (AndR coname1 trm1 coname2 trm2 coname3) with fic_AndR_elim show ?case by (fastforce simp add: abs_fresh fresh_prod subst_fresh) next case (OrR1 coname1 trm coname2) with fic_OrR1_elim show ?case by (fastforce simp add: abs_fresh fresh_prod subst_fresh) next case (OrR2 coname1 trm coname2) with fic_OrR2_elim show ?case by (fastforce simp add: abs_fresh fresh_prod subst_fresh) next case (ImpR name coname1 trm coname2) with fic_ImpR_elim show ?case by (fastforce simp add: abs_fresh fresh_prod subst_fresh) qed (use fic_rest_elims in force)+
lemma fic_subst2: assumes"fic M a""c≠a""a♯P""M≠Ax x a" shows"fic (M{x:=<c>.P}) a" using assms proof (nominal_induct M avoiding: x a c P rule: trm.strong_induct) case (Ax name coname) thenshow ?case using fic_Ax_elim by force next case (NotR name trm coname) with fic_NotR_elim show ?case by (fastforce simp add: fresh_prod subst_fresh) next case (AndR coname1 trm1 coname2 trm2 coname3) with fic_AndR_elim show ?case by simp (metis abs_fresh(2) crename_cfresh crename_fresh fic.intros(3) fresh_atm(2) substn_crename_comm') next case (OrR1 coname1 trm coname2) with fic_OrR1_elim show ?case by (fastforce simp add: abs_fresh fresh_prod subst_fresh) next case (OrR2 coname1 trm coname2) with fic_OrR2_elim show ?case by (fastforce simp add: abs_fresh fresh_prod subst_fresh) next case (ImpR name coname1 trm coname2) with fic_ImpR_elim show ?case by (fastforce simp add: abs_fresh fresh_prod subst_fresh) qed (use fic_rest_elims in force)+
lemma fic_substc_crename: assumes"fic M a""a≠b""a♯P" shows"M[a⊨c>b]{b:=(y).P} = Cut <a>.(M{b:=(y).P}) (y).P" using assms proof (nominal_induct M avoiding: a b y P rule: trm.strong_induct) case (Ax name coname) with fic_Ax_elim show ?case by(force simp add: trm.inject alpha(2) fresh_atm(2,4) swap_simps(4,8)) next case (Cut coname trm1 name trm2) with fic_rest_elims show ?caseby force next case (NotR name trm coname) with fic_NotR_elim[OF NotR.prems(1)] show ?case by (simp add: trm.inject crename_fresh fresh_fun_simp_NotR subst_fresh(6)) next case (AndR coname1 trm1 coname2 trm2 coname3) with AndR fic_AndR_elim[OF AndR.prems(1)] show ?case by (simp add: abs_fresh rename_fresh fresh_fun_simp_AndR fresh_atm(2) subst_fresh(6)) next case (OrR1 coname1 trm coname2) with fic_OrR1_elim[OF OrR1.prems(1)] show ?case by (simp add: abs_fresh rename_fresh fresh_fun_simp_OrR1 fresh_atm(2) subst_fresh(6)) next case (OrR2 coname1 trm coname2) with fic_OrR2_elim[OF OrR2.prems(1)] show ?case by (simp add: abs_fresh rename_fresh fresh_fun_simp_OrR2 fresh_atm(2) subst_fresh(6)) next case (ImpR name coname1 trm coname2) with fic_ImpR_elim[OF ImpR.prems(1)] crename_fresh show ?case by (force simp add: abs_fresh fresh_fun_simp_ImpR fresh_atm(2) subst_fresh(6)) qed (use fic_rest_elims in force)+
lemma fresh_l_redu_x: fixes z::"name" shows"M ⟶l M' ==> z♯M ==> z♯M'" proof (induct rule: l_redu.induct) case (LAxL a M x y) thenshow ?case by (metis abs_fresh(1,5) nrename_nfresh nrename_rename trm.fresh(1,3)) next case (LImp z N y P x M b a c) thenshow ?case apply (simp add: abs_fresh fresh_prod) by (metis abs_fresh(3,5) abs_supp(5) fs_name1) qed (auto simp add: abs_fresh fresh_prod crename_nfresh)
lemma fresh_l_redu_a: fixes c::"coname" shows"M ⟶l M' ==> c♯M ==> c♯M'" proof (induct rule: l_redu.induct) case (LAxR x M a b) thenshow ?case apply (simp add: abs_fresh) by (metis crename_cfresh crename_rename) next case (LAxL a M x y) with nrename_cfresh show ?case by (simp add: abs_fresh) qed (auto simp add: abs_fresh fresh_prod crename_nfresh)
nominal_inductive c_redu
by (simp_all add: abs_fresh subst_fresh)
lemma better_left[intro]:
shows "\<not>fic M a \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^sub>c M{a:=(x).N}"
proof -
assume not_fic: "\<not>fic M a"
obtain x'::"name" where fs1: "x'\<sharp>(N,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(a,M,N)" by (rule exists_fresh(2), rule fin_supp, blast)
have "Cut <a>.M (x).N = Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>c ([(a',a)]\<bullet>M){a':=(x').([(x',x)]\<bullet>N)}" using fs1 fs2 not_fic
apply(intro left)
apply (metis fic_rename perm_swap(4))
apply(simp add: fresh_left calc_atm)+
done
also have "\<dots> = M{a:=(x).N}" using fs1 fs2
by (simp add: subst_rename[symmetric] fresh_atm fresh_prod fresh_left calc_atm) finally show ?thesis by simp
qed
lemma better_right[intro]:
shows "\<not>fin N x \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^sub>c N{x:=<a>.M}"
proof -
assume not_fin: "\<not>fin N x"
obtain x'::"name" where fs1: "x'\<sharp>(N,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(a,M,N)" by (rule exists_fresh(2), rule fin_supp, blast)
have "Cut <a>.M (x).N = Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>c ([(x',x)]\<bullet>N){x':=<a'>.([(a',a)]\<bullet>M)}" using fs1 fs2 not_fin
apply (intro right)
apply (metis fin_rename perm_swap(3))
apply (simp add: fresh_left calc_atm)+
done
also have "\<dots> = N{x:=<a>.M}" using fs1 fs2
by (simp add: subst_rename[symmetric] fresh_atm fresh_prod fresh_left calc_atm) finally show ?thesis by simp
qed
lemma better_CutL_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^sub>a Cut <a>.M' (x).N"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain x'::"name" where fs1: "x'\<sharp>(M,N,x)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
have "Cut <a>.M (x).N = Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a Cut <a'>.([(a',a)]\<bullet>M') (x').([(x',x)]\<bullet>N)" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt)
also have "\<dots> = Cut <a>.M' (x).N"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_CutR_intro[intro]:
shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^sub>a Cut <a>.M (x).N'"
proof -
assume red: "N\<longrightarrow>\<^sub>a N'"
obtain x'::"name" where fs1: "x'\<sharp>(M,N,x)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
have "Cut <a>.M (x).N = Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N')" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt)
also have "\<dots> = Cut <a>.M (x).N'"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_AndRL_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^sub>a AndR <a>.M' <b>.N c"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain b'::"coname" where fs1: "b'\<sharp>(M,N,a,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,b,c,b')" by (rule exists_fresh(2), rule fin_supp, blast)
have "AndR <a>.M <b>.N c = AndR <a'>.([(a',a)]\<bullet>M) <b'>.([(b',b)]\<bullet>N) c"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a AndR <a'>.([(a',a)]\<bullet>M') <b'>.([(b',b)]\<bullet>N) c" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = AndR <a>.M' <b>.N c"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_AndRR_intro[intro]:
shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^sub>a AndR <a>.M <b>.N' c"
proof -
assume red: "N\<longrightarrow>\<^sub>a N'"
obtain b'::"coname" where fs1: "b'\<sharp>(M,N,a,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,b,c,b')" by (rule exists_fresh(2), rule fin_supp, blast)
have "AndR <a>.M <b>.N c = AndR <a'>.([(a',a)]\<bullet>M) <b'>.([(b',b)]\<bullet>N) c"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a AndR <a'>.([(a',a)]\<bullet>M) <b'>.([(b',b)]\<bullet>N') c" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = AndR <a>.M <b>.N' c"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_AndL1_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> AndL1 (x).M y \<longrightarrow>\<^sub>a AndL1 (x).M' y"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain x'::"name" where fs1: "x'\<sharp>(M,y,x)" by (rule exists_fresh(1), rule fin_supp, blast)
have "AndL1 (x).M y = AndL1 (x').([(x',x)]\<bullet>M) y"
using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a AndL1 (x').([(x',x)]\<bullet>M') y" using fs1 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = AndL1 (x).M' y"
using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_AndL2_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> AndL2 (x).M y \<longrightarrow>\<^sub>a AndL2 (x).M' y"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain x'::"name" where fs1: "x'\<sharp>(M,y,x)" by (rule exists_fresh(1), rule fin_supp, blast)
have "AndL2 (x).M y = AndL2 (x').([(x',x)]\<bullet>M) y"
using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a AndL2 (x').([(x',x)]\<bullet>M') y" using fs1 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = AndL2 (x).M' y"
using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_OrLL_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^sub>a OrL (x).M' (y).N z"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain x'::"name" where fs1: "x'\<sharp>(M,N,x,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain y'::"name" where fs2: "y'\<sharp>(M,N,x,y,z,x')" by (rule exists_fresh(1), rule fin_supp, blast)
have "OrL (x).M (y).N z = OrL (x').([(x',x)]\<bullet>M) (y').([(y',y)]\<bullet>N) z"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a OrL (x').([(x',x)]\<bullet>M') (y').([(y',y)]\<bullet>N) z" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = OrL (x).M' (y).N z"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_OrLR_intro[intro]:
shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^sub>a OrL (x).M (y).N' z"
proof -
assume red: "N\<longrightarrow>\<^sub>a N'"
obtain x'::"name" where fs1: "x'\<sharp>(M,N,x,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain y'::"name" where fs2: "y'\<sharp>(M,N,x,y,z,x')" by (rule exists_fresh(1), rule fin_supp, blast)
have "OrL (x).M (y).N z = OrL (x').([(x',x)]\<bullet>M) (y').([(y',y)]\<bullet>N) z"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a OrL (x').([(x',x)]\<bullet>M) (y').([(y',y)]\<bullet>N') z" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = OrL (x).M (y).N' z"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_OrR1_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> OrR1 <a>.M b \<longrightarrow>\<^sub>a OrR1 <a>.M' b"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain a'::"coname" where fs1: "a'\<sharp>(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
have "OrR1 <a>.M b = OrR1 <a'>.([(a',a)]\<bullet>M) b"
using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a OrR1 <a'>.([(a',a)]\<bullet>M') b" using fs1 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = OrR1 <a>.M' b"
using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_OrR2_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> OrR2 <a>.M b \<longrightarrow>\<^sub>a OrR2 <a>.M' b"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain a'::"coname" where fs1: "a'\<sharp>(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
have "OrR2 <a>.M b = OrR2 <a'>.([(a',a)]\<bullet>M) b"
using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a OrR2 <a'>.([(a',a)]\<bullet>M') b" using fs1 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = OrR2 <a>.M' b"
using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_ImpLL_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> ImpL <a>.M (x).N y \<longrightarrow>\<^sub>a ImpL <a>.M' (x).N y"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain x'::"name" where fs1: "x'\<sharp>(M,N,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
have "ImpL <a>.M (x).N y = ImpL <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N) y"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a ImpL <a'>.([(a',a)]\<bullet>M') (x').([(x',x)]\<bullet>N) y" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = ImpL <a>.M' (x).N y"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_ImpLR_intro[intro]:
shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> ImpL <a>.M (x).N y \<longrightarrow>\<^sub>a ImpL <a>.M (x).N' y"
proof -
assume red: "N\<longrightarrow>\<^sub>a N'"
obtain x'::"name" where fs1: "x'\<sharp>(M,N,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
have "ImpL <a>.M (x).N y = ImpL <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N) y"
using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a ImpL <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N') y" using fs1 fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = ImpL <a>.M (x).N' y"
using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
lemma better_ImpR_intro[intro]:
shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> ImpR (x).<a>.M b \<longrightarrow>\<^sub>a ImpR (x).<a>.M' b"
proof -
assume red: "M\<longrightarrow>\<^sub>a M'"
obtain a'::"coname" where fs2: "a'\<sharp>(M,a,b)" by (rule exists_fresh(2), rule fin_supp, blast)
have "ImpR (x).<a>.M b = ImpR (x).<a'>.([(a',a)]\<bullet>M) b"
using fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
also have "\<dots> \<longrightarrow>\<^sub>a ImpR (x).<a'>.([(a',a)]\<bullet>M') b" using fs2 red
by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
also have "\<dots> = ImpR (x).<a>.M' b"
using fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finally show ?thesis by simp
qed
text \<open>axioms do not reduce\<close>
lemma ax_do_not_l_reduce:
shows "Ax x a \<longrightarrow>\<^sub>l M \<Longrightarrow> False"
by (erule_tac l_redu.cases) (simp_all add: trm.inject)
lemma ax_do_not_c_reduce:
shows "Ax x a \<longrightarrow>\<^sub>c M \<Longrightarrow> False"
by (erule_tac c_redu.cases) (simp_all add: trm.inject)
lemma ax_do_not_a_reduce:
shows "Ax x a \<longrightarrow>\<^sub>a M \<Longrightarrow> False"
apply(erule_tac a_redu.cases)
apply(simp_all add: trm.inject)
using ax_do_not_l_reduce ax_do_not_c_reduce by blast+
lemma a_starE:
assumes a: "M \<longrightarrow>\<^sub>a* M'"
shows "M = M' \<or> (\<exists>N. M \<longrightarrow>\<^sub>a N \<and> N \<longrightarrow>\<^sub>a* M')"
using a by (induct) (auto)
lemma a_star_refl:
shows "M \<longrightarrow>\<^sub>a* M"
by blast
declare rtranclp_trans [trans]
text \<open>congruence rules for \<open>\<longrightarrow>\<^sub>a*\<close>\<close>
lemma ax_do_not_a_star_reduce:
shows "Ax x a \<longrightarrow>\<^sub>a* M \<Longrightarrow> M = Ax x a"
using a_starE ax_do_not_a_reduce by blast
lemma a_star_redu_NotL_elim:
assumes "NotL <a>.M x \<longrightarrow>\<^sub>a* R"
shows "\<exists>M'. R = NotL <a>.M' x \<and> M \<longrightarrow>\<^sub>a* M'"
using assms by (induct set: rtranclp) (use a_redu_NotL_elim in force)+
lemma a_star_redu_NotR_elim:
assumes "NotR (x).M a \<longrightarrow>\<^sub>a* R"
shows "\<exists>M'. R = NotR (x).M' a \<and> M \<longrightarrow>\<^sub>a* M'"
using assms by (induct set: rtranclp) (use a_redu_NotR_elim in force)+
lemma a_star_redu_AndR_elim:
assumes "AndR <a>.M <b>.N c\<longrightarrow>\<^sub>a* R"
shows "(\<exists>M' N'. R = AndR <a>.M' <b>.N' c \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
using assms by (induct set: rtranclp) (use a_redu_AndR_elim in force)+
lemma a_star_redu_AndL1_elim:
assumes "AndL1 (x).M y \<longrightarrow>\<^sub>a* R"
shows "\<exists>M'. R = AndL1 (x).M' y \<and> M \<longrightarrow>\<^sub>a* M'"
using assms by (induct set: rtranclp) (use a_redu_AndL1_elim in force)+
lemma a_star_redu_AndL2_elim:
assumes "AndL2 (x).M y \<longrightarrow>\<^sub>a* R"
shows "\<exists>M'. R = AndL2 (x).M' y \<and> M \<longrightarrow>\<^sub>a* M'"
using assms by (induct set: rtranclp) (use a_redu_AndL2_elim in force)+
lemma a_star_redu_OrL_elim:
assumes "OrL (x).M (y).N z \<longrightarrow>\<^sub>a* R"
shows "(\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
using assms by (induct set: rtranclp) (use a_redu_OrL_elim in force)+
lemma a_star_redu_OrR1_elim:
assumes "OrR1 <a>.M y \<longrightarrow>\<^sub>a* R"
shows "\<exists>M'. R = OrR1 <a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
using assms by (induct set: rtranclp) (use a_redu_OrR1_elim in force)+
lemma a_star_redu_OrR2_elim:
assumes "OrR2 <a>.M y \<longrightarrow>\<^sub>a* R"
shows "\<exists>M'. R = OrR2 <a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
using assms by (induct set: rtranclp) (use a_redu_OrR2_elim in force)+
lemma a_star_redu_ImpR_elim:
assumes "ImpR (x).<a>.M y \<longrightarrow>\<^sub>a* R"
shows "\<exists>M'. R = ImpR (x).<a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
using assms by (induct set: rtranclp) (use a_redu_ImpR_elim in force)+
lemma a_star_redu_ImpL_elim:
assumes "ImpL <a>.M (y).N z \<longrightarrow>\<^sub>a* R"
shows "(\<exists>M' N'. R = ImpL <a>.M' (y).N' z \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
using assms by (induct set: rtranclp) (use a_redu_ImpL_elim in force)+
text \<open>Substitution\<close>
lemma subst_not_fin1:
shows "\<not>fin(M{x:=<c>.P}) x"
proof (nominal_induct M avoiding: x c P rule: trm.strong_induct) case (Ax name coname)
with fin_rest_elims show ?case
by (auto simp: fin_Ax_elim)
next case (NotL coname trm name)
obtain x'::name where "x'\<sharp>(trm{x:=<c>.P},P)"
by (meson exists_fresh(1) fs_name1)
with NotL fin_NotL_elim fresh_fun_simp_NotL show ?case
by simp (metis fin_rest_elims(1) fresh_prod)
next case (AndL1 name1 trm name2)
obtain x'::name where "x' \<sharp> (trm{x:=<c>.P},P,name1)"
by (meson exists_fresh(1) fs_name1)
with AndL1 fin_AndL1_elim fresh_fun_simp_AndL1 show ?case
by simp (metis fin_rest_elims(1) fresh_prod)
next case (AndL2 name2 trm name2)
obtain x'::name where "x' \<sharp> (trm{x:=<c>.P},P,name2)"
by (meson exists_fresh(1) fs_name1)
with AndL2 fin_AndL2_elim fresh_fun_simp_AndL2 better_AndL2_substn show ?case
by (metis abs_fresh(1) fresh_atm(1) not_fin_subst2)
next case (OrL name1 trm1 name2 trm2 name3)
obtain x'::name where "x' \<sharp> (trm1{x:=<c>.P},P,name1,trm2{x:=<c>.P},name2)"
by (meson exists_fresh(1) fs_name1)
with OrL fin_OrL_elim fresh_fun_simp_OrL show ?case
by simp (metis fin_rest_elims(1) fresh_prod)
next case (ImpL coname trm1 name1 trm2 name2)
obtain x'::name where "x' \<sharp> (trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
by (meson exists_fresh(1) fs_name1)
with ImpL fin_ImpL_elim fresh_fun_simp_ImpL show ?case
by simp (metis fin_rest_elims(1) fresh_prod)
qed (use fin_rest_elims not_fin_subst2 in auto)
lemmas subst_not_fin2 = not_fin_subst1
text \<open>Reductions\<close>
lemma fin_l_reduce:
assumes "fin M x" and "M \<longrightarrow>\<^sub>l M'"
shows "fin M' x"
using assms fin_rest_elims(1) l_redu.simps by fastforce
lemma fin_c_reduce:
assumes "fin M x" and "M \<longrightarrow>\<^sub>c M'"
shows "fin M' x"
using assms c_redu.simps fin_rest_elims(1) by fastforce
lemma fin_a_reduce:
assumes a: "fin M x"
and b: "M \<longrightarrow>\<^sub>a M'"
shows "fin M' x"
using assms
proof (induct) case (1 x a)
then show ?case
using ax_do_not_a_reduce by auto
next case (2 x M a)
then show ?case
using a_redu_NotL_elim fresh_a_redu1 by blast
next case (3 y x M)
then show ?case
by (metis a_redu_AndL1_elim abs_fresh(1) fin.intros(3) fresh_a_redu1)
next case (4 y x M)
then show ?case
by (metis a_redu_AndL2_elim abs_fresh(1) fin.intros(4) fresh_a_redu1)
next case (5 z x M y N)
then show ?case
by (smt (verit) a_redu_OrL_elim abs_fresh(1) fin.intros(5) fresh_a_redu1)
next case (6 y M x N a)
then show ?case
by (smt (verit, best) a_redu_ImpL_elim abs_fresh(1) fin.simps fresh_a_redu1)
qed
lemma fin_a_star_reduce:
assumes a: "fin M x"
and b: "M \<longrightarrow>\<^sub>a* M'"
shows "fin M' x"
using b a by (induct set: rtranclp)(auto simp: fin_a_reduce)
lemma fic_l_reduce:
assumes a: "fic M x"
and b: "M \<longrightarrow>\<^sub>l M'"
shows "fic M' x"
using b a
by induction (use fic_rest_elims in force)+
lemma fic_c_reduce:
assumes a: "fic M x"
and b: "M \<longrightarrow>\<^sub>c M'"
shows "fic M' x"
using b a
by induction (use fic_rest_elims in force)+
lemma fic_a_reduce:
assumes a: "fic M x"
and b: "M \<longrightarrow>\<^sub>a M'"
shows "fic M' x"
using assms
proof induction case (1 x a)
then show ?case
using ax_do_not_a_reduce by fastforce
next case (2 a M x)
then show ?case
using a_redu_NotR_elim fresh_a_redu2 by blast
next case (3 c a M b N)
then show ?case
by (smt (verit) a_redu_AndR_elim abs_fresh(2) fic.intros(3) fresh_a_redu2)
next case (4 b a M)
then show ?case
by (metis a_redu_OrR1_elim abs_fresh(2) fic.intros(4) fresh_a_redu2)
next case (5 b a M)
then show ?case
by (metis a_redu_OrR2_elim abs_fresh(2) fic.simps fresh_a_redu2)
next case (6 b a M x)
then show ?case
by (metis a_redu_ImpR_elim abs_fresh(2) fic.simps fresh_a_redu2)
qed
lemma fic_a_star_reduce:
assumes a: "fic M x"
and b: "M \<longrightarrow>\<^sub>a* M'"
shows "fic M' x"
using b a
by (induct set: rtranclp) (auto simp: fic_a_reduce)
text \<open>substitution properties\<close>
lemma subst_with_ax1:
shows "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]"
proof(nominal_induct M avoiding: x a y rule: trm.strong_induct) case (Ax z b x a y)
show "(Ax z b){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (Ax z b)[x\<turnstile>n>y]"
proof (cases "z=x") caseTrue
assume eq: "z=x"
have "(Ax z b){x:=<a>.Ax y a} = Cut <a>.Ax y a (x).Ax x b" using eq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* (Ax x b)[x\<turnstile>n>y]" by blast finally show "Ax z b{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (Ax z b)[x\<turnstile>n>y]" using eq by simp
next caseFalse
assume neq: "z\<noteq>x"
then show "(Ax z b){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (Ax z b)[x\<turnstile>n>y]" using neq by simp
qed
next case (Cut b M z N x a y)
have fs: "b\<sharp>x""b\<sharp>a""b\<sharp>y""b\<sharp>N""z\<sharp>x""z\<sharp>a""z\<sharp>y""z\<sharp>M" by fact+
have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* N[x\<turnstile>n>y]" by fact
show "(Cut <b>.M (z).N){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (Cut <b>.M (z).N)[x\<turnstile>n>y]"
proof (cases "M = Ax x b") caseTrue
assume eq: "M = Ax x b"
have "(Cut <b>.M (z).N){x:=<a>.Ax y a} = Cut <a>.Ax y a (z).(N{x:=<a>.Ax y a})" using fs eq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* Cut <a>.Ax y a (z).(N[x\<turnstile>n>y])" using ih2 a_star_congs by blast
also have "\<dots> = Cut <b>.(M[x\<turnstile>n>y]) (z).(N[x\<turnstile>n>y])" using eq
by (simp add: trm.inject alpha calc_atm fresh_atm) finally show "(Cut <b>.M (z).N){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (Cut <b>.M (z).N)[x\<turnstile>n>y]" using fs by simp
next caseFalse
assume neq: "M \<noteq> Ax x b"
have "(Cut <b>.M (z).N){x:=<a>.Ax y a} = Cut <b>.(M{x:=<a>.Ax y a}) (z).(N{x:=<a>.Ax y a})"
using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* Cut <b>.(M[x\<turnstile>n>y]) (z).(N[x\<turnstile>n>y])" using ih1 ih2 a_star_congs by blast finally show "(Cut <b>.M (z).N){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (Cut <b>.M (z).N)[x\<turnstile>n>y]" using fs by simp
qed
next case (NotR z M b x a y)
have fs: "z\<sharp>x""z\<sharp>a""z\<sharp>y""z\<sharp>b" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have "(NotR (z).M b){x:=<a>.Ax y a} = NotR (z).(M{x:=<a>.Ax y a}) b" using fs by simp
also have "\<dots> \<longrightarrow>\<^sub>a* NotR (z).(M[x\<turnstile>n>y]) b" using ih by (auto intro: a_star_congs) finally show "(NotR (z).M b){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (NotR (z).M b)[x\<turnstile>n>y]" using fs by simp
next case (NotL b M z x a y)
have fs: "b\<sharp>x""b\<sharp>a""b\<sharp>y""b\<sharp>z" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
show "(NotL <b>.M z){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (NotL <b>.M z)[x\<turnstile>n>y]"
proof(cases "z=x") caseTrue
assume eq: "z=x"
obtain x'::"name" where new: "x'\<sharp>(Ax y a,M{x:=<a>.Ax y a})" by (rule exists_fresh(1)[OF fs_name1])
have "(NotL <b>.M z){x:=<a>.Ax y a} =
fresh_fun (\<lambda>x'. Cut <a>.Ax y a (x').NotL <b>.(M{x:=<a>.Ax y a}) x')"
using eq fs by simp
also have "\<dots> = Cut <a>.Ax y a (x').NotL <b>.(M{x:=<a>.Ax y a}) x'"
using new by (simp add: fresh_fun_simp_NotL fresh_prod)
also have "\<dots> \<longrightarrow>\<^sub>a* (NotL <b>.(M{x:=<a>.Ax y a}) x')[x'\<turnstile>n>y]"
using new
by (intro a_starI al_redu better_LAxL_intro) auto
also have "\<dots> = NotL <b>.(M{x:=<a>.Ax y a}) y" using new by (simp add: nrename_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* NotL <b>.(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
also have "\<dots> = (NotL <b>.M z)[x\<turnstile>n>y]" using eq by simp finally show "(NotL <b>.M z){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (NotL <b>.M z)[x\<turnstile>n>y]" by simp
next caseFalse
assume neq: "z\<noteq>x"
have "(NotL <b>.M z){x:=<a>.Ax y a} = NotL <b>.(M{x:=<a>.Ax y a}) z" using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* NotL <b>.(M[x\<turnstile>n>y]) z" using ih by (auto intro: a_star_congs) finally show "(NotL <b>.M z){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (NotL <b>.M z)[x\<turnstile>n>y]" using neq by simp
qed
next case (AndR c M d N e x a y)
have fs: "c\<sharp>x""c\<sharp>a""c\<sharp>y""d\<sharp>x""d\<sharp>a""d\<sharp>y""d\<noteq>c""c\<sharp>N""c\<sharp>e""d\<sharp>M""d\<sharp>e" by fact+
have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* N[x\<turnstile>n>y]" by fact
have "(AndR <c>.M <d>.N e){x:=<a>.Ax y a} = AndR <c>.(M{x:=<a>.Ax y a}) <d>.(N{x:=<a>.Ax y a}) e"
using fs by simp
also have "\<dots> \<longrightarrow>\<^sub>a* AndR <c>.(M[x\<turnstile>n>y]) <d>.(N[x\<turnstile>n>y]) e" using ih1 ih2 by (auto intro: a_star_congs) finally show "(AndR <c>.M <d>.N e){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndR <c>.M <d>.N e)[x\<turnstile>n>y]"
using fs by simp
next case (AndL1 u M v x a y)
have fs: "u\<sharp>x""u\<sharp>a""u\<sharp>y""u\<sharp>v" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
show "(AndL1 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL1 (u).M v)[x\<turnstile>n>y]"
proof(cases "v=x") caseTrue
assume eq: "v=x"
obtain v'::"name" where new: "v'\<sharp>(Ax y a,M{x:=<a>.Ax y a},u)" by (rule exists_fresh(1)[OF fs_name1])
have "(AndL1 (u).M v){x:=<a>.Ax y a} =
fresh_fun (\<lambda>v'. Cut <a>.Ax y a (v').AndL1 (u).(M{x:=<a>.Ax y a}) v')"
using eq fs by simp
also have "\<dots> = Cut <a>.Ax y a (v').AndL1 (u).(M{x:=<a>.Ax y a}) v'"
using new by (simp add: fresh_fun_simp_AndL1 fresh_prod)
also have "\<dots> \<longrightarrow>\<^sub>a* (AndL1 (u).(M{x:=<a>.Ax y a}) v')[v'\<turnstile>n>y]"
using new
by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp add: abs_fresh)
also have "\<dots> = AndL1 (u).(M{x:=<a>.Ax y a}) y" using fs new
by (auto simp: fresh_prod fresh_atm nrename_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* AndL1 (u).(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
also have "\<dots> = (AndL1 (u).M v)[x\<turnstile>n>y]" using eq fs by simp finally show "(AndL1 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL1 (u).M v)[x\<turnstile>n>y]" by simp
next caseFalse
assume neq: "v\<noteq>x"
have "(AndL1 (u).M v){x:=<a>.Ax y a} = AndL1 (u).(M{x:=<a>.Ax y a}) v" using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* AndL1 (u).(M[x\<turnstile>n>y]) v" using ih by (auto intro: a_star_congs) finally show "(AndL1 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL1 (u).M v)[x\<turnstile>n>y]" using fs neq by simp
qed
next case (AndL2 u M v x a y)
have fs: "u\<sharp>x""u\<sharp>a""u\<sharp>y""u\<sharp>v" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
show "(AndL2 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL2 (u).M v)[x\<turnstile>n>y]"
proof(cases "v=x") caseTrue
assume eq: "v=x"
obtain v'::"name" where new: "v'\<sharp>(Ax y a,M{x:=<a>.Ax y a},u)" by (rule exists_fresh(1)[OF fs_name1])
have "(AndL2 (u).M v){x:=<a>.Ax y a} =
fresh_fun (\<lambda>v'. Cut <a>.Ax y a (v').AndL2 (u).(M{x:=<a>.Ax y a}) v')"
using eq fs by simp
also have "\<dots> = Cut <a>.Ax y a (v').AndL2 (u).(M{x:=<a>.Ax y a}) v'"
using new by (simp add: fresh_fun_simp_AndL2 fresh_prod)
also have "\<dots> \<longrightarrow>\<^sub>a* (AndL2 (u).(M{x:=<a>.Ax y a}) v')[v'\<turnstile>n>y]"
using new
by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp add: abs_fresh)
also have "\<dots> = AndL2 (u).(M{x:=<a>.Ax y a}) y" using fs new
by (auto simp: fresh_prod fresh_atm nrename_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* AndL2 (u).(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
also have "\<dots> = (AndL2 (u).M v)[x\<turnstile>n>y]" using eq fs by simp finally show "(AndL2 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL2 (u).M v)[x\<turnstile>n>y]" by simp
next caseFalse
assume neq: "v\<noteq>x"
have "(AndL2 (u).M v){x:=<a>.Ax y a} = AndL2 (u).(M{x:=<a>.Ax y a}) v" using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* AndL2 (u).(M[x\<turnstile>n>y]) v" using ih by (auto intro: a_star_congs) finally show "(AndL2 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL2 (u).M v)[x\<turnstile>n>y]" using fs neq by simp
qed
next case (OrR1 c M d x a y)
have fs: "c\<sharp>x""c\<sharp>a""c\<sharp>y""c\<sharp>d" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have "(OrR1 <c>.M d){x:=<a>.Ax y a} = OrR1 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
also have "\<dots> \<longrightarrow>\<^sub>a* OrR1 <c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs) finally show "(OrR1 <c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (OrR1 <c>.M d)[x\<turnstile>n>y]" using fs by simp
next case (OrR2 c M d x a y)
have fs: "c\<sharp>x""c\<sharp>a""c\<sharp>y""c\<sharp>d" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have "(OrR2 <c>.M d){x:=<a>.Ax y a} = OrR2 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
also have "\<dots> \<longrightarrow>\<^sub>a* OrR2 <c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs) finally show "(OrR2 <c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (OrR2 <c>.M d)[x\<turnstile>n>y]" using fs by simp
next case (OrL u M v N z x a y)
have fs: "u\<sharp>x""u\<sharp>a""u\<sharp>y""v\<sharp>x""v\<sharp>a""v\<sharp>y""v\<noteq>u""u\<sharp>N""u\<sharp>z""v\<sharp>M""v\<sharp>z" by fact+
have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* N[x\<turnstile>n>y]" by fact
show "(OrL (u).M (v).N z){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (OrL (u).M (v).N z)[x\<turnstile>n>y]"
proof(cases "z=x") caseTrue
assume eq: "z=x"
obtain z'::"name" where new: "z'\<sharp>(Ax y a,M{x:=<a>.Ax y a},N{x:=<a>.Ax y a},u,v,y,a)"
by (rule exists_fresh(1)[OF fs_name1])
have "(OrL (u).M (v).N z){x:=<a>.Ax y a} =
fresh_fun (\<lambda>z'. Cut <a>.Ax y a (z').OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z')"
using eq fs by simp
also have "\<dots> = Cut <a>.Ax y a (z').OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z'"
using new by (simp add: fresh_fun_simp_OrL)
also have "\<dots> \<longrightarrow>\<^sub>a* (OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z')[z'\<turnstile>n>y]"
using new
by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp_all add: abs_fresh)
also have "\<dots> = OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) y" using fs new
by (auto simp: fresh_prod fresh_atm nrename_fresh subst_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* OrL (u).(M[x\<turnstile>n>y]) (v).(N[x\<turnstile>n>y]) y"
using ih1 ih2 by (auto intro: a_star_congs)
also have "\<dots> = (OrL (u).M (v).N z)[x\<turnstile>n>y]" using eq fs by simp finally show "(OrL (u).M (v).N z){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (OrL (u).M (v).N z)[x\<turnstile>n>y]" by simp
next caseFalse
assume neq: "z\<noteq>x"
have "(OrL (u).M (v).N z){x:=<a>.Ax y a} = OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) z"
using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* OrL (u).(M[x\<turnstile>n>y]) (v).(N[x\<turnstile>n>y]) z"
using ih1 ih2 by (auto intro: a_star_congs) finally show "(OrL (u).M (v).N z){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (OrL (u).M (v).N z)[x\<turnstile>n>y]" using fs neq by simp
qed
next case (ImpR z c M d x a y)
have fs: "z\<sharp>x""z\<sharp>a""z\<sharp>y""c\<sharp>x""c\<sharp>a""c\<sharp>y""z\<sharp>d""c\<sharp>d" by fact+
have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have "(ImpR (z).<c>.M d){x:=<a>.Ax y a} = ImpR (z).<c>.(M{x:=<a>.Ax y a}) d" using fs by simp
also have "\<dots> \<longrightarrow>\<^sub>a* ImpR (z).<c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs) finally show "(ImpR (z).<c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (ImpR (z).<c>.M d)[x\<turnstile>n>y]" using fs by simp
next case (ImpL c M u N v x a y)
have fs: "c\<sharp>x""c\<sharp>a""c\<sharp>y""u\<sharp>x""u\<sharp>a""u\<sharp>y""c\<sharp>N""c\<sharp>v""u\<sharp>M""u\<sharp>v" by fact+
have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]" by fact
have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* N[x\<turnstile>n>y]" by fact
show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (ImpL <c>.M (u).N v)[x\<turnstile>n>y]"
proof(cases "v=x") caseTrue
assume eq: "v=x"
obtain v'::"name" where new: "v'\<sharp>(Ax y a,M{x:=<a>.Ax y a},N{x:=<a>.Ax y a},y,a,u)"
by (rule exists_fresh(1)[OF fs_name1])
have "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} =
fresh_fun (\<lambda>v'. Cut <a>.Ax y a (v').ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v')"
using eq fs by simp
also have "\<dots> = Cut <a>.Ax y a (v').ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v'"
using new by (simp add: fresh_fun_simp_ImpL)
also have "\<dots> \<longrightarrow>\<^sub>a* (ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v')[v'\<turnstile>n>y]"
using new
by (intro a_starI a_redu.intros better_LAxL_intro fin.intros) (simp_all add: abs_fresh)
also have "\<dots> = ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) y" using fs new
by (auto simp: fresh_prod subst_fresh fresh_atm trm.inject alpha rename_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* ImpL <c>.(M[x\<turnstile>n>y]) (u).(N[x\<turnstile>n>y]) y"
using ih1 ih2 by (auto intro: a_star_congs)
also have "\<dots> = (ImpL <c>.M (u).N v)[x\<turnstile>n>y]" using eq fs by simp finally show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (ImpL <c>.M (u).N v)[x\<turnstile>n>y]" using fs by simp
next caseFalse
assume neq: "v\<noteq>x"
have "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} = ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) v"
using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* ImpL <c>.(M[x\<turnstile>n>y]) (u).(N[x\<turnstile>n>y]) v"
using ih1 ih2 by (auto intro: a_star_congs) finally show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (ImpL <c>.M (u).N v)[x\<turnstile>n>y]"
using fs neq by simp
qed
qed
lemma subst_with_ax2:
shows "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]"
proof(nominal_induct M avoiding: b a x rule: trm.strong_induct) case (Ax z c b a x)
show "(Ax z c){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (Ax z c)[b\<turnstile>c>a]"
proof (cases "c=b") caseTrue
assume eq: "c=b"
have "(Ax z c){b:=(x).Ax x a} = Cut <b>.Ax z c (x).Ax x a" using eq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* (Ax z c)[b\<turnstile>c>a]" using eq by blast finally show "(Ax z c){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (Ax z c)[b\<turnstile>c>a]" by simp
next caseFalse
assume neq: "c\<noteq>b"
then show "(Ax z c){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (Ax z c)[b\<turnstile>c>a]" by simp
qed
next case (Cut c M z N b a x)
have fs: "c\<sharp>b""c\<sharp>a""c\<sharp>x""c\<sharp>N""z\<sharp>b""z\<sharp>a""z\<sharp>x""z\<sharp>M" by fact+
have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* N[b\<turnstile>c>a]" by fact
show "(Cut <c>.M (z).N){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (Cut <c>.M (z).N)[b\<turnstile>c>a]"
proof (cases "N = Ax z b") caseTrue
assume eq: "N = Ax z b"
have "(Cut <c>.M (z).N){b:=(x).Ax x a} = Cut <c>.(M{b:=(x).Ax x a}) (x).Ax x a" using eq fs by simp
also have "\<dots> \<longrightarrow>\<^sub>a* Cut <c>.(M[b\<turnstile>c>a]) (x).Ax x a" using ih1 a_star_congs by blast
also have "\<dots> = Cut <c>.(M[b\<turnstile>c>a]) (z).(N[b\<turnstile>c>a])" using eq fs
by (simp add: trm.inject alpha calc_atm fresh_atm) finally show "(Cut <c>.M (z).N){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (Cut <c>.M (z).N)[b\<turnstile>c>a]" using fs by simp
next caseFalse
assume neq: "N \<noteq> Ax z b"
have "(Cut <c>.M (z).N){b:=(x).Ax x a} = Cut <c>.(M{b:=(x).Ax x a}) (z).(N{b:=(x).Ax x a})"
using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* Cut <c>.(M[b\<turnstile>c>a]) (z).(N[b\<turnstile>c>a])" using ih1 ih2 a_star_congs by blast finally show "(Cut <c>.M (z).N){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (Cut <c>.M (z).N)[b\<turnstile>c>a]" using fs by simp
qed
next case (NotR z M c b a x)
have fs: "z\<sharp>b""z\<sharp>a""z\<sharp>x""z\<sharp>c" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
show "(NotR (z).M c){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (NotR (z).M c)[b\<turnstile>c>a]"
proof (cases "c=b") caseTrue
assume eq: "c=b"
obtain a'::"coname" where new: "a'\<sharp>(Ax x a,M{b:=(x).Ax x a})" by (rule exists_fresh(2)[OF fs_coname1])
have "(NotR (z).M c){b:=(x).Ax x a} =
fresh_fun (\<lambda>a'. Cut <a'>.NotR (z).M{b:=(x).Ax x a} a' (x).Ax x a)"
using eq fs by simp
also have "\<dots> = Cut <a'>.NotR (z).M{b:=(x).Ax x a} a' (x).Ax x a"
using new by (simp add: fresh_fun_simp_NotR fresh_prod)
also have "\<dots> \<longrightarrow>\<^sub>a* (NotR (z).(M{b:=(x).Ax x a}) a')[a'\<turnstile>c>a]"
using new
by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) auto
also have "\<dots> = NotR (z).(M{b:=(x).Ax x a}) a" using new by (simp add: crename_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* NotR (z).(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
also have "\<dots> = (NotR (z).M c)[b\<turnstile>c>a]" using eq by simp finally show "(NotR (z).M c){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (NotR (z).M c)[b\<turnstile>c>a]" by simp
next caseFalse
assume neq: "c\<noteq>b"
have "(NotR (z).M c){b:=(x).Ax x a} = NotR (z).(M{b:=(x).Ax x a}) c" using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* NotR (z).(M[b\<turnstile>c>a]) c" using ih by (auto intro: a_star_congs) finally show "(NotR (z).M c){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (NotR (z).M c)[b\<turnstile>c>a]" using neq by simp
qed
next case (NotL c M z b a x)
have fs: "c\<sharp>b""c\<sharp>a""c\<sharp>x""c\<sharp>z" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
have "(NotL <c>.M z){b:=(x).Ax x a} = NotL <c>.(M{b:=(x).Ax x a}) z" using fs by simp
also have "\<dots> \<longrightarrow>\<^sub>a* NotL <c>.(M[b\<turnstile>c>a]) z" using ih by (auto intro: a_star_congs) finally show "(NotL <c>.M z){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (NotL <c>.M z)[b\<turnstile>c>a]" using fs by simp
next case (AndR c M d N e b a x)
have fs: "c\<sharp>b""c\<sharp>a""c\<sharp>x""d\<sharp>b""d\<sharp>a""d\<sharp>x""d\<noteq>c""c\<sharp>N""c\<sharp>e""d\<sharp>M""d\<sharp>e" by fact+
have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* N[b\<turnstile>c>a]" by fact
show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (AndR <c>.M <d>.N e)[b\<turnstile>c>a]"
proof(cases "e=b") caseTrue
assume eq: "e=b"
obtain e'::"coname" where new: "e'\<sharp>(Ax x a,M{b:=(x).Ax x a},N{b:=(x).Ax x a},c,d)"
by (rule exists_fresh(2)[OF fs_coname1])
have "(AndR <c>.M <d>.N e){b:=(x).Ax x a} =
fresh_fun (\<lambda>e'. Cut <e'>.AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e' (x).Ax x a)"
using eq fs by simp
also have "\<dots> = Cut <e'>.AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e' (x).Ax x a"
using new by (simp add: fresh_fun_simp_AndR fresh_prod)
also have "\<dots> \<longrightarrow>\<^sub>a* (AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e')[e'\<turnstile>c>a]"
using new
by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
also have "\<dots> = AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) a" using fs new
by (auto simp: fresh_prod fresh_atm subst_fresh crename_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* AndR <c>.(M[b\<turnstile>c>a]) <d>.(N[b\<turnstile>c>a]) a" using ih1 ih2 by (auto intro: a_star_congs)
also have "\<dots> = (AndR <c>.M <d>.N e)[b\<turnstile>c>a]" using eq fs by simp finally show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (AndR <c>.M <d>.N e)[b\<turnstile>c>a]" by simp
next caseFalse
assume neq: "e\<noteq>b"
have "(AndR <c>.M <d>.N e){b:=(x).Ax x a} = AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) e"
using fs neq by simp
also have "\<dots> \<longrightarrow>\<^sub>a* AndR <c>.(M[b\<turnstile>c>a]) <d>.(N[b\<turnstile>c>a]) e" using ih1 ih2 by (auto intro: a_star_congs) finally show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (AndR <c>.M <d>.N e)[b\<turnstile>c>a]"
using fs neq by simp
qed
next case (AndL1 u M v b a x)
have fs: "u\<sharp>b""u\<sharp>a""u\<sharp>x""u\<sharp>v" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
have "(AndL1 (u).M v){b:=(x).Ax x a} = AndL1 (u).(M{b:=(x).Ax x a}) v" using fs by simp
also have "\<dots> \<longrightarrow>\<^sub>a* AndL1 (u).(M[b\<turnstile>c>a]) v" using ih by (auto intro: a_star_congs) finally show "(AndL1 (u).M v){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (AndL1 (u).M v)[b\<turnstile>c>a]" using fs by simp
next case (AndL2 u M v b a x)
have fs: "u\<sharp>b""u\<sharp>a""u\<sharp>x""u\<sharp>v" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
have "(AndL2 (u).M v){b:=(x).Ax x a} = AndL2 (u).(M{b:=(x).Ax x a}) v" using fs by simp
also have "\<dots> \<longrightarrow>\<^sub>a* AndL2 (u).(M[b\<turnstile>c>a]) v" using ih by (auto intro: a_star_congs) finally show "(AndL2 (u).M v){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (AndL2 (u).M v)[b\<turnstile>c>a]" using fs by simp
next case (OrR1 c M d b a x)
have fs: "c\<sharp>b""c\<sharp>a""c\<sharp>x""c\<sharp>d" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
show "(OrR1 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR1 <c>.M d)[b\<turnstile>c>a]"
proof(cases "d=b") caseTrue
assume eq: "d=b"
obtain a'::"coname" where new: "a'\<sharp>(Ax x a,M{b:=(x).Ax x a},c,x,a)"
by (rule exists_fresh(2)[OF fs_coname1])
have "(OrR1 <c>.M d){b:=(x).Ax x a} =
fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <c>.M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by (simp)
also have "\<dots> = Cut <a'>.OrR1 <c>.M{b:=(x).Ax x a} a' (x).Ax x a"
using new by (simp add: fresh_fun_simp_OrR1)
also have "\<dots> \<longrightarrow>\<^sub>a* (OrR1 <c>.M{b:=(x).Ax x a} a')[a'\<turnstile>c>a]"
using new
by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
also have "\<dots> = OrR1 <c>.M{b:=(x).Ax x a} a" using fs new
by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* OrR1 <c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
also have "\<dots> = (OrR1 <c>.M d)[b\<turnstile>c>a]" using eq fs by simp finally show "(OrR1 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR1 <c>.M d)[b\<turnstile>c>a]" by simp
next caseFalse
assume neq: "d\<noteq>b"
have "(OrR1 <c>.M d){b:=(x).Ax x a} = OrR1 <c>.(M{b:=(x).Ax x a}) d" using fs neq by (simp)
also have "\<dots> \<longrightarrow>\<^sub>a* OrR1 <c>.(M[b\<turnstile>c>a]) d" using ih by (auto intro: a_star_congs) finally show "(OrR1 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR1 <c>.M d)[b\<turnstile>c>a]" using fs neq by simp
qed
next case (OrR2 c M d b a x)
have fs: "c\<sharp>b""c\<sharp>a""c\<sharp>x""c\<sharp>d" by fact+
have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
show "(OrR2 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR2 <c>.M d)[b\<turnstile>c>a]"
proof(cases "d=b") caseTrue
assume eq: "d=b"
obtain a'::"coname" where new: "a'\<sharp>(Ax x a,M{b:=(x).Ax x a},c,x,a)"
by (rule exists_fresh(2)[OF fs_coname1])
have "(OrR2 <c>.M d){b:=(x).Ax x a} =
fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <c>.M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by (simp)
also have "\<dots> = Cut <a'>.OrR2 <c>.M{b:=(x).Ax x a} a' (x).Ax x a"
using new by (simp add: fresh_fun_simp_OrR2)
also have "\<dots> \<longrightarrow>\<^sub>a* (OrR2 <c>.M{b:=(x).Ax x a} a')[a'\<turnstile>c>a]"
using new
by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh)
also have "\<dots> = OrR2 <c>.M{b:=(x).Ax x a} a" using fs new
by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
also have "\<dots> \<longrightarrow>\<^sub>a* OrR2 <c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
also have "\<dots> = (OrR2 <c>.M d)[b\<turnstile>c>a]" using eq fs by simp finally show "(OrR2 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR2 <c>.M d)[b\<turnstile>c>a]" by simp
next caseFalse
assume neq: "d\<noteq>b"
have "(OrR2 <c>.M d){b:=(x).Ax x a} = OrR2 <c>.(M{b:=(x).Ax x a}) d" using fs neq by (simp)
also have "\<dots> \<longrightarrow>\<^sub>a* OrR2 <c>.(M[b\<turnstile>c>a]) d" using ih by (auto intro: a_star_congs) finally show "(OrR2 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR2 <c>.M d)[b\<turnstile>c>a]" using fs neq by simp
qed
next case (OrL u M v N z b a x)
have fs: "u\<sharp>b""u\<sharp>a""u\<sharp>x""v\<sharp>b""v\<sharp>a""v\<sharp>x""v\<noteq>u""u\<sharp>N""u\<sharp>z""v\<sharp>M""v\<sharp>z" by fact+
have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* M[b\<turnstile>c>a]" by fact
have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^sub>a* N[b\<turnstile>c>a]" by fact
have "(OrL (u).M (v).N z){b:=(x).Ax x a} = OrL (u).(M{b:=(x).Ax x a}) (v).(N{b:=(x).Ax x a}) z"
using fs by simp
also have "…⟶a* OrL (u).(M[b⊨c>a]) (v).(N[b⊨c>a]) z" using ih1 ih2 by (auto intro: a_star_congs) finally show "(OrL (u).M (v).N z){b:=(x).Ax x a} ⟶a* (OrL (u).M (v).N z)[b⊨c>a]" using fs by simp next case (ImpR z c M d b a x) have fs: "z♯b" "z♯a" "z♯x" "c♯b" "c♯a" "c♯x" "z♯d" "c♯d" by fact+ have ih: "M{b:=(x).Ax x a} ⟶a* M[b⊨c>a]" by fact show "(ImpR (z).<c>.M d){b:=(x).Ax x a} ⟶a* (ImpR (z).<c>.M d)[b⊨c>a]" proof(cases "b=d") case True assume eq: "b=d" obtain a'::"coname" where new: "a'♯(Ax x a,M{b:=(x).Ax x a},x,a,c)" by (rule exists_fresh(2)[OF fs_coname1]) have "(ImpR (z).<c>.M d){b:=(x).Ax x a} = fresh_fun (λa'. Cut <a'>.ImpR z.<c>.M{b:=(x).Ax x a} a' (x).Ax x a)" using fs eq by simp also have "… = Cut <a'>.ImpR z.<c>.M{b:=(x).Ax x a} a' (x).Ax x a" using new by (simp add: fresh_fun_simp_ImpR) also have "…⟶a* (ImpR z.<c>.M{b:=(x).Ax x a} a')[a'⊨c>a]" using new by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh) also have "… = ImpR z.<c>.M{b:=(x).Ax x a} a" using fs new by (auto simp: fresh_prod crename_fresh subst_fresh fresh_atm) also have "…⟶a* ImpR z.<c>.(M[b⊨c>a]) a" using ih by (auto intro: a_star_congs) also have "… = (ImpR z.<c>.M b)[b⊨c>a]" using eq fs by simp finally show "(ImpR (z).<c>.M d){b:=(x).Ax x a} ⟶a* (ImpR (z).<c>.M d)[b⊨c>a]" using eq by simp next case False assume neq: "b≠d" have "(ImpR (z).<c>.M d){b:=(x).Ax x a} = ImpR (z).<c>.(M{b:=(x).Ax x a}) d" using fs neq by simp also have "…⟶a* ImpR (z).<c>.(M[b⊨c>a]) d" using ih by (auto intro: a_star_congs) finally show "(ImpR (z).<c>.M d){b:=(x).Ax x a} ⟶a* (ImpR (z).<c>.M d)[b⊨c>a]" using neq fs by simp qed next case (ImpL c M u N v b a x) have fs: "c♯b" "c♯a" "c♯x" "u♯b" "u♯a" "u♯x" "c♯N" "c♯v" "u♯M" "u♯v" by fact+ have ih1: "M{b:=(x).Ax x a} ⟶a* M[b⊨c>a]" by fact have ih2: "N{b:=(x).Ax x a} ⟶a* N[b⊨c>a]" by fact have "(ImpL <c>.M (u).N v){b:=(x).Ax x a} = ImpL <c>.(M{b:=(x).Ax x a}) (u).(N{b:=(x).Ax x a}) v" using fs by simp also have "…⟶a* ImpL <c>.(M[b⊨c>a]) (u).(N[b⊨c>a]) v" using ih1 ih2 by (auto intro: a_star_congs) finally show "(ImpL <c>.M (u).N v){b:=(x).Ax x a} ⟶a* (ImpL <c>.M (u).N v)[b⊨c>a]" using fs by simp qed
text ‹substitution lemmas›
lemma not_Ax1: "¬(b♯M) ==> M{b:=(y).Q} ≠ Ax x a" proof (nominal_induct M avoiding: b y Q x a rule: trm.strong_induct) case (NotR name trm coname) then show ?case by (metis fin.intros(1) fin_rest_elims(2) subst_not_fin2) next case (AndR coname1 trm1 coname2 trm2 coname3) then show ?case by (metis fin.intros(1) fin_rest_elims(3) subst_not_fin2) next case (OrR1 coname1 trm coname2) then show ?case by (metis fin.intros(1) fin_rest_elims(4) subst_not_fin2) next case (OrR2 coname1 trm coname2) then show ?case by (metis fin.intros(1) fin_rest_elims(5) subst_not_fin2) next case (ImpR name coname1 trm coname2) then show ?case by (metis fin.intros(1) fin_rest_elims(6) subst_not_fin2) qed (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
lemma not_Ax2: "¬(x♯M) ==> M{x:=<b>.Q} ≠ Ax y a" proof (nominal_induct M avoiding: b y Q x a rule: trm.strong_induct) case (NotL coname trm name) then show ?case by (metis fic.intros(1) fic_rest_elims(2) not_fic_subst1) next case (AndL1 name1 trm name2) then show ?case by (metis fic.intros(1) fic_rest_elims(4) not_fic_subst1) next case (AndL2 name1 trm name2) then show ?case by (metis fic.intros(1) fic_rest_elims(5) not_fic_subst1) next case (OrL name1 trm1 name2 trm2 name3) then show ?case by (metis fic.intros(1) fic_rest_elims(3) not_fic_subst1) next case (ImpL coname trm1 name1 trm2 name2) then show ?case by (metis fic.intros(1) fic_rest_elims(6) not_fic_subst1) qed (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
lemma interesting_subst1: assumes a: "x≠y" "x♯P" "y♯P" shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<c>.Ax y c}{y:=<c>.P}" using a proof(nominal_induct N avoiding: x y c P rule: trm.strong_induct) case (Cut d M u M' x' y' c P) with assms show ?case apply (simp add: abs_fresh) by (smt (verit) forget(1) not_Ax2) next case (NotL d M u) obtain x'::name and x''::name where "x' ♯ (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},y,x)" and "x''♯ (P,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},Ax y c,y,x)" by (meson exists_fresh(1) fs_name1) then show ?case using NotL by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget fresh_atm abs_fresh fresh_fun_simp_NotL fresh_prod) next case (AndL1 u M d) obtain x'::name and x''::name where "x' ♯ (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)" and "x''♯ (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)" by (meson exists_fresh(1) fs_name1) then show ?case using AndL1 by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget fresh_atm abs_fresh fresh_fun_simp_AndL1 fresh_prod) next case (AndL2 u M d) obtain x'::name and x''::name where "x' ♯ (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)" and "x''♯ (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)" by (meson exists_fresh(1) fs_name1) then show ?case using AndL2 by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget fresh_atm abs_fresh fresh_fun_simp_AndL2 fresh_prod) next case (OrL x1 M x2 M' x3) obtain x'::name and x''::name where "x' ♯ (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P}, M'{y:=<c>.P},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)" and "x''♯ (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P}, M'{x:=<c>.Ax y c},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)" by (meson exists_fresh(1) fs_name1) then show ?case using OrL by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget fresh_atm abs_fresh fresh_fun_simp_OrL fresh_prod subst_fresh) next case (ImpL a M x1 M' x2) obtain x'::name and x''::name where "x' ♯ (P,M{x2:=<c>.P},M{x:=<c>.Ax x2 c}{x2:=<c>.P}, M'{x2:=<c>.P},M'{x:=<c>.Ax x2 c}{x2:=<c>.P},x1,y,x)" and "x''♯ (P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P}, M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,y,x)" by (meson exists_fresh(1) fs_name1) then show ?case using ImpL by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget fresh_atm abs_fresh fresh_fun_simp_ImpL fresh_prod subst_fresh) qed (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
lemma interesting_subst1': assumes "x≠y" "x♯P" "y♯P" shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<a>.Ax y a}{y:=<c>.P}" proof - show ?thesis proof (cases "c=a") case True with assms show ?thesis by (simp add: interesting_subst1) next case False then have "N{x:=<a>.Ax y a} = N{x:=<c>.([(c,a)]∙Ax y a)}" by (simp add: fresh_atm(2,4) fresh_prod substn_rename4) with assms show ?thesis by (simp add: interesting_subst1 swap_simps) qed qed
lemma interesting_subst2: assumes a: "a≠b" "a♯P" "b♯P" shows "N{a:=(y).P}{b:=(y).P} = N{b:=(y).Ax y a}{a:=(y).P}" using a proof(nominal_induct N avoiding: a b y P rule: trm.strong_induct) case Ax then show ?case by (auto simp: abs_fresh fresh_atm forget trm.inject) next case (Cut d M u M' x' y' c P) with assms show ?case apply(auto simp: trm.inject) apply (force simp add: abs_fresh forget) apply (simp add: abs_fresh forget) by (smt (verit, ccfv_threshold) abs_fresh(1) better_Cut_substc forget(2) fresh_prod not_Ax1) next case NotL then show ?case by (auto simp: abs_fresh fresh_atm forget) next case (NotR u M d) obtain a' a''::coname where "a' ♯ (b,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P},u,y)" and "a'' ♯ (P,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P},Ax y a,y,d)" by (meson exists_fresh'(2) fs_coname1) with NotR show ?case by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_NotR) next case (AndR d1 M d2 M' d3) obtain a' a''::coname where "a' ♯ (P,M{d3:=(y).P},M{b:=(y).Ax y d3}{d3:=(y).P}, M'{d3:=(y).P},M'{b:=(y).Ax y d3}{d3:=(y).P},d1,d2,d3,b,y)" and "a'' ♯ (P,Ax y a,M{d3:=(y).Ax y a},M{d3:=(y).Ax y a}{a:=(y).P}, M'{d3:=(y).Ax y a},M'{d3:=(y).Ax y a}{a:=(y).P},d1,d2,d3,y,b)" by (meson exists_fresh'(2) fs_coname1) with AndR show ?case apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh) apply(auto simp only: fresh_prod fresh_fun_simp_AndR) apply (force simp: forget abs_fresh subst_fresh fresh_atm)+ done next case (AndL1 u M d) then show ?case by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh) next case (AndL2 u M d) then show ?case by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh) next case (OrR1 d M e) obtain a' a''::coname where "a' ♯ (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)" and "a'' ♯ (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)" by (meson exists_fresh'(2) fs_coname1) with OrR1 show ?case by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR1) next case (OrR2 d M e) obtain a' a''::coname where "a' ♯ (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)" and "a'' ♯ (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)" by (meson exists_fresh'(2) fs_coname1) with OrR2 show ?case by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR2) next case (OrL x1 M x2 M' x3) then show ?case by(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh) next case ImpL then show ?case by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh) next case (ImpR u e M d) obtain a' a''::coname where "a' ♯ (b,e,d,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P})" and "a'' ♯ (e,d,P,Ax y a,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P})" by (meson exists_fresh'(2) fs_coname1) with ImpR show ?case by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_ImpR) qed
lemma interesting_subst2': assumes "a≠b" "a♯P" "b♯P" shows "N{a:=(y).P}{b:=(y).P} = N{b:=(z).Ax z a}{a:=(y).P}" proof - show ?thesis proof (cases "z=y") case True then show ?thesis using assms by (simp add: interesting_subst2) next case False then have "N{b:=(z).Ax z a} = N{b:=(y).([(y,z)]∙Ax z a)}" by (metis fresh_atm(1,3) fresh_prod substc_rename2 trm.fresh(1)) with False assms show ?thesis by (simp add: interesting_subst2 calc_atm) qed qed
lemma subst_subst1: assumes a: "a♯(Q,b)" "x♯(y,P,Q)" "b♯Q" "y♯P" shows "M{x:=<a>.P}{b:=(y).Q} = M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using a proof(nominal_induct M avoiding: x a P b y Q rule: trm.strong_induct) case (Ax z c) then show ?case by (auto simp add: abs_fresh fresh_prod fresh_atm subst_fresh trm.inject forget) next case (Cut c M z N) then show ?case apply (clarsimp simp add: abs_fresh fresh_prod fresh_atm subst_fresh) apply (metis forget not_Ax1 not_Ax2) done next case (NotR z M c) then show ?case by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_NotR) next case (NotL c M z) obtain x'::name where "x' ♯ (P,M{x:=<a>.P},P{b:=(y).Q},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},y,Q)" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh subst_fresh fresh_fun_simp_NotL) by (metis fresh_fun_simp_NotL fresh_prod subst_fresh(5)) next case (AndR c1 M c2 N c3) then show ?case by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_AndR) next case (AndL1 z1 M z2) obtain x'::name where "x' ♯ (P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_AndL1) by (metis fresh_atm(1) fresh_fun_simp_AndL1 fresh_prod subst_fresh(5)) next case (AndL2 z1 M z2) obtain x'::name where "x' ♯ (P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_AndL2) by (metis fresh_atm(1) fresh_fun_simp_AndL2 fresh_prod subst_fresh(5)) next case (OrL z1 M z2 N z3) obtain x'::name where "x' ♯ (P,M{x:=<a>.P},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z2,z3,a,y,Q, P{b:=(y).Q},N{x:=<a>.P},N{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z1)" by (meson exists_fresh(1) fs_name1) with OrL show ?case apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_OrL) by (metis (full_types) fresh_atm(1) fresh_fun_simp_OrL fresh_prod subst_fresh(5)) next case (OrR1 c1 M c2) then show ?case by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR1) next case (OrR2 c1 M c2) then show ?case by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR2) next case (ImpR z c M d) then show ?case by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_ImpR) next case (ImpL c M z N u) obtain z'::name where "z' ♯ (P,P{b:=(y).Q},M{u:=<a>.P},N{u:=<a>.P},y,Q, M{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},N{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},z)" by (meson exists_fresh(1) fs_name1) with ImpL show ?case apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_ImpL) by (metis (full_types) fresh_atm(1) fresh_prod subst_fresh(5) fresh_fun_simp_ImpL) qed
lemma subst_subst2: assumes a: "a♯(b,P,N)" "x♯(y,P,M)" "b♯(M,N)" "y♯P" shows "M{a:=(x).N}{y:=<b>.P} = M{y:=<b>.P}{a:=(x).N{y:=<b>.P}}" using a proof(nominal_induct M avoiding: a x N y b P rule: trm.strong_induct) case (Ax z c) then show ?case by (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) next case (Cut d M' u M'') then show ?case apply (clarsimp simp add: abs_fresh fresh_prod fresh_atm subst_fresh) apply (metis forget not_Ax1 not_Ax2) done next case (NotR z M' d) obtain a'::coname where "a' ♯ (y,P,N,N{y:=<b>.P},M'{d:=(x).N},M'{y:=<b>.P}{d:=(x).N{y:=<b>.P}})" by (meson exists_fresh'(2) fs_coname1) with NotR show ?case apply(simp add: fresh_atm subst_fresh) apply(auto simp only: fresh_prod fresh_fun_simp_NotR; simp add: abs_fresh NotR) next stdM ) obtain x'::name where let b\^>1 = if bb = Rh then Lh else Bal; by (meson exists_fresh(1) fs_name1) with NotL show ?case afun inet:" 'a java.lang.StringIndexOutOfBoundsException: Range [56, 53) out of bounds for length 86
oL by pftm
java.lang.StringIndexOutOfBoundsException: Range [17, 16) out of bounds for length 58 obtain a'::coname where"a' ♯ (P,b,d,e,N,N{y:=<b>.P},M'{f:=(x).N},M''{f:=(x).N}, MiS ebOe by (meson exists_fresh'(2) fs_coname1) with AndR show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod) apply(subgoal_tac "∃a'::coname. a'♯(P,b,d,e,N,N{y:=b.P},M'{f:=(x).N},M''{f:=(x).N},
M'{y:=b.P}{f:=(x).N{y:=b.P}},M''{y:=b.P}{f:=(x).N{y:=b.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_AndR) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(2)[OF fs_coname1]) done next case (AndL1 z M' u) obtain x'::name where "x' ♯ (P,b,z,u,x,N,M'{y:=b.P},M'{y:=b.P}{a:=(x).N{y:=b.P}})" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case by (force simp add: fresh_prod fresh_atm fresh_fun_simp_AndL1 subst_fresh abs_fresh forget) next case (AndL2 z M' u) obtain x'::name where "x' ♯ (P,b,z,u,x,N,M'{y:=b.P},M'{y:=b.P}{a:=(x).N{y:=b.P}})" by (meson exists_fresh(1) fs_name1) with AndL2 show ?case by (force simp add: fresh_prod fresh_atm fresh_fun_simp_AndL2 subst_fresh abs_fresh forget) next case (OrL u M' v M'' w) obtain x'::name where "x' ♯ (P,b,u,w,v,N,N{y:=b.P},M'{y:=b.P},M''{y:=b.P},
M'{y:=b.P}{a:=(x).N{y:=b.P}},M''{y:=b.P}{a:=(x).N{y:=b.P}})" by (meson exists_fresh(1) fs_name1) with OrL show ?case by (force simp add: fresh_prod fresh_atm fresh_fun_simp_OrL subst_fresh abs_fresh forget) next case (OrR1 e M' f) obtain c'::coname where c': "c' ♯ (P,b,e,f,x,N,N{y:=b.P},
M'{f:=(x).N},M'{y:=b.P}{f:=(x).N{y:=b.P}})" by (meson exists_fresh(2) fs_coname1) with OrR1 show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR1) apply (clarsimp simp: subst_fresh abs_fresh fresh_atm) using c' apply (auto simp: fresh_prod fresh_fun_simp_OrR1) done next case (OrR2 e M' f) obtain c'::coname where c': "c' ♯ (P,b,e,f,x,N,N{y:=b.P},
M'{f:=(x).N},M'{y:=b.P}{f:=(x).N{y:=b.P}})" by (meson exists_fresh(2) fs_coname1) with OrR2 show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR2) apply (clarsimp simp: subst_fresh abs_fresh fresh_atm) using c' apply (auto simp: fresh_prod fresh_fun_simp_OrR2) done next case (ImpR x e M' f) obtain c'::coname where c': "c' ♯ (P,b,e,f,x,N,N{y:=b.P},
M'{f:=(x).N},M'{y:=b.P}{f:=(x).N{y:=b.P}})" by (meson exists_fresh(2) fs_coname1) with ImpR show ?case apply (clarsimp simp: fresh_prod fresh_fun_simp_ImpR) apply (clarsimp simp: subst_fresh abs_fresh fresh_atm) using c' apply (auto simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_fun_simp_ImpR) done next case (ImpL e M' v M'' w) obtain z'::name where z': "z' ♯ (P,b,e,w,v,N,N{y:=b.P},M'{w:=b.P},M''{w:=b.P},
M'{w:=b.P}{a:=(x).N{w:=b.P}},M''{w:=b.P}{a:=(x).N{w:=b.P}})" by (meson exists_fresh(1) fs_name1) with ImpL show ?case by (force simp add: fresh_prod fresh_atm fresh_fun_simp_ImpL subst_fresh abs_fresh forget) qed
lemma subst_subst3: assumes a: "a♯(P,N,c)" "c♯(M,N)" "x♯(y,P,M)" "y♯(P,x)" "M≠Ax y a" shows "N{x:=a.M}{y:=c.P} = N{y:=c.P}{x:=a.(M{y:=c.P})}" using a proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct) case (Ax z c) then show ?case by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) next case (Cut d M' u M'') then show ?case apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh) apply(auto) apply(auto simp add: fresh_atm trm.inject forget) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply (metis forget(1) not_Ax2) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule sym) apply(rule trans) apply(rule better_Cut_substn) apply(simp add: abs_fresh subst_fresh) apply(simp add: fresh_prod subst_fresh fresh_atm) apply(simp) by (metis forget(1) not_Ax2) next case NotR then show ?case by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) next case (NotL d M' u) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(subgoal_tac "∃x'::name. x'♯(y,P,M,M{y:=c.P},M'{x:=a.M},M'{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_NotL) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) apply(subgoal_tac "∃x'::name. x'♯(x,y,P,M,M'{y:=c.P},M'{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_NotL) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) done next case AndR then show ?case by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) next case (AndL1 u M' v) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(subgoal_tac "∃x'::name. x'♯(u,y,v,P,M,M{y:=c.P},M'{x:=a.M},M'{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_AndL1) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) apply(subgoal_tac "∃x'::name. x'♯(x,y,u,v,P,M,M'{y:=c.P},M'{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_AndL1) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) done next case (AndL2 u M' v) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(subgoal_tac "∃x'::name. x'♯(u,y,v,P,M,M{y:=c.P},M'{x:=a.M},M'{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_AndL2) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) apply(subgoal_tac "∃x'::name. x'♯(x,y,u,v,P,M,M'{y:=c.P},M'{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_AndL2) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) done next case OrR1 then show ?case by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) next case OrR2 then show ?case by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) next case (OrL x1 M' x2 M'' x3) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(subgoal_tac "∃x'::name. x'♯(y,P,M,M{y:=c.P},M'{x:=a.M},M'{y:=c.P}{x:=a.M{y:=c.P}},
x1,x2,x3,M''{x:=a.M},M''{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_OrL) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) apply(subgoal_tac "∃x'::name. x'♯(x,y,P,M,M'{y:=c.P},M'{y:=c.P}{x:=a.M{y:=c.P}},
x1,x2,x3,M''{y:=c.P},M''{y:=c.P}{x:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_OrL) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) done next case ImpR then show ?case by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) next case (ImpL d M' x1 M'' x2) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(subgoal_tac "∃x'::name. x'♯(y,P,M,M{y:=c.P},M'{x2:=a.M},M'{y:=c.P}{x2:=a.M{y:=c.P}},
x1,x2,M''{x2:=a.M},M''{y:=c.P}{x2:=a.M{y:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_ImpL) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) apply(subgoal_tac "∃x'::name. x'♯(x,y,P,M,M'{x2:=c.P},M'{x2:=c.P}{x:=a.M{x2:=c.P}},
x1,x2,M''{x2:=c.P},M''{x2:=c.P}{x:=a.M{x2:=c.P}})") apply(erule exE, simp add: fresh_prod) apply(erule conjE)+ apply(simp add: fresh_fun_simp_ImpL) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule exists_fresh'(1)[OF fs_name1]) done qed
lemma subst_subst4: assumes a: "x♯(P,N,y)" "y♯(M,N)" "a♯(c,P,M)" "c♯(P,a)" "M≠Ax x c" shows "N{a:=(x).M}{c:=(y).P} = N{c:=(y).P}{a:=(x).(M{c:=(y).P})}" using a proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct) case (Cut d M' u M'') then show ?case apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh) apply(auto) apply(simp add: fresh_atm) apply(simp add: trm.inject) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply (metis forget(2) not_Ax1) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(rule sym) apply(rule trans) apply(rule better_Cut_substc) apply(simp add: fresh_prod subst_fresh fresh_atm) apply(simp add: abs_fresh subst_fresh) apply(auto) by (metis forget(2) not_Ax1) next case (NotR u M' d) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: abs_fresh subst_fresh) apply(simp add: abs_fresh subst_fresh) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) done next case (AndR d M e M' f) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: abs_fresh subst_fresh) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) done next case (OrR1 d M' e) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: abs_fresh subst_fresh) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) done next case (OrR2 d M' e) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: abs_fresh subst_fresh) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) done next case (ImpR u d M' e) then show ?case apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: abs_fresh subst_fresh) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)+ done qed (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
end
Messung V0.5 in Prozent
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.324Angebot
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.