doc-src/IsarRef/logics.tex
author haftmann
Mon, 10 Mar 2008 21:51:43 +0100
changeset 26245 00cbf41ba625
parent 25872 69c32d6a88c7
child 26746 b010007e9d31
permissions -rw-r--r--
fixed typo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     1
13048
wenzelm
parents: 13042
diff changeset
     2
\chapter{Object-logic specific elements}\label{ch:logics}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     3
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     4
\section{General logic setup}\label{sec:object-logic}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     5
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     6
\indexisarcmd{judgment}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     7
\indexisarmeth{atomize}\indexisaratt{atomize}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     8
\indexisaratt{rule-format}\indexisaratt{rulify}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     9
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    10
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    11
  \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    12
  atomize & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    13
  atomize & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    14
  rule_format & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    15
  rulify & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    16
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    17
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    18
The very starting point for any Isabelle object-logic is a ``truth judgment''
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    19
that links object-level statements to the meta-logic (with its minimal
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    20
language of $prop$ that covers universal quantification $\Forall$ and
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    21
implication $\Imp$).
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    22
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    23
Common object-logics are sufficiently expressive to internalize rule
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    24
statements over $\Forall$ and $\Imp$ within their own language.  This is
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    25
useful in certain situations where a rule needs to be viewed as an atomic
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    26
statement from the meta-level perspective, e.g.\ $\All x x \in A \Imp P(x)$
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    27
versus $\forall x \in A. P(x)$.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    28
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    29
From the following language elements, only the $atomize$ method and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    30
$rule_format$ attribute are occasionally required by end-users, the rest is
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    31
for those who need to setup their own object-logic.  In the latter case
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    32
existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    33
realistic examples.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    34
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    35
Generic tools may refer to the information provided by object-logic
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    36
declarations internally.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    37
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    38
\railalias{ruleformat}{rule\_format}
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    39
\railterm{ruleformat}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    40
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    41
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    42
  'judgment' constdecl
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    43
  ;
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    44
  'atomize' ('(' 'full' ')')?
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    45
  ;
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    46
  ruleformat ('(' 'noasm' ')')?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    47
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    48
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    49
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    50
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    51
  
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    52
\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] declares constant $c$ as the
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    53
  truth judgment of the current object-logic.  Its type $\sigma$ should
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    54
  specify a coercion of the category of object-level propositions to $prop$ of
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    55
  the Pure meta-logic; the mixfix annotation $(mx)$ would typically just link
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    56
  the object language (internally of syntactic category $logic$) with that of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    57
  $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    58
  theory development.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    59
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    60
\item [$atomize$] (as a method) rewrites any non-atomic premises of a
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    61
  sub-goal, using the meta-level equations declared via $atomize$ (as an
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    62
  attribute) beforehand.  As a result, heavily nested goals become amenable to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    63
  fundamental operations such as resolution (cf.\ the $rule$ method) and
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    64
  proof-by-assumption (cf.\ $assumption$).  Giving the ``$(full)$'' option
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
    65
  here means to turn the whole subgoal into an object-statement (if possible),
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    66
  including the outermost parameters and assumptions as well.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    67
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    68
  A typical collection of $atomize$ rules for a particular object-logic would
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    69
  provide an internalization for each of the connectives of $\Forall$, $\Imp$,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    70
  and $\equiv$.  Meta-level conjunction expressed in the manner of minimal
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    71
  higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    72
  should be covered as well (this is particularly important for locales, see
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    73
  \S\ref{sec:locale}).
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    74
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    75
\item [$rule_format$] rewrites a theorem by the equalities declared as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    76
  $rulify$ rules in the current object-logic.  By default, the result is fully
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    77
  normalized, including assumptions and conclusions at any depth.  The
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    78
  $no_asm$ option restricts the transformation to the conclusion of a rule.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    79
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    80
  In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    81
  replace (bounded) universal quantification ($\forall$) and implication
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    82
  ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    83
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    84
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    85
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    86
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    87
\section{HOL}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    88
13039
wenzelm
parents: 13027
diff changeset
    89
\subsection{Primitive types}\label{sec:hol-typedef}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    90
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    91
\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    92
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    93
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    94
  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    95
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    96
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    97
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
    98
  'typedecl' typespec infix?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    99
  ;
13443
1c3327c348b3 typedef: "open" option;
wenzelm
parents: 13049
diff changeset
   100
  'typedef' altname? abstype '=' repset
13016
wenzelm
parents: 13014
diff changeset
   101
  ;
wenzelm
parents: 13014
diff changeset
   102
13444
4cfead92f8f7 fixed railroads;
wenzelm
parents: 13443
diff changeset
   103
  altname: '(' (name | 'open' | 'open' name) ')'
13443
1c3327c348b3 typedef: "open" option;
wenzelm
parents: 13049
diff changeset
   104
  ;
13016
wenzelm
parents: 13014
diff changeset
   105
  abstype: typespec infix?
wenzelm
parents: 13014
diff changeset
   106
  ;
wenzelm
parents: 13014
diff changeset
   107
  repset: term ('morphisms' name name)?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   108
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   109
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   110
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   111
\begin{descr}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   112
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   113
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   114
  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   115
  also declares type arity $t :: (type, \dots, type) type$, making $t$ an
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   116
  actual HOL type constructor.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   117
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   118
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   119
  non-emptiness of the set $A$.  After finishing the proof, the theory will be
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   120
  augmented by a Gordon/HOL-style type definition, which establishes a
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   121
  bijection between the representing set $A$ and the new type $t$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   122
  
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   123
  Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
13016
wenzelm
parents: 13014
diff changeset
   124
  constant) of the same name (an alternative base name may be given in
wenzelm
parents: 13014
diff changeset
   125
  parentheses).  The injection from type to set is called $Rep_t$, its inverse
wenzelm
parents: 13014
diff changeset
   126
  $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
wenzelm
parents: 13014
diff changeset
   127
  declaration).
