# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1713820108 -3600
# Node ID 34e0ddfc6dcccaff7d3c9e9b9ff28d02f71e3ace
# Parent  022a9c26b14fc78552ab1cc08cdca5e7894430ac
More tidying of Nominal proofs

diff -r 022a9c26b14f -r 34e0ddfc6dcc src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Apr 22 10:43:57 2024 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Apr 22 22:08:28 2024 +0100
@@ -145,7 +145,7 @@
 lemma finite_doms:
   shows "finite (ty_dom \<Gamma>)"
   and   "finite (trm_dom \<Gamma>)"
-by (induct \<Gamma>) (auto simp add: finite_vrs)
+by (induct \<Gamma>) (auto simp: finite_vrs)
 
 lemma ty_dom_supp:
   shows "(supp (ty_dom  \<Gamma>)) = (ty_dom  \<Gamma>)"
@@ -167,12 +167,12 @@
   assumes a: "X\<in>(ty_dom \<Gamma>)" 
   shows "\<exists>T.(TVarB X T)\<in>set \<Gamma>"
   using a 
-  apply (induct \<Gamma>, auto)
-  apply (rename_tac a \<Gamma>') 
-  apply (subgoal_tac "\<exists>T.(TVarB X T=a)")
-  apply (auto)
-  apply (auto simp add: ty_binding_existence)
-done
+proof (induction \<Gamma>)
+  case Nil then show ?case by simp
+next
+  case (Cons a \<Gamma>) then show ?case
+    using ty_binding_existence by fastforce
+qed
 
 lemma doms_append:
   shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
@@ -183,18 +183,19 @@
   fixes pi::"vrs prm"
   and   S::"ty"
   shows "pi\<bullet>S = S"
-by (induct S rule: ty.induct) (auto simp add: calc_atm)
+by (induct S rule: ty.induct) (auto simp: calc_atm)
 
 lemma fresh_ty_dom_cons:
   fixes X::"tyvrs"
   shows "X\<sharp>(ty_dom (Y#\<Gamma>)) = (X\<sharp>(tyvrs_of Y) \<and> X\<sharp>(ty_dom \<Gamma>))"
-  apply (nominal_induct rule:binding.strong_induct)
-  apply (auto)
-  apply (simp add: fresh_def supp_def eqvts)
-  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
-  apply (simp add: fresh_def supp_def eqvts)
-  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)+
-  done
+proof (nominal_induct rule:binding.strong_induct)
+  case (VarB vrs ty)
+  then show ?case by auto
+next
+  case (TVarB tyvrs ty)
+  then show ?case
+    by (simp add: at_fin_set_supp at_tyvrs_inst finite_doms(1) fresh_def supp_atm(1))
+qed
 
 lemma tyvrs_fresh:
   fixes   X::"tyvrs"
@@ -202,21 +203,19 @@
   shows   "X \<sharp> tyvrs_of a"
   and     "X \<sharp> vrs_of a"
   using assms
-  apply (nominal_induct a rule:binding.strong_induct)
-  apply (auto)
-  apply (fresh_guess)+
-done
+  by (nominal_induct a rule:binding.strong_induct) (force simp: fresh_singleton)+
 
 lemma fresh_dom:
   fixes X::"tyvrs"
   assumes a: "X\<sharp>\<Gamma>" 
   shows "X\<sharp>(ty_dom \<Gamma>)"
 using a
-apply(induct \<Gamma>)
-apply(simp add: fresh_set_empty) 
-apply(simp only: fresh_ty_dom_cons)
-apply(auto simp add: fresh_prod fresh_list_cons tyvrs_fresh) 
-done
+proof (induct \<Gamma>)
+  case Nil then show ?case by auto
+next
+  case (Cons a \<Gamma>) then show ?case
+    by (meson fresh_list_cons fresh_ty_dom_cons tyvrs_fresh(1))
+qed
 
 text \<open>Not all lists of type \<^typ>\<open>env\<close> are well-formed. One condition
   requires that in \<^term>\<open>TVarB X S#\<Gamma>\<close> all free variables of \<^term>\<open>S\<close> must be 
@@ -240,10 +239,7 @@
 lemma tyvrs_vrs_prm_simp:
   fixes pi::"vrs prm"
   shows "tyvrs_of (pi\<bullet>a) = tyvrs_of a"
-  apply (nominal_induct rule:binding.strong_induct) 
-  apply (simp_all add: eqvts)
-  apply (simp add: dj_perm_forget[OF dj_tyvrs_vrs])
-  done
+  by (nominal_induct rule:binding.strong_induct) (auto simp: vrs_prm_tyvrs_def)
 
 lemma ty_vrs_fresh:
   fixes x::"vrs"
@@ -255,17 +251,13 @@
   fixes pi::"vrs prm"
   and   \<Gamma>::"env"
   shows "(ty_dom (pi\<bullet>\<Gamma>)) = (ty_dom \<Gamma>)"
-  apply(induct \<Gamma>) 
-  apply (simp add: eqvts)
-  apply(simp add:  tyvrs_vrs_prm_simp)
-done
+by (induct \<Gamma>) (auto simp: tyvrs_vrs_prm_simp)
 
 lemma closed_in_eqvt'[eqvt]:
   fixes pi::"vrs prm"
   assumes a: "S closed_in \<Gamma>" 
   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
-using a
-by (simp add: closed_in_def ty_dom_vrs_prm_simp  ty_vrs_prm_simp)
+  using assms closed_in_def ty_dom_vrs_prm_simp ty_vrs_prm_simp by force
 
 lemma fresh_vrs_of: 
   fixes x::"vrs"
