# HG changeset patch
# User wenzelm
# Date 1630868971 -7200
# Node ID 914a214e110e8a0b22418d7b1748b35361c715af
# Parent  a810e8f2f2e92157a0de994da01a0d9e0cba00a8
more scalable operations;

diff -r a810e8f2f2e9 -r 914a214e110e src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -24,8 +24,7 @@
 fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
 fun REPEAT' tac i = REPEAT (tac i)
 
-fun frees ct = Drule.cterm_add_frees ct []
-fun free_in v ct = member (op aconvc) (frees ct) v
+fun free_in v ct = member (op aconvc) (Drule.cterm_frees_of ct) v
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =
diff -r a810e8f2f2e9 -r 914a214e110e src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Sep 05 21:09:31 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 qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm [])
+   val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_frees_of tm)
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
                                                whatis = whatis, simpset = ss}) vs
diff -r a810e8f2f2e9 -r 914a214e110e src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -188,7 +188,7 @@
   in
     fn p =>
       Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
-        (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+        (Drule.cterm_frees_of p) (K Thm.reflexive) (K Thm.reflexive)
         (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
   end;
 
diff -r a810e8f2f2e9 -r 914a214e110e src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -868,9 +868,11 @@
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
         else raise Failure "substitutable_monomial"
     | \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
-         (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
+         (substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg tm)))
+           (Thm.dest_arg1 tm)
            handle Failure _ =>
-            substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
+            substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg1 tm)))
+              (Thm.dest_arg tm))
     | _ => raise Failure "substitutable_monomial")
 
   fun isolate_variable v th =
diff -r a810e8f2f2e9 -r 914a214e110e src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -66,7 +66,7 @@
 
 fun standard_qelim_conv ctxt atcv ncv qcv p =
   let val pcv = pcv ctxt
-  in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
+  in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_frees_of p) atcv ncv qcv p end
 
 end;
 
diff -r a810e8f2f2e9 -r 914a214e110e src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/HOL/Tools/groebner.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -528,8 +528,7 @@
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun frees t = Drule.cterm_add_frees t [];
-fun free_in v t = member op aconvc (frees t) v;
+fun free_in v t = member op aconvc (Drule.cterm_frees_of t) v;
 
 val vsubst = let
  fun vsubst (t,v) tm =
@@ -737,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 = Drule.cterm_add_frees tm []
+  val avs = Drule.cterm_frees_of tm
   val P' = fold mk_forall avs tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
@@ -796,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(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons
+          orelse not(member (op aconvc) (Drule.cterm_frees_of m) v)) mons
   end
 
   fun isolate_variable vars tm =
@@ -851,7 +850,7 @@
  fun isolate_monomials vars tm =
  let
   val (cmons,vmons) =
-    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
+    List.partition (fn m => null (inter (op aconvc) vars (Drule.cterm_frees_of m)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm
diff -r a810e8f2f2e9 -r 914a214e110e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/Pure/drule.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -89,7 +89,7 @@
   val mk_term: cterm -> thm
   val dest_term: thm -> cterm
   val cterm_rule: (thm -> thm) -> cterm -> cterm
-  val cterm_add_frees: cterm -> cterm list -> cterm list
+  val cterm_frees_of: cterm -> cterm list
   val dummy_thm: thm
   val free_dummy_thm: thm
   val is_sort_constraint: term -> bool
@@ -615,7 +615,7 @@
   end;
 
 fun cterm_rule f = dest_term o f o mk_term;
-val cterm_add_frees = Thm.add_frees o mk_term;
+val cterm_frees_of = Thm.frees_of o mk_term;
 
 val dummy_thm = mk_term (certify Term.dummy_prop);
 val free_dummy_thm = Thm.tag_free_dummy dummy_thm;
diff -r a810e8f2f2e9 -r 914a214e110e src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/Pure/more_thm.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -28,6 +28,7 @@
   val add_tvars: thm -> ctyp list -> ctyp list
   val add_frees: thm -> cterm list -> cterm list
   val add_vars: thm -> cterm list -> cterm list
+  val frees_of: thm -> cterm list
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -141,6 +142,17 @@
 val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
 val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
 
+fun frees_of th =
+  (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms
+    (fn a => fn (set, list) =>
+      (case Thm.term_of a of
+        Free v =>
+          if not (Term_Subst.Frees.defined set v)
+          then (Term_Subst.Frees.add (v, ()) set, a :: list)
+          else (set, list)
+      | _ => (set, list)))
+  |> #2;
+
 
 (* ctyp operations *)