# HG changeset patch
# User wenzelm
# Date 1713625834 -7200
# Node ID e9ea4d88490d8f35f73ed335685bdc8d279c3b7f
# Parent  5972799988afaf410eb55940c0d0679d8a4058c9
backed out changeset 601ff5c7cad5: not relevant for Isabelle2024;

diff -r 5972799988af -r e9ea4d88490d src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sat Apr 20 16:07:00 2024 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Sat Apr 20 17:10:34 2024 +0200
@@ -1,6 +1,5 @@
 theory Nominal 
-  imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"
-
+imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"
 keywords
   "atom_decl" :: thy_decl and
   "nominal_datatype" :: thy_defn and
@@ -727,13 +726,17 @@
   and   b  :: "'x"
   assumes at: "at TYPE('x)"
   shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)"
-proof(induct_tac pi2)
-  show "(pi1 @ []) \<triangleq> (pi1 \<bullet> [] @ pi1)"
-    by(simp add: prm_eq_def)
-  show "\<And>a l. (pi1 @ l) \<triangleq> (pi1 \<bullet> l @ pi1)  \<Longrightarrow>
-        (pi1 @ a # l) \<triangleq> (pi1 \<bullet> (a # l) @ pi1) "
-    by(auto simp add: prm_eq_def at at2 at_append at_ds8_aux)
-qed
+apply(induct_tac pi2)
+apply(simp add: prm_eq_def)
+apply(auto simp add: prm_eq_def)
+apply(simp add: at2[OF at])
+apply(drule_tac x="aa" in spec)
+apply(drule sym)
+apply(simp)
+apply(simp add: at_append[OF at])
+apply(simp add: at2[OF at])
+apply(simp add: at_ds8_aux[OF at])
+done
 
 lemma at_ds9: 
   fixes pi1 :: "'x prm"
@@ -742,16 +745,32 @@
   and   b  :: "'x"
   assumes at: "at TYPE('x)"
   shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
-  using at at_ds8 at_prm_rev_eq1 rev_append by fastforce
+apply(induct_tac pi2)
+apply(simp add: prm_eq_def)
+apply(auto simp add: prm_eq_def)
+apply(simp add: at_append[OF at])
+apply(simp add: at2[OF at] at1[OF at])
+apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec)
+apply(drule sym)
+apply(simp)
+apply(simp add: at_ds8_aux[OF at])
+apply(simp add: at_rev_pi[OF at])
+done
 
 lemma at_ds10:
   fixes pi :: "'x prm"
   and   a  :: "'x"
   and   b  :: "'x"
-  assumes "at TYPE('x)"
-  and     "b\<sharp>(rev pi)"
+  assumes at: "at TYPE('x)"
+  and     a:  "b\<sharp>(rev pi)"
   shows "([(pi\<bullet>a,b)]@pi) \<triangleq> (pi@[(a,b)])"
-  by (metis assms at_bij1 at_ds2 at_prm_fresh)
+using a
+apply -
+apply(rule at_prm_eq_trans)
+apply(rule at_ds2[OF at])
+apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at])
+apply(rule at_prm_eq_refl)
+done
 
 \<comment> \<open>there always exists an atom that is not being in a finite set\<close>
 lemma ex_in_inf:
@@ -759,7 +778,14 @@
   assumes at: "at TYPE('x)"
   and     fs: "finite A"
   obtains c::"'x" where "c\<notin>A"
-  using at at4 ex_new_if_finite fs by blast
+proof -
+  from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
+    by (simp add: Diff_infinite_finite)
+  hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
+  then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
+  then have "c\<notin>A" by simp
+  then show ?thesis ..
+qed
 
 text \<open>there always exists a fresh name for an object with finite support\<close>
 lemma at_exists_fresh': 
@@ -780,8 +806,16 @@
   fixes S::"'a set"
   assumes a: "at TYPE('a)"
   and     b: "finite S" 
-  shows "\<exists>x. x \<notin> S"
-  by (meson a b ex_in_inf) 
+  shows "\<exists>x. x \<notin> S" 
+  using a b
+  apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite)
+  apply(simp add: at_def)
+  apply(subgoal_tac "UNIV - S \<noteq> {}")
+  apply(simp only: ex_in_conv [symmetric])
+  apply(blast)
+  apply(rule notI)
+  apply(simp)
+  done
 
 lemma at_different:
   assumes at: "at TYPE('x)"
@@ -789,8 +823,12 @@
 proof -
   have "infinite (UNIV::'x set)" by (rule at4[OF at])
   hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove)
-  have "(UNIV-{a}) \<noteq> ({}::'x set)"
-    by (metis finite.emptyI inf2) 
+  have "(UNIV-{a}) \<noteq> ({}::'x set)" 
+  proof (rule_tac ccontr, drule_tac notnotD)
+    assume "UNIV-{a} = ({}::'x set)"
+    with inf2 have "infinite ({}::'x set)" by simp
+    then show "False" by auto
+  qed
   hence "\<exists>(b::'x). b\<in>(UNIV-{a})" by blast
   then obtain b::"'x" where mem2: "b\<in>(UNIV-{a})" by blast
   from mem2 have "a\<noteq>b" by blast
@@ -801,7 +839,11 @@
 lemma at_pt_inst:
   assumes at: "at TYPE('x)"
   shows "pt TYPE('x) TYPE('x)"
-  using at at_append at_def prm_eq_def pt_def by fastforce
+apply(auto simp only: pt_def)
+apply(simp only: at1[OF at])
+apply(simp only: at_append[OF at]) 
+apply(simp only: prm_eq_def)
+done
 
 section \<open>finite support properties\<close>
 (*===================================*)
@@ -816,36 +858,56 @@
   fixes a :: "'x"
   assumes at: "at TYPE('x)"
   shows "fs TYPE('x) TYPE('x)"
