doc-src/IsarRef/generic.tex
author nipkow
Wed, 04 Aug 2004 11:25:08 +0200
changeset 15106 e8cef6993701
parent 14605 9de4d64eee3b
child 15763 b901a127ac73
permissions -rw-r--r--
aded comment
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7135
wenzelm
parents:
diff changeset
     1
13048
wenzelm
parents: 13042
diff changeset
     2
\chapter{Generic tools and packages}\label{ch:gen-tools}
7167
wenzelm
parents: 7141
diff changeset
     3
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
     4
\section{Theory specification commands}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
     5
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
     6
\subsection{Axiomatic type classes}\label{sec:axclass}
7167
wenzelm
parents: 7141
diff changeset
     7
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
     8
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
7167
wenzelm
parents: 7141
diff changeset
     9
\begin{matharray}{rcl}
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    10
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    11
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    12
  intro_classes & : & \isarmeth \\
7167
wenzelm
parents: 7141
diff changeset
    13
\end{matharray}
wenzelm
parents: 7141
diff changeset
    14
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    15
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    16
interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
8547
wenzelm
parents: 8517
diff changeset
    17
may make use of this light-weight mechanism of abstract theories
8901
e591fc327675 cite isabelle-axclass;
wenzelm
parents: 8811
diff changeset
    18
\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
    19
classes in Isabelle \cite{isabelle-axclass} that is part of the standard
8901
e591fc327675 cite isabelle-axclass;
wenzelm
parents: 8811
diff changeset
    20
Isabelle documentation.
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    21
7167
wenzelm
parents: 7141
diff changeset
    22
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
    23
  'axclass' classdecl (axmdecl prop +)
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    24
  ;
14605
9de4d64eee3b 'instance' and intro_classes now handle general sorts;
wenzelm
parents: 14212
diff changeset
    25
  'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
7167
wenzelm
parents: 7141
diff changeset
    26
  ;
wenzelm
parents: 7141
diff changeset
    27
\end{rail}
wenzelm
parents: 7141
diff changeset
    28
wenzelm
parents: 7141
diff changeset
    29
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    30
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
    31
\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11095
diff changeset
    32
  the intersection of existing classes, with additional axioms holding.  Class
10223
wenzelm
parents: 10160
diff changeset
    33
  axioms may not contain more than one type variable.  The class axioms (with
wenzelm
parents: 10160
diff changeset
    34
  implicit sort constraints added) are bound to the given names.  Furthermore
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    35
  a class introduction rule is generated (being bound as $c{.}intro$); this
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    36
  rule is employed by method $intro_classes$ to support instantiation proofs
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    37
  of this class.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    38
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    39
  The ``axioms'' are stored as theorems according to the given name
13039
wenzelm
parents: 13027
diff changeset
    40
  specifications, adding the class name $c$ as name space prefix; the same
wenzelm
parents: 13027
diff changeset
    41
  facts are also stored collectively as $c{\dtt}axioms$.
14605
9de4d64eee3b 'instance' and intro_classes now handle general sorts;
wenzelm
parents: 14212
diff changeset
    42
  
9de4d64eee3b 'instance' and intro_classes now handle general sorts;
wenzelm
parents: 14212
diff changeset
    43
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11095
diff changeset
    44
  goal stating a class relation or type arity.  The proof would usually
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11095
diff changeset
    45
  proceed by $intro_classes$, and then establish the characteristic theorems
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11095
diff changeset
    46
  of the type classes involved.  After finishing the proof, the theory will be
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11095
diff changeset
    47
  augmented by a type signature declaration corresponding to the resulting
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11095
diff changeset
    48
  theorem.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    49
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
    50
\item [$intro_classes$] repeatedly expands all class introduction rules of
10858
wenzelm
parents: 10741
diff changeset
    51
  this theory.  Note that this method usually needs not be named explicitly,
13040
wenzelm
parents: 13039
diff changeset
    52
  as it is already included in the default proof step (of $\PROOFNAME$ etc.).
wenzelm
parents: 13039
diff changeset
    53
  In particular, instantiation of trivial (syntactic) classes may be performed
wenzelm
parents: 13039
diff changeset
    54
  by a single ``$\DDOT$'' proof step.
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
    55
7167
wenzelm
parents: 7141
diff changeset
    56
\end{descr}
wenzelm
parents: 7141
diff changeset
    57
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    58
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
    59
\subsection{Locales and local contexts}\label{sec:locale}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
    60
13040
wenzelm
parents: 13039
diff changeset
    61
Locales are named local contexts, consisting of a list of declaration elements
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    62
that are modeled after the Isar proof context commands (cf.\
13040
wenzelm
parents: 13039
diff changeset
    63
\S\ref{sec:proof-context}).
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    64
13048
wenzelm
parents: 13042
diff changeset
    65
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    66
\subsubsection{Localized commands}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
    67
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    68
Existing locales may be augmented later on by adding new facts.  Note that the
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    69
actual context definition may not be changed!  Several theory commands that
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    70
produce facts in some way are available in ``localized'' versions, referring
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    71
to a named locale instead of the global theory context.
12967
wenzelm
parents: 12879
diff changeset
    72
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    73
\indexouternonterm{locale}
12967
wenzelm
parents: 12879
diff changeset
    74
\begin{rail}
wenzelm
parents: 12879
diff changeset
    75
  locale: '(' 'in' name ')'
wenzelm
parents: 12879
diff changeset
    76
  ;
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    77
\end{rail}
12967
wenzelm
parents: 12879
diff changeset
    78
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    79
Emerging facts of localized commands are stored in two versions, both in the
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    80
target locale and the theory (after export).  The latter view produces a
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    81
qualified binding, using the locale name as a name space prefix.
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    82
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    83
For example, ``$\LEMMAS~(\IN~loc)~a = \vec b$'' retrieves facts $\vec b$ from
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    84
the locale context of $loc$ and augments its body by an appropriate
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    85
``$\isarkeyword{notes}$'' element (see below).  The exported view of $a$,
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    86
after discharging the locale context, is stored as $loc{.}a$ within the global
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    87
theory.  A localized goal ``$\LEMMANAME~(\IN~loc)~a:~\phi$'' works similarly,
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    88
only that the fact emerges through the subsequent proof, which may refer to
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    89
the full infrastructure of the locale context (covering local parameters with
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    90
typing and concrete syntax, assumptions, definitions etc.).  Most notably,
13411
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
    91
fact declarations of the locale are active during the proof as well (e.g.\ 
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
    92
local $simp$ rules).
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    93
13411
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
    94
As a general principle, results exported from a locale context acquire
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
    95
additional premises according to the specification.  Usually this is only a
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
    96
single predicate according to the standard ``closed'' view of locale
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
    97
specifications.
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
    98
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
    99
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   100
\subsubsection{Locale specifications}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   101
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   102
\indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   103
\begin{matharray}{rcl}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   104
  \isarcmd{locale} & : & \isarkeep{theory} \\
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   105
  \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   106
  \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   107
\end{matharray}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   108
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   109
\indexouternonterm{contextexpr}\indexouternonterm{contextelem}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   110
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   111
\railalias{printlocale}{print\_locale}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   112
\railterm{printlocale}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   113
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   114
\begin{rail}
13411
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   115
  'locale' ('(open)')? name ('=' localeexpr)?
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   116
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   117
  printlocale localeexpr
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   118
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   119
  localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   120
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   121
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   122
  contextexpr: nameref | '(' contextexpr ')' |
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   123
  (contextexpr (name+)) | (contextexpr + '+')
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   124
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   125
  contextelem: fixes | assumes | defines | notes | includes
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   126
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   127
  fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   128
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   129
  assumes: 'assumes' (thmdecl? props + 'and')
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   130
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   131
  defines: 'defines' (thmdecl? prop proppat? + 'and')
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   132
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   133
  notes: 'notes' (thmdef? thmrefs + 'and')
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   134
  ;
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   135
  includes: 'includes' contextexpr
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   136
  ;
12967
wenzelm
parents: 12879
diff changeset
   137
\end{rail}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
   138
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   139
\begin{descr}
13411
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   140
  
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   141
\item [$\LOCALE~loc~=~import~+~body$] defines a new locale $loc$ as a context
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   142
  consisting of a certain view of existing locales ($import$) plus some
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   143
  additional elements ($body$).  Both $import$ and $body$ are optional; the
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   144
  degenerate form $\LOCALE~loc$ defines an empty locale, which may still be
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   145
  useful to collect declarations of facts later on.  Type-inference on locale
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   146
  expressions automatically takes care of the most general typing that the
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   147
  combined context elements may acquire.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   148
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   149
  The $import$ consists of a structured context expression, consisting of
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   150
  references to existing locales, renamed contexts, or merged contexts.
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   151
  Renaming uses positional notation: $c~\vec x$ means that (a prefix) the
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   152
  fixed parameters of context $c$ are named according to $\vec x$; a
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   153
  ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} means to skip that
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   154
  position.  Also note that concrete syntax only works with the original name.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   155
  Merging proceeds from left-to-right, suppressing any duplicates stemming
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   156
  from different paths through the import hierarchy.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   157
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   158
  The $body$ consists of basic context elements, further context expressions
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   159
  may be included as well.
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   160
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   161
  \begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   162
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   163
  \item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   164
    and mixfix annotation $mx$ (both are optional).  The special syntax
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   165
    declaration ``$(structure)$'' means that $x$ may be referenced
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   166
    implicitly in this context.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   167
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   168
  \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   169
    $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   170
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   171
  \item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   172
    This is close to $\DEFNAME$ within a proof (cf.\
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   173
    \S\ref{sec:proof-context}), but $\DEFINESNAME$ takes an equational
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   174
    proposition instead of variable-term pair.  The left-hand side of the
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   175
    equation may have additional arguments, e.g.\ ``$\DEFINES{}{f~\vec x
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   176
      \equiv t}$''.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   177
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   178
  \item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context.  Most
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   179
    notably, this may include arbitrary declarations in any attribute
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   180
    specifications included here, e.g.\ a local $simp$ rule.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   181
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   182
  \item [$\INCLUDES{c}$] copies the specified context in a statically scoped
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   183
    manner.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   184
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   185
    In contrast, the initial $import$ specification of a locale expression
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   186
    maintains a dynamic relation to the locales being referenced (benefiting
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   187
    from any later fact declarations in the obvious manner).
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   188
  \end{descr}
13411
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   189
  
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   190
  Note that ``$\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and
13411
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   191
  $\DEFINESNAME$ above are illegal in locale definitions.  In the long goal
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   192
  format of \S\ref{sec:goals}, term bindings may be included as expected,
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   193
  though.
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   194
  
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   195
  \medskip By default, locale specifications are ``closed up'' by turning the
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   196
  given text into a predicate definition $loc_axioms$ and deriving the
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   197
  original assumptions as local lemmas (modulo local definitions).  The
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   198
  predicate statement covers only the newly specified assumptions, omitting
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   199
  the content of included locale expressions.  The full cumulative view is
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   200
  only provided on export, involving another predicate $loc$ that refers to
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   201
  the complete specification text.
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   202
  
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   203
  In any case, the predicate arguments are those locale parameters that
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   204
  actually occur in the respective piece of text.  Also note that these
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   205
  predicates operate at the meta-level in theory, but the locale packages
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   206
  attempts to internalize statements according to the object-logic setup
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   207
  (e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   208
  also \S\ref{sec:object-logic}).  Separate introduction rules
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   209
  $loc_axioms.intro$ and $loc.intro$ are declared as well.
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   210
  
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   211
  The $(open)$ option of a locale specification prevents both the current
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   212
  $loc_axioms$ and cumulative $loc$ predicate constructions.  Predicates are
181a293aa37a locales: predicate defs;
wenzelm
parents: 13048
diff changeset
   213
  also omitted for empty specification texts.
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   214
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   215
\item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   216
  expression in a flattened form.  The notable special case
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   217
  $\isarkeyword{print_locale}~loc$ just prints the contents of the named
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   218
  locale, but keep in mind that type-inference will normalize type variables
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   219
  according to the usual alphabetical order.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   220
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   221
\item [$\isarkeyword{print_locales}$] prints the names of all locales of the
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   222
  current theory.
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   223
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   224
\end{descr}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   225
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   226
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   227
\section{Derived proof schemes}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   228
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   229
\subsection{Generalized elimination}\label{sec:obtain}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   230
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   231
\indexisarcmd{obtain}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   232
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   233
  \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   234
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   235
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   236
Generalized elimination means that additional elements with certain properties
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   237
may be introduced in the current context, by virtue of a locally proven
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   238
``soundness statement''.  Technically speaking, the $\OBTAINNAME$ language
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   239
element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   240
\S\ref{sec:proof-context}), together with a soundness proof of its additional
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   241
claim.  According to the nature of existential reasoning, assumptions get
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   242
eliminated from any result exported from the context later, provided that the
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   243
corresponding parameters do \emph{not} occur in the conclusion.
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   244
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   245
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   246
  'obtain' (vars + 'and') 'where' (props + 'and')
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   247
  ;
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   248
\end{rail}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
   249
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   250
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   251
shall refer to (optional) facts indicated for forward chaining.
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   252
\begin{matharray}{l}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   253
  \langle facts~\vec b\rangle \\
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   254
  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   255
  \quad \HAVE{}{\All{thesis} (\All{\vec x} \vec\phi \Imp thesis) \Imp thesis} \\
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   256
  \quad \PROOF{succeed} \\
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   257
  \qquad \FIX{thesis} \\
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   258
  \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\
13042
wenzelm
parents: 13041
diff changeset
   259
  \qquad \THUS{}{thesis} \\
wenzelm
parents: 13041
diff changeset
   260
  \quad\qquad \APPLY{-} \\
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   261
  \quad\qquad \USING{\vec b}~~\langle proof\rangle \\
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   262
  \quad \QED{} \\
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   263
  \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   264
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   265
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   266
Typically, the soundness proof is relatively straight-forward, often just by
13048
wenzelm
parents: 13042
diff changeset
   267
canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
wenzelm
parents: 13042
diff changeset
   268
Accordingly, the ``$that$'' reduction above is declared as simplification and
wenzelm
parents: 13042
diff changeset
   269
introduction rule.
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   270
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   271
\medskip
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   272
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   273
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   274
meta-logical existential quantifiers and conjunctions.  This concept has a
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   275
broad range of useful applications, ranging from plain elimination (or
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   276
introduction) of object-level existentials and conjunctions, to elimination
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   277
over results of symbolic evaluation of recursive definitions, for example.
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   278
Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   279
where the result is treated as a genuine assumption.
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   280
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   281
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   282
\subsection{Calculational reasoning}\label{sec:calculation}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   283
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   284
\indexisarcmd{also}\indexisarcmd{finally}
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   285
\indexisarcmd{moreover}\indexisarcmd{ultimately}
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   286
\indexisarcmd{print-trans-rules}
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   287
\indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   288
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   289
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   290
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   291
  \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   292
  \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
10154
wenzelm
parents: 10031
diff changeset
   293
  \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   294
  trans & : & \isaratt \\
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   295
  sym & : & \isaratt \\
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   296
  symmetric & : & \isaratt \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   297
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   298
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   299
Calculational proof is forward reasoning with implicit application of
11332
11ab8c8ce694 extended doc for iff attribute
oheimb
parents: 11128
diff changeset
   300
transitivity rules (such those of $=$, $\leq$, $<$).  Isabelle/Isar maintains
7391
b7ca64c8fa64 'iff' attribute;
wenzelm
parents: 7356
diff changeset
   301
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
7897
7f18f5ffbb92 *** empty log message ***
wenzelm
parents: 7526
diff changeset
   302
results obtained by transitivity composed with the current result.  Command
7f18f5ffbb92 *** empty log message ***
wenzelm
parents: 7526
diff changeset
   303
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
7f18f5ffbb92 *** empty log message ***
wenzelm
parents: 7526
diff changeset
   304
final $calculation$ by forward chaining towards the next goal statement.  Both
7f18f5ffbb92 *** empty log message ***
wenzelm
parents: 7526
diff changeset
   305
commands require valid current facts, i.e.\ may occur only after commands that
7f18f5ffbb92 *** empty log message ***
wenzelm
parents: 7526
diff changeset
   306
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   307
$\HAVENAME$, $\SHOWNAME$ etc.  The $\MOREOVER$ and $\ULTIMATELY$ commands are
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   308
similar to $\ALSO$ and $\FINALLY$, but only collect further results in
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   309
$calculation$ without applying any rules yet.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   310
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   311
Also note that the implicit term abbreviation ``$\dots$'' has its canonical
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   312
application with calculational proofs.  It refers to the argument of the
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   313
preceding statement. (The argument of a curried infix expression happens to be
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   314
its right-hand side.)
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   316
Isabelle/Isar calculations are implicitly subject to block structure in the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   317
sense that new threads of calculational reasoning are commenced for any new
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   318
block (as opened by a local goal, for example).  This means that, apart from
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   319
being able to nest calculations, there is no separate \emph{begin-calculation}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   320
command required.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   321
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   322
\medskip
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   323
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   324
The Isar calculation proof commands may be defined as follows:\footnote{We
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   325
  suppress internal bookkeeping such as proper handling of block-structure.}
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   326
\begin{matharray}{rcl}
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   327
  \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   328
  \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   329
  \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   330
  \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   331
  \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   332
