more

jvanbruegge · Sep 17, 2024 · ff7f16b · ff7f16b
1 parent 8b95f55
commit ff7f16b
Show file tree

Hide file tree

Showing 6 changed files with 14 additions and 9 deletions.
diff --git a/thys/MRBNF_FP.thy b/thys/MRBNF_FP.thy
@@ -338,7 +338,7 @@ local
   open BNF_Util
 in
 
-fun refreshability_tac B Tsupp G_thm small_thms instss simp_thms intro_thms ctxt =
+fun refreshability_tac B Tsupp G_thm small_thms instss simp_thms intro_thms elim_thms ctxt =
   let
     val fresh = infer_instantiate' ctxt
       [SOME (Thm.cterm_of ctxt B), SOME (Thm.cterm_of ctxt Tsupp),
@@ -357,7 +357,8 @@ fun refreshability_tac B Tsupp G_thm small_thms instss simp_thms intro_thms ctxt
           HEADGOAL (EVERY' (map (fn x => rtac ctxt (infer_instantiate' ctxt [NONE, SOME x] exI)) xs)) THEN
           SOLVE (HEADGOAL (SELECT_GOAL (mk_auto_tac (ctxt
             addsimps (simp_thms @ prems)
-            addSIs (ex_f :: id_onI :: intro_thms)) 0 4) THEN_ALL_NEW
+            addSIs (ex_f :: id_onI :: intro_thms)
+            addSEs elim_thms) 0 4) THEN_ALL_NEW
             SELECT_GOAL (print_tac ctxt "auto failed")))
         end;
   in

diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy
@@ -277,8 +277,8 @@ lemma ty_fresh_extend: "\<Gamma>, x <: U \<turnstile> S <: T \<Longrightarrow> x
   by (metis (no_types, lifting) UnE fst_conv snd_conv subsetD wf_ConsE wf_FFVars wf_context)
 
 binder_inductive ty
-for perms: map_context rrename_typ rrename_typ and supps: "\<lambda>\<Gamma>. dom \<Gamma> \<union> FFVars_ctxt \<Gamma>" FFVars_typ FFVars_typ
-         apply (auto simp: o_def split_beta typ.rrename_comps fun_eq_iff isPerm_def image_Un
+  for perms: map_context rrename_typ rrename_typ and supps: "\<lambda>\<Gamma>. dom \<Gamma> \<union> FFVars_ctxt \<Gamma>" FFVars_typ FFVars_typ
+                    apply (auto simp: o_def split_beta typ.rrename_comps fun_eq_iff isPerm_def image_Un
       small_def typ.FFVars_rrenames typ.rrename_cong_ids
       typ.card_of_FFVars_bounds typ.Un_bound var_typ_pre_class.UN_bound set_bd_UNIV typ.set_bd
       intro!: context_map_cong_id infinite_UNIV) [16]
@@ -304,19 +304,20 @@ for perms: map_context rrename_typ rrename_typ and supps: "\<lambda>\<Gamma>. do
         apply (rule exI)
         apply (rule exI[of _ "{z}"])
         apply (intro exI conjI)
-               apply (rule refl)+
-             apply (rule Forall_swap)
-            apply simp
+              apply (rule refl)+
             apply (rule Forall_swap)
+            apply simp
+           apply (rule Forall_swap)
            apply simp
           apply assumption+
          apply (frule prems(1)[rule_format, of "(\<Gamma>, x <: T\<^sub>1)" "S\<^sub>2" "T\<^sub>2"])
-          apply (drule prems(2)[rule_format, of "id(x := z, z := x)" "\<Gamma>, x <: T\<^sub>1" "S\<^sub>2" "T\<^sub>2", rotated 2])
+         apply (drule prems(2)[rule_format, of "id(x := z, z := x)" "\<Gamma>, x <: T\<^sub>1" "S\<^sub>2" "T\<^sub>2", rotated 2])
            apply (auto simp: extend_eqvt)
         apply (erule cong[OF cong[OF cong], THEN iffD1, of R, OF refl, rotated -1]) back
           apply (drule ty_fresh_extend)
           apply (simp_all add: supp_swap_bound)
         apply (rule context_map_cong_id; auto)
+        done
       done
     done
   done

diff --git a/thys/Prelim/Prelim.thy b/thys/Prelim/Prelim.thy
@@ -63,7 +63,7 @@ lemma bij_iff1:
 definition id_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
   "id_on A f \<equiv> \<forall> a. a \<in> A \<longrightarrow> f a = a"
 
-lemma id_on_id[simp]: "id_on A id"
+lemma id_on_id[simp,intro!]: "id_on A id"
   unfolding id_on_def by auto
 
 lemma id_on_insert[simp]: "id_on (insert x A) f \<longleftrightarrow> f x = x \<and> id_on A f"

diff --git a/thys/Untyped_Lambda_Calculus/LC_Beta.thy b/thys/Untyped_Lambda_Calculus/LC_Beta.thy
@@ -42,6 +42,7 @@ for perms: rrename rrename and supps: FFVars FFVars
              @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]]
       @{thms Lam_inject}
       @{thms prems(2) Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
+      @{thms }
       @{context}\<close>)
     done
 (*

diff --git a/thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy b/thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy
@@ -42,6 +42,7 @@ for perms: "\<lambda>_. id" rrename rrename and supps: "\<lambda>_. {}" FFVars_t
              @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]]
       @{thms Lam_inject}
       @{thms prems(2)[simplified] Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
+      @{thms }
       @{context}\<close>)
     done
   done

diff --git a/thys/Untyped_Lambda_Calculus/LC_Parallel_Beta.thy b/thys/Untyped_Lambda_Calculus/LC_Parallel_Beta.thy
@@ -41,6 +41,7 @@ for perms: rrename rrename and supps: FFVars FFVars
              @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]]
       @{thms Lam_inject}
       @{thms prems(2) Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
+      @{thms }
       @{context}\<close>)
     done
   done