Quelle Class1.thy Sprache: Isabelle

theory Class1
imports "HOL-Nominal.Nominal"
begin

section \<open>Term-Calculus from Urban's PhD\<close>

atom_decl name coname

text \<open>types\<close>

unbundle no bit_operations_syntax

nominal_datatype ty =
 PR "string"
 | NOT "ty"
 | AND "ty" "ty" (\<open>_ AND _\<close> [100,100] 100)
 | OR "ty" "ty" (\<open>_ OR _\<close> [100,100] 100)
 | IMP "ty" "ty" (\<open>_ IMP _\<close> [100,100] 100)

instantiation ty :: size
begin

nominal_primrec size_ty
where
 "size (PR s) = (1::nat)"
| "size (NOT T) = 1 + size T"
| "size (T1 AND T2) = 1 + size T1 + size T2"
| "size (T1 OR T2) = 1 + size T1 + size T2"
| "size (T1 IMP T2) = 1 + size T1 + size T2"
by (rule TrueI)+

instance ..

end

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)

text \<open>terms\<close>

nominal_datatype trm =
 Ax "name" "coname"
 | Cut "\coname\trm" "\name\trm" (\Cut <_>._ ('(_'))._\ [0,0,0,100] 101)
 | NotR "\name\trm" "coname" (\NotR ('(_'))._ _\ [0,100,100] 101)
 | NotL "\coname\trm" "name" (\NotL <_>._ _\ [0,100,100] 101)
 | AndR "\coname\trm" "\coname\trm" "coname" (\AndR <_>._ <_>._ _\ [0,100,0,100,100] 101)
 | AndL1 "\name\trm" "name" (\AndL1 (_)._ _\ [100,100,100] 101)
 | AndL2 "\name\trm" "name" (\AndL2 (_)._ _\ [100,100,100] 101)
 | OrR1 "\coname\trm" "coname" (\OrR1 <_>._ _\ [100,100,100] 101)
 | OrR2 "\coname\trm" "coname" (\OrR2 <_>._ _\ [100,100,100] 101)
 | OrL "\name\trm" "\name\trm" "name" (\OrL (_)._ (_)._ _\ [100,100,100,100,100] 101)
 | ImpR "\name\(\coname\trm)" "coname" (\ImpR (_).<_>._ _\ [100,100,100,100] 101)
 | ImpL "\coname\trm" "\name\trm" "name" (\ImpL <_>._ (_)._ _\ [100,100,100,100,100] 101)

text \<open>named terms\<close>

nominal_datatype ntrm = Na "\name\trm" (\((_):_)\ [100,100] 100)

text \<open>conamed terms\<close>

nominal_datatype ctrm = Co "\coname\trm" (\(<_>:_)\ [100,100] 100)

text \<open>renaming functions\<close>

nominal_primrec (freshness_context: "(d::coname,e::coname)")
 crename :: "trm \ coname \ coname \ trm" (\_[_\c>_]\ [100,0,0] 100)
where
 "(Ax x a)[d\c>e] = (if a=d then Ax x e else Ax x a)"
| "\a\(d,e,N);x\M\ \ (Cut .M (x).N)[d\c>e] = Cut .(M[d\c>e]) (x).(N[d\c>e])"
| "(NotR (x).M a)[d\c>e] = (if a=d then NotR (x).(M[d\c>e]) e else NotR (x).(M[d\c>e]) a)"
| "a\(d,e) \ (NotL .M x)[d\c>e] = (NotL .(M[d\c>e]) x)"
| "\a\(d,e,N,c);b\(d,e,M,c);b\a\ \ (AndR .M .N c)[d\c>e] =
 (if c=d then AndR <a>.(M[d\<turnstile>c>e]) .(N[d \<turnstile>c>e]) e else AndR <a>.(M[d\<turnstile>c>e]) .(N[d\<turnstile>c>e]) c)"