\end{matharray}
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   333
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   334
\begin{rail}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   335
  ('also' | 'finally') ('(' thmrefs ')')?
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   336
  ;
8507
d22fcea34cb7 untag: only name arg;
wenzelm
parents: 8483
diff changeset
   337
  'trans' (() | 'add' | 'del')
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   338
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   339
\end{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   340
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   341
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   342
8547
wenzelm
parents: 8517
diff changeset
   343
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   344
  follows.  The first occurrence of $\ALSO$ in some calculational thread
7905
wenzelm
parents: 7897
diff changeset
   345
  initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   346
  level of block-structure updates $calculation$ by some transitivity rule
7458
bb282845ca77 updated;
wenzelm
parents: 7396
diff changeset
   347
  applied to $calculation$ and $this$ (in that order).  Transitivity rules are
11095
2ffaf1e1e101 updated;
wenzelm
parents: 10858
diff changeset
   348
  picked from the current context, unless alternative rules are given as
2ffaf1e1e101 updated;
wenzelm
parents: 10858
diff changeset
   349
  explicit arguments.
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   350
8547
wenzelm
parents: 8517
diff changeset
   351
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   352
  $\ALSO$, and concludes the current calculational thread.  The final result
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   353
  is exhibited as fact for forward chaining towards the next goal. Basically,
7987
wenzelm
parents: 7981
diff changeset
   354
  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
wenzelm
parents: 7981
diff changeset
   355
  ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
wenzelm
parents: 7981
diff changeset
   356
  ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
wenzelm
parents: 7981
diff changeset
   357
  calculational proofs.
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   358
8619
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   359
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
63a0e1502e41 added 'moreover' and 'ultimately';
wenzelm
parents: 8594
diff changeset
   360
  but collect results only, without applying rules.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   361
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   362
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   363
  rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   364
  (for the $symmetric$ operation and single step elimination patters) of the
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   365
  current context.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   366
8547
wenzelm
parents: 8517
diff changeset
   367
\item [$trans$] declares theorems as transitivity rules.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   368
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   369
\item [$sym$] declares symmetry rules.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   370
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   371
\item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   372
  current context.  For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   373
  swapped fact derived from that assumption.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   374
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   375
  In structured proof texts it is often more appropriate to use an explicit
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   376
  single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   377
    x}~\DDOT$''.  The very same rules known to $symmetric$ are declared as
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   378
  $elim?$ as well.
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   379
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   380
\end{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   381
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   382
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   383
\section{Proof tools}
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   384
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
   385
\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   386
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   387
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   388
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   389
\indexisarmeth{fail}\indexisarmeth{succeed}
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   390
\begin{matharray}{rcl}
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   391
  unfold & : & \isarmeth \\
10741
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   392
  fold & : & \isarmeth \\
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   393
  insert & : & \isarmeth \\[0.5ex]
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   394
  erule^* & : & \isarmeth \\
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   395
  drule^* & : & \isarmeth \\
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   396
  frule^* & : & \isarmeth \\
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   397
  succeed & : & \isarmeth \\
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   398
  fail & : & \isarmeth \\
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   399
\end{matharray}
7135
wenzelm
parents:
diff changeset
   400
wenzelm
parents:
diff changeset
   401
\begin{rail}
10741
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   402
  ('fold' | 'unfold' | 'insert') thmrefs
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   403
  ;
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   404
  ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
7135
wenzelm
parents:
diff changeset
   405
  ;
wenzelm
parents:
diff changeset
   406
\end{rail}
wenzelm
parents:
diff changeset
   407
7167
wenzelm
parents: 7141
diff changeset
   408
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   409
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   410
\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   411
  given meta-level definitions throughout all goals; any chained facts
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   412
  provided are inserted into the goal and subject to rewriting as well.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   413
10741
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   414
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   415
  state.  Note that current facts indicated for forward chaining are ignored.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   416
8547
wenzelm
parents: 8517
diff changeset
   417
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
wenzelm
parents: 8517
diff changeset
   418
  basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   419
  elim-resolution, destruct-resolution, and forward-resolution, respectively
10741
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   420
  \cite{isabelle-ref}.  The optional natural number argument (default $0$)
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   421
  specifies additional assumption steps to be performed here.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   422
10741
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   423
  Note that these methods are improper ones, mainly serving for
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   424
  experimentation and tactic script emulation.  Different modes of basic rule
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   425
  application are usually expressed in Isar at the proof language level,
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   426
  rather than via implicit proof state manipulations.  For example, a proper
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   427
  single-step elimination would be done using the plain $rule$ method, with
10741
e56ac1863f2c 'insert' made proper;
wenzelm
parents: 10627
diff changeset
   428
  forward chaining of current facts.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   429
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   430
\item [$succeed$] yields a single (unchanged) result; it is the identity of
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   431
  the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   432
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   433
\item [$fail$] yields an empty result sequence; it is the identity of the
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   434
  ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   435
7167
wenzelm
parents: 7141
diff changeset
   436
\end{descr}
7135
wenzelm
parents:
diff changeset
   437
10318
wenzelm
parents: 10223
diff changeset
   438
\indexisaratt{tagged}\indexisaratt{untagged}
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   439
\indexisaratt{THEN}\indexisaratt{COMP}
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   440
\indexisaratt{unfolded}\indexisaratt{folded}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   441
\indexisaratt{standard}\indexisarattof{Pure}{elim-format}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   442
\indexisaratt{no-vars}
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   443
\begin{matharray}{rcl}
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   444
  tagged & : & \isaratt \\
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   445
  untagged & : & \isaratt \\[0.5ex]
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   446
  THEN & : & \isaratt \\
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   447
  COMP & : & \isaratt \\[0.5ex]
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   448
  unfolded & : & \isaratt \\
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   449
  folded & : & \isaratt \\[0.5ex]
9941
fe05af7ec816 renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents: 9936
diff changeset
   450
  elim_format & : & \isaratt \\
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   451
  standard^* & : & \isaratt \\
9936
f080397656d8 renamed "delrule" to "rule del";
wenzelm
parents: 9905
diff changeset
   452
  no_vars^* & : & \isaratt \\
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   453
\end{matharray}
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   454
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   455
\begin{rail}
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   456
  'tagged' (nameref+)
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   457
  ;
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   458
  'untagged' name
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   459
  ;
10154
wenzelm
parents: 10031
diff changeset
   460
  ('THEN' | 'COMP') ('[' nat ']')? thmref
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   461
  ;
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   462
  ('unfolded' | 'folded') thmrefs
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   463
  ;
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   464
\end{rail}
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   465
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   466
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   467
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   468
\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   469
  theorem.  Tags may be any list of strings that serve as comment for some
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   470
  tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   471
  result).  The first string is considered the tag name, the rest its
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   472
  arguments.  Note that untag removes any tags of the same name.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   473
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   474
\item [$THEN~a$ and $COMP~a$] compose rules by resolution.  $THEN$ resolves
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   475
  with the first premise of $a$ (an alternative position may be also
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   476
  specified); the $COMP$ version skips the automatic lifting process that is
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   477
  normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
8547
wenzelm
parents: 8517
diff changeset
   478
  \cite[\S5]{isabelle-ref}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   479
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   480
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   481
  given meta-level definitions throughout a rule.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   482
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   483
\item [$elim_format$] turns a destruction rule into elimination rule format,
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   484
  by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   485
  B$.
13048
wenzelm
parents: 13042
diff changeset
   486
  
wenzelm
parents: 13042
diff changeset
   487
  Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
wenzelm
parents: 13042
diff changeset
   488
  version of this operation.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   489
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   490
\item [$standard$] puts a theorem into the standard form of object-rules at
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   491
  the outermost theory level.  Note that this operation violates the local
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   492
  proof context (including active locales).
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   493
9232
96722b04f2ae added no_vars att;
wenzelm
parents: 9005
diff changeset
   494
\item [$no_vars$] replaces schematic variables by free ones; this is mainly
96722b04f2ae added no_vars att;
wenzelm
parents: 9005
diff changeset
   495
  for tuning output of pretty printed theorems.
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   496
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   497
\end{descr}
7135
wenzelm
parents:
diff changeset
   498
wenzelm
parents:
diff changeset
   499
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   500
\subsection{Further tactic emulations}\label{sec:tactics}
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   501
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   502
The following improper proof methods emulate traditional tactics.  These admit
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   503
direct access to the goal state, which is normally considered harmful!  In
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   504
particular, this may involve both numbered goal addressing (default 1), and
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   505
dynamic instantiation within the scope of some subgoal.
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   506
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   507
\begin{warn}
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   508
  Dynamic instantiations refer to universally quantified parameters of
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   509
  a subgoal (the dynamic context) rather than fixed variables and term
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   510
  abbreviations of a (static) Isar context.
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   511
\end{warn}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   512
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   513
Tactic emulation methods, unlike their ML counterparts, admit
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   514
simultaneous instantiation from both dynamic and static contexts.  If
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   515
names occur in both contexts goal parameters hide locally fixed
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   516
variables.  Likewise, schematic variables refer to term abbreviations,
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   517
if present in the static context.  Otherwise the schematic variable is
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   518
interpreted as a schematic variable and left to be solved by unification
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   519
with certain parts of the subgoal.
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   520
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   521
Note that the tactic emulation proof methods in Isabelle/Isar are consistently
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   522
named $foo_tac$.  Note also that variable names occurring on left hand sides
14212
cd05b503ca2d Improvements wrt rule_tac.
ballarin
parents: 14175
diff changeset
   523
of instantiations must be preceded by a question mark if they coincide with
cd05b503ca2d Improvements wrt rule_tac.
ballarin
parents: 14175
diff changeset
   524
a keyword or contain dots.
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13622
diff changeset
   525
This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   526
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   527
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   528
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   529
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
9642
d8d1f70024bd fixed indexing;
wenzelm
parents: 9614
diff changeset
   530
