# HG changeset patch # User wenzelm # Date 1630923786 -7200 # Node ID 282cd3aa6cc6c16aca1e18e44671bdda83e2d8bb # Parent 12dac3698efdbc5b0f01f1f694dd2b81a91402c2 clarified modules; diff -r 12dac3698efd -r 282cd3aa6cc6 src/Doc/Typeclass_Hierarchy/Setup.thy --- 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 \../more_antiquote.ML\ attribute_setup all = - \Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\ + \Scan.succeed (Thm.rule_attribute [] (K Thm.forall_intr_vars))\ "quantified schematic vars" setup \Config.put_global Printer.show_type_emphasis false\ diff -r 12dac3698efd -r 282cd3aa6cc6 src/HOL/Tools/Argo/argo_tactic.ML --- 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) diff -r 12dac3698efd -r 282cd3aa6cc6 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; diff -r 12dac3698efd -r 282cd3aa6cc6 src/HOL/Tools/Function/function_core.ML --- 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' diff -r 12dac3698efd -r 282cd3aa6cc6 src/HOL/Tools/Meson/meson_clausify.ML --- 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 diff -r 12dac3698efd -r 282cd3aa6cc6 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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'] diff -r 12dac3698efd -r 282cd3aa6cc6 src/HOL/Tools/SMT/smt_normalize.ML --- 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]} diff -r 12dac3698efd -r 282cd3aa6cc6 src/HOL/Tools/Transfer/transfer.ML --- 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)))) diff -r 12dac3698efd -r 282cd3aa6cc6 src/Pure/Isar/method.ML --- 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) => diff -r 12dac3698efd -r 282cd3aa6cc6 src/Pure/Proof/proof_checker.ML --- 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, ...}, _)) = diff -r 12dac3698efd -r 282cd3aa6cc6 src/Pure/drule.ML --- 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; diff -r 12dac3698efd -r 282cd3aa6cc6 src/Pure/more_thm.ML --- 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