-  by (simp add: at at_supp fs_def)
+apply(simp add: fs_def) 
+apply(simp add: at_supp[OF at])
+done
 
 lemma fs_unit_inst:
   shows "fs TYPE(unit) TYPE('x)"
-  by(simp add: fs_def supp_unit)
+apply(simp add: fs_def)
+apply(simp add: supp_unit)
+done
 
 lemma fs_prod_inst:
   assumes fsa: "fs TYPE('a) TYPE('x)"
   and     fsb: "fs TYPE('b) TYPE('x)"
   shows "fs TYPE('a\<times>'b) TYPE('x)"
-  by (simp add: assms fs1 supp_prod fs_def)
-
+apply(unfold fs_def)
+apply(auto simp add: supp_prod)
+apply(rule fs1[OF fsa])
+apply(rule fs1[OF fsb])
+done
 
 lemma fs_nprod_inst:
   assumes fsa: "fs TYPE('a) TYPE('x)"
   and     fsb: "fs TYPE('b) TYPE('x)"
   shows "fs TYPE(('a,'b) nprod) TYPE('x)"
-  unfolding fs_def by (metis assms finite_Un fs_def nprod.exhaust supp_nprod)
+apply(unfold fs_def, rule allI)
+apply(case_tac x)
+apply(auto simp add: supp_nprod)
+apply(rule fs1[OF fsa])
+apply(rule fs1[OF fsb])
+done
 
 lemma fs_list_inst:
-  assumes "fs TYPE('a) TYPE('x)"
+  assumes fs: "fs TYPE('a) TYPE('x)"
   shows "fs TYPE('a list) TYPE('x)"
-  unfolding fs_def
-  by (clarify, induct_tac x) (auto simp: fs1 assms supp_list_nil supp_list_cons)
+apply(simp add: fs_def, rule allI)
+apply(induct_tac x)
+apply(simp add: supp_list_nil)
+apply(simp add: supp_list_cons)
+apply(rule fs1[OF fs])
+done
 
 lemma fs_option_inst:
   assumes fs: "fs TYPE('a) TYPE('x)"
   shows "fs TYPE('a option) TYPE('x)"
-  unfolding fs_def
-  by (metis assms finite.emptyI fs1 option.exhaust supp_none supp_some)
+apply(simp add: fs_def, rule allI)
+apply(case_tac x)
+apply(simp add: supp_none)
+apply(simp add: supp_some)
+apply(rule fs1[OF fs])
+done
 
 section \<open>Lemmas about the permutation properties\<close>
 (*=================================================*)
@@ -892,10 +954,13 @@
   using cp by (simp add: cp_def)
 
 lemma cp_pt_inst:
-  assumes "pt TYPE('a) TYPE('x)"
-  and     "at TYPE('x)"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
   shows "cp TYPE('a) TYPE('x) TYPE('x)"
-  using assms at_ds8 cp_def pt2 pt3 by fastforce
+apply(auto simp add: cp_def pt2[OF pt,symmetric])
+apply(rule pt3[OF pt])
+apply(rule at_ds8[OF at])
+done
 
 section \<open>disjointness properties\<close>
 (*=================================*)
@@ -933,7 +998,8 @@
   fixes a::"'x"
   assumes dj: "disjoint TYPE('x) TYPE('y)"
   shows "(supp a) = ({}::'y set)"
-  by (simp add: supp_def dj_perm_forget[OF dj])
+apply(simp add: supp_def dj_perm_forget[OF dj])
+done
 
 lemma at_fresh_ineq:
   fixes a :: "'x"
@@ -950,8 +1016,15 @@
   and     ptb: "pt TYPE('b) TYPE('x)"
   and     at:  "at TYPE('x)"
   shows  "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
-  unfolding pt_def using assms
-  by (auto simp add: perm_fun_def pt1 pt2 ptb pt3 pt3_rev)
+apply(auto simp only: pt_def)
+apply(simp_all add: perm_fun_def)
+apply(simp add: pt1[OF pta] pt1[OF ptb])
+apply(simp add: pt2[OF pta] pt2[OF ptb])
+apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*)
+apply(simp add: pt3[OF pta] pt3[OF ptb])
+(*A*)
+apply(simp add: at_prm_rev_eq[OF at])
+done
 
 lemma pt_bool_inst:
   shows  "pt TYPE(bool) TYPE('x)"
@@ -960,8 +1033,11 @@
 lemma pt_set_inst:
   assumes pt: "pt TYPE('a) TYPE('x)"
   shows  "pt TYPE('a set) TYPE('x)"
-  unfolding pt_def
-  by(auto simp add: perm_set_def  pt1[OF pt] pt2[OF pt] pt3[OF pt])
+apply(simp add: pt_def)
+apply(simp_all add: perm_set_def)
+apply(simp add: pt1[OF pt])
+apply(force simp add: pt2[OF pt] pt3[OF pt])
+done
 
 lemma pt_unit_inst:
   shows "pt TYPE(unit) TYPE('x)"
@@ -970,15 +1046,23 @@
 lemma pt_prod_inst:
   assumes pta: "pt TYPE('a) TYPE('x)"
   and     ptb: "pt TYPE('b) TYPE('x)"
-shows  "pt TYPE('a \<times> 'b) TYPE('x)"
-  using assms pt1 pt2 pt3
-  by(auto simp add: pt_def)
+  shows  "pt TYPE('a \<times> 'b) TYPE('x)"
+  apply(auto simp add: pt_def)
+  apply(rule pt1[OF pta])
+  apply(rule pt1[OF ptb])
+  apply(rule pt2[OF pta])
+  apply(rule pt2[OF ptb])
+  apply(rule pt3[OF pta],assumption)
+  apply(rule pt3[OF ptb],assumption)
+  done
 
 lemma pt_list_nil: 
   fixes xs :: "'a list"
   assumes pt: "pt TYPE('a) TYPE ('x)"
   shows "([]::'x prm)\<bullet>xs = xs" 
-  by (induct_tac xs) (simp_all add: pt1[OF pt])
+apply(induct_tac xs)
+apply(simp_all add: pt1[OF pt])
+done
 
 lemma pt_list_append: 
   fixes pi1 :: "'x prm"
@@ -986,7 +1070,9 @@
   and   xs  :: "'a list"
   assumes pt: "pt TYPE('a) TYPE ('x)"
   shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)"
-  by (induct_tac xs) (simp_all add: pt2[OF pt])
+apply(induct_tac xs)
+apply(simp_all add: pt2[OF pt])
+done
 
 lemma pt_list_prm_eq: 
   fixes pi1 :: "'x prm"
@@ -994,67 +1080,55 @@
   and   xs  :: "'a list"
   assumes pt: "pt TYPE('a) TYPE ('x)"
   shows "pi1 \<triangleq> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
-  by (induct_tac xs) (simp_all add: pt3[OF pt])
+apply(induct_tac xs)
+apply(simp_all add: prm_eq_def pt3[OF pt])
+done
 
 lemma pt_list_inst:
   assumes pt: "pt TYPE('a) TYPE('x)"
   shows  "pt TYPE('a list) TYPE('x)"
-  by (simp add: pt pt_def pt_list_append pt_list_nil pt_list_prm_eq)
+apply(auto simp only: pt_def)
+apply(rule pt_list_nil[OF pt])
+apply(rule pt_list_append[OF pt])
+apply(rule pt_list_prm_eq[OF pt],assumption)
+done
 
 lemma pt_option_inst:
   assumes pta: "pt TYPE('a) TYPE('x)"
   shows  "pt TYPE('a option) TYPE('x)"
-proof -
-  have "([]::('x \<times> _) list) \<bullet> x = x" for x :: "'a option"
-    by (metis assms none_eqvt not_None_eq pt1 some_eqvt)
-  moreover have "(pi1 @ pi2) \<bullet> x = pi1 \<bullet> pi2 \<bullet> x"
-    for pi1 pi2 :: "('x \<times> 'x) list" and x :: "'a option"
-    by (metis assms none_eqvt option.collapse pt2 some_eqvt)
-  moreover have "pi1 \<bullet> x = pi2 \<bullet> x"
-    if "pi1 \<triangleq> pi2" for pi1 pi2 :: "('x \<times> 'x) list" and x :: "'a option"
-    using that pt3[OF pta] by (metis none_eqvt not_Some_eq some_eqvt)
-  ultimately show ?thesis
-    by (auto simp add: pt_def)
-qed
+apply(auto simp only: pt_def)
+apply(case_tac "x")
+apply(simp_all add: pt1[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt2[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt3[OF pta])
+done
 
 lemma pt_noption_inst:
   assumes pta: "pt TYPE('a) TYPE('x)"
   shows  "pt TYPE('a noption) TYPE('x)"
-proof -
-  have "([]::('x \<times> _) list) \<bullet> x = x" for x :: "'a noption"
-    by (metis assms nnone_eqvt noption.exhaust nsome_eqvt pt1)
-  moreover have "(pi1 @ pi2) \<bullet> x = pi1 \<bullet> pi2 \<bullet> x"
-    for pi1 pi2 :: "('x \<times> 'x) list" and x :: "'a noption"
-    using pt2[OF pta]
-    by (metis nnone_eqvt noption.exhaust nsome_eqvt)
-  moreover have "pi1 \<bullet> x = pi2 \<bullet> x"
-    if "pi1 \<triangleq> pi2"
-    for pi1 pi2 :: "('x \<times> 'x) list"
-      and x :: "'a noption"
-    using that pt3[OF pta] by (metis nnone_eqvt noption.exhaust nsome_eqvt)
-  ultimately show ?thesis
-    by (auto simp add: pt_def)
-qed
+apply(auto simp only: pt_def)
+apply(case_tac "x")
+apply(simp_all add: pt1[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt2[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt3[OF pta])
+done
 
 lemma pt_nprod_inst:
   assumes pta: "pt TYPE('a) TYPE('x)"
   and     ptb: "pt TYPE('b) TYPE('x)"
   shows  "pt TYPE(('a,'b) nprod) TYPE('x)"
-proof -
-  have "([]::('x \<times> _) list) \<bullet> x = x"
-    for x :: "('a, 'b) nprod"
-    by (metis assms(1) nprod.exhaust perm_nprod.simps pt1 ptb)
-  moreover have "(pi1 @ pi2) \<bullet> x = pi1 \<bullet> pi2 \<bullet> x"
-    for pi1 pi2 :: "('x \<times> 'x) list" and x :: "('a, 'b) nprod"
-    using pt2[OF pta] pt2[OF ptb]
-    by (metis nprod.exhaust perm_nprod.simps)
-  moreover have "pi1 \<bullet> x = pi2 \<bullet> x"
-    if "pi1 \<triangleq> pi2" for pi1 pi2 :: "('x \<times> 'x) list" and x :: "('a, 'b) nprod"
-    using that pt3[OF pta] pt3[OF ptb] by (smt (verit) nprod.exhaust perm_nprod.simps)
-  ultimately show ?thesis
-    by (auto simp add: pt_def)
-qed
-
+  apply(auto simp add: pt_def)
+  apply(case_tac x)
+  apply(simp add: pt1[OF pta] pt1[OF ptb])
+  apply(case_tac x)
+  apply(simp add: pt2[OF pta] pt2[OF ptb])
+  apply(case_tac x)
+  apply(simp add: pt3[OF pta] pt3[OF ptb])
+  done
 
 section \<open>further lemmas for permutation types\<close>
 (*==============================================*)
@@ -1162,7 +1236,12 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "[(a,b)]\<bullet>([(b,a)]\<bullet>x) = x"
-  by (metis assms at_ds5 pt_def pt_swap_bij)
+apply(simp add: pt2[OF pt,symmetric])
+apply(rule trans)
+apply(rule pt3[OF pt])
+apply(rule at_ds5'[OF at])
+apply(rule pt1[OF pt])
+done
 
 lemma pt_swap_bij'':
   fixes a  :: "'x"
@@ -1170,7 +1249,11 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "[(a,a)]\<bullet>x = x"
-  by (metis assms at_ds1 pt_def)
+apply(rule trans)
+apply(rule pt3[OF pt])
+apply(rule at_ds1[OF at])
+apply(rule pt1[OF pt])
+done
 
 lemma supp_singleton:
   shows "supp {x} = supp x"
@@ -1237,6 +1320,14 @@
   shows "(pi\<bullet>x)\<in>X"
   using a by (simp add: pt_set_bij1[OF pt, OF at])
 
+(* FIXME: is this lemma needed anywhere? *)
+lemma pt_set_bij3:
+  fixes pi :: "'x prm"
+  and   x  :: "'a"
+  and   X  :: "'a set"
+  shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
+by (simp add: perm_bool)
+
 lemma pt_subseteq_eqvt:
   fixes pi :: "'x prm"
   and   Y  :: "'a set"
@@ -1260,13 +1351,10 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
-proof -
-  have "\<exists>y. x = pi \<bullet> y \<and> P y"
-    if "P (rev pi \<bullet> x)" for x
-    using that by (metis at pt pt_pi_rev)
-  then show ?thesis
-    by (auto simp add: perm_set_def pt_rev_pi [OF assms])
-qed
+apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
+apply(rule_tac x="(rev pi)\<bullet>x" in exI)
+apply(simp add: pt_pi_rev[OF pt, OF at])
+done
 
 \<comment> \<open>some helper lemmas for the pt_perm_supp_ineq lemma\<close>
 lemma Collect_permI: 
@@ -1371,7 +1459,14 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)"
-  by (rule pt_perm_supp_ineq) (auto simp: assms at_pt_inst cp_pt_inst)
+apply(rule pt_perm_supp_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
 
 lemma pt_supp_finite_pi:
   fixes  pi  :: "'x prm"
@@ -1380,7 +1475,10 @@
   and     at: "at TYPE('x)"
   and     f: "finite ((supp x)::'x set)"
   shows "finite ((supp (pi\<bullet>x))::'x set)"
-  by (metis at at_pt_inst f pt pt_perm_supp pt_set_finite_ineq)
+apply(simp add: pt_perm_supp[OF pt, OF at, symmetric])
+apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at])
+apply(rule f)
+done
 
 lemma pt_fresh_left_ineq:  
   fixes  pi :: "'x prm"
@@ -1391,8 +1489,10 @@
   and     at:  "at TYPE('x)"
   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
-  using pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp] pt_set_bij1[OF ptb, OF at]
-  by (simp add: fresh_def)
+apply(simp add: fresh_def)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
+done
 
 lemma pt_fresh_right_ineq:  
   fixes  pi :: "'x prm"
@@ -1403,7 +1503,10 @@
   and     at:  "at TYPE('x)"
   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
-  by (simp add: assms pt_fresh_left_ineq)
+apply(simp add: fresh_def)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
+done
 
 lemma pt_fresh_bij_ineq:
   fixes  pi :: "'x prm"
@@ -1414,7 +1517,9 @@
   and     at:  "at TYPE('x)"
   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
-  using assms pt_bij1 pt_fresh_right_ineq by fastforce
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(simp add: pt_rev_pi[OF ptb, OF at])
+done
 
 lemma pt_fresh_left:  
   fixes  pi :: "'x prm"
@@ -1423,7 +1528,14 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
-  by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_left_ineq)
+apply(rule pt_fresh_left_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
 
 lemma pt_fresh_right:  
   fixes  pi :: "'x prm"
@@ -1432,7 +1544,14 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
-  by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_right_ineq)
+apply(rule pt_fresh_right_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
 
 lemma pt_fresh_bij:
   fixes  pi :: "'x prm"
@@ -1441,7 +1560,14 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
-  by (metis assms pt_bij1 pt_fresh_right)
+apply(rule pt_fresh_bij_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
 
 lemma pt_fresh_bij1:
   fixes  pi :: "'x prm"
@@ -1670,20 +1796,21 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
-  by (smt (verit, ccfv_threshold) assms pt_bij1 true_eqvt)
+apply(auto simp add: perm_bool perm_fun_def)
+apply(drule_tac x="pi\<bullet>x" in spec)
+apply(simp add: pt_rev_pi[OF pt, OF at])
+done
 
 lemma pt_ex_eqvt:
   fixes  pi :: "'x prm"
   and     x :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
-proof -
-  have "\<And>x. P x \<Longrightarrow> P (rev pi \<bullet> pi \<bullet> x)"
-    by (simp add: assms(1) at pt_rev_pi)
-  then show ?thesis
-    by(auto simp add: perm_bool perm_fun_def)
-qed
+  shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
+apply(auto simp add: perm_bool perm_fun_def)
+apply(rule_tac x="pi\<bullet>x" in exI) 
+apply(simp add: pt_rev_pi[OF pt, OF at])
+done
 
 lemma pt_ex1_eqvt:
   fixes  pi :: "'x prm"
@@ -1701,7 +1828,12 @@
   and     at: "at TYPE('x)"
   and     unique: "\<exists>!x. P x"
   shows "pi\<bullet>(THE(x::'a). P x) = (THE(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
-  by (smt (verit, best) assms perm_bool_def pt_rev_pi theI_unique unique)
+  apply(rule the1_equality [symmetric])
+  apply(simp add: pt_ex1_eqvt[OF pt at,symmetric])
+  apply(simp add: perm_bool unique)
+  apply(simp add: perm_bool pt_rev_pi [OF pt at])
+  apply(rule theI'[OF unique])
+  done
 
 section \<open>facts about supports\<close>
 (*==============================*)
@@ -1802,17 +1934,13 @@
   assumes  pt: "pt TYPE('a) TYPE('x)"
   and      at: "at TYPE ('x)"
   and      a: "\<forall>x\<in>X. (\<forall>(a::'x) (b::'x). a\<notin>S\<and>b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x)\<in>X)"
-shows  "S supports X"
-proof -
-  have "x \<in> X"
-    if "a \<notin> S" "b \<notin> S" and "x \<in> [(a, b)] \<bullet> X" for a b x
-    using that by (metis a assms(1) at pt_pi_rev pt_set_bij1a)
-  moreover have "x \<in> [(a, b)] \<bullet> X"
-    if "a \<notin> S" "b \<notin> S" and "x \<in> X" for a b x
-    using that by (simp add: a assms(1) at pt_set_bij1a)
-  ultimately show ?thesis
-    by (meson subsetI subset_antisym supports_def)
-qed
+  shows  "S supports X"
+using a
+apply(auto simp add: supports_def)
+apply(simp add: pt_set_bij1a[OF pt, OF at])
+apply(force simp add: pt_swap_bij[OF pt, OF at])
+apply(simp add: pt_set_bij1a[OF pt, OF at])
+done
 
 lemma supports_fresh:
   fixes S :: "'x set"
@@ -1822,7 +1950,10 @@
   and     a2: "finite S"
   and     a3: "a\<notin>S"
   shows "a\<sharp>x"
-  by (meson assms fresh_def in_mono supp_is_subset)
+proof (simp add: fresh_def)
+  have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
+  thus "a\<notin>(supp x)" using a3 by force
+qed
 
 lemma at_fin_set_supports:
   fixes X::"'x set"
@@ -1838,7 +1969,12 @@
   assumes a1:"infinite X"
   and     a2:"\<forall>b\<in>X. P(b)"
   shows "infinite {b\<in>X. P(b)}"
-  using assms rev_finite_subset by fastforce
+  using a1 a2 
+  apply auto
+  apply (subgoal_tac "infinite (X - {b\<in>X. P b})")
+  apply (simp add: set_diff_eq)
+  apply (simp add: Diff_infinite_finite)
+  done
 
 lemma at_fin_set_supp:
   fixes X::"'x set" 
@@ -2070,15 +2206,32 @@
 proof -
   have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
   show ?thesis
-  proof -
-    have "\<exists>x. (\<exists>u. x = pi \<bullet> u \<and> u \<in> X) \<and> pi \<bullet> z \<in> (pi \<bullet> f) x"
-      if "y \<in> X" and "z \<in> f y" for y z
-      using that by (metis assms at_pt_inst pt_fun_app_eq pt_set_bij)
-    moreover have "\<exists>u. x = pi \<bullet> u \<and> (\<exists>x\<in>X. u \<in> f x)"
-      if "x \<in> (pi \<bullet> f) (pi \<bullet> y)" and "y \<in> X" for x y
-      using that by (metis at at_pi_rev pt pt_fun_app_eq pt_set_bij1a pt_x)
-    ultimately show ?thesis
-      by (auto simp: perm_set_def)
+  proof (rule equalityI)
+    show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
+      apply(auto simp add: perm_set_def)
+      apply(rule_tac x="pi\<bullet>xb" in exI)
+      apply(rule conjI)
+      apply(rule_tac x="xb" in exI)
+      apply(simp)
+      apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xb) = pi\<bullet>(f xb)")(*A*)
+      apply(simp)
+      apply(rule pt_set_bij2[OF pt_x, OF at])
+      apply(assumption)
+      (*A*)
+      apply(rule sym)
+      apply(rule pt_fun_app_eq[OF pt, OF at])
+      done
+  next
+    show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
+      apply(auto simp add: perm_set_def)
+      apply(rule_tac x="(rev pi)\<bullet>x" in exI)
+      apply(rule conjI)
+      apply(simp add: pt_pi_rev[OF pt_x, OF at])
+      apply(rule_tac x="xb" in bexI)
+      apply(simp add: pt_set_bij1[OF pt_x, OF at])
+      apply(simp add: pt_fun_app_eq[OF pt, OF at])
+      apply(assumption)
+      done
   qed
 qed
 
@@ -2088,14 +2241,34 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
-  by (metis UNION_f_eqvt X_to_Un_supp_def assms pt_fun_eq pt_perm_supp)
+  apply(simp add: X_to_Un_supp_def)
+  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
+  apply(simp add: pt_perm_supp[OF pt, OF at])
+  apply(simp add: pt_pi_rev[OF pt, OF at])
+  done
 
 lemma Union_supports_set:
   fixes X::"('a set)"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
-  by (simp add: assms fresh_def pt_fresh_fresh supports_set)
+  apply(simp add: supports_def fresh_def[symmetric])
+  apply(rule allI)+
+  apply(rule impI)
+  apply(erule conjE)
+  apply(simp add: perm_set_def)
+  apply(auto)
+  apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
+  apply(simp)
+  apply(rule pt_fresh_fresh[OF pt, OF at])
+  apply(force)
+  apply(force)
+  apply(rule_tac x="x" in exI)
+  apply(simp)
+  apply(rule sym)
+  apply(rule pt_fresh_fresh[OF pt, OF at])
+  apply(force)+
+  done
 
 lemma Union_of_fin_supp_sets:
   fixes X::"('a set)"
@@ -2113,14 +2286,19 @@
   shows "(\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> supp X"
 proof -
   have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"  
-  proof (rule pt_empty_supp_fun_subset)
-    show "supp (\<lambda>a. X_to_Un_supp (a::'a set)::'x set) = ({}::'x set)"
-    by (simp add: X_to_Un_supp_eqvt at at_pt_inst pt pt_eqvt_fun2b pt_set_inst)
-  qed (use assms at_pt_inst pt_set_inst in auto)
+    apply(rule pt_empty_supp_fun_subset)
+    apply(force intro: pt_set_inst at_pt_inst pt at)+
+    apply(rule pt_eqvt_fun2b)
+    apply(force intro: pt_set_inst at_pt_inst pt at)+
+    apply(rule allI)+
+    apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
+    done
   hence "supp (\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> ((supp X)::'x set)" by (simp add: X_to_Un_supp_def)
   moreover
   have "supp (\<Union>x\<in>X. ((supp x)::'x set)) = (\<Union>x\<in>X. ((supp x)::'x set))"
-    using Union_of_fin_supp_sets at at_fin_set_supp fi fs by auto
+    apply(rule at_fin_set_supp[OF at])
+    apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
+    done
   ultimately show ?thesis by force
 qed
 
@@ -2131,15 +2309,12 @@
   and     fs: "fs TYPE('a) TYPE('x)" 
   and     fi: "finite X"
   shows "(supp X) = (\<Union>x\<in>X. ((supp x)::'x set))"
-proof (rule equalityI)
-  have "finite (\<Union> (supp ` X)::'x set)"
-    using Union_of_fin_supp_sets fi fs by blast
-  then show "(supp X::'x set) \<subseteq> \<Union> (supp ` X)"
-    by (metis Union_supports_set at pt supp_is_subset)
-next
-  show "(\<Union>x\<in>X. (supp x::'x set)) \<subseteq> supp X"
-    by (simp add: Union_included_in_supp at fi fs pt)
-qed
+apply(rule equalityI)
+apply(rule supp_is_subset)
+apply(rule Union_supports_set[OF pt, OF at])
+apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
+apply(rule Union_included_in_supp[OF pt, OF at, OF fs, OF fi])
+done
 
 lemma supp_fin_union:
   fixes X::"('a set)"
@@ -2178,7 +2353,9 @@
   and     f1: "finite X"
   and     f2: "finite Y"
   shows "a\<sharp>(X\<union>Y) = (a\<sharp>X \<and> a\<sharp>Y)"
-  by (simp add: assms fresh_def supp_fin_union)
+apply(simp add: fresh_def)
+apply(simp add: supp_fin_union[OF pt, OF at, OF fs, OF f1, OF f2])
+done
 
 lemma fresh_fin_insert:
   fixes X::"('a set)"
@@ -2189,7 +2366,9 @@
   and     fs: "fs TYPE('a) TYPE('x)" 
   and     f:  "finite X"
   shows "a\<sharp>(insert x X) = (a\<sharp>x \<and> a\<sharp>X)"
-  by (simp add: assms fresh_def supp_fin_insert)
+apply(simp add: fresh_def)
+apply(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF f])
+done
 
 lemma fresh_fin_insert1:
   fixes X::"('a set)"
@@ -2268,11 +2447,11 @@
 
 lemma fresh_star_Un_elim:
   "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
-proof
-  assume \<section>: "(S \<union> T) \<sharp>* c \<Longrightarrow> PROP C" and c: "S \<sharp>* c" "T \<sharp>* c"
-  show "PROP C"
-    using c by (intro \<section>) (metis Un_iff fresh_star_set)
-qed (auto simp: fresh_star_def)
+  apply rule
+  apply (simp_all add: fresh_star_def)
+  apply (erule meta_mp)
+  apply blast
+  done
 
 lemma fresh_star_insert_elim:
   "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
@@ -2306,22 +2485,22 @@
   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
   and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
-  unfolding fresh_star_def
-proof -
-  have "y \<sharp> x" if "\<forall>z\<in>pi \<bullet> a. z \<sharp> pi \<bullet> x" and "y \<in> a" for y
-    using that by (meson assms at pt_fresh_bij_ineq pt_set_bij2)
-  moreover have "y \<sharp> pi \<bullet> x" if "\<forall>z\<in>a. z \<sharp> x" and "y \<in> pi \<bullet> a" for y
-    using that by (simp add: assms pt_fresh_left_ineq pt_set_bij1a)
-  moreover have "y \<sharp> x"
-    if "\<forall>z\<in>set (pi \<bullet> b). z \<sharp> pi \<bullet> x" and "y \<in> set b" for y
-    using that by (metis at cp pt_fresh_bij_ineq pt_set_bij pta ptb set_eqvt)
-  moreover have "y \<sharp> pi \<bullet> x"
-    if "\<forall>z\<in>set b. z \<sharp> x" and "y \<in> set (pi \<bullet> b)" for y
-    using that by (metis at cp pt_fresh_left_ineq pt_set_bij1a pta ptb set_eqvt)
-  ultimately show "(\<forall>xa\<in>pi \<bullet> a. xa \<sharp> pi \<bullet> x) = (\<forall>xa\<in>a. xa \<sharp> x)" "(\<forall>xa\<in>set (pi \<bullet> b). xa \<sharp> pi \<bullet> x) = (\<forall>xa\<in>set b. xa \<sharp> x)"
-    by blast+
-qed
-
+apply(unfold fresh_star_def)
+apply(auto)
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(erule pt_set_bij2[OF ptb, OF at])
+apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt)
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+done
 
 lemma pt_fresh_star_bij:
   fixes  pi :: "'x prm"
@@ -2332,10 +2511,21 @@
   and     at: "at TYPE('x)"
   shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
   and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
-proof (rule pt_fresh_star_bij_ineq)
-  show "(pi \<bullet> b) \<sharp>* (pi \<bullet> x) = b \<sharp>* x"
-  by (simp add: at at_pt_inst cp_pt_inst pt pt_fresh_star_bij_ineq)
-qed (auto simp: at pt at_pt_inst cp_pt_inst)
+apply(rule pt_fresh_star_bij_ineq(1))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+apply(rule pt_fresh_star_bij_ineq(2))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
 
 lemma pt_fresh_star_eqvt:
   fixes  pi :: "'x prm"
@@ -2392,9 +2582,16 @@
   shows "pi\<bullet>x = x"
 using a
 apply(induct pi)
-  apply (simp add: assms(1) pt1)
 apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt])
