doc-src/IsarRef/Thy/document/ZF_Specific.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 30172 afdf7808cfd0
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
wenzelm@26840
     1
%
wenzelm@26840
     2
\begin{isabellebody}%
wenzelm@26840
     3
\def\isabellecontext{ZF{\isacharunderscore}Specific}%
wenzelm@26840
     4
%
wenzelm@26840
     5
\isadelimtheory
wenzelm@26840
     6
%
wenzelm@26840
     7
\endisadelimtheory
wenzelm@26840
     8
%
wenzelm@26840
     9
\isatagtheory
wenzelm@26840
    10
\isacommand{theory}\isamarkupfalse%
wenzelm@26840
    11
\ ZF{\isacharunderscore}Specific\isanewline
wenzelm@26895
    12
\isakeyword{imports}\ Main\isanewline
wenzelm@26845
    13
\isakeyword{begin}%
wenzelm@26845
    14
\endisatagtheory
wenzelm@26845
    15
{\isafoldtheory}%
wenzelm@26845
    16
%
wenzelm@26845
    17
\isadelimtheory
wenzelm@26845
    18
%
wenzelm@26845
    19
\endisadelimtheory
wenzelm@26845
    20
%
wenzelm@26852
    21
\isamarkupchapter{Isabelle/ZF \label{ch:zf}%
wenzelm@26845
    22
}
wenzelm@26845
    23
\isamarkuptrue%
wenzelm@26845
    24
%
wenzelm@26845
    25
\isamarkupsection{Type checking%
wenzelm@26845
    26
}
wenzelm@26845
    27
\isamarkuptrue%
wenzelm@26845
    28
%
wenzelm@26845
    29
\begin{isamarkuptext}%
wenzelm@26845
    30
The ZF logic is essentially untyped, so the concept of ``type
wenzelm@26845
    31
  checking'' is performed as logical reasoning about set-membership
wenzelm@26845
    32
  statements.  A special method assists users in this task; a version
wenzelm@26845
    33
  of this is already declared as a ``solver'' in the standard
wenzelm@26845
    34
  Simplifier setup.
wenzelm@26845
    35
wenzelm@26845
    36
  \begin{matharray}{rcl}
wenzelm@28788
    37
    \indexdef{ZF}{command}{print\_tcset}\hypertarget{command.ZF.print-tcset}{\hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28788
    38
    \indexdef{ZF}{method}{typecheck}\hypertarget{method.ZF.typecheck}{\hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}}} & : & \isa{method} \\
wenzelm@28788
    39
    \indexdef{ZF}{attribute}{TC}\hypertarget{attribute.ZF.TC}{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}} & : & \isa{attribute} \\
wenzelm@26845
    40
  \end{matharray}
wenzelm@26845
    41
wenzelm@26845
    42
  \begin{rail}
wenzelm@26845
    43
    'TC' (() | 'add' | 'del')
wenzelm@26845
    44
    ;
wenzelm@26845
    45
  \end{rail}
wenzelm@26845
    46
wenzelm@28788
    47
  \begin{description}
wenzelm@26845
    48
  
wenzelm@28788
    49
  \item \hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}} prints the collection of
wenzelm@26845
    50
  typechecking rules of the current context.
wenzelm@26845
    51
  
wenzelm@28788
    52
  \item \hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}} attempts to solve any pending
wenzelm@26845
    53
  type-checking problems in subgoals.
wenzelm@26845
    54
  
wenzelm@28788
    55
  \item \hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}} adds or deletes type-checking rules from
wenzelm@28788
    56
  the context.
wenzelm@26845
    57
wenzelm@28788
    58
  \end{description}%
wenzelm@26845
    59
\end{isamarkuptext}%
wenzelm@26845
    60
\isamarkuptrue%
wenzelm@26845
    61
%
wenzelm@26845
    62
\isamarkupsection{(Co)Inductive sets and datatypes%
wenzelm@26845
    63
}
wenzelm@26845
    64
\isamarkuptrue%
wenzelm@26845
    65
%
wenzelm@26845
    66
\isamarkupsubsection{Set definitions%
wenzelm@26845
    67
}
wenzelm@26845
    68
\isamarkuptrue%
wenzelm@26845
    69
%
wenzelm@26845
    70
\begin{isamarkuptext}%
wenzelm@26845
    71
In ZF everything is a set.  The generic inductive package also
wenzelm@26845
    72
  provides a specific view for ``datatype'' specifications.
wenzelm@26845
    73
  Coinductive definitions are available in both cases, too.
wenzelm@26845
    74
wenzelm@26845
    75
  \begin{matharray}{rcl}
wenzelm@28788
    76
    \indexdef{ZF}{command}{inductive}\hypertarget{command.ZF.inductive}{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@28788
    77
    \indexdef{ZF}{command}{coinductive}\hypertarget{command.ZF.coinductive}{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@28788
    78
    \indexdef{ZF}{command}{datatype}\hypertarget{command.ZF.datatype}{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@28788
    79
    \indexdef{ZF}{command}{codatatype}\hypertarget{command.ZF.codatatype}{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@26845
    80
  \end{matharray}
wenzelm@26845
    81
wenzelm@26845
    82
  \begin{rail}
wenzelm@26845
    83
    ('inductive' | 'coinductive') domains intros hints
wenzelm@26845
    84
    ;
wenzelm@26845
    85
wenzelm@26845
    86
    domains: 'domains' (term + '+') ('<=' | subseteq) term
wenzelm@26845
    87
    ;
wenzelm@26845
    88
    intros: 'intros' (thmdecl? prop +)
wenzelm@26845
    89
    ;
wenzelm@26845
    90
    hints: monos? condefs? typeintros? typeelims?
wenzelm@26845
    91
    ;
wenzelm@26845
    92
    monos: ('monos' thmrefs)?
wenzelm@26845
    93
    ;
wenzelm@40255
    94
    condefs: ('con_defs' thmrefs)?
wenzelm@26845
    95
    ;
wenzelm@40255
    96
    typeintros: ('type_intros' thmrefs)?
wenzelm@26845
    97
    ;
wenzelm@40255
    98
    typeelims: ('type_elims' thmrefs)?
wenzelm@26845
    99
    ;
wenzelm@26845
   100
  \end{rail}
wenzelm@26845
   101
wenzelm@26845
   102
  In the following syntax specification \isa{{\isachardoublequote}monos{\isachardoublequote}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
wenzelm@26845
   103
wenzelm@26845
   104
  \begin{rail}
wenzelm@26845
   105
    ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
wenzelm@26845
   106
    ;
wenzelm@26845
   107
wenzelm@26845
   108
    domain: ('<=' | subseteq) term
wenzelm@26845
   109
    ;
wenzelm@26845
   110
    dtspec: term '=' (con + '|')
wenzelm@26845
   111
    ;
wenzelm@26845
   112
    con: name ('(' (term ',' +) ')')?  
wenzelm@26845
   113
    ;
wenzelm@26845
   114
    hints: monos? typeintros? typeelims?
wenzelm@26845
   115
    ;
wenzelm@26845
   116
  \end{rail}
wenzelm@26845
   117
wenzelm@26845
   118
  See \cite{isabelle-ZF} for further information on inductive
wenzelm@26845
   119
  definitions in ZF, but note that this covers the old-style theory
wenzelm@26845
   120
  format.%
wenzelm@26845
   121
\end{isamarkuptext}%
wenzelm@26845
   122
\isamarkuptrue%
wenzelm@26845
   123
%
wenzelm@26845
   124
\isamarkupsubsection{Primitive recursive functions%
wenzelm@26845
   125
}
wenzelm@26845
   126
\isamarkuptrue%
wenzelm@26845
   127
%
wenzelm@26845
   128
\begin{isamarkuptext}%
wenzelm@26845
   129
\begin{matharray}{rcl}
wenzelm@28788
   130
    \indexdef{ZF}{command}{primrec}\hypertarget{command.ZF.primrec}{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@26845
   131
  \end{matharray}
wenzelm@26845
   132
wenzelm@26845
   133
  \begin{rail}
wenzelm@26845
   134
    'primrec' (thmdecl? prop +)
wenzelm@26845
   135
    ;
wenzelm@26845
   136
  \end{rail}%
wenzelm@26845
   137
\end{isamarkuptext}%
wenzelm@26845
   138
\isamarkuptrue%
wenzelm@26845
   139
%
wenzelm@26845
   140
\isamarkupsubsection{Cases and induction: emulating tactic scripts%
wenzelm@26845
   141
}
wenzelm@26845
   142
\isamarkuptrue%
wenzelm@26845
   143
%
wenzelm@26845
   144
\begin{isamarkuptext}%
wenzelm@26845
   145
The following important tactical tools of Isabelle/ZF have been
wenzelm@26845
   146
  ported to Isar.  These should not be used in proper proof texts.
wenzelm@26845
   147
wenzelm@26845
   148
  \begin{matharray}{rcl}
wenzelm@28788
   149
    \indexdef{ZF}{method}{case\_tac}\hypertarget{method.ZF.case-tac}{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
wenzelm@28788
   150
    \indexdef{ZF}{method}{induct\_tac}\hypertarget{method.ZF.induct-tac}{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
wenzelm@28788
   151
    \indexdef{ZF}{method}{ind\_cases}\hypertarget{method.ZF.ind-cases}{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
wenzelm@28788
   152
    \indexdef{ZF}{command}{inductive\_cases}\hypertarget{command.ZF.inductive-cases}{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@26845
   153
  \end{matharray}
wenzelm@26845
   154
wenzelm@26845
   155
  \begin{rail}
wenzelm@40255
   156
    ('case_tac' | 'induct_tac') goalspec? name
wenzelm@26845
   157
    ;
wenzelm@26845
   158
    indcases (prop +)
wenzelm@26845
   159
    ;
wenzelm@26845
   160
    inductivecases (thmdecl? (prop +) + 'and')
wenzelm@26845
   161
    ;
wenzelm@26845
   162
  \end{rail}%
wenzelm@26845
   163
\end{isamarkuptext}%
wenzelm@26845
   164
\isamarkuptrue%
wenzelm@26845
   165
%
wenzelm@26845
   166
\isadelimtheory
wenzelm@26845
   167
%
wenzelm@26845
   168
\endisadelimtheory
wenzelm@26845
   169
%
wenzelm@26845
   170
\isatagtheory
wenzelm@26840
   171
\isacommand{end}\isamarkupfalse%
wenzelm@26840
   172
%
wenzelm@26840
   173
\endisatagtheory
wenzelm@26840
   174
{\isafoldtheory}%
wenzelm@26840
   175
%
wenzelm@26840
   176
\isadelimtheory
wenzelm@26840
   177
%
wenzelm@26840
   178
\endisadelimtheory
wenzelm@26845
   179
\isanewline
wenzelm@26840
   180
\end{isabellebody}%
wenzelm@26840
   181
%%% Local Variables:
wenzelm@26840
   182
%%% mode: latex
wenzelm@26840
   183
%%% TeX-master: "root"
wenzelm@26840
   184
%%% End: