diff --git a/.gitignore b/.gitignore
index b25c15b8..9d4fccfe 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 *~
+Scratch.thy
diff --git a/Tools/binder_inductive.ML b/Tools/binder_inductive.ML
index bb2c50ed..fd8bdde7 100644
--- a/Tools/binder_inductive.ML
+++ b/Tools/binder_inductive.ML
@@ -21,7 +21,9 @@ fun collapse (Inl x) = x
 fun mk_insert x S =
   Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S;
 
-fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
+datatype options = No_Equiv | No_Refresh | Verbose
+
+fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_defs_lthy =
   let
     val binds = the_default [] binds_opt;
     val ({names, ...}, { def, preds, mono, induct, intrs, ... }) = Inductive.the_inductive_global no_defs_lthy (long_name no_defs_lthy pred_name);
@@ -61,6 +63,10 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
 
     val param_Ts = map (Term.typ_subst_TVars subst) param_Ts;
 
+    val param_sugars = map (fn T => Option.mapPartial (fn s =>
+      MRBNF_Sugar.binder_sugar_of no_defs_lthy s
+    ) (try (fn () => fst (dest_Type T)) ())) param_Ts;
+
     fun collect_binders (Free _) = []
       | collect_binders (Var _) = []
       | collect_binders (Bound _) = []
@@ -230,7 +236,6 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
         val thy = Proof_Context.theory_of no_defs_lthy;
         fun mk_match mk_T ts = map2 (fn t => fn T =>
           let
-            val _ = @{print} (Thm.cterm_of no_defs_lthy t, T, mk_T T)
             val t = Logic.varify_types_global t;
             val tyenv = Sign.typ_match thy (fastype_of t, mk_T T) Vartab.empty;
           in Envir.subst_term (tyenv, Vartab.empty) t end
@@ -361,17 +366,21 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
     val perms_specified = map (fn Inl _ => false | _ => true) raw_perms;
     val supps_specified = map (fn Inl _ => false | _ => true) raw_supps;
     val one_specified = map2 (fn a => fn b => a orelse b) perms_specified supps_specified;
+
     fun keep_perm xs = cond_keep xs perms_specified;
     fun keep_supp xs = cond_keep xs supps_specified;
     fun keep_both xs = cond_keep xs one_specified;
     fun keep_binders xs = cond_keep xs binders_specified;
 
+    fun option x t f = if member (op=) options x then t else f;
+
     val defs = map snd (perms @ supps);
+    val verbose = member (op=) options Verbose;
 
     val goals = map (single o rpair []) (
       keep_perm perm_id0_goals @ keep_perm perm_comp_goals @ keep_both supp_seminat_goals
       @ keep_both perm_support_goals @ keep_supp supp_small_goals @ flat (keep_binders B_small_goals)
-      @ [G_equiv_goal, G_refresh_goal]
+      @ option No_Equiv [G_equiv_goal] [] @ option No_Refresh [G_refresh_goal] []
     );
     fun after_qed thmss lthy =
       let
@@ -422,15 +431,14 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
         val m2 = length (filter not one_specified);
         val m3 = length (filter not supps_specified);
         val m4 = length (filter not binders_specified);
-        val (((((((perm_id0s, perm_comps), supp_seminats), perm_supports), supp_smalls), B_smalls), G_equiv), G_refresh) = map hd thmss
+        val (((((((perm_id0s, perm_comps), supp_seminats), perm_supports), supp_smalls), B_smalls), G_equivs), G_refreshs) = map hd thmss
           |> chop (n - m)
           ||>> chop (n - m)
           ||>> chop (n - m2)
           ||>> chop (n - m2)
           ||>> chop (num_vars * (n - m3))
           ||>> chop (length bind_ts - m4)
-          ||>> apfst hd o chop 1
-          ||> hd;
+          ||>> chop (option No_Equiv 1 0);
 
         fun map_id0_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.map_id0_of_mrbnf mrbnf]
           | map_id0_of_mr_bnf (Inr (Inl bnf)) = [BNF_Def.map_id0_of_bnf bnf]
@@ -578,6 +586,138 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
 
         val perm_ids = map (fn thm => thm RS fun_cong RS @{thm trans[OF _ id_apply]}) perm_id0s;
 
