Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Class1.thy Sprache: Isabelle

Original von: 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>

nominal_datatype ty =
 PR "string"
 | NOT "ty"
 | AND "ty" "ty" ("_ AND _" [100,100] 100)
 | OR "ty" "ty" ("_ OR _" [100,100] 100)
 | IMP "ty" "ty" ("_ IMP _" [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 add: fresh_string)

text \<open>terms\<close>

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

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,100,100] 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"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fin_supp)+
apply(fresh_guess)+
done

nominal_primrec (freshness_context: "(u::name,v::name)")
 nrename :: "trm \ name \ name \ trm" ("_[_\n>_]" [100,100,100] 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)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
apply(fresh_guess)+
done

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)]"
apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

lemma crename_coname_eqvt[eqvt]:
 fixes pi::"coname prm"
 shows "pi\(M[d\c>e]) = (pi\M)[(pi\d)\c>(pi\e)]"
apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

lemma nrename_name_eqvt[eqvt]:
 fixes pi::"name prm"
 shows "pi\(M[x\n>y]) = (pi\M)[(pi\x)\n>(pi\y)]"
apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

lemma nrename_coname_eqvt[eqvt]:
 fixes pi::"coname prm"
 shows "pi\(M[x\n>y]) = (pi\M)[(pi\x)\n>(pi\y)]"
apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
apply(auto simp add: fresh_bij eq_bij)
done

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 add: 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 add: 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 add: 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 add: 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 add: 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 add: 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 add: 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 add: 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
apply(nominal_induct M avoiding: x x' y rule: trm.strong_induct)
apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
done

lemma crename_rename:
 assumes a: "a'\M"
 shows "([(a',a)]\M)[a'\c>b]= M[a\c>b]"
using a
apply(nominal_induct M avoiding: a a' b rule: trm.strong_induct)
apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
done

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 add: 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
 apply -
 apply(rule nrename.simps)
 apply(simp add: fresh_left calc_atm)
 apply(simp add: fresh_left calc_atm)
 done
 also have "\ = Cut .(M[u\n>v]) (x).(N[u\n>v])" using fs1 fs2 a
 apply -
 apply(simp add: trm.inject alpha fresh_atm fresh_prod rename_eqvts)
 apply(simp add: calc_atm)
 apply(simp add: rename_fresh fresh_atm)
 done
 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 add: 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
 apply -
 apply(rule crename.simps)
 apply(simp add: fresh_left calc_atm)
 apply(simp add: fresh_left calc_atm)
 done
 also have "\ = Cut .(M[b\c>c]) (x).(N[b\c>c])" using fs1 fs2 a
 apply -
 apply(simp add: trm.inject alpha fresh_atm fresh_prod rename_eqvts)
 apply(simp add: calc_atm)
 apply(simp add: rename_fresh fresh_atm)
 done
 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)
 (simp_all add: calc_atm fresh_atm trm.inject alpha abs_fresh abs_supp fin_supp)

lemma crename_swap:
 shows "a\M \ [(a,b)]\M = M[b\c>a]"
by (nominal_induct M avoiding: a b rule: trm.strong_induct)
 (simp_all add: calc_atm fresh_atm trm.inject alpha abs_fresh abs_supp fin_supp)

lemma crename_ax:
 assumes a: "M[a\c>b] = Ax x c" "c\a" "c\b"
 shows "M = Ax x c"
using a
apply(nominal_induct M avoiding: a b x c rule: trm.strong_induct)
apply(simp_all add: trm.inject split: if_splits)
done

lemma nrename_ax:
 assumes a: "M[x\n>y] = Ax z a" "z\x" "z\y"
 shows "M = Ax z a"
using a
apply(nominal_induct M avoiding: x y z a rule: trm.strong_induct)
apply(simp_all add: trm.inject split: if_splits)
done

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)"
using a
apply -
apply(simp add: fresh_left)
apply(simp add: at_prm_fresh[OF at_coname_inst] fresh_list_rev)
done

lemma fresh_perm_name:
 fixes x::"name"
 and pi::"name prm"
 and M::"trm"
 assumes a: "x\pi" "x\M"
 shows "x\(pi\M)"
