some more stuff;
authorwenzelm
Wed Mar 06 14:48:21 2002 +0100 (2002-03-06)
changeset 13027ddf235f2384a
parent 13026 e45ebbb2e18e
child 13028 81c87faed78b
some more stuff;
tuned;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/logics.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Mar 05 20:55:20 2002 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Wed Mar 06 14:48:21 2002 +0100
     1.3 @@ -27,6 +27,7 @@
     1.4  \end{rail}
     1.5  
     1.6  \begin{descr}
     1.7 +  
     1.8  \item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
     1.9    the intersection of existing classes, with additional axioms holding.  Class
    1.10    axioms may not contain more than one type variable.  The class axioms (with
    1.11 @@ -51,6 +52,7 @@
    1.12    as it is already included in the default proof step (of $\PROOFNAME$,
    1.13    $\BYNAME$, etc.).  In particular, instantiation of trivial (syntactic)
    1.14    classes may be performed by a single ``$\DDOT$'' proof step.
    1.15 +
    1.16  \end{descr}
    1.17  
    1.18  
    1.19 @@ -153,8 +155,8 @@
    1.20      
    1.21    \item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$
    1.22      and mixfix annotation $mx$ (both are optional).  The special syntax
    1.23 -    declaration $(structure)$ means that $x$ may be referenced
    1.24 -    implicitly in this context. %see also FIXME
    1.25 +    declaration ``$(structure)$'' means that $x$ may be referenced
    1.26 +    implicitly in this context.
    1.27      
    1.28    \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
    1.29      $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
    1.30 @@ -343,6 +345,7 @@
    1.31    single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =
    1.32      x}~\DDOT$''.  Note that the very same rules known to $symmetric$ are
    1.33    declared as $elim$ at the same time.
    1.34 +
    1.35  \end{descr}
    1.36  
    1.37  
    1.38 @@ -404,7 +407,7 @@
    1.39  \indexisaratt{tagged}\indexisaratt{untagged}
    1.40  \indexisaratt{THEN}\indexisaratt{COMP}
    1.41  \indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded}
    1.42 -\indexisaratt{standard}\indexisaratt{elim-format}
    1.43 +\indexisaratt{standard}\indexisarattof{Pure}{elim-format}
    1.44  \indexisaratt{no-vars}
    1.45  \begin{matharray}{rcl}
    1.46    tagged & : & \isaratt \\
    1.47 @@ -433,27 +436,39 @@
    1.48  \end{rail}
    1.49  
    1.50  \begin{descr}
    1.51 +  
    1.52  \item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
    1.53    theorem.  Tags may be any list of strings that serve as comment for some
    1.54    tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
    1.55    result).  The first string is considered the tag name, the rest its
    1.56    arguments.  Note that untag removes any tags of the same name.
    1.57 +  
    1.58  \item [$THEN~n~a$ and $COMP~n~a$] compose rules.  $THEN$ resolves with the
    1.59    $n$-th premise of $a$; the $COMP$ version skips the automatic lifting
    1.60    process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
    1.61    \cite[\S5]{isabelle-ref}).
    1.62 +  
    1.63  \item [$where~\vec x = \vec t$] perform named instantiation of schematic
    1.64    variables occurring in a theorem.  Unlike instantiation tactics such as
    1.65    $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
    1.66    have to be specified (e.g.\ $\Var{x@3}$).
    1.67 +  
    1.68  \item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
    1.69    given meta-level definitions throughout a rule.
    1.70 +  
    1.71  \item [$standard$] puts a theorem into the standard form of object-rules, just
    1.72    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
    1.73 -\item [$elim_format$] turns a destruction rule into elimination rule format;
    1.74 -  see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    1.75 +  
    1.76 +\item [$elim_format$] turns a destruction rule into elimination rule format,
    1.77 +  by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
    1.78 +  B$.
    1.79 +  
    1.80 +  Note that the Classical Reasoner (\S\ref{sec:classical-att}) provides its
    1.81 +  own version of this operation.
    1.82 +  
    1.83  \item [$no_vars$] replaces schematic variables by free ones; this is mainly
    1.84    for tuning output of pretty printed theorems.
    1.85 +
    1.86  \end{descr}
    1.87  
    1.88  
    1.89 @@ -538,30 +553,37 @@
    1.90  \end{rail}
    1.91  
    1.92  \begin{descr}
    1.93 +  
    1.94  \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
    1.95    This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
    1.96    \cite[\S3]{isabelle-ref}).
    1.97 -
    1.98 +  
    1.99    Note that multiple rules may be only given there is no instantiation.  Then
   1.100    $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
   1.101    \cite[\S3]{isabelle-ref}).
   1.102 +  
   1.103  \item [$cut_tac$] inserts facts into the proof state as assumption of a
   1.104    subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
   1.105 -  that the scope of schematic variables is spread over the main goal statement.
   1.106 -  Instantiations may be given as well, see also ML tactic
   1.107 +  that the scope of schematic variables is spread over the main goal
   1.108 +  statement.  Instantiations may be given as well, see also ML tactic
   1.109    \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
   1.110 +  
   1.111  \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
   1.112    that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
   1.113    \cite[\S3]{isabelle-ref}.
   1.114 +  
   1.115  \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
   1.116    also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
   1.117    \cite[\S3]{isabelle-ref}.
   1.118 +  
   1.119  \item [$rename_tac~\vec x$] renames parameters of a goal according to the list
   1.120    $\vec x$, which refers to the \emph{suffix} of variables.
   1.121 +  
   1.122  \item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
   1.123    from right to left if $n$ is positive, and from left to right if $n$ is
   1.124    negative; the default value is $1$.  See also \texttt{rotate_tac} in
   1.125    \cite[\S3]{isabelle-ref}.
   1.126 +  
   1.127  \item [$tactic~text$] produces a proof method from any ML text of type
   1.128    \texttt{tactic}.  Apart from the usual ML environment and the current
   1.129    implicit theory context, the ML code may refer to the following locally
   1.130 @@ -604,7 +626,7 @@
   1.131  
   1.132  \indexouternonterm{simpmod}
   1.133  \begin{rail}
   1.134 -  ('simp' | simpall) ('!' ?) opt? (simpmod * )
   1.135 +  ('simp' | simpall) ('!' ?) opt? (simpmod *)
   1.136    ;
   1.137  
   1.138    opt: '(' (noasm | noasmsimp | noasmuse) ')'
   1.139 @@ -822,9 +844,9 @@
   1.140  
   1.141  \indexouternonterm{clamod}
   1.142  \begin{rail}
   1.143 -  'blast' ('!' ?) nat? (clamod * )
   1.144 +  'blast' ('!' ?) nat? (clamod *)
   1.145    ;
   1.146 -  ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod * )
   1.147 +  ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
   1.148    ;
   1.149  
   1.150    clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
   1.151 @@ -866,9 +888,9 @@
   1.152  
   1.153  \indexouternonterm{clasimpmod}
   1.154  \begin{rail}
   1.155 -  'auto' '!'? (nat nat)? (clasimpmod * )
   1.156 +  'auto' '!'? (nat nat)? (clasimpmod *)
   1.157    ;
   1.158 -  ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod * )
   1.159 +  ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
   1.160    ;
   1.161  
   1.162    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
   1.163 @@ -945,6 +967,29 @@
   1.164  \end{descr}
   1.165  
   1.166  
   1.167 +\subsubsection{Classical operations}\label{sec:classical-att}
   1.168 +
   1.169 +\indexisaratt{elim-format}\indexisaratt{swapped}
   1.170 +
   1.171 +\begin{matharray}{rcl}
   1.172 +  elim_format & : & \isaratt \\
   1.173 +  swapped & : & \isaratt \\
   1.174 +\end{matharray}
   1.175 +
   1.176 +\begin{descr}
   1.177 +  
   1.178 +\item [$elim_format$] turns a destruction rule into elimination rule format;
   1.179 +  this operation is similar to the the intuitionistic version
   1.180 +  (\S\ref{sec:misc-meth-att}), but each premise of the resulting rule acquires
   1.181 +  an additional local fact of the negated main thesis -- according to the
   1.182 +  classical principle $(\neg A \Imp A) \Imp A$.
   1.183 +  
   1.184 +\item [$swapped$] turns an introduction rule into an elimination, by resolving
   1.185 +  with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$.
   1.186 +
   1.187 +\end{descr}
   1.188 +
   1.189 +
   1.190  \subsection{Proof by cases and induction}\label{sec:cases-induct}
   1.191  
   1.192  \subsubsection{Rule contexts}\label{sec:rule-cases}
   1.193 @@ -970,20 +1015,22 @@
   1.194  The $\CASENAME$ command provides a shorthand to refer to certain parts of
   1.195  logical context symbolically.  Proof methods may provide an environment of
   1.196  named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
   1.197 -$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   1.198 -
   1.199 -FIXME
   1.200 +``$\CASE{c}$'' is that of ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''; term
   1.201 +bindings may be covered as well, such as $\Var{case}$.
   1.202  
   1.203 -It is important to note that $\CASENAME$ does \emph{not} provide any means to
   1.204 -peek at the current goal state, which is treated as strictly non-observable in
   1.205 -Isar!  Instead, the cases considered here usually emerge in a canonical way
   1.206 -from certain pieces of specification that appear in the theory somewhere else
   1.207 -(e.g.\ in an inductive definition, or recursive function).
   1.208 -
   1.209 -FIXME
   1.210 +Normally the ``terminology'' of a case value (i.e.\ the parameters $\vec x$)
   1.211 +are marked as hidden.  Using the alternative form ``$(\CASE{c}~\vec x)$''
   1.212 +enables proof writers to choose their own naming for the subsequent proof
   1.213 +text.
   1.214  
   1.215  \medskip
   1.216  
   1.217 +It is important to note that $\CASENAME$ does \emph{not} provide direct means
   1.218 +to peek at the current goal state, which is generally considered
   1.219 +non-observable in Isar.  The text of the cases basically emerge from standard
   1.220 +elimination or induction rules, which in turn are derived from previous theory
   1.221 +specifications in a canonical way (say via $\isarkeyword{inductive}$).
   1.222 +
   1.223  Named cases may be exhibited in the current proof context only if both the
   1.224  proof method and the rules involved support this.  Case names and parameters
   1.225  of basic rules may be declared by hand as well, by using appropriate
   1.226 @@ -999,32 +1046,36 @@
   1.227    caseref: nameref attributes?
   1.228    ;
   1.229  
   1.230 -  casenames (name + )
   1.231 +  casenames (name +)
   1.232    ;
   1.233 -  'params' ((name * ) + 'and')
   1.234 +  'params' ((name *) + 'and')
   1.235    ;
   1.236    'consumes' nat?
   1.237    ;
   1.238  \end{rail}
   1.239 -%FIXME bug in rail
   1.240  
   1.241  \begin{descr}
   1.242 +  
   1.243  \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
   1.244    as provided by an appropriate proof method (such as $cases$ and $induct$,
   1.245    see \S\ref{sec:cases-induct-meth}).  The command $\CASE{c}$ abbreviates
   1.246    $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   1.247 +  
   1.248  \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   1.249    state, using Isar proof language notation.  This is a diagnostic command;
   1.250    $undo$ does not apply.
   1.251 +  
   1.252  \item [$case_names~\vec c$] declares names for the local contexts of premises
   1.253    of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
   1.254    premises.
   1.255 +  
   1.256  \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
   1.257    premises $1, \dots, n$ of some theorem.  An empty list of names may be given
   1.258    to skip positions, leaving the present parameters unchanged.
   1.259    
   1.260    Note that the default usage of case rules does \emph{not} directly expose
   1.261    parameters to the proof context (see also \S\ref{sec:cases-induct-meth}).
   1.262 +  
   1.263  \item [$consumes~n$] declares the number of ``major premises'' of a rule,
   1.264    i.e.\ the number of facts to be consumed when it is applied by an
   1.265    appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}).  The default
   1.266 @@ -1036,6 +1087,7 @@
   1.267    Note that explicit $consumes$ declarations are only rarely needed; this is
   1.268    already taken care of automatically by the higher-level $cases$ and $induct$
   1.269    declarations, see also \S\ref{sec:cases-induct-att}.
   1.270 +
   1.271  \end{descr}
   1.272  
   1.273  
   1.274 @@ -1079,6 +1131,7 @@
   1.275  \end{rail}
   1.276  
   1.277  \begin{descr}
   1.278 +  
   1.279  \item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
   1.280    distinction theorem, instantiated to the subjects $insts$.  Symbolic case
   1.281    names are bound according to the rule's local contexts.
   1.282 @@ -1131,6 +1184,7 @@
   1.283    
   1.284    Additional parameters (including the $open$ option) may be given in the same
   1.285    way as for $cases$, see above.
   1.286 +
   1.287  \end{descr}
   1.288  
   1.289  Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as
   1.290 @@ -1204,7 +1258,7 @@
   1.291    
   1.292  \item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for
   1.293    sets and types of the current context.
   1.294 -
   1.295 +  
   1.296  \item [$cases$ and $induct$] (as attributes) augment the corresponding context
   1.297    of rules for reasoning about inductive sets and types, using the
   1.298    corresponding methods of the same name.  Certain definitional packages of
     2.1 --- a/doc-src/IsarRef/logics.tex	Tue Mar 05 20:55:20 2002 +0100
     2.2 +++ b/doc-src/IsarRef/logics.tex	Wed Mar 06 14:48:21 2002 +0100
     2.3 @@ -146,10 +146,9 @@
     2.4  
     2.5  \railalias{splitformat}{split\_format}
     2.6  \railterm{splitformat}
     2.7 -\railterm{complete}
     2.8  
     2.9  \begin{rail}
    2.10 -  splitformat (((name *) + 'and') | ('(' complete ')'))
    2.11 +  splitformat (((name *) + 'and') | ('(' 'complete' ')'))
    2.12    ;
    2.13  \end{rail}
    2.14  
    2.15 @@ -433,7 +432,6 @@
    2.16    \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
    2.17    \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
    2.18    \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
    2.19 -%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\  %FIXME
    2.20  \end{matharray}
    2.21  
    2.22  \railalias{recdefsimp}{recdef\_simp}
    2.23 @@ -644,6 +642,48 @@
    2.24  \end{descr}
    2.25  
    2.26  
    2.27 +\subsection{Generating executable code}
    2.28 +
    2.29 +Isabelle/Pure provides a generic infrastructure to support code generation
    2.30 +from executable specifications, both functional and relational programs.
    2.31 +Isabelle/HOL instantiates these mechanisms in a way that is amenable to
    2.32 +end-user applications.  See \cite{isabelle-HOL} for further information (this
    2.33 +actually covers the new-style theory format).
    2.34 +
    2.35 +\indexisarcmd{generate-code}\indexisarcmd{consts-code}\indexisarcmd{types-code}
    2.36 +\indexisaratt{code}
    2.37 +
    2.38 +\begin{matharray}{rcl}
    2.39 +  \isarcmd{generate_code} & : & \isartrans{theory}{theory} \\
    2.40 +  \isarcmd{consts_code} & : & \isartrans{theory}{theory} \\
    2.41 +  \isarcmd{types_code} & : & \isartrans{theory}{theory} \\  
    2.42 +  code & : & \isaratt \\
    2.43 +\end{matharray}
    2.44 +
    2.45 +\railalias{generatecode}{generate\_code}
    2.46 +\railterm{generatecode}
    2.47 +
    2.48 +\railalias{constscode}{consts\_code}
    2.49 +\railterm{constscode}
    2.50 +
    2.51 +\railalias{typescode}{types\_code}
    2.52 +\railterm{typescode}
    2.53 +
    2.54 +\begin{rail}
    2.55 +  generatecode ( () | '(' name ')') ((name '=' term) +)
    2.56 +  ;
    2.57 +  constscode (name ('::' type)? template +)
    2.58 +  ;
    2.59 +  typescode (name template +)
    2.60 +  ;
    2.61 +  template: '(' string ')'
    2.62 +  ;
    2.63 +
    2.64 +  'code' (name)?
    2.65 +  ;
    2.66 +\end{rail}
    2.67 +
    2.68 +
    2.69  \section{HOLCF}
    2.70  
    2.71  \subsection{Mixfix syntax for continuous operations}