| "x\y \ (AndL1 (x).M y)[d\c>e] = AndL1 (x).(M[d\c>e]) y"
| "x\y \ (AndL2 (x).M y)[d\c>e] = AndL2 (x).(M[d\c>e]) y"
| "a\(d,e,b) \ (OrR1 .M b)[d\c>e] = (if b=d then OrR1 .(M[d\c>e]) e else OrR1 .(M[d\c>e]) b)"
| "a\(d,e,b) \ (OrR2 .M b)[d\c>e] = (if b=d then OrR2 .(M[d\c>e]) e else OrR2 .(M[d\c>e]) b)"
| "\x\(N,z);y\(M,z);y\x\ \ (OrL (x).M (y).N z)[d\c>e] = OrL (x).(M[d\c>e]) (y).(N[d\c>e]) z"
| "a\(d,e,b) \ (ImpR (x)..M b)[d\c>e] =
 (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
| "\a\(d,e,N);x\(M,y)\ \ (ImpL .M (x).N y)[d\c>e] = ImpL .(M[d\c>e]) (x).(N[d\c>e]) y"
 by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+

nominal_primrec (freshness_context: "(u::name,v::name)")
 nrename :: "trm \ name \ name \ trm" (\_[_\n>_]\ [100,0,0] 100)
where
 "(Ax x a)[u\n>v] = (if x=u then Ax v a else Ax x a)"
| "\a\N;x\(u,v,M)\ \ (Cut .M (x).N)[u\n>v] = Cut .(M[u\n>v]) (x).(N[u\n>v])"
| "x\(u,v) \ (NotR (x).M a)[u\n>v] = NotR (x).(M[u\n>v]) a"
| "(NotL .M x)[u\n>v] = (if x=u then NotL .(M[u\n>v]) v else NotL .(M[u\n>v]) x)"
| "\a\(N,c);b\(M,c);b\a\ \ (AndR .M .N c)[u\n>v] = AndR .(M[u\n>v]) .(N[u\n>v]) c"
| "x\(u,v,y) \ (AndL1 (x).M y)[u\n>v] = (if y=u then AndL1 (x).(M[u\n>v]) v else AndL1 (x).(M[u\n>v]) y)"
| "x\(u,v,y) \ (AndL2 (x).M y)[u\n>v] = (if y=u then AndL2 (x).(M[u\n>v]) v else AndL2 (x).(M[u\n>v]) y)"
| "a\b \ (OrR1 .M b)[u\n>v] = OrR1 .(M[u\n>v]) b"
| "a\b \ (OrR2 .M b)[u\n>v] = OrR2 .(M[u\n>v]) b"
| "\x\(u,v,N,z);y\(u,v,M,z);y\x\ \ (OrL (x).M (y).N z)[u\n>v] =
 (if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)"
| "\a\b; x\(u,v)\ \ (ImpR (x)..M b)[u\n>v] = ImpR (x)..(M[u\n>v]) b"
| "\a\N;x\(u,v,M,y)\ \ (ImpL .M (x).N y)[u\n>v] =
 (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
 by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+

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)

lemmas rename_fresh = nrename_fresh crename_fresh
 nrename_nfresh crename_nfresh crename_cfresh nrename_cfresh
 nrename_nfresh' crename_cfresh'
 nrename_rename crename_rename

lemma better_nrename_Cut:
 assumes a: "x\(u,v)"
 shows "(Cut .M (x).N)[u\n>v] = Cut .(M[u\n>v]) (x).(N[u\n>v])"
proof -
 obtain x'::"name" where fs1: "x'\<sharp>(M,N,a,x,u,v)" by (rule exists_fresh(1), rule fin_supp, blast)
 obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,x,u,v)" by (rule exists_fresh(2), rule fin_supp, blast)
 have eq1: "(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)
 have "(Cut .([(a',a)]\M) (x').([(x',x)]\N))[u\n>v] =
 Cut <a'>.(([(a',a)]\<bullet>M)[u\<turnstile>n>v]) (x').(([(x',x)]\<bullet>N)[u\<turnstile>n>v])"
 using fs1 fs2
 by (intro nrename.simps; simp add: fresh_left calc_atm)
 also have "\ = Cut .(M[u\n>v]) (x).(N[u\n>v])" using fs1 fs2 a
 by(simp add: trm.inject alpha fresh_prod rename_eqvts calc_atm rename_fresh fresh_atm)
 finally show "(Cut .M (x).N)[u\n>v] = Cut .(M[u\n>v]) (x).(N[u\n>v])" using eq1
 by simp
qed

lemma better_crename_Cut:
 assumes a: "a\(b,c)"
 shows "(Cut .M (x).N)[b\c>c] = Cut .(M[b\c>c]) (x).(N[b\c>c])"
proof -
 obtain x'::"name" where fs1: "x'\<sharp>(M,N,a,x,b,c)" by (rule exists_fresh(1), rule fin_supp, blast)
 obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,x,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
 have eq1: "(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)
 have "(Cut .([(a',a)]\M) (x').([(x',x)]\N))[b\c>c] =
 Cut <a'>.(([(a',a)]\<bullet>M)[b\<turnstile>c>c]) (x').(([(x',x)]\<bullet>N)[b\<turnstile>c>c])"
 using fs1 fs2
 by (intro crename.simps; simp add: fresh_left calc_atm)
 also have "\ = Cut .(M[b\c>c]) (x).(N[b\c>c])" using fs1 fs2 a
 by(simp add: trm.inject alpha calc_atm rename_fresh fresh_atm fresh_prod rename_eqvts)
 finally show "(Cut .M (x).N)[b\c>c] = Cut .(M[b\c>c]) (x).(N[b\c>c])" using eq1
 by simp
