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 .P (x').NotL .M x') = Cut .P (x').NotL .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 .P (x').NotL .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 .P (x').NotL .M x')" by (fresh_guess) thenshow"∃b. b ♯ (λx'. Cut .P (x').NotL .M x', Cut .P (b).NotL .M b)" by (metis abs_fresh(1) abs_fresh(5) fresh_prod n trm.fresh(3)) show"x' ♯ (λx'. Cut .P (x').NotL .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:=.N}) = (pi1∙M){(pi1∙x):=<(pi1∙c)>.(pi1∙N)}" and"pi2∙(M{x:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.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:=.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:=.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:=.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:=.P},P,name1,trm2{y:=.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:=.P},P,name1,trm2{name2:=.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:=.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:=.N} = ([(y,x)]∙M){y:=.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:=.N} = M{x:=.([(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,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,a)]∙N)},M'{x:=.([(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,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,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,a)]∙N)},M'{u:=.([(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:=.N} = ([(x',x)]∙M){x':=.([(c',c)]∙N)}" proof - have"M{x:=.N} = ([(x',x)]∙M){x':=.N}"using a by (simp add: substn_rename3) alsohave"… = ([(x',x)]∙M){x':=.([(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': assumes"a♯[c].P""y♯(N,x)""M≠Ax y a" shows"(Cut .M (x).N){y:=.P} = Cut .(M{y:=.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 .M (x).N = Cut .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 .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 .M y){y:=.P} = fresh_fun (λx'. Cut .P (x').NotL .M x')" proof (generate_fresh "coname") fix ca :: coname assume d: "ca ♯ (M, P, a, c, y)" thenhave"NotL .M y = NotL .([(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:=.P} = fresh_fun (λz'. Cut .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 .P (z').AndL1 (d).([(d, x)] ∙ M){x:=.P} (z')) = (λz'. Cut .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 .P (z').AndL1 d.([(d, x)] ∙ M){y:=.P} z') = (λz'. Cut .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:=.P} = fresh_fun (λz'. Cut .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 .P (z').AndL2 (d).([(d, x)] ∙ M){x:=.P} (z')) = (λz'. Cut .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 .P (z').AndL2 d.([(d, x)] ∙ M){y:=.P} z') = (λz'. Cut .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 .M .N c){c:=(z).P} = fresh_fun (λa'. Cut .(AndR .M .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 .M .N c = AndR .([(d,a)]∙M) .([(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:=.P} = fresh_fun (λz'. Cut .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 .M d){d:=(z).P} = fresh_fun (λa'. Cut .OrR1 .M a' (z).P)" proof (generate_fresh "coname") fix c :: coname assume c: "c ♯ (M, P, a, d, z)" thenhave"OrR1 .M d = OrR1 .([(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 .M d){d:=(z).P} = fresh_fun (λa'. Cut .OrR2 .M a' (z).P)" proof (generate_fresh "coname") fix c :: coname assume c: "c ♯ (M, P, a, d, z)" thenhave"OrR2 .M d = OrR2 .([(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)..M d){d:=(z).P} = fresh_fun (λa'. Cut .ImpR (x)..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)..M d = ImpR (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 .ImpR (c')..(([(c, a)] ∙ [(c', x)] ∙ M)){d:=(z).P} a' (z).P) = fresh_fun (λa'. Cut .ImpR (x)..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 .M (x).N y){y:=.P} = fresh_fun (λz'. Cut .P (z').ImpL .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 .M (x).N y = ImpL .([(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:=.P}[a⊨c>b] = M[a⊨c>b]{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 fresh_atm) by (meson crename_ax) next case (NotL coname trm name) obtain x'::name where"x'♯(trm{x:=.P},P,P[a⊨c>b],x,trm[a⊨c>b]{x:=.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:=.P},P,P[a⊨c>b],name1,trm[a⊨c>b]{x:=.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:=.P},P,P[a⊨c>b],name1,trm[a⊨c>b]{x:=.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:=.P},trm2{x:=.P},P,P[a⊨c>b],name1,name2, trm1[a⊨c>b]{x:=.P[a⊨c>b]},trm2[a⊨c>b]{x:=.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:=.P},trm2{x:=.P},P,P[a⊨c>b],name1,name2, trm1[a⊨c>b]{x:=.P[a⊨c>b]},trm2[a⊨c>b]{x:=.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:=.P}[y⊨n>z] = M[y⊨n>z]{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: 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:=.P},P,P[y⊨n>z],x,trm[y⊨n>z]{x:=.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:=.P},P,P[y⊨n>z],name1,trm[y⊨n>z]{x:=.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:=.P},P,P[y⊨n>z],name1,trm[y⊨n>z]{x:=.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:=.P},trm2{x:=.P},P,P[y⊨n>z],name1,name2,y,z, trm1[y⊨n>z]{x:=.P[y⊨n>z]},trm2[y⊨n>z]{x:=.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:=.P},trm2{x:=.P},P,P[y⊨n>z],name1,name2,y,z, trm1[y⊨n>z]{x:=.P[y⊨n>z]},trm2[y⊨n>z]{x:=.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:=.P}[a⊨c>b] = M[a⊨c>b]{x:=.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:=.P} = M{x:=.([(c',c)]∙P)}" using fs2 substn_rename4 by force have eq': "M[a⊨c>b]{x:=.P} = M[a⊨c>b]{x:=.([(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:=.P}[a⊨c>b] = M{x:=.([(c',c)]∙P)}[a⊨c>b]"using eq by simp alsohave"… = M[a⊨c>b]{x:=.(([(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)]∙P))}"using eq2 by simp alsohave"… = M[a⊨c>b]{x:=.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:=.P}[y⊨n>z] = M[y⊨n>z]{x:=.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:=.P} = ([(x',x)]∙M){x':=.P}" using fs2 by (simp add: substn_rename3) have eq': "([(x',x)]∙(M[y⊨n>z])){x':=.P} = M[y⊨n>z]{x:=.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:=.P}[y⊨n>z] = ([(x',x)]∙M){x':=.P}[y⊨n>z]"using eq by simp alsohave"… = ([(x',x)]∙M)[y⊨n>z]{x':=.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':=.P[y⊨n>z]}"using eq2 by simp alsohave"… = ([(x',x)]∙(M[y⊨n>z])){x':=.P}"using assms by (simp add: rename_fresh) alsohave"… = M[y⊨n>z]{x:=.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_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:=.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:=.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:=.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:=.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:=.P},trm2{y:=.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:=.P},trm2{name2:=.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:=.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:=.P} = Cut .P (x).(M{y:=.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:=.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:=.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:=.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:=.P},trm2[name3⊨n>y]{y:=.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:=.P},trm2[x⊨n>y]{y:=.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 .M .N c) c"
| [intro]: "b♯[a].M ==> fic (OrR1 .M b) b"
| [intro]: "b♯[a].M ==> fic (OrR2 .M b) b"
| [intro]: "[b♯[a].M]==> fic (ImpR (x)..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 .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 .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 .M .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)..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 .M (x).N) d ==> False" and"fic (NotL .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 .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:=.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:=.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:=.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:=.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:=.P},trm2{y:=.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:=.P},trm2{name2:=.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:=.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 .(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)
lemma better_CutL_intro[intro]: shows"M⟶🪙a M' ==> Cut .M (x).N ⟶🪙a Cut .M' (x).N" proof - assume red: "M⟶🪙a M'" obtain x'::"name"where fs1: "x'♯(M,N,x)"by (rule exists_fresh(1), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,a)"by (rule exists_fresh(2), rule fin_supp, blast) have"Cut .M (x).N = Cut .([(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) alsohave"…⟶🪙a Cut .([(a',a)]∙M') (x').([(x',x)]∙N)"using fs1 fs2 red by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt) alsohave"… = Cut .M' (x).N" using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_CutR_intro[intro]: shows"N⟶🪙a N' ==> Cut .M (x).N ⟶🪙a Cut .M (x).N'" proof - assume red: "N⟶🪙a N'" obtain x'::"name"where fs1: "x'♯(M,N,x)"by (rule exists_fresh(1), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,a)"by (rule exists_fresh(2), rule fin_supp, blast) have"Cut .M (x).N = Cut .([(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) alsohave"…⟶🪙a Cut .([(a',a)]∙M) (x').([(x',x)]∙N')"using fs1 fs2 red by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt) alsohave"… = Cut .M (x).N'" using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_AndRL_intro[intro]: shows"M⟶🪙a M' ==> AndR .M .N c ⟶🪙a AndR .M' .N c" proof - assume red: "M⟶🪙a M'" obtain b'::"coname"where fs1: "b'♯(M,N,a,b,c)"by (rule exists_fresh(2), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,a,b,c,b')"by (rule exists_fresh(2), rule fin_supp, blast) have"AndR .M .N c = AndR .([(a',a)]∙M) .([(b',b)]∙N) c" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a AndR .([(a',a)]∙M') .([(b',b)]∙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) alsohave"… = AndR .M' .N c" using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_AndRR_intro[intro]: shows"N⟶🪙a N' ==> AndR .M .N c ⟶🪙a AndR .M .N' c" proof - assume red: "N⟶🪙a N'" obtain b'::"coname"where fs1: "b'♯(M,N,a,b,c)"by (rule exists_fresh(2), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,a,b,c,b')"by (rule exists_fresh(2), rule fin_supp, blast) have"AndR .M .N c = AndR .([(a',a)]∙M) .([(b',b)]∙N) c" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a AndR .([(a',a)]∙M) .([(b',b)]∙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) alsohave"… = AndR .M .N' c" using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_AndL1_intro[intro]: shows"M⟶🪙a M' ==> AndL1 (x).M y ⟶🪙a AndL1 (x).M' y" proof - assume red: "M⟶🪙a M'" obtain x'::"name"where fs1: "x'♯(M,y,x)"by (rule exists_fresh(1), rule fin_supp, blast) have"AndL1 (x).M y = AndL1 (x').([(x',x)]∙M) y" using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a AndL1 (x').([(x',x)]∙M') y"using fs1 red by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod) alsohave"… = AndL1 (x).M' y" using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_AndL2_intro[intro]: shows"M⟶🪙a M' ==> AndL2 (x).M y ⟶🪙a AndL2 (x).M' y" proof - assume red: "M⟶🪙a M'" obtain x'::"name"where fs1: "x'♯(M,y,x)"by (rule exists_fresh(1), rule fin_supp, blast) have"AndL2 (x).M y = AndL2 (x').([(x',x)]∙M) y" using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a AndL2 (x').([(x',x)]∙M') y"using fs1 red by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod) alsohave"… = AndL2 (x).M' y" using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_OrLL_intro[intro]: shows"M⟶🪙a M' ==> OrL (x).M (y).N z ⟶🪙a OrL (x).M' (y).N z" proof - assume red: "M⟶🪙a M'" obtain x'::"name"where fs1: "x'♯(M,N,x,y,z)"by (rule exists_fresh(1), rule fin_supp, blast) obtain y'::"name"where fs2: "y'♯(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)]∙M) (y').([(y',y)]∙N) z" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a OrL (x').([(x',x)]∙M') (y').([(y',y)]∙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) alsohave"… = 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) finallyshow ?thesis by simp qed
lemma better_OrLR_intro[intro]: shows"N⟶🪙a N' ==> OrL (x).M (y).N z ⟶🪙a OrL (x).M (y).N' z" proof - assume red: "N⟶🪙a N'" obtain x'::"name"where fs1: "x'♯(M,N,x,y,z)"by (rule exists_fresh(1), rule fin_supp, blast) obtain y'::"name"where fs2: "y'♯(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)]∙M) (y').([(y',y)]∙N) z" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a OrL (x').([(x',x)]∙M) (y').([(y',y)]∙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) alsohave"… = 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) finallyshow ?thesis by simp qed
lemma better_OrR1_intro[intro]: shows"M⟶🪙a M' ==> OrR1 .M b ⟶🪙a OrR1 .M' b" proof - assume red: "M⟶🪙a M'" obtain a'::"coname"where fs1: "a'♯(M,b,a)"by (rule exists_fresh(2), rule fin_supp, blast) have"OrR1 .M b = OrR1 .([(a',a)]∙M) b" using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a OrR1 .([(a',a)]∙M') b"using fs1 red by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod) alsohave"… = OrR1 .M' b" using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_OrR2_intro[intro]: shows"M⟶🪙a M' ==> OrR2 .M b ⟶🪙a OrR2 .M' b" proof - assume red: "M⟶🪙a M'" obtain a'::"coname"where fs1: "a'♯(M,b,a)"by (rule exists_fresh(2), rule fin_supp, blast) have"OrR2 .M b = OrR2 .([(a',a)]∙M) b" using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a OrR2 .([(a',a)]∙M') b"using fs1 red by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod) alsohave"… = OrR2 .M' b" using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_ImpLL_intro[intro]: shows"M⟶🪙a M' ==> ImpL .M (x).N y ⟶🪙a ImpL .M' (x).N y" proof - assume red: "M⟶🪙a M'" obtain x'::"name"where fs1: "x'♯(M,N,x,y)"by (rule exists_fresh(1), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,a)"by (rule exists_fresh(2), rule fin_supp, blast) have"ImpL .M (x).N y = ImpL .([(a',a)]∙M) (x').([(x',x)]∙N) y" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a ImpL .([(a',a)]∙M') (x').([(x',x)]∙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) alsohave"… = ImpL .M' (x).N y" using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_ImpLR_intro[intro]: shows"N⟶🪙a N' ==> ImpL .M (x).N y ⟶🪙a ImpL .M (x).N' y" proof - assume red: "N⟶🪙a N'" obtain x'::"name"where fs1: "x'♯(M,N,x,y)"by (rule exists_fresh(1), rule fin_supp, blast) obtain a'::"coname"where fs2: "a'♯(M,N,a)"by (rule exists_fresh(2), rule fin_supp, blast) have"ImpL .M (x).N y = ImpL .([(a',a)]∙M) (x').([(x',x)]∙N) y" using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a ImpL .([(a',a)]∙M) (x').([(x',x)]∙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) alsohave"… = ImpL .M (x).N' y" using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
lemma better_ImpR_intro[intro]: shows"M⟶🪙a M' ==> ImpR (x)..M b ⟶🪙a ImpR (x)..M' b" proof - assume red: "M⟶🪙a M'" obtain a'::"coname"where fs2: "a'♯(M,a,b)"by (rule exists_fresh(2), rule fin_supp, blast) have"ImpR (x)..M b = ImpR (x)..([(a',a)]∙M) b" using fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm) alsohave"…⟶🪙a ImpR (x)..([(a',a)]∙M') b"using fs2 red by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod) alsohave"… = ImpR (x)..M' b" using fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu) finallyshow ?thesis by simp qed
text‹axioms do not reduce›
lemma ax_do_not_l_reduce: shows"Ax x a ⟶🪙l M ==> False" by (erule_tac l_redu.cases) (simp_all add: trm.inject)
lemma ax_do_not_c_reduce: shows"Ax x a ⟶🪙c M ==> False" by (erule_tac c_redu.cases) (simp_all add: trm.inject)
lemma ax_do_not_a_reduce: shows"Ax x a ⟶🪙a M ==> 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_redu_NotL_elim: assumes"NotL .M x ⟶🪙a R" shows"∃M'. R = NotL .M' x ∧ M⟶🪙aM'" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply (smt (verit, best) a_redu.eqvt(2) alpha(2) fresh_a_redu2)+ done
lemma a_redu_NotR_elim: assumes"NotR (x).M a ⟶🪙a R" shows"∃M'. R = NotR (x).M' a ∧ M⟶🪙aM'" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply (smt (verit, best) a_redu.eqvt(1) alpha(1) fresh_a_redu1)+ done
lemma a_redu_AndR_elim: assumes"AndR .M .N c⟶🪙a R" shows"(∃M'. R = AndR .M' .N c ∧ M⟶🪙aM') ∨ (∃N'. R = AndR .M .N' c ∧ N⟶🪙aN')" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply (smt (verit) a_redu.eqvt(2) alpha'(2) fresh_a_redu2) by (metis a_NotL a_redu_NotL_elim trm.inject(4))
lemma a_redu_AndL1_elim: assumes"AndL1 (x).M y ⟶🪙a R" shows"∃M'. R = AndL1 (x).M' y ∧ M⟶🪙aM'" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) by (metis a_NotR a_redu_NotR_elim trm.inject(3))
lemma a_redu_AndL2_elim: assumes a: "AndL2 (x).M y ⟶🪙a R" shows"∃M'. R = AndL2 (x).M' y ∧ M⟶🪙aM'" using a apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) by (metis a_NotR a_redu_NotR_elim trm.inject(3))
lemma a_redu_OrL_elim: assumes"OrL (x).M (y).N z⟶🪙a R" shows"(∃M'. R = OrL (x).M' (y).N z ∧ M⟶🪙aM') ∨ (∃N'. R = OrL (x).M (y).N' z ∧ N⟶🪙aN')" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply (metis a_NotR a_redu_NotR_elim trm.inject(3))+ done
lemma a_redu_OrR1_elim: assumes"OrR1 .M b ⟶🪙a R" shows"∃M'. R = OrR1 .M' b ∧ M⟶🪙aM'" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) by (metis a_NotL a_redu_NotL_elim trm.inject(4))
lemma a_redu_OrR2_elim: assumes a: "OrR2 .M b ⟶🪙a R" shows"∃M'. R = OrR2 .M' b ∧ M⟶🪙aM'" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) by (metis a_redu_OrR1_elim better_OrR1_intro trm.inject(8))
lemma a_redu_ImpL_elim: assumes a: "ImpL .M (y).N z⟶🪙a R" shows"(∃M'. R = ImpL .M' (y).N z ∧ M⟶🪙aM') ∨ (∃N'. R = ImpL .M (y).N' z ∧ N⟶🪙aN')" using assms apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply (smt (verit) a_redu.eqvt(2) alpha'(2) fresh_a_redu2) by (metis a_NotR a_redu_NotR_elim trm.inject(3))
lemma a_star_redu_NotL_elim: assumes"NotL .M x ⟶🪙a* R" shows"∃M'. R = NotL .M' x ∧ M ⟶🪙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 ⟶🪙a* R" shows"∃M'. R = NotR (x).M' a ∧ M ⟶🪙a* M'" using assms by (induct set: rtranclp) (use a_redu_NotR_elim in force)+
lemma a_star_redu_AndL1_elim: assumes"AndL1 (x).M y ⟶🪙a* R" shows"∃M'. R = AndL1 (x).M' y ∧ M ⟶🪙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 ⟶🪙a* R" shows"∃M'. R = AndL2 (x).M' y ∧ M ⟶🪙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 ⟶🪙a* R" shows"(∃M' N'. R = OrL (x).M' (y).N' z ∧ M ⟶🪙a* M' ∧ N ⟶🪙a* N')" using assms by (induct set: rtranclp) (use a_redu_OrL_elim in force)+
lemma a_star_redu_OrR1_elim: assumes"OrR1 .M y ⟶🪙a* R" shows"∃M'. R = OrR1 .M' y ∧ M ⟶🪙a* M'" using assms by (induct set: rtranclp) (use a_redu_OrR1_elim in force)+
lemma a_star_redu_OrR2_elim: assumes"OrR2 .M y ⟶🪙a* R" shows"∃M'. R = OrR2 .M' y ∧ M ⟶🪙a* M'" using assms by (induct set: rtranclp) (use a_redu_OrR2_elim in force)+
lemma a_star_redu_ImpR_elim: assumes"ImpR (x)..M y ⟶🪙a* R" shows"∃M'. R = ImpR (x)..M' y ∧ M ⟶🪙a* M'" using assms by (induct set: rtranclp) (use a_redu_ImpR_elim in force)+
lemma subst_not_fin1: shows"¬fin(M{x:=.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'♯(trm{x:=.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' ♯ (trm{x:=.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' ♯ (trm{x:=.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' ♯ (trm1{x:=.P},P,name1,trm2{x:=.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' ♯ (trm1{name2:=.P},P,name1,trm2{name2:=.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‹Reductions›
lemma fin_l_reduce: assumes"fin M x"and"M ⟶🪙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 ⟶🪙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 ⟶🪙a M'" shows"fin M' x" using assms proof (induct) case (1 x a) thenshow ?case using ax_do_not_a_reduce by auto next case (2 x M a) thenshow ?case using a_redu_NotL_elim fresh_a_redu1 by blast next case (3 y x M) thenshow ?case by (metis a_redu_AndL1_elim abs_fresh(1) fin.intros(3) fresh_a_redu1) next case (4 y x M) thenshow ?case by (metis a_redu_AndL2_elim abs_fresh(1) fin.intros(4) fresh_a_redu1) next case (5 z x M y N) thenshow ?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) thenshow ?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 ⟶🪙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 ⟶🪙l M'" shows"fic M' x" using b a byinduction (use fic_rest_elims in force)+
lemma fic_c_reduce: assumes a: "fic M x" and b: "M ⟶🪙c M'" shows"fic M' x" using b a byinduction (use fic_rest_elims in force)+
lemma fic_a_reduce: assumes a: "fic M x" and b: "M ⟶🪙a M'" shows"fic M' x" using assms proofinduction case (1 x a) thenshow ?case using ax_do_not_a_reduce by fastforce next case (2 a M x) thenshow ?case using a_redu_NotR_elim fresh_a_redu2 by blast next case (3 c a M b N) thenshow ?case by (smt (verit) a_redu_AndR_elim abs_fresh(2) fic.intros(3) fresh_a_redu2) next case (4 b a M) thenshow ?case by (metis a_redu_OrR1_elim abs_fresh(2) fic.intros(4) fresh_a_redu2) next case (5 b a M) thenshow ?case by (metis a_redu_OrR2_elim abs_fresh(2) fic.simps fresh_a_redu2) next case (6 b a M x) thenshow ?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 ⟶🪙a* M'" shows"fic M' x" using b a by (induct set: rtranclp) (auto simp: fic_a_reduce)
lemma subst_with_ax2: shows"M{b:=(x).Ax x a} ⟶🪙a* M[b⊨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} ⟶🪙a* (Ax z c)[b⊨c>a]" proof (cases "c=b") case True assume eq: "c=b" have"(Ax z c){b:=(x).Ax x a} = Cut .Ax z c (x).Ax x a"using eq by simp alsohave"…⟶🪙a* (Ax z c)[b⊨c>a]"using eq by blast finallyshow"(Ax z c){b:=(x).Ax x a} ⟶🪙a* (Ax z c)[b⊨c>a]"by simp next case False assume neq: "c≠b" thenshow"(Ax z c){b:=(x).Ax x a} ⟶🪙a* (Ax z c)[b⊨c>a]"by simp qed next case (Cut c M z N b a x) have fs: "c♯b""c♯a""c♯x""c♯N""z♯b""z♯a""z♯x""z♯M"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 show"(Cut .M (z).N){b:=(x).Ax x a} ⟶🪙a* (Cut .M (z).N)[b⊨c>a]" proof (cases "N = Ax z b") case True assume eq: "N = Ax z b" have"(Cut .M (z).N){b:=(x).Ax x a} = Cut .(M{b:=(x).Ax x a}) (x).Ax x a"using eq fs by simp alsohave"…⟶🪙a* Cut .(M[b⊨c>a]) (x).Ax x a"using ih1 a_star_congs by blast alsohave"… = Cut .(M[b⊨c>a]) (z).(N[b⊨c>a])"using eq fs by (simp add: trm.inject alpha calc_atm fresh_atm) finallyshow"(Cut .M (z).N){b:=(x).Ax x a} ⟶🪙a* (Cut .M (z).N)[b⊨c>a]"using fs by simp next case False assume neq: "N ≠ Ax z b" have"(Cut .M (z).N){b:=(x).Ax x a} = Cut .(M{b:=(x).Ax x a}) (z).(N{b:=(x).Ax x a})" using fs neq by simp alsohave"…⟶🪙a* Cut .(M[b⊨c>a]) (z).(N[b⊨c>a])"using ih1 ih2 a_star_congs by blast finallyshow"(Cut .M (z).N){b:=(x).Ax x a} ⟶🪙a* (Cut .M (z).N)[b⊨c>a]"using fs by simp qed next case (NotR z M c b a x) have fs: "z♯b""z♯a""z♯x""z♯c"by fact+ have ih: "M{b:=(x).Ax x a} ⟶🪙a* M[b⊨c>a]"by fact show"(NotR (z).M c){b:=(x).Ax x a} ⟶🪙a* (NotR (z).M c)[b⊨c>a]" proof (cases "c=b") case True assume eq: "c=b" obtain a'::"coname"where new: "a'♯(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 (λa'. Cut .NotR (z).M{b:=(x).Ax x a} a' (x).Ax x a)" using eq fs by simp alsohave"… = Cut .NotR (z).M{b:=(x).Ax x a} a' (x).Ax x a" using new by (simp add: fresh_fun_simp_NotR fresh_prod) alsohave"…⟶🪙a* (NotR (z).(M{b:=(x).Ax x a}) a')[a'⊨c>a]" using new by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) auto alsohave"… = NotR (z).(M{b:=(x).Ax x a}) a"using new by (simp add: crename_fresh) alsohave"…⟶🪙a* NotR (z).(M[b⊨c>a]) a"using ih by (auto intro: a_star_congs) alsohave"… = (NotR (z).M c)[b⊨c>a]"using eq by simp finallyshow"(NotR (z).M c){b:=(x).Ax x a} ⟶🪙a* (NotR (z).M c)[b⊨c>a]"by simp next case False assume neq: "c≠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 alsohave"…⟶🪙a* NotR (z).(M[b⊨c>a]) c"using ih by (auto intro: a_star_congs) finallyshow"(NotR (z).M c){b:=(x).Ax x a} ⟶🪙a* (NotR (z).M c)[b⊨c>a]"using neq bysimp qed next case (NotL c M z b a x) have fs: "c♯b""c♯a""c♯x""c♯z"by fact+ have ih: "M{b:=(x).Ax x a} ⟶🪙a* M[b⊨c>a]"by fact have"(NotL .M z){b:=(x).Ax x a} = NotL .(M{b:=(x).Ax x a}) z"using fs by simp alsohave"…⟶🪙a* NotL .(M[b⊨c>a]) z"using ih by (auto intro: a_star_congs) finallyshow"(NotL .M z){b:=(x).Ax x a} ⟶🪙a* (NotL .M z)[b⊨c>a]"using fs by simp next case (AndR c M d N e b a x) have fs: "c♯b""c♯a""c♯x""d♯b""d♯a""d♯x""d≠c""c♯N""c♯e""d♯M""d♯e"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 show"(AndR .M .N e){b:=(x).Ax x a} ⟶🪙a* (AndR .M .N e)[b⊨c>a]" proof(cases "e=b") case True assume eq: "e=b" obtain e'::"coname"where new: "e'♯(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 .M .N e){b:=(x).Ax x a} = fresh_fun (λe'. Cut .AndR .(M{b:=(x).Ax x a}) .(N{b:=(x).Ax x a}) e' (x).Ax x a)" using eq fs by simp alsohave"… = Cut .AndR .(M{b:=(x).Ax x a}) .(N{b:=(x).Ax x a}) e' (x).Ax x a" using new by (simp add: fresh_fun_simp_AndR fresh_prod) alsohave"…⟶🪙a* (AndR .(M{b:=(x).Ax x a}) .(N{b:=(x).Ax x a}) e')[e'⊨c>a]" using new by (intro a_starI a_redu.intros better_LAxR_intro fic.intros) (simp_all add: abs_fresh) alsohave"… = AndR .(M{b:=(x).Ax x a}) .(N{b:=(x).Ax x a}) a"using fs new by (auto simp: fresh_prod fresh_atm subst_fresh crename_fresh) alsohave"…⟶🪙a* AndR .(M[b⊨c>a]) .(N[b⊨c>a]) a"using ih1 ih2 by (auto intro: a_star_congs) alsohave"… = (AndR .M .N e)[b⊨c>a]"using eq fs by simp finallyshow"(AndR .M .N e){b:=(x).Ax x a} ⟶🪙a* (AndR .M .N e)[b⊨c>a]"by simp next case False assume neq: "e≠b" have"(AndR .M .N e){b:=(x).Ax x a} = AndR .(M{b:=(x).Ax x a}) .(N{b:=(x).Ax x a}) e" using fs neq by simp alsohave"…⟶🪙a* AndR .(M[b⊨c>a]) .(N[b⊨c>a]) e"using ih1 ih2 by (auto intro: a_star_congs) finallyshow"(AndR .M .N e){b:=(x).Ax x a} ⟶🪙a* (AndR .M .N e)[b⊨c>a]" using fs neq by simp qed next case (AndL1 u M v b a x) have fs: "u♯b""u♯a""u♯x""u♯v"by fact+ have ih: "M{b:=(x).Ax x a} ⟶🪙a* M[b⊨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 alsohave"…⟶🪙a* AndL1 (u).(M[b⊨c>a]) v"using ih by (auto intro: a_star_congs) finallyshow"(AndL1 (u).M v){b:=(x).Ax x a} ⟶🪙a* (AndL1 (u).M v)[b⊨c>a]"using fs by simp next case (AndL2 u M v b a x) have fs: "u♯b""u♯a""u♯x""u♯v"by fact+ have ih: "M{b:=(x).Ax x a} ⟶🪙a* M[b⊨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 alsohave"…⟶🪙a* AndL2 (u).(M[b⊨c>a]) v"using ih by (auto intro: a_star_congs) finallyshow"(AndL2 (u).M v){b:=(x).Ax x a} ⟶🪙a* (AndL2 (u).M v)[b⊨c>a]"using fs by simp next case (OrR1 c M d b a x) have fs: "c♯b""c♯a""c♯x""c♯d"by fact+ have ih: "M{b:=(x).Ax x a} ⟶🪙a* M[b⊨c>a]"by fact show"(OrR1 .M d){b:=(x).Ax x a} ⟶🪙a* (OrR1 .M d)[b⊨c>a]" proof(cases "d=b") case True assume eq: "d=b" obtain a'::"coname"where new: "a'♯(Ax x a,M{b:=(x).Ax x a},c,x,a)" by (rule exists_fresh(2)[OF fs_coname1]) have"(OrR1 .M d){b:=(x).Ax x a} = fresh_fun (λa'. Cut .OrR1 .M{b:=(x).Ax x a} a' (x).Ax x a)"using fs eq by (simp) alsohave"… = Cut .OrR1 .M{b:=(x).Ax x a} a' (x).Ax x a" using new by (simp add: fresh_fun_simp_OrR1) alsohave"…⟶🪙a* (OrR1 .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) alsohave"… = OrR1 .M{b:=(x).Ax x a} a"using fs new by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh) alsohave"…⟶🪙a* OrR1 .(M[b⊨c>a]) a"using ih by (auto intro: a_star_congs) alsohave"… = (OrR1 .M d)[b⊨c>a]"using eq fs by simp finallyshow"(OrR1 .M d){b:=(x).Ax x a} ⟶🪙a* (OrR1 .M d)[b⊨c>a]"by simp next case False assume neq: "d≠b" have"(OrR1 .M d){b:=(x).Ax x a} = OrR1 .(M{b:=(x).Ax x a}) d"using fs neq by (simp) alsohave"…⟶🪙a* OrR1 .(M[b⊨c>a]) d"using ih by (auto intro: a_star_congs) finallyshow"(OrR1 .M d){b:=(x).Ax x a} ⟶🪙a* (OrR1 .M d)[b⊨c>a]"using fs neq by simp qed next case (OrR2 c M d b a x) have fs: "c♯b""c♯a""c♯x""c♯d"by fact+ have ih: "M{b:=(x).Ax x a} ⟶🪙a* M[b⊨c>a]"by fact show"(OrR2 .M d){b:=(x).Ax x a} ⟶🪙a* (OrR2 .M d)[b⊨c>a]" proof(cases "d=b") case True assume eq: "d=b" obtain a'::"coname"where new: "a'♯(Ax x a,M{b:=(x).Ax x a},c,x,a)" by (rule exists_fresh(2)[OF fs_coname1]) have"(OrR2 .M d){b:=(x).Ax x a} = fresh_fun (λa'. Cut .OrR2 .M{b:=(x).Ax x a} a' (x).Ax x a)"using fs eq by (simp) alsohave"… = Cut .OrR2 .M{b:=(x).Ax x a} a' (x).Ax x a" using new by (simp add: fresh_fun_simp_OrR2) alsohave"…⟶🪙a* (OrR2 .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) alsohave"… = OrR2 .M{b:=(x).Ax x a} a"using fs new by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh) alsohave"…⟶🪙a* OrR2 .(M[b⊨c>a]) a"using ih by (auto intro: a_star_congs) alsohave"… = (OrR2 .M d)[b⊨c>a]"using eq fs by simp finallyshow"(OrR2 .M d){b:=(x).Ax x a} ⟶🪙a* (OrR2 .M d)[b⊨c>a]"by simp next case False assume neq: "d≠b" have"(OrR2 .M d){b:=(x).Ax x a} = OrR2 .(M{b:=(x).Ax x a}) d"using fs neq by (simp) alsohave"…⟶🪙a* OrR2 .(M[b⊨c>a]) d"using ih by (auto intro: a_star_congs) finallyshow"(OrR2 .M d){b:=(x).Ax x a} ⟶🪙a* (OrR2 .M d)[b⊨c>a]"using fs neq by simp qed next case (OrL u M v N z b a x) have fs: "u♯b""u♯a""u♯x""v♯b""v♯a""v♯x""v≠u""u♯N""u♯z""v♯M""v♯z"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"(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 alsohave"…⟶🪙a* OrL (u).(M[b⊨c>a]) (v).(N[b⊨c>a]) z"using ih1 ih2 by (auto intro: a_star_congs) finallyshow"(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)..M d){b:=(x).Ax x a} ⟶🪙a* (ImpR (z)..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)..M d){b:=(x).Ax x a} = fresh_fun (λa'. Cut .ImpR z..M{b:=(x).Ax x a} a' (x).Ax x a)"using fs eq by simp alsohave"… = Cut .ImpR z..M{b:=(x).Ax x a} a' (x).Ax x a" using new by (simp add: fresh_fun_simp_ImpR) alsohave"…⟶🪙a* (ImpR z..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) alsohave"… = ImpR z..M{b:=(x).Ax x a} a"using fs new by (auto simp: fresh_prod crename_fresh subst_fresh fresh_atm) alsohave"…⟶🪙a* ImpR z..(M[b⊨c>a]) a"using ih by (auto intro: a_star_congs) alsohave"… = (ImpR z..M b)[b⊨c>a]"using eq fs by simp finallyshow"(ImpR (z)..M d){b:=(x).Ax x a} ⟶🪙a* (ImpR (z)..M d)[b⊨c>a]"using eq by simp next case False assume neq: "b≠d" have"(ImpR (z)..M d){b:=(x).Ax x a} = ImpR (z)..(M{b:=(x).Ax x a}) d"using fs neq by simp alsohave"…⟶🪙a* ImpR (z)..(M[b⊨c>a]) d"using ih by (auto intro: a_star_congs) finallyshow"(ImpR (z)..M d){b:=(x).Ax x a} ⟶🪙a* (ImpR (z)..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 .M (u).N v){b:=(x).Ax x a} = ImpL .(M{b:=(x).Ax x a}) (u).(N{b:=(x).Ax x a}) v" using fs by simp alsohave"…⟶🪙a* ImpL .(M[b⊨c>a]) (u).(N[b⊨c>a]) v" using ih1 ih2 by (auto intro: a_star_congs) finallyshow"(ImpL .M (u).N v){b:=(x).Ax x a} ⟶🪙a* (ImpL .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) thenshow ?case by (metis fin.intros(1) fin_rest_elims(2) subst_not_fin2) next case (AndR coname1 trm1 coname2 trm2 coname3) thenshow ?case by (metis fin.intros(1) fin_rest_elims(3) subst_not_fin2) next case (OrR1 coname1 trm coname2) thenshow ?case by (metis fin.intros(1) fin_rest_elims(4) subst_not_fin2) next case (OrR2 coname1 trm coname2) thenshow ?case by (metis fin.intros(1) fin_rest_elims(5) subst_not_fin2) next case (ImpR name coname1 trm coname2) thenshow ?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:=.Q} ≠ Ax y a" proof (nominal_induct M avoiding: b y Q x a rule: trm.strong_induct) case (NotL coname trm name) thenshow ?case by (metis fic.intros(1) fic_rest_elims(2) not_fic_subst1) next case (AndL1 name1 trm name2) thenshow ?case by (metis fic.intros(1) fic_rest_elims(4) not_fic_subst1) next case (AndL2 name1 trm name2) thenshow ?case by (metis fic.intros(1) fic_rest_elims(5) not_fic_subst1) next case (OrL name1 trm1 name2 trm2 name3) thenshow ?case by (metis fic.intros(1) fic_rest_elims(3) not_fic_subst1) next case (ImpL coname trm1 name1 trm2 name2) thenshow ?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:=.P}{x:=.P} = N{x:=.Ax y c}{y:=.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:=.P},M{x:=.Ax y c}{y:=.P},y,x)" and"x''♯ (P,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.P},Ax y c,y,x)" by (meson exists_fresh(1) fs_name1) thenshow ?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:=.P},M{x:=.Ax y c}{y:=.P},u,y,x)" and"x''♯ (P,Ax y c,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.P},u,y,x)" by (meson exists_fresh(1) fs_name1) thenshow ?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:=.P},M{x:=.Ax y c}{y:=.P},u,y,x)" and"x''♯ (P,Ax y c,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.P},u,y,x)" by (meson exists_fresh(1) fs_name1) thenshow ?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:=.P},M{x:=.Ax y c}{y:=.P}, M'{y:=.P},M'{x:=.Ax y c}{y:=.P},x1,x2,x3,y,x)" and"x''♯ (P,Ax y c,M{x:=.Ax y c},M{x:=.Ax y c}{y:=.P}, M'{x:=.Ax y c},M'{x:=.Ax y c}{y:=.P},x1,x2,x3,y,x)" by (meson exists_fresh(1) fs_name1) thenshow ?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:=.P},M{x:=.Ax x2 c}{x2:=.P}, M'{x2:=.P},M'{x:=.Ax x2 c}{x2:=.P},x1,y,x)" and"x''♯ (P,Ax y c,M{x2:=.Ax y c},M{x2:=.Ax y c}{y:=.P}, M'{x2:=.Ax y c},M'{x2:=.Ax y c}{y:=.P},x1,x2,y,x)" by (meson exists_fresh(1) fs_name1) thenshow ?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:=.P}{x:=.P} = N{x:=.Ax y a}{y:=.P}" proof - show ?thesis proof (cases "c=a") case True with assms show ?thesis by (simp add: interesting_subst1) next case False thenhave"N{x:=.Ax y a} = N{x:=.([(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 thenshow ?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 thenshow ?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) thenshow ?case by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh) next case (AndL2 u M d) thenshow ?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) thenshow ?case by(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh) next case ImpL thenshow ?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 thenshow ?thesis using assms by (simp add: interesting_subst2) next case False thenhave"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:=.P}{b:=(y).Q} = M{b:=(y).Q}{x:=.(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) thenshow ?case by (auto simp add: abs_fresh fresh_prod fresh_atm subst_fresh trm.inject forget) next case (Cut c M z N) thenshow ?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) thenshow ?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:=.P},P{b:=(y).Q},M{b:=(y).Q}{x:=.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) thenshow ?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:=.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=.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:=.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=.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:=.P},M{b:=(y).Q}{x:=.P{b:=(y).Q}},z2,z3,a,y,Q, P{b:=(y).Q},N{x:=.P},N{b:=(y).Q}{x:=.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) thenshow ?case by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR1) next case (OrR2 c1 M c2) thenshow ?case by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR2) next case (ImpR z c M d) thenshow ?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:=.P},N{u:=.P},y,Q, M{b:=(y).Q}{u:=.P{b:=(y).Q}},N{b:=(y).Q}{u:=.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:=.P} = M{y:=.P}{a:=(x).N{y:=.P}}" using a proof(nominal_induct M avoiding: a x N y b P rule: trm.strong_induct) case (Ax z c) thenshow ?case by (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) next case (Cut d M' u M'') thenshow ?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:=.P},M'{d:=(x).N},M'{y:=.P}{d:=(x).N{y:=.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) done next case (NotL d M' z) obtain x'::name where"x' ♯ (z,y,P,N,N{y:=.P},M'{y:=.P},M'{y:=.P}{a:=(x).N{y:=.P}})" by (meson exists_fresh(1) fs_name1) with NotL show ?case apply(simp add: fresh_prod fresh_atm abs_fresh) apply(auto simp only: fresh_fun_simp_NotL) by (auto simp: subst_fresh abs_fresh fresh_atm forget) next case (AndR d M' e M'' f) obtain a'::coname where"a' ♯ (P,b,d,e,N,N{y:=.P},M'{f:=(x).N},M''{f:=(x).N}, M'{y:=.P}{f:=(x).N{y:=.P}},M''{y:=.P}{f:=(x).N{y:=.P}})" 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:=.P},M'{f:=(x).N},M''{f:=(x).N}, M'{y:=.P}{f:=(x).N{y:=.P}},M''{y:=.P}{f:=(x).N{y:=.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:=.P},M'{y:=.P}{a:=(x).N{y:=.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:=.P},M'{y:=.P}{a:=(x).N{y:=.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:=.P},M'{y:=.P},M''{y:=.P}, M'{y:=.P}{a:=(x).N{y:=.P}},M''{y:=.P}{a:=(x).N{y:=.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:=.P}, M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.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:=.P}, M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.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:=.P}, M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.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:=.P},M'{w:=.P},M''{w:=.P}, M'{w:=.P}{a:=(x).N{w:=.P}},M''{w:=.P}{a:=(x).N{w:=.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
¤ 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.0.306Bemerkung:
(vorverarbeitet am 2026-04-28)
¤
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.