-  by (metis Cons_eq_append_conv append_self_conv2 assms(1) at at_fresh fresh_def pt2 pt_fresh_fresh)
+apply(subgoal_tac "((a,b)#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x")
+apply(simp only: pt2[OF pt])
+apply(rule pt_fresh_fresh[OF pt at])
+apply(simp add: fresh_def at_supp[OF at])
+apply(blast)
+apply(simp add: fresh_def at_supp[OF at])
+apply(blast)
+apply(simp add: pt2[OF pt])
+done
 
 section \<open>Infrastructure lemmas for strong rule inductions\<close>
 (*==========================================================*)
@@ -2488,43 +2685,63 @@
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
 using c1
-apply(clarsimp simp add: cp_def)
-  by (induct_tac x) auto
+apply(simp add: cp_def)
+apply(auto)
+apply(induct_tac x)
+apply(auto)
+done
 
 lemma cp_set_inst:
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
-  using c1
-  unfolding cp_def perm_set_def
-  by (smt (verit) Collect_cong mem_Collect_eq)
-
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(auto simp add: perm_set_def)
+apply(rule_tac x="pi2\<bullet>xc" in exI)
+apply(auto)
+done
 
 lemma cp_option_inst:
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
-  using c1 unfolding cp_def by (metis none_eqvt not_None_eq some_eqvt)
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(case_tac x)
+apply(auto)
+done
 
 lemma cp_noption_inst:
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
-  using c1 unfolding cp_def
-  by (metis nnone_eqvt noption.exhaust nsome_eqvt)
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(case_tac x)
+apply(auto)
+done
 
 lemma cp_unit_inst:
   shows "cp TYPE (unit) TYPE('x) TYPE('y)"
