clarified signature;
authorwenzelm
Thu, 09 Sep 2021 17:20:41 +0200
changeset 74621 36f2c4a5c21b
parent 74620 0a4cdf0036a0
child 74622 0336d6eef172
child 74624 aed955bb4cb1
clarified signature;
src/HOL/Analysis/metric_arith.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/groebner.ML
src/Pure/drule.ML
src/Tools/misc_legacy.ML
--- a/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -24,7 +24,7 @@
 fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
 fun REPEAT' tac i = REPEAT (tac i)
 
-fun free_in v ct = Cterms.defined (Misc_Legacy.cterm_frees ct) v
+fun free_in v ct = Cterms.defined (Cterms.build (Drule.add_frees_cterm ct)) v
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -206,7 +206,7 @@
    val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
    val postcv = Simplifier.rewrite (put_simpset ss ctxt);
    val nnf = K (nnf_conv ctxt then_conv postcv)
-   val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees tm)
+   val env = Cterms.list_set_rev (Cterms.build (Drule.add_frees_cterm tm))
    val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons env
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
--- a/src/HOL/Decision_Procs/langford.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -185,7 +185,7 @@
       Simplifier.rewrite
         (put_simpset dlo_ss ctxt
           addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
-    val mk_env = Cterms.list_set_rev o Misc_Legacy.cterm_frees
+    val mk_env = Cterms.list_set_rev o Cterms.build o Drule.add_frees_cterm
   in
     fn p =>
       Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -868,10 +868,10 @@
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
         else raise Failure "substitutable_monomial"
     | \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
-         (substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg tm)))
+         (substitutable_monomial (Drule.add_frees_cterm (Thm.dest_arg tm) fvs)
            (Thm.dest_arg1 tm)
            handle Failure _ =>
-            substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg1 tm)))
+            substitutable_monomial (Drule.add_frees_cterm (Thm.dest_arg1 tm) fvs)
               (Thm.dest_arg tm))
     | _ => raise Failure "substitutable_monomial")
 
--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -67,7 +67,7 @@
 fun standard_qelim_conv ctxt atcv ncv qcv p =
   let
     val pcv = pcv ctxt
-    val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees p)
+    val env = Cterms.list_set_rev (Cterms.build (Drule.add_frees_cterm p))
   in gen_qelim_conv ctxt pcv pcv pcv cons env atcv ncv qcv p end
 
 end;
--- a/src/HOL/Tools/groebner.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -528,7 +528,7 @@
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun free_in v t = Cterms.defined (Misc_Legacy.cterm_frees t) v;
+fun free_in v t = Cterms.defined (Cterms.build (Drule.add_frees_cterm t)) v;
 
 val vsubst = let
  fun vsubst (t,v) tm =
@@ -736,7 +736,7 @@
       val T = Thm.typ_of_cterm x;
       val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
     in Thm.apply all (Thm.lambda x p) end
-  val avs = Misc_Legacy.cterm_frees tm
+  val avs = Cterms.build (Drule.add_frees_cterm tm)
   val P' = fold mk_forall (Cterms.list_set_rev avs) tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
@@ -795,7 +795,7 @@
    val mons = striplist(dest_binary ring_add_tm) t
   in member (op aconvc) mons v andalso
     forall (fn m => v aconvc m
-          orelse not(Cterms.defined (Misc_Legacy.cterm_frees m) v)) mons
+          orelse not(Cterms.defined (Cterms.build (Drule.add_frees_cterm m)) v)) mons
   end
 
   fun isolate_variable vars tm =
@@ -849,9 +849,10 @@
 
  fun isolate_monomials vars tm =
  let
-  val (cmons,vmons) =
-    List.partition (fn m => null (inter (op aconvc) vars (Cterms.list_set_rev (Misc_Legacy.cterm_frees m))))
-                   (striplist ring_dest_add tm)
+  val (vmons, cmons) =
+    List.partition (fn m =>
+      let val frees = Cterms.build (Drule.add_frees_cterm m)
+      in exists (Cterms.defined frees) vars end) (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm
              else Thm.apply ring_neg_tm
--- a/src/Pure/drule.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/Pure/drule.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -88,6 +88,8 @@
   val mk_term: cterm -> thm
   val dest_term: thm -> cterm
   val cterm_rule: (thm -> thm) -> cterm -> cterm
+  val add_frees_cterm: cterm -> Cterms.set -> Cterms.set
+  val add_vars_cterm: cterm -> Cterms.set -> Cterms.set
   val dummy_thm: thm
   val free_dummy_thm: thm
   val is_sort_constraint: term -> bool
@@ -611,6 +613,9 @@
 
 fun cterm_rule f = dest_term o f o mk_term;
 
+val add_frees_cterm = Cterms.add_frees o mk_term;
+val add_vars_cterm = Cterms.add_vars o mk_term;
+
 val dummy_thm = mk_term (certify Term.dummy_prop);
 val free_dummy_thm = Thm.tag_free_dummy dummy_thm;
 
--- a/src/Tools/misc_legacy.ML	Thu Sep 09 16:53:40 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Thu Sep 09 17:20:41 2021 +0200
@@ -5,7 +5,6 @@
 
 signature MISC_LEGACY =
 sig
-  val cterm_frees: cterm -> Cterms.set
   val add_term_names: term * string list -> string list
   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
@@ -25,8 +24,6 @@
 structure Misc_Legacy: MISC_LEGACY =
 struct
 
-val cterm_frees = Cterms.build o Cterms.add_frees o Drule.mk_term;
-
 (*iterate a function over all types in a term*)
 fun it_term_types f =
 let fun iter(Const(_,T), a) = f(T,a)