clarified sections;
authorwenzelm
Mon Jul 06 20:13:51 2015 +0200 (2015-07-06)
changeset 606742f66099fb472
parent 60673 91d36d6a6a88
child 60675 a997fcb75d08
clarified sections;
src/Doc/Isar_Ref/Misc.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Doc/Isar_Ref/document/root.tex
src/Doc/ROOT
     1.1 --- a/src/Doc/Isar_Ref/Misc.thy	Mon Jul 06 20:07:41 2015 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,119 +0,0 @@
     1.4 -theory Misc
     1.5 -imports Base Main
     1.6 -begin
     1.7 -
     1.8 -chapter \<open>Other commands\<close>
     1.9 -
    1.10 -section \<open>Inspecting the context\<close>
    1.11 -
    1.12 -text \<open>
    1.13 -  \begin{matharray}{rcl}
    1.14 -    @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.15 -    @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.16 -    @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.17 -    @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.18 -    @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.19 -    @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.20 -    @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.21 -    @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.22 -    @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.23 -    @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.24 -  \end{matharray}
    1.25 -
    1.26 -  @{rail \<open>
    1.27 -    (@@{command print_theory} |
    1.28 -      @@{command print_methods} |
    1.29 -      @@{command print_attributes} |
    1.30 -      @@{command print_theorems} |
    1.31 -      @@{command print_facts}) ('!'?)
    1.32 -    ;
    1.33 -    @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
    1.34 -    ;
    1.35 -    thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
    1.36 -      'solves' | 'simp' ':' @{syntax term} | @{syntax term})
    1.37 -    ;
    1.38 -    @@{command find_consts} (const_criterion*)
    1.39 -    ;
    1.40 -    const_criterion: ('-'?)
    1.41 -      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
    1.42 -    ;
    1.43 -    @@{command thm_deps} @{syntax thmrefs}
    1.44 -    ;
    1.45 -    @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
    1.46 -  \<close>}
    1.47 -
    1.48 -  These commands print certain parts of the theory and proof context.
    1.49 -  Note that there are some further ones available, such as for the set
    1.50 -  of rules declared for simplifications.
    1.51 -
    1.52 -  \begin{description}
    1.53 -  
    1.54 -  \item @{command "print_theory"} prints the main logical content of the
    1.55 -  background theory; the ``@{text "!"}'' option indicates extra verbosity.
    1.56 -
    1.57 -  \item @{command "print_methods"} prints all proof methods available in the
    1.58 -  current theory context; the ``@{text "!"}'' option indicates extra
    1.59 -  verbosity.
    1.60 -  
    1.61 -  \item @{command "print_attributes"} prints all attributes available in the
    1.62 -  current theory context; the ``@{text "!"}'' option indicates extra
    1.63 -  verbosity.
    1.64 -  
    1.65 -  \item @{command "print_theorems"} prints theorems of the background theory
    1.66 -  resulting from the last command; the ``@{text "!"}'' option indicates
    1.67 -  extra verbosity.
    1.68 -  
    1.69 -  \item @{command "print_facts"} prints all local facts of the current
    1.70 -  context, both named and unnamed ones; the ``@{text "!"}'' option indicates
    1.71 -  extra verbosity.
    1.72 -  
    1.73 -  \item @{command "print_term_bindings"} prints all term bindings that
    1.74 -  are present in the context.
    1.75 -
    1.76 -  \item @{command "find_theorems"}~@{text criteria} retrieves facts
    1.77 -  from the theory or proof context matching all of given search
    1.78 -  criteria.  The criterion @{text "name: p"} selects all theorems
    1.79 -  whose fully qualified name matches pattern @{text p}, which may
    1.80 -  contain ``@{text "*"}'' wildcards.  The criteria @{text intro},
    1.81 -  @{text elim}, and @{text dest} select theorems that match the
    1.82 -  current goal as introduction, elimination or destruction rules,
    1.83 -  respectively.  The criterion @{text "solves"} returns all rules
    1.84 -  that would directly solve the current goal.  The criterion
    1.85 -  @{text "simp: t"} selects all rewrite rules whose left-hand side
    1.86 -  matches the given term.  The criterion term @{text t} selects all
    1.87 -  theorems that contain the pattern @{text t} -- as usual, patterns
    1.88 -  may contain occurrences of the dummy ``@{text _}'', schematic
    1.89 -  variables, and type constraints.
    1.90 -  
    1.91 -  Criteria can be preceded by ``@{text "-"}'' to select theorems that
    1.92 -  do \emph{not} match. Note that giving the empty list of criteria
    1.93 -  yields \emph{all} currently known facts.  An optional limit for the
    1.94 -  number of printed facts may be given; the default is 40.  By
    1.95 -  default, duplicates are removed from the search result. Use
    1.96 -  @{text with_dups} to display duplicates.
    1.97 -
    1.98 -  \item @{command "find_consts"}~@{text criteria} prints all constants
    1.99 -  whose type meets all of the given criteria. The criterion @{text
   1.100 -  "strict: ty"} is met by any type that matches the type pattern
   1.101 -  @{text ty}.  Patterns may contain both the dummy type ``@{text _}''
   1.102 -  and sort constraints. The criterion @{text ty} is similar, but it
   1.103 -  also matches against subtypes. The criterion @{text "name: p"} and
   1.104 -  the prefix ``@{text "-"}'' function as described for @{command
   1.105 -  "find_theorems"}.
   1.106 -
   1.107 -  \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
   1.108 -  visualizes dependencies of facts, using Isabelle's graph browser
   1.109 -  tool (see also @{cite "isabelle-system"}).
   1.110 -
   1.111 -  \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
   1.112 -  displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
   1.113 -  or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
   1.114 -  that are never used.
   1.115 -  If @{text n} is @{text 0}, the end of the range of theories
   1.116 -  defaults to the current theory. If no range is specified,
   1.117 -  only the unused theorems in the current theory are displayed.
   1.118 -  
   1.119 -  \end{description}
   1.120 -\<close>
   1.121 -
   1.122 -end
     2.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Jul 06 20:07:41 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Jul 06 20:13:51 2015 +0200
     2.3 @@ -411,7 +411,7 @@
     2.4  
     2.5    There are three forms of theorem references:
     2.6    \begin{enumerate}
     2.7 -  
     2.8 +
     2.9    \item named facts @{text "a"},
    2.10  
    2.11    \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
    2.12 @@ -456,4 +456,117 @@
    2.13    \<close>}
    2.14  \<close>
    2.15  
    2.16 +
    2.17 +section \<open>Diagnostic commands\<close>
    2.18 +
    2.19 +text \<open>
    2.20 +  \begin{matharray}{rcl}
    2.21 +    @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.22 +    @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.23 +    @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.24 +    @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.25 +    @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.26 +    @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.27 +    @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.28 +    @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.29 +    @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.30 +    @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.31 +  \end{matharray}
    2.32 +
    2.33 +  @{rail \<open>
    2.34 +    (@@{command print_theory} |
    2.35 +      @@{command print_methods} |
    2.36 +      @@{command print_attributes} |
    2.37 +      @@{command print_theorems} |
    2.38 +      @@{command print_facts}) ('!'?)
    2.39 +    ;
    2.40 +    @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
    2.41 +    ;
    2.42 +    thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
    2.43 +      'solves' | 'simp' ':' @{syntax term} | @{syntax term})
    2.44 +    ;
    2.45 +    @@{command find_consts} (const_criterion*)
    2.46 +    ;
    2.47 +    const_criterion: ('-'?)
    2.48 +      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
    2.49 +    ;
    2.50 +    @@{command thm_deps} @{syntax thmrefs}
    2.51 +    ;
    2.52 +    @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
    2.53 +  \<close>}
    2.54 +
    2.55 +  These commands print certain parts of the theory and proof context.
    2.56 +  Note that there are some further ones available, such as for the set
    2.57 +  of rules declared for simplifications.
    2.58 +
    2.59 +  \begin{description}
    2.60 +
    2.61 +  \item @{command "print_theory"} prints the main logical content of the
    2.62 +  background theory; the ``@{text "!"}'' option indicates extra verbosity.
    2.63 +
    2.64 +  \item @{command "print_methods"} prints all proof methods available in the
    2.65 +  current theory context; the ``@{text "!"}'' option indicates extra
    2.66 +  verbosity.
    2.67 +
    2.68 +  \item @{command "print_attributes"} prints all attributes available in the
    2.69 +  current theory context; the ``@{text "!"}'' option indicates extra
    2.70 +  verbosity.
    2.71 +
    2.72 +  \item @{command "print_theorems"} prints theorems of the background theory
    2.73 +  resulting from the last command; the ``@{text "!"}'' option indicates
    2.74 +  extra verbosity.
    2.75 +
    2.76 +  \item @{command "print_facts"} prints all local facts of the current
    2.77 +  context, both named and unnamed ones; the ``@{text "!"}'' option indicates
    2.78 +  extra verbosity.
    2.79 +
    2.80 +  \item @{command "print_term_bindings"} prints all term bindings that
    2.81 +  are present in the context.
    2.82 +
    2.83 +  \item @{command "find_theorems"}~@{text criteria} retrieves facts
    2.84 +  from the theory or proof context matching all of given search
    2.85 +  criteria.  The criterion @{text "name: p"} selects all theorems
    2.86 +  whose fully qualified name matches pattern @{text p}, which may
    2.87 +  contain ``@{text "*"}'' wildcards.  The criteria @{text intro},
    2.88 +  @{text elim}, and @{text dest} select theorems that match the
    2.89 +  current goal as introduction, elimination or destruction rules,
    2.90 +  respectively.  The criterion @{text "solves"} returns all rules
    2.91 +  that would directly solve the current goal.  The criterion
    2.92 +  @{text "simp: t"} selects all rewrite rules whose left-hand side
    2.93 +  matches the given term.  The criterion term @{text t} selects all
    2.94 +  theorems that contain the pattern @{text t} -- as usual, patterns
    2.95 +  may contain occurrences of the dummy ``@{text _}'', schematic
    2.96 +  variables, and type constraints.
    2.97 +
    2.98 +  Criteria can be preceded by ``@{text "-"}'' to select theorems that
    2.99 +  do \emph{not} match. Note that giving the empty list of criteria
   2.100 +  yields \emph{all} currently known facts.  An optional limit for the
   2.101 +  number of printed facts may be given; the default is 40.  By
   2.102 +  default, duplicates are removed from the search result. Use
   2.103 +  @{text with_dups} to display duplicates.
   2.104 +
   2.105 +  \item @{command "find_consts"}~@{text criteria} prints all constants
   2.106 +  whose type meets all of the given criteria. The criterion @{text
   2.107 +  "strict: ty"} is met by any type that matches the type pattern
   2.108 +  @{text ty}.  Patterns may contain both the dummy type ``@{text _}''
   2.109 +  and sort constraints. The criterion @{text ty} is similar, but it
   2.110 +  also matches against subtypes. The criterion @{text "name: p"} and
   2.111 +  the prefix ``@{text "-"}'' function as described for @{command
   2.112 +  "find_theorems"}.
   2.113 +
   2.114 +  \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
   2.115 +  visualizes dependencies of facts, using Isabelle's graph browser
   2.116 +  tool (see also @{cite "isabelle-system"}).
   2.117 +
   2.118 +  \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
   2.119 +  displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
   2.120 +  or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
   2.121 +  that are never used.
   2.122 +  If @{text n} is @{text 0}, the end of the range of theories
   2.123 +  defaults to the current theory. If no range is specified,
   2.124 +  only the unused theorems in the current theory are displayed.
   2.125 +
   2.126 +  \end{description}
   2.127 +\<close>
   2.128 +
   2.129  end
     3.1 --- a/src/Doc/Isar_Ref/document/root.tex	Mon Jul 06 20:07:41 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Mon Jul 06 20:13:51 2015 +0200
     3.3 @@ -76,7 +76,6 @@
     3.4  \input{Proof.tex}
     3.5  \input{Proof_Script.tex}
     3.6  \input{Inner_Syntax.tex}
     3.7 -\input{Misc.tex}
     3.8  \input{Generic.tex}
     3.9  \part{Isabelle/HOL}\label{part:hol}
    3.10  \input{HOL_Specific.tex}
     4.1 --- a/src/Doc/ROOT	Mon Jul 06 20:07:41 2015 +0200
     4.2 +++ b/src/Doc/ROOT	Mon Jul 06 20:13:51 2015 +0200
     4.3 @@ -166,7 +166,6 @@
     4.4      Proof
     4.5      Proof_Script
     4.6      Inner_Syntax
     4.7 -    Misc
     4.8      Generic
     4.9      HOL_Specific
    4.10      Quick_Reference