@@ -277,12 +269,12 @@
   fixes x::"vrs"
   shows "x\<sharp> trm_dom \<Gamma> = x\<sharp>\<Gamma>"
   by (induct \<Gamma>)
-    (simp_all add: fresh_set_empty fresh_list_cons
+    (simp_all add: fresh_list_cons
      fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
-     finite_doms finite_vrs fresh_vrs_of fresh_list_nil)
+     finite_doms finite_vrs fresh_vrs_of)
 
 lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_dom \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T"
-  by (auto simp add: closed_in_def fresh_def ty_dom_supp)
+  by (auto simp: closed_in_def fresh_def ty_dom_supp)
 
 text \<open>Now validity of a context is a straightforward inductive definition.\<close>
   
@@ -313,8 +305,7 @@
 proof (induct \<Delta>)
   case (Cons a \<Gamma>')
   then show ?case 
-    by (nominal_induct a rule:binding.strong_induct)
-       (auto elim: validE)
+    by (nominal_induct a rule:binding.strong_induct) auto
 qed (auto)
 
 lemma replace_type:
@@ -324,12 +315,12 @@
 using a b
 proof(induct \<Delta>)
   case Nil
-  then show ?case by (auto elim: validE intro: valid_cons simp add: doms_append closed_in_def)
+  then show ?case by (auto intro: valid_cons simp add: doms_append closed_in_def)
 next
   case (Cons a \<Gamma>')
   then show ?case 
     by (nominal_induct a rule:binding.strong_induct)
-       (auto elim: validE intro!: valid_cons simp add: doms_append closed_in_def)
+       (auto intro!: valid_cons simp add: doms_append closed_in_def)
 qed
 
 text \<open>Well-formed contexts have a unique type-binding for a type-variable.\<close> 
@@ -353,10 +344,10 @@
         by (simp add:  fresh_ty_dom_cons 
                        fresh_fin_union[OF pt_tyvrs_inst  at_tyvrs_inst fs_tyvrs_inst]  
                        finite_vrs finite_doms, 
-            auto simp add: fresh_atm fresh_singleton)
+            auto simp: fresh_atm fresh_singleton)
     qed (simp)
   }
-  ultimately show "T=S" by (auto simp add: binding.inject)
+  ultimately show "T=S" by (auto simp: binding.inject)
 qed (auto)
 
 lemma uniqueness_of_ctxt':
@@ -377,10 +368,10 @@
       thus "\<not> (\<exists>T.(VarB x' T)\<in>set(y#\<Gamma>'))" 
         by (simp add:  fresh_fin_union[OF pt_vrs_inst  at_vrs_inst fs_vrs_inst]  
                        finite_vrs finite_doms, 
-            auto simp add: fresh_atm fresh_singleton)
+            auto simp: fresh_atm fresh_singleton)
     qed (simp)
   }
-  ultimately show "T=S" by (auto simp add: binding.inject)
+  ultimately show "T=S" by (auto simp: binding.inject)
 qed (auto)
 
 section \<open>Size and Capture-Avoiding Substitution for Types\<close>
@@ -392,11 +383,7 @@
 | "size_ty (Top) = 1"
 | "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
 | "X \<sharp> T1 \<Longrightarrow> size_ty (\<forall>X<:T1. T2) = (size_ty T1) + (size_ty T2) + 1"
-  apply (finite_guess)+
-  apply (rule TrueI)+
-  apply (simp add: fresh_nat)
-  apply (fresh_guess)+
-  done
+  by (finite_guess | fresh_guess | simp)+
 
 nominal_primrec
   subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_ \<mapsto> _]\<^sub>\<tau>" [300, 0, 0] 300)
@@ -405,11 +392,7 @@
 | "(Top)[Y \<mapsto> T]\<^sub>\<tau> = Top"
 | "(T\<^sub>1 \<rightarrow> T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau> \<rightarrow> T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>"
 | "X\<sharp>(Y,T,T\<^sub>1) \<Longrightarrow> (\<forall>X<:T\<^sub>1. T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>)"
-  apply (finite_guess)+
-  apply (rule TrueI)+
-  apply (simp add: abs_fresh)
-  apply (fresh_guess)+
-  done
+  by (finite_guess | fresh_guess | simp add: abs_fresh)+
 
 lemma subst_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 
@@ -429,16 +412,16 @@
   fixes X::"tyvrs"
   assumes "X\<sharp>T" and "X\<sharp>P"
   shows   "X\<sharp>T[Y \<mapsto> P]\<^sub>\<tau>"
-using assms
-by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
-   (auto simp add: abs_fresh)
+  using assms
+  by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
+    (auto simp: abs_fresh)
 
 lemma fresh_type_subst_fresh:
-    assumes "X\<sharp>T'"
-    shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>"
-using assms 
-by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
-   (auto simp add: fresh_atm abs_fresh fresh_nat) 
+  assumes "X\<sharp>T'"
+  shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>"
+  using assms 
+  by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
+     (auto simp: fresh_atm abs_fresh) 
 
 lemma type_subst_identity: 
   "X\<sharp>T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T"
@@ -448,7 +431,7 @@
 lemma type_substitution_lemma:  
   "X \<noteq> Y \<Longrightarrow> X\<sharp>L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
   by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct)
