doc-src/IsarRef/logics.tex
author wenzelm
Thu, 03 Jan 2002 17:48:02 +0100
changeset 12621 48cafea0684b
child 12879 8e1cae1de136
permissions -rw-r--r--
next round of updates;
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
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    43
  ruleformat ('(' noasm ')')?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    44
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    45
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    46
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    47
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    48
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    49
\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    50
  truth judgment of the current object-logic.  Its type $\sigma$ should
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    51
  specify a coercion of the category of object-level propositions to $prop$ of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    52
  the Pure meta-logic; the mixfix annotation $syn$ would typically just link
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    53
  the object language (internally of syntactic category $logic$) with that of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    54
  $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    55
  theory development.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    56
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    57
\item [$atomize$] (as a method) rewrites any non-atomic premises of a
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    58
  sub-goal, using the meta-level equations declared via $atomize$ (as an
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    59
  attribute) beforehand.  As a result, heavily nested goals become amenable to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    60
  fundamental operations such as resolution (cf.\ the $rule$ method) and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    61
  proof-by-assumption (cf.\ $assumption$).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    62
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    63
  A typical collection of $atomize$ rules for a particular object-logic would
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    64
  provide an internalization for each of the connectives of $\Forall$, $\Imp$,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    65
  and $\equiv$.  Meta-level conjunction expressed in the manner of minimal
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    66
  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
    67
  should be covered as well (this is particularly important for locales, see
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    68
  \S\ref{sec:locale}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    69
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    70
\item [$rule_format$] rewrites a theorem by the equalities declared as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    71
  $rulify$ rules in the current object-logic.  By default, the result is fully
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    72
  normalized, including assumptions and conclusions at any depth.  The
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    73
  $no_asm$ option restricts the transformation to the conclusion of a rule.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    74
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    75
  In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    76
  replace (bounded) universal quantification ($\forall$) and implication
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    77
  ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    78
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    79
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    80
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    81
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    82
\section{HOL}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    83
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    84
\subsection{Primitive types}\label{sec:typedef}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    85
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    86
\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    87
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    88
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    89
  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    90
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    91
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    92
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    93
  'typedecl' typespec infix? comment?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    94
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    95
  'typedef' parname? typespec infix? \\ '=' term comment?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    96
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    97
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    98
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
    99
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   100
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   101
  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   102
  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   103
  actual HOL type constructor.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   104
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   105
  non-emptiness of the set $A$.  After finishing the proof, the theory will be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   106
  augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   107
  for more information.  Note that user-level theories usually do not directly
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   108
  refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   109
  packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   110
  $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   111
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   112
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   113
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   114
\subsection{Low-level tuples}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   115
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   116
\indexisarattof{HOL}{split-format}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   117
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   118
  split_format^* & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   119
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   120
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   121
\railalias{splitformat}{split\_format}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   122
\railterm{splitformat}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   123
\railterm{complete}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   124
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   125
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   126
  splitformat (((name * ) + 'and') | ('(' complete ')'))
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   127
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   128
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   129
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   130
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   131
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   132
\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   133
  tuple types into canonical form as specified by the arguments given; $\vec
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   134
  p@i$ refers to occurrences in premise $i$ of the rule.  The
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   135
  $split_format~(complete)$ form causes \emph{all} arguments in function
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   136
  applications to be represented canonically according to their tuple type
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   137
  structure.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   138
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   139
  Note that these operations tend to invent funny names for new local
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   140
  parameters to be introduced.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   141
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   142
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   143
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   144
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   145
\subsection{Records}\label{sec:hol-record}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   146
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   147
FIXME proof tools (simp, cases/induct; no split!?);
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   148
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   149
FIXME mixfix syntax;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   150
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   151
\indexisarcmdof{HOL}{record}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   152
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   153
  \isarcmd{record} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   154
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   155
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   156
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   157
  'record' typespec '=' (type '+')? (constdecl +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   158
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   159
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   160
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   161
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   162
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   163
  defines extensible record type $(\vec\alpha)t$, derived from the optional
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   164
  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   165
  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   166
  simply-typed extensible records.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   167
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   168
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   169
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   170
\subsection{Datatypes}\label{sec:hol-datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   171
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   172
\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   173
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   174
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   175
  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   176
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   177
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   178
\railalias{repdatatype}{rep\_datatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   179
\railterm{repdatatype}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   180
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   181
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   182
  'datatype' (dtspec + 'and')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   183
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   184
  repdatatype (name * ) dtrules
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   185
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   186
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   187
  dtspec: parname? typespec infix? '=' (cons + '|')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   188
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   189
  cons: name (type * ) mixfix? comment?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   190
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   191
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   192
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   193
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   194
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   195
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   196
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   197
  ones, generating the standard infrastructure of derived concepts (primitive
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   198
  recursion etc.).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   199
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   200
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   201
The induction and exhaustion theorems generated provide case names according
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   202
to the constructors involved, while parameters are named after the types (see
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   203
also \S\ref{sec:cases-induct}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   204
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   205
See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   206
syntax above has been slightly simplified over the old version, usually
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   207
requiring more quotes and less parentheses.  Apart from proper proof methods
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   208
for case-analysis and induction, there are also emulations of ML tactics
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   209
\texttt{case_tac} and \texttt{induct_tac} available, see
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   210
\S\ref{sec:induct_tac}.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   211
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   212
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   213
\subsection{Recursive functions}\label{sec:recursion}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   214
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   215
\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   216
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   217
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   218
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   219
  \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   220
%FIXME
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   221
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   222
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   223
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   224
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   225
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   226
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   227
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   228
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   229
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   230
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   231
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   232
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   233
\railalias{recdeftc}{recdef\_tc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   234
\railterm{recdeftc}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   235
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   236
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   237
  'primrec' parname? (equation + )
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   238
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   239
  'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   240
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   241
  recdeftc thmdecl? tc comment?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   242
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   243
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   244
  equation: thmdecl? eqn
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   245
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   246
  eqn: prop comment?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   247
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   248
  hints: '(' 'hints' (recdefmod * ) ')'
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   249
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   250
  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   251
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   252
  tc: nameref ('(' nat ')')?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   253
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   254
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   255
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   256
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   257
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   258
  datatypes, see also \cite{isabelle-HOL}.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   259
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   260
  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   261
  $(permissive)$ option tells TFL to recover from failed proof attempts,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   262
  returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   263
  $recdef_wf$ hints refer to auxiliary rules to be used in the internal
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   264
  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   265
  \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   266
  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   267
  \S\ref{sec:classical}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   268
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   269
  termination condition number $i$ (default $1$) as generated by a
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   270
  $\isarkeyword{recdef}$ definition of constant $c$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   271
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   272
  Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   273
  internal proofs without manual intervention.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   274
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   275
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   276
Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   277
\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   278
the function definition) refers to a specific induction rule, with parameters
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   279
named according to the user-specified equations.  Case names of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   280
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   281
$\isarkeyword{recdef}$ are numbered (starting from $1$).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   282
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   283
The equations provided by these packages may be referred later as theorem list
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   284
$f\mathord.simps$, where $f$ is the (collective) name of the functions
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   285
defined.  Individual equations may be named explicitly as well; note that for
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   286
$\isarkeyword{recdef}$ each specification given by the user may result in
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   287
several theorems.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   288
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   289
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   290
the following attributes.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   291
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   292
\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   293
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   294
  recdef_simp & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   295
  recdef_cong & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   296
  recdef_wf & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   297
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   298
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   299
\railalias{recdefsimp}{recdef\_simp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   300
\railterm{recdefsimp}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   301
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   302
\railalias{recdefcong}{recdef\_cong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   303
\railterm{recdefcong}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   304
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   305
\railalias{recdefwf}{recdef\_wf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   306
\railterm{recdefwf}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   307
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   308
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   309
  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   310
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   311
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   312
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   313
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   314
\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   315
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   316
\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   317
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   318
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   319
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   320
  mono & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   321
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   322
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   323
\railalias{condefs}{con\_defs}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   324
\railterm{condefs}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   325
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   326
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   327
  ('inductive' | 'coinductive') sets intros monos?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   328
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   329
  'mono' (() | 'add' | 'del')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   330
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   331
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   332
  sets: (term comment? +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   333
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   334
  intros: 'intros' (thmdecl? prop comment? +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   335
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   336
  monos: 'monos' thmrefs comment?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   337
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   338
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   339
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   340
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   341
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   342
  (co)inductive sets from the given introduction rules.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   343
\item [$mono$] declares monotonicity rules.  These rule are involved in the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   344
  automated monotonicity proof of $\isarkeyword{inductive}$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   345
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   346
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   347
See \cite{isabelle-HOL} for further information on inductive definitions in
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   348
HOL.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   349
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   350
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   351
\subsection{Arithmetic proof support}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   352
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   353
\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   354
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   355
  arith & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   356
  arith_split & : & \isaratt \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   357
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   358
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   359
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   360
  'arith' '!'?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   361
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   362
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   363
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   364
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   365
$real$).  Any current facts are inserted into the goal before running the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   366
procedure.  The ``!''~argument causes the full context of assumptions to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   367
included.  The $arith_split$ attribute declares case split rules to be
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   368
expanded before the arithmetic procedure is invoked.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   369
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   370
Note that a simpler (but faster) version of arithmetic reasoning is already
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   371
performed by the Simplifier.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   372
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   373
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   374
\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   375
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   376
The following important tactical tools of Isabelle/HOL have been ported to
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   377
Isar.  These should be never used in proper proof texts!
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   378
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   379
\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   380
\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   381
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   382
  case_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   383
  induct_tac^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   384
  ind_cases^* & : & \isarmeth \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   385
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   386
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   387
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   388
\railalias{casetac}{case\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   389
\railterm{casetac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   390
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   391
\railalias{inducttac}{induct\_tac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   392
\railterm{inducttac}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   393
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   394
\railalias{indcases}{ind\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   395
\railterm{indcases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   396
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   397
\railalias{inductivecases}{inductive\_cases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   398
\railterm{inductivecases}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   399
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   400
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   401
  casetac goalspec? term rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   402
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   403
  inducttac goalspec? (insts * 'and') rule?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   404
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   405
  indcases (prop +)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   406
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   407
  inductivecases thmdecl? (prop +) comment?
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
  rule: ('rule' ':' thmref)
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   411
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   412
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   413
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   414
\begin{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   415
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   416
  only (unless an alternative rule is given explicitly).  Furthermore,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   417
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   418
  variables to be given as instantiation.  These tactic emulations feature
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   419
  both goal addressing and dynamic instantiation.  Note that named rule cases
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   420
  are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   421
  methods (see \S\ref{sec:cases-induct}).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   422
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   423
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   424
  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   425
  forward manner.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   426
  
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   427
  While $ind_cases$ is a proof method to apply the result immediately as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   428
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   429
  theorems at the theory level for later use,
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   430
\end{descr}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   431
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   432
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   433
\section{HOLCF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   434
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   435
\subsection{Mixfix syntax for continuous operations}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   436
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   437
\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   438
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   439
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   440
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   441
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   442
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   443
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   444
HOLCF provides a separate type for continuous functions $\alpha \rightarrow
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   445
\beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   446
syntax normally refers directly to the pure meta-level function type $\alpha
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   447
\To \beta$, with application $f\,x$.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   448
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   449
The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   450
the pure versions (cf.\ \S\ref{sec:consts}).  Internally, declarations
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   451
involving continuous function types are treated specifically, transforming the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   452
syntax template accordingly and generating syntax translation rules for the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   453
abstract and concrete representation of application.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   454
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   455
The behavior for plain meta-level function types is unchanged.  Mixed
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   456
continuous and meta-level application is \emph{not} supported.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   457
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   458
\subsection{Recursive domains}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   459
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   460
\indexisarcmdof{HOLCF}{domain}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   461
\begin{matharray}{rcl}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   462
  \isarcmd{domain} & : & \isartrans{theory}{theory} \\
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   463
\end{matharray}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   464
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   465
\begin{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   466
  'domain' parname? (dmspec + 'and')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   467
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   468
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   469
  dmspec: typespec '=' (cons + '|')
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   470
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   471
  cons: name (type * ) mixfix? comment?
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   472
  ;
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   473
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   474
\end{rail}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   475
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   476
Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   477
\S\ref{sec:hol-datatype}).  Mutual recursive is supported, but no nesting nor
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   478
arbitrary branching.  Domain constructors may be strict (default) or lazy, the
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   479
latter admits to introduce infinitary objects in the typical LCF manner (lazy
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   480
lists etc.).
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   481
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   482
See also \cite{MuellerNvOS99} for further information HOLCF domains in
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   483
general.
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   484
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   485
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   486
\section{ZF}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   487
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   488
\subsection{Type checking}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   489
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   490
FIXME
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   491
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   492
\subsection{Inductive sets and datatypes}
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   493
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   494
FIXME
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   495
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   496
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   497
%%% Local Variables: 
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   498
%%% mode: latex
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   499
%%% TeX-master: "isar-ref"
48cafea0684b next round of updates;
wenzelm
parents:
diff changeset
   500
%%% End: