doc-src/IsarRef/logics.tex
 author wenzelm Mon Mar 04 22:31:21 2002 +0100 (2002-03-04) changeset 13016 c039b8ede204 parent 13014 3c1c493e6d93 child 13024 0461b281c2b5 permissions -rw-r--r--
tuned;
     1

     2 \chapter{Object-logic specific elements}\label{ch:logics}

     3

     4 \section{General logic setup}\label{sec:object-logic}

     5

     6 \indexisarcmd{judgment}

     7 \indexisarmeth{atomize}\indexisaratt{atomize}

     8 \indexisaratt{rule-format}\indexisaratt{rulify}

     9

    10 \begin{matharray}{rcl}

    11   \isarcmd{judgment} & : & \isartrans{theory}{theory} \\

    12   atomize & : & \isarmeth \\

    13   atomize & : & \isaratt \\

    14   rule_format & : & \isaratt \\

    15   rulify & : & \isaratt \\

    16 \end{matharray}

    17

    18 The very starting point for any Isabelle object-logic is a truth judgment''

    19 that links object-level statements to the meta-logic (with its minimal

    20 language of $prop$ that covers universal quantification $\Forall$ and

    21 implication $\Imp$).  Common object-logics are sufficiently expressive to

    22 \emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own

    23 language.  This is useful in certain situations where a rule needs to be

    24 viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x   25 \in A \Imp P(x)$ versus $\forall x \in A. P(x)$).

    26

    27 From the following language elements, only the $atomize$ method and

    28 $rule_format$ attribute are occasionally required by end-users, the rest is

    29 for those who need to setup their own object-logic.  In the latter case

    30 existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as

    31 realistic examples.

    32

    33 Generic tools may refer to the information provided by object-logic

    34 declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical

    35 Reasoner \S\ref{sec:classical}).

    36

    37 \begin{rail}

    38   'judgment' constdecl

    39   ;

    40   atomize ('(' 'full' ')')?

    41   ;

    42   ruleformat ('(' 'noasm' ')')?

    43   ;

    44 \end{rail}

    45

    46 \begin{descr}

    47

    48 \item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the

    49   truth judgment of the current object-logic.  Its type $\sigma$ should

    50   specify a coercion of the category of object-level propositions to $prop$ of

    51   the Pure meta-logic; the mixfix annotation $syn$ would typically just link

    52   the object language (internally of syntactic category $logic$) with that of

    53   $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any

    54   theory development.

    55

    56 \item [$atomize$] (as a method) rewrites any non-atomic premises of a

    57   sub-goal, using the meta-level equations declared via $atomize$ (as an

    58   attribute) beforehand.  As a result, heavily nested goals become amenable to

    59   fundamental operations such as resolution (cf.\ the $rule$ method) and

    60   proof-by-assumption (cf.\ $assumption$).  Giving the $(full)$'' option

    61   here means to turn the subgoal into an object-statement (if possible),

    62   including the outermost parameters and assumptions as well.

    63

    64   A typical collection of $atomize$ rules for a particular object-logic would

    65   provide an internalization for each of the connectives of $\Forall$, $\Imp$,

    66   and $\equiv$.  Meta-level conjunction expressed in the manner of minimal

    67   higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$

    68   should be covered as well (this is particularly important for locales, see

    69   \S\ref{sec:locale}).

    70

    71 \item [$rule_format$] rewrites a theorem by the equalities declared as

    72   $rulify$ rules in the current object-logic.  By default, the result is fully

    73   normalized, including assumptions and conclusions at any depth.  The

    74   $no_asm$ option restricts the transformation to the conclusion of a rule.

    75

    76   In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to

    77   replace (bounded) universal quantification ($\forall$) and implication

    78   ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.

    79

    80 \end{descr}

    81

    82

    83 \section{HOL}

    84

    85 \subsection{Primitive types}\label{sec:typedef}

    86

    87 \indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}

    88 \begin{matharray}{rcl}

    89   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\

    90   \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\

    91 \end{matharray}

    92

    93 \begin{rail}

    94   'typedecl' typespec infix?

    95   ;

    96   'typedef' parname? abstype '=' repset

    97   ;

    98

    99   abstype: typespec infix?

   100   ;

   101   repset: term ('morphisms' name name)?

   102   ;

   103 \end{rail}

   104

   105 \begin{descr}

   106

   107 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original

   108   $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but

   109   also declares type arity $t :: (term, \dots, term) term$, making $t$ an

   110   actual HOL type constructor.

   111

   112 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating

   113   non-emptiness of the set $A$.  After finishing the proof, the theory will be

   114   augmented by a Gordon/HOL-style type definition, which establishes a

   115   bijection between the representing set $A$ and the new type $t$.

   116

   117   Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term

   118   constant) of the same name (an alternative base name may be given in

   119   parentheses).  The injection from type to set is called $Rep_t$, its inverse

   120   $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$

   121   declaration).

   122

   123   Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic

   124   characterization as a corresponding injection/surjection pair (in both

   125   directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly

   126   more comfortable view on the injectivity part, suitable for automated proof

   127   tools (e.g.\ in $simp$ or $iff$ declarations).  Rules $Rep_t_cases$,

   128   $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views

   129   on surjectivity; these are already declared as type or set rules for the

   130   generic $cases$ and $induct$ methods.

   131 \end{descr}

   132

   133 Raw type declarations are rarely used in practice; the main application is

   134 with experimental (or even axiomatic!) theory fragments.  Instead of primitive

   135 HOL type definitions, user-level theories usually refer to higher-level

   136 packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or

   137 $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).

   138

   139

   140 \subsection{Adhoc tuples}

   141

   142 \indexisarattof{HOL}{split-format}

   143 \begin{matharray}{rcl}

   144   split_format^* & : & \isaratt \\

   145 \end{matharray}

   146

   147 \railalias{splitformat}{split\_format}

   148 \railterm{splitformat}

   149 \railterm{complete}

   150

   151 \begin{rail}

   152   splitformat (((name * ) + 'and') | ('(' complete ')'))

   153   ;

   154 \end{rail}

   155

   156 \begin{descr}

   157

   158 \item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level

   159   tuple types into canonical form as specified by the arguments given; $\vec   160 p@i$ refers to occurrences in premise $i$ of the rule.  The

   161   $split_format~(complete)$ form causes \emph{all} arguments in function

   162   applications to be represented canonically according to their tuple type

   163   structure.

   164

   165   Note that these operations tend to invent funny names for new local

   166   parameters to be introduced.

   167

   168 \end{descr}

   169

   170

   171 \section{Records}\label{sec:hol-record}

   172

   173 In principle, records merely generalize the concept of tuples where components

   174 may be addressed by labels instead of just position.  The logical

   175 infrastructure of records in Isabelle/HOL is slightly more advanced, though,

   176 supporting truly extensible record schemes.  This admits operations that are

   177 polymorphic with respect to record extension, yielding object-oriented''

   178 effects like (single) inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for

   179 more details on object-oriented verification and record subtyping in HOL.

   180

   181

   182 \subsection{Basic concepts}

   183

   184 Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the

   185 level of terms and types.  The notation is as follows:

   186

   187 \begin{center}

   188 \begin{tabular}{l|l|l}

   189   & record terms & record types \\ \hline

   190   fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\

   191   schematic & $\record{x = a\fs y = b\fs \more = m}$ &

   192     $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\

   193 \end{tabular}

   194 \end{center}

   195

   196 \noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}.

   197

   198 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field

   199 $y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,

   200 assuming that $a \ty A$ and $b \ty B$.

   201

   202 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields

   203 $x$ and $y$ as before, but also possibly further fields as indicated by the

   204 $\more$'' notation (which is actually part of the syntax).  The improper

   205 field $\more$'' of a record scheme is called the \emph{more part}.

   206 Logically it is just a free variable, which is occasionally referred to as

   207 \emph{row variable} in the literature.  The more part of a record scheme may

   208 be instantiated by zero or more further components.  For example, the above

   209 scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more =   210 m'}$, where $m'$ refers to a different more part.  Fixed records are special

   211 instances of record schemes, where $\more$'' is properly terminated by the

   212 $() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an

   213 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.

   214

   215 \medskip

   216

   217 Two key observations make extensible records in a simply typed language like

   218 HOL feasible:

   219 \begin{enumerate}

   220 \item the more part is internalized, as a free term or type variable,

   221 \item field names are externalized, they cannot be accessed within the logic

   222   as first-class values.

   223 \end{enumerate}

   224

   225 \medskip

   226

   227 In Isabelle/HOL record types have to be defined explicitly, fixing their field

   228 names and types, and their (optional) parent record (see

   229 {\S}\ref{sec:hol-record-def}).  Afterwards, records may be formed using above

   230 syntax, while obeying the canonical order of fields as given by their

   231 declaration.  The record package provides several standard operations like

   232 selectors and updates (see {\S}\ref{sec:hol-record-ops}).  The common setup

   233 for various generic proof tools enable succinct reasoning patterns (see

   234 {\S}\ref{sec:hol-record-thms}).  See also the Isabelle/HOL tutorial

   235 \cite{isabelle-hol-book} for further instructions on using records in

   236 practice.

   237

   238

   239 \subsection{Record specifications}\label{sec:hol-record-def}

   240

   241 \indexisarcmdof{HOL}{record}

   242 \begin{matharray}{rcl}

   243   \isarcmd{record} & : & \isartrans{theory}{theory} \\

   244 \end{matharray}

   245

   246 \begin{rail}

   247   'record' typespec '=' (type '+')? (constdecl +)

   248   ;

   249 \end{rail}

   250

   251 \begin{descr}

   252 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]

   253   defines extensible record type $(\vec\alpha)t$, derived from the optional

   254   parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.

   255

   256   The type variables of $\tau$ and $\vec\sigma$ need to be covered by the

   257   (distinct) parameters $\vec\alpha$.  Type constructor $t$ has to be new,

   258   while $\tau$ needs to specify an instance of an existing record type.  At

   259   least one new field $\vec c$ has to be specified.  Basically, field names

   260   need to belong to a unique record.  This is not a real restriction in

   261   practice, since fields are qualified by the record name internally.

   262

   263   The parent record specification $\tau$ is optional; if omitted $t$ becomes a

   264   root record.  The hierarchy of all records declared within a theory context

   265   forms a forest structure, i.e.\ a set of trees starting with a root record

   266   each.  There is no way to merge multiple parent records!

   267

   268   For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the

   269   fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is

   270   $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c   271 \ty \vec\sigma\fs \more \ty \zeta}$.

   272

   273 \end{descr}

   274

   275 \subsection{Record operations}\label{sec:hol-record-ops}

   276

   277 Any record definition of the form presented above produces certain standard

   278 operations.  Selectors and updates are provided for any field, including the

   279 improper one $more$''.  There are also cumulative record constructor

   280 functions.  To simplify the presentation below, we assume for now that

   281 $(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$.

   282

   283 \medskip \textbf{Selectors} and \textbf{updates} are available for any field

   284 (including $more$''):

   285 \begin{matharray}{lll}

   286   c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\

   287   c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To

   288     \record{\vec c \ty \vec\sigma, \more \ty \zeta}

   289 \end{matharray}

   290

   291 There is special syntax for application of updates: $r \, \record{x \asn a}$

   292 abbreviates term $x_update \, a \, r$.  Further notation for repeated updates

   293 is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z   294 \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.

   295 Note that because of postfix notation the order of fields shown here is

   296 reverse than in the actual term.  Since repeated updates are just function

   297 applications, fields may be freely permuted in $\record{x \asn a\fs y \asn   298 b\fs z \asn c}$, as far as logical equality is concerned.  Thus

   299 commutativity of updates can be proven within the logic for any two fields,

   300 but not as a general theorem: fields are not first-class values.

   301

   302 \medskip The \textbf{make} operation provides a cumulative record constructor

   303 functions:

   304 \begin{matharray}{lll}

   305   t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\

   306 \end{matharray}

   307

   308 \medskip We now reconsider the case of non-root records, which are derived of

   309 some parent.  In general, the latter may depend on another parent as well,

   310 resulting in a list of \emph{ancestor records}.  Appending the lists of fields

   311 of all ancestors results in a certain field prefix.  The record package

   312 automatically takes care of this by lifting operations over this context of

   313 ancestor fields.  Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec   314 b \ty \vec\rho$, the above record operations will get the following types:

   315 \begin{matharray}{lll}

   316   c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty

   317     \zeta} \To \sigma@i \\

   318   c@i_update & \ty & \sigma@i \To

   319     \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To

   320     \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\

   321   t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To

   322     \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\

   323 \end{matharray}

   324 \noindent

   325

   326 \medskip Some further operations address the extension aspect of a derived

   327 record scheme specifically: $fields$ produces a record fragment consisting of

   328 exactly the new fields introduced here (the result may serve as a more part

   329 elsewhere); $extend$ takes a fixed record and adds a given more part;

   330 $truncate$ restricts a record scheme to a fixed record.

   331

   332 \begin{matharray}{lll}

   333   t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\

   334   t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To

   335     \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\

   336   t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To

   337     \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\

   338 \end{matharray}

   339

   340 \noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.

   341

   342

   343 \subsection{Derived rules and proof tools}\label{sec:hol-record-thms}

   344

   345 The record package proves several results internally, declaring these facts to

   346 appropriate proof tools.  This enables users to reason about record structures

   347 quite comfortably.  Assume that $t$ is a record type as specified above.

   348

   349 \begin{enumerate}

   350

   351 \item Standard conversions for selectors or updates applied to record

   352   constructor terms are made part of the default Simplifier context; thus

   353   proofs by reduction of basic operations merely require the $simp$ method

   354   without further arguments.  These rules are available as $t{\dtt}simps$.

   355

   356 \item Selectors applied to updated records are automatically reduced by an

   357   internal simplification procedure, which is also part of the default

   358   Simplifier context.

   359

   360 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'   361 \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$

   362   rules.  These rules are available as $t{\dtt}iffs$.

   363

   364 \item The introduction rule for record equality analogous to $x~r = x~r' \Imp   365 y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the

   366   basic rule context as $intro?$''.  The rule is called $t{\dtt}equality$.

   367

   368 \item Representations of arbitrary record expressions as canonical constructor

   369   terms are provided both in $cases$ and $induct$ format (cf.\ the generic

   370   proof methods of the same name, \S\ref{sec:cases-induct}).  Several

   371   variations are available, for fixed records, record schemes, more parts etc.

   372

   373   The generic proof methods are sufficiently smart to pick the most sensible

   374   rule according to the type of the indicated record expression: users just

   375   need to apply something like $(cases r)$'' to a certain proof problem.

   376

   377 \item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,

   378   $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but

   379   usually need to be expanded by hand, using the collective fact

   380   $t{\dtt}defs$.

   381

   382 \end{enumerate}

   383

   384

   385 \subsection{Datatypes}\label{sec:hol-datatype}

   386

   387 \indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}

   388 \begin{matharray}{rcl}

   389   \isarcmd{datatype} & : & \isartrans{theory}{theory} \\

   390   \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\

   391 \end{matharray}

   392

   393 \railalias{repdatatype}{rep\_datatype}

   394 \railterm{repdatatype}

   395

   396 \begin{rail}

   397   'datatype' (dtspec + 'and')

   398   ;

   399   repdatatype (name * ) dtrules

   400   ;

   401

   402   dtspec: parname? typespec infix? '=' (cons + '|')

   403   ;

   404   cons: name (type * ) mixfix?

   405   ;

   406   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs

   407 \end{rail}

   408

   409 \begin{descr}

   410 \item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.

   411 \item [$\isarkeyword{rep_datatype}$] represents existing types as inductive

   412   ones, generating the standard infrastructure of derived concepts (primitive

   413   recursion etc.).

   414 \end{descr}

   415

   416 The induction and exhaustion theorems generated provide case names according

   417 to the constructors involved, while parameters are named after the types (see

   418 also \S\ref{sec:cases-induct}).

   419

   420 See \cite{isabelle-HOL} for more details on datatypes, but beware of the

   421 old-style theory syntax being used there!  Apart from proper proof methods for

   422 case-analysis and induction, there are also emulations of ML tactics

   423 \texttt{case_tac} and \texttt{induct_tac} available, see

   424 \S\ref{sec:induct_tac}; these admit to refer directly to the internal

   425 structure of subgoals (including internally bound parameters).

   426

   427

   428 \subsection{Recursive functions}\label{sec:recursion}

   429

   430 \indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}

   431 \begin{matharray}{rcl}

   432   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\

   433   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\

   434   \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\

   435 %FIXME

   436 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\

   437 \end{matharray}

   438

   439 \railalias{recdefsimp}{recdef\_simp}

   440 \railterm{recdefsimp}

   441

   442 \railalias{recdefcong}{recdef\_cong}

   443 \railterm{recdefcong}

   444

   445 \railalias{recdefwf}{recdef\_wf}

   446 \railterm{recdefwf}

   447

   448 \railalias{recdeftc}{recdef\_tc}

   449 \railterm{recdeftc}

   450

   451 \begin{rail}

   452   'primrec' parname? (equation + )

   453   ;

   454   'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?

   455   ;

   456   recdeftc thmdecl? tc

   457   ;

   458

   459   equation: thmdecl? prop

   460   ;

   461   hints: '(' 'hints' (recdefmod * ) ')'

   462   ;

   463   recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod

   464   ;

   465   tc: nameref ('(' nat ')')?

   466   ;

   467 \end{rail}

   468

   469 \begin{descr}

   470 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over

   471   datatypes, see also \cite{isabelle-HOL} FIXME.

   472 \item [$\isarkeyword{recdef}$] defines general well-founded recursive

   473   functions (using the TFL package), see also \cite{isabelle-HOL} FIXME.  The

   474   $(permissive)$ option tells TFL to recover from failed proof attempts,

   475   returning unfinished results.  The $recdef_simp$, $recdef_cong$, and

   476   $recdef_wf$ hints refer to auxiliary rules to be used in the internal

   477   automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\

   478   \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier

   479   (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\

   480   \S\ref{sec:classical}).

   481 \item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover

   482   termination condition number $i$ (default $1$) as generated by a

   483   $\isarkeyword{recdef}$ definition of constant $c$.

   484

   485   Note that in most cases, $\isarkeyword{recdef}$ is able to finish its

   486   internal proofs without manual intervention.

   487 \end{descr}

   488

   489 Both kinds of recursive definitions accommodate reasoning by induction (cf.\

   490 \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of

   491 the function definition) refers to a specific induction rule, with parameters

   492 named according to the user-specified equations.  Case names of

   493 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of

   494 $\isarkeyword{recdef}$ are numbered (starting from $1$).

   495

   496 The equations provided by these packages may be referred later as theorem list

   497 $f\mathord.simps$, where $f$ is the (collective) name of the functions

   498 defined.  Individual equations may be named explicitly as well; note that for

   499 $\isarkeyword{recdef}$ each specification given by the user may result in

   500 several theorems.

   501

   502 \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using

   503 the following attributes.

   504

   505 \indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}

   506 \begin{matharray}{rcl}

   507   recdef_simp & : & \isaratt \\

   508   recdef_cong & : & \isaratt \\

   509   recdef_wf & : & \isaratt \\

   510 \end{matharray}

   511

   512 \railalias{recdefsimp}{recdef\_simp}

   513 \railterm{recdefsimp}

   514

   515 \railalias{recdefcong}{recdef\_cong}

   516 \railterm{recdefcong}

   517

   518 \railalias{recdefwf}{recdef\_wf}

   519 \railterm{recdefwf}

   520

   521 \begin{rail}

   522   (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')

   523   ;

   524 \end{rail}

   525

   526

   527 \subsection{(Co)Inductive sets}\label{sec:hol-inductive}

   528

   529 \indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}

   530 \begin{matharray}{rcl}

   531   \isarcmd{inductive} & : & \isartrans{theory}{theory} \\

   532   \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\

   533   mono & : & \isaratt \\

   534 \end{matharray}

   535

   536 \railalias{condefs}{con\_defs}

   537 \railterm{condefs}

   538

   539 \begin{rail}

   540   ('inductive' | 'coinductive') sets intros monos?

   541   ;

   542   'mono' (() | 'add' | 'del')

   543   ;

   544

   545   sets: (term +)

   546   ;

   547   intros: 'intros' (thmdecl? prop +)

   548   ;

   549   monos: 'monos' thmrefs

   550   ;

   551 \end{rail}

   552

   553 \begin{descr}

   554 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define

   555   (co)inductive sets from the given introduction rules.

   556 \item [$mono$] declares monotonicity rules.  These rule are involved in the

   557   automated monotonicity proof of $\isarkeyword{inductive}$.

   558 \end{descr}

   559

   560 See \cite{isabelle-HOL} FIXME for further information on inductive definitions

   561 in HOL.

   562

   563

   564 \subsection{Arithmetic proof support}

   565

   566 \indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}

   567 \begin{matharray}{rcl}

   568   arith & : & \isarmeth \\

   569   arith_split & : & \isaratt \\

   570 \end{matharray}

   571

   572 \begin{rail}

   573   'arith' '!'?

   574   ;

   575 \end{rail}

   576

   577 The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,

   578 $real$).  Any current facts are inserted into the goal before running the

   579 procedure.  The !''~argument causes the full context of assumptions to be

   580 included.  The $arith_split$ attribute declares case split rules to be

   581 expanded before the arithmetic procedure is invoked.

   582

   583 Note that a simpler (but faster) version of arithmetic reasoning is already

   584 performed by the Simplifier.

   585

   586

   587 \subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}

   588

   589 The following important tactical tools of Isabelle/HOL have been ported to

   590 Isar.  These should be never used in proper proof texts!

   591

   592 \indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}

   593 \indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}

   594 \begin{matharray}{rcl}

   595   case_tac^* & : & \isarmeth \\

   596   induct_tac^* & : & \isarmeth \\

   597   ind_cases^* & : & \isarmeth \\

   598   \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\

   599 \end{matharray}

   600

   601 \railalias{casetac}{case\_tac}

   602 \railterm{casetac}

   603

   604 \railalias{inducttac}{induct\_tac}

   605 \railterm{inducttac}

   606

   607 \railalias{indcases}{ind\_cases}

   608 \railterm{indcases}

   609

   610 \railalias{inductivecases}{inductive\_cases}

   611 \railterm{inductivecases}

   612

   613 \begin{rail}

   614   casetac goalspec? term rule?

   615   ;

   616   inducttac goalspec? (insts * 'and') rule?

   617   ;

   618   indcases (prop +)

   619   ;

   620   inductivecases (thmdecl? (prop +) + 'and')

   621   ;

   622

   623   rule: ('rule' ':' thmref)

   624   ;

   625 \end{rail}

   626

   627 \begin{descr}

   628 \item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes

   629   only (unless an alternative rule is given explicitly).  Furthermore,

   630   $case_tac$ does a classical case split on booleans; $induct_tac$ allows only

   631   variables to be given as instantiation.  These tactic emulations feature

   632   both goal addressing and dynamic instantiation.  Note that named rule cases

   633   are \emph{not} provided as would be by the proper $induct$ and $cases$ proof

   634   methods (see \S\ref{sec:cases-induct}).

   635

   636 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface

   637   to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted

   638   forward manner.

   639

   640   While $ind_cases$ is a proof method to apply the result immediately as

   641   elimination rules, $\isarkeyword{inductive_cases}$ provides case split

   642   theorems at the theory level for later use,

   643 \end{descr}

   644

   645

   646 \section{HOLCF}

   647

   648 \subsection{Mixfix syntax for continuous operations}

   649

   650 \indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}

   651

   652 \begin{matharray}{rcl}

   653   \isarcmd{consts} & : & \isartrans{theory}{theory} \\

   654   \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\

   655 \end{matharray}

   656

   657 HOLCF provides a separate type for continuous functions $\alpha \rightarrow   658 \beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix

   659 syntax normally refers directly to the pure meta-level function type $\alpha   660 \To \beta$, with application $f\,x$.

   661

   662 The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as

   663 the pure versions (cf.\ \S\ref{sec:consts}).  Internally, declarations

   664 involving continuous function types are treated specifically, transforming the

   665 syntax template accordingly and generating syntax translation rules for the

   666 abstract and concrete representation of application.

   667

   668 The behavior for plain meta-level function types is unchanged.  Mixed

   669 continuous and meta-level application is \emph{not} supported.

   670

   671 \subsection{Recursive domains}

   672

   673 \indexisarcmdof{HOLCF}{domain}

   674 \begin{matharray}{rcl}

   675   \isarcmd{domain} & : & \isartrans{theory}{theory} \\

   676 \end{matharray}

   677

   678 \begin{rail}

   679   'domain' parname? (dmspec + 'and')

   680   ;

   681

   682   dmspec: typespec '=' (cons + '|')

   683   ;

   684   cons: name (type * ) mixfix?

   685   ;

   686   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs

   687 \end{rail}

   688

   689 Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\

   690 \S\ref{sec:hol-datatype}).  Mutual recursive is supported, but no nesting nor

   691 arbitrary branching.  Domain constructors may be strict (default) or lazy, the

   692 latter admits to introduce infinitary objects in the typical LCF manner (e.g.\

   693 lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF

   694 domains.

   695

   696

   697 \section{ZF}

   698

   699 \subsection{Type checking}

   700

   701 FIXME

   702

   703 \subsection{Inductive sets and datatypes}

   704

   705 FIXME

   706

   707

   708 %%% Local Variables:

   709 %%% mode: latex

   710 %%% TeX-master: "isar-ref"

   711 %%% End: