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]) <b>.(N[d \<turnstile>c>e]) e else AndR <a>.(M[d\<turnstile>c>e]) <b>.(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 <b>.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 <b>.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 <b>.M a') (x).P))"
and "pi2\fresh_fun (\a'. Cut .(OrR1 .M a') (x).P)=
fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 <b>.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 <b>.M a') (x).P))"
and "pi2\fresh_fun (\a'. Cut .(OrR2 .M a') (x).P)=
fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 <b>.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).<b>.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).<b>.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 <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(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}) <b>.(N{d:=(z).P}) a') (z).P)
else AndR <a>.(M{d:=(z).P}) <b>.(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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.56Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
