doc-src/IsarRef/logics.tex
author wenzelm
Mon, 04 Mar 2002 19:07:58 +0100
changeset 13014 3c1c493e6d93
parent 12879 8e1cae1de136
child 13016 c039b8ede204
permissions -rw-r--r--
records from logics-HOL; improved typedef; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     1
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
     2
\chapter{Object-logic specific elements}\label{ch:logics}
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
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    21
implication $\Imp$).  Common object-logics are sufficiently expressive to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    22
\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    23
language.  This is useful in certain situations where a rule needs to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    24
viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    25
\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    26
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    27
From the following language elements, only the $atomize$ method and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    28
$rule_format$ attribute are occasionally required by end-users, the rest is
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    29
for those who need to setup their own object-logic.  In the latter case
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    30
existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    31
realistic examples.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    32
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    33
Generic tools may refer to the information provided by object-logic
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    34
declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    35
Reasoner \S\ref{sec:classical}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    36
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    37
\railalias{ruleformat}{rule\_format}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    38
\railterm{ruleformat}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    39
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    40
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    41
  'judgment' constdecl
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    42
  ;
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    43
  atomize ('(' 'full' ')')?
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    44
  ;
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    45
  ruleformat ('(' 'noasm' ')')?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    46
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    47
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    48
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    49
\begin{descr}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    50
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    51
\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    52
  truth judgment of the current object-logic.  Its type $\sigma$ should
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    53
  specify a coercion of the category of object-level propositions to $prop$ of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    54
  the Pure meta-logic; the mixfix annotation $syn$ would typically just link
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    55
  the object language (internally of syntactic category $logic$) with that of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    56
  $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    57
  theory development.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    58
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    59
\item [$atomize$] (as a method) rewrites any non-atomic premises of a
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    60
  sub-goal, using the meta-level equations declared via $atomize$ (as an
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    61
  attribute) beforehand.  As a result, heavily nested goals become amenable to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    62
  fundamental operations such as resolution (cf.\ the $rule$ method) and
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    63
  proof-by-assumption (cf.\ $assumption$).  Giving the ``$(full)$'' option
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    64
  here means to turn the subgoal into an object-statement (if possible),
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    65
  including the outermost parameters and assumptions as well.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    66
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    67
  A typical collection of $atomize$ rules for a particular object-logic would
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    68
  provide an internalization for each of the connectives of $\Forall$, $\Imp$,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    69
  and $\equiv$.  Meta-level conjunction expressed in the manner of minimal
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    70
  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
    71
  should be covered as well (this is particularly important for locales, see
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    72
  \S\ref{sec:locale}).
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    73
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    74
\item [$rule_format$] rewrites a theorem by the equalities declared as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    75
  $rulify$ rules in the current object-logic.  By default, the result is fully
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    76
  normalized, including assumptions and conclusions at any depth.  The
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    77
  $no_asm$ option restricts the transformation to the conclusion of a rule.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
    78
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    79
  In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    80
  replace (bounded) universal quantification ($\forall$) and implication
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    81
  ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    82
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    83
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    84
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    85
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    86
\section{HOL}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    87
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    88
\subsection{Primitive types}\label{sec:typedef}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    89
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    90
\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    91
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    92
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    93
  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    94
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    95
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    96
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
    97
  'typedecl' typespec infix?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    98
  ;
