# HG changeset patch # User wenzelm # Date 1631200841 -7200 # Node ID 36f2c4a5c21b52ea2114d93b9ce18c373627ffd5 # Parent 0a4cdf0036a08933ed4fa81139b700ec9e5cf267 clarified signature; diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/HOL/Analysis/metric_arith.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 = diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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, diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/HOL/Decision_Procs/langford.ML --- 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 diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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>\(+) :: real \ _\$_$_ => - (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") diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/HOL/Tools/Qelim/qelim.ML --- 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; diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/HOL/Tools/groebner.ML --- 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>\All\, (T --> \<^typ>\bool\) --> \<^typ>\bool\)) 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 diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/Pure/drule.ML --- 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; diff -r 0a4cdf0036a0 -r 36f2c4a5c21b src/Tools/misc_legacy.ML --- 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)