using a
apply -
apply(simp add: fresh_left)
apply(simp add: at_prm_fresh[OF at_name_inst] fresh_list_rev)
done

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'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "\n::name. n\(c,P,a,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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 -
apply(perm_simp)
apply(generate_fresh "name")
apply(auto simp add: fresh_prod)
apply(simp add: fresh_fun_simp_NotL)
apply(rule sym)
apply(rule trans)
apply(rule fresh_fun_simp_NotL)
apply(rule fresh_perm_name)
apply(assumption)
apply(assumption)
apply(rule fresh_perm_name)
apply(assumption)
apply(assumption)
apply(simp add: at_prm_fresh[OF at_name_inst] swap_simps)
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,pi2\P,pi2\M,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_NotL calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "\n::name. n\(c,P,x,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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 -
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,x,pi1\P,pi1\M,pi1\x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL1 at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,x,pi2\P,pi2\M,pi2\x,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL1 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "\n::name. n\(c,P,x,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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 -
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,x,pi1\P,pi1\M,pi1\x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL2 at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,x,pi2\P,pi2\M,pi2\x,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndL2 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "\n::name. n\(c,P,x,M,u,N)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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 -
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(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrL at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
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(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrL calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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'"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_name_inst)
apply(rule at_name_inst)
apply(finite_guess)
apply(subgoal_tac "\n::name. n\(c,P,x,M,N)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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 -
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,N,x,pi1\P,pi1\M,pi1\N,pi1\x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpL at_prm_fresh[OF at_name_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "\n::name. n\(P,M,N,x,pi2\P,pi2\M,pi2\N,pi2\x,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpL calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "\n::coname. n\(x,P,y,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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 -
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,pi1\P,pi1\M,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_NotR calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,pi2\P,pi2\M,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_NotR at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "\n::coname. n\(x,P,b,M,c,N)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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 -
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(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndR calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
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(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_AndR at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "\n::coname. n\(x,P,b,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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))"
 and "pi2\fresh_fun (\a'. Cut .(OrR1 .M a') (x).P)=
 fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 .M a') (x).P))"
apply -
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,b,pi1\P,pi1\M,pi1\b,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR1 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,b,pi2\P,pi2\M,pi2\b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma fresh_fun_simp_OrR2:
 assumes a: "a'\P" "a'\M" "a'\b"
 shows "fresh_fun (\a'. Cut .(OrR2 .M a') (x).P) = Cut .(OrR2 .M a') (x).P"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "\n::coname. n\(x,P,b,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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))"
 and "pi2\fresh_fun (\a'. Cut .(OrR2 .M a') (x).P)=
 fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 .M a') (x).P))"
apply -
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,b,pi1\P,pi1\M,pi1\b,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR2 calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,b,pi2\P,pi2\M,pi2\b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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"
using a
apply -
apply(rule fresh_fun_app)
apply(rule pt_coname_inst)
apply(rule at_coname_inst)
apply(finite_guess)
apply(subgoal_tac "\n::coname. n\(x,P,y,b,M)")
apply(erule exE)
apply(rule_tac x="n" in exI)
apply(simp add: fresh_prod abs_fresh)
apply(fresh_guess)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(fresh_guess)
done

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))"
 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))"
apply -
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,b,pi1\P,pi1\M,pi1\b,pi1)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpR calc_atm)
apply(rule exists_fresh')
apply(simp add: fin_supp)
apply(perm_simp)
apply(subgoal_tac "\n::coname. n\(P,M,b,pi2\P,pi2\M,pi2\b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
apply(simp add: fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

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)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::name. x\(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::name. x\(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::name. x\(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::name. x\(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::name. x\(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::name. x\(x3,P,y1,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::name. x\(x3,P,y1,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(fresh_guess)+
done

nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
 substc :: "trm \ coname \ name \ trm \ trm" ("_{_:=(_)._}" [100,100,100,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)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
apply(rule impI)
apply(subgoal_tac "\x::coname. x\(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::coname. x\(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::coname. x\(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::coname. x\(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::coname. x\(x1,P,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::coname. x\(x1,P,x2,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh fresh_atm abs_supp)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(rule impI)
apply(subgoal_tac "\x::coname. x\(x1,P,x2,y1)", erule exE, simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh fresh_atm)
apply(rule exists_fresh', simp add: fin_supp)
apply(simp add: abs_fresh abs_supp)+
apply(fresh_guess add: abs_fresh fresh_prod)+
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)}"
apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
apply(auto simp add: eq_bij fresh_bij eqvts)
apply(perm_simp)+
done

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)}"
apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
apply(auto simp add: eq_bij fresh_bij eqvts)
apply(perm_simp)+
done

lemma supp_subst1:
 shows "supp (M{y:=.P}) \ ((supp M) - {y}) \ (supp P)"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
done

lemma supp_subst2:
 shows "supp (M{y:=.P}) \ supp (M) \ ((supp P) - {c})"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)+
done

lemma supp_subst3:
 shows "supp (M{c:=(x).P}) \ ((supp M) - {c}) \ (supp P)"
apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
done

lemma supp_subst4:
 shows "supp (M{c:=(x).P}) \ (supp M) \ ((supp P) - {x})"
apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpR abs_fresh abs_supp fin_supp fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
done

lemma supp_subst5:
 shows "(supp M - {y}) \ supp (M{y:=.P})"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
done

lemma supp_subst6:
 shows "(supp M) \ ((supp (M{y:=.P}))::coname set)"
apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},P,name1,trm2{y:=.P},name2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},P,name1,trm2{name2:=.P})")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm)
apply(blast)
apply(rule exists_fresh'(1)[OF fs_name1])
apply(blast)
done

lemma supp_subst7:
 shows "(supp M - {c}) \ supp (M{c:=(x).P})"
apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
apply(auto)
apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname:=(x).P},P)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(subgoal_tac "\x'::coname. x'\(trm1{coname3:=(x).P},P,trm2{coname3:=(x).P},coname1,coname2)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
apply(simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
apply(blast)
apply(rule exists_fresh'(2)[OF fs_coname1])
apply(blast)+
apply(subgoal_tac "\x'::coname. x'\(trm{coname2:=(x).P},P,coname1)")
apply(erule exE)
apply(simp add: fresh_prod)
apply(erule conjE)+
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Class1.thy Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©