--- a/src/Doc/Implementation/Logic.thy Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Doc/Implementation/Logic.thy Tue Apr 18 12:23:37 2023 +0200
@@ -949,7 +949,7 @@
text %mlref \<open>
\begin{mldecls}
- @{define_ML Thm.extra_shyps: "thm -> Sortset.T"} \\
+ @{define_ML Thm.extra_shyps: "thm -> sort list"} \\
@{define_ML Thm.strip_shyps: "thm -> thm"} \\
\end{mldecls}
@@ -971,7 +971,7 @@
theorem (in empty) false: False
using bad by blast
-ML_val \<open>\<^assert> (Sortset.dest (Thm.extra_shyps @{thm false}) = [\<^sort>\<open>empty\<close>])\<close>
+ML_val \<open>\<^assert> (Thm.extra_shyps @{thm false} = [\<^sort>\<open>empty\<close>])\<close>
text \<open>
Thanks to the inference kernel managing sort hypothesis according to their
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Apr 18 12:23:37 2023 +0200
@@ -17,7 +17,7 @@
val make_with_cache : machine -> theory -> term list -> thm list -> computer
val theory_of : computer -> theory
val hyps_of : computer -> term list
- val shyps_of : computer -> Sortset.T
+ val shyps_of : computer -> sort list
(* ! *) val update : computer -> thm list -> unit
(* ! *) val update_with_cache : computer -> term list -> thm list -> unit
@@ -169,12 +169,13 @@
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 * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming)
option Unsynchronized.ref
fun theory_of (Computer (Unsynchronized.ref (SOME (thy,_,_,_,_,_,_)))) = thy
fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
-fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shypset,_,_,_)))) = shypset
+fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
+fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
@@ -187,7 +188,7 @@
fun ref_of (Computer r) = r
-datatype cthm = ComputeThm of term list * Sortset.T * term
+datatype cthm = ComputeThm of term list * sort list * term
fun thm2cthm th =
(if not (null (Thm.tpairs_of th)) then raise Make "theorems may not contain tpairs" else ();
@@ -219,11 +220,11 @@
(n, vars, AbstractMachine.PConst (c, args@[pb]))
end
- fun thm2rule (encoding, hyptable, shypset) th =
+ fun thm2rule (encoding, hyptable, shyptable) th =
let
val (ComputeThm (hyps, shyps, prop)) = th
val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
- val shypset = Sortset.merge (shyps, shypset)
+ val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
val (a, b) = Logic.dest_equals prop
handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
@@ -269,15 +270,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, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
end
- val ((encoding, hyptable, shypset), rules) =
+ val ((encoding, hyptable, shyptable), rules) =
fold_rev (fn th => fn (encoding_hyptable, rules) =>
let
val (encoding_hyptable, rule) = thm2rule encoding_hyptable th
in (encoding_hyptable, rule::rules) end)
- ths ((encoding, Termtab.empty, Sortset.empty), [])
+ ths ((encoding, Termtab.empty, Sorttab.empty), [])
fun make_cache_pattern t (encoding, cache_patterns) =
let
@@ -298,9 +299,9 @@
fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
- val shypset = Sortset.fold (fn s => has_witness s ? Sortset.remove s) shypset shypset
+ val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
- in (thy, encoding, Termtab.keys hyptable, shypset, prog, stamp, default_naming) end
+ in (thy, encoding, Termtab.keys hyptable, shyptable, 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)))
@@ -334,19 +335,23 @@
Termtab.keys (add hyps2 (add hyps1 Termtab.empty))
end
+fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab
+
+fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
+
val (_, export_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (\<^binding>\<open>compute\<close>, fn (thy, hyps, shyps, prop) =>
let
- fun remove_term t = Sortset.subtract (Sortset.build (Sortset.insert_term t))
+ val shyptab = add_shyps shyps Sorttab.empty
+ fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
+ fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
- val shyps = Sortset.fold (fn s => has_witness s ? Sortset.remove s) shyps shyps
- val shyps =
- if Sortset.is_empty shyps then Sortset.empty
- else fold remove_term (prop::hyps) shyps
+ val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
+ val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
val _ =
- if not (Sortset.is_empty shyps) then
+ if not (null shyps) then
raise Compute ("dangling sort hypotheses: " ^
- commas (map (Syntax.string_of_sort_global thy) (Sortset.dest shyps)))
+ commas (map (Syntax.string_of_sort_global thy) shyps))
else ()
in
Thm.global_cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
@@ -374,7 +379,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 (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq
end
(* --------- Simplify ------------ *)
@@ -382,7 +387,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 * term list * sort list
exception ParamSimplify of computer * theorem
@@ -614,7 +619,7 @@
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_shyps (Sortset.merge (shyps_of_theorem th, shyps_of_theorem th')) th
+ val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th
in
update_theory thy th
end
@@ -631,9 +636,10 @@
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 shyps = Sortset.merge (shyps_of_theorem th, shyps_of computer)
+ val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer))
in
export_thm (theory_of_theorem th) hyps shyps prop
end
end
+
--- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Tue Apr 18 12:23:37 2023 +0200
@@ -365,12 +365,12 @@
(!changed, result)
end
-datatype cthm = ComputeThm of term list * Sortset.T * term
+datatype cthm = ComputeThm of term list * sort list * 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 (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) =
cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
--- a/src/HOL/Types_To_Sets/internalize_sort.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML Tue Apr 18 12:23:37 2023 +0200
@@ -31,7 +31,7 @@
val thy = Thm.theory_of_thm thm;
val tvar = Thm.typ_of ctvar;
- val (ucontext, _) = Logic.unconstrainT Sortset.empty (Thm.prop_of thm);
+ val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm);
fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
fun reduce_to_non_proper_sort (TVar (name, sort)) =
--- a/src/Pure/Thy/export_theory.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/Thy/export_theory.ML Tue Apr 18 12:23:37 2023 +0200
@@ -264,7 +264,7 @@
in ((sorts @ typargs, args, prop), proof) end;
fun standard_prop_of thm =
- standard_prop Name.context (Sortset.dest (Thm.extra_shyps thm)) (Thm.full_prop_of thm);
+ standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
val encode_prop =
let open XML.Encode Term_XML.Encode
--- a/src/Pure/envir.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/envir.ML Tue Apr 18 12:23:37 2023 +0200
@@ -17,7 +17,7 @@
val empty: int -> env
val init: env
val merge: env * env -> env
- val insert_sorts: env -> Sortset.T -> Sortset.T
+ val insert_sorts: env -> sort list -> sort list
val genvars: string -> env * typ list -> env * term list
val genvar: string -> env * typ -> env * term
val lookup1: tenv -> indexname * typ -> term option
@@ -94,7 +94,7 @@
(*NB: type unification may invent new sorts*) (* FIXME tenv!? *)
-val insert_sorts = Vartab.fold (Sortset.insert_typ o #2 o #2) o type_env;
+val insert_sorts = Vartab.fold (Sorts.insert_typ o #2 o #2) o type_env;
(*Generate a list of distinct variables.
Increments index to make them distinct from ALL present variables. *)
--- a/src/Pure/logic.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/logic.ML Tue Apr 18 12:23:37 2023 +0200
@@ -66,7 +66,7 @@
map_atyps: typ -> typ,
constraints: ((typ * class) * term) list,
outer_constraints: (typ * class) list};
- val unconstrainT: Sortset.T -> term -> unconstrain_context * term
+ val unconstrainT: sort list -> term -> unconstrain_context * term
val protectC: term
val protect: term -> term
val unprotect: term -> term
@@ -365,7 +365,7 @@
fun unconstrainT shyps prop =
let
val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
- val extra = Sortset.dest (fold (Sortset.remove o #2) present shyps);
+ val extra = fold (Sorts.remove_sort o #2) present shyps;
val n = length present;
val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
--- a/src/Pure/more_thm.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/more_thm.ML Tue Apr 18 12:23:37 2023 +0200
@@ -57,7 +57,7 @@
val undeclared_hyps: Context.generic -> thm -> term list
val check_hyps: Context.generic -> thm -> thm
val declare_term_sorts: term -> Proof.context -> Proof.context
- val extra_shyps': Proof.context -> thm -> Sortset.T
+ val extra_shyps': Proof.context -> thm -> sort list
val check_shyps: Proof.context -> thm -> thm
val weaken_sorts': Proof.context -> cterm -> cterm
val elim_implies: thm -> thm -> thm
@@ -253,8 +253,8 @@
structure Hyps = Proof_Data
(
- type T = {checked_hyps: bool, hyps: Termset.T, shyps: Sortset.T};
- fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = Sortset.empty};
+ type T = {checked_hyps: bool, hyps: Termset.T, shyps: sort Ord_List.T};
+ fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = []};
);
fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} =>
@@ -299,19 +299,19 @@
fun declare_term_sorts t =
map_hyps (fn (checked_hyps, hyps, shyps) =>
- (checked_hyps, hyps, Sortset.insert_term t shyps));
+ (checked_hyps, hyps, Sorts.insert_term t shyps));
fun extra_shyps' ctxt th =
- Sortset.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
+ Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
fun check_shyps ctxt raw_th =
let
val th = Thm.strip_shyps raw_th;
val extra_shyps = extra_shyps' ctxt th;
in
- if Sortset.is_empty extra_shyps then th
+ if null extra_shyps then th
else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
- Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) (Sortset.dest extra_shyps)))))
+ Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps))))
end;
val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get;
@@ -718,7 +718,7 @@
|> perhaps (try Thm.strip_shyps);
val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
- val extra_shyps = Sortset.dest (extra_shyps' ctxt th);
+ val extra_shyps = extra_shyps' ctxt th;
val tags = Thm.get_tags th;
val tpairs = Thm.tpairs_of th;
--- a/src/Pure/proofterm.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/proofterm.ML Tue Apr 18 12:23:37 2023 +0200
@@ -136,7 +136,7 @@
val abstract_rule_proof: string * term -> proof -> proof
val combination_proof: term -> term -> term -> term -> proof -> proof -> proof
val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
- Sortset.T -> proof -> proof
+ sort list -> proof -> proof
val of_sort_proof: Sorts.algebra ->
(class * class -> proof) ->
(string * class list list * class -> proof) ->
@@ -177,19 +177,19 @@
val export_proof_boxes: proof_body list -> unit
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> (class * class -> proof) ->
- (string * class list list * class -> proof) -> string * Position.T -> Sortset.T ->
+ (string * class list list * class -> proof) -> string * Position.T -> sort list ->
term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
val unconstrain_thm_proof: theory -> (class * class -> proof) ->
- (string * class list list * class -> proof) -> Sortset.T -> term ->
+ (string * class list list * class -> proof) -> sort list -> term ->
(serial * proof_body future) list -> proof_body -> thm * proof
- val get_identity: Sortset.T -> term list -> term -> proof ->
+ val get_identity: sort list -> term list -> term -> proof ->
{serial: serial, theory_name: string, name: string} option
- val get_approximative_name: Sortset.T -> term list -> term -> proof -> string
+ val get_approximative_name: sort list -> term list -> term -> proof -> string
type thm_id = {serial: serial, theory_name: string}
val make_thm_id: serial * string -> thm_id
val thm_header_id: thm_header -> thm_id
val thm_id: thm -> thm_id
- val get_id: Sortset.T -> term list -> term -> proof -> thm_id option
+ val get_id: sort list -> term list -> term -> proof -> thm_id option
val this_id: thm_id option -> thm_id -> bool
val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} ->
proof list -> (thm_header * proof) list (*exception MIN_PROOF*)
@@ -1086,7 +1086,7 @@
fun strip_shyps_proof algebra present witnessed extra prf =
let
- val replacements = present @ witnessed @ map (`Logic.dummy_tfree) (Sortset.dest extra);
+ val replacements = present @ witnessed @ map (`Logic.dummy_tfree) extra;
fun get_replacement S =
replacements |> get_first (fn (T', S') =>
if Sorts.sort_le algebra (S', S) then SOME T' else NONE);
@@ -1182,7 +1182,7 @@
fun const_proof mk name prop =
let
val args = prop_args prop;
- val ({outer_constraints, ...}, prop1) = Logic.unconstrainT Sortset.empty prop;
+ val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop;
val head = mk (name, prop1, NONE);
in proof_combP (proof_combt' (head, args), map PClass outer_constraints) end;
--- a/src/Pure/sorts.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/sorts.ML Tue Apr 18 12:23:37 2023 +0200
@@ -14,6 +14,16 @@
signature SORTS =
sig
+ val make: sort list -> sort Ord_List.T
+ val subset: sort Ord_List.T * sort Ord_List.T -> bool
+ val union: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+ val subtract: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+ val remove_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+ val insert_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+ val insert_typ: typ -> sort Ord_List.T -> sort Ord_List.T
+ val insert_typs: typ list -> sort Ord_List.T -> sort Ord_List.T
+ val insert_term: term -> sort Ord_List.T -> sort Ord_List.T
+ val insert_terms: term list -> sort Ord_List.T -> sort Ord_List.T
type algebra
val classes_of: algebra -> serial Graph.T
val arities_of: algebra -> (class * sort list) list Symtab.table
@@ -59,6 +69,35 @@
structure Sorts: SORTS =
struct
+
+(** ordered lists of sorts **)
+
+val make = Ord_List.make Term_Ord.sort_ord;
+val subset = Ord_List.subset Term_Ord.sort_ord;
+val union = Ord_List.union Term_Ord.sort_ord;
+val subtract = Ord_List.subtract Term_Ord.sort_ord;
+
+val remove_sort = Ord_List.remove Term_Ord.sort_ord;
+val insert_sort = Ord_List.insert Term_Ord.sort_ord;
+
+fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
+ | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
+ | insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss
+and insert_typs [] Ss = Ss
+ | insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss);
+
+fun insert_term (Const (_, T)) Ss = insert_typ T Ss
+ | insert_term (Free (_, T)) Ss = insert_typ T Ss
+ | insert_term (Var (_, T)) Ss = insert_typ T Ss
+ | insert_term (Bound _) Ss = Ss
+ | insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss)
+ | insert_term (t $ u) Ss = insert_term t (insert_term u Ss);
+
+fun insert_terms [] Ss = Ss
+ | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss);
+
+
+
(** order-sorted algebra **)
(*
--- a/src/Pure/term_ord.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/term_ord.ML Tue Apr 18 12:23:37 2023 +0200
@@ -224,38 +224,6 @@
structure Termset = Set(Termtab.Key);
-structure Sortset:
-sig
- include SET
- val insert_typ: typ -> T -> T
- val insert_typs: typ list -> T -> T
- val insert_term: term -> T -> T
- val insert_terms: term list -> T -> T
-end =
-struct
-
-structure Set = Set(Sorttab.Key);
-open Set;
-
-fun insert_typ (TFree (_, S)) Ss = insert S Ss
- | insert_typ (TVar (_, S)) Ss = insert S Ss
- | insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss
-and insert_typs [] Ss = Ss
- | insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss);
-
-fun insert_term (Const (_, T)) Ss = insert_typ T Ss
- | insert_term (Free (_, T)) Ss = insert_typ T Ss
- | insert_term (Var (_, T)) Ss = insert_typ T Ss
- | insert_term (Bound _) Ss = Ss
- | insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss)
- | insert_term (t $ u) Ss = insert_term t (insert_term u Ss);
-
-fun insert_terms [] Ss = Ss
- | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss);
-
-end;
-
structure Var_Graph = Graph(Vartab.Key);
-structure Sort_Graph = Graph(Sorttab.Key);
structure Typ_Graph = Graph(Typtab.Key);
structure Term_Graph = Graph(Termtab.Key);
--- a/src/Pure/thm.ML Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/thm.ML Tue Apr 18 12:23:37 2023 +0200
@@ -69,7 +69,7 @@
val theory_name: thm -> string
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
- val shyps_of: thm -> Sortset.T
+ val shyps_of: thm -> sort Ord_List.T
val hyps_of: thm -> term list
val prop_of: thm -> term
val tpairs_of: thm -> (term * term) list
@@ -98,7 +98,7 @@
val join_transfer_context: Proof.context * thm -> Proof.context * thm
val renamed_prop: term -> thm -> thm
val weaken: cterm -> thm -> thm
- val weaken_sorts: Sortset.T -> cterm -> cterm
+ val weaken_sorts: sort list -> cterm -> cterm
val proof_bodies_of: thm list -> proof_body list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
@@ -108,7 +108,7 @@
val expose_proof: theory -> thm -> unit
val future: thm future -> cterm -> thm
val thm_deps: thm -> Proofterm.thm Ord_List.T
- val extra_shyps: thm -> Sortset.T
+ val extra_shyps: thm -> sort list
val strip_shyps: thm -> thm
val derivation_closed: thm -> bool
val derivation_name: thm -> string
@@ -189,7 +189,7 @@
(** certified types **)
-datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: Sortset.T};
+datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T};
fun typ_of (Ctyp {T, ...}) = T;
@@ -197,7 +197,7 @@
let
val T = Sign.certify_typ thy raw_T;
val maxidx = Term.maxidx_of_typ T;
- val sorts = Sortset.build (Sortset.insert_typ T);
+ val sorts = Sorts.insert_typ T [];
in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end;
val ctyp_of = global_ctyp_of o Proof_Context.theory_of;
@@ -219,7 +219,7 @@
val dest_ctyp1 = dest_ctypN 1;
fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
-fun insert_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sortset.merge (sorts0, sorts);
+fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);
fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs =
@@ -232,7 +232,7 @@
Ctyp {
cert = fold join_certificate_ctyp cargs cert,
maxidx = fold maxidx_ctyp cargs ~1,
- sorts = Sortset.build (fold insert_sorts_ctyp cargs),
+ sorts = fold union_sorts_ctyp cargs [],
T = if length args = length cargs then Type (a, As) else err ()}
| _ => err ())
end;
@@ -243,7 +243,7 @@
(*certified terms with checked typ, maxidx, and sorts*)
datatype cterm =
- Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: Sortset.T};
+ Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T};
exception CTERM of string * cterm list;
@@ -259,7 +259,7 @@
fun global_cterm_of thy tm =
let
val (t, T, maxidx) = Sign.certify_term thy tm;
- val sorts = Sortset.build (Sortset.insert_term t);
+ val sorts = Sorts.insert_term t [];
in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
val cterm_of = global_cterm_of o Proof_Context.theory_of;
@@ -345,7 +345,7 @@
t = f $ x,
T = rty,
maxidx = Int.max (maxidx1, maxidx2),
- sorts = Sortset.merge (sorts1, sorts2)}
+ sorts = Sorts.union sorts1 sorts2}
else raise CTERM ("apply: types don't agree", [cf, cx])
| apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);
@@ -356,7 +356,7 @@
Cterm {cert = join_certificate0 (ct1, ct2),
t = t, T = T1 --> T2,
maxidx = Int.max (maxidx1, maxidx2),
- sorts = Sortset.merge (sorts1, sorts2)}
+ sorts = Sorts.union sorts1 sorts2}
end;
fun lambda t u = lambda_name ("", t) u;
@@ -430,7 +430,7 @@
tags: Properties.T, (*additional annotations/comments*)
maxidx: int, (*maximum index of any Var or TVar*)
constraints: constraint Ord_List.T, (*implicit proof obligations for sort constraints*)
- shyps: Sortset.T, (*sort hypotheses*)
+ shyps: sort Ord_List.T, (*sort hypotheses*)
hyps: term Ord_List.T, (*hypotheses*)
tpairs: (term * term) list, (*flex-flex pairs*)
prop: term} (*conclusion*)
@@ -544,7 +544,7 @@
(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
- ||| Sortset.ord o apply2 shyps_of);
+ ||| list_ord Term_Ord.sort_ord o apply2 shyps_of);
(* implicit theory context *)
@@ -658,7 +658,7 @@
val thy = Context.certificate_theory cert
handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE);
val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
- val sorts = Sortset.merge (sorts1, sorts2);
+ val sorts = Sorts.union sorts1 sorts2;
fun mk_cTinst ((a, i), (S, T)) =
(((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts});
fun mk_ctinst ((x, i), (U, t)) =
@@ -719,17 +719,18 @@
tags = tags,
maxidx = maxidx,
constraints = constraints,
- shyps = Sortset.merge (sorts, shyps),
+ shyps = Sorts.union sorts shyps,
hyps = insert_hyps A hyps,
tpairs = tpairs,
prop = prop})
end;
-fun weaken_sorts more_sorts ct =
+fun weaken_sorts raw_sorts ct =
let
val Cterm {cert, t, T, maxidx, sorts} = ct;
val thy = theory_of_cterm ct;
- val sorts' = Sortset.fold (Sortset.insert o Sign.certify_sort thy) more_sorts sorts;
+ val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);
+ val sorts' = Sorts.union sorts more_sorts;
in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
@@ -816,7 +817,7 @@
val _ = null constraints orelse err "bad sort constraints";
val _ = null tpairs orelse err "bad flex-flex constraints";
val _ = null hyps orelse err "bad hyps";
- val _ = Sortset.subset (shyps, orig_shyps) orelse err "bad shyps";
+ val _ = Sorts.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);
in thm end;
@@ -854,7 +855,7 @@
val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop);
val cert = Context.Certificate thy;
val maxidx = maxidx_of_term prop;
- val shyps = Sortset.build (Sortset.insert_term prop);
+ val shyps = Sorts.insert_term prop [];
in
Thm (der,
{cert = cert, tags = [], maxidx = maxidx,
@@ -1019,13 +1020,13 @@
(*Dangling sort constraints of a thm*)
fun extra_shyps (th as Thm (_, {shyps, ...})) =
- Sortset.subtract (Sortset.build (fold_terms {hyps = true} Sortset.insert_term th)) shyps;
+ Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps;
(*Remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
- solve_constraints (
- if Sortset.is_empty shyps then thm
- else
+fun strip_shyps thm =
+ (case thm of
+ Thm (_, {shyps = [], ...}) => thm
+ | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) =>
let
val thy = theory_of_thm thm;
@@ -1037,29 +1038,30 @@
val present =
(fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
- val extra = fold (Sortset.remove o #2) present shyps;
- val witnessed = Sign.witness_sorts thy present (Sortset.dest extra);
- val non_witnessed =
- fold (Sortset.remove o #2) witnessed extra |> Sortset.dest |> map (`minimize);
+ val extra = fold (Sorts.remove_sort o #2) present shyps;
+ val witnessed = Sign.witness_sorts thy present extra;
+ val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
val extra' =
non_witnessed |> map_filter (fn (S, _) =>
if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S)
- |> Sortset.make;
+ |> Sorts.make;
val constrs' =
non_witnessed |> maps (fn (S1, S2) =>
- let val S0 = the (Sortset.get_first (fn S => if le (S, S1) then SOME S else NONE) extra')
+ let val S0 = the (find_first (fn S => le (S, S1)) extra')
in rel (S0, S1) @ rel (S1, S2) end);
val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints;
- val shyps' = fold (Sortset.insert o #2) present extra';
+ val shyps' = fold (Sorts.insert_sort o #2) present extra';
in
Thm (deriv_rule_unconditional
(Proofterm.strip_shyps_proof algebra present witnessed extra') der,
{cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
- end);
+ end)
+ |> solve_constraints;
+
(*** Closed theorems with official name ***)
@@ -1209,7 +1211,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = constraints,
- shyps = Sortset.merge (sorts, shyps),
+ shyps = Sorts.union sorts shyps,
hyps = remove_hyps A hyps,
tpairs = tpairs,
prop = Logic.mk_implies (A, prop)});
@@ -1236,7 +1238,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraintsA constraints,
- shyps = Sortset.merge (shypsA, shyps),
+ shyps = Sorts.union shypsA shyps,
hyps = union_hyps hypsA hyps,
tpairs = union_tpairs tpairsA tpairs,
prop = B})
@@ -1268,7 +1270,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = constraints,
- shyps = Sortset.merge (sorts, shyps),
+ shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
@@ -1297,7 +1299,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = constraints,
- shyps = Sortset.merge (sorts, shyps),
+ shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
prop = Term.betapply (A, t)})
@@ -1361,7 +1363,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
- shyps = Sortset.merge (shyps1, shyps2),
+ shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = eq $ t1 $ t2})
@@ -1433,7 +1435,7 @@
tags = [],
maxidx = maxidx,
constraints = constraints,
- shyps = Sortset.merge (sorts, shyps),
+ shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
prop = Logic.mk_equals
@@ -1473,7 +1475,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
- shyps = Sortset.merge (shyps1, shyps2),
+ shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = Logic.mk_equals (f $ t, g $ u)}))
@@ -1501,7 +1503,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
- shyps = Sortset.merge (shyps1, shyps2),
+ shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = Logic.mk_equals (A, B)})
@@ -1530,7 +1532,7 @@
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
constraints = union_constraints constraints1 constraints2,
- shyps = Sortset.merge (shyps1, shyps2),
+ shyps = Sorts.union shyps1 shyps2,
hyps = union_hyps hyps1 hyps2,
tpairs = union_tpairs tpairs1 tpairs2,
prop = B})
@@ -1644,7 +1646,7 @@
val add_instT_cert = add_cert (fn Ctyp {cert, ...} => cert);
val add_inst_cert = add_cert (fn Cterm {cert, ...} => cert);
-fun add_sorts sorts_of (_, c) sorts = Sortset.merge (sorts_of c, sorts);
+fun add_sorts sorts_of (_, c) sorts = Sorts.union (sorts_of c) sorts;
val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts);
val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts);
@@ -1811,7 +1813,7 @@
tags = [],
maxidx = maxidx_of_term prop',
constraints = [],
- shyps = Sortset.make [[]], (*potentially redundant*)
+ shyps = [[]], (*potentially redundant*)
hyps = [],
tpairs = [],
prop = prop'})
@@ -1863,7 +1865,7 @@
in
if not (null (hyps_of thm)) then
err "theorem may not contain hypotheses"
- else if not (Sortset.is_empty (extra_shyps thm)) then
+ else if not (null (extra_shyps thm)) then
err "theorem may not contain sort hypotheses"
else if not (null (tpairs_of thm)) then
err "theorem may not contain flex-flex pairs"
@@ -1899,7 +1901,7 @@
tags = [],
maxidx = maxidx + inc,
constraints = constraints,
- shyps = Sortset.merge (sorts, shyps),
+ shyps = Sorts.union shyps sorts, (*sic!*)
hyps = hyps,
tpairs = map (apply2 lift_abs) tpairs,
prop = Logic.list_implies (map lift_all As, lift_all B)})
@@ -2191,7 +2193,7 @@
{tags = [],
maxidx = Envir.maxidx_of env,
constraints = constraints',
- shyps = Envir.insert_sorts env (Sortset.merge (shyps1, shyps2)),
+ shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2),
hyps = union_hyps hyps1 hyps2,
tpairs = ntpairs,
prop = Logic.list_implies normp,