wenzelm
parents: 13014
diff changeset
   128
  
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   129
  Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   130
  basic characterization as a corresponding injection/surjection pair (in both
13016
wenzelm
parents: 13014
diff changeset
   131
  directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   132
  more convenient view on the injectivity part, suitable for automated proof
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   133
  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   134
  $Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   135
  alternative views on surjectivity; these are already declared as set or type
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   136
  rules for the generic $cases$ and $induct$ methods.
13443
1c3327c348b3 typedef: "open" option;
wenzelm
parents: 13049
diff changeset
   137
  
1c3327c348b3 typedef: "open" option;
wenzelm
parents: 13049
diff changeset
   138
  An alternative name may be specified in parentheses; the default is to use
1c3327c348b3 typedef: "open" option;
wenzelm
parents: 13049
diff changeset
   139
  $t$ as indicated before.  The $open$ declaration suppresses a separate
1c3327c348b3 typedef: "open" option;
wenzelm
parents: 13049
diff changeset
   140
  constant definition for the representing set.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   141
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   142
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   143
Note that raw type declarations are rarely used in practice; the main
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   144
application is with experimental (or even axiomatic!) theory fragments.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   145
Instead of primitive HOL type definitions, user-level theories usually refer
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   146
to higher-level packages such as $\isarkeyword{record}$ (see
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   147
\S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   148
\S\ref{sec:hol-datatype}).
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   149
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   150
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   151
\subsection{Adhoc tuples}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   152
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   153
\indexisarattof{HOL}{split-format}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   154
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   155
  split_format^* & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   156
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   157
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   158
\railalias{splitformat}{split\_format}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   159
\railterm{splitformat}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   160
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   161
\begin{rail}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   162
  splitformat (((name *) + 'and') | ('(' 'complete' ')'))
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   163
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   164
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   165
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   166
\begin{descr}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   167
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   168
\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   169
  tuple types into canonical form as specified by the arguments given; $\vec
13049
wenzelm
parents: 13048
diff changeset
   170
  p@i$ refers to occurrences in premise $i$ of the rule.  The ``$(complete)$''
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   171
  option causes \emph{all} arguments in function applications to be
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   172
  represented canonically according to their tuple type structure.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   173
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   174
  Note that these operations tend to invent funny names for new local
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   175
  parameters to be introduced.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   176
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   177
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   178
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   179
13039
wenzelm
parents: 13027
diff changeset
   180
\subsection{Records}\label{sec:hol-record}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   181
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   182
In principle, records merely generalize the concept of tuples, where
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   183
components may be addressed by labels instead of just position.  The logical
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   184
infrastructure of records in Isabelle/HOL is slightly more advanced, though,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   185
supporting truly extensible record schemes.  This admits operations that are
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   186
polymorphic with respect to record extension, yielding ``object-oriented''
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   187
effects like (single) inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   188
more details on object-oriented verification and record subtyping in HOL.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   189
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   190
13039
wenzelm
parents: 13027
diff changeset
   191
\subsubsection{Basic concepts}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   192
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   193
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   194
level of terms and types.  The notation is as follows:
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   195
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   196
\begin{center}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   197
\begin{tabular}{l|l|l}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   198
  & record terms & record types \\ \hline
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   199
  fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   200
  schematic & $\record{x = a\fs y = b\fs \more = m}$ &
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   201
    $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   202
\end{tabular}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   203
\end{center}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   204
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   205
\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   206
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   207
A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   208
$y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   209
assuming that $a \ty A$ and $b \ty B$.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   210
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   211
A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   212
$x$ and $y$ as before, but also possibly further fields as indicated by the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   213
``$\more$'' notation (which is actually part of the syntax).  The improper
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   214
field ``$\more$'' of a record scheme is called the \emph{more part}.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   215
Logically it is just a free variable, which is occasionally referred to as
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   216
``row variable'' in the literature.  The more part of a record scheme may be
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   217
instantiated by zero or more further components.  For example, the previous
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   218
scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more =
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   219
  m'}$, where $m'$ refers to a different more part.  Fixed records are special
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   220
instances of record schemes, where ``$\more$'' is properly terminated by the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   221
$() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   222
abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   223
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   224
\medskip
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   225
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   226
Two key observations make extensible records in a simply typed language like
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   227
HOL feasible:
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   228
\begin{enumerate}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   229
\item the more part is internalized, as a free term or type variable,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   230
\item field names are externalized, they cannot be accessed within the logic
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   231
  as first-class values.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   232
\end{enumerate}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   233
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   234
\medskip
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   235
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   236
In Isabelle/HOL record types have to be defined explicitly, fixing their field
13042
wenzelm
parents: 13041
diff changeset
   237
names and types, and their (optional) parent record.  Afterwards, records may
wenzelm
parents: 13041
diff changeset
   238
be formed using above syntax, while obeying the canonical order of fields as
wenzelm
parents: 13041
diff changeset
   239
given by their declaration.  The record package provides several standard
wenzelm
parents: 13041
diff changeset
   240
operations like selectors and updates.  The common setup for various generic
wenzelm
parents: 13041
diff changeset
   241
proof tools enable succinct reasoning patterns.  See also the Isabelle/HOL
wenzelm
parents: 13041
diff changeset
   242
tutorial \cite{isabelle-hol-book} for further instructions on using records in
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   243
practice.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   244
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   245
13042
wenzelm
parents: 13041
diff changeset
   246
\subsubsection{Record specifications}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   247
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   248
\indexisarcmdof{HOL}{record}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   249
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   250
  \isarcmd{record} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   251
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   252
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   253
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   254
  'record' typespec '=' (type '+')? (constdecl +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   255
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   256
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   257
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   258
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   259
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   260
  defines extensible record type $(\vec\alpha)t$, derived from the optional
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   261
  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   262
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   263
  The type variables of $\tau$ and $\vec\sigma$ need to be covered by the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   264
  (distinct) parameters $\vec\alpha$.  Type constructor $t$ has to be new,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   265
  while $\tau$ needs to specify an instance of an existing record type.  At
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   266
  least one new field $\vec c$ has to be specified.  Basically, field names
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   267
  need to belong to a unique record.  This is not a real restriction in
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   268
  practice, since fields are qualified by the record name internally.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   269
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   270
  The parent record specification $\tau$ is optional; if omitted $t$ becomes a
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   271
  root record.  The hierarchy of all records declared within a theory context
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   272
  forms a forest structure, i.e.\ a set of trees starting with a root record
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   273
  each.  There is no way to merge multiple parent records!
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   274
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   275
  For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   276
  fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   277
  $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   278
    \ty \vec\sigma\fs \more \ty \zeta}$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   279
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   280
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   281
13042
wenzelm
parents: 13041
diff changeset
   282
\subsubsection{Record operations}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   283
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   284
Any record definition of the form presented above produces certain standard
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   285
operations.  Selectors and updates are provided for any field, including the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   286
improper one ``$more$''.  There are also cumulative record constructor
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   287
functions.  To simplify the presentation below, we assume for now that
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   288
$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   289
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   290
\medskip \textbf{Selectors} and \textbf{updates} are available for any field
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   291
(including ``$more$''):
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   292
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   293
  c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   294
  c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   295
    \record{\vec c \ty \vec\sigma, \more \ty \zeta}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   296
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   297
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   298
There is special syntax for application of updates: $r \, \record{x \asn a}$
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   299
abbreviates term $x_update \, a \, r$.  Further notation for repeated updates
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   300
is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   301
  \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   302
Note that because of postfix notation the order of fields shown here is
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   303
reverse than in the actual term.  Since repeated updates are just function
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   304
applications, fields may be freely permuted in $\record{x \asn a\fs y \asn
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   305
  b\fs z \asn c}$, as far as logical equality is concerned.  Thus
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   306
commutativity of independent updates can be proven within the logic for any
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   307
two fields, but not as a general theorem.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   308
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   309
\medskip The \textbf{make} operation provides a cumulative record constructor
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   310
function:
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   311
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   312
  t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   313
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   314
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   315
\medskip We now reconsider the case of non-root records, which are derived of
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   316
some parent.  In general, the latter may depend on another parent as well,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   317
resulting in a list of \emph{ancestor records}.  Appending the lists of fields
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   318
of all ancestors results in a certain field prefix.  The record package
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   319
automatically takes care of this by lifting operations over this context of
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   320
ancestor fields.  Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   321
b \ty \vec\rho$, the above record operations will get the following types:
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   322
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   323
  c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   324
    \zeta} \To \sigma@i \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   325
  c@i_update & \ty & \sigma@i \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   326
    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   327
    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   328
  t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   329
    \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   330
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   331
\noindent
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   332
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   333
\medskip Some further operations address the extension aspect of a derived
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   334
record scheme specifically: $fields$ produces a record fragment consisting of
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   335
exactly the new fields introduced here (the result may serve as a more part
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   336
elsewhere); $extend$ takes a fixed record and adds a given more part;
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   337
$truncate$ restricts a record scheme to a fixed record.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   338
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   339
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   340
  t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   341
  t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   342
    \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   343
  t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   344
    \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   345
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   346
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   347
\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   348
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   349
13042
wenzelm
parents: 13041
diff changeset
   350
