# HG changeset patch # User wenzelm # Date 1681159098 -7200 # Node ID b43ee37926a9413c603f417c94980ad0e9648237 # Parent 15d39d6bb258f83c7793ccf050128f0bcc76e816 performance tuning: replace Ord_List by Set(); diff -r 15d39d6bb258 -r b43ee37926a9 src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Apr 10 22:38:18 2023 +0200 @@ -169,7 +169,7 @@ (Thm.implies_intr (Thm.cprop_of tha) thb); fun prove_hyp tha thb = - if exists (curry op aconv (Thm.concl_of tha)) (Thm.hyps_of thb) (* FIXME !? *) + if Termset.exists (curry op aconv (Thm.concl_of tha)) (Thm.hyps_of thb) (* FIXME !? *) then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb; val pth = @{lemma "(((x::real) < y) \ (y - x > 0))" and "((x \ y) \ (y - x \ 0))" and diff -r 15d39d6bb258 -r b43ee37926a9 src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/HOL/Library/old_recdef.ML Mon Apr 10 22:38:18 2023 +0200 @@ -920,8 +920,9 @@ fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm); fun dest_thm thm = - (map HOLogic.dest_Trueprop (Thm.hyps_of thm), HOLogic.dest_Trueprop (Thm.prop_of thm)) - handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop"; + (map HOLogic.dest_Trueprop (Termset.dest (Thm.hyps_of thm)), + HOLogic.dest_Trueprop (Thm.prop_of thm)) + handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop"; (* Inference rules *) @@ -1101,7 +1102,7 @@ fun DISJ_CASESL disjth thl = let val c = cconcl disjth fun eq th atm = - exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th) + Termset.exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th) val tml = Dcterm.strip_disj c fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases" | DL th [th1] = PROVE_HYP th th1 diff -r 15d39d6bb258 -r b43ee37926a9 src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Mon Apr 10 22:38:18 2023 +0200 @@ -16,7 +16,7 @@ val make : machine -> theory -> thm list -> computer val make_with_cache : machine -> theory -> term list -> thm list -> computer val theory_of : computer -> theory - val hyps_of : computer -> term list + val hyps_of : computer -> Termset.T val shyps_of : computer -> Sortset.T (* ! *) val update : computer -> thm list -> unit (* ! *) val update_with_cache : computer -> term list -> thm list -> unit @@ -169,7 +169,7 @@ fun default_naming i = "v_" ^ string_of_int i datatype computer = Computer of - (theory * Encode.encoding * term list * Sortset.T * prog * unit Unsynchronized.ref * naming) + (theory * Encode.encoding * Termset.T * Sortset.T * prog * unit Unsynchronized.ref * naming) option Unsynchronized.ref fun theory_of (Computer (Unsynchronized.ref (SOME (thy,_,_,_,_,_,_)))) = thy @@ -187,7 +187,7 @@ fun ref_of (Computer r) = r -datatype cthm = ComputeThm of term list * Sortset.T * term +datatype cthm = ComputeThm of Termset.T * Sortset.T * term fun thm2cthm th = (if not (null (Thm.tpairs_of th)) then raise Make "theorems may not contain tpairs" else (); @@ -219,10 +219,10 @@ (n, vars, AbstractMachine.PConst (c, args@[pb])) end - fun thm2rule (encoding, hyptable, shypset) th = + fun thm2rule (encoding, hypset, shypset) th = let val (ComputeThm (hyps, shyps, prop)) = th - val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable + val hypset = Termset.merge (hyps, hypset) val shypset = Sortset.merge (shyps, shypset) val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop) val (a, b) = Logic.dest_equals prop @@ -269,15 +269,15 @@ fun rename_guard (AbstractMachine.Guard (a,b)) = AbstractMachine.Guard (rename 0 vars a, rename 0 vars b) in - ((encoding, hyptable, shypset), (map rename_guard prems, pattern, rename 0 vars right)) + ((encoding, hypset, shypset), (map rename_guard prems, pattern, rename 0 vars right)) end - val ((encoding, hyptable, shypset), rules) = - fold_rev (fn th => fn (encoding_hyptable, rules) => + val ((encoding, hypset, shypset), rules) = + fold_rev (fn th => fn (encoding_hypset, rules) => let - val (encoding_hyptable, rule) = thm2rule encoding_hyptable th - in (encoding_hyptable, rule::rules) end) - ths ((encoding, Termtab.empty, Sortset.empty), []) + val (encoding_hypset, rule) = thm2rule encoding_hypset th + in (encoding_hypset, rule::rules) end) + ths ((encoding, Termset.empty, Sortset.empty), []) fun make_cache_pattern t (encoding, cache_patterns) = let @@ -287,7 +287,7 @@ (encoding, p::cache_patterns) end - val (encoding, _) = fold_rev make_cache_pattern cache_pattern_terms (encoding, []) + val (encoding, _) = Termset.fold_rev make_cache_pattern cache_pattern_terms (encoding, []) val prog = case machine of @@ -300,17 +300,18 @@ val shypset = Sortset.fold (fn s => has_witness s ? Sortset.remove s) shypset shypset - in (thy, encoding, Termtab.keys hyptable, shypset, prog, stamp, default_naming) end + in (thy, encoding, hypset, shypset, prog, stamp, default_naming) end fun make_with_cache machine thy cache_patterns raw_thms = - Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) + Computer (Unsynchronized.ref + (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty (Termset.make cache_patterns) raw_thms))) fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms fun update_with_cache computer cache_patterns raw_thms = let val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) - (encoding_of computer) cache_patterns raw_thms + (encoding_of computer) (Termset.make cache_patterns) raw_thms val _ = (ref_of computer) := SOME c in () @@ -327,13 +328,6 @@ (* An oracle for exporting theorems; must only be accessible from inside this structure! *) (* ------------------------------------------------------------------------------------- *) -fun merge_hyps hyps1 hyps2 = -let - fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab -in - Termtab.keys (add hyps2 (add hyps1 Termtab.empty)) -end - val (_, export_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\compute\, fn (thy, hyps, shyps, prop) => let @@ -374,7 +368,7 @@ val t = infer_types naming encoding ty t val eq = Logic.mk_equals (t', t) in - export_thm thy (hyps_of computer) (shyps_of computer) eq + export_thm thy (Termset.dest (hyps_of computer)) (shyps_of computer) eq end (* --------- Simplify ------------ *) @@ -382,7 +376,7 @@ datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int | Prem of AbstractMachine.term datatype theorem = Theorem of theory * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table - * prem list * AbstractMachine.term * term list * Sortset.T + * prem list * AbstractMachine.term * Termset.T * Sortset.T exception ParamSimplify of computer * theorem @@ -613,7 +607,7 @@ let val th = update_varsubst varsubst th val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th - val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th + val th = update_hyps (Termset.merge (hyps_of_theorem th, hyps_of_theorem th')) th val th = update_shyps (Sortset.merge (shyps_of_theorem th, shyps_of_theorem th')) th in update_theory thy th @@ -630,10 +624,10 @@ fun run t = infer (runprog (prog_of computer) (apply_subst true varsubst t)) fun runprem p = run (prem2term p) val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th)) - val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th) + val hyps = Termset.merge (hyps_of computer, hyps_of_theorem th) val shyps = Sortset.merge (shyps_of_theorem th, shyps_of computer) in - export_thm (theory_of_theorem th) hyps shyps prop + export_thm (theory_of_theorem th) (Termset.dest hyps) shyps prop end end diff -r 15d39d6bb258 -r b43ee37926a9 src/HOL/Matrix_LP/Compute_Oracle/linker.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Mon Apr 10 22:38:18 2023 +0200 @@ -365,12 +365,12 @@ (!changed, result) end -datatype cthm = ComputeThm of term list * Sortset.T * term +datatype cthm = ComputeThm of Termset.T * Sortset.T * term fun thm2cthm th = ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th) val cthm_ord' = - prod_ord (prod_ord (list_ord Term_Ord.term_ord) Sortset.ord) Term_Ord.term_ord + prod_ord (prod_ord Termset.ord Sortset.ord) Term_Ord.term_ord fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2)) diff -r 15d39d6bb258 -r b43ee37926a9 src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/HOL/Tools/sat.ML Mon Apr 10 22:38:18 2023 +0200 @@ -153,9 +153,9 @@ val _ = cond_tracing ctxt (fn () => "Resolving clause: " ^ Thm.string_of_thm ctxt c1 ^ - " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^ + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Termset.dest (Thm.hyps_of c1)) ^ ")\nwith clause: " ^ Thm.string_of_thm ctxt c2 ^ - " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")") + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Termset.dest (Thm.hyps_of c2)) ^ ")") (* the two literals used for resolution *) val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] @@ -186,7 +186,7 @@ cond_tracing ctxt (fn () => "Resulting clause: " ^ Thm.string_of_thm ctxt c_new ^ " (hyps: " ^ - ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")") + ML_Syntax.print_list (Syntax.string_of_term ctxt) (Termset.dest (Thm.hyps_of c_new)) ^ ")") val _ = Unsynchronized.inc counter in diff -r 15d39d6bb258 -r b43ee37926a9 src/HOL/Types_To_Sets/local_typedef.ML --- a/src/HOL/Types_To_Sets/local_typedef.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/HOL/Types_To_Sets/local_typedef.ML Mon Apr 10 22:38:18 2023 +0200 @@ -35,7 +35,7 @@ val thy = Thm.theory_of_thm thm; val prop = Thm.prop_of thm; - val hyps = Thm.hyps_of thm; + val hyps = Termset.dest (Thm.hyps_of thm); val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs"; diff -r 15d39d6bb258 -r b43ee37926a9 src/HOL/Types_To_Sets/unoverloading.ML --- a/src/HOL/Types_To_Sets/unoverloading.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/HOL/Types_To_Sets/unoverloading.ML Mon Apr 10 22:38:18 2023 +0200 @@ -80,7 +80,7 @@ let fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]); - val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses"; + val _ = Termset.is_empty (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses"; val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs"; val prop = Thm.prop_of thm; diff -r 15d39d6bb258 -r b43ee37926a9 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/Pure/Isar/element.ML Mon Apr 10 22:38:18 2023 +0200 @@ -266,7 +266,7 @@ val mark_witness = Logic.protect; fun witness_prop (Witness (t, _)) = t; -fun witness_hyps (Witness (_, th)) = Thm.hyps_of th; +fun witness_hyps (Witness (_, th)) = Termset.dest (Thm.hyps_of th); fun map_witness f (Witness witn) = Witness (f witn); fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th)); diff -r 15d39d6bb258 -r b43ee37926a9 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/Pure/more_thm.ML Mon Apr 10 22:38:18 2023 +0200 @@ -278,14 +278,13 @@ map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); fun undeclared_hyps context th = - Thm.hyps_of th - |> filter_out + Termset.fold_rev (case context of - Context.Theory _ => K false + Context.Theory _ => cons | Context.Proof ctxt => - (case Hyps.get ctxt of - {checked_hyps = false, ...} => K true - | {hyps, ...} => Termset.member hyps)); + let val {checked_hyps, hyps, ...} = Hyps.get ctxt + in fn hyp => if not checked_hyps orelse Termset.member hyps hyp then I else cons hyp end) + (Thm.hyps_of th) []; fun check_hyps context th = (case undeclared_hyps context th of @@ -447,7 +446,7 @@ val fixed = Frees.build (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> - fold Frees.add_frees (Thm.hyps_of th)); + Termset.fold Frees.add_frees (Thm.hyps_of th)); 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 @@ -460,7 +459,9 @@ fun unvarify_global thy th = let val prop = Thm.full_prop_of th; - val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) + val _ = + (Logic.unvarify_global prop; + Termset.fold (fn t => fn () => ignore (Logic.unvarify_global t)) (Thm.hyps_of th) ()) handle TERM (msg, _) => raise THM (msg, 0, [th]); val cert = Thm.global_cterm_of thy; @@ -717,7 +718,9 @@ |> perhaps (try (Thm.transfer' ctxt)) |> perhaps (try Thm.strip_shyps); - val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; + val hyps = + if show_hyps then Termset.dest (Thm.hyps_of th) + else undeclared_hyps (Context.Proof ctxt) th; val extra_shyps = Sortset.dest (extra_shyps' ctxt th); val tags = Thm.get_tags th; val tpairs = Thm.tpairs_of th; diff -r 15d39d6bb258 -r b43ee37926a9 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/Pure/raw_simplifier.ML Mon Apr 10 22:38:18 2023 +0200 @@ -1280,8 +1280,8 @@ let val prem' = Thm.rhs_of eqn; val tprems = map Thm.term_of prems; - val i = 1 + fold Integer.max (map (fn p => - find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1; + val i = 1 + Termset.fold (fn p => + Integer.max (find_index (fn q => q aconv p) tprems)) (Thm.hyps_of eqn) ~1; val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt; in mut_impc prems concl rrss asms (prem' :: prems') diff -r 15d39d6bb258 -r b43ee37926a9 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/Pure/thm.ML Mon Apr 10 22:38:18 2023 +0200 @@ -70,7 +70,7 @@ val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val shyps_of: thm -> Sortset.T - val hyps_of: thm -> term list + val hyps_of: thm -> Termset.T val prop_of: thm -> term val tpairs_of: thm -> (term * term) list val concl_of: thm -> term @@ -433,7 +433,7 @@ maxidx: int, (*maximum index of any Var or TVar*) constraints: Constraints.T, (*implicit proof obligations for sort constraints*) shyps: Sortset.T, (*sort hypotheses*) - hyps: term Ord_List.T, (*hypotheses*) + hyps: Termset.T, (*hypotheses*) tpairs: (term * term) list, (*flex-flex pairs*) prop: term} (*conclusion*) and deriv = Deriv of @@ -456,7 +456,7 @@ fun rep_thm (Thm (_, args)) = args; fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) = - fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps; + fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? Termset.fold f hyps; fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} @@ -487,10 +487,6 @@ fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop; -val union_hyps = Ord_List.union Term_Ord.fast_term_ord; -val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; -val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; - fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) = Context.join_certificate (cert1, cert2); @@ -537,7 +533,8 @@ (prems_of th); fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = - map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps; + map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) + (Termset.dest hyps); (* thm order: ignores theory context! *) @@ -546,7 +543,7 @@ pointer_eq_ord (Term_Ord.fast_term_ord o apply2 prop_of ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of - ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of + ||| Termset.ord o apply2 hyps_of ||| Sortset.ord o apply2 shyps_of); @@ -723,7 +720,7 @@ maxidx = maxidx, constraints = constraints, shyps = Sortset.merge (sorts, shyps), - hyps = insert_hyps A hyps, + hyps = Termset.insert A hyps, tpairs = tpairs, prop = prop}) end; @@ -818,7 +815,7 @@ val _ = prop aconv orig_prop orelse err "bad prop"; val _ = Constraints.is_empty constraints orelse err "bad sort constraints"; val _ = null tpairs orelse err "bad flex-flex constraints"; - val _ = null hyps orelse err "bad hyps"; + val _ = Termset.is_empty hyps orelse err "bad hyps"; val _ = Sortset.subset (shyps, orig_shyps) orelse err "bad shyps"; val _ = forall_promises (fn j => i <> j) promises orelse err "bad dependencies"; val _ = join_promises (dest_promises promises); @@ -841,7 +838,7 @@ maxidx = maxidx, constraints = Constraints.empty, shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = prop}) end; @@ -861,7 +858,8 @@ in Thm (der, {cert = cert, tags = [], maxidx = maxidx, - constraints = Constraints.empty, shyps = shyps, hyps = [], tpairs = [], prop = prop}) + constraints = Constraints.empty, shyps = shyps, + hyps = Termset.empty, tpairs = [], prop = prop}) end | NONE => raise THEORY ("No axiom " ^ quote name, [thy])); @@ -1074,12 +1072,12 @@ (*non-deterministic, depends on unknown promises*) fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = - Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body); + Proofterm.get_approximative_name shyps (Termset.dest hyps) prop (Proofterm.proof_of body); fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = let val self_id = - (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of + (case Proofterm.get_identity shyps (Termset.dest hyps) prop (Proofterm.proof_of body) of NONE => K false | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE; @@ -1087,11 +1085,11 @@ (*deterministic name of finished proof*) fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) = - Proofterm.get_approximative_name shyps hyps prop (proof_of thm); + Proofterm.get_approximative_name shyps (Termset.dest hyps) prop (proof_of thm); (*identified PThm node*) fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) = - Proofterm.get_id shyps hyps prop (proof_of thm); + Proofterm.get_id shyps (Termset.dest hyps) prop (proof_of thm); (*dependencies of PThm node*) fun thm_deps (thm as Thm (Deriv {promises, body = PBody {thms, ...}, ...}, _)) = @@ -1115,7 +1113,7 @@ val ps = map (apsnd (Future.map fulfill_body)) (dest_promises promises); val (pthm, proof) = Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) - name_pos shyps hyps prop ps body; + name_pos shyps (Termset.dest hyps) prop ps body; val der' = make_deriv empty_promises [] [pthm] proof; in Thm (der', args) end); @@ -1153,7 +1151,7 @@ maxidx = maxidx, constraints = Constraints.empty, shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = prop}) end @@ -1190,7 +1188,7 @@ maxidx = ~1, constraints = Constraints.empty, shyps = sorts, - hyps = [prop], + hyps = Termset.make [prop], tpairs = [], prop = prop}) end; @@ -1214,7 +1212,7 @@ maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sortset.merge (sorts, shyps), - hyps = remove_hyps A hyps, + hyps = Termset.remove A hyps, tpairs = tpairs, prop = Logic.mk_implies (A, prop)}); @@ -1241,7 +1239,7 @@ maxidx = Int.max (maxidx1, maxidx2), constraints = Constraints.merge (constraintsA, constraints), shyps = Sortset.merge (shypsA, shyps), - hyps = union_hyps hypsA hyps, + hyps = Termset.merge (hypsA, hyps), tpairs = union_tpairs tpairsA tpairs, prop = B}) else err () @@ -1257,7 +1255,7 @@ *) fun occs x ts tpairs = let fun occs t = Logic.occs (x, t) - in exists occs ts orelse exists (occs o fst) tpairs orelse exists (occs o snd) tpairs end; + in Termset.exists occs ts orelse exists (occs o fst) tpairs orelse exists (occs o snd) tpairs end; fun forall_intr (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...}) @@ -1279,7 +1277,7 @@ in (case x of Free (a, _) => check_result a hyps - | Var ((a, _), _) => check_result a [] + | Var ((a, _), _) => check_result a Termset.empty | _ => raise THM ("forall_intr: not a variable", 0, [th])) end; @@ -1320,7 +1318,7 @@ maxidx = maxidx, constraints = Constraints.empty, shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = Logic.mk_equals (t, t)}); @@ -1366,7 +1364,7 @@ maxidx = Int.max (maxidx1, maxidx2), constraints = Constraints.merge (constraints1, constraints2), shyps = Sortset.merge (shyps1, shyps2), - hyps = union_hyps hyps1 hyps2, + hyps = Termset.merge (hyps1, hyps2), tpairs = union_tpairs tpairs1 tpairs2, prop = eq $ t1 $ t2}) | _ => err "premises" @@ -1389,7 +1387,7 @@ maxidx = maxidx, constraints = Constraints.empty, shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = Logic.mk_equals (t, t')}) end; @@ -1401,7 +1399,7 @@ maxidx = maxidx, constraints = Constraints.empty, shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = Logic.mk_equals (t, Envir.eta_contract t)}); @@ -1412,7 +1410,7 @@ maxidx = maxidx, constraints = Constraints.empty, shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = Logic.mk_equals (t, Envir.eta_long [] t)}); @@ -1445,7 +1443,7 @@ in (case x of Free (a, _) => check_result a hyps - | Var ((a, _), _) => check_result a [] + | Var ((a, _), _) => check_result a Termset.empty | _ => raise THM ("abstract_rule: not a variable", 0, [th])) end; @@ -1478,7 +1476,7 @@ maxidx = Int.max (maxidx1, maxidx2), constraints = Constraints.merge (constraints1, constraints2), shyps = Sortset.merge (shyps1, shyps2), - hyps = union_hyps hyps1 hyps2, + hyps = Termset.merge (hyps1, hyps2), tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (f $ t, g $ u)})) | _ => raise THM ("combination: premises", 0, [th1, th2])) @@ -1506,7 +1504,7 @@ maxidx = Int.max (maxidx1, maxidx2), constraints = Constraints.merge (constraints1, constraints2), shyps = Sortset.merge (shyps1, shyps2), - hyps = union_hyps hyps1 hyps2, + hyps = Termset.merge (hyps1, hyps2), tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (A, B)}) else err "not equal" @@ -1535,7 +1533,7 @@ maxidx = Int.max (maxidx1, maxidx2), constraints = Constraints.merge (constraints1, constraints2), shyps = Sortset.merge (shyps1, shyps2), - hyps = union_hyps hyps1 hyps2, + hyps = Termset.merge (hyps1, hyps2), tpairs = union_tpairs tpairs1 tpairs2, prop = B}) else err "not equal" @@ -1599,7 +1597,7 @@ | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t | bad_term (t $ u) = bad_term t orelse bad_term u | bad_term (Bound _) = false; - val _ = exists bad_term hyps andalso + val _ = Termset.exists bad_term hyps andalso raise THM ("generalize: variable free in assumptions", 0, [th]); val generalize = Term_Subst.generalize (tfrees, frees) idx; @@ -1759,7 +1757,7 @@ maxidx = maxidx, constraints = Constraints.empty, shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = Logic.mk_implies (A, A)}); @@ -1783,7 +1781,7 @@ maxidx = maxidx, constraints = Constraints.build (insert_constraints thy (T, [c])), shyps = sorts, - hyps = [], + hyps = Termset.empty, tpairs = [], prop = prop}) else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, []) @@ -1798,7 +1796,7 @@ val thy = theory_of_thm thm; fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); - val _ = null hyps orelse err "bad hyps"; + val _ = Termset.is_empty hyps orelse err "bad hyps"; val _ = null tpairs orelse err "bad flex-flex constraints"; val tfrees = build_rev (Term.add_tfree_names prop); val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); @@ -1816,7 +1814,7 @@ maxidx = maxidx_of_term prop', constraints = Constraints.empty, shyps = Sortset.make [[]], (*potentially redundant*) - hyps = [], + hyps = Termset.empty, tpairs = [], prop = prop'}) end); @@ -1824,7 +1822,7 @@ (*Replace all TFrees not fixed or in the hyps by new TVars*) fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = let - val tfrees = fold TFrees.add_tfrees hyps fixed; + val tfrees = Termset.fold TFrees.add_tfrees hyps fixed; val prop1 = attach_tpairs tpairs prop; val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); @@ -1865,7 +1863,7 @@ val thm = strip_shyps raw_thm; fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); in - if not (null (hyps_of thm)) then + if not (Termset.is_empty (hyps_of thm)) then err "theorem may not contain hypotheses" else if not (Sortset.is_empty (extra_shyps thm)) then err "theorem may not contain sort hypotheses" @@ -2196,7 +2194,7 @@ maxidx = Envir.maxidx_of env, constraints = constraints', shyps = Envir.insert_sorts env (Sortset.merge (shyps1, shyps2)), - hyps = union_hyps hyps1 hyps2, + hyps = Termset.merge (hyps1, hyps2), tpairs = ntpairs, prop = Logic.list_implies normp, cert = cert}) diff -r 15d39d6bb258 -r b43ee37926a9 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Mon Apr 10 20:51:01 2023 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Mon Apr 10 22:38:18 2023 +0200 @@ -64,7 +64,8 @@ bound vars with binders outside the redex *) val ns = - IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts); + IsaND.variant_names ctxt (Thm.full_prop_of rule :: Termset.dest (Thm.hyps_of rule)) + (map fst Ts); val (fromnames, tonames, Ts') = fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>