New command find_consts searching for constants by type (by Timothy Bourke).

--- a/etc/isar-keywords-ZF.el	Thu Feb 12 12:35:45 2009 -0800
+++ b/etc/isar-keywords-ZF.el	Fri Feb 13 07:53:38 2009 +1100
@@ -73,6 +73,7 @@
     "extract_type"
     "finalconsts"
     "finally"
+    "find_consts"
     "find_theorems"
     "fix"
     "from"
@@ -280,6 +281,7 @@
     "disable_pr"
     "display_drafts"
     "enable_pr"
+    "find_consts"
     "find_theorems"
     "full_prf"
     "header"

--- a/etc/isar-keywords.el	Thu Feb 12 12:35:45 2009 -0800
+++ b/etc/isar-keywords.el	Fri Feb 13 07:53:38 2009 +1100
@@ -95,6 +95,7 @@
     "extract_type"
     "finalconsts"
     "finally"
+    "find_consts"
     "find_theorems"
     "fix"
     "fixpat"
@@ -346,6 +347,7 @@
     "display_drafts"
     "enable_pr"
     "export_code"
+    "find_consts"
     "find_theorems"
     "full_prf"
     "header"

--- a/lib/jedit/isabelle.xml	Thu Feb 12 12:35:45 2009 -0800
+++ b/lib/jedit/isabelle.xml	Fri Feb 13 07:53:38 2009 +1100
@@ -135,6 +135,7 @@
       <KEYWORD4>file</KEYWORD4>
       <OPERATOR>finalconsts</OPERATOR>
       <OPERATOR>finally</OPERATOR>
+      <LABEL>find_consts</LABEL>
       <LABEL>find_theorems</LABEL>
       <KEYWORD2>fix</KEYWORD2>
       <KEYWORD4>fixes</KEYWORD4>

--- a/src/Pure/IsaMakefile	Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/IsaMakefile	Fri Feb 13 07:53:38 2009 +1100
@@ -38,10 +38,10 @@
   Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
   Isar/class_target.ML Isar/code.ML Isar/code_unit.ML			\
   Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
-  Isar/expression.ML Isar/find_theorems.ML Isar/isar.ML			\
-  Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML		\
+  Isar/expression.ML Isar/find_theorems.ML Isar/find_consts.ML          \
+  Isar/isar.ML Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
   Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
-  Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
+  Isar/locale.ML Isar/method.ML Isar/net_rules.ML			\
   Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
   Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
   Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\

--- a/src/Pure/Isar/ROOT.ML	Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/ROOT.ML	Fri Feb 13 07:53:38 2009 +1100
@@ -90,5 +90,6 @@
 use "rule_insts.ML";
 use "../Thy/thm_deps.ML";
 use "find_theorems.ML";
+use "find_consts.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";

--- a/src/Pure/Isar/find_theorems.ML	Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/find_theorems.ML	Fri Feb 13 07:53:38 2009 +1100
@@ -103,21 +103,10 @@
 
 (* filter_name *)
 
-fun match_string pat str =
-  let
-    fun match [] _ = true
-      | match (p :: ps) s =
-          size p <= size s andalso
-            (case try (unprefix p) s of
-              SOME s' => match ps s'
-            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
-  in match (space_explode "*" pat) str end;
-
 fun filter_name str_pat (thmref, _) =
   if match_string str_pat (Facts.name_of_ref thmref)
   then SOME (0, 0) else NONE;
 
-
 (* filter intro/elim/dest/solves rules *)
 
 fun filter_dest ctxt goal (_, thm) =

--- a/src/Pure/Isar/isar_cmd.ML	Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Feb 13 07:53:38 2009 +1100
@@ -64,6 +64,8 @@
   val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     -> Toplevel.transition -> Toplevel.transition
+  val find_consts: (bool * FindConsts.criterion) list ->
+                   Toplevel.transition -> Toplevel.transition
   val unused_thms: (string list * string list option) option ->
     Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
@@ -432,6 +434,12 @@
     |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
   end);
 
+(* retrieve constants *)
+
+fun find_consts spec =
+  Toplevel.unknown_theory o Toplevel.keep (fn state =>
+  let val ctxt = (Proof.context_of o Toplevel.enter_proof_body) state
+  in FindConsts.find_consts ctxt spec end);
 
 (* print proof context contents *)
 

--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 13 07:53:38 2009 +1100
@@ -878,6 +878,22 @@
 
 end;
 
+local
+
+val criterion =
+  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Strict ||
+  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Name ||
+  P.xname >> FindConsts.Loose;
+
+in
+
+val _ =
+  OuterSyntax.improper_command "find_consts" "search constants by type pattern"
+    K.diag (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+            >> (Toplevel.no_timing oo IsarCmd.find_consts));
+
+end;
+
 val _ =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));

--- a/src/Pure/library.ML	Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/library.ML	Fri Feb 13 07:53:38 2009 +1100
@@ -159,6 +159,7 @@
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
   val multiply: 'a list -> 'a list list -> 'a list list
+  val match_string: string -> string -> bool
 
   (*lists as sets -- see also Pure/General/ord_list.ML*)
   val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
@@ -554,7 +555,6 @@
 fun multiply [] _ = []
   | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
 
-
 (* direct product *)
 
 fun map_product f _ [] = []
@@ -787,7 +787,16 @@
       if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
       else replicate_string (k div 2) (a ^ a) ^ a;
 
-
+(*crude matching of str against simple glob pat*)
+fun match_string pat str =
+  let
+    fun match [] _ = true
+      | match (p :: ps) s =
+          size p <= size s andalso
+            (case try (unprefix p) s of
+              SOME s' => match ps s'
+            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
+  in match (space_explode "*" pat) str end;
 
 (** lists as sets -- see also Pure/General/ord_list.ML **)
 

--- a/src/Pure/term.ML	Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/term.ML	Fri Feb 13 07:53:38 2009 +1100
@@ -64,6 +64,7 @@
   val strip_comb: term -> term * term list
   val head_of: term -> term
   val size_of_term: term -> int
+  val size_of_typ: typ -> int
   val map_atyps: (typ -> typ) -> typ -> typ
   val map_aterms: (term -> term) -> term -> term
   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
@@ -391,6 +392,13 @@
       | add_size (_, n) = n + 1;
   in add_size (tm, 0) end;
 
+(*number of tfrees, tvars, and constructors in a type*)
+fun size_of_typ ty =
+  let
+    fun add_size (Type (_, ars), n) = foldl add_size (n + 1) ars
+      | add_size (_, n) = n + 1;
+  in add_size (ty, 0) end;
+
 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   | map_atyps f T = f T;