qed

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 \<open>substitution functions\<close>

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)
 then show "\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 fresh_fun_NotL[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\x'. Cut .P (x').NotL .M x')=
 fresh_fun (pi1\<bullet>(\<lambda>x'. Cut <c>.P (x').NotL <a>.M x'))"
 and "pi2\fresh_fun (\x'. Cut .P (x').NotL .M x')=
 fresh_fun (pi2\<bullet>(\<lambda>x'. Cut <c>.P (x').NotL <a>.M x'))"
 apply(perm_simp)
 apply(generate_fresh "name")
 apply(auto simp: fresh_prod fresh_fun_simp_NotL)
 apply (metis fresh_bij(1) fresh_fun_simp_NotL name_prm_coname_def)
 apply(perm_simp)
 apply(subgoal_tac "\n::name. n\(P,M,pi2\P,pi2\M,pi2)")
 apply (metis fresh_fun_simp_NotL fresh_prodD swap_simps(8) trm.perm(14) trm.perm(16))
 by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_AndL1:
 assumes a: "z'\P" "z'\M" "z'\x"
 shows "fresh_fun (\z'. Cut .P(z').AndL1 (x).M z') = Cut .P (z').AndL1 (x).M z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
 obtain n::name where "n\(c,P,x,M)"
 by (meson exists_fresh(1) fs_name1)
 then show "\a. a \ (\z'. Cut .P(z').AndL1 x. M z', Cut .P(a).AndL1 x. M a)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
next
 show "z' \ (\z'. Cut .P(z').AndL1 x. M z')"
 using a by(fresh_guess)
qed finite_guess

lemma fresh_fun_AndL1[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\z'. Cut .P (z').AndL1 (x).M z')=
 fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z'))"
 and "pi2\fresh_fun (\z'. Cut .P (z').AndL1 (x).M z')=
 fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z'))"
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,x,pi1\P,pi1\M,pi1\x,pi1)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL1 at_prm_fresh[OF at_name_inst] swap_simps)
 apply (meson exists_fresh(1) fs_name1)
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,x,pi2\P,pi2\M,pi2\x,pi2)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL1 calc_atm)
 by (meson exists_fresh'(1) fs_name1)

lemma fresh_fun_simp_AndL2:
 assumes a: "z'\P" "z'\M" "z'\x"
 shows "fresh_fun (\z'. Cut .P (z').AndL2 (x).M z') = Cut .P (z').AndL2 (x).M z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
 obtain n::name where "n\(c,P,x,M)"
 by (meson exists_fresh(1) fs_name1)
 then show "\a. a \ (\z'. Cut .P(z').AndL2 x. M z', Cut .P(a).AndL2 x. M a)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
next
 show "z' \ (\z'. Cut .P(z').AndL2 x. M z')"
 using a by(fresh_guess)
qed finite_guess

lemma fresh_fun_AndL2[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\z'. Cut .P (z').AndL2 (x).M z')=
 fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z'))"
 and "pi2\fresh_fun (\z'. Cut .P (z').AndL2 (x).M z')=
 fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z'))"
 apply(perm_simp)
 apply(subgoal_tac "\n::name. n\(P,M,x,pi1\P,pi1\M,pi1\x,pi1)")
 apply(force simp add: fresh_prod fresh_fun_simp_AndL2 at_prm_fresh[OF at_name_inst] swap_simps)
 apply (meson exists_fresh(1) fs_name1)
 apply(perm_simp)
 apply(subgoal_tac "\n::name. n\(P,M,x,pi2\P,pi2\M,pi2\x,pi2)")
 apply(force simp add: fresh_prod fresh_fun_simp_AndL2 calc_atm)
 by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_OrL:
 assumes a: "z'\P" "z'\M" "z'\N" "z'\u" "z'\x"
 shows "fresh_fun (\z'. Cut .P(z').OrL(x).M(u).N z') = Cut .P (z').OrL (x).M (u).N z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
 obtain n::name where "n\(c,P,x,M,u,N)"
 by (meson exists_fresh(1) fs_name1)
 then show "\a. a \ (\z'. Cut .P(z').OrL(x).M(u).N(z'), Cut .P(a).OrL(x).M(u).N(a))"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
next
 show "z' \ (\z'. Cut .P(z').OrL(x).M(u).N(z'))"
 using a by(fresh_guess)
qed finite_guess

lemma fresh_fun_OrL[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\z'. Cut .P(z').OrL (x).M(u).N z')=
 fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').OrL(x).M (u).N z'))"
 and "pi2\fresh_fun (\z'. Cut .P(z').OrL (x).M(u).N z')=
 fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P(z').OrL(x).M(u).N z'))"
 apply(perm_simp)
 apply(subgoal_tac "\n::name. n\(P,M,N,x,u,pi1\P,pi1\M,pi1\N,pi1\x,pi1\u,pi1)")
 apply(force simp add: fresh_prod fresh_fun_simp_OrL at_prm_fresh[OF at_name_inst] swap_simps)
 apply (meson exists_fresh(1) fs_name1)
 apply(perm_simp)
 apply(subgoal_tac "\n::name. n\(P,M,N,x,u,pi2\P,pi2\M,pi2\N,pi2\x,pi2\u,pi2)")
 apply(force simp add: fresh_prod fresh_fun_simp_OrL calc_atm)
 by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_ImpL:
 assumes a: "z'\P" "z'\M" "z'\N" "z'\x"
 shows "fresh_fun (\z'. Cut .P (z').ImpL .M (x).N z') = Cut .P (z').ImpL .M (x).N z'"
proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
 obtain n::name where "n\(c,P,x,M,N)"
 by (meson exists_fresh(1) fs_name1)
 then show "\aa. aa \ (\z'. Cut .P(z').ImpL .M(x).N z', Cut .P(aa).ImpL .M(x).N aa)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
next
 show "z' \ (\z'. Cut .P(z').ImpL .M(x).N z')"
 using a by(fresh_guess)
qed finite_guess

lemma fresh_fun_ImpL[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\z'. Cut .P (z').ImpL .M (x).N z')=
 fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
 and "pi2\fresh_fun (\z'. Cut .P (z').ImpL .M (x).N z')=
 fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
 apply(perm_simp)
 apply(subgoal_tac "\n::name. n\(P,M,N,x,pi1\P,pi1\M,pi1\N,pi1\x,pi1)")
 apply(force simp add: fresh_prod fresh_fun_simp_ImpL at_prm_fresh[OF at_name_inst] swap_simps)
 apply (meson exists_fresh(1) fs_name1)
 apply(perm_simp)
 apply(subgoal_tac "\n::name. n\(P,M,N,x,pi2\P,pi2\M,pi2\N,pi2\x,pi2)")
 apply(force simp add: fresh_prod fresh_fun_simp_ImpL calc_atm)
 by (meson exists_fresh(1) fs_name1)

lemma fresh_fun_simp_NotR:
 assumes a: "a'\P" "a'\M"
 shows "fresh_fun (\a'. Cut .(NotR (y).M a') (x).P) = Cut .(NotR (y).M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
 obtain n::coname where "n\(x,P,y,M)"
 by (metis assms(1) assms(2) fresh_atm(4) fresh_prod)
 then show "\a. a \ (\a'. Cut .(NotR (y).M a') (x).P, Cut .NotR(y).M(a) (x).P)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
qed (use a in \<open>fresh_guess|finite_guess\<close>)+

lemma fresh_fun_NotR[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\a'. Cut .(NotR (y).M a') (x).P)=
 fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P))"
 and "pi2\fresh_fun (\a'. Cut .(NotR (y).M a') (x).P)=
 fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P))"
 apply(perm_simp)
 apply(subgoal_tac "\n::coname. n\(P,M,pi1\P,pi1\M,pi1)")
 apply(force simp add: fresh_prod fresh_fun_simp_NotR calc_atm)
 apply (meson exists_fresh(2) fs_coname1)
 apply(perm_simp)
 apply(subgoal_tac "\n::coname. n\(P,M,pi2\P,pi2\M,pi2)")
 apply(force simp: fresh_prod fresh_fun_simp_NotR at_prm_fresh[OF at_coname_inst] swap_simps)
 by (meson exists_fresh(2) fs_coname1)

lemma fresh_fun_simp_AndR:
 assumes a: "a'\P" "a'\M" "a'\N" "a'\b" "a'\c"
 shows "fresh_fun (\a'. Cut .(AndR .M .N a') (x).P) = Cut .(AndR .M .N a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
 obtain n::coname where "n\(x,P,b,M,c,N)"
 by (meson exists_fresh(2) fs_coname1)
 then show "\a. a \ (\a'. Cut .AndR .M .N(a') (x).P, Cut .AndR .M .N(a) (x).P)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
qed (use a in \<open>fresh_guess|finite_guess\<close>)+

lemma fresh_fun_AndR[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\a'. Cut .(AndR .M .N a') (x).P)=
 fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(AndR .M <c>.N a') (x).P))"
 and "pi2\fresh_fun (\a'. Cut .(AndR .M .N a') (x).P)=
 fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(AndR .M <c>.N a') (x).P))"
 apply(perm_simp)
 apply(subgoal_tac "\n::coname. n\(P,M,N,b,c,pi1\P,pi1\M,pi1\N,pi1\b,pi1\c,pi1)")
 apply(force simp add: fresh_prod fresh_fun_simp_AndR calc_atm)
 apply (meson exists_fresh(2) fs_coname1)
 apply(perm_simp)
 apply(subgoal_tac "\n::coname. n\(P,M,N,b,c,pi2\P,pi2\M,pi2\N,pi2\b,pi2\c,pi2)")
 apply(force simp add: fresh_prod fresh_fun_simp_AndR at_prm_fresh[OF at_coname_inst] swap_simps)
 by (meson exists_fresh(2) fs_coname1)

lemma fresh_fun_simp_OrR1:
 assumes a: "a'\P" "a'\M" "a'\b"
 shows "fresh_fun (\a'. Cut .(OrR1 .M a') (x).P) = Cut .(OrR1 .M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
 obtain n::coname where "n\(x,P,b,M)"
 by (meson exists_fresh(2) fs_coname1)
 then show "\a. a \ (\a'. Cut .OrR1 .M(a') (x).P, Cut .OrR1 .M(a) (x).P)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
qed (use a in \<open>fresh_guess|finite_guess\<close>)+

lemma fresh_fun_OrR1[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\a'. Cut .(OrR1 .M a') (x).P) =
 fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 .M a') (x).P))" (is "?t1")
 and "pi2\fresh_fun (\a'. Cut .(OrR1 .M a') (x).P) =
 fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 .M a') (x).P))" (is "?t2")
proof -
 obtain n::coname where "n\(P,M,b,pi1\P,pi1\M,pi1\b,pi1)"
 by (meson exists_fresh(2) fs_coname1)
 then show ?t1
 by perm_simp (force simp add: fresh_prod fresh_fun_simp_OrR1 calc_atm)
 obtain n::coname where "n\(P,M,b,pi2\P,pi2\M,pi2\b,pi2)"
 by (meson exists_fresh(2) fs_coname1)
 then show ?t2
 by perm_simp
 (force simp add: fresh_prod fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
qed

lemma fresh_fun_simp_OrR2:
 assumes "a'\P" "a'\M" "a'\b"
 shows "fresh_fun (\a'. Cut .(OrR2 .M a') (x).P) = Cut .(OrR2 .M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
 obtain n::coname where "n\(x,P,b,M)"
 by (meson exists_fresh(2) fs_coname1)
 then show "\a. a \ (\a'. Cut .OrR2 .M(a') (x).P, Cut .OrR2 .M(a) (x).P)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
qed (use assms in \<open>fresh_guess|finite_guess\<close>)+

lemma fresh_fun_OrR2[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\a'. Cut .(OrR2 .M a') (x).P) =
 fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 .M a') (x).P))" (is "?t1")
 and "pi2\fresh_fun (\a'. Cut .(OrR2 .M a') (x).P) =
 fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 .M a') (x).P))" (is "?t2")
proof -
 obtain n::coname where "n\(P,M,b,pi1\P,pi1\M,pi1\b,pi1)"
 by (meson exists_fresh(2) fs_coname1)
 then show ?t1
 by perm_simp (force simp add: fresh_prod fresh_fun_simp_OrR2 calc_atm)
 obtain n::coname where "n\(P,M,b,pi2\P,pi2\M,pi2\b,pi2)"
 by (meson exists_fresh(2) fs_coname1)
 then show ?t2
 by perm_simp
 (force simp add: fresh_prod fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
qed

lemma fresh_fun_simp_ImpR:
 assumes a: "a'\P" "a'\M" "a'\b"
 shows "fresh_fun (\a'. Cut .(ImpR (y)..M a') (x).P) = Cut .(ImpR (y)..M a') (x).P"
proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
 obtain n::coname where "n\(x,P,y,b,M)"
 by (meson exists_fresh(2) fs_coname1)
 then show "\a. a \ (\a'. Cut .(ImpR (y)..M a') (x).P, Cut .(ImpR (y)..M a) (x).P)"
 apply(intro exI [where x="n"])
 apply(simp add: fresh_prod abs_fresh)
 apply(fresh_guess)
 done
qed (use a in \<open>fresh_guess|finite_guess\<close>)+

lemma fresh_fun_ImpR[eqvt_force]:
 fixes pi1::"name prm"
 and pi2::"coname prm"
 shows "pi1\fresh_fun (\a'. Cut .(ImpR (y)..M a') (x).P) =
 fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y)..M a') (x).P))" (is "?t1")
 and "pi2\fresh_fun (\a'. Cut .(ImpR (y)..M a') (x).P)=
 fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y)..M a') (x).P))" (is "?t2")
