doc-src/IsarRef/logics.tex
author nipkow
Wed, 04 Aug 2004 11:25:08 +0200
changeset 15106 e8cef6993701
parent 14682 a5072752114c
child 17659 b1019337c857
permissions -rw-r--r--
aded comment
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
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   438
\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   439
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   440
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   441
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   442
  \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   443
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   444
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   445
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   446
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   447
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   448
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   449
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   450
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   451
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   452
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   453
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   454
\railalias{recdeftc}{recdef\_tc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   455
\railterm{recdeftc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   456
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   457
\begin{rail}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   458
  'primrec' parname? (equation +)
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   459
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   460
  'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   461
  ;
12879
wenzelm
parents: 12621
diff changeset
   462
  recdeftc thmdecl? tc
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   463
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   464
12879
wenzelm
parents: 12621
diff changeset
   465
  equation: thmdecl? prop
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   466
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   467
  hints: '(' 'hints' (recdefmod *) ')'
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   468
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   469
  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   470
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   471
  tc: nameref ('(' nat ')')?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   472
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   473
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   474
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   475
\begin{descr}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   476
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   477
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   478
  datatypes, see also \cite{isabelle-HOL}.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   479
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   480
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   481
  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   482
  ``$(permissive)$'' option tells TFL to recover from failed proof attempts,
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   483
  returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   484
  $recdef_wf$ hints refer to auxiliary rules to be used in the internal
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   485
  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   486
  \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   487
  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   488
  \S\ref{sec:classical}).
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   489
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   490
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   491
  termination condition number $i$ (default $1$) as generated by a
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   492
  $\isarkeyword{recdef}$ definition of constant $c$.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   493
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   494
  Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   495
  internal proofs without manual intervention.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   496
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   497
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   498
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   499
Both kinds of recursive definitions accommodate reasoning by induction (cf.\
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   500
\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   501
the function definition) refers to a specific induction rule, with parameters
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   502
named according to the user-specified equations.  Case names of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   503
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   504
$\isarkeyword{recdef}$ are numbered (starting from $1$).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   505
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   506
The equations provided by these packages may be referred later as theorem list
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   507
$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   508
Individual equations may be named explicitly as well; note that for
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   509
$\isarkeyword{recdef}$ each specification given by the user may result in
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   510
several theorems.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   511
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   512
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   513
the following attributes.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   514
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   515
\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   516
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   517
  recdef_simp & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   518
  recdef_cong & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   519
  recdef_wf & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   520
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   521
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   522
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   523
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   524
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   525
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   526
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   527
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   528
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   529
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   530
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   531
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   532
  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   533
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   534
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   535
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   536
\subsection{Definition by specification}\label{sec:hol-specification}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   537
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   538
\indexisarcmdof{HOL}{specification}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   539
\begin{matharray}{rcl}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   540
  \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
   541
  \isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   542
\end{matharray}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   543
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   544
\begin{rail}
14619
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   545
('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   546
;
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14619
diff changeset
   547
decl: ((name ':')? term '(' 'overloaded' ')'?)
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   548
\end{rail}
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   549
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   550
\begin{descr}
14165
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
   551
\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
   552
  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
   553
  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
   554
  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
   555
  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
   556
\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
   557
  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
   558
  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
   559
  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
   560
  in the first place.
14119
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   561
\item[$decl$] declares a constant to be defined by the specification
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   562
  given.  The definition for the constant $c$ is bound to the name
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   563
  $c$\_def unless a theorem name is given in the declaration.
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   564
  Overloaded constants should be declared as such.
fb9c392644a1 Added the specification command.
skalberg
parents: 13444
diff changeset
   565
\end{descr}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   566
14619
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   567
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
   568
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
   569
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
   570
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
   571
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
   572
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
   573
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
   574
one should use $\isarkeyword{ax_specification}$.
8876ad83b1fb Added documentation for ax_specification, as well as a small comparison of
skalberg
parents: 14165
diff changeset
   575
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   576
\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   577
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   578
\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   579
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   580
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   581
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   582
  mono & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   583
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   584
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   585
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   586
  ('inductive' | 'coinductive') sets intros monos?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   587
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   588
  'mono' (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   589
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   590
12879
wenzelm
parents: 12621
diff changeset
   591
  sets: (term +)
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   592
  ;
12879
wenzelm
parents: 12621
diff changeset
   593
  intros: 'intros' (thmdecl? prop +)
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   594
  ;
12879
wenzelm
parents: 12621
diff changeset
   595
  monos: 'monos' thmrefs
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   596
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   597
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   598
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   599
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   600
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   601
  (co)inductive sets from the given introduction rules.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   602
\item [$mono$] declares monotonicity rules.  These rule are involved in the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   603
  automated monotonicity proof of $\isarkeyword{inductive}$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   604
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   605
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   606
See \cite{isabelle-HOL} for further information on inductive definitions in
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   607
HOL, but note that this covers the old-style theory format.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   608
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   609
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   610
\subsection{Arithmetic proof support}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   611
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   612
\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   613
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   614
  arith & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   615
  arith_split & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   616
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   617
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   618
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   619
  'arith' '!'?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   620
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   621
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   622
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   623
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   624
$real$).  Any current facts are inserted into the goal before running the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   625
procedure.  The ``!''~argument causes the full context of assumptions to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   626
included.  The $arith_split$ attribute declares case split rules to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   627
expanded before the arithmetic procedure is invoked.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   628
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   629
Note that a simpler (but faster) version of arithmetic reasoning is already
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   630
performed by the Simplifier.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   631
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   632
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   633
\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   634
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   635
The following important tactical tools of Isabelle/HOL have been ported to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   636
Isar.  These should be never used in proper proof texts!
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   637
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   638
\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   639
\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   640
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   641
  case_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   642
  induct_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   643
  ind_cases^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   644
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   645
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   646
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   647
\railalias{casetac}{case\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   648
\railterm{casetac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   649
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   650
\railalias{inducttac}{induct\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   651
\railterm{inducttac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   652
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   653
\railalias{indcases}{ind\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   654
\railterm{indcases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   655
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   656
\railalias{inductivecases}{inductive\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   657
\railterm{inductivecases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   658
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   659
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   660
  casetac goalspec? term rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   661
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   662
  inducttac goalspec? (insts * 'and') rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   663
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   664
  indcases (prop +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   665
  ;
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   666
  inductivecases (thmdecl? (prop +) + 'and')
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   667
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   668
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   669
  rule: ('rule' ':' thmref)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   670
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   671
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   672
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   673
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   674
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   675
  only (unless an alternative rule is given explicitly).  Furthermore,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   676
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   677
  variables to be given as instantiation.  These tactic emulations feature
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   678
  both goal addressing and dynamic instantiation.  Note that named rule cases
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   679
  are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   680
  methods (see \S\ref{sec:cases-induct}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   681
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   682
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   683
  to the internal \texttt{mk_cases} operation.  Rules are simplified in an
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   684
  unrestricted forward manner.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   685
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   686
  While $ind_cases$ is a proof method to apply the result immediately as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   687
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   688
  theorems at the theory level for later use,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   689
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   690
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   691
13039
wenzelm
parents: 13027
diff changeset
   692
\subsection{Executable code}
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   693
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   694
Isabelle/Pure provides a generic infrastructure to support code generation
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   695
from executable specifications, both functional and relational programs.
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   696
Isabelle/HOL instantiates these mechanisms in a way that is amenable to
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   697
end-user applications.  See \cite{isabelle-HOL} for further information (this
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   698
actually covers the new-style theory format as well).
13027
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   699
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   700
\indexisarcmd{generate-code}\indexisarcmd{consts-code}\indexisarcmd{types-code}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   701
\indexisaratt{code}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   702
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   703
\begin{matharray}{rcl}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   704
  \isarcmd{generate_code} & : & \isartrans{theory}{theory} \\
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   705
  \isarcmd{consts_code} & : & \isartrans{theory}{theory} \\
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   706
  \isarcmd{types_code} & : & \isartrans{theory}{theory} \\  
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   707
  code & : & \isaratt \\
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   708
\end{matharray}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   709
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   710
\railalias{generatecode}{generate\_code}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   711
\railterm{generatecode}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   712
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   713
\railalias{constscode}{consts\_code}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   714
\railterm{constscode}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   715
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   716
\railalias{typescode}{types\_code}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   717
\railterm{typescode}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   718
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   719
\begin{rail}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   720
  generatecode ( () | '(' name ')') ((name '=' term) +)
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   721
  ;
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   722
  constscode (name ('::' type)? template +)
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   723
  ;
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   724
  typescode (name template +)
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   725
  ;
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   726
  template: '(' string ')'
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   727
  ;
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   728
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   729
  'code' (name)?
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   730
  ;
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   731
\end{rail}
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   732
ddf235f2384a some more stuff;
wenzelm
parents: 13024
diff changeset
   733
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   734
\section{HOLCF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   735
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   736
\subsection{Mixfix syntax for continuous operations}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   737
14682
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
   738
\indexisarcmdof{HOLCF}{consts}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   739
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   740
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   741
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   742
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   743
14165
67b4c4cdb270 New specification syntax added (the specification may be split over
skalberg
parents: 14119
diff changeset
   744
HOLCF provides a separate type for continuous functions $\alpha \to
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   745
\beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   746
syntax normally refers directly to the pure meta-level function type $\alpha
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   747
\To \beta$, with application $f\,x$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   748
14682
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
   749
The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\ 
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
   750
\S\ref{sec:consts}) such that declarations involving continuous function types
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
   751
are treated specifically.  Any given syntax template is transformed
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
   752
internally, generating translation rules for the abstract and concrete
a5072752114c HOLCF: discontinued special version of 'constdefs';
wenzelm
parents: 14642
diff changeset
   753
representation of continuous application.  Note that mixing of HOLCF and Pure
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14619
diff changeset
   754
application is \emph{not} supported!
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   755
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   756
\subsection{Recursive domains}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   757
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   758
\indexisarcmdof{HOLCF}{domain}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   759
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   760
  \isarcmd{domain} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   761
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   762
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   763
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   764
  'domain' parname? (dmspec + 'and')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   765
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   766
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   767
  dmspec: typespec '=' (cons + '|')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   768
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   769
  cons: name (type *) mixfix?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   770
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   771
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   772
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   773
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   774
Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   775
\S\ref{sec:hol-datatype}).  Mutual recursion is supported, but no nesting nor
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   776
arbitrary branching.  Domain constructors may be strict (default) or lazy, the
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   777
latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   778
lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   779
domains.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   780
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   781
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   782
\section{ZF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   783
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   784
\subsection{Type checking}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   785
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   786
The ZF logic is essentially untyped, so the concept of ``type checking'' is
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   787
performed as logical reasoning about set-membership statements.  A special
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   788
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
   789
``solver'' in the standard Simplifier setup.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   790
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   791
\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   792
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   793
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   794
  \isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   795
  typecheck & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   796
  TC & : & \isaratt \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   797
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   798
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   799
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   800
  'TC' (() | 'add' | 'del')
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   801
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   802
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   803
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   804
\begin{descr}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   805
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   806
\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   807
  the current context.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   808
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   809
  Note that the component built into the Simplifier only knows about those
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   810
  rules being declared globally in the theory!
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   811
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   812
\item [$typecheck$] attempts to solve any pending type-checking problems in
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   813
  subgoals.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   814
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   815
\item [$TC$] adds or deletes type-checking rules from the context.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   816
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   817
\end{descr}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   818
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   819
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   820
\subsection{(Co)Inductive sets and datatypes}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   821
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   822
\subsubsection{Set definitions}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   823
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   824
In ZF everything is a set.  The generic inductive package also provides a
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   825
specific view for ``datatype'' specifications.  Coinductive definitions are
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13039
diff changeset
   826
available in both cases, too.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   827
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   828
\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   829
\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   830
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   831
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   832
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   833
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   834
  \isarcmd{codatatype} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   835
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   836
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   837
\railalias{CONDEFS}{con\_defs}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   838
\railterm{CONDEFS}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   839
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   840
\railalias{TYPEINTROS}{type\_intros}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   841
\railterm{TYPEINTROS}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   842
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   843
\railalias{TYPEELIMS}{type\_elims}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   844
\railterm{TYPEELIMS}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   845
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   846
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   847
  ('inductive' | 'coinductive') domains intros hints
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   848
  ;
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   849
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   850
  domains: 'domains' (term + '+') ('<=' | subseteq) term
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   851
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   852
  intros: 'intros' (thmdecl? prop +)
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   853
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   854
  hints: monos? condefs? typeintros? typeelims?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   855
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   856
  monos: ('monos' thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   857
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   858
  condefs: (CONDEFS thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   859
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   860
  typeintros: (TYPEINTROS thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   861
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   862
  typeelims: (TYPEELIMS thmrefs)?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   863
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   864
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   865
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   866
In the following diagram $monos$, $typeintros$, and $typeelims$ are the same
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   867
as above.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   868
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   869
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   870
  ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   871
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   872
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   873
  domain: ('<=' | subseteq) term
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   874
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   875
  dtspec: term '=' (con + '|')
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   876
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   877
  con: name ('(' (term ',' +) ')')?  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   878
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   879
  hints: monos? typeintros? typeelims?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   880
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   881
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   882
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   883
See \cite{isabelle-ZF} for further information on inductive definitions in
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   884
HOL, but note that this covers the old-style theory format.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   885
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   886
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   887
\subsubsection{Primitive recursive functions}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   888
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   889
\indexisarcmdof{ZF}{primrec}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   890
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   891
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   892
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   893
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   894
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   895
  'primrec' (thmdecl? prop +)
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   896
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   897
\end{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   898
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   899
13042
wenzelm
parents: 13041
diff changeset
   900
\subsubsection{Cases and induction: emulating tactic scripts}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   901
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   902
The following important tactical tools of Isabelle/ZF have been ported to
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   903
Isar.  These should be never used in proper proof texts!
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   904
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   905
\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   906
\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   907
\begin{matharray}{rcl}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   908
  case_tac^* & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   909
  induct_tac^* & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   910
  ind_cases^* & : & \isarmeth \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   911
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   912
\end{matharray}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   913
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   914
\begin{rail}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   915
  (casetac | inducttac) goalspec? name
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   916
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   917
  indcases (prop +)
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   918
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   919
  inductivecases (thmdecl? (prop +) + 'and')
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   920
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   921
\end{rail}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   922
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   923
%%% Local Variables:
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   924
%%% mode: latex
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   925
%%% TeX-master: "isar-ref"
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   926
%%% End: