--- a/src/HOL/Nominal/Examples/Class.thy Thu Jul 03 00:56:45 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Thu Jul 03 00:58:30 2008 +0200
@@ -369,7 +369,7 @@
apply(rule fresh_perm_name)
apply(assumption)
apply(assumption)
-apply(simp add: at_prm_fresh[OF at_name_inst])
+apply(simp add: at_prm_fresh[OF at_name_inst] swap_simps)
apply(perm_simp)
apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,pi2\<bullet>P,pi2\<bullet>M,pi2)")
apply(simp add: fresh_prod)
@@ -410,7 +410,7 @@
apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_AndL1 at_prm_fresh[OF at_name_inst])
+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)
@@ -453,7 +453,7 @@
apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_AndL2 at_prm_fresh[OF at_name_inst])
+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)
@@ -496,7 +496,7 @@
apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,u,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>x,pi1\<bullet>u,pi1)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_OrL at_prm_fresh[OF at_name_inst])
+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)
@@ -539,7 +539,7 @@
apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>x,pi1)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_ImpL at_prm_fresh[OF at_name_inst])
+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)
@@ -589,7 +589,7 @@
apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,pi2\<bullet>P,pi2\<bullet>M,pi2)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_NotR at_prm_fresh[OF at_coname_inst])
+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
@@ -632,7 +632,7 @@
apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,N,b,c,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>N,pi2\<bullet>b,pi2\<bullet>c,pi2)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_AndR at_prm_fresh[OF at_coname_inst])
+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
@@ -675,7 +675,7 @@
apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst])
+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
@@ -718,7 +718,7 @@
apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst])
+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
@@ -761,7 +761,7 @@
apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
apply(simp add: fresh_prod)
apply(auto)
-apply(simp add: fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst])
+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
@@ -10332,12 +10332,12 @@
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>xa" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
lemma NOTRIGHT_eqvt_coname:
@@ -10358,12 +10358,12 @@
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>xa" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
consts
@@ -10392,12 +10392,12 @@
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>xa" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
lemma NOTLEFT_eqvt_coname:
@@ -10418,12 +10418,12 @@
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>xa" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
consts
@@ -10460,14 +10460,14 @@
apply(rule_tac x="(rev pi)\<bullet>b" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
apply(rule_tac x="(rev pi)\<bullet>N" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
lemma ANDRIGHT_eqvt_coname:
@@ -10557,12 +10557,12 @@
apply(rule_tac x="(rev pi)\<bullet>xa" in exI)
apply(rule_tac x="(rev pi)\<bullet>y" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
consts
@@ -10617,12 +10617,12 @@
apply(rule_tac x="(rev pi)\<bullet>xa" in exI)
apply(rule_tac x="(rev pi)\<bullet>y" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
consts
@@ -10694,14 +10694,14 @@
apply(rule_tac x="(rev pi)\<bullet>z" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
apply(rule_tac x="(rev pi)\<bullet>N" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
consts
@@ -10730,12 +10730,12 @@
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>b" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
lemma ORRIGHT1_eqvt_coname:
@@ -10790,12 +10790,12 @@
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>b" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
lemma ORRIGHT2_eqvt_coname:
@@ -10860,16 +10860,16 @@
apply(perm_simp add: nsubst_eqvt)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp add: fresh_right)
+apply(simp add: swap_simps fresh_left)
apply(rule_tac x="(rev pi)\<bullet>(<b>:ImpR xa.<a>.M b)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)\<bullet>xa" in exI)
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>b" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
-apply(simp)
+apply(simp add: swap_simps)
apply(rule conjI)
apply(auto)[1]
apply(drule_tac x="pi\<bullet>z" in spec)
@@ -10886,9 +10886,9 @@
apply(drule_tac x="pi\<bullet>c" in spec)
apply(drule_tac x="pi\<bullet>Q" in spec)
apply(drule mp)
-apply(simp add: fresh_right)
+apply(simp add: swap_simps fresh_left)
apply(rule_tac x="<c>:Q" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(auto)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
@@ -10913,7 +10913,7 @@
apply(perm_simp add: csubst_eqvt)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-apply(simp add: fresh_right)
+apply(simp add: swap_simps fresh_left)
apply(auto)[1]
apply(rule_tac x="<a>:(M{xb:=<((rev pi)\<bullet>c)>.((rev pi)\<bullet>Q)})" in exI)
apply(perm_simp add: nsubst_eqvt)
@@ -10926,17 +10926,17 @@
apply(rule_tac x="(rev pi)\<bullet>a" in exI)
apply(rule_tac x="(rev pi)\<bullet>b" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(2))
-apply(simp)
+apply(simp add: swap_simps)
apply(rule conjI)
apply(auto)[1]
apply(drule_tac x="pi\<bullet>z" in spec)
apply(drule_tac x="pi\<bullet>P" in spec)
-apply(simp add: fresh_right)
+apply(simp add: swap_simps fresh_left)
apply(drule mp)
apply(rule_tac x="(z):P" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(auto)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
@@ -10988,14 +10988,14 @@
apply(rule_tac x="(rev pi)\<bullet>y" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
apply(rule_tac x="(rev pi)\<bullet>N" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
lemma IMPLEFT_eqvt_coname:
@@ -11023,14 +11023,14 @@
apply(rule_tac x="(rev pi)\<bullet>y" in exI)
apply(rule_tac x="(rev pi)\<bullet>M" in exI)
apply(rule_tac x="(rev pi)\<bullet>N" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-apply(simp)
+apply(simp add: swap_simps)
done
lemma sum_cases:
@@ -11376,7 +11376,7 @@
apply(perm_simp)
apply(rule_tac x="rev pi\<bullet>a" in exI)
apply(rule_tac x="rev pi\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(auto)[1]
apply(drule_tac x="pi\<bullet>x" in spec)
apply(drule_tac x="pi\<bullet>P" in spec)
@@ -11407,7 +11407,7 @@
apply(perm_simp)
apply(rule_tac x="rev pi\<bullet>xa" in exI)
apply(rule_tac x="rev pi\<bullet>M" in exI)
-apply(simp)
+apply(simp add: swap_simps)
apply(auto)[1]
apply(drule_tac x="pi\<bullet>a" in spec)
apply(drule_tac x="pi\<bullet>P" in spec)
@@ -12547,7 +12547,6 @@
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
-apply(simp)
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
@@ -12582,7 +12581,6 @@
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
apply(simp)
-apply(simp)
apply(case_tac "b=aa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
@@ -12617,7 +12615,6 @@
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
apply(simp)
-apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
@@ -12648,7 +12645,6 @@
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
-apply(simp)
done
lemma IMPLEFT_elim:
@@ -13084,7 +13080,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="\<parallel>(ty1)\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="cb" and z="ca" in alpha_name_coname)
@@ -13114,7 +13109,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="\<parallel><ty2>\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="ca" and z="c" in alpha_name_coname)
@@ -13149,7 +13143,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="\<parallel>(ty1)\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="cb" and z="ca" in alpha_name_coname)
@@ -13184,7 +13177,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="\<parallel><ty2>\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(case_tac "a=aa")
apply(simp)
apply(generate_fresh "name")
@@ -13221,7 +13213,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="\<parallel>(ty1)\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(simp)
apply(case_tac "ba=aa")
apply(simp)
@@ -13259,7 +13250,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="\<parallel>(ty1)\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
@@ -13295,7 +13285,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="\<parallel>(ty1)\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(case_tac "a=aa")
apply(simp)
apply(generate_fresh "name")
@@ -13332,7 +13321,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="\<parallel><ty2>\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(simp)
apply(case_tac "ba=aa")
apply(simp)
@@ -13370,7 +13358,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="\<parallel><ty2>\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
@@ -13406,7 +13393,6 @@
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="\<parallel><ty2>\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
-apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
done
text {* Main lemma 1 *}
@@ -14772,7 +14758,6 @@
apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
-apply(simp add: calc_atm)
apply(rule_tac x="[(name,x)]\<bullet>[(coname1, c)]\<bullet>trm" in exI)
apply(perm_simp)
apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
@@ -15884,7 +15869,6 @@
apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
-apply(simp add: calc_atm)
apply(rule_tac x="[(name,x)]\<bullet>[(coname1, c)]\<bullet>trm" in exI)
apply(perm_simp)
apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
@@ -17360,7 +17344,6 @@
apply(drule_tac pi="[(ca,z)]" and X="\<parallel>(B1)\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name csubst_eqvt)
apply(perm_simp)
-apply(simp add: calc_atm)
done