-    (auto simp add: type_subst_fresh type_subst_identity)
+    (auto simp: type_subst_fresh type_subst_identity)
 
 lemma type_subst_rename:
   "Y\<sharp>T \<Longrightarrow> ([(Y,X)]\<bullet>T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>"
@@ -469,7 +452,7 @@
   shows "X\<sharp>a[Y \<mapsto> P]\<^sub>b"
 using assms
 by (nominal_induct a rule: binding.strong_induct)
-   (auto simp add: type_subst_fresh)
+   (auto simp: type_subst_fresh)
 
 lemma binding_subst_identity: 
   shows "X\<sharp>B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
@@ -487,7 +470,7 @@
   shows   "X\<sharp>\<Gamma>[Y \<mapsto> P]\<^sub>e"
 using assms
 by (induct \<Gamma>)
-   (auto simp add: fresh_list_cons binding_subst_fresh)
+   (auto simp: fresh_list_cons binding_subst_fresh)
 
 lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
@@ -519,7 +502,7 @@
   fixes X::"tyvrs"
   shows "X\<sharp>t \<Longrightarrow> X\<sharp>u \<Longrightarrow> X\<sharp>t[x \<mapsto> u]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
-    (auto simp add: trm.fresh abs_fresh)
+    (auto simp: abs_fresh)
 
 lemma subst_trm_fresh_var: 
   "x\<sharp>u \<Longrightarrow> x\<sharp>t[x \<mapsto> u]"
@@ -553,10 +536,7 @@
 | "(t1 \<cdot>\<^sub>\<tau> T)[Y \<mapsto>\<^sub>\<tau> T2] = t1[Y \<mapsto>\<^sub>\<tau> T2] \<cdot>\<^sub>\<tau> T[Y \<mapsto> T2]\<^sub>\<tau>"
 | "X\<sharp>(Y,T,T2) \<Longrightarrow> (\<lambda>X<:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>X<:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])" 
 | "(\<lambda>x:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>x:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh ty_vrs_fresh)+
-apply(simp add: type_subst_fresh)
+apply(finite_guess | simp add: abs_fresh ty_vrs_fresh type_subst_fresh)+
 apply(fresh_guess add: ty_vrs_fresh abs_fresh)+
 done
 
@@ -564,7 +544,7 @@
   fixes X::"tyvrs"
   shows "X\<sharp>t \<Longrightarrow> X\<sharp>T \<Longrightarrow> X\<sharp>t[Y \<mapsto>\<^sub>\<tau> T]"
   by (nominal_induct t avoiding: Y T rule: trm.strong_induct)
-    (auto simp add: abs_fresh type_subst_fresh)
+    (auto simp: abs_fresh type_subst_fresh)
 
 lemma subst_trm_ty_fresh':
   "X\<sharp>T \<Longrightarrow> X\<sharp>t[X \<mapsto>\<^sub>\<tau> T]"
@@ -633,7 +613,7 @@
   have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact
   hence "T closed_in \<Gamma>" by force
   ultimately show "(Tvar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp
-qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp)
+qed (auto simp: closed_in_def ty.supp supp_atm abs_supp)
 
 lemma subtype_implies_fresh:
   fixes X::"tyvrs"
@@ -647,7 +627,7 @@
   from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed)
   hence "supp S \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" 
     and "supp T \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def)
-  ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
+  ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp: supp_prod fresh_def)
 qed
 
 lemma valid_ty_dom_fresh:
@@ -655,19 +635,26 @@
   assumes valid: "\<turnstile> \<Gamma> ok"
   shows "X\<sharp>(ty_dom \<Gamma>) = X\<sharp>\<Gamma>" 
   using valid