12879
wenzelm
parents: 12621
diff changeset
    99
  'typedef' parname? typespec infix? '=' term
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   100
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   101
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   102
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   103
\begin{descr}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   104
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   105
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   106
  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   107
  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   108
  actual HOL type constructor.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   109
  
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   110
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   111
  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
   112
  augmented by a Gordon/HOL-style type definition, which establishes a
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   113
  bijection between the representing set $A$ and the new type $t$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   114
  
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   115
  Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   116
  constant) of the same name.  The injection from type to set is called
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   117
  $Rep_t$, its inverse $Abs_t$.  Theorems $Rep_t$, $Rep_inverse$, and
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   118
  $Abs_inverse$ provide the most basic characterization as a corresponding
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   119
  injection/surjection pair (in both directions).  Rules $Rep_t_inject$ and
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   120
  $Abs_t_inject$ provide a slightly more comfortable view on the injectivity
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   121
  part; likewise do $Rep_t_cases$, $Rep_t_induct$, and $Abs_t_cases$,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   122
  $Abs_t_induct$ for surjectivity.  The latter rules are already declare as
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   123
  type or set rules for the generic $cases$ and $induct$ methods.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   124
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   125
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   126
Raw type declarations are rarely useful in practice.  The main application is
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   127
with experimental (or even axiomatic!) theory fragments.  Instead of primitive
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   128
HOL type definitions, user-level theories usually refer to higher-level
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   129
packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   130
$\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   131
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   132
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   133
\subsection{Adhoc tuples}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   134
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   135
\indexisarattof{HOL}{split-format}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   136
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   137
  split_format^* & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   138
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   139
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   140
\railalias{splitformat}{split\_format}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   141
\railterm{splitformat}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   142
\railterm{complete}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   143
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   144
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   145
  splitformat (((name * ) + 'and') | ('(' complete ')'))
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   146
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   147
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   148
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   149
\begin{descr}
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   150
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   151
\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   152
  tuple types into canonical form as specified by the arguments given; $\vec
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   153
  p@i$ refers to occurrences in premise $i$ of the rule.  The
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   154
  $split_format~(complete)$ form causes \emph{all} arguments in function
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   155
  applications to be represented canonically according to their tuple type
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   156
  structure.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   157
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   158
  Note that these operations tend to invent funny names for new local
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   159
  parameters to be introduced.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   160
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   161
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   162
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   163
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   164
\section{Records}\label{sec:hol-record}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   165
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   166
In principle, records merely generalize the concept of tuples where components
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   167
may be addressed by labels instead of just position.  The logical
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   168
infrastructure of records in Isabelle/HOL is slightly more advanced, though,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   169
supporting truly extensible record schemes.  This admits operations that are
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   170
polymorphic with respect to record extension, yielding ``object-oriented''
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   171
effects like (single) inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   172
more details on object-oriented verification and record subtyping in HOL.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   173
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   174
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   175
\subsection{Basic concepts}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   176
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   177
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   178
level of terms and types.  The notation is as follows:
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   179
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   180
\begin{center}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   181
\begin{tabular}{l|l|l}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   182
  & record terms & record types \\ \hline
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   183
  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
   184
  schematic & $\record{x = a\fs y = b\fs \more = m}$ &
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   185
    $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   186
\end{tabular}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   187
\end{center}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   188
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   189
\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   190
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   191
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
   192
$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
   193
assuming that $a \ty A$ and $b \ty B$.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   194
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   195
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
   196
$x$ and $y$ as before, but also possibly further fields as indicated by the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   197
``$\more$'' notation (which is actually part of the syntax).  The improper
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   198
field ``$\more$'' of a record scheme is called the \emph{more part}.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   199
Logically it is just a free variable, which is occasionally referred to as
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   200
\emph{row variable} in the literature.  The more part of a record scheme may
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   201
be instantiated by zero or more further components.  For example, the above
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   202
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
   203
  m'}$, where $m'$ refers to a different more part.  Fixed records are special
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   204
instances of record schemes, where ``$\more$'' is properly terminated by the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   205
$() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   206
abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   207
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   208
\medskip
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   209
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   210
Two key observations make extensible records in a simply typed language like
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   211
HOL feasible:
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   212
\begin{enumerate}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   213
\item the more part is internalized, as a free term or type variable,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   214
\item field names are externalized, they cannot be accessed within the logic
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   215
  as first-class values.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   216
\end{enumerate}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   217
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   218
\medskip
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   219
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   220
In Isabelle/HOL record types have to be defined explicitly, fixing their field
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   221
names and types, and their (optional) parent record (see
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   222
{\S}\ref{sec:hol-record-def}).  Afterwards, records may be formed using above
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   223
syntax, while obeying the canonical order of fields as given by their
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   224
declaration.  The record package provides several standard operations like
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   225
selectors and updates (see {\S}\ref{sec:hol-record-ops}).  The common setup
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   226
for various generic proof tools enable succinct reasoning patterns (see
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   227
{\S}\ref{sec:hol-record-thms}).  See also the Isabelle/HOL tutorial
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   228
\cite{isabelle-hol-book} for further instructions on using records in
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   229
practice.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   230
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   231
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   232
\subsection{Record specifications}\label{sec:hol-record-def}
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   233
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   234
\indexisarcmdof{HOL}{record}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   235
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   236
  \isarcmd{record} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   237
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   238
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   239
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   240
  'record' typespec '=' (type '+')? (constdecl +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   241
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   242
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   243
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   244
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   245
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   246
  defines extensible record type $(\vec\alpha)t$, derived from the optional
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   247
  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   248
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   249
  The type variables of $\tau$ and $\vec\sigma$ need to be covered by the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   250
  (distinct) parameters $\vec\alpha$.  Type constructor $t$ has to be new,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   251
  while $\tau$ needs to specify an instance of an existing record type.  At
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   252
  least one new field $\vec c$ has to be specified.  Basically, field names
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   253
  need to belong to a unique record.  This is not a real restriction in
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   254
  practice, since fields are qualified by the record name internally.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   255
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   256
  The parent record specification $\tau$ is optional; if omitted $t$ becomes a
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   257
  root record.  The hierarchy of all records declared within a theory context
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   258
  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
   259
  each.  There is no way to merge multiple parent records!
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   260
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   261
  For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   262
  fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   263
  $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   264
    \ty \vec\sigma\fs \more \ty \zeta}$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   265
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   266
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   267
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   268
\subsection{Record operations}\label{sec:hol-record-ops}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   269
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   270
Any record definition of the form presented above produces certain standard
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   271
operations.  Selectors and updates are provided for any field, including the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   272
improper one ``$more$''.  There are also cumulative record constructor
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   273
functions.  To simplify the presentation below, we assume for now that
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   274
$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   275
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   276
\medskip \textbf{Selectors} and \textbf{updates} are available for any field
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   277
(including ``$more$''):
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   278
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   279
  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
   280
  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
   281
    \record{\vec c \ty \vec\sigma, \more \ty \zeta}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   282
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   283
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   284
There is special syntax for application of updates: $r \, \record{x \asn a}$
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   285
abbreviates term $x_update \, a \, r$.  Further notation for repeated updates
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   286
is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   287
  \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
   288
Note that because of postfix notation the order of fields shown here is
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   289
reverse than in the actual term.  Since repeated updates are just function
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   290
applications, fields may be freely permuted in $\record{x \asn a\fs y \asn
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   291
  b\fs z \asn c}$, as far as logical equality is concerned.  Thus
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   292
commutativity of updates can be proven within the logic for any two fields,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   293
but not as a general theorem: fields are not first-class values.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   294
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   295
\medskip The \textbf{make} operation provides a cumulative record constructor
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   296
functions:
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   297
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   298
  t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   299
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   300
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   301
\medskip We now reconsider the case of non-root records, which are derived of
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   302
some parent.  In general, the latter may depend on another parent as well,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   303
resulting in a list of \emph{ancestor records}.  Appending the lists of fields
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   304
of all ancestors results in a certain field prefix.  The record package
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   305
automatically takes care of this by lifting operations over this context of
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   306
ancestor fields.  Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   307
b \ty \vec\rho$, the above record operations will get the following types:
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   308
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   309
  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
   310
    \zeta} \To \sigma@i \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   311
  c@i_update & \ty & \sigma@i \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   312
    \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
   313
    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   314
  t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   315
    \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   316
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   317
\noindent
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   318
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   319
\medskip Some further operations address the extension aspect of a derived
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   320
record scheme specifically: $fields$ produces a record fragment consisting of
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   321
exactly the new fields introduced here (the result may serve as a more part
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   322
elsewhere); $extend$ takes a fixed record and adds a given more part;
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   323
$truncate$ restricts a record scheme to a fixed record.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   324
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   325
\begin{matharray}{lll}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   326
  t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   327
  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
   328
    \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
   329
  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
   330
    \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   331
