# HG changeset patch # User wenzelm # Date 1631191826 -7200 # Node ID f084d599bb448f3d24360e030494c1cedf9dd9e6 # Parent d01920a8b082066ab2bd8b3617ff2767bf8b339b clarified set of items with order of addition; diff -r d01920a8b082 -r f084d599bb44 src/HOL/Analysis/metric_arith.ML --- a/src/HOL/Analysis/metric_arith.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/HOL/Analysis/metric_arith.ML Thu Sep 09 14:50:26 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 = member (op aconvc) (Misc_Legacy.cterm_frees ct) v +fun free_in v ct = Cterms.defined (Misc_Legacy.cterm_frees ct) v (* build a cterm set with elements cts of type ty *) fun mk_ct_set ctxt ty = diff -r d01920a8b082 -r f084d599bb44 src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Sep 09 14:50:26 2021 +0200 @@ -206,7 +206,8 @@ 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 (Misc_Legacy.cterm_frees tm) + val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees 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, whatis = whatis, simpset = ss}) vs diff -r d01920a8b082 -r f084d599bb44 src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/HOL/Decision_Procs/langford.ML Thu Sep 09 14:50:26 2021 +0200 @@ -185,10 +185,11 @@ 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 in fn p => Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons - (Misc_Legacy.cterm_frees p) (K Thm.reflexive) (K Thm.reflexive) + (mk_env p) (K Thm.reflexive) (K Thm.reflexive) (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p end; diff -r d01920a8b082 -r f084d599bb44 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Sep 09 14:50:26 2021 +0200 @@ -860,18 +860,18 @@ fun substitutable_monomial fvs tm = (case Thm.term_of tm of Free (_, \<^typ>\real\) => - if not (member (op aconvc) fvs tm) then (@1, tm) + if not (Cterms.defined fvs tm) then (@1, tm) else raise Failure "substitutable_monomial" | \<^term>\(*) :: real \ _\ $ _ $ (Free _) => if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso - not (member (op aconvc) fvs (Thm.dest_arg tm)) + not (Cterms.defined fvs (Thm.dest_arg tm)) then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm) else raise Failure "substitutable_monomial" | \<^term>\(+) :: real \ _\$_$_ => - (substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm))) + (substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg tm))) (Thm.dest_arg1 tm) handle Failure _ => - substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm))) + substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg1 tm))) (Thm.dest_arg tm)) | _ => raise Failure "substitutable_monomial") @@ -898,7 +898,7 @@ fun make_substitution th = let - val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th)) + val (c,v) = substitutable_monomial Cterms.empty (Thm.dest_arg1(concl th)) val th1 = Drule.arg_cong_rule (Thm.apply \<^cterm>\(*) :: real \ _\ (RealArith.cterm_of_rat (Rat.inv c))) diff -r d01920a8b082 -r f084d599bb44 src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Thu Sep 09 14:50:26 2021 +0200 @@ -65,8 +65,10 @@ in fun standard_qelim_conv ctxt atcv ncv qcv p = - let val pcv = pcv ctxt - in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end + let + val pcv = pcv ctxt + val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees p) + in gen_qelim_conv ctxt pcv pcv pcv cons env atcv ncv qcv p end end; diff -r d01920a8b082 -r f084d599bb44 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/HOL/Tools/groebner.ML Thu Sep 09 14:50:26 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 = member op aconvc (Misc_Legacy.cterm_frees t) v; +fun free_in v t = Cterms.defined (Misc_Legacy.cterm_frees t) v; val vsubst = let fun vsubst (t,v) tm = @@ -737,7 +737,7 @@ 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 P' = fold mk_forall avs 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 if is_forall bod then raise CTERM("ring: non-universal formula",[tm]) @@ -752,7 +752,7 @@ Thm.equal_elim (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym]) (th2 |> Thm.cprop_of)) th2 - in specl avs + in specl (Cterms.list_set_rev avs) ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD) end end @@ -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(member (op aconvc) (Misc_Legacy.cterm_frees m) v)) mons + orelse not(Cterms.defined (Misc_Legacy.cterm_frees m) v)) mons end fun isolate_variable vars tm = @@ -850,7 +850,7 @@ fun isolate_monomials vars tm = let val (cmons,vmons) = - List.partition (fn m => null (inter (op aconvc) vars (Misc_Legacy.cterm_frees m))) + List.partition (fn m => null (inter (op aconvc) vars (Cterms.list_set_rev (Misc_Legacy.cterm_frees 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 d01920a8b082 -r f084d599bb44 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/Pure/General/table.ML Thu Sep 09 14:50:26 2021 +0200 @@ -25,7 +25,6 @@ val map: (key -> 'a -> 'b) -> 'a table -> 'b table val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a - val size: 'a table -> int val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list val min: 'a table -> (key * 'a) option @@ -62,8 +61,6 @@ val insert_set: key -> set -> set val remove_set: key -> set -> set val make_set: key list -> set - val subset: set * set -> bool - val eq_set: set * set -> bool end; functor Table(Key: KEY): TABLE = @@ -124,7 +121,6 @@ fold left (f p1 (fold mid (f p2 (fold right x)))); in fold end; -fun size tab = fold_table (fn _ => fn n => n + 1) tab 0; fun dest tab = fold_rev_table cons tab []; fun keys tab = fold_rev_table (cons o #1) tab []; @@ -450,9 +446,6 @@ fun remove_set x : set -> set = delete_safe x; fun make_set xs = build (fold insert_set xs); -fun subset (A: set, B: set) = forall (defined B o #1) A; -fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); - (* ML pretty-printing *) diff -r d01920a8b082 -r f084d599bb44 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/Pure/Isar/obtain.ML Thu Sep 09 14:50:26 2021 +0200 @@ -105,7 +105,7 @@ let val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I)); val T = - (case Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of + (case Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees of SOME T => T | NONE => the_default dummyT (Variable.default_type ctxt z)); in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end; diff -r d01920a8b082 -r f084d599bb44 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/Pure/Tools/rule_insts.ML Thu Sep 09 14:50:26 2021 +0200 @@ -53,7 +53,7 @@ error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos); fun the_sort tvars (ai, pos) : sort = - (case TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of + (case TVars.get_first (fn ((bi, S), _) => if ai = bi then SOME S else NONE) tvars of SOME S => S | NONE => error_var "No such type variable in theorem: " (ai, pos)); @@ -128,7 +128,7 @@ val instT1 = Term_Subst.instantiateT (TVars.make (map (read_type ctxt1 tvars) type_insts)); val vars1 = - Vartab.build (vars |> Vars.fold (fn ((v, T), ()) => + Vartab.build (vars |> Vars.fold (fn ((v, T), _) => Vartab.insert (K true) (v, instT1 T))); (*term instantiations*) diff -r d01920a8b082 -r f084d599bb44 src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/Pure/goal.ML Thu Sep 09 14:50:26 2021 +0200 @@ -122,7 +122,7 @@ val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As)); val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees); val instT = - build (tfrees |> TFrees.fold (fn ((a, S), ()) => + build (tfrees |> TFrees.fold (fn ((a, S), _) => cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S))))); val global_prop = diff -r d01920a8b082 -r f084d599bb44 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/Pure/more_thm.ML Thu Sep 09 14:50:26 2021 +0200 @@ -12,6 +12,7 @@ val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T + structure Cterms: ITEMS structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool @@ -23,6 +24,7 @@ include THM structure Ctermtab: TABLE structure Thmtab: TABLE + structure Cterms: ITEMS val eq_ctyp: ctyp * ctyp -> bool val aconvc: cterm * cterm -> bool val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table @@ -220,6 +222,7 @@ (* scalable collections *) +structure Cterms = Items(type key = cterm val ord = fast_term_ord); structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); structure Thmtab = Table(type key = thm val ord = thm_ord); @@ -452,16 +455,8 @@ (* implicit generalization over variables -- canonical order *) fun forall_intr_vars th = - let - val (_, vars) = - (th, (Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var - (fn ct => fn (seen, vars) => - let val v = Term.dest_Var (Thm.term_of ct) in - if not (Vars.defined seen v) - then (Vars.add_set v seen, ct :: vars) - else (seen, vars) - end); - in fold Thm.forall_intr vars th end; + let val vars = Cterms.build (Thm.fold_atomic_cterms {hyps = false} Term.is_Var Cterms.add_set th) + in fold_rev Thm.forall_intr (Cterms.list_set vars) th end; fun forall_intr_frees th = let @@ -469,15 +464,11 @@ Frees.build (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> fold Frees.add_frees (Thm.hyps_of th)); - val (_, frees) = - (th, (fixed, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free - (fn ct => fn (seen, frees) => - let val v = Term.dest_Free (Thm.term_of ct) in - if not (Frees.defined seen v) - then (Frees.add_set v seen, ct :: frees) - else (seen, frees) - end); - in fold Thm.forall_intr frees th end; + val is_fixed = Frees.defined fixed o Term.dest_Free o Thm.term_of; + val frees = + Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Free + (fn ct => not (is_fixed ct) ? Cterms.add_set ct)); + in fold_rev Thm.forall_intr (Cterms.list_set frees) th end; (* unvarify_global: global schematic variables *) diff -r d01920a8b082 -r f084d599bb44 src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/Pure/term_ord.ML Thu Sep 09 14:50:26 2021 +0200 @@ -11,11 +11,11 @@ type 'a table val empty: 'a table val build: ('a table -> 'a table) -> 'a table + val size: 'a table -> int val is_empty: 'a table -> bool val map: (key -> 'a -> 'b) -> 'a table -> 'b table val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a - val size: 'a table -> int val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list val exists: (key * 'a -> bool) -> 'a table -> bool @@ -25,9 +25,11 @@ val defined: 'a table -> key -> bool val add: key * 'a -> 'a table -> 'a table val make: (key * 'a) list -> 'a table - type set = unit table + type set = int table val add_set: key -> set -> set val make_set: key list -> set + val list_set: set -> key list + val list_set_rev: set -> key list val subset: set * set -> bool val eq_set: set * set -> bool end; @@ -35,37 +37,55 @@ functor Items(Key: KEY): ITEMS = struct +(* table with length *) + structure Table = Table(Key); type key = Table.key; -type 'a table = 'a Table.table; +datatype 'a table = Items of int * 'a Table.table; + +fun size (Items (n, _)) = n; +fun table (Items (_, tab)) = tab; + +val empty = Items (0, Table.empty); +fun build (f: 'a table -> 'a table) = f empty; +fun is_empty items = size items = 0; -val empty = Table.empty; -val build = Table.build; -val is_empty = Table.is_empty; -val size = Table.size; -val dest = Table.dest; -val keys = Table.keys; -val exists = Table.exists; -val forall = Table.forall; -val get_first = Table.get_first; -val lookup = Table.lookup; -val defined = Table.defined; +fun dest items = Table.dest (table items); +fun keys items = Table.keys (table items); +fun exists pred = Table.exists pred o table; +fun forall pred = Table.forall pred o table; +fun get_first get = Table.get_first get o table; +fun lookup items = Table.lookup (table items); +fun defined items = Table.defined (table items); + +fun add (key, x) (items as Items (n, tab)) = + if Table.defined tab key then items + else Items (n + 1, Table.update_new (key, x) tab); -fun add entry = Table.insert (K true) entry; -fun make entries = Table.build (fold add entries); +fun make entries = build (fold add entries); + + +(* set with order of addition *) -type set = unit table; +type set = int table; -fun add_set x = add (x, ()); +fun add_set x (items as Items (n, tab)) = + if Table.defined tab x then items + else Items (n + 1, Table.update_new (x, n) tab); + fun make_set xs = build (fold add_set xs); fun subset (A: set, B: set) = forall (defined B o #1) A; fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); -val map = Table.map; -val fold = Table.fold; -val fold_rev = Table.fold_rev; +fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1 +val list_set = list_set_ord int_ord; +val list_set_rev = list_set_ord (rev_order o int_ord); + +fun map f (Items (n, tab)) = Items (n, Table.map f tab); +fun fold f = Table.fold f o table; +fun fold_rev f = Table.fold_rev f o table; end; diff -r d01920a8b082 -r f084d599bb44 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Thu Sep 09 14:05:31 2021 +0200 +++ b/src/Tools/misc_legacy.ML Thu Sep 09 14:50:26 2021 +0200 @@ -5,8 +5,8 @@ signature MISC_LEGACY = sig - val thm_frees: thm -> cterm list - val cterm_frees: cterm -> cterm list + val thm_frees: thm -> Cterms.set + 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 @@ -26,16 +26,7 @@ structure Misc_Legacy: MISC_LEGACY = struct -fun thm_frees th = - (th, (Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free - (fn ct => fn (set, list) => - let val v = Term.dest_Free (Thm.term_of ct) in - if not (Frees.defined set v) - then (Frees.add_set v set, ct :: list) - else (set, list) - end) - |> #2; - +val thm_frees = Cterms.build o Thm.fold_atomic_cterms {hyps = true} Term.is_Free Cterms.add_set; val cterm_frees = thm_frees o Drule.mk_term; (*iterate a function over all types in a term*)