# HG changeset patch
# User wenzelm
# Date 1631195127 -7200
# Node ID ad2899cdd52801429013e89491c94134183a348b
# Parent  f084d599bb448f3d24360e030494c1cedf9dd9e6
clarified modules;

diff -r f084d599bb44 -r ad2899cdd528 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/ROOT.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -150,6 +150,7 @@
 subsection "Core of tactical proof system";
 
 ML_file "term_ord.ML";
+ML_file "term_items.ML";
 ML_file "term_subst.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
@@ -171,6 +172,7 @@
 ML_file "theory.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
+ML_file "cterm_items.ML";
 ML_file "more_pattern.ML";
 ML_file "more_unify.ML";
 ML_file "more_thm.ML";
diff -r f084d599bb44 -r ad2899cdd528 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/conv.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -81,7 +81,7 @@
 fun try_conv cv = cv else_conv all_conv;
 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
 
-fun cache_conv (cv: conv) = Thm.cterm_cache cv;
+fun cache_conv (cv: conv) = Ctermtab.cterm_cache cv;
 
 
 
diff -r f084d599bb44 -r ad2899cdd528 src/Pure/cterm_items.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/cterm_items.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -0,0 +1,38 @@
+(*  Title:      Pure/cterm_items.ML
+    Author:     Makarius
+
+Scalable collections of term items: for type thm and cterm.
+See als Pure/term_items.ML.
+*)
+
+structure Ctermtab:
+sig
+  include TABLE
+  val cterm_cache: (cterm -> 'a) -> cterm -> 'a
+end =
+struct
+
+structure Table = Table(type key = cterm val ord = Thm.fast_term_ord);
+open Table;
+
+fun cterm_cache f = Cache.create empty lookup update f;
+
+end;
+
+
+structure Thmtab:
+sig
+  include TABLE
+  val thm_cache: (thm -> 'a) -> thm -> 'a
+end =
+struct
+
+structure Table = Table(type key = thm val ord = Thm.thm_ord);
+open Table;
+
+fun thm_cache f = Cache.create empty lookup update f;
+
+end;
+
+
+structure Cterms: TERM_ITEMS = Term_Items(type key = cterm val ord = Thm.fast_term_ord);
diff -r f084d599bb44 -r ad2899cdd528 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -12,9 +12,6 @@
   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
   type attribute = Context.generic * thm -> Context.generic option * thm option
 end;
@@ -22,9 +19,6 @@
 signature THM =
 sig
   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
@@ -41,11 +35,6 @@
   val dest_equals_rhs: cterm -> cterm
   val lhs_of: thm -> cterm
   val rhs_of: thm -> cterm
-  val fast_term_ord: cterm ord
-  val term_ord: cterm ord
-  val thm_ord: thm ord
-  val cterm_cache: (cterm -> 'a) -> cterm -> 'a
-  val thm_cache: (thm -> 'a) -> thm -> 'a
   val is_reflexive: thm -> bool
   val eq_thm: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
@@ -205,37 +194,12 @@
 val rhs_of = dest_equals_rhs o Thm.cprop_of;
 
 
-(* certified term order *)
-
-val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of;
-val term_ord = Term_Ord.term_ord o apply2 Thm.term_of;
-
-
-(* thm order: ignores theory context! *)
-
-val thm_ord =
-  Term_Ord.fast_term_ord o apply2 Thm.prop_of
-  ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of
-  ||| list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of
-  ||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of;
-
-
-(* 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);
-
-fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;
-fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f;
-
-
 (* equality *)
 
 fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
   handle TERM _ => false;
 
-val eq_thm = is_equal o thm_ord;
+val eq_thm = is_equal o Thm.thm_ord;
 
 val eq_thm_prop = op aconv o apply2 Thm.full_prop_of;
 
diff -r f084d599bb44 -r ad2899cdd528 src/Pure/term_items.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_items.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -0,0 +1,193 @@
+(*  Title:      Pure/term_items.ML
+    Author:     Makarius
+
+Scalable collections of term items:
+  - table: e.g. for instantiation
+  - set with order of addition, e.g. occurrences within term
+*)
+
+signature TERM_ITEMS =
+sig
+  type key
+  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 dest: 'a table -> (key * 'a) list
+  val keys: 'a table -> key list
+  val exists: (key * 'a -> bool) -> 'a table -> bool
+  val forall: (key * 'a -> bool) -> 'a table -> bool
+  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
+  val lookup: 'a table -> key -> 'a option
+  val defined: 'a table -> key -> bool
+  val add: key * 'a -> 'a table -> 'a table
+  val make: (key * 'a) list -> 'a 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;
+
+functor Term_Items(Key: KEY): TERM_ITEMS =
+struct
+
+(* table with length *)
+
+structure Table = Table(Key);
+
+type key = Table.key;
+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;
+
+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 make entries = build (fold add entries);
+
+
+(* set with order of addition *)
+
+type set = int table;
+
+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);
+
+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;
+
+
+structure TFrees:
+sig
+  include TERM_ITEMS
+  val add_tfreesT: typ -> set -> set
+  val add_tfrees: term -> set -> set
+end =
+struct
+
+structure Items = Term_Items
+(
+  type key = string * sort;
+  val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord);
+);
+open Items;
+
+val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
+val add_tfrees = fold_types add_tfreesT;
+
+end;
+
+
+structure TVars:
+sig
+  include TERM_ITEMS
+  val add_tvarsT: typ -> set -> set
+  val add_tvars: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items(
+  type key = indexname * sort;
+  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord);
+);
+open Term_Items;
+
+val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
+val add_tvars = fold_types add_tvarsT;
+
+end;
+
+
+structure Frees:
+sig
+  include TERM_ITEMS
+  val add_frees: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+  type key = string * typ;
+  val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord);
+);
+open Term_Items;
+
+val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
+
+end;
+
+
+structure Vars:
+sig
+  include TERM_ITEMS
+  val add_vars: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+  type key = indexname * typ;
+  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
+);
+open Term_Items;
+
+val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
+
+end;
+
+
+structure Names:
+sig
+  include TERM_ITEMS
+  val add_tfree_namesT: typ -> set -> set
+  val add_tfree_names: term -> set -> set
+  val add_free_names: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+  type key = string;
+  val ord = fast_string_ord
+);
+open Term_Items;
+
+val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
+val add_tfree_names = fold_types add_tfree_namesT;
+val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
+
+end;
diff -r f084d599bb44 -r ad2899cdd528 src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/term_ord.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -2,137 +2,11 @@
     Author:     Tobias Nipkow, TU Muenchen
     Author:     Makarius
 
-Term orderings and scalable collections.
+Term orderings.
 *)
 
-signature ITEMS =
-sig
-  type key
-  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 dest: 'a table -> (key * 'a) list
-  val keys: 'a table -> key list
-  val exists: (key * 'a -> bool) -> 'a table -> bool
-  val forall: (key * 'a -> bool) -> 'a table -> bool
-  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
-  val lookup: 'a table -> key -> 'a option
-  val defined: 'a table -> key -> bool
-  val add: key * 'a -> 'a table -> 'a table
-  val make: (key * 'a) list -> 'a 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;
-
-functor Items(Key: KEY): ITEMS =
-struct
-
-(* table with length *)
-
-structure Table = Table(Key);
-
-type key = Table.key;
-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;
-
-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 make entries = build (fold add entries);
-
-
-(* set with order of addition *)
-
-type set = int table;
-
-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);
-
-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;
-
-signature BASIC_TERM_ORD =
-sig
-  structure Vartab: TABLE
-  structure Sorttab: TABLE
-  structure Typtab: TABLE
-  structure Termtab: TABLE
-  structure Var_Graph: GRAPH
-  structure Sort_Graph: GRAPH
-  structure Typ_Graph: GRAPH
-  structure Term_Graph: GRAPH
-  structure TFrees:
-  sig
-    include ITEMS
-    val add_tfreesT: typ -> set -> set
-    val add_tfrees: term -> set -> set
-  end
-  structure TVars:
-  sig
-    include ITEMS
-    val add_tvarsT: typ -> set -> set
-    val add_tvars: term -> set -> set
-  end
-  structure Frees:
-  sig
-    include ITEMS
-    val add_frees: term -> set -> set
-  end
-  structure Vars:
-  sig
-    include ITEMS
-    val add_vars: term -> set -> set
-  end
-  structure Names:
-  sig
-    include ITEMS
-    val add_tfree_namesT: typ -> set -> set
-    val add_tfree_names: term -> set -> set
-    val add_free_names: term -> set -> set
-  end
-end;
-
 signature TERM_ORD =
 sig
-  include BASIC_TERM_ORD
   val fast_indexname_ord: indexname ord
   val sort_ord: sort ord
   val typ_ord: typ ord
@@ -144,7 +18,6 @@
   val term_ord: term ord
   val hd_ord: term ord
   val term_lpo: (term -> int) -> term ord
-  val term_cache: (term -> 'a) -> term -> 'a
 end;
 
 structure Term_Ord: TERM_ORD =
@@ -326,65 +199,27 @@
 val term_lpo = term_lpo
 end;
 
+end;
+
 
 (* scalable collections *)
 
-structure Vartab = Table(type key = indexname val ord = fast_indexname_ord);
-structure Sorttab = Table(type key = sort val ord = sort_ord);
-structure Typtab = Table(type key = typ val ord = typ_ord);
-structure Termtab = Table(type key = term val ord = fast_term_ord);
-
-fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
+structure Vartab = Table(type key = indexname val ord = Term_Ord.fast_indexname_ord);
+structure Sorttab = Table(type key = sort val ord = Term_Ord.sort_ord);
+structure Typtab = Table(type key = typ val ord = Term_Ord.typ_ord);
 
-structure Var_Graph = Graph(type key = indexname val ord = fast_indexname_ord);
-structure Sort_Graph = Graph(type key = sort val ord = sort_ord);
-structure Typ_Graph = Graph(type key = typ val ord = typ_ord);
-structure Term_Graph = Graph(type key = term val ord = fast_term_ord);
-
-structure TFrees =
+structure Termtab:
+sig
+  include TABLE;
+  val term_cache: (term -> 'a) -> term -> 'a
+end =
 struct
-  structure Items =
-    Items(type key = string * sort val ord = pointer_eq_ord (prod_ord fast_string_ord sort_ord));
-  open Items;
-  val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
-  val add_tfrees = fold_types add_tfreesT;
-end;
-
-structure TVars =
-struct
-  structure Items =
-    Items(type key = indexname * sort val ord = pointer_eq_ord (prod_ord fast_indexname_ord sort_ord));
-  open Items;
-  val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
-  val add_tvars = fold_types add_tvarsT;
+  structure Table = Table(type key = term val ord = Term_Ord.fast_term_ord);
+  open Table;
+  fun term_cache f = Cache.create empty lookup update f;
 end;
 
-structure Frees =
-struct
-  structure Items =
-    Items(type key = string * typ val ord = pointer_eq_ord (prod_ord fast_string_ord typ_ord));
-  open Items;
-  val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
-end;
-
-structure Vars =
-struct
-  structure Items =
-    Items(type key = indexname * typ val ord = pointer_eq_ord (prod_ord fast_indexname_ord typ_ord));
-  open Items;
-  val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
-end;
-
-structure Names =
-struct
-  structure Items = Items(type key = string val ord = fast_string_ord);
-  open Items;
-  val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
-  val add_tfree_names = fold_types add_tfree_namesT;
-  val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
-end;
-
-end;
-
-structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
-open Basic_Term_Ord;
+structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
+structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
+structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
+structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);
diff -r f084d599bb44 -r ad2899cdd528 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/thm.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -41,6 +41,8 @@
   val global_cterm_of: theory -> term -> cterm
   val cterm_of: Proof.context -> term -> cterm
   val renamed_term: term -> cterm -> cterm
+  val fast_term_ord: cterm ord
+  val term_ord: cterm ord
   val dest_comb: cterm -> cterm * cterm
   val dest_fun: cterm -> cterm
   val dest_arg: cterm -> cterm
@@ -82,6 +84,7 @@
   val cconcl_of: thm -> cterm
   val cprems_of: thm -> cterm list
   val chyps_of: thm -> cterm list
+  val thm_ord: thm ord
   exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
   val theory_of_cterm: cterm -> theory
   val theory_of_thm: thm -> theory
@@ -269,6 +272,9 @@
   if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts}
   else raise TERM ("renamed_term: terms disagree", [t, t']);
 
+val fast_term_ord = Term_Ord.fast_term_ord o apply2 term_of;
+val term_ord = Term_Ord.term_ord o apply2 term_of;
+
 
 (* destructors *)
 
@@ -518,6 +524,15 @@
   map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
 
 
+(* thm order: ignores theory context! *)
+
+val thm_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
+  ||| list_ord Term_Ord.sort_ord o apply2 shyps_of;
+
+
 (* implicit theory context *)
 
 exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option;