proof -
 obtain n::coname where "n\(P,M,b,pi1\P,pi1\M,pi1\b,pi1)"
 by (meson exists_fresh(2) fs_coname1)
 then show ?t1
 by perm_simp (force simp add: fresh_prod fresh_fun_simp_ImpR calc_atm)
 obtain n::coname where "n\(P,M,b,pi2\P,pi2\M,pi2\b,pi2)"
 by (meson exists_fresh(2) fs_coname1)
 then show ?t2
 by perm_simp
 (force simp add: fresh_prod fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
qed

nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
 substn :: "trm \ name \ coname \ trm \ trm" (\_{_:=<_>._}\ [100,100,100,100] 100)
where
 "(Ax x a){y:=.P} = (if x=y then Cut .P (y).Ax y a else Ax x a)"
| "\a\(c,P,N);x\(y,P,M)\ \ (Cut .M (x).N){y:=.P} =
 (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
| "x\(y,P) \ (NotR (x).M a){y:=.P} = NotR (x).(M{y:=.P}) a"
| "a\(c,P) \ (NotL .M x){y:=.P} =
 (if x=y then fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x') else NotL <a>.(M{y:=<c>.P}) x)"
| "\a\(c,P,N,d);b\(c,P,M,d);b\a\ \
 (AndR <a>.M .N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) .(N{y:=<c>.P}) d"
| "x\(y,P,z) \ (AndL1 (x).M z){y:=.P} =
 (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z')
 else AndL1 (x).(M{y:=<c>.P}) z)"
| "x\(y,P,z) \ (AndL2 (x).M z){y:=.P} =
 (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z')
 else AndL2 (x).(M{y:=<c>.P}) z)"
| "a\(c,P,b) \ (OrR1 .M b){y:=.P} = OrR1 .(M{y:=.P}) b"
| "a\(c,P,b) \ (OrR2 .M b){y:=.P} = OrR2 .(M{y:=.P}) b"
| "\x\(y,N,P,z);u\(y,M,P,z);x\u\ \ (OrL (x).M (u).N z){y:=.P} =
 (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z')
 else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
| "\a\(b,c,P); x\(y,P)\ \ (ImpR (x)..M b){y:=.P} = ImpR (x)..(M{y:=.P}) b"
| "\a\(N,c,P);x\(y,P,M,z)\ \ (ImpL .M (x).N z){y:=.P} =
 (if y=z then fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z')
 else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
apply(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess | rule strip)+
apply(subgoal_tac "\x::name. x\(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_NotL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "\x::name. x\(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "\x::name. x\(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "\x::name. x\(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_OrL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "\x::name. x\(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_OrL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "\x::name. x\(x3,P,y1,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)

apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
apply(subgoal_tac "\x::name. x\(x3,P,y1,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply (meson exists_fresh(1) fs_name1)
apply(fresh_guess)+
done

nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
 substc :: "trm \ coname \ name \ trm \ trm" (\_{_:=('(_'))._}\ [100,0,0,100] 100)
where
 "(Ax x a){d:=(z).P} = (if d=a then Cut .(Ax x a) (z).P else Ax x a)"
| "\a\(d,P,N);x\(z,P,M)\ \ (Cut .M (x).N){d:=(z).P} =
 (if N=Ax x d then Cut <a>.(M{d:=(z).P}) (z).P else Cut <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}))"
| "x\(z,P) \ (NotR (x).M a){d:=(z).P} =
 (if d=a then fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(M{d:=(z).P}) a' (z).P) else NotR (x).(M{d:=(z).P}) a)"
| "a\(d,P) \ (NotL .M x){d:=(z).P} = NotL .(M{d:=(z).P}) x"
| "\a\(P,c,N,d);b\(P,c,M,d);b\a\ \ (AndR .M .N c){d:=(z).P} =
 (if d=c then fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(M{d:=(z).P}) .(N{d:=(z).P}) a') (z).P)
 else AndR <a>.(M{d:=(z).P}) .(N{d:=(z).P}) c)"
| "x\(y,z,P) \ (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
| "x\(y,P,z) \ (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
| "a\(d,P,b) \ (OrR1 .M b){d:=(z).P} =
 (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(M{d:=(z).P}) a' (z).P) else OrR1 <a>.(M{d:=(z).P}) b)"
| "a\(d,P,b) \ (OrR2 .M b){d:=(z).P} =
 (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(M{d:=(z).P}) a' (z).P) else OrR2 <a>.(M{d:=(z).P}) b)"
| "\x\(N,z,P,u);y\(M,z,P,u);x\y\ \ (OrL (x).M (y).N u){d:=(z).P} =
 OrL (x).(M{d:=(z).P}) (y).(N{d:=(z).P}) u"
| "\a\(b,d,P); x\(z,P)\ \ (ImpR (x)..M b){d:=(z).P} =
 (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(M{d:=(z).P}) a' (z).P)
 else ImpR (x).<a>.(M{d:=(z).P}) b)"
| "\a\(N,d,P);x\(y,z,P,M)\ \ (ImpL .M (x).N y){d:=(z).P} =
 ImpL <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}) y"
apply(finite_guess | simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "\x::coname. x\(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "\x::coname. x\(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "\x::coname. x\(x1,P,y1,x3,y2)")
apply(force simp add: fresh_prod fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "\x::coname. x\(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
apply(subgoal_tac "\x::coname. x\(x1,P,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp | rule strip)+
apply(subgoal_tac "\x::coname. x\(x1,P,x2,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpR abs_fresh fresh_atm abs_supp)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh abs_supp | rule strip)+
apply(subgoal_tac "\x::coname. x\(x1,P,x2,y1)")
apply(force simp add: fresh_prod fresh_fun_simp_ImpR abs_fresh fresh_atm)
apply(meson exists_fresh' fin_supp)

apply(simp add: abs_fresh | fresh_guess add: abs_fresh)+
done

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'\<sharp>(trm{y:=<c>.P},P)"
 by (meson exists_fresh(1) fs_name1)
 with NotL
 show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast)
next
 case (AndL1 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL1 show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast)
next
 case (AndL2 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL2 show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast)
next
 case (OrL name1 trm1 name2 trm2 name3)
 obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
 by (meson exists_fresh(1) fs_name1)
 with OrL show ?case
 by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast)
next
 case (ImpL coname trm1 name1 trm2 name2)
 obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
 by (meson exists_fresh(1) fs_name1)
 with ImpL show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast)
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

text \<open>Identical to the previous proof\<close>
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'\<sharp>(trm{y:=<c>.P},P)"
 by (meson exists_fresh(1) fs_name1)
 with NotL
 show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL; blast)
next
 case (AndL1 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL1 show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1 fresh_atm; blast)
next
 case (AndL2 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL2 show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2 fresh_atm; blast)
next
 case (OrL name1 trm1 name2 trm2 name3)
 obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
 by (meson exists_fresh(1) fs_name1)
 with OrL show ?case
 by (auto simp: fs_name1 fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL fresh_atm; blast)
next
 case (ImpL coname trm1 name1 trm2 name2)
 obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
 by (meson exists_fresh(1) fs_name1)
 with ImpL show ?case
 by (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL fresh_atm; blast)
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

lemma supp_subst3:
 shows "supp (M{c:=(x).P}) \ ((supp M) - {c}) \ (supp P)"
proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
 case (NotR name trm coname)
 obtain x'::coname where "x'\<sharp>(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'\<sharp>(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'\<sharp>(trm{y:=<c>.P},P)"
 by (meson exists_fresh(1) fs_name1)
 with NotL
 show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL)
 apply (auto simp: fresh_def)
 done
next
 case (AndL1 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL1 show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1)
 apply (auto simp: fresh_def)
 done
next
 case (AndL2 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL2 show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2)
 apply (auto simp: fresh_def)
 done
next
 case (OrL name1 trm1 name2 trm2 name3)
 obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
 by (meson exists_fresh(1) fs_name1)
 with OrL show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL)
 apply (fastforce simp: fresh_def)+
 done
next
 case (ImpL coname trm1 name1 trm2 name2)
 obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
 by (meson exists_fresh(1) fs_name1)
 with ImpL show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL)
 apply (fastforce simp: fresh_def)+
 done
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

lemma supp_subst6:
 shows "(supp M) \ ((supp (M{y:=.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'\<sharp>(trm{y:=<c>.P},P)"
 by (meson exists_fresh(1) fs_name1)
 with NotL
 show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_NotL)
 apply (auto simp: fresh_def)
 done
next
 case (AndL1 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL1 show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL1)
 apply (auto simp: fresh_def)
 done
next
 case (AndL2 name1 trm name2)
 obtain x'::name where "x'\<sharp>(trm{y:=<c>.P},P,name1)"
 by (meson exists_fresh(1) fs_name1)
 with AndL2 show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_AndL2)
 apply (auto simp: fresh_def)
 done
next
 case (OrL name1 trm1 name2 trm2 name3)
 obtain x'::name where "x'\<sharp>(trm1{y:=<c>.P},P,name1,trm2{y:=<c>.P},name2)"
 by (meson exists_fresh(1) fs_name1)
 with OrL show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_OrL)
 apply (fastforce simp: fresh_def)+
 done
next
 case (ImpL coname trm1 name1 trm2 name2)
 obtain x'::name where "x'\<sharp>(trm1{name2:=<c>.P},P,name1,trm2{name2:=<c>.P})"
 by (meson exists_fresh(1) fs_name1)
 with ImpL show ?case
 apply (auto simp: fresh_prod abs_supp supp_atm trm.supp fresh_fun_simp_ImpL)
 apply (fastforce simp: fresh_def)+
 done
qed (simp add: abs_supp supp_atm trm.supp fs_name1; blast)+

lemma supp_subst7:
 shows "(supp M - {c}) \ supp (M{c:=(x).P})"
proof (nominal_induct M avoiding: x P c rule: trm.strong_induct)
 case (NotR name trm coname)
 obtain x'::coname where "x'\<sharp>(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'\<sharp>(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'\<sharp>(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'\<sharp>(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'\<sharp>(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'\<sharp>(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'\<sharp>(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'\<sharp>(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'\<sharp>(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'\<sharp>(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)+

lemmas subst_supp = supp_subst1 supp_subst2 supp_subst3 supp_subst4
 supp_subst5 supp_subst6 supp_subst7 supp_subst8
lemma subst_fresh:
 fixes x::"name"
 and c::"coname"
 shows "x\P \ x\M{x:=.P}"
 and "b\P \ b\M{b:=(y).P}"
 and "x\(M,P) \ x\M{y:=.P}"
 and "x\M \ x\M{c:=(x).P}"
 and "x\(M,P) \ x\M{c:=(y).P}"
 and "b\(M,P) \ b\M{c:=(y).P}"
 and "b\M \ b\M{y:=.P}"
 and "b\(M,P) \ b\M{y:=.P}"
 using subst_supp
 by(fastforce simp add: fresh_def supp_prod)+

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)
 then show ?case
 apply(auto simp: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
 apply (metis (no_types, lifting))+
 done
next
 case ImpL
 then show ?case
 by (auto simp: calc_atm alpha fresh_atm abs_fresh fresh_prod fresh_left)
 metis
next
 case (Cut d M y M')
 then show ?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'\<sharp>(N,M{c3:=(y).([(y,x)]\<bullet>N)},M'{c3:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>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)
 then show ?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)
 then show ?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')
 then show ?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)
 then show ?case
 by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
 case NotR
 then show ?case
 by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
next
 case (NotL d M y)
 then obtain a'::name where "a'\<sharp>(N, M{x:=<c>.([(c,a)]\<bullet>N)}, [(c,a)]\<bullet>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)
 then obtain a'::name where "a'\<sharp>(N,M{x:=<c>.([(c,a)]\<bullet>N)},M'{x:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>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)
 then obtain a'::name where "a'\<sharp>(N,M{x:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>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)
 then obtain a'::name where "a'\<sharp>(N,M{x:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>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)
 then obtain a'::name where "a'\<sharp>(N,M{u:=<c>.([(c,a)]\<bullet>N)},M'{u:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>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')
 then show ?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)
 also have "\ = ([(x',x)]\M){x':=.([(c',c)]\N)}" using a by (simp add: substn_rename4)
 finally show ?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)
 also have "\ = ([(c',c)]\M){c':=(x').([(x',x)]\N)}" using a by (simp add: substc_rename2)
 finally show ?thesis by simp
qed

lemmas subst_rename = substc_rename1 substc_rename2 substn_rename3 substn_rename4 subst_rename5 subst_rename6

lemma better_Cut_substn[simp]:
 assumes a: "a\[c].P" "x\(y,P)"
 shows "(Cut .M (x).N){y:=.P} =
 (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
proof -
 obtain x'::"name" where fs1: "x'\<sharp>(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
 obtain a'::"coname" where fs2: "a'\<sharp>(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
 have eq1: "(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)
 have eq2: "(M=Ax y a) = (([(a',a)]\M)=Ax y a')"
 by (metis perm_swap(4) swap_simps(4) swap_simps(8) trm.perm(13))
 have "(Cut .M (x).N){y:=.P} = (Cut .([(a',a)]\M) (x').([(x',x)]\N)){y:=.P}"
 using eq1 by simp
 also have "\ = (if ([(a',a)]\M)=Ax y a' then Cut .P (x').(([(x',x)]\N){y:=.P})
 else Cut <a'>.(([(a',a)]\<bullet>M){y:=<c>.P}) (x').(([(x',x)]\<bullet>N){y:=<c>.P}))"
 using fs1 fs2 by (auto simp: fresh_prod fresh_left calc_atm fresh_atm)
 also have "\ =(if M=Ax y a then Cut .P (x).(N{y:=.P}) else Cut .(M{y:=.P}) (x).(N{y:=.P}))"
 using fs1 fs2 a
 unfolding eq2[symmetric]
 apply(auto simp: trm.inject)
 apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh eqvts perm_fresh_fresh calc_atm)
 apply (simp add: fresh_atm(2) substn_rename4)
 by (metis abs_fresh(2) fresh_atm(2) fresh_prod perm_fresh_fresh(2) substn_rename4)
 finally show ?thesis by simp
qed

lemma better_Cut_substc[simp]:
 assumes a: "a\(c,P)" "x\[y].P"
 shows "(Cut .M (x).N){c:=(y).P} =
 (if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))"
proof -
 obtain x'::"name" where fs1: "x'\<sharp>(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
 obtain a'::"coname" where fs2: "a'\<sharp>(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
 have eq1: "(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)
 have eq2: "(N=Ax x c) = (([(x',x)]\N)=Ax x' c)"
 by (metis perm_dj(1) perm_swap(1) swap_simps(1) trm.perm(1))
 have "(Cut .M (x).N){c:=(y).P} = (Cut .([(a',a)]\M) (x').([(x',x)]\N)){c:=(y).P}"
 using eq1 by simp
 also have "\ = (if ([(x',x)]\N)=Ax x' c then Cut .(([(a',a)]\M){c:=(y).P}) (y).P
 else Cut <a'>.(([(a',a)]\<bullet>M){c:=(y).P}) (x').(([(x',x)]\<bullet>N){c:=(y).P}))"
 using fs1 fs2 by (simp add: fresh_prod fresh_left calc_atm fresh_atm trm.inject)
 also have "\ =(if N=Ax x c then Cut .(M{c:=(y).P}) (y).P else Cut .(M{c:=(y).P}) (x).(N{c:=(y).P}))"
 using fs1 fs2 a
 unfolding eq2[symmetric]
 apply(auto simp: trm.inject)
 apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh eqvts perm_fresh_fresh calc_atm)
 by (metis abs_fresh(1) fresh_atm(1) fresh_prod perm_fresh_fresh(1) substc_rename2)
 finally show ?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)
 then have *: "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)"
 then have "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')"
--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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 ist noch experimentell.