1.1 --- a/etc/isar-keywords-ZF.el	Thu Feb 12 12:35:45 2009 -0800
     1.2 +++ b/etc/isar-keywords-ZF.el	Fri Feb 13 07:53:38 2009 +1100
     1.3 @@ -73,6 +73,7 @@
     1.4      "extract_type"
     1.5      "finalconsts"
     1.6      "finally"
     1.7 +    "find_consts"
     1.8      "find_theorems"
     1.9      "fix"
    1.10      "from"
    1.11 @@ -280,6 +281,7 @@
    1.12      "disable_pr"
    1.13      "display_drafts"
    1.14      "enable_pr"
    1.15 +    "find_consts"
    1.16      "find_theorems"
    1.17      "full_prf"
    1.18      "header"

     2.1 --- a/etc/isar-keywords.el	Thu Feb 12 12:35:45 2009 -0800
     2.2 +++ b/etc/isar-keywords.el	Fri Feb 13 07:53:38 2009 +1100
     2.3 @@ -95,6 +95,7 @@
     2.4      "extract_type"
     2.5      "finalconsts"
     2.6      "finally"
     2.7 +    "find_consts"
     2.8      "find_theorems"
     2.9      "fix"
    2.10      "fixpat"
    2.11 @@ -346,6 +347,7 @@
    2.12      "display_drafts"
    2.13      "enable_pr"
    2.14      "export_code"
    2.15 +    "find_consts"
    2.16      "find_theorems"
    2.17      "full_prf"
    2.18      "header"

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

     4.1 --- a/src/Pure/IsaMakefile	Thu Feb 12 12:35:45 2009 -0800
     4.2 +++ b/src/Pure/IsaMakefile	Fri Feb 13 07:53:38 2009 +1100
     4.3 @@ -38,10 +38,10 @@
     4.4    Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
     4.5    Isar/class_target.ML Isar/code.ML Isar/code_unit.ML			\
     4.6    Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
     4.7 -  Isar/expression.ML Isar/find_theorems.ML Isar/isar.ML			\
     4.8 -  Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML		\
     4.9 +  Isar/expression.ML Isar/find_theorems.ML Isar/find_consts.ML          \
    4.10 +  Isar/isar.ML Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
    4.11    Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
    4.12 -  Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
    4.13 +  Isar/locale.ML Isar/method.ML Isar/net_rules.ML			\
    4.14    Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
    4.15    Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
    4.16    Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\

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

     6.1 --- a/src/Pure/Isar/find_theorems.ML	Thu Feb 12 12:35:45 2009 -0800
     6.2 +++ b/src/Pure/Isar/find_theorems.ML	Fri Feb 13 07:53:38 2009 +1100
     6.3 @@ -103,21 +103,10 @@
     6.4  
     6.5  (* filter_name *)
     6.6  
     6.7 -fun match_string pat str =
     6.8 -  let
     6.9 -    fun match [] _ = true
    6.10 -      | match (p :: ps) s =
    6.11 -          size p <= size s andalso
    6.12 -            (case try (unprefix p) s of
    6.13 -              SOME s' => match ps s'
    6.14 -            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
    6.15 -  in match (space_explode "*" pat) str end;
    6.16 -
    6.17  fun filter_name str_pat (thmref, _) =
    6.18    if match_string str_pat (Facts.name_of_ref thmref)
    6.19    then SOME (0, 0) else NONE;
    6.20  
    6.21 -
    6.22  (* filter intro/elim/dest/solves rules *)
    6.23  
    6.24  fun filter_dest ctxt goal (_, thm) =

     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Feb 12 12:35:45 2009 -0800
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Feb 13 07:53:38 2009 +1100
     7.3 @@ -64,6 +64,8 @@
     7.4    val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
     7.5    val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     7.6      -> Toplevel.transition -> Toplevel.transition
     7.7 +  val find_consts: (bool * FindConsts.criterion) list ->
     7.8 +                   Toplevel.transition -> Toplevel.transition
     7.9    val unused_thms: (string list * string list option) option ->
    7.10      Toplevel.transition -> Toplevel.transition
    7.11    val print_binds: Toplevel.transition -> Toplevel.transition
    7.12 @@ -432,6 +434,12 @@
    7.13      |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
    7.14    end);
    7.15  
    7.16 +(* retrieve constants *)
    7.17 +
    7.18 +fun find_consts spec =
    7.19 +  Toplevel.unknown_theory o Toplevel.keep (fn state =>
    7.20 +  let val ctxt = (Proof.context_of o Toplevel.enter_proof_body) state
    7.21 +  in FindConsts.find_consts ctxt spec end);
    7.22  
    7.23  (* print proof context contents *)
    7.24  

     8.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Feb 12 12:35:45 2009 -0800
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 13 07:53:38 2009 +1100
     8.3 @@ -878,6 +878,22 @@
     8.4  
     8.5  end;
     8.6  
     8.7 +local
     8.8 +
     8.9 +val criterion =
    8.10 +  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Strict ||
    8.11 +  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Name ||
    8.12 +  P.xname >> FindConsts.Loose;
    8.13 +
    8.14 +in
    8.15 +
    8.16 +val _ =
    8.17 +  OuterSyntax.improper_command "find_consts" "search constants by type pattern"
    8.18 +    K.diag (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    8.19 +            >> (Toplevel.no_timing oo IsarCmd.find_consts));
    8.20 +
    8.21 +end;
    8.22 +
    8.23  val _ =
    8.24    OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
    8.25      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));

     9.1 --- a/src/Pure/library.ML	Thu Feb 12 12:35:45 2009 -0800
     9.2 +++ b/src/Pure/library.ML	Fri Feb 13 07:53:38 2009 +1100
     9.3 @@ -159,6 +159,7 @@
     9.4    val replicate_string: int -> string -> string
     9.5    val translate_string: (string -> string) -> string -> string
     9.6    val multiply: 'a list -> 'a list list -> 'a list list
     9.7 +  val match_string: string -> string -> bool
     9.8  
     9.9    (*lists as sets -- see also Pure/General/ord_list.ML*)
    9.10    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    9.11 @@ -554,7 +555,6 @@
    9.12  fun multiply [] _ = []
    9.13    | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
    9.14  
    9.15 -
    9.16  (* direct product *)
    9.17  
    9.18  fun map_product f _ [] = []
    9.19 @@ -787,7 +787,16 @@
    9.20        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
    9.21        else replicate_string (k div 2) (a ^ a) ^ a;
    9.22  
    9.23 -
    9.24 +(*crude matching of str against simple glob pat*)
    9.25 +fun match_string pat str =
    9.26 +  let
    9.27 +    fun match [] _ = true
    9.28 +      | match (p :: ps) s =
    9.29 +          size p <= size s andalso
    9.30 +            (case try (unprefix p) s of
    9.31 +              SOME s' => match ps s'
    9.32 +            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
    9.33 +  in match (space_explode "*" pat) str end;
    9.34  
    9.35  (** lists as sets -- see also Pure/General/ord_list.ML **)
    9.36  

    10.1 --- a/src/Pure/term.ML	Thu Feb 12 12:35:45 2009 -0800
    10.2 +++ b/src/Pure/term.ML	Fri Feb 13 07:53:38 2009 +1100
    10.3 @@ -64,6 +64,7 @@
    10.4    val strip_comb: term -> term * term list
    10.5    val head_of: term -> term
    10.6    val size_of_term: term -> int
    10.7 +  val size_of_typ: typ -> int
    10.8    val map_atyps: (typ -> typ) -> typ -> typ
    10.9    val map_aterms: (term -> term) -> term -> term
   10.10    val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
   10.11 @@ -391,6 +392,13 @@
   10.12        | add_size (_, n) = n + 1;
   10.13    in add_size (tm, 0) end;
   10.14  
   10.15 +(*number of tfrees, tvars, and constructors in a type*)
   10.16 +fun size_of_typ ty =
   10.17 +  let
   10.18 +    fun add_size (Type (_, ars), n) = foldl add_size (n + 1) ars
   10.19 +      | add_size (_, n) = n + 1;
   10.20 +  in add_size (ty, 0) end;
   10.21 +
   10.22  fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   10.23    | map_atyps f T = f T;
   10.24