\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   531
\indexisarmeth{rotate-tac}\indexisarmeth{tactic}
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   532
\begin{matharray}{rcl}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   533
  rule_tac^* & : & \isarmeth \\
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   534
  erule_tac^* & : & \isarmeth \\
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   535
  drule_tac^* & : & \isarmeth \\
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   536
  frule_tac^* & : & \isarmeth \\
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   537
  cut_tac^* & : & \isarmeth \\
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   538
  thin_tac^* & : & \isarmeth \\
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   539
  subgoal_tac^* & : & \isarmeth \\
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   540
  rename_tac^* & : & \isarmeth \\
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   541
  rotate_tac^* & : & \isarmeth \\
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   542
  tactic^* & : & \isarmeth \\
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   543
\end{matharray}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   544
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   545
\railalias{ruletac}{rule\_tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   546
\railterm{ruletac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   547
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   548
\railalias{eruletac}{erule\_tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   549
\railterm{eruletac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   550
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   551
\railalias{druletac}{drule\_tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   552
\railterm{druletac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   553
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   554
\railalias{fruletac}{frule\_tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   555
\railterm{fruletac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   556
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   557
\railalias{cuttac}{cut\_tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   558
\railterm{cuttac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   559
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   560
\railalias{thintac}{thin\_tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   561
\railterm{thintac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   562
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   563
\railalias{subgoaltac}{subgoal\_tac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   564
\railterm{subgoaltac}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   565
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   566
\railalias{renametac}{rename\_tac}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   567
\railterm{renametac}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   568
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   569
\railalias{rotatetac}{rotate\_tac}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   570
\railterm{rotatetac}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   571
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   572
\begin{rail}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   573
  ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   574
  ( insts thmref | thmrefs )
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   575
  ;
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   576
  subgoaltac goalspec? (prop +)
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   577
  ;
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   578
  renametac goalspec? (name +)
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   579
  ;
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   580
  rotatetac goalspec? int?
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   581
  ;
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   582
  'tactic' text
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   583
  ;
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   584
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   585
  insts: ((name '=' term) + 'and') 'in'
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   586
  ;
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   587
\end{rail}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   588
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   589
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   590
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   591
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   592
  This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   593
  \cite[\S3]{isabelle-ref}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   594
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   595
  Multiple rules may be only given if there is no instantiation; then
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   596
  $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   597
  \cite[\S3]{isabelle-ref}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   598
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   599
\item [$cut_tac$] inserts facts into the proof state as assumption of a
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   600
  subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   601
  that the scope of schematic variables is spread over the main goal
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   602
  statement.  Instantiations may be given as well, see also ML tactic
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   603
  \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   604
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   605
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   606
  that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   607
  \cite[\S3]{isabelle-ref}.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   608
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   609
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   610
  also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   611
  \cite[\S3]{isabelle-ref}.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   612
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   613
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   614
  $\vec x$, which refers to the \emph{suffix} of variables.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   615
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   616
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   617
  from right to left if $n$ is positive, and from left to right if $n$ is
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   618
  negative; the default value is $1$.  See also \texttt{rotate_tac} in
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   619
  \cite[\S3]{isabelle-ref}.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   620
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   621
\item [$tactic~text$] produces a proof method from any ML text of type
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   622
  \texttt{tactic}.  Apart from the usual ML environment and the current
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   623
  implicit theory context, the ML code may refer to the following locally
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   624
  bound values:
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   625
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   626
{\footnotesize\begin{verbatim}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   627
val ctxt  : Proof.context
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   628
val facts : thm list
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   629
val thm   : string -> thm
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   630
val thms  : string -> thm list
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   631
\end{verbatim}}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   632
  Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   633
  indicates any current facts for forward-chaining, and
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   634
  \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   635
  theorems) from the context.
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   636
\end{descr}
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   637
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   638
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   639
\subsection{The Simplifier}\label{sec:simplifier}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   640
13048
wenzelm
parents: 13042
diff changeset
   641
\subsubsection{Simplification methods}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
   642
8483
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   643
\indexisarmeth{simp}\indexisarmeth{simp-all}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   644
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   645
  simp & : & \isarmeth \\
8483
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   646
  simp_all & : & \isarmeth \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   647
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   648
8483
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   649
\railalias{simpall}{simp\_all}
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   650
\railterm{simpall}
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   651
8704
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   652
\railalias{noasm}{no\_asm}
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   653
\railterm{noasm}
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   654
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   655
\railalias{noasmsimp}{no\_asm\_simp}
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   656
\railterm{noasmsimp}
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   657
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   658
\railalias{noasmuse}{no\_asm\_use}
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   659
\railterm{noasmuse}
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   660
13617
1430360d9782 Documented new "asm_lr" option for simp.
berghofe
parents: 13425
diff changeset
   661
\railalias{asmlr}{asm\_lr}
1430360d9782 Documented new "asm_lr" option for simp.
berghofe
parents: 13425
diff changeset
   662
\railterm{asmlr}
1430360d9782 Documented new "asm_lr" option for simp.
berghofe
parents: 13425
diff changeset
   663
11128
48c63b87566e index mod syntax;
wenzelm
parents: 11100
diff changeset
   664
\indexouternonterm{simpmod}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   665
\begin{rail}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   666
  ('simp' | simpall) ('!' ?) opt? (simpmod *)
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   667
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   668
13617
1430360d9782 Documented new "asm_lr" option for simp.
berghofe
parents: 13425
diff changeset
   669
  opt: '(' (noasm | noasmsimp | noasmuse | asmlr) ')'
8704
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   670
  ;
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   671
  simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
9847
32ce11c3f6b1 added 'iff' modifier;
wenzelm
parents: 9799
diff changeset
   672
    'split' (() | 'add' | 'del')) ':' thmrefs
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   673
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   674
\end{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   675
7321
wenzelm
parents: 7319
diff changeset
   676
\begin{descr}
13015
wenzelm
parents: 12976
diff changeset
   677
8547
wenzelm
parents: 8517
diff changeset
   678
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
8594
d2e2a3df6871 rail token vs. terminal;
wenzelm
parents: 8547
diff changeset
   679
  according to the arguments given.  Note that the \railtterm{only} modifier
8547
wenzelm
parents: 8517
diff changeset
   680
  first removes all other rewrite rules, congruences, and looper tactics
8594
d2e2a3df6871 rail token vs. terminal;
wenzelm
parents: 8547
diff changeset
   681
  (including splits), and then behaves like \railtterm{add}.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   682
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   683
  \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   684
  rules (see also \cite{isabelle-ref}), the default is to add.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   685
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   686
  \medskip The \railtterm{split} modifiers add or delete rules for the
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   687
  Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   688
  only if the Simplifier method has been properly setup to include the
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   689
  Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   690
13015
wenzelm
parents: 12976
diff changeset
   691
\item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from
wenzelm
parents: 12976
diff changeset
   692
  the last to the first one).
wenzelm
parents: 12976
diff changeset
   693
7321
wenzelm
parents: 7319
diff changeset
   694
\end{descr}
wenzelm
parents: 7319
diff changeset
   695
13015
wenzelm
parents: 12976
diff changeset
   696
By default the Simplifier methods take local assumptions fully into account,
wenzelm
parents: 12976
diff changeset
   697
using equational assumptions in the subsequent normalization process, or
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   698
simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in
13015
wenzelm
parents: 12976
diff changeset
   699
\cite[\S10]{isabelle-ref}).  In structured proofs this is usually quite well
wenzelm
parents: 12976
diff changeset
   700
behaved in practice: just the local premises of the actual goal are involved,
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   701
additional facts may be inserted via explicit forward-chaining (using $\THEN$,
13015
wenzelm
parents: 12976
diff changeset
   702
$\FROMNAME$ etc.).  The full context of assumptions is only included if the
wenzelm
parents: 12976
diff changeset
   703
``$!$'' (bang) argument is given, which should be used with some care, though.
7321
wenzelm
parents: 7319
diff changeset
   704
13015
wenzelm
parents: 12976
diff changeset
   705
Additional Simplifier options may be specified to tune the behavior further
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   706
(mostly for unstructured scripts with many accidental local facts):
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   707
``$(no_asm)$'' means assumptions are ignored completely (cf.\
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   708
\texttt{simp_tac}), ``$(no_asm_simp)$'' means assumptions are used in the
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   709
simplification of the conclusion but are not themselves simplified (cf.\
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   710
\texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   711
simplified but are not used in the simplification of each other or the
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   712
conclusion (cf.\ \texttt{full_simp_tac}).
13617
1430360d9782 Documented new "asm_lr" option for simp.
berghofe
parents: 13425
diff changeset
   713
For compatibility reasons, there is also an option ``$(asm_lr)$'',
1430360d9782 Documented new "asm_lr" option for simp.
berghofe
parents: 13425
diff changeset
   714
which means that an assumption is only used for simplifying assumptions
1430360d9782 Documented new "asm_lr" option for simp.
berghofe
parents: 13425
diff changeset
   715
which are to the right of it (cf.\ \texttt{asm_lr_simp_tac}).
8704
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   716
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   717
\medskip
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   718
f76f41f24c44 Simplifier options;
wenzelm
parents: 8667
diff changeset
   719
The Splitter package is usually configured to work as part of the Simplifier.
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   720
The effect of repeatedly applying \texttt{split_tac} can be simulated by
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   721
``$(simp~only\colon~split\colon~\vec a)$''.  There is also a separate $split$
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   722
method available for single-step case splitting.
8483
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   723
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   724
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   725
\subsubsection{Declaring rules}
8483
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   726
8667
4230d17073ea print_simpset / print_claset command;
wenzelm
parents: 8638
diff changeset
   727
\indexisarcmd{print-simpset}
8638
21cb46716f32 added 'cong' att;
wenzelm
parents: 8619
diff changeset
   728
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
7321
wenzelm
parents: 7319
diff changeset
   729
\begin{matharray}{rcl}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   730
  \isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\
7321
wenzelm
parents: 7319
diff changeset
   731
  simp & : & \isaratt \\
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   732
  cong & : & \isaratt \\
8483
b437907f9b26 Named local contexts (cases);
wenzelm
parents: 8203
diff changeset
   733
  split & : & \isaratt \\
7321
wenzelm
parents: 7319
diff changeset
   734
\end{matharray}
wenzelm
parents: 7319
diff changeset
   735
wenzelm
parents: 7319
diff changeset
   736
\begin{rail}
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   737
  ('simp' | 'cong' | 'split') (() | 'add' | 'del')
7321
wenzelm
parents: 7319
diff changeset
   738
  ;
wenzelm
parents: 7319
diff changeset
   739
\end{rail}
wenzelm
parents: 7319
diff changeset
   740
wenzelm
parents: 7319
diff changeset
   741
\begin{descr}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   742
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   743
\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   744
  the Simplifier, which is also known as ``simpset'' internally
8667
4230d17073ea print_simpset / print_claset command;
wenzelm
parents: 8638
diff changeset
   745
  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   746
8547
wenzelm
parents: 8517
diff changeset
   747
\item [$simp$] declares simplification rules.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   748
8638
21cb46716f32 added 'cong' att;
wenzelm
parents: 8619
diff changeset
   749
\item [$cong$] declares congruence rules.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   750
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   751
\item [$split$] declares case split rules.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   752
7321
wenzelm
parents: 7319
diff changeset
   753
\end{descr}
7319
wenzelm
parents: 7315
diff changeset
   754
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   755
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   756
\subsubsection{Forward simplification}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   757
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   758
\indexisaratt{simplified}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   759
\begin{matharray}{rcl}
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   760
  simplified & : & \isaratt \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   761
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   762
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   763
\begin{rail}
13015
wenzelm
parents: 12976
diff changeset
   764
  'simplified' opt? thmrefs?
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   765
  ;
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   766
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   767
  opt: '(' (noasm | noasmsimp | noasmuse) ')'
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   768
  ;
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   769
\end{rail}
7905
wenzelm
parents: 7897
diff changeset
   770
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   771
\begin{descr}
13048
wenzelm
parents: 13042
diff changeset
   772
  
13015
wenzelm
parents: 12976
diff changeset
   773
\item [$simplified~\vec a$] causes a theorem to be simplified, either by
wenzelm
parents: 12976
diff changeset
   774
  exactly the specified rules $\vec a$, or the implicit Simplifier context if
wenzelm
parents: 12976
diff changeset
   775
  no arguments are given.  The result is fully simplified by default,
wenzelm
parents: 12976
diff changeset
   776
  including assumptions and conclusion; the options $no_asm$ etc.\ tune the
13048
wenzelm
parents: 13042
diff changeset
   777
  Simplifier in the same way as the for the $simp$ method.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   778
13015
wenzelm
parents: 12976
diff changeset
   779
  Note that forward simplification restricts the simplifier to its most basic
wenzelm
parents: 12976
diff changeset
   780
  operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
wenzelm
parents: 12976
diff changeset
   781
  are \emph{not} involved here.  The $simplified$ attribute should be only
wenzelm
parents: 12976
diff changeset
   782
  rarely required under normal circumstances.
wenzelm
parents: 12976
diff changeset
   783
9905
14a71104a498 improved att names;
wenzelm
parents: 9847
diff changeset
   784
\end{descr}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   785
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   786
13048
wenzelm
parents: 13042
diff changeset
   787
\subsubsection{Low-level equational reasoning}
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   788
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12967
diff changeset
   789
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   790
\begin{matharray}{rcl}
13015
wenzelm
parents: 12976
diff changeset
   791
  subst^* & : & \isarmeth \\
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   792
  hypsubst^* & : & \isarmeth \\
13015
wenzelm
parents: 12976
diff changeset
   793
  split^* & : & \isarmeth \\
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   794
\end{matharray}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   795
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   796
\begin{rail}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   797
  'subst' thmref
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   798
  ;
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   799
  'split' ('(' 'asm' ')')? thmrefs
9703
bf65780eed02 added 'split' method;
wenzelm
parents: 9642
diff changeset
   800
  ;
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   801
\end{rail}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   802
13015
wenzelm
parents: 12976
diff changeset
   803
These methods provide low-level facilities for equational reasoning that are
wenzelm
parents: 12976
diff changeset
   804
intended for specialized applications only.  Normally, single step
wenzelm
parents: 12976
diff changeset
   805
calculations would be performed in a structured text (see also
wenzelm
parents: 12976
diff changeset
   806
\S\ref{sec:calculation}), while the Simplifier methods provide the canonical
wenzelm
parents: 12976
diff changeset
   807
way for automated normalization (see \S\ref{sec:simplifier}).
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   808
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   809
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   810
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   811
\item [$subst~a$] performs a single substitution step using rule $a$, which
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   812
  may be either a meta or object equality.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   813
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   814
\item [$hypsubst$] performs substitution using some assumption; this only
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   815
  works for equations of the form $x = t$ where $x$ is a free or bound
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   816
  variable.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   817
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   818
\item [$split~\vec a$] performs single-step case splitting using rules $thms$.
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   819
  By default, splitting is performed in the conclusion of a goal; the $asm$
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   820
  option indicates to operate on assumptions instead.
13048
wenzelm
parents: 13042
diff changeset
   821
  
9703
bf65780eed02 added 'split' method;
wenzelm
parents: 9642
diff changeset
   822
  Note that the $simp$ method already involves repeated application of split
13048
wenzelm
parents: 13042
diff changeset
   823
  rules as declared in the current context.
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   824
\end{descr}
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   825
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   826
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   827
\subsection{The Classical Reasoner}\label{sec:classical}
7135
wenzelm
parents:
diff changeset
   828
13048
wenzelm
parents: 13042
diff changeset
   829
\subsubsection{Basic methods}
7321
wenzelm
parents: 7319
diff changeset
   830
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   831
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   832
\indexisarmeth{intro}\indexisarmeth{elim}
7321
wenzelm
parents: 7319
diff changeset
   833
\begin{matharray}{rcl}
wenzelm
parents: 7319
diff changeset
   834
  rule & : & \isarmeth \\
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   835
  contradiction & : & \isarmeth \\
7321
wenzelm
parents: 7319
diff changeset
   836
  intro & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   837
  elim & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   838
\end{matharray}
wenzelm
parents: 7319
diff changeset
   839
wenzelm
parents: 7319
diff changeset
   840
\begin{rail}
8547
wenzelm
parents: 8517
diff changeset
   841
  ('rule' | 'intro' | 'elim') thmrefs?
7321
wenzelm
parents: 7319
diff changeset
   842
  ;
wenzelm
parents: 7319
diff changeset
   843
\end{rail}
wenzelm
parents: 7319
diff changeset
   844
wenzelm
parents: 7319
diff changeset
   845
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   846
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   847
\item [$rule$] as offered by the classical reasoner is a refinement over the
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   848
  primitive one (see \S\ref{sec:pure-meth-att}).  Both versions essentially
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   849
  work the same, but the classical version observes the classical rule context
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   850
  in addition to that of Isabelle/Pure.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   851
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   852
  Common object logics (HOL, ZF, etc.) declare a rich collection of classical
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   853
  rules (even if these would qualify as intuitionistic ones), but only few
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   854
  declarations to the rule context of Isabelle/Pure
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   855
  (\S\ref{sec:pure-meth-att}).
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   856
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   857
\item [$contradiction$] solves some goal by contradiction, deriving any result
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   858
  from both $\neg A$ and $A$.  Chained facts, which are guaranteed to
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   859
  participate, may appear in either order.
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   860
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   861
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   862
  elim-resolution, after having inserted any chained facts.  Exactly the rules
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   863
  given as arguments are taken into account; this allows fine-tuned
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   864
  decomposition of a proof problem, in contrast to common automated tools.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   865
7321
wenzelm
parents: 7319
diff changeset
   866
\end{descr}
wenzelm
parents: 7319
diff changeset
   867
wenzelm
parents: 7319
diff changeset
   868
13048
wenzelm
parents: 13042
diff changeset
   869
\subsubsection{Automated methods}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   870
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   871
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   872
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
7321
wenzelm
parents: 7319
diff changeset
   873
\begin{matharray}{rcl}
9780
d25d6a977ea6 added 'safe' method;
wenzelm
parents: 9711
diff changeset
   874
  blast & : & \isarmeth \\
d25d6a977ea6 added 'safe' method;
wenzelm
parents: 9711
diff changeset
   875
  fast & : & \isarmeth \\
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   876
  slow & : & \isarmeth \\
9780
d25d6a977ea6 added 'safe' method;
wenzelm
parents: 9711
diff changeset
   877
  best & : & \isarmeth \\
d25d6a977ea6 added 'safe' method;
wenzelm
parents: 9711
diff changeset
   878
  safe & : & \isarmeth \\
d25d6a977ea6 added 'safe' method;
wenzelm
parents: 9711
diff changeset
   879
  clarify & : & \isarmeth \\
7321
wenzelm
parents: 7319
diff changeset
   880
\end{matharray}
wenzelm
parents: 7319
diff changeset
   881
11128
48c63b87566e index mod syntax;
wenzelm
parents: 11100
diff changeset
   882
\indexouternonterm{clamod}
7321
wenzelm
parents: 7319
diff changeset
   883
\begin{rail}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   884
  'blast' ('!' ?) nat? (clamod *)
7321
wenzelm
parents: 7319
diff changeset
   885
  ;
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   886
  ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
7321
wenzelm
parents: 7319
diff changeset
   887
  ;
wenzelm
parents: 7319
diff changeset
   888
9408
d3d56e1d2ec1 classical atts now intro! / intro / intro?;
wenzelm
parents: 9232
diff changeset
   889
  clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
7321
wenzelm
parents: 7319
diff changeset
   890
  ;
wenzelm
parents: 7319
diff changeset
   891
\end{rail}
wenzelm
parents: 7319
diff changeset
   892
wenzelm
parents: 7319
diff changeset
   893
\begin{descr}
wenzelm
parents: 7319
diff changeset
   894
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   895
  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
10858
wenzelm
parents: 10741
diff changeset
   896
  user-supplied search bound (default 20).
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   897
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   898
  classical reasoner.  See \texttt{fast_tac}, \texttt{slow_tac},
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   899
  \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   900
  \cite[\S11]{isabelle-ref} for more information.
7321
wenzelm
parents: 7319
diff changeset
   901
\end{descr}
wenzelm
parents: 7319
diff changeset
   902
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   903
Any of the above methods support additional modifiers of the context of
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   904
classical rules.  Their semantics is analogous to the attributes given before.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   905
Facts provided by forward chaining are inserted into the goal before
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   906
commencing proof search.  The ``!''~argument causes the full context of
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   907
assumptions to be included as well.
7321
wenzelm
parents: 7319
diff changeset
   908
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   909
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   910
\subsubsection{Combined automated methods}\label{sec:clasimp}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   911
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   912
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   913
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
7321
wenzelm
parents: 7319
diff changeset
   914
\begin{matharray}{rcl}
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   915
  auto & : & \isarmeth \\
7321
wenzelm
parents: 7319
diff changeset
   916
  force & : & \isarmeth \\
9438
6131037f8a11 removed slow, slow_best methods;
wenzelm
parents: 9408
diff changeset
   917
  clarsimp & : & \isarmeth \\
9606
1bf495402ae9 moved tactic emulation methods here;
wenzelm
parents: 9480
diff changeset
   918
  fastsimp & : & \isarmeth \\
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   919
  slowsimp & : & \isarmeth \\
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   920
  bestsimp & : & \isarmeth \\
7321
wenzelm
parents: 7319
diff changeset
   921
\end{matharray}
wenzelm
parents: 7319
diff changeset
   922
11128
48c63b87566e index mod syntax;
wenzelm
parents: 11100
diff changeset
   923
\indexouternonterm{clasimpmod}
7321
wenzelm
parents: 7319
diff changeset
   924
\begin{rail}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   925
  'auto' '!'? (nat nat)? (clasimpmod *)
9780
d25d6a977ea6 added 'safe' method;
wenzelm
parents: 9711
diff changeset
   926
  ;
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   927
  ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
7321
wenzelm
parents: 7319
diff changeset
   928
  ;
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   929
9711
75df6a20b0b3 'cong' modifiers;
wenzelm
parents: 9703
diff changeset
   930
  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
10031
12fd0fcf755a attribute / modifier 'iff': support "?" mode;
wenzelm
parents: 9941
diff changeset
   931
    ('cong' | 'split') (() | 'add' | 'del') |
12fd0fcf755a attribute / modifier 'iff': support "?" mode;
wenzelm
parents: 9941
diff changeset
   932
    'iff' (((() | 'add') '?'?) | 'del') |
9408
d3d56e1d2ec1 classical atts now intro! / intro / intro?;
wenzelm
parents: 9232
diff changeset
   933
    (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
7321
wenzelm
parents: 7319
diff changeset
   934
\end{rail}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   935
7321
wenzelm
parents: 7319
diff changeset
   936
\begin{descr}
9799
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   937
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   938
  provide access to Isabelle's combined simplification and classical reasoning
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   939
  tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   940
  \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
038b018f86f5 'split' method: '(asm)' option;
wenzelm
parents: 9780
diff changeset
   941
  added as wrapper, see \cite[\S11]{isabelle-ref} for more information.  The
13048
wenzelm
parents: 13042
diff changeset
   942
  modifier arguments correspond to those given in \S\ref{sec:simplifier} and
wenzelm
parents: 13042
diff changeset
   943
  \S\ref{sec:classical}.  Just note that the ones related to the Simplifier
wenzelm
parents: 13042
diff changeset
   944
  are prefixed by \railtterm{simp} here.
9614
8ca1fc75230e renamed 'RS' to 'THEN';
wenzelm
parents: 9606
diff changeset
   945
7987
wenzelm
parents: 7981
diff changeset
   946
  Facts provided by forward chaining are inserted into the goal before doing
wenzelm
parents: 7981
diff changeset
   947
  the search.  The ``!''~argument causes the full context of assumptions to be
wenzelm
parents: 7981
diff changeset
   948
  included as well.
7321
wenzelm
parents: 7319
diff changeset
   949
\end{descr}
wenzelm
parents: 7319
diff changeset
   950
7987
wenzelm
parents: 7981
diff changeset
   951
13048
wenzelm
parents: 13042
diff changeset
   952
\subsubsection{Declaring rules}
7135
wenzelm
parents:
diff changeset
   953
8667
4230d17073ea print_simpset / print_claset command;
wenzelm
parents: 8638
diff changeset
   954
\indexisarcmd{print-claset}
7391
b7ca64c8fa64 'iff' attribute;
wenzelm
parents: 7356
diff changeset
   955
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
9936
f080397656d8 renamed "delrule" to "rule del";
wenzelm
parents: 9905
diff changeset
   956
\indexisaratt{iff}\indexisaratt{rule}
7321
wenzelm
parents: 7319
diff changeset
   957
\begin{matharray}{rcl}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   958
  \isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\
7321
wenzelm
parents: 7319
diff changeset
   959
  intro & : & \isaratt \\
wenzelm
parents: 7319
diff changeset
   960
  elim & : & \isaratt \\
wenzelm
parents: 7319
diff changeset
   961
  dest & : & \isaratt \\
9936
f080397656d8 renamed "delrule" to "rule del";
wenzelm
parents: 9905
diff changeset
   962
  rule & : & \isaratt \\
7391
b7ca64c8fa64 'iff' attribute;
wenzelm
parents: 7356
diff changeset
   963
  iff & : & \isaratt \\
7321
wenzelm
parents: 7319
diff changeset
   964
\end{matharray}
7135
wenzelm
parents:
diff changeset
   965
7321
wenzelm
parents: 7319
diff changeset
   966
\begin{rail}
9408
d3d56e1d2ec1 classical atts now intro! / intro / intro?;
wenzelm
parents: 9232
diff changeset
   967
  ('intro' | 'elim' | 'dest') ('!' | () | '?')
7321
wenzelm
parents: 7319
diff changeset
   968
  ;
9936
f080397656d8 renamed "delrule" to "rule del";
wenzelm
parents: 9905
diff changeset
   969
  'rule' 'del'
f080397656d8 renamed "delrule" to "rule del";
wenzelm
parents: 9905
diff changeset
   970
  ;
10031
12fd0fcf755a attribute / modifier 'iff': support "?" mode;
wenzelm
parents: 9941
diff changeset
   971
  'iff' (((() | 'add') '?'?) | 'del')
9936
f080397656d8 renamed "delrule" to "rule del";
wenzelm
parents: 9905
diff changeset
   972
  ;
7321
wenzelm
parents: 7319
diff changeset
   973
\end{rail}
7135
wenzelm
parents:
diff changeset
   974
7321
wenzelm
parents: 7319
diff changeset
   975
\begin{descr}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   976
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   977
\item [$\isarcmd{print_claset}$] prints the collection of rules declared to
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   978
  the Classical Reasoner, which is also known as ``simpset'' internally
8667
4230d17073ea print_simpset / print_claset command;
wenzelm
parents: 8638
diff changeset
   979
  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   980
8517
062e6cd78534 obtain;
wenzelm
parents: 8507
diff changeset
   981
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
11332
11ab8c8ce694 extended doc for iff attribute
oheimb
parents: 11128
diff changeset
   982
  destruction rules, respectively.  By default, rules are considered as
9408
d3d56e1d2ec1 classical atts now intro! / intro / intro?;
wenzelm
parents: 9232
diff changeset
   983
  \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   984
  single ``!'' classifies as \emph{safe}.  Rule declarations marked by ``?''
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   985
  coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   986
  are only applied in single steps of the $rule$ method).
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   987
11332
11ab8c8ce694 extended doc for iff attribute
oheimb
parents: 11128
diff changeset
   988
\item [$rule~del$] deletes introduction, elimination, or destruction rules from
9936
f080397656d8 renamed "delrule" to "rule del";
wenzelm
parents: 9905
diff changeset
   989
  the context.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   990
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   991
\item [$iff$] declares logical equivalences to the Simplifier and the
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   992
  Classical reasoner at the same time.  Non-conditional rules result in a
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   993
  ``safe'' introduction and elimination pair; conditional ones are considered
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
   994
  ``unsafe''.  Rules with negative conclusion are automatically inverted
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   995
  (using $\neg$ elimination internally).
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   996
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   997
  The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only,
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   998
  and omits the Simplifier declaration.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
   999
7321
wenzelm
parents: 7319
diff changeset
  1000
\end{descr}
7135
wenzelm
parents:
diff changeset
  1001
8203
2fcc6017cb72 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents: 8195
diff changeset
  1002
13048
wenzelm
parents: 13042
diff changeset
  1003
\subsubsection{Classical operations}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1004
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1005
\indexisaratt{elim-format}\indexisaratt{swapped}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1006
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1007
\begin{matharray}{rcl}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1008
  elim_format & : & \isaratt \\
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1009
  swapped & : & \isaratt \\
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1010
\end{matharray}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1011
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1012
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1013
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1014
\item [$elim_format$] turns a destruction rule into elimination rule format;
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1015
  this operation is similar to the the intuitionistic version
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1016
  (\S\ref{sec:misc-meth-att}), but each premise of the resulting rule acquires
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1017
  an additional local fact of the negated main thesis; according to the
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1018
  classical principle $(\neg A \Imp A) \Imp A$.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1019
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1020
\item [$swapped$] turns an introduction rule into an elimination, by resolving
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1021
  with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$.
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1022
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1023
\end{descr}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1024
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1025
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1026
\subsection{Proof by cases and induction}\label{sec:cases-induct}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1027
13048
wenzelm
parents: 13042
diff changeset
  1028
\subsubsection{Rule contexts}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1029
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1030
\indexisarcmd{case}\indexisarcmd{print-cases}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1031
\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1032
\begin{matharray}{rcl}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1033
  \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1034
  \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1035
  case_names & : & \isaratt \\
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1036
  params & : & \isaratt \\
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1037
  consumes & : & \isaratt \\
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1038
\end{matharray}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1039
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1040
Basically, Isar proof contexts are built up explicitly using commands like
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1041
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1042
verification tasks this can become hard to manage, though.  In particular, a
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1043
large number of local contexts may emerge from case analysis or induction over
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1044
inductive sets and types.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1045
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1046
\medskip
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1047
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1048
The $\CASENAME$ command provides a shorthand to refer to certain parts of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1049
logical context symbolically.  Proof methods may provide an environment of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1050
named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1051
``$\CASE{c}$'' is that of ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''.  Term
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1052
bindings may be covered as well, such as $\Var{case}$ for the intended
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1053
conclusion.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1054
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1055
Normally the ``terminology'' of a case value (i.e.\ the parameters $\vec x$)
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1056
are marked as hidden.  Using the explicit form ``$\CASE{(c~\vec x)}$'' enables
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1057
proof writers to choose their own names for the subsequent proof text.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1058
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1059
\medskip
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1060
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1061
It is important to note that $\CASENAME$ does \emph{not} provide direct means
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1062
to peek at the current goal state, which is generally considered
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1063
non-observable in Isar.  The text of the cases basically emerge from standard
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1064
elimination or induction rules, which in turn are derived from previous theory
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1065
specifications in a canonical way (say from $\isarkeyword{inductive}$
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1066
definitions).
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1067
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1068
Named cases may be exhibited in the current proof context only if both the
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1069
proof method and the rules involved support this.  Case names and parameters
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1070
of basic rules may be declared by hand as well, by using appropriate
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1071
attributes.  Thus variant versions of rules that have been derived manually
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1072
may be used in advanced case analysis later.
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1073
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1074
\railalias{casenames}{case\_names}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1075
\railterm{casenames}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1076
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1077
\begin{rail}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1078
  'case' (caseref | '(' caseref ((name | underscore) +) ')')
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1079
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1080
  caseref: nameref attributes?
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1081
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1082
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1083
  casenames (name +)
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1084
  ;
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1085
  'params' ((name *) + 'and')
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1086
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1087
  'consumes' nat?
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1088
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1089
\end{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1090
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1091
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1092
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1093
\item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x,
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1094
  \vec \phi$, as provided by an appropriate proof method (such as $cases$ and
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1095
  $induct$, see \S\ref{sec:cases-induct-meth}).  The command ``$\CASE{(c~\vec
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1096
    x)}$'' abbreviates ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1097
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1098
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1099
  state, using Isar proof language notation.  This is a diagnostic command;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1100
  $undo$ does not apply.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1101
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1102
\item [$case_names~\vec c$] declares names for the local contexts of premises
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1103
  of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1104
  premises.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1105
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1106
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1107
  premises $1, \dots, n$ of some theorem.  An empty list of names may be given
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1108
  to skip positions, leaving the present parameters unchanged.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1109
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1110
  Note that the default usage of case rules does \emph{not} directly expose
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1111
  parameters to the proof context (see also \S\ref{sec:cases-induct-meth}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1112
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1113
\item [$consumes~n$] declares the number of ``major premises'' of a rule,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1114
  i.e.\ the number of facts to be consumed when it is applied by an
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1115
  appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}).  The default
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1116
  value of $consumes$ is $n = 1$, which is appropriate for the usual kind of
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1117
  cases and induction rules for inductive sets (cf.\
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1118
  \S\ref{sec:hol-inductive}).  Rules without any $consumes$ declaration given
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1119
  are treated as if $consumes~0$ had been specified.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1120
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1121
  Note that explicit $consumes$ declarations are only rarely needed; this is
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1122
  already taken care of automatically by the higher-level $cases$ and $induct$
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1123
  declarations, see also \S\ref{sec:cases-induct-att}.
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1124
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1125
\end{descr}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1126
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1127
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1128
\subsubsection{Proof methods}\label{sec:cases-induct-meth}
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1129
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1130
\indexisarmeth{cases}\indexisarmeth{induct}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1131
\begin{matharray}{rcl}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1132
  cases & : & \isarmeth \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1133
  induct & : & \isarmeth \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1134
\end{matharray}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1135
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1136
The $cases$ and $induct$ methods provide a uniform interface to case analysis
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1137
and induction over datatypes, inductive sets, and recursive functions.  The
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1138
corresponding rules may be specified and instantiated in a casual manner.
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1139
Furthermore, these methods provide named local contexts that may be invoked
13048
wenzelm
parents: 13042
diff changeset
  1140
via the $\CASENAME$ proof command within the subsequent proof text.  This
wenzelm
parents: 13042
diff changeset
  1141
accommodates compact proof texts even when reasoning about large
wenzelm
parents: 13042
diff changeset
  1142
specifications.
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1143
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1144
\begin{rail}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1145
  'cases' spec
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1146
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1147
  'induct' spec
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1148
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1149
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1150
  spec: open? args rule?
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1151
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1152
  open: '(' 'open' ')'
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1153
  ;
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1154
  args: (insts * 'and')
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1155
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1156
  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1157
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1158
\end{rail}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1159
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1160
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1161
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1162
\item [$cases~insts~R$] applies method $rule$ with an appropriate case
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1163
  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1164
  names are bound according to the rule's local contexts.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1165
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1166
  The rule is determined as follows, according to the facts and arguments
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1167
  passed to the $cases$ method:
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1168
  \begin{matharray}{llll}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1169
    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1170
                    & cases &           & \Text{classical case split} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1171
                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1172
    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1173
    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1174
  \end{matharray}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1175
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1176
  Several instantiations may be given, referring to the \emph{suffix} of
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1177
  premises of the case rule; within each premise, the \emph{prefix} of
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1178
  variables is instantiated.  In most situations, only a single term needs to
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1179
  be specified; this refers to the first variable of the last premise (it is
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1180
  usually the same for all cases).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1181
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1182
  The ``$(open)$'' option causes the parameters of the new local contexts to
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1183
  be exposed to the current proof context.  Thus local variables stemming from
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1184
  distant parts of the theory development may be introduced in an implicit
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1185
  manner, which can be quite confusing to the reader.  Furthermore, this
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1186
  option may cause unwanted hiding of existing local variables, resulting in
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1187
  less robust proof texts.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1188
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1189
\item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1190
  induction rules, which are determined as follows:
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1191
  \begin{matharray}{llll}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1192
    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1193
                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1194
    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1195
    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1196
  \end{matharray}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1197
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1198
  Several instantiations may be given, each referring to some part of a mutual
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1199
  inductive definition or datatype --- only related partial induction rules
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1200
  may be used together, though.  Any of the lists of terms $P, x, \dots$
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1201
  refers to the \emph{suffix} of variables present in the induction rule.
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1202
  This enables the writer to specify only induction variables, or both
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1203
  predicates and variables, for example.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1204
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1205
  The ``$(open)$'' option works the same way as for $cases$.
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1206
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1207
\end{descr}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1208
13048
wenzelm
parents: 13042
diff changeset
  1209
Above methods produce named local contexts, as determined by the instantiated
wenzelm
parents: 13042
diff changeset
  1210
rule as specified in the text.  Beyond that, the $induct$ method guesses
wenzelm
parents: 13042
diff changeset
  1211
further instantiations from the goal specification itself.  Any persisting
wenzelm
parents: 13042
diff changeset
  1212
unresolved schematic variables of the resulting rule will render the the
wenzelm
parents: 13042
diff changeset
  1213
corresponding case invalid.  The term binding $\Var{case}$\indexisarvar{case}
wenzelm
parents: 13042
diff changeset
  1214
for the conclusion will be provided with each case, provided that term is
wenzelm
parents: 13042
diff changeset
  1215
fully specified.
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1216
13048
wenzelm
parents: 13042
diff changeset
  1217
The $\isarkeyword{print_cases}$ command prints all named cases present in the
wenzelm
parents: 13042
diff changeset
  1218
current proof state.
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1219
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1220
\medskip
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1221
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1222
It is important to note that there is a fundamental difference of the $cases$
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1223
and $induct$ methods in handling of non-atomic goal statements: $cases$ just
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1224
applies a certain rule in backward fashion, splitting the result into new
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1225
goals with the local contexts being augmented in a purely monotonic manner.
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1226
13622
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1227
In contrast, $induct$ passes the full goal statement through the
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1228
``recursive'' course involved in the induction.  Thus the original statement
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1229
is basically replaced by separate copies, corresponding to the induction
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1230
hypotheses and conclusion; the original goal context is no longer available.
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1231
This behavior allows \emph{strengthened induction predicates} to be expressed
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1232
concisely as meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1233
\psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive''
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1234
assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1235
``$\FIX{\vec x}$''.  Also note that local definitions may be expressed as
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1236
$\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
9768ba6ab5e7 *** empty log message ***
nipkow
parents: 13617
diff changeset
  1237
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1238
13425
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13411
diff changeset
  1239
In induction proofs, local assumptions introduced by cases are split into two
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13411
diff changeset
  1240
different kinds: $hyps$ stemming from the rule and $prems$ from the goal
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13411
diff changeset
  1241
statement.  This is reflected in the extracted cases accordingly, so invoking
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13411
diff changeset
  1242
``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13411
diff changeset
  1243
$c\mathord.prems$, as well as fact $c$ to hold the all-inclusive list.
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13411
diff changeset
  1244
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1245
\medskip
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1246
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1247
Facts presented to either method are consumed according to the number of
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1248
``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}),
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1249
which is usually $0$ for plain cases and induction rules of datatypes etc.\
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1250
and $1$ for rules of inductive sets and the like.  The remaining facts are
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1251
inserted into the goal verbatim before the actual $cases$ or $induct$ rule is
43a97a2155d0 first stage of major update;
wenzelm
parents: 11691
diff changeset
  1252
applied (thus facts may be even passed through an induction).
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1253
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1254
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1255
\subsubsection{Declaring rules}\label{sec:cases-induct-att}
11691
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1256
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1257
\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1258
\begin{matharray}{rcl}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1259
  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1260
  cases & : & \isaratt \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1261
  induct & : & \isaratt \\
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1262
\end{matharray}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1263
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1264
\begin{rail}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1265
  'cases' spec
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1266
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1267
  'induct' spec
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1268
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1269
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1270
  spec: ('type' | 'set') ':' nameref
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1271
  ;
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1272
\end{rail}
fc9bd420162c induct/cases made generic, removed simplified/stripped options;
wenzelm
parents: 11469
diff changeset
  1273
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1274
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1275
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1276
\item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1277
  sets and types of the current context.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13040
diff changeset
  1278
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1279
\item [$cases$ and $induct$] (as attributes) augment the corresponding context
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1280
  of rules for reasoning about inductive sets and types, using the
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1281
  corresponding methods of the same name.  Certain definitional packages of
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1282
  object-logics usually declare emerging cases and induction rules as
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1283
  expected, so users rarely need to intervene.
13048
wenzelm
parents: 13042
diff changeset
  1284
  
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1285
  Manual rule declarations usually include the the $case_names$ and $ps$
0461b281c2b5 more stuff;
wenzelm
parents: 13015
diff changeset
  1286
  attributes to adjust na