--- a/NEWS Fri May 16 20:44:51 2025 +0200
+++ b/NEWS Sun May 18 14:33:01 2025 +0000
@@ -75,6 +75,15 @@
*** HOL ***
+* ML bindings for theorms Ball_def, Bex_def, CollectD, CollectE, CollectI,
+Collect_conj_eq, Collect_mem_eq, IntD1, IntD2, IntE, IntI, Int_Collect, UNIV_I,
+UNIV_witness, UnE, UnI1, UnI2, ballE, ballI, bexCI, bexE, bexI, bex_triv, bspec,
+contra_subsetD, equalityCE, equalityD1, equalityD2, equalityE, equalityI,
+imageE, imageI, image_Un, image_insert, insert_commute, insert_iff,
+mem_Collect_eq, rangeE, rangeI, range_eqI, subsetCE, subsetD, subsetI,
+subset_refl, subset_trans, vimageD, vimageE, vimageI, vimageI2, vimage_Collect,
+vimage_Int, vimage_Un. INCOMPATIBILITY, use thm(s) antiquotation instead.
+
* Normalization by evaluation (method "normalization", command value) could
yield false positives due to incomplete handling of polymorphism in certain
situations; this is now corrected.
--- a/src/Doc/Tutorial/Protocol/Message.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Sun May 18 14:33:01 2025 +0000
@@ -850,7 +850,7 @@
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
(Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
- (insert_commute RS ssubst) 1),
+ (@{thm insert_commute} RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ctxt 1,
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/Auth/Message.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Message.thy Sun May 18 14:33:01 2025 +0000
@@ -830,7 +830,7 @@
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
(Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
- (insert_commute RS ssubst) 1),
+ (@{thm insert_commute} RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ctxt 1,
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/Auth/OtwayReesBella.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy Sun May 18 14:33:01 2025 +0000
@@ -239,8 +239,8 @@
val analz_image_freshK_ss =
simpset_of
- (\<^context> delsimps [image_insert, image_Un]
- delsimps [@{thm imp_disjL}] (*reduces blow-up*)
+ (\<^context> delsimps @{thms image_insert image_Un}
+ delsimps @{thms imp_disjL} (*reduces blow-up*)
addsimps @{thms analz_image_freshK_simps})
end
@@ -249,7 +249,7 @@
method_setup analz_freshCryptK = \<open>
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
- (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+ (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshCryptK_lemma}),
ALLGOALS (asm_simp_tac
(put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))])))\<close>
--- a/src/HOL/Auth/Public.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Public.thy Sun May 18 14:33:01 2025 +0000
@@ -407,8 +407,8 @@
val analz_image_freshK_ss =
simpset_of
- (\<^context> delsimps [image_insert, image_Un]
- delsimps [@{thm imp_disjL}] (*reduces blow-up*)
+ (\<^context> delsimps @{thms image_insert image_Un}
+ delsimps @{thms imp_disjL} (*reduces blow-up*)
addsimps @{thms analz_image_freshK_simps})
(*Tactic for possibility theorems*)
@@ -433,7 +433,7 @@
method_setup analz_freshK = \<open>
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
- (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+ (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))])))\<close>
"for proving the Session Key Compromise theorem"
--- a/src/HOL/Auth/Shared.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Shared.thy Sun May 18 14:33:01 2025 +0000
@@ -218,8 +218,8 @@
val analz_image_freshK_ss =
simpset_of
- (\<^context> delsimps [image_insert, image_Un]
- delsimps [@{thm imp_disjL}] (*reduces blow-up*)
+ (\<^context> delsimps @{thms image_insert image_Un}
+ delsimps @{thms imp_disjL} (*reduces blow-up*)
addsimps @{thms analz_image_freshK_simps})
end
@@ -237,7 +237,7 @@
method_setup analz_freshK = \<open>
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
- (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+ (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))])))\<close>
"for proving the Session Key Compromise theorem"
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Sun May 18 14:33:01 2025 +0000
@@ -817,7 +817,7 @@
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST
- (resolve_tac ctxt [allI, ballI, impI]),
+ (resolve_tac ctxt @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy},
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sun May 18 14:33:01 2025 +0000
@@ -826,7 +826,7 @@
method_setup sc_analz_freshK = \<open>
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
- (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+ (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Sun May 18 14:33:01 2025 +0000
@@ -383,8 +383,8 @@
val analz_image_freshK_ss =
simpset_of
- (\<^context> delsimps [image_insert, image_Un]
- delsimps [@{thm imp_disjL}] (*reduces blow-up*)
+ (\<^context> delsimps @{thms image_insert image_Un}
+ delsimps @{thms imp_disjL} (*reduces blow-up*)
addsimps @{thms analz_image_freshK_simps})
end
\<close>
@@ -400,7 +400,7 @@
method_setup analz_freshK = \<open>
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
- (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+ (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))])))\<close>
"for proving the Session Key Compromise theorem"
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Sun May 18 14:33:01 2025 +0000
@@ -150,13 +150,13 @@
resolve_tac ctxt @{thms relcomppI},
resolve_tac ctxt @{thms GrpI},
resolve_tac ctxt [refl],
- resolve_tac ctxt [CollectI],
+ resolve_tac ctxt @{thms CollectI},
BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
resolve_tac ctxt @{thms relcomppI}, assume_tac ctxt,
resolve_tac ctxt @{thms conversepI},
resolve_tac ctxt @{thms GrpI},
resolve_tac ctxt [refl],
- resolve_tac ctxt [CollectI],
+ resolve_tac ctxt @{thms CollectI},
BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
hyp_subst_tac ctxt,
--- a/src/HOL/Hoare/hoare_tac.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Sun May 18 14:33:01 2025 +0000
@@ -115,7 +115,7 @@
(**Simp_tacs**)
fun before_set2pred_simp_tac ctxt =
- simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]);
+ simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm Collect_conj_eq} RS sym, @{thm Compl_Collect}]);
fun split_simp_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
@@ -135,9 +135,9 @@
fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
before_set2pred_simp_tac ctxt i THEN_MAYBE
EVERY [
- resolve_tac ctxt [subsetI] i,
- resolve_tac ctxt [CollectI] i,
- dresolve_tac ctxt [CollectD] i,
+ resolve_tac ctxt @{thms subsetI} i,
+ resolve_tac ctxt @{thms CollectI} i,
+ dresolve_tac ctxt @{thms CollectD} i,
TRY (split_all_tac ctxt i) THEN_MAYBE
(rename_tac var_names i THEN
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
@@ -151,13 +151,13 @@
(*******************************************************************************)
fun max_simp_tac ctxt var_names tac =
- FIRST' [resolve_tac ctxt [subset_refl],
+ FIRST' [resolve_tac ctxt @{thms subset_refl},
set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
fun basic_simp_tac ctxt var_names tac =
simp_tac
(put_simpset HOL_basic_ss ctxt
- addsimps [mem_Collect_eq, @{thm split_conv}] |> Simplifier.add_proc Record.simproc)
+ addsimps @{thms mem_Collect_eq split_conv} |> Simplifier.add_proc Record.simproc)
THEN_MAYBE' max_simp_tac ctxt var_names tac;
@@ -189,7 +189,7 @@
rule_tac true (i + 1)]]
THEN (
if pre_cond then basic_simp_tac ctxt var_names tac i
- else resolve_tac ctxt [subset_refl] i)));
+ else resolve_tac ctxt @{thms subset_refl} i)));
in rule_tac end;
@@ -227,7 +227,7 @@
rule_tac true (i + 1)]]
THEN (
if pre_cond then basic_simp_tac ctxt var_names tac i
- else resolve_tac ctxt [subset_refl] i)));
+ else resolve_tac ctxt @{thms subset_refl} i)));
in rule_tac end;
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Sun May 18 14:33:01 2025 +0000
@@ -777,12 +777,12 @@
apply(tactic \<open>TRYALL (eresolve_tac \<^context> [disjE])\<close>)
apply simp_all
apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
- resolve_tac \<^context> [subset_trans],
+ resolve_tac \<^context> @{thms subset_trans},
eresolve_tac \<^context> @{thms Graph3},
force_tac \<^context>,
assume_tac \<^context>])\<close>)
apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
- eresolve_tac \<^context> [subset_trans],
+ eresolve_tac \<^context> @{thms subset_trans},
resolve_tac \<^context> @{thms Graph9},
force_tac \<^context>])\<close>)
apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI1],
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Sun May 18 14:33:01 2025 +0000
@@ -1188,7 +1188,7 @@
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
\<comment> \<open>35 subgoals left\<close>
apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI1],
- resolve_tac \<^context> [subset_trans],
+ resolve_tac \<^context> @{thms subset_trans},
eresolve_tac \<^context> @{thms Graph3},
force_tac \<^context>,
assume_tac \<^context>])\<close>)
--- a/src/HOL/Nominal/nominal_datatype.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun May 18 14:33:01 2025 +0000
@@ -133,7 +133,7 @@
val at_fin_set_fresh = @{thm at_fin_set_fresh};
val abs_fun_eq1 = @{thm abs_fun_eq1};
-fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq mem_Collect_eq];
+fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq @{thm mem_Collect_eq}];
fun mk_perm Ts t u =
let
@@ -587,7 +587,7 @@
Const (cname, U --> HOLogic.boolT)) NONE
(fn ctxt =>
resolve_tac ctxt [exI] 1 THEN
- resolve_tac ctxt [CollectI] 1 THEN
+ resolve_tac ctxt @{thms CollectI} 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac ctxt rep_intrs 1))) thy |> (fn ((_, r), thy) =>
let
--- a/src/HOL/SET_Protocol/Message_SET.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Sun May 18 14:33:01 2025 +0000
@@ -848,7 +848,7 @@
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
(Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
- (insert_commute RS ssubst) 1),
+ (@{thm insert_commute} RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ctxt 1,
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/Set.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Set.thy Sun May 18 14:33:01 2025 +0000
@@ -2027,59 +2027,4 @@
lemmas set_mp = subsetD
lemmas set_rev_mp = rev_subsetD
-ML \<open>
-val Ball_def = @{thm Ball_def}
-val Bex_def = @{thm Bex_def}
-val CollectD = @{thm CollectD}
-val CollectE = @{thm CollectE}
-val CollectI = @{thm CollectI}
-val Collect_conj_eq = @{thm Collect_conj_eq}
-val Collect_mem_eq = @{thm Collect_mem_eq}
-val IntD1 = @{thm IntD1}
-val IntD2 = @{thm IntD2}
-val IntE = @{thm IntE}
-val IntI = @{thm IntI}
-val Int_Collect = @{thm Int_Collect}
-val UNIV_I = @{thm UNIV_I}
-val UNIV_witness = @{thm UNIV_witness}
-val UnE = @{thm UnE}
-val UnI1 = @{thm UnI1}
-val UnI2 = @{thm UnI2}
-val ballE = @{thm ballE}
-val ballI = @{thm ballI}
-val bexCI = @{thm bexCI}
-val bexE = @{thm bexE}
-val bexI = @{thm bexI}
-val bex_triv = @{thm bex_triv}
-val bspec = @{thm bspec}
-val contra_subsetD = @{thm contra_subsetD}
-val equalityCE = @{thm equalityCE}
-val equalityD1 = @{thm equalityD1}
-val equalityD2 = @{thm equalityD2}
-val equalityE = @{thm equalityE}
-val equalityI = @{thm equalityI}
-val imageE = @{thm imageE}
-val imageI = @{thm imageI}
-val image_Un = @{thm image_Un}
-val image_insert = @{thm image_insert}
-val insert_commute = @{thm insert_commute}
-val insert_iff = @{thm insert_iff}
-val mem_Collect_eq = @{thm mem_Collect_eq}
-val rangeE = @{thm rangeE}
-val rangeI = @{thm rangeI}
-val range_eqI = @{thm range_eqI}
-val subsetCE = @{thm subsetCE}
-val subsetD = @{thm subsetD}
-val subsetI = @{thm subsetI}
-val subset_refl = @{thm subset_refl}
-val subset_trans = @{thm subset_trans}
-val vimageD = @{thm vimageD}
-val vimageE = @{thm vimageE}
-val vimageI = @{thm vimageI}
-val vimageI2 = @{thm vimageI2}
-val vimage_Collect = @{thm vimage_Collect}
-val vimage_Int = @{thm vimage_Int}
-val vimage_Un = @{thm vimage_Un}
-\<close>
-
end
--- a/src/HOL/Tools/BNF/bnf_comp.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun May 18 14:33:01 2025 +0000
@@ -868,7 +868,7 @@
else inter (op =) repTA_tfrees all_TA_params_in_order);
val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
- (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+ (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
val repTB = mk_T_of_bnf Ds Bs bnf;
val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
@@ -900,7 +900,7 @@
val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE
- (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+ (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite, bd_regularCard) =
if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl},
@@ -930,7 +930,7 @@
fun map_cong0_tac ctxt =
EVERY' (rtac ctxt @{thm type_copy_map_cong0} :: rtac ctxt (map_cong0_of_bnf bnf) ::
map (fn i => EVERY' [select_prem_tac ctxt live (dtac ctxt meta_spec) i, etac ctxt meta_mp,
- etac ctxt (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
+ etac ctxt (o_apply RS @{thm equalityD2} RS set_mp)]) (1 upto live)) 1;
fun set_map0_tac thm ctxt =
rtac ctxt (@{thm type_copy_set_map0} OF [type_definition, thm]) 1;
val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt (@{thm ordLess_ordIso_trans} OF
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Sun May 18 14:33:01 2025 +0000
@@ -98,11 +98,11 @@
EVERY' (map_index (fn (i, map_cong0) =>
rtac ctxt map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
EVERY' [select_prem_tac ctxt n (dtac ctxt @{thm meta_spec}) (k + 1), etac ctxt meta_mp,
- rtac ctxt (equalityD2 RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans),
+ rtac ctxt (@{thm equalityD2} RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans),
rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union),
rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I},
REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1},
- rtac ctxt (o_apply RS equalityD2 RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt])
+ rtac ctxt (o_apply RS @{thm equalityD2} RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt])
comp_set_alts))
map_cong0s) 1)
end;
@@ -211,7 +211,7 @@
unfold_thms_tac ctxt comp_wit_thms THEN
REPEAT_DETERM ((assume_tac ctxt ORELSE'
REPEAT_DETERM o eresolve_tac ctxt @{thms UnionE UnE} THEN'
- etac ctxt imageE THEN' TRY o dresolve_tac ctxt Gwit_thms THEN'
+ etac ctxt @{thm imageE} THEN' TRY o dresolve_tac ctxt Gwit_thms THEN'
(etac ctxt FalseE ORELSE'
hyp_subst_tac ctxt THEN'
dresolve_tac ctxt Fwit_thms THEN'
@@ -232,7 +232,7 @@
(rtac ctxt subset_UNIV ORELSE' assume_tac ctxt) 1 THEN
REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1))) ORELSE
- ((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
+ ((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt @{thm CollectI}) 1 THEN
REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt subset_UNIV 1));
@@ -251,7 +251,7 @@
REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
rtac ctxt conjI THEN' rtac ctxt @{thm empty_subsetI}) 1)) THEN
(rtac ctxt @{thm empty_subsetI} ORELSE' assume_tac ctxt) 1) ORELSE
- ((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
+ ((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt @{thm CollectI}) 1 THEN
REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt @{thm empty_subsetI} 1));
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun May 18 14:33:01 2025 +0000
@@ -2038,7 +2038,7 @@
val consumes_attr = Attrib.consumes 1;
in
map (mk_thm ctxt fpTs ctrss
- #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr))
+ #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS @{thm bspec})) (cons consumes_attr))
(transpose setss)
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun May 18 14:33:01 2025 +0000
@@ -506,7 +506,7 @@
live_nesting_set_maps @ extra_unfolds @ basic_sumprod_thms_set @
@{thms UN_UN_flatten UN_Un_distrib UN_Un sup_assoc[THEN sym]}) THEN
ALLGOALS (rtac ctxt @{thm set_eqI[OF iffI]}) THEN
- ALLGOALS (REPEAT_DETERM o etac ctxt UnE) THEN
+ ALLGOALS (REPEAT_DETERM o etac ctxt @{thm UnE}) THEN
ALLGOALS (REPEAT o resolve_tac ctxt @{thms UnI1 UnI2} THEN' assume_tac ctxt);
fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Sun May 18 14:33:01 2025 +0000
@@ -238,7 +238,7 @@
val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
val in_mono'_thms = map (fn thm =>
- (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
+ (thm OF (replicate m @{thm subset_refl})) RS @{thm set_mp}) in_monos;
val map_arg_cong_thms =
let
@@ -306,7 +306,7 @@
val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
val coalg_in_thms = map (fn i =>
- coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
+ coalg_def RS iffD1 RS mk_conjunctN n i RS @{thm bspec}) ks
val coalg_set_thmss =
let
@@ -336,7 +336,7 @@
in
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} => (rtac ctxt (coalg_def RS iffD2) 1 THEN CONJ_WRAP
- (K (EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
+ (K (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm CollectI},
CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm subset_UNIV}])) allAs] 1)) ss))
|> Thm.close_derivation \<^here>
end;
@@ -423,7 +423,7 @@
(map prove image_goals, map prove elim_goals)
end;
- val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, imageI]) mor_image_thms;
+ val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, @{thm imageI}]) mor_image_thms;
val mor_incl_thm =
let
@@ -436,7 +436,7 @@
|> Thm.close_derivation \<^here>
end;
- val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
+ val mor_id_thm = mor_incl_thm OF (replicate n @{thm subset_refl});
val mor_comp_thm =
let
@@ -757,7 +757,7 @@
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
typedef (sbdT_bind, sum_bdT_params', NoSyn)
(HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt =>
- EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+ EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
val sbdT = Type (sbdT_name, sum_bdT_params);
val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
@@ -1341,7 +1341,7 @@
|> Thm.close_derivation \<^here>;
val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
- val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
+ val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, @{thm UNIV_I}]) mor_image'_thms;
val timer = time (timer "Final coalgebra");
@@ -1467,7 +1467,7 @@
val mor_unfold_thm =
let
val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
- val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
+ val morEs' = map (fn thm => (thm OF [mor_final_thm, @{thm UNIV_I}]) RS sym) morE_thms;
val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks));
val vars = Variable.add_free_names lthy goal [];
in
@@ -1476,7 +1476,7 @@
unfold_defs Abs_inverses' morEs' map_comp_id_thms map_cong0s)
|> Thm.close_derivation \<^here>
end;
- val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
+ val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, @{thm UNIV_I}]) RS sym) morE_thms;
val (raw_coind_thms, raw_coind_thm) =
let
@@ -2008,7 +2008,7 @@
((set_minimal
|> Thm.instantiate' cTs (mk_induct_tinst phis jsets y y')
|> unfold_thms lthy incls) OF
- (replicate n ballI @
+ (replicate n @{thm ballI} @
maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
|> singleton (Proof_Context.export names_lthy lthy)
|> rule_by_tactic lthy (ALLGOALS (TRY o etac lthy asm_rl)))
@@ -2049,7 +2049,7 @@
|> Thm.close_derivation \<^here>))
ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
in
- map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
+ map2 (map2 (fn le => fn ge => @{thm equalityI} OF [le, ge])) set_le_thmss set_ge_thmss
|> `transpose
end;
@@ -2451,7 +2451,7 @@
goals dtor_Jset_induct_thms
|> map split_conj_thm
|> transpose
- |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
+ |> map (map_filter (try (fn thm => thm RS @{thm bspec} RS mp)))
|> curry op ~~ (map_index Library.I (map (close_wit I) wits))
|> filter (fn (_, thms) => length thms = m)
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sun May 18 14:33:01 2025 +0000
@@ -108,7 +108,7 @@
val sum_case_cong_weak = @{thm sum.case_cong_weak};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
-val rev_bspec = Drule.rotate_prems 1 bspec;
+val rev_bspec = Drule.rotate_prems 1 @{thm bspec};
val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\<union>)"]};
val converse_shift = @{thm converse_subset_swap} RS iffD1;
@@ -116,29 +116,29 @@
dtac ctxt (coalg_def RS iffD1) 1 THEN
REPEAT_DETERM (etac ctxt conjE 1) THEN
EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
- REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN assume_tac ctxt 1;
+ REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) THEN assume_tac ctxt 1;
fun mk_mor_elim_tac ctxt mor_def =
(dtac ctxt (mor_def RS iffD1) THEN'
REPEAT o etac ctxt conjE THEN'
TRY o rtac ctxt @{thm image_subsetI} THEN'
- etac ctxt bspec THEN'
+ etac ctxt @{thm bspec} THEN'
assume_tac ctxt) 1;
fun mk_mor_incl_tac ctxt mor_def map_ids =
(rtac ctxt (mor_def RS iffD2) THEN'
rtac ctxt conjI THEN'
- CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
+ CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
map_ids THEN'
CONJ_WRAP' (fn thm =>
- (EVERY' [rtac ctxt ballI, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1;
+ (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1;
fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids =
let
- fun fbetw_tac image = EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
+ fun fbetw_tac image = EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
etac ctxt image, assume_tac ctxt];
fun mor_tac ((mor_image, morE), map_comp_id) =
- EVERY' [rtac ctxt ballI, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
+ EVERY' [rtac ctxt @{thm ballI}, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE,
etac ctxt mor_image, assume_tac ctxt];
in
@@ -151,24 +151,24 @@
let
val n = length morEs;
fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
- rtac ctxt UNIV_I, rtac ctxt sym, rtac ctxt o_apply];
+ rtac ctxt @{thm UNIV_I}, rtac ctxt sym, rtac ctxt o_apply];
in
EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
- rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs,
+ rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) morEs,
CONJ_WRAP' (fn i =>
- EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt ballI, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1
+ EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt @{thm ballI}, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1
end;
fun mk_mor_str_tac ctxt ks mor_UNIV =
(rtac ctxt (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac ctxt refl)) ks) 1;
fun mk_set_incl_Jset_tac ctxt rec_Suc =
- EVERY' (map (rtac ctxt) [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym,
- rec_Suc]) 1;
+ EVERY' (map (rtac ctxt) (@{thms SUP_upper2 UNIV_I ord_le_eq_trans Un_upper1 sym} @
+ [rec_Suc])) 1;
fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i =
- EVERY' (map (rtac ctxt) [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2,
- rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
+ EVERY' (map (rtac ctxt) (@{thms UN_least subsetI UN_I UNIV_I set_mp equalityD2} @
+ [rec_Suc, @{thm UnI2}, mk_UnIN n i]) @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
@@ -182,7 +182,7 @@
else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
(K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE],
- rtac ctxt subset_trans, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
+ rtac ctxt @{thm subset_trans}, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
rec_Sucs] 1;
fun mk_Jset_minimal_tac ctxt n col_minimal =
@@ -221,18 +221,18 @@
fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
- etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
+ etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt @{thm bexE},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
assume_tac ctxt])
@{thms fst_diag_id snd_diag_id},
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn (i, thm) =>
if i <= m
- then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans,
- etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
+ then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm subset_trans},
+ etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
rtac ctxt @{thm case_prodI}, rtac ctxt refl]
else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}])
@@ -242,9 +242,9 @@
EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
dtac ctxt (in_rel RS @{thm iffD1}),
- REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
- @{thms CollectE Collect_case_prod_in_rel_leE}),
- rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
+ REPEAT_DETERM o eresolve_tac ctxt
+ @{thms CollectE conjE exE CollectE Collect_case_prod_in_rel_leE},
+ rtac ctxt @{thm bexI}, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
@@ -253,7 +253,7 @@
rtac ctxt trans, rtac ctxt map_cong0,
REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt],
REPEAT_DETERM_N n o rtac ctxt refl,
- assume_tac ctxt, rtac ctxt CollectI,
+ assume_tac ctxt, rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn (i, thm) =>
if i <= m then rtac ctxt subset_UNIV
else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
@@ -268,8 +268,8 @@
fun mk_bis_converse_tac ctxt m bis_rel rel_congs rel_converseps =
EVERY' [rtac ctxt (bis_rel RS iffD2), dtac ctxt (bis_rel RS iffD1),
REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
- CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt subset_trans,
- rtac ctxt equalityD2, rtac ctxt @{thm converse_Times}])) rel_congs,
+ CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt @{thm subset_trans},
+ rtac ctxt @{thm equalityD2}, rtac ctxt @{thm converse_Times}])) rel_congs,
CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
@@ -312,13 +312,13 @@
unfold_thms_tac ctxt [bis_def] THEN
EVERY' [rtac ctxt conjI,
CONJ_WRAP' (fn i =>
- EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, assume_tac ctxt,
+ EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt @{thm bspec}, assume_tac ctxt,
dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks,
CONJ_WRAP' (fn (i, in_mono) =>
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E},
- dtac ctxt bspec, assume_tac ctxt,
+ dtac ctxt @{thm bspec}, assume_tac ctxt,
dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp,
- assume_tac ctxt, etac ctxt bexE, rtac ctxt bexI, assume_tac ctxt, rtac ctxt in_mono,
+ assume_tac ctxt, etac ctxt @{thm bexE}, rtac ctxt @{thm bexI}, assume_tac ctxt, rtac ctxt in_mono,
REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]},
assume_tac ctxt]) (ks ~~ in_monos)] 1
end;
@@ -328,14 +328,14 @@
val n = length lsbis_defs;
in
EVERY' [rtac ctxt (Thm.permute_prems 0 1 bis_cong), EVERY' (map (rtac ctxt) lsbis_defs),
- rtac ctxt bis_Union, rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, exE],
+ rtac ctxt bis_Union, rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE exE},
hyp_subst_tac ctxt, etac ctxt bis_cong, EVERY' (map (rtac ctxt o mk_nth_conv n) (1 upto n))] 1
end;
fun mk_incl_lsbis_tac ctxt n i lsbis_def =
- EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt CollectI,
+ EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt @{thm CollectI},
REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
- rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1;
+ rtac ctxt @{thm equalityD2}, rtac ctxt (mk_nth_conv n i)] 1;
fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
EVERY' [rtac ctxt @{thm equivI},
@@ -359,26 +359,26 @@
val n = length strT_defs;
val ks = 1 upto n;
fun coalg_tac (i, (active_sets, def)) =
- EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
+ EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE},
hyp_subst_tac ctxt, rtac ctxt (def RS trans RS @{thm ssubst_mem}), etac ctxt (arg_cong RS trans),
- rtac ctxt (mk_sum_caseN n i), rtac ctxt CollectI,
+ rtac ctxt (mk_sum_caseN n i), rtac ctxt @{thm CollectI},
REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
CONJ_WRAP' (fn (i, thm) => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
- rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
+ rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
rtac ctxt conjI,
rtac ctxt conjI, etac ctxt @{thm empty_Shift}, dtac ctxt set_rev_mp,
- etac ctxt equalityD1, etac ctxt CollectD,
- rtac ctxt ballI,
- CONJ_WRAP' (fn i => EVERY' [rtac ctxt ballI, etac ctxt CollectE, dtac ctxt @{thm ShiftD},
- dtac ctxt bspec, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
- dtac ctxt bspec, rtac ctxt CollectI, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
+ etac ctxt @{thm equalityD1}, etac ctxt @{thm CollectD},
+ rtac ctxt @{thm ballI},
+ CONJ_WRAP' (fn i => EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm CollectE}, dtac ctxt @{thm ShiftD},
+ dtac ctxt @{thm bspec}, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
+ dtac ctxt @{thm bspec}, rtac ctxt @{thm CollectI}, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt,
CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
- dtac ctxt bspec, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec,
+ dtac ctxt @{thm bspec}, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt @{thm bspec},
etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt,
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
@@ -400,14 +400,14 @@
EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn Lev_0 =>
- EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
+ EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
etac ctxt @{thm singletonE}, etac ctxt ssubst, rtac ctxt @{thm list.size(3)}]) Lev_0s,
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn Lev_Suc =>
- EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
- CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
+ EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
+ CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
(fn i =>
- EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
+ EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt,
rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]},
REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
etac ctxt mp, assume_tac ctxt]) ks])
@@ -450,16 +450,16 @@
EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
- EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
+ EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
CONJ_WRAP' (fn i' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
(if i = i'
then EVERY' [dtac ctxt (mk_InN_inject n i), hyp_subst_tac ctxt,
CONJ_WRAP' (fn (i'', Lev_0'') =>
EVERY' [rtac ctxt impI, rtac ctxt @{thm ssubst_mem[OF append_Nil]},
- rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i''),
- rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
- etac ctxt conjI, rtac ctxt (Lev_0'' RS equalityD2 RS set_mp),
+ rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp), rtac ctxt (mk_UnIN n i''),
+ rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
+ etac ctxt conjI, rtac ctxt (Lev_0'' RS @{thm equalityD2} RS set_mp),
rtac ctxt @{thm singletonI}])
(ks ~~ Lev_0s)]
else etac ctxt (mk_InN_not_InM i' i RS notE)))
@@ -467,15 +467,15 @@
((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
- EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
- CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
+ EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
+ CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
(fn (i, from_to_sbd) =>
- EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
+ EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt,
CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
CONJ_WRAP' (fn i'' =>
- EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS equalityD2 RS set_mp),
+ EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp),
rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i),
- rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
+ rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym),
rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans),
etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE,
@@ -496,19 +496,19 @@
EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
- EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
+ EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
CONJ_WRAP' (fn i'' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
(if i = i''
then EVERY' [dtac ctxt @{thm ssubst_mem[OF sym[OF append_Nil]]},
- dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), dtac ctxt (mk_InN_inject n i),
+ dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp), dtac ctxt (mk_InN_inject n i),
hyp_subst_tac ctxt,
- CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
- (fn k => REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
+ CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
+ (fn k => REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN'
dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
(if k = i'
- then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt imageI]
+ then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt @{thm imageI}]
else etac ctxt (mk_InN_not_InM i' k RS notE)))
(rev ks)]
else etac ctxt (mk_InN_not_InM i'' i RS notE)))
@@ -517,15 +517,15 @@
((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
- EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
- CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
+ EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
+ CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
(fn (i, (from_to_sbd, to_sbd_inj)) =>
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN' hyp_subst_tac ctxt THEN'
CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
dtac ctxt @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
- dtac ctxt (Lev_Suc RS equalityD1 RS set_mp) THEN'
- CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn k =>
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
+ dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp) THEN'
+ CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE})) (fn k =>
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN'
dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
(if k = i
then EVERY' [dtac ctxt (mk_InN_inject n i),
@@ -556,26 +556,26 @@
fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'),
(rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) =
- EVERY' [rtac ctxt ballI, rtac ctxt (carT_def RS equalityD2 RS set_mp),
- rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI,
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (carT_def RS @{thm equalityD2} RS set_mp),
+ rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI,
rtac ctxt conjI,
- rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
+ rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp),
rtac ctxt @{thm singletonI},
(**)
- rtac ctxt ballI, etac ctxt @{thm UN_E},
+ rtac ctxt @{thm ballI}, etac ctxt @{thm UN_E},
CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
(set_Levs, set_image_Levs))))) =>
- EVERY' [rtac ctxt ballI,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
+ EVERY' [rtac ctxt @{thm ballI},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
rtac ctxt (rev_mp OF [rv_last, impI]), etac ctxt exE, rtac ctxt (isNode_def RS iffD2),
rtac ctxt exI, rtac ctxt conjI,
if n = 1 then rtac ctxt refl
else etac ctxt (sum_case_cong_weak RS trans) THEN' rtac ctxt (mk_sum_caseN n i),
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
- EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
- rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, etac ctxt set_Lev,
- if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt subsetI,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
+ EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt @{thm equalityI}, rtac ctxt @{thm image_subsetI},
+ rtac ctxt @{thm CollectI}, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, etac ctxt set_Lev,
+ if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt @{thm subsetI},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
REPEAT_DETERM_N 4 o etac ctxt thin_rl,
rtac ctxt set_image_Lev,
assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
@@ -590,12 +590,12 @@
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
if n = 1 then rtac ctxt refl else rtac ctxt (mk_sum_caseN n i),
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
- EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
- rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt set_Lev,
- rtac ctxt (Lev_0 RS equalityD2 RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
- assume_tac ctxt, rtac ctxt subsetI,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
- rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
+ EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt @{thm equalityI}, rtac ctxt @{thm image_subsetI},
+ rtac ctxt @{thm CollectI}, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, rtac ctxt set_Lev,
+ rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
+ assume_tac ctxt, rtac ctxt @{thm subsetI},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
+ rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp),
rtac ctxt @{thm singletonI}, dtac ctxt length_Lev',
etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF
trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
@@ -604,7 +604,7 @@
fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)),
((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
- EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def,
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def,
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
@@ -614,20 +614,20 @@
EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd =>
DETERM o EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt prod_injectI, rtac ctxt conjI,
rtac ctxt trans, rtac ctxt @{thm Shift_def},
- rtac ctxt equalityI, rtac ctxt subsetI, etac ctxt thin_rl,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm UN_E}], dtac ctxt length_Lev', dtac ctxt asm_rl,
+ rtac ctxt @{thm equalityI}, rtac ctxt @{thm subsetI}, etac ctxt thin_rl,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE UN_E}, dtac ctxt length_Lev', dtac ctxt asm_rl,
etac ctxt thin_rl, dtac ctxt @{thm set_rev_mp[OF _ equalityD1]},
rtac ctxt (@{thm length_Cons} RS arg_cong RS trans), rtac ctxt Lev_Suc,
- CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn i'' =>
- EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
+ CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE})) (fn i'' =>
+ EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE},
dtac ctxt list_inject_iffD1, etac ctxt conjE,
if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'),
dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
else etac ctxt (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
- rtac ctxt @{thm UN_least}, rtac ctxt subsetI, rtac ctxt CollectI, rtac ctxt @{thm UN_I[OF UNIV_I]},
- rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt CollectI,
+ rtac ctxt @{thm UN_least}, rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm UN_I[OF UNIV_I]},
+ rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt @{thm CollectI},
REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt,
rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI,
CONVERSION (Conv.top_conv
@@ -651,7 +651,7 @@
fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs =
EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans),
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE bexE}, rtac ctxt (o_apply RS trans),
etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
EVERY' (map (fn equiv_LSBIS =>
@@ -663,7 +663,7 @@
EVERY' [rtac ctxt (coalg_def RS iffD2),
CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
EVERY' [rtac ctxt @{thm univ_preserves}, rtac ctxt equiv_LSBIS, rtac ctxt congruent_str_final,
- rtac ctxt ballI, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt CollectI,
+ rtac ctxt @{thm ballI}, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt @{thm CollectI},
REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
@@ -675,22 +675,22 @@
fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs =
EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI,
CONJ_WRAP' (fn equiv_LSBIS =>
- EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
rtac ctxt equiv_LSBIS, assume_tac ctxt])
equiv_LSBISs,
CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
- EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply])
(equiv_LSBISs ~~ congruent_str_finals)] 1;
fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
unfold_thms_tac ctxt defs THEN
EVERY' [rtac ctxt conjI,
- CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps,
+ CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' rtac ctxt thm) Reps,
CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
- EVERY' [rtac ctxt ballI, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L,
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L,
EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
- EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse,
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse,
etac ctxt set_rev_mp, rtac ctxt coalg_final_set, rtac ctxt Rep])
Abs_inverses coalg_final_sets)])
(Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
@@ -698,8 +698,8 @@
fun mk_mor_Abs_tac ctxt defs Abs_inverses =
unfold_thms_tac ctxt defs THEN
EVERY' [rtac ctxt conjI,
- CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
- CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1;
+ CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) Abs_inverses,
+ CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1;
fun mk_mor_unfold_tac ctxt m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
EVERY' [rtac ctxt iffD2, rtac ctxt mor_UNIV,
@@ -727,12 +727,12 @@
rtac ctxt mor_T_final, EVERY' (map (fn thm => rtac ctxt (thm RS @{thm relInvImage_Gr})) lsbis_incls),
rtac ctxt impI,
CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
- EVERY' [rtac ctxt subset_trans, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt subset_trans,
- rtac ctxt @{thm relInvImage_mono}, rtac ctxt subset_trans, etac ctxt incl_lsbis,
+ EVERY' [rtac ctxt @{thm subset_trans}, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt @{thm subset_trans},
+ rtac ctxt @{thm relInvImage_mono}, rtac ctxt @{thm subset_trans}, etac ctxt incl_lsbis,
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]},
rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong},
rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl,
- rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
+ rtac ctxt @{thm subset_trans}, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on},
rtac ctxt Rep_inject])
(Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
@@ -742,13 +742,13 @@
CONJ_WRAP' (fn (raw_coind, unfold_def) =>
EVERY' [rtac ctxt @{thm ext}, etac ctxt (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac ctxt mor,
rtac ctxt @{thm image2_eqI}, rtac ctxt refl, rtac ctxt (unfold_def RS arg_cong RS trans),
- rtac ctxt (o_apply RS sym), rtac ctxt UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
+ rtac ctxt (o_apply RS sym), rtac ctxt @{thm UNIV_I}]) (raw_coinds ~~ unfold_defs) 1;
fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply,
rtac ctxt trans, rtac ctxt unfold, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
EVERY' (map (fn thm =>
- rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
+ rtac ctxt @{thm ballI} THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
rtac ctxt sym, rtac ctxt id_apply] 1;
fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
@@ -770,11 +770,11 @@
REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
REPEAT_DETERM_N m o rtac ctxt refl,
REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]},
- etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm case_prodD}])
+ etac ctxt mp, etac ctxt @{thm CollectE}, etac ctxt @{thm case_prodD}])
rel_congs,
rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp,
- rtac ctxt CollectI, etac ctxt @{thm case_prodI}])) rel_congs] 1;
+ rtac ctxt @{thm CollectI}, etac ctxt @{thm case_prodI}])) rel_congs] 1;
fun mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0 =
EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (o_apply RS trans RS sym),
@@ -789,8 +789,8 @@
REPEAT_DETERM_N n o rtac ctxt @{thm Un_upper1},
REPEAT_DETERM_N n o
EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
- EVERY' [rtac ctxt subsetI, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
- etac ctxt UnE, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt UnE,
+ EVERY' [rtac ctxt @{thm subsetI}, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
+ etac ctxt @{thm UnE}, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt @{thm UnE},
EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)])
(1 upto n) set_Jsets set_Jset_Jsetss)] 1;
@@ -831,27 +831,27 @@
REPEAT_DETERM_N n o rtac ctxt fst_convol_fun_cong_sym,
rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0,
EVERY' (maps (fn set_Jset =>
- [rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt CollectE,
- REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, etac ctxt set_Jset]) set_Jsets),
+ [rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt @{thm CollectE},
+ REPEAT_DETERM o etac ctxt conjE, etac ctxt @{thm bspec}, etac ctxt set_Jset]) set_Jsets),
REPEAT_DETERM_N n o rtac ctxt snd_convol_fun_cong_sym,
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
EVERY' (map (fn set_map0 => EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
- rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt refl])
+ rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI}, rtac ctxt refl])
(take m set_map0s)),
CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
- rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI,
- rtac ctxt CollectI, etac ctxt CollectE,
+ rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI,
+ rtac ctxt @{thm CollectI}, etac ctxt @{thm CollectE},
REPEAT_DETERM o etac ctxt conjE,
CONJ_WRAP' (fn set_Jset_Jset =>
- EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
+ EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm bspec}, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
rtac ctxt (conjI OF [refl, refl])])
(drop m set_map0s ~~ set_Jset_Jsetss)])
(map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @
[rtac ctxt impI,
CONJ_WRAP' (fn k =>
- EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt CollectI,
+ EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt @{thm CollectI},
rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) ks]) 1
end
@@ -898,7 +898,7 @@
REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})),
EVERY' (map2 (fn i => fn set_sbd => EVERY' [
rtac ctxt (@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [sbd_regularCard,
- sbd_Cinfinite]), rtac ctxt set_sbd, rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE,
+ sbd_Cinfinite]), rtac ctxt set_sbd, rtac ctxt @{thm ballI}, REPEAT_DETERM o etac ctxt allE,
etac ctxt (mk_conjunctN n i)]) (1 upto n) (drop m set_sbds))])
(rec_Sucs ~~ set_sbdss)] 1
end;
@@ -906,7 +906,7 @@
fun mk_set_bd_tac ctxt sbd_Cinfinite sbd_regularCard natLeq_ordLess_bd col_bd =
EVERY' (map (rtac ctxt) [@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [
sbd_regularCard, sbd_Cinfinite], @{thm ordIso_ordLess_trans}, @{thm card_of_nat},
- natLeq_ordLess_bd, ballI, col_bd]) 1;
+ natLeq_ordLess_bd, @{thm ballI}, col_bd]) 1;
fun mk_le_rel_OO_tac ctxt coinduct rel_Jrels le_rel_OOs =
EVERY' (rtac ctxt coinduct :: map2 (fn rel_Jrel => fn le_rel_OO =>
@@ -920,21 +920,21 @@
fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN
REPEAT_DETERM (assume_tac ctxt 1 ORELSE
- EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
+ EVERY' [dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt dtor_set,
K (unfold_thms_tac ctxt dtor_ctors),
- REPEAT_DETERM_N n o etac ctxt UnE,
+ REPEAT_DETERM_N n o etac ctxt @{thm UnE},
REPEAT_DETERM o
- (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
+ (TRY o REPEAT_DETERM o etac ctxt @{thm UnE} THEN' TRY o etac ctxt @{thm UN_E} THEN'
(eresolve_tac ctxt wit ORELSE'
(dresolve_tac ctxt wit THEN'
(etac ctxt FalseE ORELSE'
- EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
- K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac ctxt UnE]))))] 1);
+ EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt dtor_set,
+ K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac ctxt @{thm UnE}]))))] 1);
fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
rtac ctxt induct 1 THEN ALLGOALS (TRY o rtac ctxt impI THEN' TRY o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
- ALLGOALS (REPEAT_DETERM o etac ctxt imageE THEN' TRY o hyp_subst_tac ctxt) THEN
+ ALLGOALS (REPEAT_DETERM o etac ctxt @{thm imageE} THEN' TRY o hyp_subst_tac ctxt) THEN
ALLGOALS (TRY o
FIRST' [rtac ctxt TrueI, rtac ctxt refl, etac ctxt (refl RSN (2, mp)), dresolve_tac ctxt wits THEN' etac ctxt FalseE]);
@@ -963,16 +963,16 @@
val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
val in_Jrel = nth in_Jrels (i - 1);
val if_tac =
- EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
- rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+ EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+ rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
EVERY' (map2 (fn set_map0 => fn set_incl =>
EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply,
etac ctxt (set_incl RS @{thm subset_trans})])
passive_set_map0s dtor_set_incls),
CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
- EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
- rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+ EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls,
rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
(in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
@@ -983,8 +983,8 @@
rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt])
@{thms fst_conv snd_conv}];
val only_if_tac =
- EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
- rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+ EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+ rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least},
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0,
@@ -993,14 +993,14 @@
(fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans,
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least},
- dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
+ dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt @{thm imageE},
dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
- REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
- @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+ REPEAT_DETERM o eresolve_tac ctxt
+ @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
hyp_subst_tac ctxt,
dtac ctxt (in_Jrel RS iffD1),
dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, assume_tac ctxt])
(rev (active_set_map0s ~~ in_Jrels))])
(dtor_sets ~~ passive_set_map0s),
rtac ctxt conjI,
@@ -1009,8 +1009,8 @@
rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
- REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
- @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+ REPEAT_DETERM o eresolve_tac ctxt
+ @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels),
assume_tac ctxt]]
@@ -1031,7 +1031,7 @@
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, hyp_subst_tac ctxt,
rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI,
rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym),
rtac ctxt (dtor_unfold RS map_arg_cong RS trans), rtac ctxt (trans OF [map_comp0, map_cong]),
@@ -1042,10 +1042,10 @@
REPEAT_DETERM_N n o (rtac ctxt @{thm trans[OF o_apply]} THEN' rtac ctxt @{thm snd_conv}),
etac ctxt (@{thm prod.case} RS map_arg_cong RS trans),
SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}),
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn set_map0 =>
EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
- rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI},
+ rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI},
FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp,
assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
set_map0s])
@@ -1061,18 +1061,18 @@
EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
+ REPEAT_DETERM o eresolve_tac ctxt [@{thm CollectE}, @{thm conjE}, Collect_splitD_set_mp, set_rev_mp],
hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
- rtac ctxt subset_refl])
+ rtac ctxt @{thm subset_refl}])
unfolds set_map0ss ks) 1 THEN
EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
EVERY' (map (fn set_map0 =>
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
- etac ctxt imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
+ etac ctxt @{thm imageE}, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt,
rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
(drop m set_map0s)))
@@ -1087,13 +1087,13 @@
REPEAT_DETERM (etac ctxt exE 1) THEN
CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
EVERY' [rtac ctxt @{thm predicate2I}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI,
- if null helper_inds then rtac ctxt UNIV_I
- else rtac ctxt CollectI THEN'
+ if null helper_inds then rtac ctxt @{thm UNIV_I}
+ else rtac ctxt @{thm CollectI} THEN'
CONJ_WRAP' (fn helper_ind =>
EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI,
- REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
- dtac ctxt bspec, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
+ REPEAT_DETERM o resolve_tac ctxt @{thms subsetI CollectI iffD2[OF split_beta]},
+ dtac ctxt @{thm bspec}, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
etac ctxt (refl RSN (2, conjI))])
helper_inds,
rtac ctxt conjI,
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sun May 18 14:33:01 2025 +0000
@@ -214,7 +214,7 @@
end;
val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
- val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
+ val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m @{thm subset_refl})) bnfs;
val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
val timer = time (timer "Derived simple theorems");
@@ -461,7 +461,7 @@
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
typedef (sbdT_bind, sum_bdT_params', NoSyn)
(HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt =>
- EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+ EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
val sbdT = Type (sbdT_name, sum_bdT_params);
val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
@@ -751,12 +751,12 @@
val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
typedef (IIT_bind, params, NoSyn)
- (HOLogic.mk_UNIV II_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+ (HOLogic.mk_UNIV II_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
val IIT = Type (IIT_name, params');
val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT);
- val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info;
+ val Abs_IIT_inverse_thm = @{thm UNIV_I} RS #Abs_inverse IIT_loc_info;
val initT = IIT --> Asuc_bdT;
val active_initTs = replicate n initT;
@@ -1080,7 +1080,7 @@
end;
val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
- ((rtac lthy CollectI THEN' CONJ_WRAP' (K (rtac lthy @{thm subset_UNIV})) (1 upto m + n)) 1)
+ ((rtac lthy @{thm CollectI} THEN' CONJ_WRAP' (K (rtac lthy @{thm subset_UNIV})) (1 upto m + n)) 1)
(mor_fold_thm RS morE)) morE_thms;
val (fold_unique_mor_thms, fold_unique_mor_thm) =
@@ -1389,7 +1389,7 @@
val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) =
typedef (sbd0T_bind, sum_bd0T_params', NoSyn)
(HOLogic.mk_UNIV sum_bd0T) NONE (fn ctxt =>
- EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+ EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
val sbd0T = Type (sbd0T_name, sum_bd0T_params);
val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T);
@@ -1564,8 +1564,8 @@
fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) ::
map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS
- (mk_Un_upper n i RS subset_trans) RSN
- (2, @{thm UN_upper} RS subset_trans))
+ (mk_Un_upper n i RS @{thm subset_trans}) RSN
+ (2, @{thm UN_upper} RS @{thm subset_trans}))
(1 upto n);
val set_Iset_thmsss = transpose (map (map mk_set_thms) ctor_Iset_thmss);
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sun May 18 14:33:01 2025 +0000
@@ -86,20 +86,20 @@
val ord_eq_le_trans = @{thm ord_eq_le_trans};
val subset_trans = @{thm subset_trans};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
-val rev_bspec = Drule.rotate_prems 1 bspec;
+val rev_bspec = Drule.rotate_prems 1 @{thm bspec};
val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\<union>)"]};
val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]};
fun mk_alg_set_tac ctxt alg_def =
- EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI,
+ EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt @{thm bspec}, rtac ctxt @{thm CollectI},
REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1;
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
(EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
REPEAT_DETERM o FIRST'
[EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits],
- EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits],
- EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
+ EVERY' [rtac ctxt @{thm subsetI}, rtac ctxt FalseE, eresolve_tac ctxt wits],
+ EVERY' [rtac ctxt @{thm subsetI}, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN'
etac ctxt @{thm emptyE}) 1;
@@ -107,30 +107,30 @@
(dtac ctxt (mor_def RS iffD1) THEN'
REPEAT o etac ctxt conjE THEN'
TRY o rtac ctxt @{thm image_subsetI} THEN'
- etac ctxt bspec THEN'
+ etac ctxt @{thm bspec} THEN'
assume_tac ctxt) 1;
fun mk_mor_incl_tac ctxt mor_def map_ids =
(rtac ctxt (mor_def RS iffD2) THEN'
rtac ctxt conjI THEN'
- CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
+ CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
map_ids THEN'
CONJ_WRAP' (fn thm =>
- (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1;
+ (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1;
fun mk_mor_comp_tac ctxt mor_def set_maps map_comp_ids =
let
val fbetw_tac =
- EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}),
- etac ctxt bspec, etac ctxt bspec, assume_tac ctxt];
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS @{thm ssubst_mem}),
+ etac ctxt @{thm bspec}, etac ctxt @{thm bspec}, assume_tac ctxt];
fun mor_tac (set_map, map_comp_id) =
- EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS trans), rtac ctxt trans,
rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
- REPEAT o eresolve_tac ctxt [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
+ REPEAT o eresolve_tac ctxt @{thms CollectE conjE}, etac ctxt @{thm bspec}, rtac ctxt @{thm CollectI}] THEN'
CONJ_WRAP' (fn thm =>
FIRST' [rtac ctxt subset_UNIV,
(EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
- etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
+ etac ctxt @{thm bspec}, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
rtac ctxt (map_comp_id RS arg_cong);
in
(dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN'
@@ -142,20 +142,20 @@
fun mk_mor_str_tac ctxt ks mor_def =
(rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
- CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN'
- CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1;
+ CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm UNIV_I}])) ks THEN'
+ CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt refl])) ks) 1;
fun mk_mor_UNIV_tac ctxt m morEs mor_def =
let
val n = length morEs;
fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
- rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n),
+ rtac ctxt @{thm CollectI}, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n),
rtac ctxt sym, rtac ctxt o_apply];
in
EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
- rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs,
+ rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) morEs,
REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM_N n o dtac ctxt (@{thm fun_eq_iff} RS iffD1),
- CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans,
+ CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans,
etac ctxt (o_apply RS sym RS trans), rtac ctxt o_apply])) morEs] 1
end;
@@ -164,17 +164,17 @@
val n = length alg_sets;
fun set_tac thm =
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono},
- rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}];
+ rtac ctxt @{thm equalityD1}, etac ctxt @{thm bij_betw_imp_surj_on}];
val alg_tac =
CONJ_WRAP' (fn (set_maps, alg_set) =>
- EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
- rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
- rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
+ EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt set_mp,
+ rtac ctxt @{thm equalityD1}, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
+ rtac ctxt @{thm imageI}, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
(set_mapss ~~ alg_sets);
val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN'
CONJ_WRAP' (fn (set_maps, alg_set) =>
- EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
+ EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set,
EVERY' (map set_tac (drop m set_maps))])
(set_mapss ~~ alg_sets);
@@ -187,15 +187,15 @@
EVERY' [REPEAT_DETERM o etac ctxt conjE, rtac ctxt rev_mp, rtac ctxt @{thm Cinfinite_limit_finite},
REPEAT_DETERM_N n o rtac ctxt @{thm finite.insertI}, rtac ctxt @{thm finite.emptyI},
REPEAT_DETERM_N n o etac ctxt @{thm insert_subsetI}, rtac ctxt @{thm empty_subsetI},
- rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt bexE, rtac ctxt bexI,
+ rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt @{thm bexE}, rtac ctxt @{thm bexI},
CONJ_WRAP' (fn i =>
- EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
+ EVERY' [etac ctxt @{thm bspec}, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
(0 upto n - 1),
assume_tac ctxt] 1;
fun mk_min_algs_tac ctxt worel in_congs =
let
- val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec,
+ val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt @{thm bspec},
assume_tac ctxt, etac ctxt arg_cong];
fun minH_tac thm =
EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm,
@@ -208,9 +208,9 @@
end;
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
- rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI,
- rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
- assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD},
+ rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt @{thm subsetI},
+ rtac ctxt @{thm UnI1}, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
+ assume_tac ctxt, rtac ctxt @{thm equalityD1}, dtac ctxt @{thm notnotD},
hyp_subst_tac ctxt, rtac ctxt refl] 1;
fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
@@ -234,7 +234,7 @@
val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq},
rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order,
- assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE,
+ assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt @{thm ballI}, etac ctxt allE,
dtac ctxt mp, etac ctxt @{thm underS_E},
dtac ctxt mp, etac ctxt @{thm underS_Field},
REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite]
@@ -271,7 +271,7 @@
fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, etac ctxt alg_set,
REPEAT_DETERM o (etac ctxt subset_trans THEN' minG_tac)];
in
(rtac ctxt induct THEN'
@@ -284,21 +284,21 @@
let
val n = length min_algs;
fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
- [rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
+ [rtac ctxt @{thm bexE}, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds];
fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
- EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
- EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
+ EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
+ EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt @{thm bexE},
rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl,
assume_tac ctxt, rtac ctxt set_mp,
- rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2,
+ rtac ctxt @{thm equalityD2}, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt @{thm UnI2},
rtac ctxt @{thm image_eqI}, rtac ctxt refl,
- rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
+ rtac ctxt @{thm CollectI}, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
REPEAT_DETERM o etac ctxt conjE,
CONJ_WRAP' (K (FIRST' [assume_tac ctxt,
- EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I},
+ EVERY' [etac ctxt subset_trans, rtac ctxt @{thm subsetI}, rtac ctxt @{thm UN_I},
etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]]))
set_bds];
in
@@ -310,7 +310,7 @@
EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}),
rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans},
rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq},
- rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of,
+ rtac ctxt suc_Asuc, rtac ctxt @{thm ballI}, dtac ctxt rev_mp, rtac ctxt card_of,
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1;
fun mk_least_min_alg_tac ctxt min_alg_def least =
@@ -319,8 +319,8 @@
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1;
fun mk_alg_select_tac ctxt Abs_inverse =
- EVERY' [rtac ctxt ballI,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
+ EVERY' [rtac ctxt @{thm ballI},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt] 1 THEN
unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1;
fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
@@ -329,16 +329,16 @@
val n = length alg_sets;
val fbetw_tac =
CONJ_WRAP'
- (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec,
- etac ctxt CollectE, assume_tac ctxt])) alg_sets;
+ (K (EVERY' [rtac ctxt @{thm ballI}, etac ctxt rev_bspec,
+ etac ctxt @{thm CollectE}, assume_tac ctxt])) alg_sets;
val mor_tac =
- CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
+ CONJ_WRAP' (fn thm => EVERY' [rtac ctxt @{thm ballI}, rtac ctxt thm]) str_init_defs;
fun alg_epi_tac ((alg_set, str_init_def), set_map) =
- EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
- rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec],
+ EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm ballI}, forward_tac ctxt [alg_select RS @{thm bspec}],
rtac ctxt (str_init_def RS @{thm ssubst_mem}),
etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
- rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
+ rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt @{thm bspec},
assume_tac ctxt]];
in
EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}),
@@ -355,7 +355,7 @@
REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
- rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
+ rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI,
rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1
@@ -368,7 +368,7 @@
val ks = (1 upto n);
fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono,
- REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
+ REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt @{thm CollectI},
REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
fun cong_tac ct map_cong0 = EVERY'
[rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong),
@@ -376,8 +376,8 @@
REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
- EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm CollectI},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
rtac ctxt trans, mor_tac morE in_mono,
rtac ctxt trans, cong_tac ct map_cong0,
@@ -395,17 +395,17 @@
let
val n = length least_min_algs;
- fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
+ fun mk_alg_tac alg_set = EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm CollectI},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
- rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
+ rtac ctxt mp, etac ctxt @{thm bspec}, rtac ctxt @{thm CollectI},
REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets,
- CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
+ CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
alg_sets];
fun mk_induct_tac least_min_alg =
- rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
+ rtac ctxt @{thm ballI} THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
rtac ctxt (alg_def RS iffD2) THEN'
CONJ_WRAP' mk_alg_tac alg_sets;
in
@@ -415,9 +415,9 @@
fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss =
unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
EVERY' [rtac ctxt conjI,
- CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps,
+ CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' rtac ctxt thm) Reps,
CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) =>
- EVERY' [rtac ctxt ballI, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set),
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set),
EVERY' (map2 (fn Rep => fn set_map =>
EVERY' [rtac ctxt (set_map RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt Rep])
Reps (drop m set_maps))])
@@ -426,12 +426,12 @@
fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs =
unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
EVERY' [rtac ctxt conjI,
- CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
+ CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) Abs_inverses,
CONJ_WRAP' (fn (ct, thm) =>
- EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
+ EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
EVERY' (map (fn Abs_inverse =>
- EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
+ EVERY' [rtac ctxt (o_apply RS trans RS @{thm ballI}), etac ctxt (set_mp RS Abs_inverse),
assume_tac ctxt])
Abs_inverses)])
(cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;
@@ -445,7 +445,7 @@
let
fun mk_unique type_def =
EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
- rtac ctxt ballI, resolve_tac ctxt init_unique_mors,
+ rtac ctxt @{thm ballI}, resolve_tac ctxt init_unique_mors,
EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
@@ -456,7 +456,7 @@
fun mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt (dtor_def RS fun_cong RS trans),
rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
- EVERY' (map (fn thm => rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply]))
+ EVERY' (map (fn thm => rtac ctxt @{thm ballI} THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply]))
ctor_o_folds),
rtac ctxt sym, rtac ctxt id_apply] 1;
@@ -477,19 +477,19 @@
val ks = 1 upto n;
fun mk_IH_tac Rep_inv Abs_inv set_map =
- DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec,
- dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE,
+ DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt @{thm bspec},
+ dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, rtac ctxt set_map, etac ctxt @{thm imageE},
hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp,
assume_tac ctxt, assume_tac ctxt];
fun mk_closed_tac (k, (morE, set_maps)) =
- EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI,
+ EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt @{thm ballI}, rtac ctxt impI,
rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec},
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, dtac ctxt @{thm meta_spec},
EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt];
fun mk_induct_tac (Rep, Rep_inv) =
- EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))];
+ EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, @{thm bspec}))];
in
(rtac ctxt mp THEN' rtac ctxt impI THEN'
DETERM o CONJ_WRAP_GEN' (etac ctxt conjE THEN' rtac ctxt conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
@@ -572,7 +572,7 @@
rtac ctxt (@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [
bd_regularCard, bd_Cinfinite, set_bd
]),
- rtac ctxt ballI,
+ rtac ctxt @{thm ballI},
Goal.assume_rule_tac ctxt
];
@@ -587,11 +587,11 @@
fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps =
let
- fun use_asm thm = EVERY' [etac ctxt bspec, etac ctxt set_rev_mp, rtac ctxt thm];
+ fun use_asm thm = EVERY' [etac ctxt @{thm bspec}, etac ctxt set_rev_mp, rtac ctxt thm];
fun useIH set_sets = EVERY' [rtac ctxt mp, Goal.assume_rule_tac ctxt,
CONJ_WRAP' (fn thm =>
- EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_rev_mp, etac ctxt thm]) set_sets];
+ EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm bspec}, etac ctxt set_rev_mp, etac ctxt thm]) set_sets];
fun mk_map_cong0 ctor_map map_cong0 set_setss =
EVERY' [rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
@@ -610,9 +610,9 @@
REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2),
rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}),
rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt,
- REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt],
+ REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm ballI}, rtac ctxt impI, assume_tac ctxt],
REPEAT_DETERM_N (length le_rel_OOs) o
- EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]])
+ EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm ballI}, Goal.assume_rule_tac ctxt]])
ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
(* BNF tactics *)
@@ -645,14 +645,14 @@
fun mk_wit_tac ctxt n ctor_set wit =
REPEAT_DETERM (assume_tac ctxt 1 ORELSE
- EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
+ EVERY' [dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt ctor_set,
REPEAT_DETERM o
- (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
+ (TRY o REPEAT_DETERM o etac ctxt @{thm UnE} THEN' TRY o etac ctxt @{thm UN_E} THEN'
(eresolve_tac ctxt wit ORELSE'
(dresolve_tac ctxt wit THEN'
(etac ctxt FalseE ORELSE'
- EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
- REPEAT_DETERM_N n o etac ctxt UnE]))))] 1);
+ EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt ctor_set,
+ REPEAT_DETERM_N n o etac ctxt @{thm UnE}]))))] 1);
fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss =
@@ -665,16 +665,16 @@
val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
val if_tac =
- EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
- rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+ EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+ rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
EVERY' (map2 (fn set_map0 => fn ctor_set_incl =>
EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply,
rtac ctxt (ctor_set_incl RS subset_trans), etac ctxt le_arg_cong_ctor_dtor])
passive_set_map0s ctor_set_incls),
CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
- EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
- rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+ EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn thm =>
EVERY' (map (etac ctxt) [thm RS subset_trans, le_arg_cong_ctor_dtor]))
ctor_set_set_incls,
@@ -688,8 +688,8 @@
etac ctxt eq_arg_cong_ctor_dtor])
fst_snd_convs];
val only_if_tac =
- EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
- rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+ EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+ rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least},
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]},
@@ -697,13 +697,13 @@
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
- dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
+ dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt @{thm imageE},
dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
- REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
- @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+ REPEAT_DETERM o eresolve_tac ctxt
+ @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
hyp_subst_tac ctxt,
dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, assume_tac ctxt])
(rev (active_set_map0s ~~ in_Irels))])
(ctor_sets ~~ passive_set_map0s),
rtac ctxt conjI,
@@ -713,8 +713,8 @@
EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
dtac ctxt set_rev_mp, assume_tac ctxt,
dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
- REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
- @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+ REPEAT_DETERM o eresolve_tac ctxt
+ @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
hyp_subst_tac ctxt,
dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex},
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])
--- a/src/HOL/Tools/BNF/bnf_lift.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Sun May 18 14:33:01 2025 +0000
@@ -623,14 +623,14 @@
fun rel_OO_Grp_tac ctxt =
HEADGOAL (EVERY' ([SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt ext))),
- SELECT_GOAL (unfold_thms_tac ctxt [@{thm OO_Grp_alt}, mem_Collect_eq,
- o_apply, @{thm vimage2p_def}, in_rel_of_bnf bnf_F, Bex_def, mem_Collect_eq]),
+ SELECT_GOAL (unfold_thms_tac ctxt (@{thms OO_Grp_alt mem_Collect_eq
+ o_apply vimage2p_def} @ in_rel_of_bnf bnf_F :: @{thms Bex_def mem_Collect_eq})),
rtac ctxt iffI,
SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))),
forward_tac ctxt
[zip_closed_thm OF (replicate 2 (Rep_thm RSN (2, @{thm ssubst_mem})))],
assume_tac ctxt,
- SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [bexE, conjE]))),
+ SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms bexE conjE}))),
etac ctxt Rep_cases_thm,
hyp_subst_tac ctxt,
SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt exI))),
@@ -813,11 +813,11 @@
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
REPEAT_DETERM o dtac ctxt (mk_sym set_F'_rsp),
SELECT_GOAL (unfold_thms_tac ctxt [#set_map_F' set_F'_thms]),
- rtac ctxt ballI, dtac ctxt @{thm equalityD1[THEN subsetD]}, assume_tac ctxt,
+ rtac ctxt @{thm ballI}, dtac ctxt @{thm equalityD1[THEN subsetD]}, assume_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt @{thms image_iff}),
- etac ctxt bexE, dtac ctxt set_mp, assume_tac ctxt,
+ etac ctxt @{thm bexE}, dtac ctxt set_mp, assume_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt @{thms mem_Collect_eq case_prod_beta}),
- rtac ctxt bexI, hyp_subst_tac ctxt, assume_tac ctxt, etac ctxt @{thm hypsubst},
+ rtac ctxt @{thm bexI}, hyp_subst_tac ctxt, assume_tac ctxt, etac ctxt @{thm hypsubst},
etac ctxt @{thm imageI}, assume_tac ctxt]
end;
in
@@ -1132,10 +1132,10 @@
replicate live @{thm Grp_conversep_nonempty} RS rev_mp),
rtac ctxt impI, dtac ctxt @{thm predicate2D}, etac ctxt @{thm relcomppI2[rotated]},
rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
- REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV],
+ REPEAT_DETERM o resolve_tac ctxt @{thms CollectI conjI subset_UNIV},
rtac ctxt (rel_flip RS iffD2),
rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
- REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV],
+ REPEAT_DETERM o resolve_tac ctxt @{thms CollectI conjI subset_UNIV},
SELECT_GOAL (unfold_thms_tac ctxt (rel_eq_onp :: @{thms Grp_conversep_eq_onp})),
etac ctxt @{thm predicate2D[OF rel_conj_eq_onp, rotated]},
rtac ctxt equiv_thm']);
@@ -1204,21 +1204,21 @@
fun F_in'_mono_tac ctxt =
unfold_thms_tac ctxt [#def F_in', #def F_in] THEN
HEADGOAL (EVERY'
- [rtac ctxt subsetI,
- etac ctxt vimageE,
+ [rtac ctxt @{thm subsetI},
+ etac ctxt @{thm vimageE},
etac ctxt @{thm ImageE},
- etac ctxt CollectE,
- etac ctxt CollectE,
+ etac ctxt @{thm CollectE},
+ etac ctxt @{thm CollectE},
dtac ctxt @{thm case_prodD},
hyp_subst_tac ctxt,
- rtac ctxt (vimageI OF [refl]),
+ rtac ctxt @{thm vimageI [OF refl]},
rtac ctxt @{thm ImageI},
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt @{thm case_prodI},
assume_tac ctxt ORELSE' rtac ctxt refl,
- rtac ctxt CollectI,
- etac ctxt subset_trans,
- etac ctxt (@{thm insert_mono} OF [@{thm image_mono}])]);
+ rtac ctxt @{thm CollectI},
+ etac ctxt @{thm subset_trans},
+ etac ctxt @{thm insert_mono [OF image_mono]}]);
val F_in'_mono_thm = prove lthy [var_A, var_A'] F_in'_mono_tm F_in'_mono_tac;
(* F_in'_Inter: F_in' (\<Inter>S) = (\<Inter>A\<in>S. F_in' A) *)
@@ -1234,13 +1234,13 @@
(unfold_thms_tac ctxt @{thms Inter_empty INT_empty UNIV_sum_unit_conv}),
rtac ctxt @{thm set_eqI},
rtac ctxt iffI,
- rtac ctxt UNIV_I,
- rtac ctxt (vimageI OF [refl]),
+ rtac ctxt @{thm UNIV_I},
+ rtac ctxt @{thm vimageI [OF refl]},
rtac ctxt @{thm ImageI},
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt @{thm case_prodI},
rtac ctxt (#reflp qthms),
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt subset_UNIV,
etac ctxt @{thm exE[OF ex_in_conv[THEN iffD2]]},
EqSubst.eqsubst_tac ctxt [0] @{thms image_INT[of _ UNIV _ id, simplified]},
@@ -1248,31 +1248,31 @@
assume_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt @{thms INT_extend_simps vimage_INT[symmetric]}),
rtac ctxt @{thm arg_cong2[where f=vimage, OF refl]},
- rtac ctxt equalityI,
- rtac ctxt subsetI,
+ rtac ctxt @{thm equalityI},
+ rtac ctxt @{thm subsetI},
rtac ctxt @{thm InterI},
- etac ctxt imageE,
+ etac ctxt @{thm imageE},
etac ctxt @{thm ImageE},
- etac ctxt CollectE,
- etac ctxt CollectE,
+ etac ctxt @{thm CollectE},
+ etac ctxt @{thm CollectE},
dtac ctxt @{thm case_prodD},
hyp_subst_tac ctxt,
rtac ctxt @{thm ImageI[OF CollectI]},
etac ctxt @{thm case_prodI} ORELSE' (SELECT_GOAL
(unfold_thms_tac ctxt @{thms prod.case}) THEN' rtac ctxt @{thm refl}),
- rtac ctxt CollectI,
- etac ctxt subset_trans,
+ rtac ctxt @{thm CollectI},
+ etac ctxt @{thm subset_trans},
etac ctxt @{thm INT_lower[OF imageI]},
rtac ctxt (@{thm subset_trans} OF [asm_rl, rel_Inter_thm]),
K (unfold_thms_tac ctxt @{thms image_image}),
- rtac ctxt subset_refl,
+ rtac ctxt @{thm subset_refl},
K (unfold_thms_tac ctxt @{thms INT_extend_simps ex_in_conv[symmetric]}),
rtac ctxt exI,
- rtac ctxt imageI,
+ rtac ctxt @{thm imageI},
assume_tac ctxt,
rtac ctxt exI,
rtac ctxt @{thm InterI},
- etac ctxt imageE,
+ etac ctxt @{thm imageE},
hyp_subst_tac ctxt,
rtac ctxt @{thm insertI1}]);
@@ -1298,22 +1298,22 @@
(* F_in'_alt2: F_in' A = {x. set_F' x \<subseteq> A} *)
val F_in'_alt2_tm = mk_Trueprop_eq
(#tm F_in' $ var_A, mk_in [var_A] [#tm set_F'] typ_aF);
- fun F_in'_alt2_tac ctxt = HEADGOAL (rtac ctxt equalityI THEN'
+ fun F_in'_alt2_tac ctxt = HEADGOAL (rtac ctxt @{thm equalityI} THEN'
(Subgoal.FOCUS o K) (unfold_thms_tac ctxt (map #def [set_F', F_in', F_in])) ctxt
THEN' EVERY'
- [rtac ctxt subsetI,
- rtac ctxt CollectI,
- rtac ctxt subsetI,
- dtac ctxt vimageD,
+ [rtac ctxt @{thm subsetI},
+ rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm subsetI},
+ dtac ctxt @{thm vimageD},
etac ctxt @{thm ImageE},
- etac ctxt CollectE,
- etac ctxt CollectE,
+ etac ctxt @{thm CollectE},
+ etac ctxt @{thm CollectE},
dtac ctxt @{thm case_prodD},
dtac ctxt @{thm InterD},
rtac ctxt @{thm imageI[OF CollectI]},
etac ctxt (#symp qthms),
etac ctxt @{thm UnionE},
- etac ctxt imageE,
+ etac ctxt @{thm imageE},
hyp_subst_tac ctxt,
etac ctxt @{thm subset_lift_sum_unitD},
etac ctxt @{thm setr.cases},
@@ -1321,28 +1321,28 @@
assume_tac ctxt])
THEN unfold_thms_tac ctxt [#def set_F'] THEN
(HEADGOAL o EVERY')
- [rtac ctxt subsetI,
- etac ctxt CollectE,
- etac ctxt (subsetD OF [F_in'_mono_thm]),
+ [rtac ctxt @{thm subsetI},
+ etac ctxt @{thm CollectE},
+ etac ctxt (@{thm subsetD} OF [F_in'_mono_thm]),
EqSubst.eqsubst_tac ctxt [0] [F_in'_Inter_thm],
rtac ctxt @{thm InterI}] THEN
REPEAT_DETERM (HEADGOAL (etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt)) THEN
(HEADGOAL o EVERY')
- [etac ctxt CollectE,
+ [etac ctxt @{thm CollectE},
SELECT_GOAL (unfold_thms_tac ctxt (map #def [F_in', F_in])),
rtac ctxt @{thm vimageI[OF refl]},
rtac ctxt @{thm ImageI},
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt @{thm case_prodI},
etac ctxt (#symp qthms),
- rtac ctxt CollectI,
- rtac ctxt subsetI,
+ rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm subsetI},
rtac ctxt @{thm sum_insert_Inl_unit},
assume_tac ctxt,
hyp_subst_tac ctxt,
- rtac ctxt imageI,
+ rtac ctxt @{thm imageI},
rtac ctxt @{thm UnionI},
- rtac ctxt imageI,
+ rtac ctxt @{thm imageI},
assume_tac ctxt,
rtac ctxt @{thm setr.intros[OF refl]}];
val F_in'_alt2_thm = prove lthy [var_A] F_in'_alt2_tm F_in'_alt2_tac;
@@ -1355,22 +1355,22 @@
[rtac ctxt @{thm set_eqI},
rtac ctxt iffI,
rtac ctxt @{thm InterI},
- etac ctxt CollectE,
- etac ctxt CollectE,
- dtac ctxt subsetD,
+ etac ctxt @{thm CollectE},
+ etac ctxt @{thm CollectE},
+ dtac ctxt @{thm subsetD},
assume_tac ctxt,
assume_tac ctxt,
etac ctxt @{thm InterD},
- rtac ctxt CollectI,
- rtac ctxt CollectI,
- rtac ctxt subset_refl]);
+ rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm subset_refl}]);
val set_F'_alt_thm = prove lthy [var_x] set_F'_alt_tm set_F'_alt_tac;
(* map_F_in_F_in'I: x \<in> F_in' B \<Longrightarrow> map_F f x \<in> F_in' (f ` B) *)
val map_F_in_F_in'I_tm = mk_Trueprop_implies ([HOLogic.mk_mem (var_x, #tm F_in' $ var_A')],
HOLogic.mk_mem (map_F_fs_x, subst_b (#tm F_in') $ (mk_image var_f $ var_A')));
fun map_F_in_F_in'I_tac ctxt =
- Local_Defs.unfold_tac ctxt ([#def F_in', #def F_in, Bex_def] @ @{thms vimage_def Image_iff}) THEN
+ Local_Defs.unfold_tac ctxt (#def F_in' :: #def F_in :: @{thms Bex_def vimage_def Image_iff}) THEN
HEADGOAL (EVERY'
[etac ctxt @{thm CollectE},
etac ctxt exE,
@@ -1386,7 +1386,7 @@
dtac ctxt (map_F_rsp_of (map mk_Maybe_map var_fs) ctxt),
SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms o_def map_sum.simps})),
assume_tac ctxt,
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
SELECT_GOAL (unfold_thms_tac ctxt set_map_thms),
etac ctxt @{thm image_map_sum_unit_subset}]);
val map_F_in_F_in'I_thm =
@@ -1422,7 +1422,7 @@
fun subset_UNIVs n = fold (fn a => fn b => conjI OF [a, b]) (replicate (n-1)
@{thm subset_UNIV}) @{thm subset_UNIV};
val GrpI_inst = infer_instantiate' ctxt (map SOME [Thm.cterm_of ctxt map_F_fs, x])
- @{thm GrpI} OF [refl, CollectI] OF [subset_UNIVs live];
+ @{thm GrpI} OF @{thms refl CollectI} OF [subset_UNIVs live];
in EVERY [
HEADGOAL (Method.insert_tac ctxt [rel_pos_distr_thm_inst]),
@@ -1437,7 +1437,7 @@
rtac ctxt @{thm relcomppI},
rtac ctxt rel_refl_strong]),
REPEAT_DETERM_N idx (HEADGOAL (rtac ctxt refl)),
- HEADGOAL (rtac ctxt conjI THEN' TWICE (etac ctxt subsetD THEN' assume_tac ctxt)),
+ HEADGOAL (rtac ctxt conjI THEN' TWICE (etac ctxt @{thm subsetD} THEN' assume_tac ctxt)),
REPEAT_DETERM_N (live-idx-1) (HEADGOAL (rtac ctxt refl)),
HEADGOAL (EVERY'
[rtac ctxt @{thm relcomppI},
@@ -1453,24 +1453,24 @@
etac ctxt @{thm GrpE},
hyp_subst_tac ctxt,
rtac ctxt @{thm ImageI},
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt @{thm case_prodI},
assume_tac ctxt,
EqSubst.eqsubst_asm_tac ctxt [1] rel_map,
EqSubst.eqsubst_asm_tac ctxt [1] [in_rel_of_bnf bnf_F],
etac ctxt exE,
- etac ctxt CollectE,
+ etac ctxt @{thm CollectE},
etac ctxt conjE,
etac ctxt conjE,
- etac ctxt CollectE,
+ etac ctxt @{thm CollectE},
hyp_subst_tac ctxt,
- rtac ctxt CollectI]),
+ rtac ctxt @{thm CollectI}]),
unfold_thms_tac ctxt set_map_thms,
- HEADGOAL (rtac ctxt (subsetI OF [vimageI] OF [refl]) THEN'
+ HEADGOAL (rtac ctxt (@{thm subsetI} OF @{thms vimageI} OF [refl]) THEN'
etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt),
REPEAT_DETERM_N 6 (HEADGOAL (etac ctxt Drule.thin_rl)),
REPEAT_DETERM_N (live-1) (HEADGOAL (etac ctxt conjE)),
- HEADGOAL (EVERY' [dtac ctxt subsetD, assume_tac ctxt, etac ctxt CollectE]),
+ HEADGOAL (EVERY' [dtac ctxt @{thm subsetD}, assume_tac ctxt, etac ctxt @{thm CollectE}]),
unfold_thms_tac ctxt @{thms split_beta},
HEADGOAL (etac ctxt conjunct2)] end;
@@ -1478,20 +1478,20 @@
[rtac ctxt @{thm set_eqI},
rtac ctxt iffI,
etac ctxt @{thm ImageE},
- etac ctxt CollectE,
- etac ctxt CollectE,
+ etac ctxt @{thm CollectE},
+ etac ctxt @{thm CollectE},
dtac ctxt @{thm case_prodD},
- rtac ctxt (vimageI OF [refl]),
+ rtac ctxt @{thm vimageI [OF refl]},
rtac ctxt @{thm ImageI},
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt @{thm case_prodI},
etac ctxt map_F_rsp,
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
EqSubst.eqsubst_tac ctxt [0] [set_map_F_thm],
etac ctxt @{thm subset_vimage_image_subset},
- etac ctxt vimageE,
+ etac ctxt @{thm vimageE},
etac ctxt @{thm ImageE},
- TWICE (etac ctxt CollectE),
+ TWICE (etac ctxt @{thm CollectE}),
dtac ctxt @{thm case_prodD},
hyp_subst_tac ctxt,
Subgoal.FOCUS_PARAMS subgoal_tac ctxt]);
@@ -1506,18 +1506,18 @@
rtac ctxt iffI,
EqSubst.eqsubst_asm_tac ctxt [0] [set_F'_alt_thm],
etac ctxt @{thm InterD},
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt map_F_in_F_in'I_thm,
SELECT_GOAL (unfold_thms_tac ctxt [F_in'_alt2_thm]),
- rtac ctxt CollectI,
- rtac ctxt subset_refl,
+ rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm subset_refl},
SELECT_GOAL (unfold_thms_tac ctxt [set_F'_alt_thm]),
rtac ctxt @{thm InterI},
- etac ctxt imageE,
- etac ctxt CollectE,
+ etac ctxt @{thm imageE},
+ etac ctxt @{thm CollectE},
hyp_subst_tac ctxt,
etac ctxt @{thm vimageD[OF InterD]},
- rtac ctxt CollectI]) THEN
+ rtac ctxt @{thm CollectI}]) THEN
(* map_F f x \<in> F_in' X \<Longrightarrow> x \<in> F_in' (f -` X) *)
HEADGOAL (Subgoal.FOCUS_PARAMS (fn {context = ctxt, params, ...} =>
let
@@ -1534,7 +1534,7 @@
@{thms lift_sum_unit_vimage_commute vimage_comp o_def map_sum.simps}),
unfold_thms_tac ctxt [@{thm o_def[symmetric]}, map_F_comp0],
Local_Defs.fold_tac ctxt @{thms vimage_comp},
- HEADGOAL (etac ctxt (vimageI OF [refl]))] end) ctxt);
+ HEADGOAL (etac ctxt @{thm vimageI [OF refl]})] end) ctxt);
(* set_F'_subset: set_F' x \<subseteq> set_F x *)
val set_F'_subset_tm = HOLogic.mk_Trueprop (mk_leq (#tm set_F' $ var_x) (set_F $ var_x));
@@ -1542,17 +1542,17 @@
let val int_e_thm = infer_instantiate' ctxt
(replicate 3 NONE @ [SOME (Thm.cterm_of ctxt (map_F_Just $ var_x))]) @{thm INT_E};
in HEADGOAL (EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [#def set_F']),
- rtac ctxt subsetI,
+ rtac ctxt @{thm subsetI},
etac ctxt int_e_thm,
SELECT_GOAL (unfold_thms_tac ctxt [set_map_F_thm]),
etac ctxt @{thm UN_E},
- etac ctxt imageE,
+ etac ctxt @{thm imageE},
hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt @{thms sum_set_simps singleton_iff}),
hyp_subst_tac ctxt,
assume_tac ctxt,
etac ctxt notE,
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
rtac ctxt (#reflp qthms)])
end;
in
@@ -1594,9 +1594,9 @@
(unfold_thms_tac ctxt
(maps (fn {F_in'_def, F_in_def, ...} => [F_in'_def, F_in_def]) set_F'_thmss) ::
map (REPEAT_DETERM_N live o HEADGOAL)
- [etac ctxt vimageE,
+ [etac ctxt @{thm vimageE},
etac ctxt @{thm ImageE},
- etac ctxt CollectE THEN' etac ctxt CollectE,
+ etac ctxt @{thm CollectE} THEN' etac ctxt @{thm CollectE},
dtac ctxt @{thm case_prodD}] @
HEADGOAL (hyp_subst_tac ctxt THEN' rotate_tac (~live)) ::
map (fn i => (HEADGOAL o EVERY')
@@ -1610,7 +1610,7 @@
SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms case_sum_o_inj(2)})),
EqSubst.eqsubst_tac ctxt [0] [map_F_cong OF replicate i refl @ asm_rl :: replicate (live-i) refl],
rtac ctxt @{thm sum.case_cong[OF refl refl]},
- etac ctxt bspec,
+ etac ctxt @{thm bspec},
hyp_subst_tac ctxt,
etac ctxt @{thm subset_lift_sum_unitD},
assume_tac ctxt,
@@ -1641,9 +1641,9 @@
EVERY (map (fn {F_in'_alt2, ...} =>
unfold_thms_tac ctxt [F_in'_alt2] THEN
HEADGOAL (EVERY'
- [rtac ctxt CollectI,
- rtac ctxt subset_refl,
- rtac ctxt ballI,
+ [rtac ctxt @{thm CollectI},
+ rtac ctxt @{thm subset_refl},
+ rtac ctxt @{thm ballI},
SELECT_GOAL (unfold_thms_tac ctxt [o_apply]),
rtac ctxt @{thm arg_cong[where f=Inr]},
asm_full_simp_tac ctxt])) set_F'_thmss) end;
@@ -1750,7 +1750,7 @@
[dtac ctxt (in_rel RS iffD1),
etac ctxt exE,
TWICE (etac ctxt conjE),
- etac ctxt CollectE,
+ etac ctxt @{thm CollectE},
hyp_subst_tac ctxt]),
(REPEAT_DETERM_N (live-1) o HEADGOAL) (etac ctxt conjE),
HEADGOAL (Subgoal.FOCUS_PARAMS subgoal1_tac ctxt THEN' etac ctxt exE),
@@ -1834,7 +1834,7 @@
REPEAT_FIRST (resolve_tac ctxt [conjI]),
HEADGOAL (EVERY' (maps (fn {set_F'_respect, ...} =>
[etac ctxt @{thm subset_trans[rotated]},
- rtac ctxt equalityD1,
+ rtac ctxt @{thm equalityD1},
rtac ctxt (@{thm rel_funD} OF [set_F'_respect]),
rtac ctxt (#rep_abs qthms),
rtac ctxt (#reflp qthms)]) set_F'_thmss)),
@@ -1927,9 +1927,9 @@
HEADGOAL (rtac ctxt exI),
HEADGOAL (EVERY' (maps (fn thms =>
[rtac ctxt conjI,
- rtac ctxt subsetI,
+ rtac ctxt @{thm subsetI},
dtac ctxt (set_mp OF [#set_F'_subset thms]),
- dtac ctxt subsetD,
+ dtac ctxt @{thm subsetD},
assume_tac ctxt, assume_tac ctxt]) set_F'_thmss)),
(REPEAT_DETERM o HEADGOAL)
(rtac ctxt conjI ORELSE' hyp_subst_tac ctxt THEN' rtac ctxt (#reflp qthms))]
@@ -2059,7 +2059,7 @@
prepare_solve (K I) (K I) (K I) (K I) (K tacs) args;
fun copy_bnf_tac {context = ctxt, prems = _} =
- REPEAT_DETERM (resolve_tac ctxt [bexI, conjI, UNIV_I, refl, subset_refl] 1);
+ REPEAT_DETERM (resolve_tac ctxt @{thms bexI conjI UNIV_I refl subset_refl} 1);
val copy_bnf =
apfst (apfst (rpair NONE))
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun May 18 14:33:01 2025 +0000
@@ -569,7 +569,7 @@
fun non_empty_typedef_tac non_empty_pred ctxt i =
(Method.insert_tac ctxt [non_empty_pred] THEN'
- SELECT_GOAL (Local_Defs.unfold0_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
+ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms mem_Collect_eq}) THEN' assume_tac ctxt) i
val uTname = unique_Tname (rty, qty)
val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
val ((_, tcode_dt), lthy2) = lthy1
--- a/src/HOL/Tools/Qelim/cooper.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun May 18 14:33:01 2025 +0000
@@ -105,14 +105,11 @@
val unity_coeff_ex = Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [] @{thm "unity_coeff_ex"};
-val [zdvd_mono,simp_from_to,all_not_ex] =
- [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
-
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
val eval_ss =
simpset_of (put_simpset presburger_ss \<^context>
- addsimps [simp_from_to] delsimps [insert_iff, bex_triv]);
+ addsimps @{thms simp_from_to} delsimps @{thms insert_iff bex_triv});
fun eval_conv ctxt = Simplifier.rewrite (put_simpset eval_ss ctxt);
(* recognising cterm without moving to terms *)
@@ -408,7 +405,7 @@
val k = l div dest_number c
val kt = HOLogic.mk_number iT k
val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
- ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
+ ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS @{thm zdvd_mono})
val (d',t') = (mulC$kt$d, mulC$kt$r)
val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
RS eq_reflection
@@ -571,7 +568,7 @@
val conv_ss =
simpset_of (put_simpset HOL_basic_ss \<^context>
addsimps (@{thms simp_thms} @ take 4 @{thms ex_simps} @
- [not_all, all_not_ex, @{thm ex_disj_distrib}]));
+ [not_all, @{thm all_not_ex}, @{thm ex_disj_distrib}]));
fun conv ctxt p =
Qelim.gen_qelim_conv ctxt
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sun May 18 14:33:01 2025 +0000
@@ -153,10 +153,10 @@
in
EVERY' [rtac ctxt ext, SELECT_GOAL (Local_Defs.unfold0_tac ctxt [@{thm Domainp.simps},
in_rel_of_bnf bnf, pred_def]), rtac ctxt iffI,
- REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
- CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt ballI, dtac ctxt (set_map RS equalityD1 RS set_mp),
- etac ctxt imageE, dtac ctxt set_rev_mp, assume_tac ctxt,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm case_prodE}],
+ REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt,
+ CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt @{thm ballI}, dtac ctxt (set_map RS @{thm equalityD1} RS set_mp),
+ etac ctxt @{thm imageE}, dtac ctxt set_rev_mp, assume_tac ctxt,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE case_prodE},
hyp_subst_tac ctxt, rtac ctxt @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
etac ctxt @{thm DomainPI}]) set_map's,
REPEAT_DETERM o etac ctxt conjE,
@@ -164,10 +164,10 @@
rtac ctxt refl, rtac ctxt (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
map_id_of_bnf bnf]),
REPEAT_DETERM_N n o (EVERY' [rtac ctxt @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
- rtac ctxt @{thm fst_conv}]), rtac ctxt CollectI,
+ rtac ctxt @{thm fst_conv}]), rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt (set_map RS @{thm ord_eq_le_trans}),
- REPEAT_DETERM o resolve_tac ctxt [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
- dtac ctxt (rotate_prems 1 bspec), assume_tac ctxt,
+ REPEAT_DETERM o resolve_tac ctxt @{thms image_subsetI CollectI case_prodI},
+ dtac ctxt (rotate_prems 1 @{thm bspec}), assume_tac ctxt,
etac ctxt @{thm DomainpE}, etac ctxt @{thm someI}]) set_map's
]
end
--- a/src/HOL/Tools/record.ML Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/record.ML Sun May 18 14:33:01 2025 +0000
@@ -86,7 +86,7 @@
(({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
let
val exists_thm =
- UNIV_I
+ @{thm UNIV_I}
|> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
val proj_constr = Abs_inverse OF [exists_thm];
val absT = Type (tyco, map TFree vs);
@@ -103,7 +103,7 @@
thy
|> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
(Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn)
- (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1))
+ (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' @{thms UNIV_witness} 1))
|-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Sun May 18 14:33:01 2025 +0000
@@ -306,9 +306,9 @@
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
fun list_of_Int th =
(list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
- handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+ handle THM _ => (list_of_Int (th RS @{thm IntD1}) @ list_of_Int (th RS @{thm IntD2}))
handle THM _ => (list_of_Int (th RS @{thm INT_D}))
- handle THM _ => (list_of_Int (th RS bspec))
+ handle THM _ => (list_of_Int (th RS @{thm bspec}))
handle THM _ => [th];
\<close>
@@ -319,7 +319,7 @@
fun normalized th =
normalized (th RS spec
handle THM _ => th RS @{thm lessThanBspec}
- handle THM _ => th RS bspec
+ handle THM _ => th RS @{thm bspec}
handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
handle THM _ => th;
in