# HG changeset patch
# User wenzelm
# Date 1116773471 -7200
# Node ID 66561f6814bdb9ddafc38e08e1aa8ef75b32d162
# Parent  96a9bf7ac18df0bafa60b9a37392b04e601fc4a9
added string_of_thmref, selections, fact_index_of, valid_thms;
moved find_matching_thms, is_matching_thm, find_intros/intros_goal/elims to Isar/find_theorems.ML;
tuned

diff -r 96a9bf7ac18d -r 66561f6814bd src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun May 22 16:51:10 2005 +0200
+++ b/src/Pure/pure_thy.ML	Sun May 22 16:51:11 2005 +0200
@@ -14,7 +14,6 @@
   val get_thms: theory -> thmref -> thm list
   val get_thmss: theory -> thmref list -> thm list
   val thms_of: theory -> (string * thm) list
-  val thms_with_names_of: theory -> (string * thm list) list
   structure ProtoPure:
     sig
       val thy: theory
@@ -26,21 +25,17 @@
 sig
   include BASIC_PURE_THY
   datatype interval = FromTo of int * int | From of int | Single of int
+  val string_of_thmref: thmref -> string
   val get_thm_closure: theory -> thmref -> thm
   val get_thms_closure: theory -> thmref -> thm list
   val single_thm: string -> thm list -> thm
   val select_thm: thmref -> thm list -> thm list
+  val selections: string * thm list -> (thmref * thm) list
   val cond_extern_thm_sg: Sign.sg -> string -> xstring
-  val thms_containing: theory -> string list * string list -> (string * thm list) list
-  val find_theorems: ('a * 'b list) list -> ('a * 'b -> bool) list -> ('a * 'b list) list
+  val fact_index_of: theory -> FactIndex.T
+  val valid_thms: theory -> thmref * thm list -> bool
+  val thms_containing: theory -> FactIndex.spec -> (string * thm list) list
   val thms_containing_consts: theory -> string list -> (string * thm) list
-  val find_matching_thms: (thm -> thm list) * (term -> term)
-        -> theory -> term -> (string * thm) list
-  val is_matching_thm: (thm -> thm list) * (term -> term)
-        -> Sign.sg -> term -> (string * thm) -> bool
-  val find_intros: theory -> term -> (string * thm) list
-  val find_intros_goal : theory -> thm -> int -> (string * thm) list
-  val find_elims : theory -> term -> (string * thm) list
   val hide_thms: bool -> string list -> theory -> theory
   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
   val smart_store_thms: (bstring * thm list) -> thm list
@@ -106,25 +101,25 @@
 
   type T =
     {space: NameSpace.T,
-      thms_tab: thm list Symtab.table,
+      theorems: thm list Symtab.table,
       index: FactIndex.T} ref;
 
   fun mk_empty _ =
-    ref {space = NameSpace.empty, thms_tab = Symtab.empty, index = FactIndex.empty}: T;
+    ref {space = NameSpace.empty, theorems = Symtab.empty, index = FactIndex.empty}: T;
 
   val empty = mk_empty ();
   fun copy (ref x) = ref x;
   val prep_ext = mk_empty;
   val merge = mk_empty;
 
-  fun pretty sg (ref {space, thms_tab, index = _}) =
+  fun pretty sg (ref {space, theorems, index = _}) =
     let
       val prt_thm = Display.pretty_thm_sg sg;
       fun prt_thms (name, [th]) =
             Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
         | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
 
-      val thmss = NameSpace.cond_extern_table space thms_tab;
+      val thmss = NameSpace.cond_extern_table space theorems;
     in Pretty.big_list "theorems:" (map prt_thms thmss) end;
 
   fun print sg data = Pretty.writeln (pretty sg data);
@@ -135,6 +130,8 @@
 val get_theorems = TheoremsData.get;
 
 val cond_extern_thm_sg = NameSpace.cond_extern o #space o ! o get_theorems_sg;
+val fact_index_of = #index o ! o get_theorems;
+
 
 
 (* print theory *)
@@ -157,35 +154,50 @@
   | single_thm name _ = error ("Single theorem expected " ^ quote name);
 
 
-(* selections *)
+(* datatype interval *)
 
 datatype interval =
   FromTo of int * int |
   From of int |
   Single of int;
 
-type thmref = xstring * interval list option;
-
-local
-
 fun interval _ (FromTo (i, j)) = i upto j
   | interval n (From i) = i upto n
   | interval _ (Single i) = [i];
 
-fun select name thms n i =
-  if i < 1 orelse i > n then
-    error ("Bad subscript " ^ string_of_int i ^ " for " ^
-      quote name ^ " (length " ^ string_of_int n ^ ")")
-  else List.nth (thms, i - 1);
+fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
+  | string_of_interval (From i) = string_of_int i ^ "-"
+  | string_of_interval (Single i) = string_of_int i;
+
+
+(* type thmref *)
 
-in
+type thmref = xstring * interval list option;
+
+fun string_of_thmref (name, NONE) = name
+  | string_of_thmref (name, SOME is) =
+      name ^ enclose "(" ")" (commas (map string_of_interval is));
+
+
+(* select_thm *)
 
 fun select_thm (_, NONE) thms = thms
   | select_thm (name, SOME is) thms =
-      let val n = length thms
-      in map (select name thms n) (List.concat (map (interval n) is)) end;
+      let
+        val n = length thms;
+        fun select i =
+          if i < 1 orelse i > n then
+            error ("Bad subscript " ^ string_of_int i ^ " for " ^
+              quote name ^ " (length " ^ string_of_int n ^ ")")
+          else List.nth (thms, i - 1);
+      in map select (List.concat (map (interval n) is)) end;
 
-end;
+
+(* selections *)
+
+fun selections (name, [thm]) = [((name, NONE), thm)]
+  | selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) =>
+      ((name, SOME [Single i]), thm));
 
 
 (* get_thm(s)_closure -- statically scoped versions *)
@@ -195,11 +207,11 @@
 fun lookup_thms thy =
   let
     val sg_ref = Sign.self_ref (Theory.sign_of thy);
-    val ref {space, thms_tab, ...} = get_theorems thy;
+    val ref {space, theorems, ...} = get_theorems thy;
   in
     fn name =>
       Option.map (map (Thm.transfer_sg (Sign.deref sg_ref)))        (*semi-dynamic identity*)
-      (Symtab.lookup (thms_tab, NameSpace.intern space name))   (*static content*)
+      (Symtab.lookup (theorems, NameSpace.intern space name))   (*static content*)
   end;
 
 fun get_thms_closure thy =
@@ -223,135 +235,33 @@
 fun get_thm thy (namei as (name, _)) = single_thm name (get_thms thy namei);
 
 
-(* thms_of *)
+(* thms_containing etc. *)
 
-fun thms_of thy =
-  let val ref {thms_tab, ...} = get_theorems thy in
-    map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms_tab)))
-  end;
-
-(* thms_with_names_of - theorems in this theory and their names *)
-fun thms_with_names_of thy = 
-  TheoremsData.get thy |> ! |> #index |> FactIndex.find ([],[]);
-  (* looking for nothing in a FactIndex finds everything, i.e. all theorems *)
+fun valid_thms thy (thmref, ths) =
+  (case try (transform_error (get_thms thy)) thmref of
+    NONE => false
+  | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths'));
 
-(* thms_containing *)
-
-fun thms_containing thy idx =
-  let
-    fun valid (name, ths) =
-      (case try (transform_error (get_thms thy)) (name, NONE) of
-        NONE => false
-      | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths'));
-  in
-    (thy :: Theory.ancestors_of thy)
-    |> map (gen_distinct eq_fst o List.filter valid o FactIndex.find idx o #index o ! o get_theorems)
-    |> List.concat
-  end;
+fun thms_containing theory spec =
+  (theory :: Theory.ancestors_of theory)
+  |> map (fn thy =>
+      FactIndex.find (fact_index_of thy) spec
+      |> List.filter (fn (name, ths) => valid_thms theory ((name, NONE), ths))
+      |> gen_distinct eq_fst)
+  |> List.concat;
 
 fun thms_containing_consts thy consts =
   thms_containing thy (consts, []) |> map #2 |> List.concat
-  |> map (fn th => (Thm.name_of_thm th, th))
+  |> map (fn th => (Thm.name_of_thm th, th));
 
-(* Searching based on filters *)
-(* a filter must only take a (name:string, theorem:Thm.thm) and return true
-   if it finds a match, false if it doesn't *)
 
-(* given facts and filters, find all facts in which at least one theorem 
-   matches on ALL filters *)
-fun find_theorems facts filters =
-  let
-    (* break fact up into theorems, but associate them with the name of this 
-       fact, so that filters looking by name will only consider the fact's
-       name *)
-    fun fact_to_names_thms (name, thms) =
-      map (fn thm => (name, thm)) thms;
+(* thms_of *)
 
-    (* all filters return true when applied to a named theorem *)
-    fun match_all_filters filters name_thm =
-      List.all (fn filter => filter name_thm) filters;
-
-    (* at least one theorem in this fact which matches all filters *)
-    fun fact_matches_filters filters fact =
-      List.exists (match_all_filters filters) (fact_to_names_thms fact);
-
-    fun matches x = (fact_matches_filters filters x)
-  in
-    List.filter matches facts
+fun thms_of thy =
+  let val ref {theorems, ...} = get_theorems thy in
+    map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest theorems)))
   end;
 
-(* intro/elim theorems *)
-
-(* intro: given a goal state, find a suitable intro rule for some subgoal *)
-(* elim: given a theorem thm,
-         find a theorem whose major premise eliminates the conclusion of thm *)
-
-fun top_const t = (case head_of t of Const (c, _) => SOME c | _ => NONE);
-
-(* This is a hack to remove the Trueprop constant that most logics use *)
-fun rem_top (_ $ t) = t
-  | rem_top _ = Bound 0 (* does not match anything *)
-
-(*returns all those named_thms whose subterm extracted by extract can be
-  instantiated to obj; the list is sorted according to the number of premises
-  and the size of the required substitution.*)
-fun select_match(c,obj, signobj, named_thms, (extract_thms,extract_term)) =
-  let val tsig = Sign.tsig_of signobj
-      fun matches prop =
-        let val pat = extract_term prop
-        in case head_of pat of
-             Const(d,_) => c=d andalso Pattern.matches tsig (pat,obj)
-           | _ => false
-        end
-
-      fun substsize prop =
-            let val pat = extract_term prop
-                val (_,subst) = Pattern.match tsig (pat,obj)
-            in Vartab.foldl (op + o apsnd (size_of_term o snd o snd)) (0, subst)
-            end
-
-      fun thm_ord ((p0,s0,_),(p1,s1,_)) =
-            prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
-
-      fun select((p as (_,thm))::named_thms, sels) =
-            let
-              fun sel(thm::thms,sels) =     
-                    let val {prop, ...} = rep_thm thm
-                    in if matches prop
-                       then (nprems_of thm,substsize prop,p)::sels
-                       else sel(thms,sels)
-                    end
-                | sel([],sels) = sels
-             val {sign, ...} = rep_thm thm
-           in select(named_thms,if Sign.subsig(sign, signobj)
-                                then sel(extract_thms thm,sels)
-                                else sels)
-           end
-        | select([],sels) = sels
-
-  in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
-
-(* like find_matching_thms, but for one named theorem only *)
-fun is_matching_thm extract sg prop name_thm =
-  (case top_const prop of NONE => false
-   | SOME c => 
-      not ([] = select_match(c,prop, sg,[name_thm],extract)));
-
-
-fun find_matching_thms extract thy prop =
-  (case top_const prop of NONE => []
-   | SOME c => let val thms = thms_containing_consts thy [c]
-               in select_match(c,prop,Theory.sign_of thy,thms,extract) end)
-
-val find_intros =
-  find_matching_thms (single, rem_top o Logic.strip_imp_concl)
-
-fun find_intros_goal thy st i =
-  find_intros thy (rem_top(Logic.concl_of_goal (prop_of st) i));
-
-val find_elims = find_matching_thms
-  (fn thm => if Thm.no_prems thm then [] else [thm],
-   rem_top o hd o Logic.strip_imp_prems)
 
 
 (** store theorems **)                    (*DESTRUCTIVE*)
@@ -360,9 +270,9 @@
 
 fun hide_thms fully names thy =
   let
-    val r as ref {space, thms_tab, index} = get_theorems thy;
+    val r as ref {space, theorems, index} = get_theorems thy;
     val space' = NameSpace.hide fully (space, names);
-  in r := {space = space', thms_tab = thms_tab, index = index}; thy end;
+  in r := {space = space', theorems = theorems, index = index}; thy end;
 
 
 (* naming *)
@@ -396,22 +306,23 @@
         val (thy', thms') = app_att (thy, pre_name name thms);
         val named_thms = post_name name thms';
 
-        val r as ref {space, thms_tab, index} = get_theorems_sg sg;
+        val r as ref {space, theorems, index} = get_theorems_sg sg;
         val space' = NameSpace.extend' acc (space, [name]);
-        val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
-        val index' = FactIndex.add (K false) (index, (name, named_thms));
+        val theorems' = Symtab.update ((name, named_thms), theorems);
+        val index' = FactIndex.add (K false) (name, named_thms) index;
       in
-        (case Symtab.lookup (thms_tab, name) of
+        (case Symtab.lookup (theorems, name) of
           NONE => ()
         | SOME thms' =>
             if Library.equal_lists Thm.eq_thm (thms', named_thms) then warn_same name
             else warn_overwrite name);
-        r := {space = space', thms_tab = thms_tab', index = index'};
+        r := {space = space', theorems = theorems', index = index'};
         (thy', named_thms)
       end;
 
 fun enter_thms sg = gen_enter_thms Sign.full_name NameSpace.accesses sg;
 
+
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((bname, thms), atts) thy =
@@ -445,18 +356,13 @@
 
 in
 
-(* if path is set, only permit unqualified names *)
-
+(*if path is set, only permit unqualified names*)
 val note_thmss = gen_note_thmss enter_thms get_thms;
 val note_thmss_i = gen_note_thmss enter_thms (K I);
 
-(* always permit qualified names,
-   clients may specify non-standard access policy *)
-
-fun note_thmss_accesses acc =
-  gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms;
-fun note_thmss_accesses_i acc =
-  gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I);
+(*always permit qualified names, clients may specify non-standard access policy*)
+fun note_thmss_accesses acc = gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms;
+fun note_thmss_accesses_i acc = gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I);
 
 end;
 
@@ -615,15 +521,11 @@
 
 (*** the ProtoPure theory ***)
 
-
-(*It might make sense to restrict the polymorphism of the constant "==" to
-  sort logic, instead of the universal sort, {}.  Unfortunately, this change
-  causes HOL/Import/shuffler.ML to fail.*)
-
 val proto_pure =
   Theory.pre_pure
-  |> Library.apply [TheoremsData.init, TheoryManagementData.init, Proofterm.init]
-  |> put_name "ProtoPure"
+  |> TheoryManagementData.init |> put_name "ProtoPure"
+  |> TheoremsData.init
+  |> Proofterm.init
   |> global_path
   |> Theory.add_types
    [("fun", 2, NoSyn),
@@ -666,10 +568,7 @@
   val Goal_def = get_axiom thy "Goal_def";
 end;
 
-
 end;
 
-
 structure BasicPureThy: BASIC_PURE_THY = PureThy;
 open BasicPureThy;
-