\subsubsection{Derived rules and proof tools}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   351
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   352
The record package proves several results internally, declaring these facts to
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   353
appropriate proof tools.  This enables users to reason about record structures
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   354
quite conveniently.  Assume that $t$ is a record type as specified above.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   355
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   356
\begin{enumerate}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   357
  
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   358
\item Standard conversions for selectors or updates applied to record
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   359
  constructor terms are made part of the default Simplifier context; thus
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   360
  proofs by reduction of basic operations merely require the $simp$ method
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   361
  without further arguments.  These rules are available as $t{\dtt}simps$,
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   362
  too.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   363
  
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   364
\item Selectors applied to updated records are automatically reduced by an
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   365
  internal simplification procedure, which is also part of the standard
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   366
  Simplifier setup.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   367
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   368
\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   369
  \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   370
  rules.  These rules are available as $t{\dtt}iffs$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   371
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   372
\item The introduction rule for record equality analogous to $x~r = x~r' \Imp
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   373
  y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   374
  basic rule context as ``$intro?$''.  The rule is called $t{\dtt}equality$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   375
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   376
\item Representations of arbitrary record expressions as canonical constructor
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   377
  terms are provided both in $cases$ and $induct$ format (cf.\ the generic
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   378
  proof methods of the same name, \S\ref{sec:cases-induct}).  Several
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   379
  variations are available, for fixed records, record schemes, more parts etc.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   380
  
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   381
  The generic proof methods are sufficiently smart to pick the most sensible
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   382
  rule according to the type of the indicated record expression: users just
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   383
  need to apply something like ``$(cases~r)$'' to a certain proof problem.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   384
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   385
\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   386
  $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   387
  usually need to be expanded by hand, using the collective fact
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   388
  $t{\dtt}defs$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   389
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   390
\end{enumerate}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   391
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   392
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   393
\subsection{Datatypes}\label{sec:hol-datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   394
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   395
\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   396
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   397
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   398
  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   399
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   400
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   401
\railalias{repdatatype}{rep\_datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   402
\railterm{repdatatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   403
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   404
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   405
  'datatype' (dtspec + 'and')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   406
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   407
  repdatatype (name *) dtrules
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   408
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   409
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   410
  dtspec: parname? typespec infix? '=' (cons + '|')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   411
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   412
  cons: name (type *) mixfix?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   413
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   414
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   415
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   416
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   417
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   418
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   419
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   420
  ones, generating the standard infrastructure of derived concepts (primitive
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   421
  recursion etc.).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   422
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   423
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   424
The induction and exhaustion theorems generated provide case names according
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   425
to the constructors involved, while parameters are named after the types (see
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   426
also \S\ref{sec:cases-induct}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   427
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   428
See \cite{isabelle-HOL} for more details on datatypes, but beware of the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   429
old-style theory syntax being used there!  Apart from proper proof methods for
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   430
case-analysis and induction, there are also emulations of ML tactics
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   431
\texttt{case_tac} and \texttt{induct_tac} available, see
13042
wenzelm
parents: 13041
diff changeset
   432
\S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal
wenzelm
parents: 13041
diff changeset
   433
structure of subgoals (including internally bound parameters).
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   434
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   435
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   436
\subsection{Recursive functions}\label{sec:recursion}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   437
25872
haftmann
parents: 24992
diff changeset
   438
\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{fun}\indexisarcmdof{HOL}{function}\indexisarcmdof{HOL}{termination}
24524
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   439
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   440
\begin{matharray}{rcl}
25872
haftmann
parents: 24992
diff changeset
   441
  \isarcmd{primrec} & : & \isarkeep{local{\dsh}theory} \\
haftmann
parents: 24992
diff changeset
   442
  \isarcmd{fun} & : & \isarkeep{local{\dsh}theory} \\
haftmann
parents: 24992
diff changeset
   443
  \isarcmd{function} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
haftmann
parents: 24992
diff changeset
   444
  \isarcmd{termination} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
24524
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   445
\end{matharray}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   446
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   447
\railalias{funopts}{function\_opts}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   448
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   449
\begin{rail}
25872
haftmann
parents: 24992
diff changeset
   450
  'primrec' target? fixes 'where' equations
24524
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   451
  ;
25872
haftmann
parents: 24992
diff changeset
   452
  equations: (thmdecl? prop + '|')
24524
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   453
  ;
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   454
  ('fun' | 'function') (funopts)? fixes 'where' clauses
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   455
  ;
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   456
  clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   457
  ;
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   458
  funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   459
  'default' term) + ',') ')'
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   460
  ;
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   461
  'termination' ( term )?
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   462
\end{rail}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   463
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   464
\begin{descr}
25872
haftmann
parents: 24992
diff changeset
   465
24524
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   466
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   467
  datatypes, see also \cite{isabelle-HOL}.
25872
haftmann
parents: 24992
diff changeset
   468
24524
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   469
\item [$\isarkeyword{function}$] defines functions by general
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   470
  wellfounded recursion. A detailed description with examples can be
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   471
  found in \cite{isabelle-function}. The function is specified by a
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   472
  set of (possibly conditional) recursive equations with arbitrary
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   473
  pattern matching. The command generates proof obligations for the
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   474
  completeness and the compatibility of patterns.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   475
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   476
  The defined function is considered partial, and the resulting
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   477
  simplification rules (named $f.psimps$) and induction rule (named
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   478
  $f.pinduct$) are guarded by a generated domain predicate $f_dom$. 
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   479
  The $\isarkeyword{termination}$ command can then be used to establish
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   480
  that the function is total.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   481
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   482
\item [$\isarkeyword{fun}$] is a shorthand notation for
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   483
  $\isarkeyword{function}~(\textit{sequential})$, followed by automated
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   484
  proof attemts regarding pattern matching and termination. For
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   485
  details, see \cite{isabelle-function}.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   486
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   487
\item [$\isarkeyword{termination}$~f] commences a termination proof
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   488
  for the previously defined function $f$. If no name is given, it
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   489
  refers to the most recent function definition. After the proof is
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   490
  closed, the recursive equations and the induction principle is established.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   491
\end{descr}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   492
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   493
Recursive definitions introduced by both the $\isarkeyword{primrec}$
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   494
and the $\isarkeyword{function}$ command accommodate reasoning by
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   495
induction (cf.\ \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   496
(where $c$ is the name of the function definition) refers to a
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   497
specific induction rule, with parameters named according to the
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   498
user-specified equations.  Case names of $\isarkeyword{primrec}$ are
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   499
that of the datatypes involved, while those of
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   500
$\isarkeyword{function}$ are numbered (starting from $1$).
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   501
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   502
The equations provided by these packages may be referred later as theorem list
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   503
$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   504
Individual equations may be named explicitly as well.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   505
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   506
The $\isarkeyword{function}$ command accepts the following options:
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   507
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   508
\begin{descr}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   509
\item [\emph{sequential}] enables a preprocessor which disambiguates
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   510
  overlapping patterns by making them mutually disjoint. Earlier
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   511
  equations take precedence over later ones. This allows to give the
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   512
  specification in a format very similar to functional programming.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   513
  Note that the resulting simplification and induction rules
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   514
  correspond to the transformed specification, not the one given
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   515
  originally. This usually means that each equation given by the user
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   516
  may result in several theroems.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   517
  Also note that this automatic transformation only works
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   518
  for ML-style datatype patterns.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   519
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   520
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   521
\item [\emph{in name}] gives the target for the definition.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   522
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   523
\item [\emph{domintros}] enables the automated generation of
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   524
  introduction rules for the domain predicate. While mostly not
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   525
  needed, they can be helpful in some proofs about partial functions.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   526
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   527
\item [\emph{tailrec}] generates the unconstrained recursive equations
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   528
  even without a termination proof, provided that the function is
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   529
  tail-recursive. This currently only works 
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   530
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   531
\item [\emph{default d}] allows to specify a default value for a
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   532
  (partial) function, which will ensure that $f(x)=d(x)$ whenever $x
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   533
  \notin \textit{f\_dom}$. This feature is experimental.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   534
\end{descr}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   535
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   536
\subsubsection{Proof methods related to recursive definitions}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   537
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   538
\indexisarmethof{HOL}{pat\_completeness}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   539
\indexisarmethof{HOL}{relation}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   540
\indexisarmethof{HOL}{lexicographic\_order}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   541
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   542
\begin{matharray}{rcl}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   543
  pat\_completeness & : & \isarmeth \\
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   544
  relation & : & \isarmeth \\
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   545
  lexicographic\_order & : & \isarmeth \\
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   546
\end{matharray}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   547
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   548
\begin{rail}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   549
  'pat\_completeness'
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   550
  ;
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   551
  'relation' term
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   552
  ;
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   553
  'lexicographic\_order' clasimpmod
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   554
\end{rail}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   555
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   556
\begin{descr}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   557
\item [\emph{pat\_completeness}] Specialized method to solve goals
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   558
  regarding the completeness of pattern matching, as required by the
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   559
  $\isarkeyword{function}$ package (cf.~\cite{isabelle-function}).
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   560
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   561
\item [\emph{relation R}] Introduces a termination proof using the
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   562
  relation $R$. The resulting proof state will contain goals
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   563
  expressing that $R$ is wellfounded, and that the arguments
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   564
  of recursive calls decrease with respect to $R$. Usually, this
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   565
  method is used as the initial proof step of manual termination
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   566
  proofs.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   567
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   568
\item [\emph{lexicographic\_order}] Attempts a fully automated
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   569
  termination proof by searching for a lexicographic combination of
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   570
  size measures on the arguments of the function. The method
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   571
  accepts the same arguments as the \emph{auto} method, which it uses
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   572
  internally to prove local descents. Hence, modifiers like
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   573
  \emph{simp}, \emph{intro} etc.\ can be used to add ``hints'' for the
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   574
  automated proofs. In case of failure, extensive information is
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   575
  printed, which can help to analyse the failure (cf.~\cite{isabelle-function}).
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   576
\end{descr}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   577
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   578
\subsubsection{Legacy recursion package}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   579
\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   580
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   581
The use of the legacy $\isarkeyword{recdef}$ command is now deprecated
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   582
in favour of $\isarkeyword{function}$ and $\isarkeyword{fun}$.
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   583
6892fdc7e9f8 Documented function package in IsarRef-manual.
krauss
parents: 24482
diff changeset
   584
\begin{matharray}{rcl}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   585
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   586
  \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   587
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   588
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   589
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   590
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   591
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   592
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   593
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   594
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   595
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   596
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   597
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   598
\railalias{recdeftc}{recdef\_tc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   599
\railterm{recdeftc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   600
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   601
\begin{rail}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   602
  'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   603
  ;
12879
wenzelm
parents: 12621
diff changeset
   604
  recdeftc thmdecl? tc
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   605
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   606
  hints: '(' 'hints' (recdefmod *) ')'
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   607
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   608
  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   609
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   610
  tc: nameref ('(' nat ')')?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   611
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   612
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   613
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   614
\begin{descr}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   615
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   616
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   617
  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   618
  ``$(permissive)$'' option tells TFL to recover from failed proof attempts,
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   619
  returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   620
  $recdef_wf$ hints refer to auxiliary rules to be used in the internal
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   621
  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   622
  \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   623
  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   624
  \S\ref{sec:classical}).
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   625
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   626
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   627
  termination condition number $i$ (default $1$) as generated by a
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   628
  $\isarkeyword{recdef}$ definition of constant $c$.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   629
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   630
  Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   631
  internal proofs without manual intervention.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   632
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   633
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   634
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   635
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   636
the following attributes.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   637
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   638
\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   639
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   640
  recdef_simp & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   641
  recdef_cong & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   642
  recdef_wf & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   643
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   644
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   645
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   646
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   647
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   648
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   649
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   650
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   651
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   652
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   653
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   654
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   655
  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   656
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   657
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   658
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   659
\subsection{Definition by specification}\label{sec:hol-specification}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   660
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   661
\indexisarcmdof{HOL}{specification}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   662
\begin{matharray}{rcl}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   663
  \isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\
14619
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   664
  \isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   665
\end{matharray}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   666
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   667
\begin{rail}
14619
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   668
('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   669
;
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14619
diff changeset
   670
decl: ((name ':')? term '(' 'overloaded' ')'?)
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   671
\end{rail}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   672
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   673
\begin{descr}
14165
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
   674
\item [$\isarkeyword{specification}~decls~\phi$] sets up a goal stating
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
   675
  the existence of terms with the properties specified to hold for the
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
   676
  constants given in $\mathit{decls}$.  After finishing the proof, the
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
   677
  theory will be augmented with definitions for the given constants,
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
   678
  as well as with theorems stating the properties for these constants.
14619
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   679
\item [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   680
  the existence of terms with the properties specified to hold for the
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   681
  constants given in $\mathit{decls}$.  After finishing the proof, the
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   682
  theory will be augmented with axioms expressing the properties given
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   683
  in the first place.
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   684
\item[$decl$] declares a constant to be defined by the specification
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   685
  given.  The definition for the constant $c$ is bound to the name
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   686
  $c$\_def unless a theorem name is given in the declaration.
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   687
  Overloaded constants should be declared as such.
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   688
\end{descr}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   689
14619
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   690
Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   691
is to some extent a matter of style.  $\isarkeyword{specification}$ introduces no new axioms,
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   692
and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{ax_specification}$
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   693
does introduce axioms, but only after the user has explicitly proven it to be
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   694
safe.  A practical issue must be considered, though: After introducing two constants
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   695
with the same properties using $\isarkeyword{specification}$, one can prove
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   696
that the two constants are, in fact, equal.  If this might be a problem,
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   697
one should use $\isarkeyword{ax_specification}$.
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   698
24477
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   699
\subsection{Inductive and coinductive definitions}\label{sec:hol-inductive}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   700
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   701
An {\bf inductive definition} specifies the least predicate (or set) $R$ closed under given
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   702
rules.  (Applying a rule to elements of~$R$ yields a result within~$R$.)  For
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   703
example, a structural operational semantics is an inductive definition of an
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   704
evaluation relation.  Dually, a {\bf coinductive definition} specifies the
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   705
greatest predicate (or set) $R$ consistent with given rules.  (Every element of~$R$ can be
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   706
seen as arising by applying a rule to elements of~$R$.)  An important example
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   707
is using bisimulation relations to formalise equivalence of processes and
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   708
infinite data structures.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   709
24477
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   710
This package is related to the ZF one, described in a separate
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   711
paper,%
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   712
\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   713
  distributed with Isabelle.}  %
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   714
which you should refer to in case of difficulties.  The package is simpler
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   715
than ZF's thanks to HOL's extra-logical automatic type-checking.  The types of
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   716
the (co)inductive predicates (or sets) determine the domain of the fixedpoint definition, and
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   717
the package does not have to use inference rules for type-checking.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   718
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   719
\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductive-set}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductive-set}\indexisarattof{HOL}{mono}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   720
\begin{matharray}{rcl}
25872
haftmann
parents: 24992
diff changeset
   721
  \isarcmd{inductive} & : & \isarkeep{local{\dsh}theory} \\
haftmann
parents: 24992
diff changeset
   722
  \isarcmd{inductive_set} & : & \isarkeep{local{\dsh}theory} \\
haftmann
parents: 24992
diff changeset
   723
  \isarcmd{coinductive} & : & \isarkeep{local{\dsh}theory} \\
haftmann
parents: 24992
diff changeset
   724
  \isarcmd{coinductive_set} & : & \isarkeep{local{\dsh}theory} \\
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   725
  mono & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   726
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   727
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   728
\begin{rail}
24482
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   729
  ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   730
  ('where' clauses)? ('monos' thmrefs)?
24477
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   731
  ;
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   732
  clauses: (thmdecl? prop + '|')
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   733
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   734
  'mono' (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   735
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   736
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   737
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   738
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   739
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
24477
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   740
  (co)inductive predicates from the introduction rules given in the \texttt{where} section.
24482
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   741
  The optional \texttt{for} section contains a list of parameters of the (co)inductive
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   742
  predicates that remain fixed throughout the definition.
24477
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   743
  The optional \texttt{monos} section contains \textit{monotonicity theorems},
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   744
  which are required for each operator applied to a recursive set in the introduction rules.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   745
  There {\bf must} be a theorem of the form $A \leq B \Imp M~A \leq M~B$, for each
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   746
  premise $M~R@i~t$ in an introduction rule!
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   747
\item [$\isarkeyword{inductive_set}$ and $\isarkeyword{coinductive_set}$] are wrappers
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   748
  for to the previous commands, allowing the definition of (co)inductive sets.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   749
\item [$mono$] declares monotonicity rules.  These rule are involved in the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   750
  automated monotonicity proof of $\isarkeyword{inductive}$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   751
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   752
24477
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   753
\subsubsection{Derived rules}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   754
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   755
Each (co)inductive definition $R$ adds definitions to the theory and also
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   756
proves some theorems:
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   757
\begin{description}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   758
\item[$R{\dtt}intros$] is the list of introduction rules, now proved as theorems, for
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   759
the recursive predicates (or sets).  The rules are also available individually,
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   760
using the names given them in the theory file.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   761
\item[$R{\dtt}cases$] is the case analysis (or elimination) rule.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   762
\item[$R{\dtt}(co)induct$] is the (co)induction rule.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   763
\end{description}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   764
When several predicates $R@1$, $\ldots$, $R@n$ are defined simultaneously,
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   765
the list of introduction rules is called $R@1_\ldots_R@n{\dtt}intros$, the
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   766
case analysis rules are called $R@1{\dtt}cases$, $\ldots$, $R@n{\dtt}cases$, and
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   767
the list of mutual induction rules is called $R@1_\ldots_R@n{\dtt}inducts$.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   768
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   769
\subsubsection{Monotonicity theorems}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   770
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   771
Each theory contains a default set of theorems that are used in monotonicity
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   772
proofs. New rules can be added to this set via the $mono$ attribute.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   773
Theory \texttt{Inductive} shows how this is done. In general, the following
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   774
monotonicity theorems may be added:
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   775
\begin{itemize}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   776
\item Theorems of the form $A \leq B \Imp M~A \leq M~B$, for proving
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   777
  monotonicity of inductive definitions whose introduction rules have premises
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   778
  involving terms such as $M~R@i~t$.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   779
\item Monotonicity theorems for logical operators, which are of the general form
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   780
  $\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   781
    \cdots \to \cdots$.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   782
  For example, in the case of the operator $\lor$, the corresponding theorem is
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   783
  \[
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   784
  \infer{P@1 \lor P@2 \to Q@1 \lor Q@2}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   785
    {P@1 \to Q@1 & P@2 \to Q@2}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   786
  \]
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   787
\item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   788
  \[
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   789
  (\lnot \lnot P) ~=~ P \qquad\qquad
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   790
  (\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q)
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   791
  \]
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   792
\item Equations for reducing complex operators to more primitive ones whose
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   793
  monotonicity can easily be proved, e.g.
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   794
  \[
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   795
  (P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   796
  \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   797
  \]
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   798
\end{itemize}
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   799
f45e301b9e5c Updated section about inductive definitions.
berghofe
parents: 24348
diff changeset
   800
%FIXME: Example of an inductive definition
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   801
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   802
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   803
\subsection{Arithmetic proof support}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   804
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   805
\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   806
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   807
  arith & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   808
  arith_split & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   809
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   810
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   811
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   812
  'arith' '!'?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   813
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   814
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   815
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   816
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   817
$real$).  Any current facts are inserted into the goal before running the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   818
procedure.  The ``!''~argument causes the full context of assumptions to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   819
included.  The $arith_split$ attribute declares case split rules to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   820
expanded before the arithmetic procedure is invoked.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   821
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   822
Note that a simpler (but faster) version of arithmetic reasoning is already
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   823
performed by the Simplifier.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   824
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   825
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   826
\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   827
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   828
The following important tactical tools of Isabelle/HOL have been ported to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   829
Isar.  These should be never used in proper proof texts!
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   830
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   831
\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   832
\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   833
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   834
  case_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   835
  induct_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   836
  ind_cases^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   837
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   838
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   839
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   840
\railalias{casetac}{case\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   841
\railterm{casetac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   842
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   843
\railalias{inducttac}{induct\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   844
\railterm{inducttac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   845
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   846
\railalias{indcases}{ind\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   847
\railterm{indcases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   848
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   849
\railalias{inductivecases}{inductive\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   850
\railterm{inductivecases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   851
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   852
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   853
  casetac goalspec? term rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   854
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   855
  inducttac goalspec? (insts * 'and') rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   856
  ;
24482
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   857
  indcases (prop +) ('for' (name +)) ?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   858
  ;
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   859
  inductivecases (thmdecl? (prop +) + 'and')
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   860
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   861
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   862
  rule: ('rule' ':' thmref)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   863
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   864
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   865
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   866
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   867
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   868
  only (unless an alternative rule is given explicitly).  Furthermore,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   869
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   870
  variables to be given as instantiation.  These tactic emulations feature
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   871
  both goal addressing and dynamic instantiation.  Note that named rule cases
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   872
  are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   873
  methods (see \S\ref{sec:cases-induct}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   874
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   875
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   876
  to the internal \texttt{mk_cases} operation.  Rules are simplified in an
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   877
  unrestricted forward manner.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   878
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   879
  While $ind_cases$ is a proof method to apply the result immediately as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   880
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
24482
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   881
  theorems at the theory level for later use.
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   882
  The \texttt{for} option of the $ind_cases$ method allows to specify a list
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   883
  of variables that should be generalized before applying the resulting rule.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   884
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   885
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   886
13039
wenzelm
parents: 13027
diff changeset
   887
\subsection{Executable code}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   888
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   889
Isabelle/Pure provides two generic frameworks to support code
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   890
generation from executable specifications. Isabelle/HOL
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   891
instantiates these mechanisms in a
26245
00cbf41ba625 fixed typo
haftmann
parents: 25872
diff changeset
   892
way that is amenable to end-user applications.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   893
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   894
One framework generates code from both functional and
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   895
relational programs to SML.  See
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   896
\cite{isabelle-HOL} for further information (this actually covers the
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   897
new-style theory format as well).
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   898
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   899
\indexisarcmd{value}\indexisarcmd{code-module}\indexisarcmd{code-library}
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   900
\indexisarcmd{consts-code}\indexisarcmd{types-code}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   901
\indexisaratt{code}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   902
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   903
\begin{matharray}{rcl}
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   904
  \isarcmd{value}^* & : & \isarkeep{theory~|~proof} \\
17659
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   905
  \isarcmd{code_module} & : & \isartrans{theory}{theory} \\
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   906
  \isarcmd{code_library} & : & \isartrans{theory}{theory} \\
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   907
  \isarcmd{consts_code} & : & \isartrans{theory}{theory} \\
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   908
  \isarcmd{types_code} & : & \isartrans{theory}{theory} \\  
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   909
  code & : & \isaratt \\
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   910
\end{matharray}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   911
17659
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   912
\railalias{verblbrace}{\texttt{\ttlbrace*}}
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   913
\railalias{verbrbrace}{\texttt{*\ttrbrace}}
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   914
\railterm{verblbrace}
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   915
\railterm{verbrbrace}
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   916
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   917
\begin{rail}
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   918
'value' term;
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   919
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   920
( 'code\_module' | 'code\_library' ) modespec ? name ? \\
17659
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   921
  ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   922
  'contains' ( ( name '=' term ) + | term + );
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   923
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   924
modespec : '(' ( name * ) ')';
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   925
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   926
'consts\_code' (codespec +);
17659
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   927
22921
475ff421a6a3 consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents: 22845
diff changeset
   928
codespec : const template attachment ?;
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   929
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   930
'types\_code' (tycodespec +);
17659
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   931
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   932
tycodespec : name template attachment ?;
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   933
22921
475ff421a6a3 consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents: 22845
diff changeset
   934
const: term;
475ff421a6a3 consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents: 22845
diff changeset
   935
17659
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   936
template: '(' string ')';
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   937
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   938
attachment: 'attach' modespec ? verblbrace text verbrbrace;
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   939
b1019337c857 Updated description of code generator.
berghofe
parents: 14682
diff changeset
   940
'code' (name)?;
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   941
\end{rail}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   942
19988
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   943
\begin{descr}
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   944
\item [$\isarkeyword{value}~t$] reads, evaluates and prints a term
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   945
  using the code generator.
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   946
\end{descr}
05f940b9ef15 added 'value';
wenzelm
parents: 17659
diff changeset
   947
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   948
The other framework generates code from functional programs
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
   949
(including overloading using type classes) to SML \cite{SML},
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
   950
OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   951
Conceptually, code generation is split up in three steps: \emph{selection}
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   952
of code theorems, \emph{translation} into an abstract executable view
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   953
and \emph{serialization} to a specific \emph{target language}.
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   954
See \cite{isabelle-codegen} for an introduction on how to use it.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   955
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
   956
\indexisarcmd{export-code}
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   957
\indexisarcmd{code-thms}
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   958
\indexisarcmd{code-deps}
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   959
\indexisarcmd{code-datatype}
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   960
\indexisarcmd{code-const}
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   961
\indexisarcmd{code-type}
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   962
\indexisarcmd{code-class}
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   963
\indexisarcmd{code-instance}
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
   964
\indexisarcmd{code-monad}
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   965
\indexisarcmd{code-reserved}
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
   966
\indexisarcmd{code-include}
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   967
\indexisarcmd{code-modulename}
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
   968
\indexisarcmd{code-exception}
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
   969
\indexisarcmd{print-codesetup}
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   970
\indexisaratt{code func}
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   971
\indexisaratt{code inline}
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   972
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   973
\begin{matharray}{rcl}
24348
c708ea5b109a renamed code_gen to export_code
haftmann
parents: 24248
diff changeset
   974
  \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   975
  \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   976
  \isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   977
  \isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   978
  \isarcmd{code_const} & : & \isartrans{theory}{theory} \\
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   979
  \isarcmd{code_type} & : & \isartrans{theory}{theory} \\
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   980
  \isarcmd{code_class} & : & \isartrans{theory}{theory} \\
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   981
  \isarcmd{code_instance} & : & \isartrans{theory}{theory} \\
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
   982
  \isarcmd{code_monad} & : & \isartrans{theory}{theory} \\
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   983
  \isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
   984
  \isarcmd{code_include} & : & \isartrans{theory}{theory} \\
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
   985
  \isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
   986
  \isarcmd{code_exception} & : & \isartrans{theory}{theory} \\
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
   987
  \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   988
  code\ func & : & \isaratt \\
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   989
  code\ inline & : & \isaratt \\
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   990
\end{matharray}
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   991
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
   992
\begin{rail}
24348
c708ea5b109a renamed code_gen to export_code
haftmann
parents: 24248
diff changeset
   993
'export\_code' ( constexpr + ) ? \\
24482
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   994
  ( ( 'in' target ( 'module\_name' string ) ? \\
5edb9a54900f - tuned section about inductive predicates
berghofe
parents: 24477
diff changeset
   995
      ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   996
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   997
'code\_thms' ( constexpr + ) ?;
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   998
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
   999
'code\_deps' ( constexpr + ) ?;
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1000
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1001
const : term;
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1002
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1003
constexpr : ( const | 'name.*' | '*' );
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1004
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1005
typeconstructor : nameref;
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1006
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1007
class : nameref;
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1008
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1009
target : 'OCaml' | 'SML' | 'Haskell';
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1010
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1011
'code\_datatype' const +;
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1012
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1013
'code\_const' (const + 'and') \\
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1014
  ( ( '(' target ( syntax ? + 'and' ) ')' ) + );
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1015
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1016
'code\_type' (typeconstructor + 'and') \\
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1017
  ( ( '(' target ( syntax ? + 'and' ) ')' ) + );
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1018
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1019
'code\_class' (class + 'and') \\
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1020
  ( ( '(' target \\
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1021
    ( ( string ('where' \\
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1022
      ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + );
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1023
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1024
'code\_instance' (( typeconstructor '::' class ) + 'and') \\
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1025
  ( ( '(' target ( '-' ? + 'and' ) ')' ) + );
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1026
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1027
'code\_monad' const const target;
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1028
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1029
'code\_reserved' target ( string + );
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1030
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1031
'code\_include' target ( string ( string | '-') );
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1032
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1033
'code\_modulename' target ( ( string string ) + );
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1034
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1035
'code\_exception' ( const + );
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1036
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1037
syntax : string | ( 'infix' | 'infixl' | 'infixr' ) nat string;
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1038
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1039
'print\_codesetup';
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1040
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1041
'code\ func' ( 'del' ) ?;
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1042
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1043
'code\ inline' ( 'del' ) ?;
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1044
\end{rail}
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1045
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1046
\begin{descr}
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1047
24348
c708ea5b109a renamed code_gen to export_code
haftmann
parents: 24248
diff changeset
  1048
\item [$\isarcmd{export_code}$] is the canonical interface for generating and
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1049
  serializing code: for a given list of constants, code is generated for the specified
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1050
  target language(s).  Abstract code is cached incrementally.  If no constant is given,
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1051
  the currently cached code is serialized.  If no serialization instruction
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1052
  is given, only abstract code is cached.
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1053
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1054
  Constants may be specified by giving them literally, referring
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1055
  to all exeuctable contants within a certain theory named ``name''
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1056
  by giving (``name.*''), or referring to \emph{all} executable
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1057
  constants currently available (``*'').
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1058
23807
d36e3ffdb5ce updated
haftmann
parents: 22921
diff changeset
  1059
  By default, for each involved theory one corresponding name space module
24248
d276e4b53d6b dropped code_axioms
haftmann
parents: 23807
diff changeset
  1060
  is generated.  Alternativly, a module name may be specified after the
d276e4b53d6b dropped code_axioms
haftmann
parents: 23807
diff changeset
  1061
  (``module_name'') keyword; then \emph{all} code is placed in this module.
23807
d36e3ffdb5ce updated
haftmann
parents: 22921
diff changeset
  1062
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1063
  For \emph{SML} and \emph{OCaml}, the file specification refers to
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1064
  a single file;  for \emph{Haskell}, it refers to a whole directory,
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1065
  where code is generated in multiple files reflecting the module hierarchy.
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1066
  The file specification ``-'' denotes standard output.  For \emph{SML},
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1067
  omitting the file specification compiles code internally
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1068
  in the context of the current ML session.
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1069
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1070
  Serializers take an optional list of arguments in parentheses. 
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1071
  For \emph{Haskell} a module name prefix may be given using the ``root:''
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1072
  argument;  ``string\_classes'' adds a ``deriving (Read, Show)'' clause
21090
e694285770a2 added option of Haskell serializer
haftmann
parents: 21077
diff changeset
  1073
  to each appropriate datatype declaration.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1074
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1075
\item [$\isarcmd{code_thms}$] prints a list of theorems representing the
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1076
  corresponding program containing all given constants; if no constants are
24248
d276e4b53d6b dropped code_axioms
haftmann
parents: 23807
diff changeset
  1077
  given, the currently cached code theorems are printed.
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1078
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1079
\item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1080
  corresponding program containing all given constants; if no constants are
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1081
  given, the currently cached code theorems are visualized.
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1082
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1083
\item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type.
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1084
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1085
\item [$\isarcmd{code_const}$] associates a list of constants
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1086
  with target-specific serializations; omitting a serialization
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1087
  deletes an existing serialization.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1088
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1089
\item [$\isarcmd{code_type}$] associates a list of type constructors
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1090
  with target-specific serializations; omitting a serialization
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1091
  deletes an existing serialization.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1092
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1093
\item [$\isarcmd{code_class}$] associates a list of classes
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1094
  with target-specific class names; in addition, constants associated
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1095
  with this class may be given target-specific names used for instance
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1096
  declarations; omitting a serialization
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1097
  deletes an existing serialization.  Applies only to \emph{Haskell}.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1098
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1099
\item [$\isarcmd{code_instance}$] declares a list of type constructor / class
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1100
  instance relations as ``already present'' for a given target.
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1101
  Omitting a ``-'' deletes an existing ``already present'' declaration.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1102
  Applies only to \emph{Haskell}.
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1103
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1104
\item [$\isarcmd{code_monad}$] provides an auxiliary mechanism
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1105
  to generate monadic code.
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1106
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1107
\item [$\isarcmd{code_reserved}$] declares a list of names
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1108
  as reserved for a given target, preventing it to be shadowed
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1109
  by any generated code.
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1110
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1111
\item [$\isarcmd{code_include}$] adds arbitrary named content (''include``)
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1112
  to generated code. A as last argument ``-'' will remove an already added ''include``.
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1113
22752
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1114
\item [$\isarcmd{code_modulename}$] declares aliasings from one module name
8b3131eeb509 updated code generator
haftmann
parents: 22291
diff changeset
  1115
  onto another.
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1116
24992
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1117
\item [$\isarcmd{code_exception}$] declares constants which are not required
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1118
  to have a definition by a defining equations; these are mapped on exceptions
d33713284207 code_include replaces code_moduleprolog
haftmann
parents: 24524
diff changeset
  1119
  instead.
21077
d6c141871b29 extended section on code generator
haftmann
parents: 20587
diff changeset
  1120
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1121
\item [$code\ func$] selects (or with option ''del``, deselects) explicitly
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1122
  a defining equation for code generation.  Usually packages introducing
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1123
  defining equations provide a resonable default setup for selection.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1124
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1125
\item [$code\ inline$] declares (or with option ''del``, removes)
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1126
  inlining theorems which are applied as rewrite rules to any defining equation
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1127
  during preprocessing.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1128
22291
bfaba62cc92c adjusted to new code generator Isar commands
haftmann
parents: 21090
diff changeset
  1129
\item [$\isarcmd{print_codesetup}$] gives an overview on selected
22845
5f9138bcb3d7 changed code generator invocation syntax
haftmann
parents: 22752
diff changeset
  1130
  defining equations, code generator datatypes and preprocessor setup.
20587
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1131
f43a46316fa5 added section on code generation 2
haftmann
parents: 19988
diff changeset
  1132
\end{descr}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
  1133
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1134
\section{HOLCF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1135
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1136
\subsection{Mixfix syntax for continuous operations}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1137
14682
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
  1138
\indexisarcmdof{HOLCF}{consts}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1139
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1140
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1141
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1142
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1143
14165
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
  1144
HOLCF provides a separate type for continuous functions $\alpha \to
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1145
\beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1146
syntax normally refers directly to the pure meta-level function type $\alpha
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1147
\To \beta$, with application $f\,x$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1148
14682
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
  1149
The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\ 
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
  1150
\S\ref{sec:consts}) such that declarations involving continuous function types
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
  1151
are treated specifically.  Any given syntax template is transformed
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
  1152
internally, generating translation rules for the abstract and concrete
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
  1153
representation of continuous application.  Note that mixing of HOLCF and Pure
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14619
diff changeset
  1154
application is \emph{not} supported!
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1155
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1156
\subsection{Recursive domains}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1157
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1158
\indexisarcmdof{HOLCF}{domain}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1159
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1160
  \isarcmd{domain} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1161
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1162
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1163
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1164
  'domain' parname? (dmspec + 'and')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1165
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1166
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1167
  dmspec: typespec '=' (cons + '|')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1168
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1169
  cons: name (type *) mixfix?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1170
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1171
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1172
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1173
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
  1174
Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
  1175
\S\ref{sec:hol-datatype}).  Mutual recursion is supported, but no nesting nor
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1176
arbitrary branching.  Domain constructors may be strict (default) or lazy, the
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
  1177
latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
  1178
lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
  1179
domains.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1180
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1181
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1182
\section{ZF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1183
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1184
\subsection{Type checking}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1185
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1186
The ZF logic is essentially untyped, so the concept of ``type checking'' is
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1187
performed as logical reasoning about set-membership statements.  A special
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1188
method assists users in this task; a version of this is already declared as a
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
  1189
``solver'' in the standard Simplifier setup.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1190
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1191
\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1192
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1193
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1194
  \isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1195
  typecheck & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1196
  TC & : & \isaratt \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1197
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1198
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1199
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1200
  'TC' (() | 'add' | 'del')
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1201
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1202
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1203
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1204
\begin{descr}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1205
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1206
\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1207
  the current context.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1208
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1209
  Note that the component built into the Simplifier only knows about those
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1210
  rules being declared globally in the theory!
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1211
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1212
\item [$typecheck$] attempts to solve any pending type-checking problems in
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1213
  subgoals.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1214
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1215
\item [$TC$] adds or deletes type-checking rules from the context.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1216
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1217
\end{descr}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1218
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1219
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1220
\subsection{(Co)Inductive sets and datatypes}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1221
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1222
\subsubsection{Set definitions}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1223
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1224
In ZF everything is a set.  The generic inductive package also provides a
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1225
specific view for ``datatype'' specifications.  Coinductive definitions are
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
  1226
available in both cases, too.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1227
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1228
\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1229
\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1230
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1231
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1232
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1233
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1234
  \isarcmd{codatatype} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1235
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1236
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1237
\railalias{CONDEFS}{con\_defs}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1238
\railterm{CONDEFS}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1239
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1240
\railalias{TYPEINTROS}{type\_intros}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1241
\railterm{TYPEINTROS}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1242
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1243
\railalias{TYPEELIMS}{type\_elims}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1244
\railterm{TYPEELIMS}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1245
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1246
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1247
  ('inductive' | 'coinductive') domains intros hints
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1248
  ;
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1249
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1250
  domains: 'domains' (term + '+') ('<=' | subseteq) term
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1251
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1252
  intros: 'intros' (thmdecl? prop +)
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1253
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1254
  hints: monos? condefs? typeintros? typeelims?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1255
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1256
  monos: ('monos' thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1257
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1258
  condefs: (CONDEFS thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1259
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1260
  typeintros: (TYPEINTROS thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1261
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1262
  typeelims: (TYPEELIMS thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1263
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1264
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1265
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1266
In the following diagram $monos$, $typeintros$, and $typeelims$ are the same
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1267
as above.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1268
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1269
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1270
  ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1271
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1272
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1273
  domain: ('<=' | subseteq) term
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1274
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1275
  dtspec: term '=' (con + '|')
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1276
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1277
  con: name ('(' (term ',' +) ')')?  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1278
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1279
  hints: monos? typeintros? typeelims?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1280
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1281
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1282
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1283
See \cite{isabelle-ZF} for further information on inductive definitions in
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1284
HOL, but note that this covers the old-style theory format.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1285
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1286
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1287
\subsubsection{Primitive recursive functions}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1288
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1289
\indexisarcmdof{ZF}{primrec}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1290
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1291
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1292
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1293
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1294
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1295
  'primrec' (thmdecl? prop +)
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1296
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1297
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1298
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1299
13042
wenzelm
parents: 13041
diff changeset
  1300
\subsubsection{Cases and induction: emulating tactic scripts}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1301
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1302
The following important tactical tools of Isabelle/ZF have been ported to
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1303
Isar.  These should be never used in proper proof texts!
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1304
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1305
\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1306
\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1307
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1308
  case_tac^* & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1309
  induct_tac^* & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1310
  ind_cases^* & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1311
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1312
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1313
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1314
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1315
  (casetac | inducttac) goalspec? name
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1316
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1317
  indcases (prop +)
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1318
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1319
  inductivecases (thmdecl? (prop +) + 'and')
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1320
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1321
\end{rail}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1322
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
  1323
%%% Local Variables:
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1324
%%% mode: latex
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
  1325
%%% TeX-master: "isar-ref"
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
  1326
%%% End: