--- a/src/Doc/Typeclass_Hierarchy/Setup.thy Mon Sep 06 12:11:17 2021 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy Mon Sep 06 12:23:06 2021 +0200
@@ -6,7 +6,7 @@
ML_file \<open>../more_antiquote.ML\<close>
attribute_setup all =
- \<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (K Thm.forall_intr_vars))\<close>
"quantified schematic vars"
setup \<open>Config.put_global Printer.show_type_emphasis false\<close>
--- a/src/HOL/Tools/Argo/argo_tactic.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Mon Sep 06 12:23:06 2021 +0200
@@ -692,7 +692,7 @@
thm
|> instantiate_elim_rule
|> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
- |> Drule.forall_intr_vars
+ |> Thm.forall_intr_vars
|> Conv.fconv_rule (atomize_conv ctxt)
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Sep 06 12:23:06 2021 +0200
@@ -830,7 +830,7 @@
(Variable.gen_all lthy
(Drule.rename_bvars'
(map (SOME o fst) xs')
- (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
+ (Thm.forall_intr_vars (case_thm RS (sel_def RS trans)))));
val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss;
--- a/src/HOL/Tools/Function/function_core.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Mon Sep 06 12:23:06 2021 +0200
@@ -466,7 +466,7 @@
forall_intr_rename (n, Thm.cterm_of lthy (Var (varmap (n, T), T)))) qs thm
end
in
- ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
+ ((Rdef, map2 requantify intrs intrs_gen, Thm.forall_intr_vars elim_gen, induct), lthy)
end
fun define_graph (G_binding, G_type) fvar clauses RCss lthy =
@@ -809,7 +809,7 @@
|> Thm.forall_intr (Thm.cterm_of ctxt' x)
|> (fn it => Drule.compose (it, 2, wf_induct_rule))
|> curry op RS (Thm.assume wfR')
- |> forall_intr_vars
+ |> Thm.forall_intr_vars
|> (fn it => it COMP allI)
|> fold Thm.implies_intr hyps
|> Thm.implies_intr wfR'
--- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Sep 06 12:23:06 2021 +0200
@@ -300,7 +300,7 @@
val th =
th |> transform_elim_theorem
|> zero_var_indexes
- |> new_skolem ? forall_intr_vars
+ |> new_skolem ? Thm.forall_intr_vars
val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
|> Meson.cong_extensionalize_thm ctxt
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Sep 06 12:23:06 2021 +0200
@@ -42,7 +42,7 @@
fun atomize_thm ctxt thm =
let
- val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
+ val thm' = Thm.legacy_freezeT (Thm.forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Sep 06 12:23:06 2021 +0200
@@ -255,7 +255,7 @@
instantiate_elim #>
norm_def #>
Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
- Drule.forall_intr_vars #>
+ Thm.forall_intr_vars #>
Conv.fconv_rule (gen_normalize1_conv ctxt) #>
(* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
--- a/src/HOL/Tools/Transfer/transfer.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Mon Sep 06 12:23:06 2021 +0200
@@ -696,7 +696,7 @@
val rules = extra_rules @ get_transfer_raw ctxt
val eq_rules = get_relator_eq_raw ctxt
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
- val thm1 = Drule.forall_intr_vars thm
+ val thm1 = Thm.forall_intr_vars thm
val instT =
rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
@@ -731,7 +731,7 @@
val rules = extra_rules @ get_transfer_raw ctxt
val eq_rules = get_relator_eq_raw ctxt
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
- val thm1 = Drule.forall_intr_vars thm
+ val thm1 = Thm.forall_intr_vars thm
val instT =
rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
--- a/src/Pure/Isar/method.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/Pure/Isar/method.ML Mon Sep 06 12:23:06 2021 +0200
@@ -118,7 +118,7 @@
fun insert_tac _ [] _ = all_tac
| insert_tac ctxt facts i =
- EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
+ EVERY (map (fn r => resolve_tac ctxt [Thm.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
fun insert thms =
CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
--- a/src/Pure/Proof/proof_checker.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML Mon Sep 06 12:23:06 2021 +0200
@@ -81,7 +81,7 @@
val ctye =
(tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
in
- Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
+ Thm.instantiate (ctye, []) (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
end;
fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
--- a/src/Pure/drule.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/Pure/drule.ML Mon Sep 06 12:23:06 2021 +0200
@@ -14,7 +14,6 @@
val strip_imp_concl: cterm -> cterm
val cprems_of: thm -> cterm list
val forall_intr_list: cterm list -> thm -> thm
- val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
val lift_all: Proof.context -> cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
@@ -164,11 +163,6 @@
(*Generalization over a list of variables*)
val forall_intr_list = fold_rev Thm.forall_intr;
-(*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th =
- let val vs = build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Var (insert (op aconvc)))
- in fold Thm.forall_intr vs th end;
-
fun outer_params t =
let val vs = Term.strip_all_vars t
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
--- a/src/Pure/more_thm.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/Pure/more_thm.ML Mon Sep 06 12:23:06 2021 +0200
@@ -76,6 +76,7 @@
val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
val forall_intr_frees: thm -> thm
+ val forall_intr_vars: thm -> thm
val unvarify_global: theory -> thm -> thm
val unvarify_axiom: theory -> string -> thm
val rename_params_rule: string list * int -> thm -> thm
@@ -459,7 +460,11 @@
in Thm.instantiate ([], inst) thm' end;
-(* forall_intr_frees: generalization over all suitable Free variables *)
+(* implicit generalization over variables -- canonical order *)
+
+fun forall_intr_vars th =
+ let val vs = build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Var (insert (op aconvc)))
+ in fold Thm.forall_intr vs th end;
fun forall_intr_frees th =
let