+        val G_equiv = if member (op=) options No_Equiv then hd G_equivs else
+          Goal.prove_sorry lthy [] [] G_equiv_goal (fn {context=ctxt, ...} => EVERY1 [
+            K (Local_Defs.unfold0_tac ctxt [snd G]),
+            REPEAT_DETERM o EVERY' [
+              TRY o etac ctxt @{thm disj_forward},
+              REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
+              REPEAT_DETERM_N (length param_Ts + 1) o etac ctxt @{thm subst[OF sym]},
+              Subgoal.FOCUS_PARAMS (fn {context=ctxt, params, ...} =>
+                let
+                  val (fs, args) = map (Thm.term_of o snd) params
+                    |> drop 2
+                    |> chop 1
+                    ||> drop (length param_Ts);
+                  val (mr_bnfs, ts) = apfst (map snd o flat) (split_list (map (fn x => case find_index (curry (op=) (fastype_of x)) param_Ts of
+                    ~1 => (case find_index (curry (op=) (fastype_of x)) var_Ts of
+                      ~1 => apsnd (fn t => t $ x) (build_permute_for fs var_Ts (fastype_of x))
+                      | n => ([], nth fs n $ x))
+                    | n => ([], Term.list_comb (fst (nth perms n), fs) $ x)
+                  ) args));
+                  val equiv_commute = Named_Theorems.get ctxt "MRBNF_Recursor.equiv_commute";
+                  val equiv = Named_Theorems.get ctxt "MRBNF_Recursor.equiv" @ equiv_commute;
+                  val equiv_simps = Named_Theorems.get ctxt "MRBNF_Recursor.equiv_simps"
+                  val monos = Inductive.get_monos ctxt
+                  val set_maps = maps set_map_of_mr_bnf mr_bnfs;
+                in EVERY1 [
+                  EVERY' (map (fn t => rtac ctxt (
+                    infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)] exI
+                  )) ts),
+                  SELECT_GOAL (Local_Defs.unfold0_tac ctxt (map snd perms)),
+                  rtac ctxt conjI,
+                  SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{thms image_Un} @ equiv_simps)),
+                  REPEAT_DETERM o rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<union>)"]},
+                  REPEAT_DETERM1 o EVERY' [
+                    resolve_tac ctxt @{thms image_single[symmetric] image_empty refl} ORELSE' EVERY' [
+                      resolve_tac ctxt (map (fn thm => thm RS sym) (set_maps @ equiv_simps) @ equiv_simps),
+                      REPEAT_DETERM o assume_tac ctxt
+                    ]
+                  ],
+                  K (Local_Defs.unfold0_tac ctxt @{thms id_apply}),
+                  K (Local_Defs.unfold0_tac ctxt @{thms id_def[symmetric]}),
+                  REPEAT_DETERM o EVERY' [
+                    TRY o rtac ctxt conjI,
+                    SELECT_GOAL (EVERY1 [
+                      REPEAT_DETERM1 o FIRST' [
+                        assume_tac ctxt,
+                        eresolve_tac ctxt [conjE],
+                        resolve_tac ctxt @{thms conjI refl TrueI bij_imp_bij_inv supp_inv_bound},
+                        rtac ctxt impI THEN' eresolve_tac ctxt @{thms injD[OF bij_is_inj, rotated -1]},
+                        EVERY' [
+                          SELECT_GOAL (Local_Defs.unfold0_tac ctxt (map_filter (try (fn thm => thm RS sym)) equiv_commute)),
+                          REPEAT_DETERM1 o EVERY' [
+                            EqSubst.eqsubst_tac ctxt [0] (map (Local_Defs.unfold0 ctxt (map snd perms)) perm_comps),
+                            REPEAT_DETERM1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_inv_bound bij_imp_bij_inv})
+                          ],
+                          K (Local_Defs.unfold0_tac ctxt @{thms inv_o_simp1 inv_o_simp2 inv_simp1 inv_simp2}),
+                          K (Local_Defs.unfold0_tac ctxt (map (Local_Defs.unfold0 ctxt (map snd perms)) perm_ids)),
+                          assume_tac ctxt
+                        ],
+                        eresolve_tac ctxt (map_filter (try (fn thm => Drule.rotate_prems ~1 thm)) equiv),
+                        CHANGED o SELECT_GOAL (Local_Defs.unfold0_tac ctxt (equiv @ equiv_simps @ flat (map_filter (Option.map #permute_simps) param_sugars))),
+                        eresolve_tac ctxt (map (fn thm => Drule.rotate_prems ~1 (thm RS mp)) monos),
+                        resolve_tac ctxt monos,
+                        CHANGED o SELECT_GOAL (Local_Defs.unfold0_tac ctxt (flat (map_filter (Option.map (map (fn thm => thm RS sym) o #permute_simps)) param_sugars)))
+                      ]
+                    ])
+                  ]
+                ] end
+              ) ctxt
+            ]
+          ]);
+        val _ = (verbose ? @{print}) G_equiv
+
+        val G_refresh = if member (op=) options No_Refresh then hd (G_refreshs) else
+          let
+            val var_rules = map (fn thm =>
+              let val t = Logic.unvarify_global (Thm.prop_of thm)
+              in (map Free (rev (Term.add_frees t [])), t) end
+            ) intrs;
+
+            fun collect_permutes _ (Free _) = []
+              | collect_permutes _ (Var _) = []
+              | collect_permutes _ (Bound _) = []
+              | collect_permutes _ (Const _) = []
+              | collect_permutes vars (Abs (_, _, t)) = collect_permutes vars t
+              | collect_permutes vars (t as (t1 $ t2)) = case try (dest_Type o Term.body_type o fastype_of) t of
+                NONE => collect_permutes vars t1 @ collect_permutes vars t2
+                | SOME (s, _) => (case MRBNF_Sugar.binder_sugar_of no_defs_lthy s of
+                    NONE => collect_permutes vars t1 @ collect_permutes vars t2
+                    | SOME sugar =>
+                      let val (ctor, args) = Term.strip_comb t
+                      in case (map_filter I (map_index (fn (i, (t, _)) =>
+                          if (op=) (apply2 (fst o dest_Const) (t, ctor)) then
+                            SOME i else NONE
+                          ) (#ctors sugar))) of
+                        [] => collect_permutes vars t1 @ collect_permutes vars t2
+                        | ctor_idx::_ => (case nth (hd (#bsetss sugar)) ctor_idx of
+                          NONE => maps (collect_permutes vars) args
+                          | SOME _ =>
+                            let
+                              val arg_Ts = Term.binder_types (fastype_of ctor);
+                              val permute_bounds = nth (#permute_bounds sugar) ctor_idx;
+                              val var_args = map (fn t => if member (op=) vars t then SOME t else NONE) args;
+                              val result = map_filter I (map2 (fn NONE => K NONE
+                                | SOME perm => Option.map (fn x => (x, perm))
+                              ) permute_bounds var_args);
+
+                              val tyenv = @{fold 2} (fn NONE => K I | SOME perm => fn T =>
+                                Sign.typ_match (Proof_Context.theory_of no_defs_lthy) (body_type (fastype_of perm), T)
+                              ) permute_bounds arg_Ts Vartab.empty;
+
+                            in map (apsnd (Envir.subst_term (tyenv, Vartab.empty))) result
+                              @ maps (collect_permutes vars) args
+                            end
+                          )
+                      end
+                    );
+              fun isNONE NONE = true
+                | isNONE _ = false
+              val permute_bounds = map (distinct (op=) o uncurry collect_permutes) var_rules;
+              val matrix = map2 (fn (vars, _) => fn perms =>
+                let val inner = map (AList.lookup (op=) perms) vars;
+                in if forall isNONE inner then NONE else SOME inner end
+              ) var_rules permute_bounds;
+              val _ = (verbose ? @{print}) (map (Option.map (map (Option.map (Thm.cterm_of lthy)))) matrix)
+          in Goal.prove_sorry lthy [] [] G_refresh_goal (fn {context=ctxt, ...} => EVERY1 [
+            K (Local_Defs.unfold0_tac ctxt (snd G :: map snd perms)),
+            Subgoal.FOCUS (fn {context=ctxt, prems, ...} =>
+              refreshability_tac_internal verbose (map fst supps) matrix (nth prems 2) (nth prems 1) supp_smalls (map snd supps) ctxt
+            ) ctxt
+          ]) end;
+        val _ = (verbose ? @{print}) G_refresh
+
         fun mk_induct mono = Drule.rotate_prems ~1 (
           apply_n @{thm le_funD} n (@{thm lfp_induct} OF [mono])
             RS @{thm le_boolD}
@@ -986,7 +1126,15 @@ val parse_perm_supps =
     >> (fn ps => fold extract_perm_supp ps (NONE, NONE))
   || Scan.succeed (NONE, NONE);
 
-val binder_inductive_parser = Parse.name -- Scan.option (
+val options_parser = Parse.group (fn () => "option")
+  ((Parse.reserved "no_auto_equiv" >> K No_Equiv)
+    || (Parse.reserved "no_auto_refresh" >> K No_Refresh)
+    || (Parse.reserved "verbose" >> K Verbose))
+
+val config_parser = Scan.optional (@{keyword "("} |--
+  Parse.!!! (Parse.list1 options_parser) --| @{keyword ")"}) []
+
+val binder_inductive_parser = config_parser -- Parse.name -- Scan.option (
     @{keyword where} |-- Parse.enum1 "|" (Parse.name --| @{keyword binds} -- Parse.and_list Parse.term)
   ) -- parse_perm_supps
 
diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML
index 7958910a..8bd3a668 100644
--- a/Tools/mrbnf_sugar.ML
+++ b/Tools/mrbnf_sugar.ML
@@ -17,6 +17,7 @@ type binder_sugar = {
   permute_simps: thm list,
   subst_simps: thm list option,
   bsetss: term option list list,
+  permute_bounds: term option list list,
   bset_bounds: thm list,
   mrbnf: MRBNF_Def.mrbnf,
   strong_induct: thm,
@@ -59,6 +60,7 @@ type binder_sugar = {
   permute_simps: thm list,
   subst_simps: thm list option,
   bsetss: term option list list,
+  permute_bounds: term option list list,
   bset_bounds: thm list,
   mrbnf: MRBNF_Def.mrbnf,
   strong_induct: thm,
@@ -67,12 +69,13 @@ type binder_sugar = {
 };
 
 fun morph_binder_sugar phi { map_simps, permute_simps, set_simpss, subst_simps, mrbnf,
-  strong_induct, distinct, ctors, bsetss, bset_bounds } = {
+  strong_induct, distinct, ctors, bsetss, bset_bounds, permute_bounds } = {
   map_simps = map (Morphism.thm phi) map_simps,
   permute_simps = map (Morphism.thm phi) permute_simps,
   set_simpss = map (map (Morphism.thm phi)) set_simpss,
   subst_simps = Option.map (map (Morphism.thm phi)) subst_simps,
   bsetss = map (map (Option.map (Morphism.term phi))) bsetss,
+  permute_bounds = map (map (Option.map (Morphism.term phi))) permute_bounds,
   bset_bounds = map (Morphism.thm phi) bset_bounds,
   mrbnf = MRBNF_Def.morph_mrbnf phi mrbnf,
   strong_induct = Morphism.thm phi strong_induct,
@@ -334,8 +337,7 @@ fun create_binder_datatype (spec : spec) lthy =
     val bounds = map_filter (fn (x, MRBNF_Def.Bound_Var) => SOME (TFree x) | _ => NONE) (#vars spec);
     val frees = map_filter (fn (x, MRBNF_Def.Free_Var) => SOME (TFree x) | _ => NONE) (#vars spec);
 
-    (* TODO: Use mrbnf sets here (only relevant for passive variables) *)
-    val (bset_optss, set_simpss) = split_list (map (fn FVars =>
+    val param_vars = map (fn FVars =>
       let
         fun get_var vars = hd (filter (fn T =>
           Term.typ_subst_atomic replace T = HOLogic.dest_setT (range_type (fastype_of FVars))
@@ -345,7 +347,12 @@ fun create_binder_datatype (spec : spec) lthy =
         val rec_bounds = map (nth rec_vars) (the_default [] (
           Option.mapPartial (try (nth (#binding_rel spec))) (get_index bound bounds)
         ));
-      in split_list (map2 (fn (ctor, _) => fn (_, tys) =>
+      in (free, bound, rec_bounds) end
+    ) (#FVars quotient);
+
+    (* TODO: Use mrbnf sets here (only relevant for passive variables) *)
+    val (bset_optss, set_simpss) = split_list (map2 (fn FVars => fn (free, bound, rec_bounds) =>
+      split_list (map2 (fn (ctor, _) => fn (_, tys) =>
         let
           val (xs, _) = lthy
             |> mk_Frees "x" tys;
@@ -406,9 +413,10 @@ fun create_binder_datatype (spec : spec) lthy =
           ]
         ])) end
       ) ctors (#ctors spec))
-    end) (#FVars quotient));
+    ) (#FVars quotient) param_vars);
 
     val ctors_tys = ctors ~~ map snd (#ctors spec);
+
     val distinct = flat (flat (map_index (fn (i, ((ctor, ctor_def), tys1)) => map_index (fn (j, ((ctor2, ctor2_def), tys2)) =>
       let
         val ((xs, ys), _) = names_lthy
@@ -427,7 +435,7 @@ fun create_binder_datatype (spec : spec) lthy =
       ])] end
     ) ctors_tys) ctors_tys));
 
-    (* TODO: map_bij (rename simps); injection *)
+    (* TODO: injection *)
 
     (* Term for variable substitution *)
     val x = length replace - #rec_vars spec;
@@ -653,10 +661,10 @@ fun create_binder_datatype (spec : spec) lthy =
         ];
       in mk_map_simps lthy true fs (SOME o MRBNF_Recursor.mk_supp_bound) (fn t => fn _ => SOME (mk_imsupp t)) (K []) [] mapx tac end;
 
+    val (fs, _) = lthy
+        |> mk_Frees "f" (map (fn a => a --> a) vars);
     val permute_simps =
       let
-        val (fs, _) = lthy
-          |> mk_Frees "f" (map (fn a => a --> a) vars);
         val Ts' = snd (dest_Type qT);
         val mapx = Term.subst_atomic_types (Ts' ~~ vars) (#rename quotient);
         fun tac ctxt prems = EVERY1 [
@@ -673,6 +681,27 @@ fun create_binder_datatype (spec : spec) lthy =
         (single o HOLogic.mk_Trueprop o mk_bij) bounds mapx tac
       end;
 
+    val permute_boundss = map2 (fn (_, tys) => fn permute_simp =>
+      let
+        val (xs, _) = lthy
+          |> mk_Frees "x" (map (Term.typ_subst_atomic replace) tys);
+        val permute_args = Thm.prop_of permute_simp
+          |> Logic.strip_imp_concl
+          |> HOLogic.dest_Trueprop
+          |> snd o HOLogic.dest_eq
+          |> Logic.unvarify_global
+          |> snd o Term.strip_comb;
+
+        val bound = map (fn T =>
+          map (fn (_, bound, rec_bounds) => member (op=) (bound::rec_bounds) T) param_vars
+        ) tys;
+      in @{map 3} (fn x => fn t => fn bn => if not (exists I bn) then NONE else SOME (
+         fold_rev (fn (b, f) => fn t => Term.absfree (dest_Free f) (if b then t else
+           Term.subst_atomic [(f, HOLogic.id_const (domain_type (fastype_of f)))] t
+         )) (bn ~~ fs) (Term.absfree (dest_Free x) t)
+      )) xs permute_args bound end
+    ) ctors_tys permute_simps;
+
     val cmin_UNIV = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars);
     val Cinfinite_card = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_conj (
       mk_cinfinite cmin_UNIV, mk_Card_order cmin_UNIV
@@ -751,6 +780,7 @@ fun create_binder_datatype (spec : spec) lthy =
       strong_induct = strong_induct,
       subst_simps = Option.map snd tvsubst_opt,
       bsetss = bset_optss,
+      permute_bounds = permute_boundss,
       bset_bounds = [],
       mrbnf = mrbnf,
       distinct = distinct,
diff --git a/thys/Infinitary_FOL/InfFOL.thy b/thys/Infinitary_FOL/InfFOL.thy
index c992c12b..172912c5 100644
--- a/thys/Infinitary_FOL/InfFOL.thy
+++ b/thys/Infinitary_FOL/InfFOL.thy
@@ -339,7 +339,7 @@ inductive deduct :: "ifol set\<^sub>k \<Rightarrow> ifol \<Rightarrow> bool" (in
 | AllI: "\<lbrakk> \<Delta> \<turnstile> f ; set\<^sub>k\<^sub>2 V \<inter> \<Union>(FFVars_ifol' ` set\<^sub>k \<Delta>) = {} \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> All V f"
 | AllE: "\<lbrakk> \<Delta> \<turnstile> All V f ; supp \<rho> \<subseteq> set\<^sub>k\<^sub>2 V \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> f\<lbrakk>\<rho>\<rbrakk>"
 
-binder_inductive deduct
+binder_inductive (no_auto_equiv, no_auto_refresh) deduct
   subgoal for R B \<sigma> x1 x2
     unfolding induct_rulify_fallback split_beta
     apply (elim disj_forward exE)
diff --git a/thys/Infinitary_Lambda_Calculus/ILC.thy b/thys/Infinitary_Lambda_Calculus/ILC.thy
index f00b686c..b93edbfa 100644
--- a/thys/Infinitary_Lambda_Calculus/ILC.thy
+++ b/thys/Infinitary_Lambda_Calculus/ILC.thy
@@ -71,7 +71,6 @@ lemma inj_embed: "inj embed"
   unfolding embed_def
   by (rule someI_ex[OF ex_inj_infinite_regular_var_iterm_pre[where 'a='a]])
 
-
 (****************************)
 (* DATATYPE-SPECIFIC CUSTOMIZATION  *)
 
@@ -831,11 +830,11 @@ unfolding imkSubst_def by auto
 lemma card_dsset_ivar: "|dsset xs| <o |UNIV::ivar set|"
 using countable_card_ivar countable_card_le_natLeq dsset_natLeq by auto
 
-lemma SSupp_imkSubst[simp,intro]: "|SSupp (imkSubst xs es)| <o |UNIV::ivar set|"
+lemma SSupp_imkSubst[simp,intro]: "|SSupp (imkSubst xs es)| <o |UNIV::'a::var_iterm_pre set|"
 proof-
   have "SSupp (imkSubst xs es) \<subseteq> dsset xs"
   unfolding SSupp_def by auto (metis imkSubst_idle)
-  thus ?thesis by (simp add: card_of_subset_bound card_dsset_ivar)
+  thus ?thesis by (simp add: card_of_subset_bound dsset_card_ls)
 qed
 
 lemma imkSubst_smap_irrename:
@@ -947,7 +946,16 @@ proof-
         imkSubst_idle imkSubst_smap iterm.set(3) not_imageI) . . .
 qed
 
-
+lemma irrename_itvsubst[equiv_commute]:
+  fixes \<sigma>::"ivar \<Rightarrow> ivar"
+  shows "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::ivar set|
+  \<Longrightarrow> irrename \<sigma> (itvsubst (imkSubst xs es2) e1) = itvsubst (imkSubst (dsmap \<sigma> xs) (smap (irrename \<sigma>) es2)) (irrename \<sigma> e1)"
+  apply (rule trans)
+   apply (rule box_equals[OF iterm.rrename_tvsubst[THEN fun_cong] comp_apply comp_apply])
+     apply assumption+
+   apply (rule SSupp_imkSubst)
+  apply (rule arg_cong2[OF _ refl, of _ _ itvsubst])
+  using imkSubst_smap_irrename[symmetric, of \<sigma>] by auto
 
 (* RECURSOR PREPARATIONS: *)
 
diff --git a/thys/Infinitary_Lambda_Calculus/ILC_Beta.thy b/thys/Infinitary_Lambda_Calculus/ILC_Beta.thy
index 0bc49596..0a999140 100644
--- a/thys/Infinitary_Lambda_Calculus/ILC_Beta.thy
+++ b/thys/Infinitary_Lambda_Calculus/ILC_Beta.thy
@@ -24,7 +24,7 @@ inductive istep :: "itrm \<Rightarrow> itrm \<Rightarrow> bool" where
 | iAppR: "istep (snth es2 i) e2' \<Longrightarrow> istep (iApp e1 es2) (iApp e1 (supd es2 i e2'))"
 | Xi: "istep e e' \<Longrightarrow> istep (iLam xs e) (iLam xs e')"
 
-binder_inductive istep
+binder_inductive (no_auto_equiv, no_auto_refresh) istep
   subgoal for R B \<sigma> x1 x2
     apply (elim disj_forward exE conjE)
     subgoal for xs e1 es2
diff --git a/thys/Infinitary_Lambda_Calculus/ILC_affine.thy b/thys/Infinitary_Lambda_Calculus/ILC_affine.thy
index 63e3f719..596fea1e 100644
--- a/thys/Infinitary_Lambda_Calculus/ILC_affine.thy
+++ b/thys/Infinitary_Lambda_Calculus/ILC_affine.thy
@@ -21,7 +21,7 @@ inductive affine  :: "itrm \<Rightarrow> bool" where
  \<Longrightarrow>
  affine (iApp e1 es2)"
 
-binder_inductive affine
+binder_inductive (no_auto_equiv, no_auto_refresh) affine
   unfolding isPerm_def induct_rulify_fallback
   subgoal for R B \<sigma> t
     apply(elim disjE)
diff --git a/thys/MRBNF_FP.thy b/thys/MRBNF_FP.thy
index b9b074c4..ba145e0a 100644
--- a/thys/MRBNF_FP.thy
+++ b/thys/MRBNF_FP.thy
@@ -347,13 +347,19 @@ lemma extend_fresh:
   unfolding Int_Un_distrib fun_eq_iff o_apply id_apply
   by blast
 
+named_theorems refresh_extends
+named_theorems refresh_smalls
+named_theorems refresh_simps
+named_theorems refresh_intros
+named_theorems refresh_elims
+
 ML \<open>
 local
   open BNF_Util
   open BNF_FP_Util
 in
 
-fun refreshability_tac verbose supps renames instss G_thm eqvt_thm extend_thms small_thms simp_thms intro_thms elim_thms ctxt =
+fun refreshability_tac_common verbose supps instss G_thm eqvt_thm extend_thms small_thms simp_thms intro_thms elim_thms ctxt =
   let
     val n = length supps;
     fun case_tac NONE _ prems ctxt = HEADGOAL (Method.insert_tac ctxt prems THEN' 
@@ -375,15 +381,17 @@ val _ = prems |> map (Thm.pretty_thm ctxt #> verbose ? @{print tracing});
             |> Library.foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>);
           val fresh = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt B), SOME (Thm.cterm_of ctxt A)]
             @{thm extend_fresh};
+          val _ = (verbose ? @{print tracing}) fresh
 
           fun case_inner_tac fs fprems ctxt =
-            let
+            let 
+              val _ = (verbose ? @{print tracing}) fs
               val f = hd fs |> snd |> Thm.term_of;
               val ex_f = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt f)] exI;
               val ex_B' = infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt (mk_image f $ B))] exI;
               val args = params |> map (snd #> Thm.term_of);
               val xs = @{map 2} (fn i => fn a => Thm.cterm_of ctxt
-                (case i of SOME i => nth renames i $ f $ a | NONE => a)) insts args;
+                (case i of SOME t => t $ f $ a | NONE => a)) insts args;
 val _ = fprems |> map (Thm.pretty_thm ctxt #> verbose ? @{print tracing});
               val eqvt_thm = eqvt_thm OF take 2 fprems;
               val extra_assms = assms RL (eqvt_thm :: extend_thms);
@@ -403,24 +411,40 @@ val _ = extra_assms |> map (Thm.pretty_thm ctxt #> verbose ? @{print tracing});
                   addSEs elim_thms) 0 10) THEN_ALL_NEW (SELECT_GOAL (print_tac ctxt "auto failed")))
             end;
           val small_ctxt = ctxt addsimps small_thms;
-        in
-          HEADGOAL (rtac ctxt (fresh RS exE) THEN'
-          SELECT_GOAL (auto_tac (small_ctxt addsimps [hd defs])) THEN'
-          REPEAT_DETERM_N 2 o (asm_simp_tac small_ctxt) THEN'
-          SELECT_GOAL (unfold_tac ctxt @{thms Int_Un_distrib Un_empty}) THEN'
-          REPEAT_DETERM o etac ctxt conjE THEN'
+        in EVERY1 [
+          rtac ctxt (fresh RS exE),
+          if verbose then K (print_tac ctxt "after_fresh") else K all_tac,
+          SELECT_GOAL (auto_tac (small_ctxt addsimps [hd defs])),
+          if verbose then K (print_tac ctxt "after_auto") else K all_tac,
+          REPEAT_DETERM_N 2 o (asm_simp_tac small_ctxt),
+          SELECT_GOAL (unfold_tac ctxt @{thms Int_Un_distrib Un_empty}),
+          REPEAT_DETERM o etac ctxt conjE,
+          if verbose then K (print_tac ctxt "pre_case_inner_tac") else K all_tac,
           Subgoal.SUBPROOF (fn focus =>
-            case_inner_tac (#params focus) (#prems focus) (#context focus)) ctxt)
-        end;
+            case_inner_tac (#params focus) (#prems focus) (#context focus)) ctxt
+        ] end;
   in
-    unfold_tac ctxt @{thms conj_disj_distribL ex_disj_distrib} THEN
-    HEADGOAL (
-      rtac ctxt (G_thm RSN (2, cut_rl)) THEN'
-      REPEAT_ALL_NEW (eresolve_tac ctxt @{thms exE conjE disj_forward}) THEN'
+    unfold_tac ctxt @{thms conj_disj_distribL ex_disj_distrib} THEN EVERY1 [
+      rtac ctxt (G_thm RSN (2, cut_rl)),
+      REPEAT_ALL_NEW (eresolve_tac ctxt @{thms exE conjE disj_forward}),
+      if verbose then K (print_tac ctxt "pre_case_tac") else K all_tac,
       EVERY' (map (fn insts => Subgoal.SUBPROOF (fn focus =>
-        case_tac insts (#params focus) (#prems focus) (#context focus)) ctxt) instss))
+        case_tac insts (#params focus) (#prems focus) (#context focus)) ctxt) instss)
+    ]
   end;
 
+fun refreshability_tac_internal verbose supps instss G_thm eqvt_thm smalls simps ctxt =
+  refreshability_tac_common verbose supps instss G_thm eqvt_thm
+    (Named_Theorems.get ctxt "MRBNF_FP.refresh_extends")
+    (smalls @ Named_Theorems.get ctxt "MRBNF_FP.refresh_smalls")
+    (simps @ Named_Theorems.get ctxt "MRBNF_FP.refresh_simps")
+    (Named_Theorems.get ctxt "MRBNF_FP.refresh_intros")
+    (Named_Theorems.get ctxt "MRBNF_FP.refresh_elims") ctxt;
+
+fun refreshability_tac verbose supps renames instss =
+  let val instss' = map (Option.map (map (Option.map (nth renames)))) instss
+  in refreshability_tac_common verbose supps instss' end
+
 end;
 \<close>
 
diff --git a/thys/MRBNF_Recursor.thy b/thys/MRBNF_Recursor.thy
index 55039d02..63c863cb 100644
--- a/thys/MRBNF_Recursor.thy
+++ b/thys/MRBNF_Recursor.thy
@@ -10,6 +10,18 @@ ML_file \<open>../Tools/mrbnf_vvsubst.ML\<close>
 ML_file \<open>../Tools/mrbnf_tvsubst.ML\<close>
 ML_file \<open>../Tools/mrbnf_sugar.ML\<close>
 
+named_theorems equiv
+named_theorems equiv_commute
+named_theorems equiv_simps
+
+declare Un_iff[equiv_simps] de_Morgan_disj[equiv_simps]
+  inj_image_mem_iff[OF bij_is_inj, equiv_simps]
+  singleton_iff[equiv_simps] image_empty[equiv_simps]
+  Int_Un_distrib[equiv_simps] Un_empty[equiv_simps]
+  image_is_empty[equiv_simps] image_Int[OF bij_is_inj, symmetric, equiv_simps]
+  inj_eq[OF bij_is_inj, equiv_simps] inj_eq[OF bij_is_inj, equiv_simps]
+  image_insert[equiv_simps] insert_iff[equiv_simps] notin_empty_eq_True[equiv_simps]
+
 context begin
 ML_file \<open>../Tools/binder_induction.ML\<close>
 end
diff --git a/thys/POPLmark/POPLmark_1A.thy b/thys/POPLmark/POPLmark_1A.thy
index f7911238..f609cd5e 100644
--- a/thys/POPLmark/POPLmark_1A.thy
+++ b/thys/POPLmark/POPLmark_1A.thy
@@ -108,7 +108,6 @@ using assms(1,2) proof (binder_induction \<Gamma> "\<forall>X<:S\<^sub>1. S\<^su
       apply (rule ty.equiv)
        apply (rule bij_swap supp_swap_bound infinite_var)+
         apply (rule SA_All(6))
-        apply (unfold map_context_def[symmetric])
      apply (subst extend_eqvt)
        apply (rule bij_swap supp_swap_bound infinite_var)+
      apply (rule arg_cong3[of _ _ _ _ _ _ extend])
@@ -145,7 +144,6 @@ using assms(1,2) proof (binder_induction \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^
       apply (rule ty.equiv)
        apply (rule bij_swap supp_swap_bound infinite_var)+
         apply (rule SA_All(6))
-        apply (unfold map_context_def[symmetric])
      apply (subst extend_eqvt)
        apply (rule bij_swap supp_swap_bound infinite_var)+
      apply (rule arg_cong3[of _ _ _ _ _ _ extend])
diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy
index 8e78562d..874317bc 100644
--- a/thys/POPLmark/SystemFSub.thy
+++ b/thys/POPLmark/SystemFSub.thy
@@ -102,7 +102,7 @@ lemma Forall_swap: "y \<notin> FFVars_typ T2 - {x} \<Longrightarrow> Forall (x::
 type_synonym type = "var typ"
 type_synonym \<Gamma>\<^sub>\<tau> = "(var \<times> type) list"
 
-definition map_context :: "(var \<Rightarrow> var) \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> \<Gamma>\<^sub>\<tau>" where
+abbreviation map_context :: "(var \<Rightarrow> var) \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> \<Gamma>\<^sub>\<tau>" where
   "map_context f \<equiv> map (map_prod f (rrename_typ f))"
 
 abbreviation FFVars_ctxt :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> var set" where
@@ -117,19 +117,18 @@ abbreviation disjoint :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> \<Gamma>\<^sub>\<t
   "disjoint \<Gamma> \<Delta> \<equiv> dom \<Gamma> \<inter> dom \<Delta> = {}"
 
 lemma map_context_id[simp]: "map_context id = id"
-  unfolding map_context_def by simp
+  by simp
 lemma map_context_comp0[simp]:
   assumes "bij f" "|supp f| <o |UNIV::var set|" "bij g" "|supp g| <o |UNIV::var set|"
   shows "map_context f \<circ> map_context g = map_context (f \<circ> g)"
   apply (rule ext)
-  unfolding map_context_def
   using assms by (auto simp: typ.rrename_comps)
 lemmas map_context_comp = trans[OF comp_apply[symmetric] fun_cong[OF map_context_comp0]]
 declare map_context_comp[simp]
 lemma context_dom_set[simp]:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
   shows "dom (map_context f xs) = f ` dom xs"
-  unfolding map_context_def by force
+  by force
 lemma set_bd_UNIV: "|set xs| <o |UNIV::var set|"
   apply (rule ordLess_ordLeq_trans)
     apply (tactic \<open>resolve_tac @{context} (BNF_Def.set_bd_of_bnf (the (BNF_Def.bnf_of @{context} @{type_name list}))) 1\<close>)
@@ -143,7 +142,6 @@ lemma context_map_cong_id:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
   and "\<And>a. a \<in> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<Longrightarrow> f a = a"
 shows "map_context f \<Gamma> = \<Gamma>"
-  unfolding map_context_def
   apply (rule trans)
    apply (rule list.map_cong0[of _ _ id])
    apply (rule trans)
@@ -167,29 +165,29 @@ inductive_cases
   and wf_ConsE[elim!]: "\<turnstile> (a#\<Gamma>) ok"
 print_theorems
 
-lemma in_context_eqvt:
+lemma in_context_eqvt[equiv]:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
   shows "x <: T \<in> \<Gamma> \<Longrightarrow> f x <: rrename_typ f T \<in> map_context f \<Gamma>"
-  using assms unfolding map_context_def by auto
+  using assms by auto
 
-lemma extend_eqvt:
+lemma extend_eqvt[equiv_commute]:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
   shows "map_context f (\<Gamma>,x<:T) = map_context f \<Gamma>,f x <: rrename_typ f T"
-  using assms unfolding map_context_def by simp
+  using assms by simp
 
-lemma closed_in_eqvt:
+lemma closed_in_eqvt[equiv]:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
   shows "S closed_in \<Gamma> \<Longrightarrow> rrename_typ f S closed_in map_context f \<Gamma>"
-  using assms by (auto simp: typ.FFVars_rrenames)
+  using assms by (metis context_dom_set image_mono typ.FFVars_rrenames)
 
-lemma wf_eqvt:
+lemma wf_eqvt[equiv]:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
   shows "\<turnstile> \<Gamma> ok \<Longrightarrow> \<turnstile> map_context f \<Gamma> ok"
-unfolding map_context_def proof (induction \<Gamma>)
+proof (induction \<Gamma>)
   case (Cons a \<Gamma>)
   then show ?case using assms apply auto
     apply (metis fst_conv image_iff)
-    using closed_in_eqvt map_context_def by fastforce
+    using closed_in_eqvt by fastforce
 qed simp
 
 abbreviation Tsupp :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> type \<Rightarrow> type \<Rightarrow> var set" where
@@ -232,7 +230,7 @@ lemma map_context_swap_FFVars[simp]:
 "\<forall>k\<in>set \<Gamma>. x \<noteq> fst k \<and> x \<notin> FFVars_typ (snd k) \<and>
            xx \<noteq> fst k \<and> xx \<notin> FFVars_typ (snd k) \<Longrightarrow>
     map_context (id(x := xx, xx := x)) \<Gamma> = \<Gamma>"
-  unfolding map_context_def apply(rule map_idI) by auto
+  apply(rule map_idI) by auto
 
 lemma isPerm_swap: "isPerm (id(x := z, z := x))"
   unfolding isPerm_def by (auto simp: supp_swap_bound infinite_UNIV)
@@ -276,14 +274,7 @@ declare ty.intros[intro]
 lemma ty_fresh_extend: "\<Gamma>, x <: U \<turnstile> S <: T \<Longrightarrow> x \<notin> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<and> x \<notin> FFVars_typ U"
   by (metis (no_types, lifting) UnE fst_conv snd_conv subsetD wf_ConsE wf_FFVars wf_context)
 
-binder_inductive ty
-  subgoal for R B \<sigma> \<Gamma> T1 T2
-    unfolding split_beta
-    by (elim disj_forward exE)
-      (auto simp add: isPerm_def supp_inv_bound map_context_def[symmetric] typ_vvsubst_rrename
-        typ.rrename_comps typ.FFVars_rrenames wf_eqvt extend_eqvt
-        | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-        | ((rule exI[of _ "rrename_typ \<sigma> _"])+, (rule conjI)?, rule in_context_eqvt))+
+binder_inductive (no_auto_refresh) ty
   subgoal premises prems for R B \<Gamma> T1 T2
     by (tactic \<open>refreshability_tac false
       [@{term "\<lambda>\<Gamma>. dom \<Gamma> \<union> FFVars_ctxt \<Gamma>"}, @{term "FFVars_typ :: type \<Rightarrow> var set"}, @{term "FFVars_typ :: type \<Rightarrow> var set"}]
diff --git a/thys/Pi_Calculus/Commitment.thy b/thys/Pi_Calculus/Commitment.thy
index 42d89a52..21b3b92a 100644
--- a/thys/Pi_Calculus/Commitment.thy
+++ b/thys/Pi_Calculus/Commitment.thy
@@ -337,9 +337,21 @@ fun ns :: "act \<Rightarrow> var set" where
 abbreviation "bvars \<equiv> bns"
 abbreviation "fvars \<equiv> fns"
 
+lemma ns_equiv[equiv]: "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
+  \<sigma> x \<in> ns (map_action \<sigma> \<alpha>) \<longleftrightarrow> x \<in> ns \<alpha>"
+  by (cases \<alpha>) auto
+
 lemma bns_bound: "|bns \<alpha>| <o |UNIV::'a::var_commit_pre set|"
   by (metis Commitment.var_ID_class.large bns.elims finite_iff_le_card_var finite_ordLess_infinite2 insert_bound large_imp_infinite singl_bound)
 
+lemma rrename_commit_Cmt[simp]: "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
+  rrename_commit \<sigma> (Cmt \<alpha> P) = Cmt (map_action \<sigma> \<alpha>) (rrename \<sigma> P)"
+  by (cases \<alpha>) auto
+
+lemma fra_equiv[equiv]: "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
+  fra (map_action \<sigma> \<alpha>) = fra \<alpha>"
+  by (cases \<alpha>) auto
+
 local_setup \<open>MRBNF_Sugar.register_binder_sugar "Commitment.commit" {
   ctors = [
     (@{term Finp}, @{thm Finp_def}),
@@ -351,7 +363,7 @@ local_setup \<open>MRBNF_Sugar.register_binder_sugar "Commitment.commit" {
   ],
   permute_simps = @{thms
     rrename_commit_Finp rrename_commit_Fout rrename_commit_Bout
-    rrename_commit_Binp rrename_commit_Tau
+    rrename_commit_Tau rrename_commit_Binp rrename_commit_Cmt
   },
   map_simps = [],
   distinct = [],
@@ -363,6 +375,14 @@ local_setup \<open>MRBNF_Sugar.register_binder_sugar "Commitment.commit" {
     SOME @{term "\<lambda>x1 x2 x3. {x2}"},
     SOME @{term "\<lambda>x P. bns x"}
   ]],
+  permute_bounds = [
+    [NONE, NONE, NONE],
+    [NONE, NONE, NONE],
+    [NONE, NONE, NONE],
+    [NONE],
+    [NONE, NONE, NONE],
+    [NONE, NONE]
+  ],
   bset_bounds = @{thms bns_bound},
   strong_induct = @{thm refl},
   mrbnf = the (MRBNF_Def.mrbnf_of @{context} "Commitment.commit_pre"),
@@ -372,12 +392,7 @@ local_setup \<open>MRBNF_Sugar.register_binder_sugar "Commitment.commit" {
 
 abbreviation "swapa act x y \<equiv> map_action (id(x:=y,y:=x)) act"
 
-lemma bvars_map_action[simp]: "bvars (map_action \<sigma> act) = image \<sigma> (bvars act)"
-by (cases act, auto)
-
-lemma rrename_commit_Cmt[simp]:
-"bij \<sigma> \<and> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
- rrename_commit \<sigma> (Cmt act P) = Cmt (map_action \<sigma> act) (rrename \<sigma> P)"
+lemma bvars_map_action[simp, equiv_simps]: "bvars (map_action \<sigma> act) = image \<sigma> (bvars act)"
 by (cases act, auto)
 
 lemma bvars_act_bout: "bvars act = {} \<or> (\<exists>a b. act = bout a b) \<or> (\<exists>a b. act = binp a b)"
diff --git a/thys/Pi_Calculus/Pi.thy b/thys/Pi_Calculus/Pi.thy
index ff765d46..c1a13be7 100644
--- a/thys/Pi_Calculus/Pi.thy
+++ b/thys/Pi_Calculus/Pi.thy
@@ -20,10 +20,11 @@ for
   vvsubst: vvsubst
   tvsubst: tvsubst
 
+declare term.FFVars_rrenames[equiv_simps]
+
 (****************************)
 (* DATATYPE-SPECIFIC CUSTOMIZATION  *)
 
-
 (* Monomorphising: *)
 instance var :: var_term_pre apply standard
   using Field_natLeq infinite_iff_card_of_nat infinite_var
@@ -407,7 +408,7 @@ lemmas usub_simps = usub_simps_free usub_Inp usub_Res
 
 
 
-lemma rrename_usub[simp]:
+lemma rrename_usub[simp, equiv]:
 assumes \<sigma>: "bij \<sigma>" "|supp \<sigma>| <o |UNIV::var set|"
 shows "rrename \<sigma> (usub P u (x::var)) = usub (rrename \<sigma> P) (\<sigma> u) (\<sigma> x)"
 using assms
@@ -457,7 +458,7 @@ proof-
       using term_pre.supp_comp_bound by auto . .
 qed
 
-lemma Inp_eq_usub: 
+lemma Inp_eq_usub:
   assumes il: "Inp x y Q = Inp x y' Q'"
   shows "usub Q z y = usub Q' z y'"
   by (metis (no_types, lifting) Inp_inject_swap Inp_refresh il usub_refresh)
@@ -472,4 +473,9 @@ apply auto
 apply(rule rrename_cong)
 by (auto simp: term_pre.supp_comp_bound)
 
+lemma rrename_equiv[equiv]:
+  assumes "bij (f::var\<Rightarrow>var)" "|supp f| <o |UNIV::var set|"
+  shows "rrename f P = rrename f Q \<longleftrightarrow> P = Q"
+  by (simp add: assms(1,2) term.rrename_bijs)
+
 end
diff --git a/thys/Pi_Calculus/Pi_Transition_Early.thy b/thys/Pi_Calculus/Pi_Transition_Early.thy
index e986d1f4..cf449bb5 100644
--- a/thys/Pi_Calculus/Pi_Transition_Early.thy
+++ b/thys/Pi_Calculus/Pi_Transition_Early.thy
@@ -11,27 +11,7 @@ inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
 | ScopeBound: "\<lbrakk> trans P (Bout a x P') ; y \<notin> {a, x} ; x \<notin> FFVars P \<union> {a} \<rbrakk> \<Longrightarrow> trans (Res y P) (Bout a x (Res y P'))"
 | ParLeft: "\<lbrakk> trans P (Cmt \<alpha> P') ; bns \<alpha> \<inter> (FFVars P \<union> FFVars Q) = {} \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Cmt \<alpha> (P' \<parallel> Q))"
 
-(*
-lemma "B = bvars \<alpha>' \<Longrightarrow> P = Paa \<parallel> Qaa \<Longrightarrow> Q = Cmt \<alpha>' (P'a \<parallel> Qaa) \<Longrightarrow> R Paa (Cmt \<alpha>' P'a) \<Longrightarrow>
-   bvars \<alpha>' \<inter> (FFVars Paa \<union> FFVars Qaa) = {} \<Longrightarrow>
-  \<exists>Pa \<alpha> P' Qa.
-       xa ` B = bvars \<alpha> \<and>
-       P = Pa \<parallel> Qa \<and>
-       Q = Cmt \<alpha> (P' \<parallel> Qa) \<and>
-       R Pa (Cmt \<alpha> P') \<and> bvars \<alpha> \<inter> FFVars Pa = {} \<and> bvars \<alpha> \<inter> FFVars Qa = {}"
-  apply (cases \<alpha>'; hypsubst_thin; unfold Cmt.simps bns.simps)
-*)
-
-binder_inductive trans
-  subgoal for R B \<sigma> x1 x2
-    apply simp
-    apply (elim disj_forward)
-    by (auto simp: isPerm_def
-        term.rrename_comps action.map_comp action.map_id
-        | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-        | (rule exI[of _ "map_action \<sigma> _"])
-        | (rule exI[of _ "rrename \<sigma> _"])
-        | ((rule exI[of _ "\<sigma> _"])+; auto))+
+binder_inductive (no_auto_refresh) trans
   subgoal premises prems for R B P Q
     by (tactic \<open>refreshability_tac false
       [@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars_commit :: cmt \<Rightarrow> var set"}]
diff --git a/thys/Pi_Calculus/Pi_Transition_Late.thy b/thys/Pi_Calculus/Pi_Transition_Late.thy
index b7ef79fe..d7181452 100644
--- a/thys/Pi_Calculus/Pi_Transition_Late.thy
+++ b/thys/Pi_Calculus/Pi_Transition_Late.thy
@@ -11,15 +11,7 @@ inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
 | ScopeBound: "\<lbrakk> trans P (Bout a x P') ; y \<notin> {a, x} ; x \<notin> FFVars P \<union> {a} \<rbrakk> \<Longrightarrow> trans (Res y P) (Bout a x (Res y P'))"
 | ParLeft: "\<lbrakk> trans P (Cmt \<alpha> P') ; bns \<alpha> \<inter> (FFVars P \<union> FFVars Q) = {} \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Cmt \<alpha> (P' \<parallel> Q))"
 
-binder_inductive trans
-  subgoal for R B \<sigma> x1 x2
-    apply simp
-    apply (elim disj_forward)
-    by (auto simp: isPerm_def
-        term.rrename_comps action.map_comp action.map_id
-        | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-        | (rule exI[of _ "map_action \<sigma> _"] exI[of _ "rrename \<sigma> _"])
-        | ((rule exI[of _ "\<sigma> _"])+; auto))+
+binder_inductive (no_auto_refresh) trans
   subgoal premises prems for R B P Q
     by (tactic \<open>refreshability_tac false
       [@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars_commit :: cmt \<Rightarrow> var set"}]
diff --git a/thys/Pi_Calculus/Pi_cong.thy b/thys/Pi_Calculus/Pi_cong.thy
index 9800c537..5fef1caf 100644
--- a/thys/Pi_Calculus/Pi_cong.thy
+++ b/thys/Pi_Calculus/Pi_cong.thy
@@ -17,15 +17,9 @@ inductive cong :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<equiv>\<
 | "x \<noteq> y \<Longrightarrow> Res x (Res y P) \<equiv>\<^sub>\<pi> Res y (Res x P)"
 | "Res x Zero \<equiv>\<^sub>\<pi> Zero"
 | "Bang P \<equiv>\<^sub>\<pi> Par P (Bang P)"
-| cong_3: "x \<notin> FFVars Q \<Longrightarrow> Res x (Par P Q) \<equiv>\<^sub>\<pi> Par (Res x P) Q"
+| "x \<notin> FFVars Q \<Longrightarrow> Res x (Par P Q) \<equiv>\<^sub>\<pi> Par (Res x P) Q"
 
-binder_inductive cong
-  subgoal for R B \<sigma> x1 x2
-    apply simp
-    by (elim disj_forward case_prodE)
-      (auto simp: isPerm_def term.rrename_comps
-        | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-        | ((rule exI[of _ "\<sigma> _"])+; auto))+
+binder_inductive (no_auto_refresh) cong
   subgoal premises prems for R B P Q
     by (tactic \<open>refreshability_tac false
       [@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
@@ -61,7 +55,8 @@ inductive trans :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<rightar
 | "P \<rightarrow> Q \<Longrightarrow> Res x P \<rightarrow> Res x Q"
 | "P \<equiv>\<^sub>\<pi> P' \<Longrightarrow> P' \<rightarrow> Q' \<Longrightarrow> Q' \<equiv>\<^sub>\<pi> Q \<Longrightarrow> P \<rightarrow> Q"
 
-binder_inductive trans
+(* needs equiv_commute of vvsubst *)
+binder_inductive (no_auto_equiv, no_auto_refresh) trans
   subgoal for R B \<sigma> x1 x2
     apply simp
     apply (elim disj_forward exE)
diff --git a/thys/STLC/STLC.thy b/thys/STLC/STLC.thy
index bef92a5f..63e85b52 100644
--- a/thys/STLC/STLC.thy
+++ b/thys/STLC/STLC.thy
@@ -200,12 +200,22 @@ no_notation Set.member  ("(_/ : _)" [51, 51] 50)
 definition fresh :: "'a::var_terms_pre \<Rightarrow> ('a * 'b) fset \<Rightarrow> bool" ("(_/ \<sharp> _)" [51, 51] 50) where
   "fresh x \<Gamma> \<equiv> x |\<notin>| fst |`| \<Gamma>"
 
-lemma isin_rename: "bij f \<Longrightarrow> (f x, \<tau>) |\<in>| map_prod f id |`| \<Gamma> \<longleftrightarrow> (x, \<tau>) |\<in>| \<Gamma>"
-  by force
-
 abbreviation extend :: "('a * \<tau>) fset \<Rightarrow> 'a::var_terms_pre \<Rightarrow> \<tau> \<Rightarrow> ('a * \<tau>) fset" ("(_,_:_)" [52, 52, 52] 53) where
   "extend \<Gamma> a \<tau> \<equiv> finsert (a, \<tau>) \<Gamma>"
 
+lemma isin_rename[equiv]: "bij f \<Longrightarrow> (f x, \<tau>) |\<in>| map_prod f id |`| \<Gamma> \<longleftrightarrow> (x, \<tau>) |\<in>| \<Gamma>"
+by force
+
+lemma fresh_rename[equiv]: "bij f \<Longrightarrow> f x \<sharp> map_prod f id |`| \<Gamma> \<longleftrightarrow> x \<sharp> \<Gamma>"
+unfolding fresh_def by force
+
+lemma extend_equiv[equiv_commute]:
+  fixes f::"'a::var_terms_pre \<Rightarrow> 'a"
+  assumes "bij f"
+  shows
+    "map_prod f id |`| (\<Gamma>,x:\<tau>) = (map_prod f id |`| \<Gamma>),f x:\<tau>"
+    by simp
+
 inductive Step :: "'a::var_terms_pre terms \<Rightarrow> 'a terms \<Rightarrow> bool" (infixr "\<^bold>\<longrightarrow>" 25) where
   ST_Beta: "App (Abs x \<tau> e) e2 \<^bold>\<longrightarrow> tvsubst (tvVVr_tvsubst(x:=e2)) e"
 | ST_App: "e1 \<^bold>\<longrightarrow> e1' \<Longrightarrow> App e1 e2 \<^bold>\<longrightarrow> App e1' e2"
@@ -218,17 +228,10 @@ inductive Ty :: "('a::var_terms_pre * \<tau>) fset \<Rightarrow> 'a terms \<Righ
 lemma map_prod_comp0: "map_prod f1 f2 \<circ> map_prod f3 f4 = map_prod (f1 \<circ> f3) (f2 \<circ> f4)"
   using prod.map_comp by auto
 
-binder_inductive Ty
-  subgoal for R B \<sigma> x1 x2 x3
-    apply (elim disj_forward)
-      apply (auto simp: map_prod_comp0 terms.rrename_comps[OF _ _ bij_imp_bij_inv supp_inv_bound]
-    terms.rrename_ids)
-     apply force
-    apply (rule exI)
-    apply (rule conjI)
-     apply (rule refl)
-    apply (simp add: terms.rrename_comps[OF _ _ bij_imp_bij_inv supp_inv_bound] terms.rrename_ids)
-    unfolding fresh_def by force
+declare singl_bound[refresh_smalls] terms.Un_bound[refresh_smalls]
+  cinfinite_imp_infinite[OF terms_pre.UNIV_cinfinite, refresh_smalls]
+
+binder_inductive (no_auto_refresh) Ty
   subgoal for R B x1 x2 x3
     apply (rule exI[of _ B])
     unfolding fresh_def by auto
@@ -248,12 +251,9 @@ lemma provided:
     "map_prod f id |`| (\<Gamma>,x:\<tau>) = (map_prod f id |`| \<Gamma>),f x:\<tau>"
     (* freshness *)
     "\<lbrakk> x \<sharp> \<Gamma> ; \<Gamma>,x:\<tau> \<turnstile>\<^sub>t\<^sub>y e : \<tau>\<^sub>2 \<rbrakk> \<Longrightarrow> x \<notin> \<Union>(Basic_BNFs.fsts ` fset \<Gamma>)"
-   apply (simp add: assms isin_rename)
-  unfolding fresh_def
-     apply force
-  using assms(1) fimage_iff apply fastforce
-   apply simp
-  using fimage_iff by fastforce
+    using assms apply (auto simp only: equiv equiv_commute)
+    using fimage_iff
+    by (metis fresh_def fsts.cases)
 
 inductive_cases
   Ty_VarE[elim]: "\<Gamma> \<turnstile>\<^sub>t\<^sub>y Var x : \<tau>"
diff --git a/thys/Untyped_Lambda_Calculus/LC.thy b/thys/Untyped_Lambda_Calculus/LC.thy
index ea7615e2..c9c6192c 100644
--- a/thys/Untyped_Lambda_Calculus/LC.thy
+++ b/thys/Untyped_Lambda_Calculus/LC.thy
@@ -18,6 +18,9 @@ for
   vvsubst: vvsubst
   tvsubst: tvsubst
 
+thm term.permute
+thm term.rrename_tvsubst
+
 (****************************)
 (* DATATYPE-SPECIFIC CUSTOMIZATION  *)
 
@@ -28,7 +31,7 @@ instance var :: var_term_pre apply standard
   by (auto simp add: regularCard_var)
 
 instance var::cinf
-apply standard 
+apply standard
   subgoal apply(rule exI[of _ "inv Variable"])
   by (simp add: bij_Variable bij_is_inj)
   subgoal using infinite_var . .
@@ -58,8 +61,8 @@ lemma FFVars_tvsubst[simp]:
   using term.FVars_VVr apply (auto simp add: SSupp_def)
   by (smt (verit) singletonD term.FVars_VVr)
 
-lemma fsupp_le[simp]: 
-"fsupp (\<sigma>::var\<Rightarrow>var) \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set|" 
+lemma fsupp_le[simp]:
+"fsupp (\<sigma>::var\<Rightarrow>var) \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set|"
 by (simp add: finite_card_var fsupp_def supp_def)
 
 (* Enabling some simplification rules: *)
@@ -137,19 +140,19 @@ assumes f: "|SSupp f| <o |UNIV::var set|" and g: "|SSupp g| <o |UNIV::var set|"
 and eq: "(\<And>z. (z::var) \<in> FFVars P \<Longrightarrow> f z = g z)"
 shows "tvsubst f P = tvsubst g P"
 proof-
-  have fg: "|IImsupp f| <o |UNIV::var set|" "|IImsupp g| <o |UNIV::var set|" 
-    using f g  
-    by (simp_all add: IImsupp_def term.card_of_FFVars_bounds 
-       term_prevar_term_prevar_term_prevar_prodIDterm_prevar_prodIDsum_class.UN_bound 
-       term_prevar_term_prevar_term_prevar_prodIDterm_prevar_prodIDsum_class.Un_bound) 
-  have 0: "|IImsupp f \<union> IImsupp g| <o |UNIV::var set|" 
+  have fg: "|IImsupp f| <o |UNIV::var set|" "|IImsupp g| <o |UNIV::var set|"
+    using f g
+    by (simp_all add: IImsupp_def term.card_of_FFVars_bounds
+       term_prevar_term_prevar_term_prevar_prodIDterm_prevar_prodIDsum_class.UN_bound
+       term_prevar_term_prevar_term_prevar_prodIDterm_prevar_prodIDsum_class.Un_bound)
+  have 0: "|IImsupp f \<union> IImsupp g| <o |UNIV::var set|"
     using fg var_term_pre_class.Un_bound by blast
   show ?thesis using 0 eq apply(binder_induction P avoiding: "IImsupp f" "IImsupp g" rule: term.strong_induct)
     subgoal using fg by auto
-    subgoal using fg by simp  
+    subgoal using fg by simp
     subgoal using f g by simp
     subgoal using f g by simp
-    subgoal using f g fg apply simp unfolding IImsupp_def SSupp_def 
+    subgoal using f g fg apply simp unfolding IImsupp_def SSupp_def
     by auto metis .
 qed
 
@@ -185,7 +188,7 @@ lemma Lam_inject: "(Lam x e = Lam x' e') = (\<exists>f. bij f \<and> |supp (f::v
 
 lemma Lam_same_inject[simp]: "Lam (x::var) e = Lam x e' \<longleftrightarrow> e = e'"
 unfolding Lam_inject apply safe
-apply(rule term.rrename_cong_ids[symmetric]) 
+apply(rule term.rrename_cong_ids[symmetric])
 unfolding id_on_def by auto
 
 lemma bij_map_term_pre: "bij f \<Longrightarrow> |supp (f::var \<Rightarrow> var)| <o |UNIV::var set| \<Longrightarrow> bij (map_term_pre (id::var \<Rightarrow>var) f (rrename f) id)"
@@ -291,14 +294,72 @@ lemma SSupp_upd_bound:
       elim!: ordLeq_ordLess_trans[OF card_of_mono1 ordLess_ordLeq_trans[OF term_pre.Un_bound], rotated, of _ "{a}"]
       intro: card_of_mono1)
 
+lemma SSupp_upd_Var_bound[simp,intro!]: "|SSupp (Var(x::'a := t))| <o |UNIV::'a::var_term_pre set|"
+  unfolding VVr_eq_Var fun_upd_def SSupp_def
+  by (auto split: if_splits) (metis (mono_tags, lifting) card_of_subset_bound insert_subset mem_Collect_eq subsetI term.card_of_FFVars_bounds term.set(1))
+
+lemma tusubst_equiv[equiv]:
+  fixes \<sigma>::"'a::var_term_pre \<Rightarrow> 'a"
+  assumes "bij \<sigma>" "|supp \<sigma>| <o |UNIV::'a set|"
+  shows "rrename \<sigma> (tvsubst (Var(x := t')) t) = tvsubst (Var(\<sigma> x := rrename \<sigma> t')) (rrename \<sigma> t)"
+  apply (rule trans)
+   apply (rule trans[OF comp_apply[symmetric] term.rrename_tvsubst[THEN fun_cong]])
+     apply (rule assms)+
+   apply (rule SSupp_upd_Var_bound)
+  apply (unfold comp_def fun_upd_def)
+  apply (rule arg_cong2[OF _ refl, of _ _ tvsubst])
+  apply (rule ext)
+  apply (rule case_split)
+   apply (rule sym)
+   apply (rule trans[OF if_P])
+    apply (erule sym)
+   apply (subst if_P)
+    apply (erule subst)
+    apply (rule inv_simp1)
+    apply (rule assms)
+   apply (rule refl)
+  apply (subst if_not_P)
+   apply (erule contrapos_nn)
+   apply hypsubst_thin
+   apply (rule inv_simp2)
+   apply (rule assms)
+  apply (subst if_not_P)
+   apply (erule contrapos_nn)
+   apply (erule sym)
+  apply (rule trans)
+   apply (rule term.permute)
+    apply (rule assms)+
+  apply (rule arg_cong[of _ _ Var])
+  apply (rule inv_simp2)
+  apply (rule assms)
+  done
+
+lemma fun_upd_equiv[equiv]:
+  fixes \<sigma>::"'a::var_term_pre \<Rightarrow> 'a"
+  assumes "bij \<sigma>" "|supp \<sigma>| <o |UNIV::'a set|"
+    and equiv: "\<And>x. rrename \<sigma> (f x) = f (\<sigma> x)"
+  shows "rrename \<sigma> ((f(x := t)) y) = (f(\<sigma> x := rrename \<sigma> t)) (\<sigma> y)"
+  apply (unfold comp_def fun_upd_def)
+  apply (rule case_split)
+   apply (subst if_P)
+    apply assumption
+   apply hypsubst_thin
+   apply (subst if_P)
+    apply (rule refl)
+   apply (rule refl)
+  apply (unfold if_not_P)
+  apply (subst if_not_P)
+   apply (erule contrapos_nn)
+   apply (erule injD[OF bij_is_inj, rotated])
+   apply (rule assms)
+  apply (rule equiv)
+  done
+
 corollary SSupp_upd_VVr_bound[simp,intro!]: "|SSupp (VVr(a:=(t::trm)))| <o |UNIV::var set|"
   apply (rule iffD2[OF SSupp_upd_bound])
   apply (rule term.SSupp_VVr_bound)
   done
 
-lemma SSupp_upd_Var_bound[simp,intro!]: "|SSupp (Var(a:=(t::trm)))| <o |UNIV::var set|"
-using SSupp_upd_VVr_bound by auto
-
 lemma supp_swap_bound[simp,intro!]: "|supp (id(x::var := xx, xx := x))| <o |UNIV:: var set|"
 by (simp add: cinfinite_imp_infinite supp_swap_bound term.UNIV_cinfinite)
 
@@ -342,7 +403,7 @@ lemma IImsupp_Var: "IImsupp (Var(x := e)) \<subseteq> FFVars e \<union> {x}"
 unfolding LC.IImsupp_def LC.SSupp_def by auto
 
 lemma IImsupp_Var': "y \<noteq> x \<and> y \<notin> FFVars e \<Longrightarrow> y \<notin> IImsupp (Var(x := e))"
-using IImsupp_Var by auto 
+using IImsupp_Var by auto
 
 lemma IImsupp_rrename_su:
 assumes s[simp]: "bij (\<sigma>::var\<Rightarrow>var)" "|supp \<sigma>| <o  |UNIV:: var set|"
@@ -442,11 +503,11 @@ qed
 
 (* Unary (term-for-var) substitution versus renaming: *)
 
-lemma supp_SSupp_Var_le[simp]: "SSupp (Var \<circ> \<sigma>) = supp \<sigma>" 
+lemma supp_SSupp_Var_le[simp]: "SSupp (Var \<circ> \<sigma>) = supp \<sigma>"
 unfolding supp_def SSupp_def by simp
 
-lemma rrename_eq_tvsubst_Var: 
-assumes "bij (\<sigma>::var\<Rightarrow>var)" "|supp \<sigma>| <o |UNIV::var set|" 
+lemma rrename_eq_tvsubst_Var:
+assumes "bij (\<sigma>::var\<Rightarrow>var)" "|supp \<sigma>| <o |UNIV::var set|"
 shows "rrename \<sigma> = tvsubst (Var o \<sigma>)"
 proof
   fix t
@@ -459,8 +520,8 @@ proof
     then show ?case by (simp add: assms IImsupp_def disjoint_iff not_in_supp_alt)
   qed (auto simp: assms)
 qed
-     
-lemma rrename_eq_tvsubst_Var': 
+
+lemma rrename_eq_tvsubst_Var':
 "bij (\<sigma>::var\<Rightarrow>var) \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> rrename \<sigma> e = tvsubst (Var o \<sigma>) e"
 using rrename_eq_tvsubst_Var by auto
 
@@ -647,8 +708,8 @@ term "permutFvars (\<lambda>f t. rrename t f) FFVars"
 
 lemma swappingFvars_swap_FFVars: "swappingFvars swap FFVars"
 unfolding swappingFvars_def apply auto
-  apply (metis id_swapTwice rrename_o_swap term.rrename_ids) 
-  using sw_invol2 apply metis 
+  apply (metis id_swapTwice rrename_o_swap term.rrename_ids)
+  using sw_invol2 apply metis
   by (metis (no_types, lifting) image_iff sw_invol2)
 
 lemma nswapping_swap: "nswapping swap"
@@ -658,7 +719,7 @@ by (metis id_swapTwice2 rrename_o_swap)
 
 lemma permutFvars_rrename_FFVar: "permutFvars (\<lambda>t f. rrename f (t::trm)) FFVars"
 unfolding permutFvars_def apply auto
-  apply (simp add: finite_iff_le_card_var fsupp_def supp_def term.rrename_comps) 
+  apply (simp add: finite_iff_le_card_var fsupp_def supp_def term.rrename_comps)
   apply (simp add: finite_iff_le_card_var fsupp_def supp_def)
   apply (simp add: finite_iff_le_card_var fsupp_def image_in_bij_eq supp_def) .
 
@@ -680,7 +741,7 @@ by (simp add: fsupp_supp permut_rrename toPerm_toSwp)
 (* *)
 (* Substitution from a sequence (here, a list) *)
 
-(* "making" the substitution function that maps each xs_i to es_i; only 
+(* "making" the substitution function that maps each xs_i to es_i; only
 meaningful if xs is non-repetitive *)
 definition "mkSubst xs es \<equiv> \<lambda>x. if distinct xs \<and> x \<in> set xs then nth es (theN xs x) else Var x"
 
@@ -691,7 +752,7 @@ lemma mkSubst_idle[simp]: "\<not> distinct xs \<or> \<not> x \<in> set xs \<Long
 unfolding mkSubst_def by auto
 
 lemma card_set_var: "|set xs| <o |UNIV::var set|"
-by (simp add: infinite_var) 
+by (simp add: infinite_var)
 
 lemma SSupp_mkSubst[simp,intro]: "|SSupp (mkSubst xs es)| <o |UNIV::var set|"
 proof-
@@ -700,11 +761,11 @@ proof-
   thus ?thesis by (simp add: card_of_subset_bound card_set_var)
 qed
 
-lemma mkSubst_map_rrename: 
-assumes s: "bij (\<sigma>::var\<Rightarrow>var)" "|supp \<sigma>| <o |UNIV::var set|" 
+lemma mkSubst_map_rrename:
+assumes s: "bij (\<sigma>::var\<Rightarrow>var)" "|supp \<sigma>| <o |UNIV::var set|"
 and l: "length es2 = length xs"
 shows "mkSubst (map \<sigma> xs) (map (rrename \<sigma>) es2) \<circ> \<sigma> = rrename \<sigma> \<circ> mkSubst xs es2"
-proof(rule ext)  
+proof(rule ext)
   fix x
   show "(mkSubst (map \<sigma> xs) (map (rrename \<sigma>) es2) \<circ> \<sigma>) x = (rrename \<sigma> \<circ> mkSubst xs es2) x"
   proof(cases "distinct xs \<and> x \<in> set xs")
@@ -712,7 +773,7 @@ proof(rule ext)
     hence F: "\<not> distinct (map \<sigma> xs) \<or> \<not> \<sigma> x \<in> set (map \<sigma> xs)"
     using s by auto
     thus ?thesis using F False
-    unfolding o_def apply(subst mkSubst_idle) 
+    unfolding o_def apply(subst mkSubst_idle)
       subgoal by auto
       subgoal using s by auto .
   next
@@ -721,43 +782,43 @@ proof(rule ext)
     hence T: "distinct (map \<sigma> xs)" and Ti: "\<sigma> x = nth (map \<sigma> xs) i"
     using s by auto
     thus ?thesis using T Tr
-    unfolding o_def Ti apply(subst mkSubst_nth) 
+    unfolding o_def Ti apply(subst mkSubst_nth)
       subgoal by auto
-      subgoal using i unfolding Tri by auto 
+      subgoal using i unfolding Tri by auto
       subgoal using l i unfolding Tri by auto .
   qed
 qed
 
-lemma mkSubst_map_rrename_inv: 
+lemma mkSubst_map_rrename_inv:
 assumes "bij (\<sigma>::var\<Rightarrow>var)" "|supp \<sigma>| <o |UNIV::var set|" "length es2 = length xs"
 shows "mkSubst (map \<sigma> xs) (map (rrename \<sigma>) es2) = rrename \<sigma> \<circ> mkSubst xs es2 o inv \<sigma>"
 unfolding mkSubst_map_rrename[OF assms, symmetric] using assms unfolding fun_eq_iff by auto
 
-lemma card_SSupp_itvsubst_mkSubst_rrename_inv: 
-"bij (\<sigma>::var\<Rightarrow>var) \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> 
- length es = length xs \<Longrightarrow> 
+lemma card_SSupp_itvsubst_mkSubst_rrename_inv:
+"bij (\<sigma>::var\<Rightarrow>var) \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
+ length es = length xs \<Longrightarrow>
 |SSupp (tvsubst (rrename \<sigma> \<circ> mkSubst xs es \<circ> inv \<sigma>) \<circ> (Var \<circ> \<sigma>))| <o |UNIV::var set|"
 by (metis SSupp_tvsubst_bound SSupp_mkSubst mkSubst_map_rrename_inv supp_SSupp_Var_le)
 
-lemma card_SSupp_mkSubst_rrename_inv: 
-"bij (\<sigma>::var\<Rightarrow>var) \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> 
- length es = length xs \<Longrightarrow> 
+lemma card_SSupp_mkSubst_rrename_inv:
+"bij (\<sigma>::var\<Rightarrow>var) \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
+ length es = length xs \<Longrightarrow>
  |SSupp (rrename \<sigma> \<circ> mkSubst xs es \<circ> inv \<sigma>)| <o |UNIV::var set|"
 by (metis SSupp_mkSubst mkSubst_map_rrename_inv)
 
-lemma mkSubst_smap: "bij f \<Longrightarrow> distinct xs \<Longrightarrow> z \<in> set xs \<Longrightarrow> 
- length es = length xs \<Longrightarrow> 
+lemma mkSubst_smap: "bij f \<Longrightarrow> distinct xs \<Longrightarrow> z \<in> set xs \<Longrightarrow>
+ length es = length xs \<Longrightarrow>
  mkSubst (map f xs) es (f z) = mkSubst xs es z"
-by (metis bij_distinct_smap distinct_Ex1 length_map mkSubst_nth nth_map) 
+by (metis bij_distinct_smap distinct_Ex1 length_map mkSubst_nth nth_map)
 
 
 (* *)
 
-lemma Lam_eq_tvsubst: 
+lemma Lam_eq_tvsubst:
 assumes il: "Lam (x::var) e1 = Lam x' e1'"
 shows "tvsubst (Var (x:=e2)) e1 = tvsubst (Var (x':=e2)) e1'"
 proof-
-  obtain f where f: "bij f" "|supp f| <o |UNIV::var set|" "id_on (FFVars (Lam x e1)) f" 
+  obtain f where f: "bij f" "|supp f| <o |UNIV::var set|" "id_on (FFVars (Lam x e1)) f"
   and 0: "x' = f x" "e1' = rrename f e1" using il[unfolded Lam_inject] by auto
   show ?thesis unfolding 0 apply(subst rrename_eq_tvsubst_Var')
     subgoal by fact subgoal by fact
@@ -767,7 +828,7 @@ proof-
       subgoal apply(rule tvsubst_cong)
         subgoal by simp
         subgoal by (simp add: SSupp_tvsubst_bound f(2))
-        subgoal apply simp 
+        subgoal apply simp
      subgoal using f(1) f(3) id_onD by fastforce . . . .
 qed
 
@@ -780,9 +841,9 @@ thm Lam_inject[no_vars]
 
 lemma Lam_inject_strong:
 assumes "Lam (x::var) e = Lam x' e'"
-shows "\<exists>f. bij f \<and> |supp f| <o |UNIV::var set| \<and>  
+shows "\<exists>f. bij f \<and> |supp f| <o |UNIV::var set| \<and>
    id_on (- {x,x'}) f \<and> id_on (FFVars (Lam x e)) f \<and>
-   f x = x' \<and> rrename f e = e'" 
+   f x = x' \<and> rrename f e = e'"
 apply(rule exI[of _ "id(x := x', x' := x)"])
 using assms unfolding Lam_inject_swap apply safe
 unfolding id_on_def by auto (metis fun_upd_twist)
@@ -790,10 +851,10 @@ unfolding id_on_def by auto (metis fun_upd_twist)
 
 lemma Lam_inject_strong':
 assumes il: "Lam (x::var) e = Lam x' e'" and z: "z \<notin> FFVars (Lam x e) \<union> FFVars (Lam x' e')"
-shows 
-"\<exists>f f'. 
-   bij f \<and> |supp f| <o |UNIV::var set| \<and> id_on (- {x,z}) f \<and> id_on (FFVars (Lam x e)) f \<and> f x = z \<and> 
-   bij f' \<and> |supp f'| <o |UNIV::var set| \<and> id_on (- {x',z}) f' \<and> id_on (FFVars (Lam x' e')) f' \<and> f' x' = z \<and> 
+shows
+"\<exists>f f'.
+   bij f \<and> |supp f| <o |UNIV::var set| \<and> id_on (- {x,z}) f \<and> id_on (FFVars (Lam x e)) f \<and> f x = z \<and>
+   bij f' \<and> |supp f'| <o |UNIV::var set| \<and> id_on (- {x',z}) f' \<and> id_on (FFVars (Lam x' e')) f' \<and> f' x' = z \<and>
    rrename f e = rrename f' e'"
 proof-
   define f where "f = id(x := z, z := x)"
@@ -802,15 +863,15 @@ proof-
   define f' where "f' = id(x' := z, z := x')"
   have f': "bij f' \<and> |supp f'| <o |UNIV::var set| \<and> id_on (- {x',z}) f' \<and> id_on (FFVars (Lam x' e')) f' \<and> f' x' = z"
   using z unfolding f'_def id_on_def by auto
- 
+
   obtain g where g: "bij g \<and> |supp g| <o |UNIV::var set| \<and> id_on (FFVars (Lam x e)) g \<and> g x = x'" and ge: "e' = rrename g e"
   using il unfolding Lam_inject by auto
 
-  have ff': "rrename f e = rrename f' e'" 
+  have ff': "rrename f e = rrename f' e'"
   unfolding f_def f'_def ge unfolding f_def f'_def using g apply(subst term.rrename_comps)
     subgoal by auto  subgoal by auto subgoal by auto subgoal by auto
     subgoal apply(rule rrename_cong) using g
-      subgoal by auto  subgoal by auto subgoal by auto 
+      subgoal by auto  subgoal by auto subgoal by auto
       subgoal using term_pre.supp_comp_bound by auto
       subgoal using term_pre.supp_comp_bound z unfolding id_on_def by auto . .
 
@@ -821,7 +882,7 @@ qed
 
 lemma trm_rrename_induct[case_names Var App Lam]:
 assumes VVar: "\<And>x. P (Var (x::var))"
-and AApp: "\<And>e1 e2. P e1 \<Longrightarrow> P e2 \<Longrightarrow> P (App e1 e2)" 
+and AApp: "\<And>e1 e2. P e1 \<Longrightarrow> P e2 \<Longrightarrow> P (App e1 e2)"
 and LLam: "\<And>x e. (\<And>f. bij f \<Longrightarrow> |supp f| <o |UNIV::var set| \<Longrightarrow> P (rrename f e)) \<Longrightarrow> P (Lam x e)"
 shows "P t"
 proof-
@@ -842,110 +903,110 @@ qed
 
 (* RECURSOR *)
 
-locale LC_Rec = 
+locale LC_Rec =
 fixes B :: "'b set"
-and VarB :: "var \<Rightarrow> 'b" 
+and VarB :: "var \<Rightarrow> 'b"
 and AppB :: "'b \<Rightarrow> 'b \<Rightarrow> 'b"
 and LamB :: "var \<Rightarrow> 'b \<Rightarrow> 'b"
 and renB :: "(var \<Rightarrow> var) \<Rightarrow> 'b \<Rightarrow> 'b"
 and FVarsB :: "'b \<Rightarrow> var set"
-assumes 
+assumes
 (* closedness: *)
 VarB_B[simp,intro]: "\<And>x. VarB x \<in> B"
-and 
+and
 AppB_B[simp,intro]: "\<And>b1 b2. {b1,b2} \<subseteq> B \<Longrightarrow> AppB b1 b2 \<in> B"
-and 
+and
 LamB_B[simp,intro]: "\<And>x b. b \<in>  B \<Longrightarrow> LamB x b \<in> B"
-and 
+and
 renB_B[simp]: "\<And>\<sigma> b. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> b \<in> B \<Longrightarrow> renB \<sigma> b \<in> B"
-and 
+and
 (* proper axioms: *)
 renB_id[simp,intro]: "\<And>b. b \<in> B \<Longrightarrow> renB id b = b"
-and 
-renB_comp[simp,intro]: "\<And>b \<sigma> \<tau>. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> 
+and
+renB_comp[simp,intro]: "\<And>b \<sigma> \<tau>. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
     bij \<tau> \<Longrightarrow> |supp \<tau>| <o |UNIV::var set| \<Longrightarrow> b \<in> B \<Longrightarrow> renB (\<tau> o \<sigma>) b = renB \<tau> (renB \<sigma> b)"
-and 
-renB_cong[simp]: "\<And>\<sigma> b. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> 
-   (\<forall>x \<in> FVarsB b. \<sigma> x = x) \<Longrightarrow> 
+and
+renB_cong[simp]: "\<And>\<sigma> b. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
+   (\<forall>x \<in> FVarsB b. \<sigma> x = x) \<Longrightarrow>
    renB \<sigma> b = b"
-(* and 
-NB: This is redundant:  
-renB_FVarsB[simp]: "\<And>\<sigma> x b. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> 
+(* and
+NB: This is redundant:
+renB_FVarsB[simp]: "\<And>\<sigma> x b. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
    x \<in> FVarsB (renB \<sigma> b) \<longleftrightarrow> inv \<sigma> x \<in> FVarsB b"
 *)
-and 
+and
 (* *)
 renB_VarB[simp]: "\<And>\<sigma> x. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> renB \<sigma> (VarB x) = VarB (\<sigma> x)"
-and 
-renB_AppB[simp]: "\<And>\<sigma> b1 b2. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> {b1,b2} \<subseteq> B \<Longrightarrow> 
+and
+renB_AppB[simp]: "\<And>\<sigma> b1 b2. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> {b1,b2} \<subseteq> B \<Longrightarrow>
    renB \<sigma> (AppB b1 b2) = AppB (renB \<sigma> b1) (renB \<sigma> b2)"
-and 
-renB_LamB[simp]: "\<And>\<sigma> x b. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> b \<in> B \<Longrightarrow> 
+and
+renB_LamB[simp]: "\<And>\<sigma> x b. bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> b \<in> B \<Longrightarrow>
    renB \<sigma> (LamB x b) = LamB (\<sigma> x) (renB \<sigma> b)"
 (* *)
-and 
+and
 FVarsB_VarB: "\<And>x. FVarsB (VarB x) \<subseteq> {x}"
-and 
+and
 FVarsB_AppB: "\<And>b1 b2. {b1,b2} \<subseteq> B \<Longrightarrow> FVarsB (AppB b1 b2) \<subseteq> FVarsB b1 \<union> FVarsB b2"
-and 
+and
 FVarsB_LamB: "\<And>x b. b \<in> B \<Longrightarrow> FVarsB (LamB x b) \<subseteq> FVarsB b - {x}"
-begin 
+begin
 
 lemma not_in_FVarsB_LamB: "b \<in> B \<Longrightarrow> x \<notin> FVarsB (LamB x b)"
 using FVarsB_LamB by auto
 
-lemma LamB_inject_strong_rev: 
-assumes bb': "{b,b'} \<subseteq> B" and 
-x': "x' = x \<or> x' \<notin> FVarsB b" and 
-f: "bij f" "|supp f| <o |UNIV::var set|" 
+lemma LamB_inject_strong_rev:
+assumes bb': "{b,b'} \<subseteq> B" and
+x': "x' = x \<or> x' \<notin> FVarsB b" and
+f: "bij f" "|supp f| <o |UNIV::var set|"
 "id_on (- {x, x'}) f" "f x = x'" and r: "renB f b = b'"
 shows "LamB x b = LamB x' b'"
 proof-
   have id: "id_on (FVarsB (LamB x b)) f"
   using f FVarsB_LamB bb' x' unfolding id_on_def by auto
   have "LamB x b = renB f (LamB x b)"
-  apply(rule sym) apply(rule renB_cong) using f bb' FVarsB_LamB unfolding id_on_def 
+  apply(rule sym) apply(rule renB_cong) using f bb' FVarsB_LamB unfolding id_on_def
   using id unfolding id_on_def by auto
   also have "\<dots> = LamB x' b'" apply(subst renB_LamB) using f r bb' by auto
   finally show ?thesis .
 qed
 
-lemma LamB_inject_strong'_rev: 
-assumes bb': "{b,b'} \<subseteq> B"  
+lemma LamB_inject_strong'_rev:
+assumes bb': "{b,b'} \<subseteq> B"
 and z: "z = x \<or> z \<notin> FVarsB b" "z = x' \<or> z \<notin> FVarsB b'"
-and f: "bij f" "|supp f| <o |UNIV::var set|" "id_on (- {x, z}) f" "f x = z" 
-and f': "bij f'" "|supp f'| <o |UNIV::var set|" "id_on (- {x', z}) f'" "f' x' = z" 
+and f: "bij f" "|supp f| <o |UNIV::var set|" "id_on (- {x, z}) f" "f x = z"
+and f': "bij f'" "|supp f'| <o |UNIV::var set|" "id_on (- {x', z}) f'" "f' x' = z"
 and r: "renB f b = renB f' b'"
-shows "LamB x b = LamB x' b'" 
+shows "LamB x b = LamB x' b'"
 proof-
   define c where c: "c = renB f b"
   have c': "c = renB f' b'" unfolding c r ..
-  have "LamB x b = LamB z c"  
-  apply(rule LamB_inject_strong_rev[of _ _ _ _ f]) 
+  have "LamB x b = LamB z c"
+  apply(rule LamB_inject_strong_rev[of _ _ _ _ f])
   using assms FVarsB_LamB id_on_def unfolding c by auto
-  also have "LamB z c = LamB x' b'"  
-  apply(rule sym, rule LamB_inject_strong_rev[of _ _ _ _ f']) 
+  also have "LamB z c = LamB x' b'"
+  apply(rule sym, rule LamB_inject_strong_rev[of _ _ _ _ f'])
   using assms FVarsB_LamB id_on_def unfolding c by auto
   finally show ?thesis .
 qed
 
-(* NB: 
-We obtain a more general recursor if we replace renB_cong with LamB_inject_strong_rev; 
-and an even more general one if we replace it with LamB_inject_strong'_rev. 
+(* NB:
+We obtain a more general recursor if we replace renB_cong with LamB_inject_strong_rev;
+and an even more general one if we replace it with LamB_inject_strong'_rev.
 *)
 
-definition morFromTrm where 
-"morFromTrm H \<equiv> 
- (\<forall>e. H e \<in> B) \<and>  
- (\<forall>x. H (Var x) = VarB x) \<and> 
- (\<forall>e1 e2. H (App e1 e2) = AppB (H e1) (H e2)) \<and> 
- (\<forall>x e. H (Lam x e) = LamB x (H e)) \<and> 
- (\<forall>\<sigma> e. bij \<sigma> \<and> |supp \<sigma>| <o |UNIV::var set| \<longrightarrow> H (rrename \<sigma> e) = renB \<sigma> (H e)) \<and> 
+definition morFromTrm where
+"morFromTrm H \<equiv>
+ (\<forall>e. H e \<in> B) \<and>
+ (\<forall>x. H (Var x) = VarB x) \<and>
+ (\<forall>e1 e2. H (App e1 e2) = AppB (H e1) (H e2)) \<and>
+ (\<forall>x e. H (Lam x e) = LamB x (H e)) \<and>
+ (\<forall>\<sigma> e. bij \<sigma> \<and> |supp \<sigma>| <o |UNIV::var set| \<longrightarrow> H (rrename \<sigma> e) = renB \<sigma> (H e)) \<and>
  (\<forall>e. FVarsB (H e) \<subseteq> FFVars e)"
 
 (* *)
 
-inductive R where 
+inductive R where
 Var: "R (Var x) (VarB x)"
 |
 App: "R e1 b1 \<Longrightarrow> R e2 b2 \<Longrightarrow> R (App e1 e2) (AppB b1 b2)"
@@ -959,27 +1020,27 @@ apply safe
   subgoal using R.cases by fastforce
   subgoal by (auto intro: R.intros) .
 
-lemma R_App_elim: 
+lemma R_App_elim:
 assumes "R (App e1 e2) b"
 shows "\<exists>b1 b2. R e1 b1 \<and> R e2 b2 \<and> b = AppB b1 b2"
 by (metis App_inject R.simps assms term.distinct(1) term.distinct(4))
 
-lemma R_Lam_elim: 
+lemma R_Lam_elim:
 assumes "R (Lam x e) b"
 shows "\<exists>x' e' b'. R e' b' \<and> Lam x e = Lam x' e' \<and> b = LamB x' b'"
 using assms by (cases rule: R.cases) auto
 
-lemma R_total: 
+lemma R_total:
 "\<exists>b. R e b"
 apply(induct e) by (auto intro: R.intros)
 
-lemma R_B: 
+lemma R_B:
 "R e b \<Longrightarrow> b \<in> B"
 apply(induct rule: R.induct) by auto
 
-lemma R_main: 
-"(\<forall>b b'. R e b \<longrightarrow> R e b' \<longrightarrow> b = b') \<and> 
- (\<forall>b. R e b \<longrightarrow> FVarsB b \<subseteq> FFVars e) \<and> 
+lemma R_main:
+"(\<forall>b b'. R e b \<longrightarrow> R e b' \<longrightarrow> b = b') \<and>
+ (\<forall>b. R e b \<longrightarrow> FVarsB b \<subseteq> FFVars e) \<and>
  (\<forall>b f. R e b \<and> bij f \<and> |supp f| <o |UNIV::var set|
         \<longrightarrow> R (rrename f e) (renB f b))"
 proof(induct e rule: trm_rrename_induct)
@@ -987,12 +1048,12 @@ proof(induct e rule: trm_rrename_induct)
   then show ?case using FVarsB_VarB by auto
 next
   case (App e1 e2)
-  then show ?case apply safe 
+  then show ?case apply safe
     subgoal by (metis R_App_elim)
-    subgoal by simp (smt (verit, del_insts) FVarsB_AppB R_App_elim 
+    subgoal by simp (smt (verit, del_insts) FVarsB_AppB R_App_elim
       R_B Un_iff bot.extremum insert_Diff insert_subset)
-    subgoal apply(drule R_App_elim) 
-      by (smt (verit, del_insts) R.simps R_B bot.extremum insert_subset renB_AppB 
+    subgoal apply(drule R_App_elim)
+      by (smt (verit, del_insts) R.simps R_B bot.extremum insert_subset renB_AppB
       term.permute(2)) .
 next
   case (Lam x t)
@@ -1003,7 +1064,7 @@ next
   note Lam33 = Lam3[of id, simplified]
 
   show ?case proof safe
-    fix b1 b2 assume RLam: "R (Lam x t) b1" "R (Lam x t) b2" 
+    fix b1 b2 assume RLam: "R (Lam x t) b1" "R (Lam x t) b2"
     then obtain x1' t1' b1' x2' t2' b2'
     where 1: "R t1' b1'" "Lam x t = Lam x1' t1'" "b1 = LamB x1' b1'"
     and   2: "R t2' b2'" "Lam x t = Lam x2' t2'" "b2 = LamB x2' b2'"
@@ -1014,43 +1075,43 @@ next
 
     have "|{x,x1',x2'} \<union> FFVars t \<union> FFVars t1' \<union> FFVars t2'| <o |UNIV::var set|"
     by (metis Un_insert_right singl_bound sup_bot_right term.set_bd_UNIV var_term_pre_class.Un_bound)
-    then obtain z where z: 
-    "z \<notin> {x,x1',x2'} \<union> FFVars t \<union> FFVars t1' \<union> FFVars t2'" 
+    then obtain z where z:
+    "z \<notin> {x,x1',x2'} \<union> FFVars t \<union> FFVars t1' \<union> FFVars t2'"
     by (meson exists_fresh)
 
-    obtain f1 f1' where 
+    obtain f1 f1' where
     f1: "bij f1" "|supp f1| <o |UNIV::var set|"
-       "id_on (- {x, z}) f1 \<and> id_on (FFVars (Lam x t)) f1" and 
+       "id_on (- {x, z}) f1 \<and> id_on (FFVars (Lam x t)) f1" and
     f1': "bij f1'" "|supp f1'| <o |UNIV::var set|"
        "id_on (- {x1', z}) f1' \<and> id_on (FFVars (Lam x1' t1')) f1'"
-    and z1: "f1 x = z" "f1' x1' = z"  
-    and f1f1': "rrename f1 t = rrename f1' t1'"   
+    and z1: "f1 x = z" "f1' x1' = z"
+    and f1f1': "rrename f1 t = rrename f1' t1'"
     using z Lam_inject_strong'[OF 1(2), of z] by auto
 
     have if1': "bij (inv f1' o f1)" "|supp (inv f1' o f1)| <o |UNIV::var set|"
     by (auto simp add: f1 f1' term_pre.supp_comp_bound)
 
-    have t1': "t1' = rrename (inv f1' o f1) t"  
-    using f1f1' by (metis (mono_tags, lifting) bij_imp_bij_inv f1 f1' 
+    have t1': "t1' = rrename (inv f1' o f1) t"
+    using f1f1' by (metis (mono_tags, lifting) bij_imp_bij_inv f1 f1'
        inv_o_simp1 supp_inv_bound term.rrename_comps term.rrename_ids)
 
     have fvb1': "FVarsB b1' \<subseteq> FFVars t1'"
     using Lam2[OF if1', unfolded t1'[symmetric], OF 1(1)] .
 
-    obtain f2 f2' where 
+    obtain f2 f2' where
     f2: "bij f2" "|supp f2| <o |UNIV::var set|"
-      "id_on (- {x, z}) f2 \<and> id_on (FFVars (Lam x t)) f2" and 
+      "id_on (- {x, z}) f2 \<and> id_on (FFVars (Lam x t)) f2" and
     f2': "bij f2'" "|supp f2'| <o |UNIV::var set|"
       "id_on (- {x2', z}) f2' \<and> id_on (FFVars (Lam x2' t2')) f2'"
-    and z2: "f2 x = z" "f2' x2' = z"  
-    and f2f2': "rrename f2 t = rrename f2' t2'"   
+    and z2: "f2 x = z" "f2' x2' = z"
+    and f2f2': "rrename f2 t = rrename f2' t2'"
     using z Lam_inject_strong'[OF 2(2), of z] by auto
 
     have if2': "bij (inv f2' o f2)" "|supp (inv f2' o f2)| <o |UNIV::var set|"
     by (auto simp add: f2 f2' term_pre.supp_comp_bound)
 
-    have t2': "t2' = rrename (inv f2' o f2) t" 
-    using f2f2' by (metis (mono_tags, lifting) bij_imp_bij_inv f2 f2' 
+    have t2': "t2' = rrename (inv f2' o f2) t"
+    using f2f2' by (metis (mono_tags, lifting) bij_imp_bij_inv f2 f2'
       inv_o_simp1 supp_inv_bound term.rrename_comps term.rrename_ids)
 
     have fvb2': "FVarsB b2' \<subseteq> FFVars t2'"
@@ -1059,59 +1120,59 @@ next
     define ff2' where "ff2' = f1 o (inv f2) o f2'"
 
     have ff2': "bij ff2'" "|supp ff2'| <o |UNIV::var set|"
-       "id_on (- {x2', z}) ff2' \<and> id_on (FFVars (Lam x2' t2')) ff2'" 
-    unfolding ff2'_def using f1 f2 f2'  
-      subgoal by auto 
+       "id_on (- {x2', z}) ff2' \<and> id_on (FFVars (Lam x2' t2')) ff2'"
+    unfolding ff2'_def using f1 f2 f2'
+      subgoal by auto
       subgoal unfolding ff2'_def using f1 f2 f2' by (simp add: term_pre.supp_comp_bound)
       subgoal unfolding ff2'_def using f1 f2 f2' unfolding id_on_def by simp (metis inv_simp1 z1(1) z2(1)) .
 
     have zz2: "ff2' x2' = z"
     by (metis comp_def f2 ff2'_def inv_simp1 z1(1) z2(1) z2(2))
- 
-    have rew1: "rrename f1' (rrename (inv f1' \<circ> f1) t) = rrename f1 t" 
+
+    have rew1: "rrename f1' (rrename (inv f1' \<circ> f1) t) = rrename f1 t"
     using f1f1' t1' by auto
 
-    have rew2: "rrename ff2' (rrename (inv f2' \<circ> f2) t) = rrename f1 t" 
+    have rew2: "rrename ff2' (rrename (inv f2' \<circ> f2) t) = rrename f1 t"
     by (smt (verit, del_insts) bij_betw_imp_inj_on bij_imp_bij_inv bij_o f1(1) f1(2) f2'(1) f2'(2) f2(1) f2(2) f2f2' ff2'_def o_inv_o_cancel supp_inv_bound term.rrename_comps term_pre.supp_comp_bound)
- 
-    show "b1 = b2" unfolding 1(3) 2(3) 
+
+    show "b1 = b2" unfolding 1(3) 2(3)
     apply(rule LamB_inject_strong'_rev[OF b12', of z _ _ f1' ff2'])
       subgoal using z fvb1' by auto
       subgoal using z fvb2' by auto
       subgoal using f1' by auto  subgoal using f1' by auto
       subgoal using f1' by auto  subgoal using z1 by auto
       subgoal using ff2' by auto  subgoal using ff2' by auto
-      subgoal using ff2' by auto  subgoal using zz2 by auto 
-      subgoal apply(rule Lam1[OF f1(1,2)])  
+      subgoal using ff2' by auto  subgoal using zz2 by auto
+      subgoal apply(rule Lam1[OF f1(1,2)])
         subgoal using Lam3[OF if1' 1(1)[unfolded t1'] f1'(1,2), unfolded rew1] .
         subgoal using Lam3[OF if2' 2(1)[unfolded t2'] ff2'(1,2), unfolded rew2] . . .
   (* *)
   next
-    fix b y 
+    fix b y
     assume R: "R (Lam x t) b" and yy: "y \<in> FVarsB b"
     then obtain x' t' b'
-    where 0: "R t' b'" "Lam x t = Lam x' t'" "b = LamB x' b'" 
+    where 0: "R t' b'" "Lam x t = Lam x' t'" "b = LamB x' b'"
     using R_Lam_elim by metis
 
     have b': "b' \<in>  B"
     using 0(1,3) R_B by auto
 
-    have y: "y \<noteq> x'" "y \<in> FVarsB b'" using b' yy unfolding 0 
+    have y: "y \<noteq> x'" "y \<in> FVarsB b'" using b' yy unfolding 0
     using FVarsB_LamB[OF b'] by auto
 
     have "|{x,x'} \<union> FFVars t \<union> FFVars t'| <o |UNIV::var set|"
     by (metis Un_insert_right singl_bound sup_bot_right term.set_bd_UNIV var_term_pre_class.Un_bound)
-    then obtain z where z: 
-    "z \<notin> {x,x'} \<union> FFVars t \<union> FFVars t'" 
+    then obtain z where z:
+    "z \<notin> {x,x'} \<union> FFVars t \<union> FFVars t'"
     by (meson exists_fresh)
 
-    obtain f where 
+    obtain f where
     f: "bij f" "|supp f| <o |UNIV::var set|"
-       "id_on (- {x, x'}) f \<and> id_on (FFVars (Lam x t)) f" 
-    and z: "f x = x'"   
-    and t': "t' = rrename f t" 
+       "id_on (- {x, x'}) f \<and> id_on (FFVars (Lam x t)) f"
+    and z: "f x = x'"
+    and t': "t' = rrename f t"
     using  Lam_inject_strong[OF 0(2)] by auto
-    
+
     have fvb't': "FVarsB b' \<subseteq> FFVars t'"
     using Lam2[OF f(1,2), unfolded t'[symmetric], OF 0(1)] .
     have yt': "y \<in> FFVars t'" using fvb't' y(2) by auto
@@ -1123,9 +1184,9 @@ next
 
     assume "R (Lam x t) b" and f: "bij f" "|supp f| <o |UNIV::var set|"
 
-   
+
     then obtain x' t' b'
-    where 0: "R t' b'" "Lam x t = Lam x' t'" "b = LamB x' b'" 
+    where 0: "R t' b'" "Lam x t = Lam x' t'" "b = LamB x' b'"
     using R_Lam_elim by metis
 
 
@@ -1134,15 +1195,15 @@ next
 
     have "|{x,x'} \<union> FFVars t \<union> FFVars t'| <o |UNIV::var set|"
     by (metis Un_insert_right singl_bound sup_bot_right term.set_bd_UNIV var_term_pre_class.Un_bound)
-    then obtain z where z: 
-    "z \<notin> {x,x'} \<union> FFVars t \<union> FFVars t'" 
+    then obtain z where z:
+    "z \<notin> {x,x'} \<union> FFVars t \<union> FFVars t'"
     by (meson exists_fresh)
 
-    obtain g where 
+    obtain g where
     g: "bij g" "|supp g| <o |UNIV::var set|"
-       "id_on (- {x, x'}) g \<and> id_on (FFVars (Lam x t)) g" 
-    and z: "g x = x'"   
-    and t': "t' = rrename g t" 
+       "id_on (- {x, x'}) g \<and> id_on (FFVars (Lam x t)) g"
+    and z: "g x = x'"
+    and t': "t' = rrename g t"
     using Lam_inject_strong[OF 0(2)] by auto
 
     have RR: "R (Lam (f x') (rrename f t')) (LamB (f x') (renB f b'))"
@@ -1151,11 +1212,11 @@ next
       subgoal using 0(1) unfolding t' .
       subgoal by fact subgoal by fact .
 
-    show "R (rrename f (Lam x t)) (renB f b)" 
-    unfolding 0 using RR apply(subst term.permute) 
+    show "R (rrename f (Lam x t)) (renB f b)"
+    unfolding 0 using RR apply(subst term.permute)
       subgoal using f by auto subgoal using f by auto
       subgoal apply(subst renB_LamB)
-       using f b' by auto .  
+       using f b' by auto .
   qed
 qed
 
@@ -1194,16 +1255,16 @@ using morFromTrm_rec unfolding morFromTrm_def by auto
 lemma rec_Lam[simp]: "rec (Lam x e) = LamB x (rec e)"
 using morFromTrm_rec unfolding morFromTrm_def by auto
 
-lemma rec_rrename: "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow> 
+lemma rec_rrename: "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::var set| \<Longrightarrow>
  rec (rrename \<sigma> e) = renB \<sigma> (rec e)"
 using morFromTrm_rec unfolding morFromTrm_def by auto
 
 lemma FVarsB_rec: "FVarsB (rec e) \<subseteq> FFVars e"
 using morFromTrm_rec unfolding morFromTrm_def by auto
 
-lemma rec_unique: 
-assumes "\<And>e. H e \<in> B" 
-"\<And>x. H (Var x) = VarB x" 
+lemma rec_unique:
+assumes "\<And>e. H e \<in> B"
+"\<And>x. H (Var x) = VarB x"
 "\<And>e1 e2. H (App e1 e2) = AppB (H e1) (H e2)"
 "\<And>x e. H (Lam x e) = LamB x (H e)"
 shows "H = rec"
@@ -1213,8 +1274,10 @@ using assms by auto .
 
 end (* context LC_Rec *)
 
-
-
-
+lemmas smalls = emp_bound singl_bound term.Un_bound infinite term.card_of_FFVars_bounds
+declare smalls[refresh_smalls]
+declare Lam_inject[refresh_simps]
+declare Lam_eq_tvsubst[refresh_intros] term.rrename_cong_ids[symmetric, refresh_intros]
+declare id_on_antimono[refresh_elims]
 
 end
diff --git a/thys/Untyped_Lambda_Calculus/LC_Beta.thy b/thys/Untyped_Lambda_Calculus/LC_Beta.thy
index 5e2ce323..8b736b4d 100644
--- a/thys/Untyped_Lambda_Calculus/LC_Beta.thy
+++ b/thys/Untyped_Lambda_Calculus/LC_Beta.thy
@@ -1,7 +1,7 @@
 (* Here we instantiate the general enhanced rule induction to beta reduction
 for the (untyped) lambda-calculus *)
 theory LC_Beta
-imports LC "Binders.Generic_Barendregt_Enhanced_Rule_Induction" "Prelim.Curry_LFP" "Prelim.More_Stream" LC_Head_Reduction
+  imports LC "Binders.Generic_Barendregt_Enhanced_Rule_Induction" "Prelim.Curry_LFP" "Prelim.More_Stream" LC_Head_Reduction
 begin
 
 (* INSTANTIATING THE ABSTRACT SETTING: *)
@@ -19,22 +19,7 @@ inductive step :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
 | AppR: "step e2 e2' \<Longrightarrow> step (App e1 e2) (App e1 e2')"
 | Xi: "step e e' \<Longrightarrow> step (Lam x e) (Lam x e')"
 
-binder_inductive step
-  subgoal for \<sigma> R B t  \<comment> \<open>equivariance\<close>
-    by (elim disj_forward case_prodE)
-      (auto simp: isPerm_def term.rrename_comps rrename_tvsubst_comp
-         | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-         | ((rule exI[of _ "\<sigma> _"])+; auto))+
-  subgoal premises prems for R B t1 t2  \<comment> \<open>refreshability\<close>
-    by (tactic \<open>refreshability_tac false
-      [@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
-      [@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
-      [SOME [SOME 1, SOME 0, NONE], NONE, NONE, SOME [SOME 0, SOME 0, SOME 1]]
-      @{thm prems(3)} @{thm prems(2)} @{thms }
-      @{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite}
-      @{thms Lam_inject} @{thms Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
-      @{thms } @{context}\<close>)
-  done
+binder_inductive step .
 
 thm step.strong_induct step.equiv
 
diff --git a/thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy b/thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy
index 6d6bf1c6..0cb8871a 100644
--- a/thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy
+++ b/thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy
@@ -7,7 +7,7 @@ begin
 
 (* *)
 
-abbreviation Tsupp :: "nat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> var set" where 
+abbreviation Tsupp :: "nat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> var set" where
 "Tsupp d e1 e2 \<equiv> {} \<union> FFVars_term e1 \<union> FFVars_term e2"
 
 lemma fresh: "\<exists>xx. xx \<notin> Tsupp d e1 e2"
@@ -19,22 +19,7 @@ inductive stepD :: "nat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> bool"
 | AppR: "stepD d e2 e2' \<Longrightarrow> stepD (Suc d) (App e1 e2) (App e1 e2')"
 | Xi: "stepD d e e' \<Longrightarrow> stepD d (Lam x e) (Lam x e')"
 
-binder_inductive stepD
-  subgoal for R B \<sigma> x1 x2 x3
-    by (elim disj_forward exE case_prodE)
-      (auto simp: isPerm_def term.rrename_comps rrename_tvsubst_comp
-        | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-        | ((rule exI[of _ "\<sigma> _"])+; auto))+
-  subgoal premises prems for R B d t1 t2
-    by (tactic \<open>refreshability_tac false
-      [@{term "(\<lambda>_. {}) :: nat \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
-      [@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
-      [SOME [SOME 1, SOME 0, NONE], NONE, NONE, SOME [NONE, SOME 0, SOME 0, SOME 1]]
-      @{thm prems(3)} @{thm prems(2)} @{thms }
-      @{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite}
-      @{thms Lam_inject} @{thms Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
-      @{thms } @{context}\<close>)
-  done
+binder_inductive stepD .
 
 thm stepD.strong_induct
 thm stepD.equiv
diff --git a/thys/Untyped_Lambda_Calculus/LC_Parallel_Beta.thy b/thys/Untyped_Lambda_Calculus/LC_Parallel_Beta.thy
index 43564347..e43ffcc5 100644
--- a/thys/Untyped_Lambda_Calculus/LC_Parallel_Beta.thy
+++ b/thys/Untyped_Lambda_Calculus/LC_Parallel_Beta.thy
@@ -15,25 +15,19 @@ inductive pstep :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
 | Xi: "pstep e e' \<Longrightarrow> pstep (Lam x e) (Lam x e')"
 | PBeta: "pstep e1 e1' \<Longrightarrow> pstep e2 e2' \<Longrightarrow> pstep (App (Lam x e1) e2) (tvsubst (Var(x:=e2')) e1')"
 
-binder_inductive pstep
-  subgoal for \<sigma> R B x1 x2
-    by (elim disj_forward exE)
-      (auto simp: isPerm_def
-         term.rrename_comps rrename_tvsubst_comp
-         | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-         | ((rule exI[of _ "\<sigma> _"])+; auto))+
-  subgoal premises prems for R B t1 t2
-    by (tactic \<open>refreshability_tac false
-      [@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
+binder_inductive (no_auto_refresh) pstep
+ subgoal premises prems for R B t1 t2
+     by (tactic \<open>refreshability_tac false
+       [@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
       [@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
       [NONE, NONE, SOME [SOME 0, SOME 0, SOME 1], SOME [SOME 0, SOME 0, NONE, NONE, SOME 1]]
       @{thm prems(3)} @{thm prems(2)} @{thms }
       @{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite}
       @{thms Lam_inject} @{thms Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
       @{thms id_on_antimono} @{context}\<close>)
-  done
+ done
 
 thm pstep.strong_induct
 thm pstep.equiv
 
-end
\ No newline at end of file
+end