--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sat Apr 15 23:11:08 2023 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Mon Apr 17 23:32:46 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 -> Termset.T
+ val hyps_of : computer -> term list
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 * Termset.T * Sortset.T * prog * unit Unsynchronized.ref * naming)
+ (theory * Encode.encoding * term list * 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 Termset.T * Sortset.T * term
+datatype cthm = ComputeThm of term list * 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, hypset, shypset) th =
+ fun thm2rule (encoding, hyptable, shypset) th =
let
val (ComputeThm (hyps, shyps, prop)) = th
- val hypset = Termset.merge (hyps, hypset)
+ val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
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, hypset, shypset), (map rename_guard prems, pattern, rename 0 vars right))
+ ((encoding, hyptable, shypset), (map rename_guard prems, pattern, rename 0 vars right))
end
- val ((encoding, hypset, shypset), rules) =
- fold_rev (fn th => fn (encoding_hypset, rules) =>
+ val ((encoding, hyptable, shypset), rules) =
+ fold_rev (fn th => fn (encoding_hyptable, rules) =>
let
- val (encoding_hypset, rule) = thm2rule encoding_hypset th
- in (encoding_hypset, rule::rules) end)
- ths ((encoding, Termset.empty, Sortset.empty), [])
+ val (encoding_hyptable, rule) = thm2rule encoding_hyptable th
+ in (encoding_hyptable, rule::rules) end)
+ ths ((encoding, Termtab.empty, Sortset.empty), [])
fun make_cache_pattern t (encoding, cache_patterns) =
let
@@ -287,7 +287,7 @@
(encoding, p::cache_patterns)
end
- val (encoding, _) = Termset.fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
+ val (encoding, _) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
val prog =
case machine of
@@ -300,18 +300,17 @@
val shypset = Sortset.fold (fn s => has_witness s ? Sortset.remove s) shypset shypset
- in (thy, encoding, hypset, shypset, prog, stamp, default_naming) end
+ in (thy, encoding, Termtab.keys hyptable, 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 (Termset.make cache_patterns) raw_thms)))
+ Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty 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) (Termset.make cache_patterns) raw_thms
+ (encoding_of computer) cache_patterns raw_thms
val _ = (ref_of computer) := SOME c
in
()
@@ -328,6 +327,13 @@
(* 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>\<open>compute\<close>, fn (thy, hyps, shyps, prop) =>
let
@@ -368,7 +374,7 @@
val t = infer_types naming encoding ty t
val eq = Logic.mk_equals (t', t)
in
- export_thm thy (Termset.dest (hyps_of computer)) (shyps_of computer) eq
+ export_thm thy (hyps_of computer) (shyps_of computer) eq
end
(* --------- Simplify ------------ *)
@@ -376,7 +382,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 * Termset.T * Sortset.T
+ * prem list * AbstractMachine.term * term list * Sortset.T
exception ParamSimplify of computer * theorem
@@ -607,7 +613,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 (Termset.merge (hyps_of_theorem th, hyps_of_theorem th')) th
+ val th = update_hyps (merge_hyps (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
@@ -624,10 +630,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 = Termset.merge (hyps_of computer, hyps_of_theorem th)
+ val hyps = merge_hyps (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) (Termset.dest hyps) shyps prop
+ export_thm (theory_of_theorem th) hyps shyps prop
end
end
--- a/src/Pure/thm.ML Sat Apr 15 23:11:08 2023 +0200
+++ b/src/Pure/thm.ML Mon Apr 17 23:32:46 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 -> Termset.T
+ val hyps_of: thm -> term list
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: Termset.T, (*hypotheses*)
+ hyps: term Ord_List.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 ? Termset.fold f hyps;
+ fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? 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,6 +487,10 @@
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);
@@ -533,8 +537,7 @@
(prems_of th);
fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) =
- map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t})
- (Termset.dest hyps);
+ map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
(* thm order: ignores theory context! *)
@@ -543,7 +546,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
- ||| Termset.ord o apply2 hyps_of
+ ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of
||| Sortset.ord o apply2 shyps_of);
@@ -720,7 +723,7 @@
maxidx = maxidx,
constraints = constraints,
shyps = Sortset.merge (sorts, shyps),
- hyps = Termset.insert A hyps,
+ hyps = insert_hyps A hyps,
tpairs = tpairs,
prop = prop})
end;
@@ -815,7 +818,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 _ = Termset.is_empty hyps orelse err "bad hyps";
+ val _ = null 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);
@@ -838,7 +841,7 @@
maxidx = maxidx,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = prop})
end;
@@ -858,8 +861,7 @@
in
Thm (der,
{cert = cert, tags = [], maxidx = maxidx,
- constraints = Constraints.empty, shyps = shyps,
- hyps = Termset.empty, tpairs = [], prop = prop})
+ constraints = Constraints.empty, shyps = shyps, hyps = [], tpairs = [], prop = prop})
end
| NONE => raise THEORY ("No axiom " ^ quote name, [thy]));
@@ -1073,12 +1075,12 @@
(*non-deterministic, depends on unknown promises*)
fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
- Proofterm.get_approximative_name shyps (Termset.dest hyps) prop (Proofterm.proof_of body);
+ Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body);
fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
let
val self_id =
- (case Proofterm.get_identity shyps (Termset.dest hyps) prop (Proofterm.proof_of body) of
+ (case Proofterm.get_identity shyps 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;
@@ -1086,11 +1088,11 @@
(*deterministic name of finished proof*)
fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
- Proofterm.get_approximative_name shyps (Termset.dest hyps) prop (proof_of thm);
+ Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
(*identified PThm node*)
fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
- Proofterm.get_id shyps (Termset.dest hyps) prop (proof_of thm);
+ Proofterm.get_id shyps hyps prop (proof_of thm);
(*dependencies of PThm node*)
fun thm_deps (thm as Thm (Deriv {promises, body = PBody {thms, ...}, ...}, _)) =
@@ -1115,7 +1117,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 (Termset.dest hyps) prop ps body;
+ name_pos shyps hyps prop ps body;
val der' = make_deriv empty_promises Oracles.empty (PThms.make [pthm]) proof;
in Thm (der', args) end);
@@ -1153,7 +1155,7 @@
maxidx = maxidx,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = prop})
end
@@ -1190,7 +1192,7 @@
maxidx = ~1,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.make [prop],
+ hyps = [prop],
tpairs = [],
prop = prop})
end;
@@ -1214,7 +1216,7 @@
maxidx = Int.max (maxidx1, maxidx2),
constraints = constraints,
shyps = Sortset.merge (sorts, shyps),
- hyps = Termset.remove A hyps,
+ hyps = remove_hyps A hyps,
tpairs = tpairs,
prop = Logic.mk_implies (A, prop)});
@@ -1241,7 +1243,7 @@
maxidx = Int.max (maxidx1, maxidx2),
constraints = Constraints.merge (constraintsA, constraints),
shyps = Sortset.merge (shypsA, shyps),
- hyps = Termset.merge (hypsA, hyps),
+ hyps = union_hyps hypsA hyps,
tpairs = union_tpairs tpairsA tpairs,
prop = B})
else err ()
@@ -1257,7 +1259,7 @@
*)
fun occs x ts tpairs =
let fun occs t = Logic.occs (x, t)
- in Termset.exists occs ts orelse exists (occs o fst) tpairs orelse exists (occs o snd) tpairs end;
+ in 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 +1281,7 @@
in
(case x of
Free (a, _) => check_result a hyps
- | Var ((a, _), _) => check_result a Termset.empty
+ | Var ((a, _), _) => check_result a []
| _ => raise THM ("forall_intr: not a variable", 0, [th]))
end;
@@ -1320,7 +1322,7 @@
maxidx = maxidx,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, t)});
@@ -1366,7 +1368,7 @@
maxidx = Int.max (maxidx1, maxidx2),
constraints = Constraints.merge (constraints1, constraints2),
shyps = Sortset.merge (shyps1, shyps2),
- hyps = Termset.merge (hyps1, hyps2),
+ hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = eq $ t1 $ t2})
| _ => err "premises"
@@ -1389,7 +1391,7 @@
maxidx = maxidx,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, t')})
end;
@@ -1401,7 +1403,7 @@
maxidx = maxidx,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, Envir.eta_contract t)});
@@ -1412,7 +1414,7 @@
maxidx = maxidx,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = Logic.mk_equals (t, Envir.eta_long [] t)});
@@ -1445,7 +1447,7 @@
in
(case x of
Free (a, _) => check_result a hyps
- | Var ((a, _), _) => check_result a Termset.empty
+ | Var ((a, _), _) => check_result a []
| _ => raise THM ("abstract_rule: not a variable", 0, [th]))
end;
@@ -1478,7 +1480,7 @@
maxidx = Int.max (maxidx1, maxidx2),
constraints = Constraints.merge (constraints1, constraints2),
shyps = Sortset.merge (shyps1, shyps2),
- hyps = Termset.merge (hyps1, hyps2),
+ hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = Logic.mk_equals (f $ t, g $ u)}))
| _ => raise THM ("combination: premises", 0, [th1, th2]))
@@ -1506,7 +1508,7 @@
maxidx = Int.max (maxidx1, maxidx2),
constraints = Constraints.merge (constraints1, constraints2),
shyps = Sortset.merge (shyps1, shyps2),
- hyps = Termset.merge (hyps1, hyps2),
+ hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = Logic.mk_equals (A, B)})
else err "not equal"
@@ -1535,7 +1537,7 @@
maxidx = Int.max (maxidx1, maxidx2),
constraints = Constraints.merge (constraints1, constraints2),
shyps = Sortset.merge (shyps1, shyps2),
- hyps = Termset.merge (hyps1, hyps2),
+ hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = B})
else err "not equal"
@@ -1599,7 +1601,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 _ = Termset.exists bad_term hyps andalso
+ val _ = exists bad_term hyps andalso
raise THM ("generalize: variable free in assumptions", 0, [th]);
val generalize = Term_Subst.generalize (tfrees, frees) idx;
@@ -1759,7 +1761,7 @@
maxidx = maxidx,
constraints = Constraints.empty,
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = Logic.mk_implies (A, A)});
@@ -1783,7 +1785,7 @@
maxidx = maxidx,
constraints = Constraints.build (insert_constraints thy (T, [c])),
shyps = sorts,
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = prop})
else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
@@ -1798,7 +1800,7 @@
val thy = theory_of_thm thm;
fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
- val _ = Termset.is_empty hyps orelse err "bad hyps";
+ val _ = null 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 +1818,7 @@
maxidx = maxidx_of_term prop',
constraints = Constraints.empty,
shyps = Sortset.make [[]], (*potentially redundant*)
- hyps = Termset.empty,
+ hyps = [],
tpairs = [],
prop = prop'})
end);
@@ -1824,7 +1826,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 = Termset.fold TFrees.add_tfrees hyps fixed;
+ val tfrees = 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 +1867,7 @@
val thm = strip_shyps raw_thm;
fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
in
- if not (Termset.is_empty (hyps_of thm)) then
+ if not (null (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 +2198,7 @@
maxidx = Envir.maxidx_of env,
constraints = constraints',
shyps = Envir.insert_sorts env (Sortset.merge (shyps1, shyps2)),
- hyps = Termset.merge (hyps1, hyps2),
+ hyps = union_hyps hyps1 hyps2,
tpairs = ntpairs,
prop = Logic.list_implies normp,
cert = cert})