-  apply induct
-  apply (simp add: fresh_list_nil fresh_set_empty)
-  apply (simp_all add: binding.fresh fresh_list_cons
-     fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms fresh_atm)
-  apply (auto simp add: closed_in_fresh)
-  done
+proof induct
+  case valid_nil
+  then show ?case by auto
+next
+  case (valid_consT \<Gamma> X T)
+  then show ?case
+    by (auto simp: fresh_list_cons closed_in_fresh
+     fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
+next
+  case (valid_cons \<Gamma> x T)
+  then show ?case
+    using fresh_atm by (auto simp: fresh_list_cons closed_in_fresh)
+qed
 
 equivariance subtype_of
 
 nominal_inductive subtype_of
   apply (simp_all add: abs_fresh)
-  apply (fastforce simp add: valid_ty_dom_fresh dest: subtype_implies_ok)
-  apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+
+  apply (fastforce simp: valid_ty_dom_fresh dest: subtype_implies_ok)
+  apply (force simp: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+
   done
 
 section \<open>Reflexivity of Subtyping\<close>
@@ -685,7 +672,7 @@
   hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom)
   have "(\<forall>X<:T\<^sub>2. T\<^sub>1) closed_in \<Gamma>" by fact
   hence closed\<^sub>T2: "T\<^sub>2 closed_in \<Gamma>" and closed\<^sub>T1: "T\<^sub>1 closed_in ((TVarB  X T\<^sub>2)#\<Gamma>)" 
-    by (auto simp add: closed_in_def ty.supp abs_supp)
+    by (auto simp: closed_in_def ty.supp abs_supp)
   have ok: "\<turnstile> \<Gamma> ok" by fact  
   hence ok': "\<turnstile> ((TVarB X T\<^sub>2)#\<Gamma>) ok" using closed\<^sub>T2 fresh_ty_dom by simp
   have "\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>2" using ih_T\<^sub>2 closed\<^sub>T2 ok by simp
@@ -693,7 +680,7 @@
   have "((TVarB X T\<^sub>2)#\<Gamma>) \<turnstile> T\<^sub>1 <: T\<^sub>1" using ih_T\<^sub>1 closed\<^sub>T1 ok' by simp
   ultimately show "\<Gamma> \<turnstile> (\<forall>X<:T\<^sub>2. T\<^sub>1) <: (\<forall>X<:T\<^sub>2. T\<^sub>1)" using fresh_cond 
     by (simp add: subtype_of.SA_all)
-qed (auto simp add: closed_in_def ty.supp supp_atm)
+qed (auto simp: closed_in_def ty.supp supp_atm)
 
 lemma subtype_reflexivity_semiautomated:
   assumes a: "\<turnstile> \<Gamma> ok"
@@ -701,7 +688,7 @@
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
 apply(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
-apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def)
+apply(auto simp: ty.supp abs_supp supp_atm closed_in_def)
   \<comment> \<open>Too bad that this instantiation cannot be found automatically by
   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
   an explicit definition for \<open>closed_in_def\<close>.\<close>
@@ -719,20 +706,15 @@
   "\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (TVarB X Q)\<in>set \<Gamma> \<longrightarrow> (TVarB X Q)\<in>set \<Delta>"
 
 lemma extends_ty_dom:
-  assumes a: "\<Delta> extends \<Gamma>"
+  assumes "\<Delta> extends \<Gamma>"
   shows "ty_dom \<Gamma> \<subseteq> ty_dom \<Delta>"
-  using a 
-  apply (auto simp add: extends_def)
-  apply (drule ty_dom_existence)
-  apply (force simp add: ty_dom_inclusion)
-  done
+  using assms
+  by (meson extends_def subsetI ty_dom_existence ty_dom_inclusion) 
 
 lemma extends_closed:
-  assumes a1: "T closed_in \<Gamma>"
-  and     a2: "\<Delta> extends \<Gamma>"
+  assumes "T closed_in \<Gamma>" and "\<Delta> extends \<Gamma>"
   shows "T closed_in \<Delta>"
-  using a1 a2
-  by (auto dest: extends_ty_dom simp add: closed_in_def)
+  by (meson assms closed_in_def extends_ty_dom order.trans)
 
 lemma extends_memb:
   assumes a: "\<Delta> extends \<Gamma>"
@@ -787,7 +769,7 @@
   have "T\<^sub>1 closed_in \<Delta>" using ext closed\<^sub>T1 by (simp only: extends_closed)
   hence "\<turnstile> ((TVarB X T\<^sub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover 
-  have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
+  have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp: extends_def)
   ultimately have "((TVarB X T\<^sub>1)#\<Delta>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp
   moreover
   have "\<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp 
@@ -815,7 +797,7 @@
   have "T\<^sub>1 closed_in \<Delta>" using ext closed\<^sub>T1 by (simp only: extends_closed)
   hence "\<turnstile> ((TVarB X T\<^sub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover
-  have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
+  have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp: extends_def)
   ultimately have "((TVarB X T\<^sub>1)#\<Delta>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp
   moreover
   have "\<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp 
