# HG changeset patch
# User wenzelm
# Date 1128437260 -7200
# Node ID b0cd55afead18fce747466f2fe74541bd5388b7e
# Parent  58a306d9f7363052ef201e7e6c31fe67bdfcb953
find_theorems: support * wildcard in name: criterion;

diff -r 58a306d9f736 -r b0cd55afead1 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Oct 04 16:47:39 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Oct 04 16:47:40 2005 +0200
@@ -1425,7 +1425,7 @@
 \indexisarcmd{print-facts}\indexisarcmd{print-binds}
 \indexisarcmd{print-commands}\indexisarcmd{print-syntax}
 \indexisarcmd{print-methods}\indexisarcmd{print-attributes}
-\indexisarcmd{thms-containing}\indexisarcmd{thm-deps}
+\indexisarcmd{find-theorems}\indexisarcmd{thm-deps}
 \indexisarcmd{print-theorems}
 \begin{matharray}{rcl}
   \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
@@ -1433,25 +1433,19 @@
   \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\
-  \isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{find_theorems}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_facts}^* & : & \isarkeep{proof} \\
   \isarcmd{print_binds}^* & : & \isarkeep{proof} \\
 \end{matharray}
 
-\railalias{thmscontaining}{thms\_containing}
-\railterm{thmscontaining}
-
-\railalias{thmdeps}{thm\_deps}
-\railterm{thmdeps}
-
 \begin{rail}
-  thmscontaining (('(' nat ')')?) (criterion *)
+  'find\_theorems' (('(' nat ')')?) (criterion *)
   ;
   criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
     'simp' ':' term | term)
   ;
-  thmdeps thmrefs
+  'thm\_deps' thmrefs
   ;
 \end{rail}
 
@@ -1482,16 +1476,16 @@
   transaction; this allows to inspect the result of advanced definitional
   packages, such as $\isarkeyword{datatype}$.
   
-\item [$\isarkeyword{thms_containing}~\vec c$] retrieves facts from the theory
-  or proof context matching all of the search criteria $\vec c$.  The criterion
-  $name: s$ selects all theorems that contain $s$ in their fully qualified
-  name.  The criteria $intro$, $elim$, and $dest$ select theorems that match
-  the current goal as introduction, elimination or destruction rules,
-  respectively.  The criterion $simp: t$ selects all rewrite rules whose
-  left-hand side matches the given term.  The criterion term $t$ selects all
-  theorems that contain the pattern $t$ -- as usual, patterns may contain
-  occurrences of the dummy ``$\_$'', schematic variables, and type
-  constraints.
+\item [$\isarkeyword{find_theorems}~\vec c$] retrieves facts from the theory
+  or proof context matching all of the search criteria $\vec c$.  The
+  criterion $name: p$ selects all theorems whose fully qualified name matches
+  pattern $p$, which may contain ``$*$'' wildcards.  The criteria $intro$,
+  $elim$, and $dest$ select theorems that match the current goal as
+  introduction, elimination or destruction rules, respectively.  The criterion
+  $simp: t$ selects all rewrite rules whose left-hand side matches the given
+  term.  The criterion term $t$ selects all theorems that contain the pattern
+  $t$ -- as usual, patterns may contain occurrences of the dummy ``$\_$'',
+  schematic variables, and type constraints.
   
   Criteria can be preceded by ``$-$'' to select theorems that do \emph{not}
   match. Note that giving the empty list of criteria yields \emph{all}
diff -r 58a306d9f736 -r b0cd55afead1 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Tue Oct 04 16:47:39 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Tue Oct 04 16:47:40 2005 +0200
@@ -109,16 +109,20 @@
 
 (* filter_name *)
 
-fun is_substring pat str =
-  if String.size pat = 0 then true
-  else if String.size pat > String.size str then false
-  else if String.substring (str, 0, String.size pat) = pat then true
-  else is_substring pat (String.extract (str, 1, NONE));
+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;
 
 (*filter that just looks for a string in the name,
   substring match only (no regexps are performed)*)
 fun filter_name str_pat (thmref, _) =
-  if is_substring str_pat (PureThy.name_of_thmref thmref)
+  if match_string str_pat (PureThy.name_of_thmref thmref)
   then SOME (0, 0) else NONE;