-  by (simp add: cp_def)
+apply(simp add: cp_def)
+done
 
 lemma cp_bool_inst:
   shows "cp TYPE (bool) TYPE('x) TYPE('y)"
-  apply(clarsimp simp add: cp_def)
-  by (induct_tac x) auto
+apply(simp add: cp_def)
+apply(rule allI)+
+apply(induct_tac x)
+apply(simp_all)
+done
 
 lemma cp_prod_inst:
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
   shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
 using c1 c2
-  by (simp add: cp_def)
+apply(simp add: cp_def)
+done
 
 lemma cp_fun_inst:
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
@@ -2532,8 +2749,11 @@
   and     pt: "pt TYPE ('y) TYPE('x)"
   and     at: "at TYPE ('x)"
   shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
-  using c1 c2
-  by(auto simp add: cp_def perm_fun_def fun_eq_iff at pt pt_list_inst pt_prod_inst pt_rev_pi rev_eqvt)
+using c1 c2
+apply(auto simp add: cp_def perm_fun_def fun_eq_iff)
+apply(simp add: rev_eqvt[symmetric])
+apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
+done
 
 
 section \<open>Andy's freshness lemma\<close>
@@ -2636,7 +2856,9 @@
   and     f1: "finite ((supp h)::'x set)"
   and     a: "a\<sharp>h" "a\<sharp>h a"
   shows "(fresh_fun h) = (h a)"
-  by (meson assms fresh_fun_app fresh_prod pt)
+apply(rule fresh_fun_app[OF pt, OF at, OF f1])
+apply(auto simp add: fresh_prod intro: a)
+done
 
 lemma fresh_fun_equiv_ineq:
   fixes h :: "'y\<Rightarrow>'a"
@@ -2716,7 +2938,11 @@
   and     f1: "finite ((supp h)::'x set)"
   and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
   shows "((supp h)::'x set) supports (fresh_fun h)"
-  by(simp flip: fresh_def add: supports_def assms at_pt_inst fresh_fun_equiv pt_fresh_fresh pt_fun_inst)
+  apply(simp add: supports_def fresh_def[symmetric])
+  apply(auto)
+  apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a])
+  apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
+  done
   
 section \<open>Abstraction function\<close>
 (*==============================*)
@@ -2725,7 +2951,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)"
-  by (simp add: at at_pt_inst pt pt_fun_inst pt_noption_inst)
+  by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at])
 
 definition abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" (\<open>[_]._\<close> [100,100] 100) where 
   "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))"
@@ -2747,22 +2973,26 @@
   and     ptb: "pt TYPE('y) TYPE('x)"
   and     at:  "at TYPE('x)"
   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
-shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
-  unfolding fun_eq_iff
-proof
-  fix y
-  have "(((rev pi)\<bullet>y) = a) = (y = pi\<bullet>a)"
-    by (metis at pt_rev_pi ptb)
-  moreover
-  have "(((rev pi)\<bullet>y)\<sharp>x) = (y\<sharp>(pi\<bullet>x))"
-    by (simp add: assms pt_fresh_left_ineq)
-  moreover
-  have "pi\<bullet>([(a,(rev pi)\<bullet>y)]\<bullet>x) = [(pi\<bullet>a,y)]\<bullet>(pi\<bullet>x)"
-    using assms cp1[OF cp] by (simp add: pt_pi_rev)
-  ultimately
-  show "(pi \<bullet> [a].x) y = ([(pi \<bullet> a)].(pi \<bullet> x)) y"
-    by (simp add: abs_fun_def perm_fun_def)
-qed
+  shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
+  apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
+  apply(simp only: fun_eq_iff)
+  apply(rule allI)
+  apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
+  apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*)
+  apply(subgoal_tac "pi\<bullet>([(a,(rev pi)\<bullet>xa)]\<bullet>x) = [(pi\<bullet>a,xa)]\<bullet>(pi\<bullet>x)")(*C*)
+  apply(simp)
+(*C*)
+  apply(simp add: cp1[OF cp])
+  apply(simp add: pt_pi_rev[OF ptb, OF at])
+(*B*)
+  apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+(*A*)
+  apply(rule iffI)
+  apply(rule pt_bij2[OF ptb, OF at, THEN sym])
+  apply(simp)
+  apply(rule pt_bij2[OF ptb, OF at])
+  apply(simp)
+done
 
 lemma abs_fun_pi:
   fixes a  :: "'x"
@@ -2771,14 +3001,25 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
-  by (simp add: abs_fun_pi_ineq at at_pt_inst cp_pt_inst pt)
+apply(rule abs_fun_pi_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
 
 lemma abs_fun_eq1: 
   fixes x  :: "'a"
   and   y  :: "'a"
   and   a  :: "'x"
   shows "([a].x = [a].y) = (x = y)"
-  by (metis abs_fun_def noption.inject)
+apply(auto simp add: abs_fun_def)
+apply(auto simp add: fun_eq_iff)
+apply(drule_tac x="a" in spec)
+apply(simp)
+done
 
 lemma abs_fun_eq2:
   fixes x  :: "'a"
@@ -2969,7 +3210,10 @@
       and as: "[a].x = [b].y"
       and fr: "c\<noteq>a" "c\<noteq>b" "c\<sharp>x" "c\<sharp>y" 
   shows "x = [(a,c)]\<bullet>[(b,c)]\<bullet>y"
-  using assms by (metis abs_fun_fresh pt_swap_bij)
+using as fr
+apply(drule_tac sym)
+apply(simp add: abs_fun_fresh[OF pt, OF at] pt_swap_bij[OF pt, OF at])
+done
 
 lemma abs_fun_supp_approx:
   fixes x :: "'a"
@@ -3115,10 +3359,12 @@
   and     at:  "at TYPE('x)"
   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   and     dj:  "disjoint TYPE('y) TYPE('x)"
-shows "((supp ([a].x))::'x set) = (supp x)"
-unfolding supp_def
-  using abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj]
-  by (smt (verit, ccfv_threshold) Collect_cong abs_fun_eq1)
+  shows "((supp ([a].x))::'x set) = (supp x)"
+apply(auto simp add: supp_def)
+apply(auto simp add: abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(auto simp add: dj_perm_forget[OF dj])
+apply(auto simp add: abs_fun_eq1) 
+done
 
 lemma fresh_abs_fun_iff_ineq: 
   fixes a :: "'y"
@@ -3207,7 +3453,17 @@
   have pt_prm: "pt TYPE('x prm) TYPE('x)" 
     by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]])  
   from a show ?thesis
-    by (auto simp add: prm_eq_def at pt pt_perm_compose')
+    apply -
+    apply(auto simp add: prm_eq_def)
+    apply(rule_tac pi="rev pi3" in pt_bij4[OF pt, OF at])
+    apply(rule trans)
+    apply(rule pt_perm_compose[OF pt, OF at])
+    apply(simp add: pt_rev_pi[OF pt_prm, OF at])
+    apply(rule sym)
+    apply(rule trans)
+    apply(rule pt_perm_compose[OF pt, OF at])
+    apply(simp add: pt_rev_pi[OF pt_prm, OF at])
+    done
 qed
 
 (************************)
@@ -3268,32 +3524,32 @@
 by (simp add: perm_int_def)
 
 lemma numeral_int_eqvt: 
- shows "pi\<bullet>((numeral n)::int) = numeral n"
-  using perm_int_def by blast 
+ shows "pi\<bullet>((numeral n)::int) = numeral n" 
+by (simp add: perm_int_def perm_int_def)
 
 lemma neg_numeral_int_eqvt:
-  shows "pi\<bullet>((- numeral n)::int) = - numeral n"
-  by (simp add: perm_int_def)
+ shows "pi\<bullet>((- numeral n)::int) = - numeral n"
+by (simp add: perm_int_def perm_int_def)
 
 lemma max_int_eqvt:
   fixes x::"int"
   shows "pi\<bullet>(max (x::int) y) = max (pi\<bullet>x) (pi\<bullet>y)" 
-  by (simp add:perm_int_def) 
+by (simp add:perm_int_def) 
 
 lemma min_int_eqvt:
   fixes x::"int"
   shows "pi\<bullet>(min x y) = min (pi\<bullet>x) (pi\<bullet>y)" 
-  by (simp add:perm_int_def) 
+by (simp add:perm_int_def) 
 
 lemma plus_int_eqvt:
   fixes x::"int"
   shows "pi\<bullet>(x + y) = (pi\<bullet>x) + (pi\<bullet>y)" 
-  by (simp add:perm_int_def) 
+by (simp add:perm_int_def) 
 
 lemma minus_int_eqvt:
   fixes x::"int"
   shows "pi\<bullet>(x - y) = (pi\<bullet>x) - (pi\<bullet>y)" 
-  by (simp add:perm_int_def) 
+by (simp add:perm_int_def) 
 
 lemma mult_int_eqvt:
   fixes x::"int"
@@ -3303,7 +3559,7 @@
 lemma div_int_eqvt:
   fixes x::"int"
   shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)" 
-  by (simp add:perm_int_def) 
+by (simp add:perm_int_def) 
 
 (*******************************************************)
 (* Setup of the theorem attributes eqvt and eqvt_force *)