src/Doc/Isar_Ref/Misc.thy
 author wenzelm Wed Mar 25 11:39:52 2015 +0100 (2015-03-25) changeset 59809 87641097d0f3 parent 58618 782f0b662cae child 59917 9830c944670f permissions -rw-r--r--
tuned signature;
     1 theory Misc

     2 imports Base Main

     3 begin

     4

     5 chapter \<open>Other commands\<close>

     6

     7 section \<open>Inspecting the context\<close>

     8

     9 text \<open>

    10   \begin{matharray}{rcl}

    11     @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    12     @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    13     @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    14     @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    15     @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    16     @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    17     @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    18     @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    19     @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    20     @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

    21   \end{matharray}

    22

    23   @{rail \<open>

    24     (@@{command print_theory} | @@{command print_theorems} | @@{command print_facts}) ('!'?)

    25     ;

    26

    27     @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )

    28     ;

    29     thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |

    30       'solves' | 'simp' ':' @{syntax term} | @{syntax term})

    31     ;

    32     @@{command find_consts} (constcriterion * )

    33     ;

    34     constcriterion: ('-'?)

    35       ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})

    36     ;

    37     @@{command thm_deps} @{syntax thmrefs}

    38     ;

    39     @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?

    40   \<close>}

    41

    42   These commands print certain parts of the theory and proof context.

    43   Note that there are some further ones available, such as for the set

    44   of rules declared for simplifications.

    45

    46   \begin{description}

    47

    48   \item @{command "print_theory"} prints the main logical content of

    49   the background theory; the @{text "!"}'' option indicates extra

    50   verbosity.

    51

    52   \item @{command "print_methods"} prints all proof methods

    53   available in the current theory context.

    54

    55   \item @{command "print_attributes"} prints all attributes

    56   available in the current theory context.

    57

    58   \item @{command "print_theorems"} prints theorems of the background

    59   theory resulting from the last command; the @{text "!"}'' option

    60   indicates extra verbosity.

    61

    62   \item @{command "print_facts"} prints all local facts of the

    63   current context, both named and unnamed ones; the @{text "!"}''

    64   option indicates extra verbosity.

    65

    66   \item @{command "print_term_bindings"} prints all term bindings that

    67   are present in the context.

    68

    69   \item @{command "find_theorems"}~@{text criteria} retrieves facts

    70   from the theory or proof context matching all of given search

    71   criteria.  The criterion @{text "name: p"} selects all theorems

    72   whose fully qualified name matches pattern @{text p}, which may

    73   contain @{text "*"}'' wildcards.  The criteria @{text intro},

    74   @{text elim}, and @{text dest} select theorems that match the

    75   current goal as introduction, elimination or destruction rules,

    76   respectively.  The criterion @{text "solves"} returns all rules

    77   that would directly solve the current goal.  The criterion

    78   @{text "simp: t"} selects all rewrite rules whose left-hand side

    79   matches the given term.  The criterion term @{text t} selects all

    80   theorems that contain the pattern @{text t} -- as usual, patterns

    81   may contain occurrences of the dummy @{text _}'', schematic

    82   variables, and type constraints.

    83

    84   Criteria can be preceded by @{text "-"}'' to select theorems that

    85   do \emph{not} match. Note that giving the empty list of criteria

    86   yields \emph{all} currently known facts.  An optional limit for the

    87   number of printed facts may be given; the default is 40.  By

    88   default, duplicates are removed from the search result. Use

    89   @{text with_dups} to display duplicates.

    90

    91   \item @{command "find_consts"}~@{text criteria} prints all constants

    92   whose type meets all of the given criteria. The criterion @{text

    93   "strict: ty"} is met by any type that matches the type pattern

    94   @{text ty}.  Patterns may contain both the dummy type @{text _}''

    95   and sort constraints. The criterion @{text ty} is similar, but it

    96   also matches against subtypes. The criterion @{text "name: p"} and

    97   the prefix @{text "-"}'' function as described for @{command

    98   "find_theorems"}.

    99

   100   \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}

   101   visualizes dependencies of facts, using Isabelle's graph browser

   102   tool (see also @{cite "isabelle-sys"}).

   103

   104   \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}

   105   displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}

   106   or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and

   107   that are never used.

   108   If @{text n} is @{text 0}, the end of the range of theories

   109   defaults to the current theory. If no range is specified,

   110   only the unused theorems in the current theory are displayed.

   111

   112   \end{description}

   113 \<close>

   114

   115 end