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