@@ -836,9 +818,8 @@
 lemma S_ForallE_left:
   shows "\<lbrakk>\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^sub>1; X\<sharp>T\<rbrakk>
          \<Longrightarrow> T = Top \<or> (\<exists>T\<^sub>1 T\<^sub>2. T = (\<forall>X<:T\<^sub>1. T\<^sub>2) \<and> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 \<and> ((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2)"
-apply(erule subtype_of.strong_cases[where X="X"])
-apply(auto simp add: abs_fresh ty.inject alpha)
-done
+  using subtype_of.strong_cases[where X="X"]
+  by(force simp: abs_fresh ty.inject alpha)
 
 text \<open>Next we prove the transitivity and narrowing for the subtyping-relation. 
 The POPLmark-paper says the following:
@@ -942,7 +923,7 @@
       moreover
       have "S\<^sub>1 closed_in \<Gamma>" and "S\<^sub>2 closed_in ((TVarB X Q\<^sub>1)#\<Gamma>)" 
         using lh_drv_prm\<^sub>1 lh_drv_prm\<^sub>2 by (simp_all add: subtype_implies_closed)
-      then have "(\<forall>X<:S\<^sub>1. S\<^sub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
+      then have "(\<forall>X<:S\<^sub>1. S\<^sub>2) closed_in \<Gamma>" by (force simp: closed_in_def ty.supp abs_supp)
       moreover
       have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
       moreover
@@ -1060,7 +1041,7 @@
     by (rule exists_fresh) (rule fin_supp)
   then have "Y \<sharp> (\<Gamma>, t\<^sub>1, T2)" by simp
   moreover from Y have "(\<forall>X<:T11. T12) = (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)"
-    by (auto simp add: ty.inject alpha' fresh_prod fresh_atm)
+    by (auto simp: ty.inject alpha' fresh_prod fresh_atm)
   with H1 have "\<Gamma> \<turnstile> t\<^sub>1 : (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)" by simp
   ultimately have "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (([(Y, X)] \<bullet> T12)[Y \<mapsto> T2]\<^sub>\<tau>)" using H2
     by (rule T_TApp)
@@ -1079,7 +1060,7 @@
 lemma ok_imp_VarB_closed_in:
   assumes ok: "\<turnstile> \<Gamma> ok"
   shows "VarB x T \<in> set \<Gamma> \<Longrightarrow> T closed_in \<Gamma>" using ok
-  by induct (auto simp add: binding.inject closed_in_def)
+  by induct (auto simp: binding.inject closed_in_def)
 
 lemma tyvrs_of_subst: "tyvrs_of (B[X \<mapsto> T]\<^sub>b) = tyvrs_of B"
   by (nominal_induct B rule: binding.strong_induct) simp_all
@@ -1095,18 +1076,26 @@
 
 lemma subst_closed_in:
   "T closed_in (\<Delta> @ TVarB X S # \<Gamma>) \<Longrightarrow> U closed_in \<Gamma> \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> closed_in (\<Delta>[X \<mapsto> U]\<^sub>e @ \<Gamma>)"
-  apply (nominal_induct T avoiding: X U \<Gamma> rule: ty.strong_induct)
-  apply (simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst)
-  apply blast
-  apply (simp add: closed_in_def ty.supp)
-  apply (simp add: closed_in_def ty.supp)
-  apply (simp add: closed_in_def ty.supp abs_supp)
-  apply (drule_tac x = X in meta_spec)
-  apply (drule_tac x = U in meta_spec)
-  apply (drule_tac x = "(TVarB tyvrs ty2) # \<Gamma>" in meta_spec)
-  apply (simp add: doms_append ty_dom_subst)
-  apply blast
-  done
+proof (nominal_induct T avoiding: X U \<Gamma> rule: ty.strong_induct)
+  case (Tvar tyvrs)
+  then show ?case
+    by (auto simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst)
+next
+  case Top
+  then show ?case
+    using closed_in_def fresh_def by fastforce
+next
+  case (Arrow ty1 ty2)
+  then show ?case
+    by (simp add: closed_in_def ty.supp)
+next
+  case (Forall tyvrs ty1 ty2)
+  then have "supp (ty1[X \<mapsto> U]\<^sub>\<tau>) \<subseteq> ty_dom (\<Delta>[X \<mapsto> U]\<^sub>e @ TVarB tyvrs ty2 # \<Gamma>)"
+    apply (simp add: closed_in_def ty.supp abs_supp)
+    by (metis Diff_subset_conv Un_left_commute doms_append(1) le_supI2 ty_dom.simps(2) tyvrs_of.simps(2))
+  with Forall show ?case
+    by (auto simp add: closed_in_def ty.supp abs_supp doms_append)
+qed
 
 lemmas subst_closed_in' = subst_closed_in [where \<Delta>="[]", simplified]
 
@@ -1120,12 +1109,12 @@
   show ?case by (rule ok_imp_VarB_closed_in)
 next
   case (T_App \<Gamma> t\<^sub>1 T\<^sub>1 T\<^sub>2 t\<^sub>2)
-  then show ?case by (auto simp add: ty.supp closed_in_def)
+  then show ?case by (auto simp: ty.supp closed_in_def)
 next
   case (T_Abs x T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   from \<open>VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok)
-  with T_Abs show ?case by (auto simp add: ty.supp closed_in_def)
+  with T_Abs show ?case by (auto simp: ty.supp closed_in_def)
 next
   case (T_Sub \<Gamma> t S T)
   from \<open>\<Gamma> \<turnstile> S <: T\<close> show ?case by (simp add: subtype_implies_closed)
@@ -1133,11 +1122,11 @@
   case (T_TAbs X T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   from \<open>TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok)
-  with T_TAbs show ?case by (auto simp add: ty.supp closed_in_def abs_supp)
+  with T_TAbs show ?case by (auto simp: ty.supp closed_in_def abs_supp)
 next
   case (T_TApp X \<Gamma> t\<^sub>1 T2 T11 T12)
   then have "T12 closed_in (TVarB X T11 # \<Gamma>)"
-    by (auto simp add: closed_in_def ty.supp abs_supp)
+    by (auto simp: closed_in_def ty.supp abs_supp)
   moreover from T_TApp have "T2 closed_in \<Gamma>"
     by (simp add: subtype_implies_closed)
   ultimately show ?case by (rule subst_closed_in')
@@ -1177,7 +1166,7 @@
   then have "(\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]" using H
     by (rule E_Abs)
   moreover from y have "(\<lambda>x:T11. t12) \<cdot> v2 = (\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2"
-    by (auto simp add: trm.inject alpha' fresh_prod fresh_atm)
+    by (auto simp: trm.inject alpha' fresh_prod fresh_atm)
   ultimately have "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]"
     by simp
   with y show ?thesis by (simp add: subst_trm_rename)
@@ -1190,7 +1179,7 @@
   then have "(\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]"
     by (rule E_TAbs)
   moreover from Y have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 = (\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2"
-    by (auto simp add: trm.inject alpha' fresh_prod fresh_atm)
+    by (auto simp: trm.inject alpha' fresh_prod fresh_atm)
   ultimately have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]"
     by simp
   with Y show ?thesis by (simp add: subst_trm_ty_rename)
@@ -1217,42 +1206,33 @@
 using assms ty_dom_cons closed_in_def by auto
 
 lemma closed_in_weaken: "T closed_in (\<Delta> @ \<Gamma>) \<Longrightarrow> T closed_in (\<Delta> @ B # \<Gamma>)"
-  by (auto simp add: closed_in_def doms_append)
+  by (auto simp: closed_in_def doms_append)
 
 lemma closed_in_weaken': "T closed_in \<Gamma> \<Longrightarrow> T closed_in (\<Delta> @ \<Gamma>)"
-  by (auto simp add: closed_in_def doms_append)
+  by (auto simp: closed_in_def doms_append)
 
 lemma valid_subst:
   assumes ok: "\<turnstile> (\<Delta> @ TVarB X Q # \<Gamma>) ok"
   and closed: "P closed_in \<Gamma>"
   shows "\<turnstile> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using ok closed
-  apply (induct \<Delta>)
-  apply simp_all
-  apply (erule validE)
-  apply assumption
-  apply (erule validE)
-  apply simp
-  apply (rule valid_consT)
-  apply assumption
-  apply (simp add: doms_append ty_dom_subst)
-  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
-  apply (rule_tac S=Q in subst_closed_in')
-  apply (simp add: closed_in_def doms_append ty_dom_subst)
-  apply (simp add: closed_in_def doms_append)
-  apply blast
-  apply simp
-  apply (rule valid_cons)
-  apply assumption
-  apply (simp add: doms_append trm_dom_subst)
-  apply (rule_tac S=Q in subst_closed_in')
-  apply (simp add: closed_in_def doms_append ty_dom_subst)
-  apply (simp add: closed_in_def doms_append)
-  apply blast
-  done
+proof (induct \<Delta>)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a \<Delta>)
+  then have *: "\<turnstile> (a # \<Delta> @ TVarB X Q # \<Gamma>) ok"
+    by fastforce
+  then show ?case
+    apply (rule validE)
+    using Cons
+     apply (simp add: at_tyvrs_inst closed doms_append(1) finite_doms(1) fresh_fin_insert fs_tyvrs_inst pt_tyvrs_inst subst_closed_in ty_dom_subst)
+    by (simp add: doms_append(2) subst_closed_in Cons.hyps closed trm_dom_subst)
+qed
 
 lemma ty_dom_vrs:
   shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
-by (induct G) (auto)
+  by (induct G) (auto)
 
 lemma valid_cons':
   assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
@@ -1321,15 +1301,7 @@
   then have closed: "T\<^sub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
   have "\<turnstile> (VarB y T\<^sub>1 # \<Delta> @ B # \<Gamma>) ok"
-    apply (rule valid_cons)
-    apply (rule T_Abs)
-    apply (simp add: doms_append
-      fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
-      fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
-      finite_doms finite_vrs fresh_vrs_of T_Abs fresh_trm_dom)
-    apply (rule closed_in_weaken)
-    apply (rule closed)
-    done
+    by (simp add: T_Abs closed closed_in_weaken fresh_list_append fresh_list_cons fresh_trm_dom)
   then have "\<turnstile> ((VarB y T\<^sub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
   with _ have "(VarB y T\<^sub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2"
     by (rule T_Abs) simp
@@ -1349,15 +1321,8 @@
   have closed: "T\<^sub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
   have "\<turnstile> (TVarB X T\<^sub>1 # \<Delta> @ B # \<Gamma>) ok"
-    apply (rule valid_consT)
-    apply (rule T_TAbs)
-    apply (simp add: doms_append
-      fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
-      fresh_fin_union [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
-      finite_doms finite_vrs tyvrs_fresh T_TAbs fresh_dom)
-    apply (rule closed_in_weaken)
-    apply (rule closed)
-    done
+    by (simp add: T_TAbs at_tyvrs_inst closed closed_in_weaken doms_append finite_doms finite_vrs
+        fresh_dom fresh_fin_union fs_tyvrs_inst pt_tyvrs_inst tyvrs_fresh)
   then have "\<turnstile> ((TVarB X T\<^sub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
   with _ have "(TVarB X T\<^sub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2"
     by (rule T_TAbs) simp
@@ -1375,12 +1340,14 @@
 
 lemma type_weaken':
  "\<Gamma> \<turnstile> t : T \<Longrightarrow>  \<turnstile> (\<Delta>@\<Gamma>) ok \<Longrightarrow> (\<Delta>@\<Gamma>) \<turnstile> t : T"
-  apply (induct \<Delta>)
-  apply simp_all
-  apply (erule validE)
-  apply (insert type_weaken [of "[]", simplified])
-  apply simp_all
-  done
+proof (induct \<Delta>)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a \<Delta>)
+  then show ?case
+    by (metis append_Cons append_Nil type_weaken validE(3))
+qed
 
 text \<open>A.6\<close>
 
@@ -1458,7 +1425,7 @@
    next
      assume "x\<noteq>y"
      then show ?case using T_Var
-       by (auto simp add:binding.inject dest: valid_cons')
+       by (auto simp:binding.inject dest: valid_cons')
    qed
  next
    case (T_App t1 T1 T2 t2 x u D)
@@ -1474,13 +1441,13 @@
  next
    case (T_TAbs X T1 t2 T2 x u D)
    from \<open>TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2\<close> have "X \<sharp> T1"
-     by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
+     by (auto simp: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
    with \<open>X \<sharp> u\<close> and T_TAbs show ?case by fastforce
  next
    case (T_TApp X t1 T2 T11 T12 x u D)
    then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
    then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" using T_TApp
-     by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar)
+     by (force simp: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar)
 qed
 
 subsubsection \<open>Type Substitution Preserves Subtyping\<close>
@@ -1538,7 +1505,7 @@
       from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
       then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_dom_fresh)
       with Y have "X \<sharp> S"
-        by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons)
+        by (induct \<Gamma>) (auto simp: fresh_list_nil fresh_list_cons)
       with ST have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S<:T[X \<mapsto> P]\<^sub>\<tau>"
         by (simp add: type_subst_identity)
       moreover from Y have "TVarB Y S \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp
@@ -1642,7 +1609,7 @@
   from T_TApp have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (\<forall>X'<:T11. T12)[X \<mapsto> P]\<^sub>\<tau>"
     by simp
   with X' and T_TApp show ?case
-    by (auto simp add: fresh_atm type_substitution_lemma
+    by (auto simp: fresh_atm type_substitution_lemma
       fresh_list_append fresh_list_cons
       ctxt_subst_fresh' type_subst_fresh subst_trm_ty_fresh
       intro: substT_subtype)
@@ -1822,7 +1789,7 @@
   case (T_Sub t S)
   from \<open>[] \<turnstile> S <: T\<^sub>1 \<rightarrow> T\<^sub>2\<close>
   obtain S\<^sub>1 S\<^sub>2 where S: "S = S\<^sub>1 \<rightarrow> S\<^sub>2" 
-    by cases (auto simp add: T_Sub)
+    by cases (auto simp: T_Sub)
   then show ?case using \<open>val t\<close> by (rule T_Sub)
 qed (auto)
 
@@ -1834,7 +1801,7 @@
   case (T_Sub t S)
   from \<open>[] \<turnstile> S <: (\<forall>X<:T\<^sub>1. T\<^sub>2)\<close>
   obtain X S\<^sub>1 S\<^sub>2 where S: "S = (\<forall>X<:S\<^sub>1. S\<^sub>2)"
-    by cases (auto simp add: T_Sub)
+    by cases (auto simp: T_Sub)
   then show ?case using T_Sub by auto 
 qed (auto)
 
diff -r 022a9c26b14f -r 34e0ddfc6dcc src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Mon Apr 22 10:43:57 2024 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Mon Apr 22 22:08:28 2024 +0100
@@ -355,7 +355,7 @@
     by (metis abs_fresh(1) btrm.fresh(2) fresh_star_set supp_fst)
 qed (auto simp: fresh_star_set)
 
-lemma psubst_nil: "[]\<lparr>t\<rparr> = t" "[]\<lparr>t'\<rparr>\<^sub>b = t'"
+lemma psubst_nil[simp]: "[]\<lparr>t\<rparr> = t" "[]\<lparr>t'\<rparr>\<^sub>b = t'"
   by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil)
 
 lemma psubst_cons:
@@ -367,9 +367,20 @@
 
 lemma psubst_append:
   "(supp (map fst (\<theta>\<^sub>1 @ \<theta>\<^sub>2))::name set) \<sharp>* map snd (\<theta>\<^sub>1 @ \<theta>\<^sub>2) \<Longrightarrow> (\<theta>\<^sub>1 @ \<theta>\<^sub>2)\<lparr>t\<rparr> = \<theta>\<^sub>2\<lparr>\<theta>\<^sub>1\<lparr>t\<rparr>\<rparr>"
-  by (induct \<theta>\<^sub>1 arbitrary: t)
-    (simp_all add: psubst_nil split_paired_all supp_list_cons psubst_cons fresh_star_def
-      fresh_list_cons fresh_list_append supp_list_append)
+proof (induct \<theta>\<^sub>1 arbitrary: t)
+  case Nil
+  then show ?case
+    by (auto simp: psubst_nil)
+next
+  case (Cons a \<theta>\<^sub>1)
+  then show ?case
+  proof (cases a)
+    case (Pair a b)
+    with Cons show ?thesis
+      apply (simp add: supp_list_cons fresh_star_set fresh_list_cons)
+      by (metis Un_iff fresh_star_set map_append psubst_cons(1) supp_list_append)
+  qed
+qed
 
 lemma abs_pat_psubst [simp]:
   "(supp p::name set) \<sharp>* \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>[p]. t\<rparr>\<^sub>b = (\<lambda>[p]. \<theta>\<lparr>t\<rparr>\<^sub>b)"
diff -r 022a9c26b14f -r 34e0ddfc6dcc src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 22 10:43:57 2024 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 22 22:08:28 2024 +0100
@@ -139,7 +139,7 @@
   by (simp add: perm_bool)
 
 (* permutation on sets *)
-lemma empty_eqvt:
+lemma empty_eqvt[simp]:
   shows "pi\<bullet>{} = {}"
   by (simp add: perm_set_def)
 
@@ -210,11 +210,11 @@
   shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
   by (simp add: fresh_def)
 
-lemma supp_unit:
+lemma supp_unit[simp]:
   shows "supp () = {}"
   by (simp add: supp_def)
 
-lemma supp_set_empty:
+lemma supp_set_empty[simp]:
   shows "supp {} = {}"
   by (force simp add: supp_def empty_eqvt)
 
@@ -230,7 +230,7 @@
   shows "(supp (nPair x y)) = (supp x)\<union>(supp y)"
   by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
 
-lemma supp_list_nil:
+lemma supp_list_nil[simp]:
   shows "supp [] = {}"
   by (simp add: supp_def)
 
@@ -251,47 +251,47 @@
   shows "supp (rev xs) = (supp xs)"
   by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)
 
-lemma supp_bool:
+lemma supp_bool[simp]:
   fixes x  :: "bool"
   shows "supp x = {}"
   by (cases "x") (simp_all add: supp_def)
 
-lemma supp_some:
+lemma supp_some[simp]:
   fixes x :: "'a"
   shows "supp (Some x) = (supp x)"
   by (simp add: supp_def)
 
-lemma supp_none:
+lemma supp_none[simp]:
   fixes x :: "'a"
   shows "supp (None) = {}"
   by (simp add: supp_def)
 
-lemma supp_int:
+lemma supp_int[simp]:
   fixes i::"int"
   shows "supp (i) = {}"
   by (simp add: supp_def perm_int_def)
 
-lemma supp_nat:
+lemma supp_nat[simp]:
   fixes n::"nat"
   shows "(supp n) = {}"
   by (simp add: supp_def perm_nat_def)
 
-lemma supp_char:
+lemma supp_char[simp]:
   fixes c::"char"
   shows "(supp c) = {}"
   by (simp add: supp_def perm_char_def)
   
-lemma supp_string:
+lemma supp_string[simp]:
   fixes s::"string"
   shows "(supp s) = {}"
   by (simp add: supp_def perm_string)
 
 (* lemmas about freshness *)
-lemma fresh_set_empty:
+lemma fresh_set_empty[simp]:
   shows "a\<sharp>{}"
   by (simp add: fresh_def supp_set_empty)
 
-lemma fresh_unit:
+lemma fresh_unit[simp]:
   shows "a\<sharp>()"
   by (simp add: fresh_def supp_unit)
 
@@ -302,7 +302,7 @@
   shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
   by (simp add: fresh_def supp_prod)
 
-lemma fresh_list_nil:
+lemma fresh_list_nil[simp]:
   fixes a :: "'x"
   shows "a\<sharp>[]"
   by (simp add: fresh_def supp_list_nil) 
@@ -321,48 +321,48 @@
   shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
   by (simp add: fresh_def supp_list_append)
 
-lemma fresh_list_rev:
+lemma fresh_list_rev[simp]:
   fixes a :: "'x"
   and   xs :: "'a list"
   shows "a\<sharp>(rev xs) = a\<sharp>xs"
   by (simp add: fresh_def supp_list_rev)
 
-lemma fresh_none:
+lemma fresh_none[simp]:
   fixes a :: "'x"
   shows "a\<sharp>None"
   by (simp add: fresh_def supp_none)
 
-lemma fresh_some:
+lemma fresh_some[simp]:
   fixes a :: "'x"
   and   x :: "'a"
   shows "a\<sharp>(Some x) = a\<sharp>x"
   by (simp add: fresh_def supp_some)
 
-lemma fresh_int:
+lemma fresh_int[simp]:
   fixes a :: "'x"
   and   i :: "int"
   shows "a\<sharp>i"
   by (simp add: fresh_def supp_int)
 
-lemma fresh_nat:
+lemma fresh_nat[simp]:
   fixes a :: "'x"
   and   n :: "nat"
   shows "a\<sharp>n"
   by (simp add: fresh_def supp_nat)
 
-lemma fresh_char:
+lemma fresh_char[simp]:
   fixes a :: "'x"
   and   c :: "char"
   shows "a\<sharp>c"
   by (simp add: fresh_def supp_char)
 
-lemma fresh_string:
+lemma fresh_string[simp]:
   fixes a :: "'x"
   and   s :: "string"
   shows "a\<sharp>s"
   by (simp add: fresh_def supp_string)
 
-lemma fresh_bool:
+lemma fresh_bool[simp]:
   fixes a :: "'x"
   and   b :: "bool"
   shows "a\<sharp>b"
@@ -953,7 +953,7 @@
   unfolding pt_def using assms
   by (auto simp add: perm_fun_def pt1 pt2 ptb pt3 pt3_rev)
 
-lemma pt_bool_inst:
+lemma pt_bool_inst[simp]:
   shows  "pt TYPE(bool) TYPE('x)"
   by (simp add: pt_def perm_bool_def)
 
@@ -963,7 +963,7 @@
   unfolding pt_def
   by(auto simp add: perm_set_def  pt1[OF pt] pt2[OF pt] pt3[OF pt])
 
-lemma pt_unit_inst:
+lemma pt_unit_inst[simp]:
   shows "pt TYPE(unit) TYPE('x)"
   by (simp add: pt_def)
 
@@ -3213,11 +3213,11 @@
 (************************)
 (* Various eqvt-lemmas  *)
 
-lemma Zero_nat_eqvt:
+lemma Zero_nat_eqvt[simp]:
   shows "pi\<bullet>(0::nat) = 0" 
 by (auto simp add: perm_nat_def)
 
-lemma One_nat_eqvt:
+lemma One_nat_eqvt[simp]:
   shows "pi\<bullet>(1::nat) = 1"
 by (simp add: perm_nat_def)
 
@@ -3259,19 +3259,19 @@
   shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)" 
 by (simp add:perm_nat_def) 
 
-lemma Zero_int_eqvt:
+lemma Zero_int_eqvt[simp]:
   shows "pi\<bullet>(0::int) = 0" 
 by (auto simp add: perm_int_def)
 
-lemma One_int_eqvt:
+lemma One_int_eqvt[simp]:
   shows "pi\<bullet>(1::int) = 1"
 by (simp add: perm_int_def)
 
-lemma numeral_int_eqvt: 
+lemma numeral_int_eqvt[simp]: 
  shows "pi\<bullet>((numeral n)::int) = numeral n"
   using perm_int_def by blast 
 
-lemma neg_numeral_int_eqvt:
+lemma neg_numeral_int_eqvt[simp]:
   shows "pi\<bullet>((- numeral n)::int) = - numeral n"
   by (simp add: perm_int_def)