\end{matharray}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   332
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   333
\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   334
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   335
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   336
\subsection{Derived rules and proof tools}\label{sec:hol-record-thms}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   337
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   338
The record package proves several results internally, declaring these facts to
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   339
appropriate proof tools.  This enables users to reason about record structures
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   340
quite comfortably.  Assume that $t$ is a record type as specified above.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   341
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   342
\begin{enumerate}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   343
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   344
\item Standard conversions for selectors or updates applied to record
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   345
  constructor terms are made part of the default Simplifier context; thus
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   346
  proofs by reduction of basic operations merely require the $simp$ method
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   347
  without further arguments.  These rules are available as $t{\dtt}simps$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   348
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   349
\item Selectors applied to updated records are automatically reduced by an
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   350
  internal simplification procedure, which is also part of the default
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   351
  Simplifier context.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   352
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   353
\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
   354
  \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   355
  rules.  These rules are available as $t{\dtt}iffs$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   356
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   357
\item The introduction rule for record equality analogous to $x~r = x~r' \Imp
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   358
  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
   359
  basic rule context as ``$intro?$''.  The rule is called $t{\dtt}equality$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   360
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   361
\item Representations of arbitrary record expressions as canonical constructor
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   362
  terms are provided both in $cases$ and $induct$ format (cf.\ the generic
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   363
  proof methods of the same name, \S\ref{sec:cases-induct}).  Several
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   364
  variations are available, for fixed records, record schemes, more parts etc.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   365
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   366
  The generic proof methods are sufficiently smart to pick the most sensible
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   367
  rule according to the type of the indicated record expression: users just
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   368
  need to apply something like ``$(cases r)$'' to a certain proof problem.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   369
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   370
\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   371
  $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   372
  usually need to be expanded by hand, using the collective fact
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   373
  $t{\dtt}defs$.
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   374
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   375
\end{enumerate}
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   376
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   377
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   378
\subsection{Datatypes}\label{sec:hol-datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   379
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   380
\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   381
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   382
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   383
  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   384
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   385
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   386
\railalias{repdatatype}{rep\_datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   387
\railterm{repdatatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   388
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   389
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   390
  'datatype' (dtspec + 'and')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   391
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   392
  repdatatype (name * ) dtrules
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   393
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   394
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   395
  dtspec: parname? typespec infix? '=' (cons + '|')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   396
  ;
12879
wenzelm
parents: 12621
diff changeset
   397
  cons: name (type * ) mixfix?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   398
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   399
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   400
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   401
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   402
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   403
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   404
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   405
  ones, generating the standard infrastructure of derived concepts (primitive
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   406
  recursion etc.).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   407
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   408
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   409
The induction and exhaustion theorems generated provide case names according
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   410
to the constructors involved, while parameters are named after the types (see
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   411
also \S\ref{sec:cases-induct}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   412
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   413
See \cite{isabelle-HOL} for more details on datatypes, but beware of the
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   414
old-style theory syntax being used there!  Apart from proper proof methods for
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   415
case-analysis and induction, there are also emulations of ML tactics
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   416
\texttt{case_tac} and \texttt{induct_tac} available, see
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   417
\S\ref{sec:induct_tac}; these admit to refer directly to the internal
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   418
structure of subgoals (including internally bound parameters).
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   419
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   420
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   421
\subsection{Recursive functions}\label{sec:recursion}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   422
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   423
\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   424
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   425
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   426
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   427
  \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   428
%FIXME
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   429
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   430
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   431
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   432
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   433
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   434
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   435
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   436
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   437
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   438
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   439
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   440
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   441
\railalias{recdeftc}{recdef\_tc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   442
\railterm{recdeftc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   443
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   444
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   445
  'primrec' parname? (equation + )
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   446
  ;
12879
wenzelm
parents: 12621
diff changeset
   447
  'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   448
  ;
12879
wenzelm
parents: 12621
diff changeset
   449
  recdeftc thmdecl? tc
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   450
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   451
12879
wenzelm
parents: 12621
diff changeset
   452
  equation: thmdecl? prop
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   453
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   454
  hints: '(' 'hints' (recdefmod * ) ')'
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   455
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   456
  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   457
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   458
  tc: nameref ('(' nat ')')?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   459
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   460
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   461
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   462
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   463
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   464
  datatypes, see also \cite{isabelle-HOL} FIXME.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   465
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   466
  functions (using the TFL package), see also \cite{isabelle-HOL} FIXME.  The
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   467
  $(permissive)$ option tells TFL to recover from failed proof attempts,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   468
  returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   469
  $recdef_wf$ hints refer to auxiliary rules to be used in the internal
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   470
  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   471
  \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   472
  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   473
  \S\ref{sec:classical}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   474
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   475
  termination condition number $i$ (default $1$) as generated by a
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   476
  $\isarkeyword{recdef}$ definition of constant $c$.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   477
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   478
  Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   479
  internal proofs without manual intervention.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   480
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   481
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   482
Both kinds of recursive definitions accommodate reasoning by induction (cf.\
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   483
\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   484
the function definition) refers to a specific induction rule, with parameters
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   485
named according to the user-specified equations.  Case names of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   486
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   487
$\isarkeyword{recdef}$ are numbered (starting from $1$).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   488
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   489
The equations provided by these packages may be referred later as theorem list
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   490
$f\mathord.simps$, where $f$ is the (collective) name of the functions
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   491
defined.  Individual equations may be named explicitly as well; note that for
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   492
$\isarkeyword{recdef}$ each specification given by the user may result in
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   493
several theorems.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   494
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   495
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   496
the following attributes.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   497
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   498
\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   499
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   500
  recdef_simp & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   501
  recdef_cong & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   502
  recdef_wf & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   503
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   504
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   505
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   506
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   507
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   508
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   509
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   510
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   511
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   512
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   513
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   514
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   515
  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   516
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   517
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   518
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   519
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   520
\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   521
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   522
\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   523
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   524
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   525
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   526
  mono & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   527
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   528
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   529
\railalias{condefs}{con\_defs}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   530
\railterm{condefs}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   531
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   532
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   533
  ('inductive' | 'coinductive') sets intros monos?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   534
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   535
  'mono' (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   536
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   537
12879
wenzelm
parents: 12621
diff changeset
   538
  sets: (term +)
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   539
  ;
12879
wenzelm
parents: 12621
diff changeset
   540
  intros: 'intros' (thmdecl? prop +)
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   541
  ;
12879
wenzelm
parents: 12621
diff changeset
   542
  monos: 'monos' thmrefs
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   543
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   544
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   545
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   546
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   547
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   548
  (co)inductive sets from the given introduction rules.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   549
\item [$mono$] declares monotonicity rules.  These rule are involved in the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   550
  automated monotonicity proof of $\isarkeyword{inductive}$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   551
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   552
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   553
See \cite{isabelle-HOL} FIXME for further information on inductive definitions
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   554
in HOL.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   555
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   556
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   557
\subsection{Arithmetic proof support}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   558
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   559
\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   560
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   561
  arith & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   562
  arith_split & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   563
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   564
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   565
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   566
  'arith' '!'?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   567
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   568
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   569
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   570
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   571
$real$).  Any current facts are inserted into the goal before running the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   572
procedure.  The ``!''~argument causes the full context of assumptions to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   573
included.  The $arith_split$ attribute declares case split rules to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   574
expanded before the arithmetic procedure is invoked.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   575
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   576
Note that a simpler (but faster) version of arithmetic reasoning is already
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   577
performed by the Simplifier.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   578
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   579
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   580
\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   581
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   582
The following important tactical tools of Isabelle/HOL have been ported to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   583
Isar.  These should be never used in proper proof texts!
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   584
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   585
\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   586
\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   587
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   588
  case_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   589
  induct_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   590
  ind_cases^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   591
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   592
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   593
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   594
\railalias{casetac}{case\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   595
\railterm{casetac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   596
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   597
\railalias{inducttac}{induct\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   598
\railterm{inducttac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   599
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   600
\railalias{indcases}{ind\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   601
\railterm{indcases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   602
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   603
\railalias{inductivecases}{inductive\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   604
\railterm{inductivecases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   605
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   606
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   607
  casetac goalspec? term rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   608
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   609
  inducttac goalspec? (insts * 'and') rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   610
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   611
  indcases (prop +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   612
  ;
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   613
  inductivecases (thmdecl? (prop +) + 'and')
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   614
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   615
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   616
  rule: ('rule' ':' thmref)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   617
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   618
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   619
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   620
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   621
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   622
  only (unless an alternative rule is given explicitly).  Furthermore,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   623
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   624
  variables to be given as instantiation.  These tactic emulations feature
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   625
  both goal addressing and dynamic instantiation.  Note that named rule cases
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   626
  are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   627
  methods (see \S\ref{sec:cases-induct}).
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   628
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   629
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   630
  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   631
  forward manner.
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   632
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   633
  While $ind_cases$ is a proof method to apply the result immediately as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   634
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   635
  theorems at the theory level for later use,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   636
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   637
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   638
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   639
\section{HOLCF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   640
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   641
\subsection{Mixfix syntax for continuous operations}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   642
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   643
\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   644
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   645
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   646
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   647
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   648
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   649
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   650
HOLCF provides a separate type for continuous functions $\alpha \rightarrow
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   651
\beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   652
syntax normally refers directly to the pure meta-level function type $\alpha
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   653
\To \beta$, with application $f\,x$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   654
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   655
The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   656
the pure versions (cf.\ \S\ref{sec:consts}).  Internally, declarations
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   657
involving continuous function types are treated specifically, transforming the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   658
syntax template accordingly and generating syntax translation rules for the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   659
abstract and concrete representation of application.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   660
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   661
The behavior for plain meta-level function types is unchanged.  Mixed
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   662
continuous and meta-level application is \emph{not} supported.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   663
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   664
\subsection{Recursive domains}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   665
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   666
\indexisarcmdof{HOLCF}{domain}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   667
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   668
  \isarcmd{domain} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   669
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   670
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   671
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   672
  'domain' parname? (dmspec + 'and')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   673
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   674
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   675
  dmspec: typespec '=' (cons + '|')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   676
  ;
12879
wenzelm
parents: 12621
diff changeset
   677
  cons: name (type * ) mixfix?
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   678
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   679
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   680
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   681
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   682
Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   683
\S\ref{sec:hol-datatype}).  Mutual recursive is supported, but no nesting nor
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   684
arbitrary branching.  Domain constructors may be strict (default) or lazy, the
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   685
latter admits to introduce infinitary objects in the typical LCF manner (e.g.\
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   686
lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   687
domains.
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   688
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   689
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   690
\section{ZF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   691
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   692
\subsection{Type checking}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   693
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   694
FIXME
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   695
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   696
\subsection{Inductive sets and datatypes}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   697
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   698
FIXME
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   699
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   700
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   701
%%% Local Variables:
12621
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   702
%%% mode: latex
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   703
%%% TeX-master: "isar-ref"
13014
3c1c493e6d93 records from logics-HOL;
wenzelm
parents: 12879
diff changeset
   704
%%% End: