Make build work again

.gitignore

@@ -1 +1,2 @@
 *~
+Scratch.thy

Tools/binder_inductive.ML

@@ -21,7 +21,7 @@ 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;
 
-datatype options = No_Equiv | No_Refresh
+datatype options = No_Equiv | No_Refresh | Verbose
 
 fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_defs_lthy =
   let
@@ -375,6 +375,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_def
     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
@@ -655,7 +656,7 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_def
               ) ctxt
             ]
           ]);
-        val _ = @{print} G_equiv
+        val _ = (verbose ? @{print}) G_equiv
 
         val G_refresh = if member (op=) options No_Refresh then hd (G_refreshs) else
           let
@@ -708,14 +709,14 @@ fun binder_inductive_cmd (((options, pred_name), binds_opt), perms_supps) no_def
                 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 _ = @{print} (map (Option.map (map (Option.map (Thm.cterm_of lthy)))) matrix)
+              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 false (map fst supps) matrix (nth prems 2) (nth prems 1) supp_smalls (map snd supps) ctxt
+              refreshability_tac_internal verbose (map fst supps) matrix (nth prems 2) (nth prems 1) supp_smalls (map snd supps) ctxt
             ) ctxt
           ]) end;
-        val _ = @{print} G_refresh
+        val _ = (verbose ? @{print}) G_refresh
 
         fun mk_induct mono = Drule.rotate_prems ~1 (
           apply_n @{thm le_funD} n (@{thm lfp_induct} OF [mono])
@@ -1127,7 +1128,8 @@ val parse_perm_supps =
 
 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 "no_auto_refresh" >> K No_Refresh)
+    || (Parse.reserved "verbose" >> K Verbose))
 
 val config_parser = Scan.optional (@{keyword "("} |--
   Parse.!!! (Parse.list1 options_parser) --| @{keyword ")"}) []

thys/Infinitary_FOL/InfFOL.thy

@@ -231,7 +231,9 @@ unfolding kmember_def map_fun_def id_o o_id map_set\<^sub>k_def
 unfolding comp_def Abs_set\<^sub>k_inverse[OF UNIV_I]
 apply transfer apply transfer by blast
 
-lemma in_k_equiv[equiv]: "bij (\<sigma>::'a::var_ifol'_pre \<Rightarrow> 'a) \<Longrightarrow> |supp \<sigma>| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k map_set\<^sub>k (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k \<Delta>"
+lemma in_k_equiv: "isPerm \<sigma> \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k map_set\<^sub>k (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k \<Delta>"
+  unfolding isPerm_def
+  apply (erule conjE)
   apply (rule iffI)
   apply (drule in_k_equiv'[rotated])
   apply (rule bij_imp_bij_inv)
@@ -249,11 +251,13 @@ lemma in_k_equiv[equiv]: "bij (\<sigma>::'a::var_ifol'_pre \<Rightarrow> 'a) \<L
   apply assumption
   done
 
-lemma in_k1_equiv'[equiv]: "bij \<sigma> \<Longrightarrow> f \<in>\<^sub>k\<^sub>1 F \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) F"
+lemma in_k1_equiv': "bij \<sigma> \<Longrightarrow> f \<in>\<^sub>k\<^sub>1 F \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) F"
 apply (unfold k1member_def map_fun_def comp_def id_def map_set\<^sub>k\<^sub>1_def Abs_set\<^sub>k\<^sub>1_inverse[OF UNIV_I])
 apply transfer apply transfer by blast
 
-lemma in_k1_equiv[equiv]: "bij (\<sigma>::'a::var_ifol'_pre \<Rightarrow> 'a) \<Longrightarrow> |supp \<sigma>| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k\<^sub>1 \<Delta>"
+lemma in_k1_equiv: "isPerm \<sigma> \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k\<^sub>1 \<Delta>"
+  unfolding isPerm_def
+  apply (erule conjE)
   apply (rule iffI)
   apply (drule in_k1_equiv'[rotated])
   apply (rule bij_imp_bij_inv)
@@ -335,8 +339,8 @@ 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
-(*  subgoal for R B \<sigma> x1 x2
+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)
           apply (auto simp: ifol'.rrename_comps in_k_equiv in_k_equiv' isPerm_def ifol'.rrename_ids supp_inv_bound)
@@ -408,8 +412,8 @@ binder_inductive deduct
       apply (metis ifol'.rrename_bijs ifol'.rrename_inv_simps inv_simp1 set\<^sub>k.map_ident_strong)
       apply (erule image_mono)
       done
-    done*)
-(*  subgoal premises prems for R B \<Delta> x2
+    done
+  subgoal premises prems for R B \<Delta> x2
     using prems(2-) unfolding induct_rulify_fallback split_beta
     unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
     apply (elim disj_forward)
@@ -598,12 +602,7 @@ binder_inductive deduct
         by (smt (verit) Int_iff Un_Int_eq(1) X_def \<sigma>_def bij_betw_apply disjoint_iff image_iff)
     qed
     done
-  done*)
-  sorry
-
-lemma all_mono_bij:
-  "bij f \<Longrightarrow> (\<And>x. P x \<longrightarrow> Q (f x)) \<Longrightarrow> (\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
-  by (metis bij_pointE)
+  done
 
 thm deduct.strong_induct
 thm deduct.equiv

thys/Infinitary_Lambda_Calculus/ILC_Beta.thy

@@ -24,7 +24,42 @@ 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
+        apply(rule exI[of _ "dsmap \<sigma> xs"])
+        apply(rule exI[of _ "irrename \<sigma> e1"])
+        apply(rule exI[of _ "smap (irrename \<sigma>) es2"])
+        apply (simp add: iterm.rrename_comps) apply(subst irrename_itvsubst_comp) apply auto
+        apply(subst imkSubst_smap_irrename_inv) unfolding isPerm_def apply auto
+        apply(subst irrename_eq_itvsubst_iVar'[of _ e1]) unfolding isPerm_def apply auto
+        apply(subst itvsubst_comp)
+        subgoal by (metis SSupp_imkSubst imkSubst_smap_irrename_inv)
+        subgoal by (smt (verit, best) SSupp_def VVr_eq_Var card_of_subset_bound mem_Collect_eq not_in_supp_alt o_apply subsetI)
+        subgoal apply(rule itvsubst_cong)
+          subgoal using SSupp_irrename_bound by blast
+          subgoal using card_SSupp_itvsubst_imkSubst_irrename_inv isPerm_def by auto
+          subgoal for x apply simp apply(subst iterm.subst(1))
+            subgoal using card_SSupp_imkSubst_irrename_inv[unfolded isPerm_def] by auto
+            subgoal by simp . . .
+      (* *)
+  subgoal for e1 e1' es2
+      apply(rule exI[of _ "irrename \<sigma> e1"]) apply(rule exI[of _ "irrename \<sigma> e1'"])
+      apply(rule exI[of _ "smap (irrename \<sigma>) es2"])
+      by (simp add: iterm.rrename_comps)
+    (* *)
+  subgoal for es2 i e2' e1
+      apply(rule exI[of _ "smap (irrename \<sigma>) es2"])
+      apply(rule exI[of _ i])
+      apply(rule exI[of _ "irrename \<sigma> e2'"])
+      apply(rule exI[of _ "irrename \<sigma> e1"])
+      apply (simp add: iterm.rrename_comps) .
+    (* *)
+  subgoal for e e' xs
+      apply(rule exI[of _ "irrename \<sigma> e"]) apply(rule exI[of _ "irrename \<sigma> e'"])
+      apply(rule exI[of _ "dsmap \<sigma> xs"])
+      by (simp add: iterm.rrename_comps) .
   subgoal premises prems for R B x1 x2
     using prems(2-) apply safe
     subgoal for xs e1 es2

thys/Infinitary_Lambda_Calculus/ILC_affine.thy

@@ -21,9 +21,8 @@ inductive affine  :: "itrm \<Rightarrow> bool" where
  \<Longrightarrow>
  affine (iApp e1 es2)"
 
-binder_inductive affine
-
-  (*unfolding isPerm_def induct_rulify_fallback
+binder_inductive (no_auto_equiv, no_auto_refresh) affine
+  unfolding isPerm_def induct_rulify_fallback
   subgoal for R B \<sigma> t
     apply(elim disjE)
     subgoal apply(rule disjI3_1)
@@ -51,7 +50,7 @@ binder_inductive affine
         done
       done
     done
-  done*)
+  done
   subgoal premises prems for R B t
     using prems(2-)
      apply safe

thys/MRBNF_FP.thy

@@ -359,13 +359,8 @@ local
   open BNF_FP_Util
 in
 
-fun refreshability_tac verbose supps instss G_thm eqvt_thm smalls simps 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 extend_thms = Named_Theorems.get ctxt "MRBNF_FP.refresh_extends";
-    val small_thms = smalls @ Named_Theorems.get ctxt "MRBNF_FP.refresh_smalls";
-    val simp_thms = simps @ Named_Theorems.get ctxt "MRBNF_FP.refresh_simps";
-    val intro_thms = Named_Theorems.get ctxt "MRBNF_FP.refresh_intros";
-    val elim_thms = Named_Theorems.get ctxt "MRBNF_FP.refresh_elims";
     val n = length supps;
     fun case_tac NONE _ prems ctxt = HEADGOAL (Method.insert_tac ctxt prems THEN' 
         K (if verbose then print_tac ctxt "pre_simple_auto" else all_tac)) THEN SOLVE (auto_tac ctxt)
@@ -418,22 +413,38 @@ val _ = extra_assms |> map (Thm.pretty_thm ctxt #> verbose ? @{print tracing});
           val small_ctxt = ctxt addsimps small_thms;
         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;
   in
     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)
     ]
   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>
 

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])

thys/POPLmark/SystemFSub.thy

@@ -274,7 +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
+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"}]

thys/Pi_Calculus/Commitment.thy

@@ -375,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"),

thys/Pi_Calculus/Pi_Transition_Early.thy

@@ -11,18 +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
+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"}]

thys/Pi_Calculus/Pi_Transition_Late.thy

@@ -10,9 +10,8 @@ inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
 | ScopeFree: "\<lbrakk> trans P (Cmt \<alpha> P') ; fra \<alpha> ; x \<notin> ns \<alpha> \<rbrakk> \<Longrightarrow> trans (Res x P) (Cmt \<alpha> (Res x P'))"
 | 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))"
-thm equiv
-declare [[ML_print_depth=10000]]
-binder_inductive trans
+
+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"}]

thys/Pi_Calculus/Pi_cong.thy

@@ -19,7 +19,7 @@ inductive cong :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<equiv>\<
 | "Bang P \<equiv>\<^sub>\<pi> Par P (Bang P)"
 | "x \<notin> FFVars Q \<Longrightarrow> Res x (Par P Q) \<equiv>\<^sub>\<pi> Par (Res x P) Q"
 
-binder_inductive cong
+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"}]
@@ -56,7 +56,14 @@ inductive trans :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<rightar
 | "P \<equiv>\<^sub>\<pi> P' \<Longrightarrow> P' \<rightarrow> Q' \<Longrightarrow> Q' \<equiv>\<^sub>\<pi> Q \<Longrightarrow> P \<rightarrow> Q"
 
 (* needs equiv_commute of vvsubst *)
-binder_inductive trans
+binder_inductive (no_auto_equiv, no_auto_refresh) trans
+  subgoal for R B \<sigma> x1 x2
+    apply simp
+    apply (elim disj_forward exE)
+       apply  (auto simp: isPerm_def term.rrename_comps
+        | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
+        | ((rule exI[of _ "\<sigma> _"])+; auto))+
+    by (metis cong.equiv bij_imp_inv' term.rrename_bijs term.rrename_inv_simps)
   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"}]

thys/STLC/STLC.thy

@@ -228,7 +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
+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

thys/Untyped_Lambda_Calculus/LC.thy

@@ -1274,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

thys/Untyped_Lambda_Calculus/LC_Beta.thy

@@ -19,11 +19,6 @@ 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')"
 
-lemmas smalls = emp_bound singl_bound term.Un_bound infinite
-declare smalls[refresh_smalls]
-declare Lam_inject[refresh_simps]
-declare Lam_eq_tvsubst[refresh_intros] term.rrename_cong_ids[symmetric, refresh_intros]
-
 binder_inductive step .
 
 thm step.strong_induct step.equiv

thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy

@@ -19,17 +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 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