--- a/doc-src/IsarRef/Thy/ZF_Specific.thy Wed May 07 13:05:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Wed May 07 13:38:15 2008 +0200
@@ -4,4 +4,137 @@
imports ZF
begin
+chapter {* ZF specific elements *}
+
+section {* Type checking *}
+
+text {*
+ The ZF logic is essentially untyped, so the concept of ``type
+ checking'' is performed as logical reasoning about set-membership
+ statements. A special method assists users in this task; a version
+ of this is already declared as a ``solver'' in the standard
+ Simplifier setup.
+
+ \begin{matharray}{rcl}
+ @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{method_def (ZF) typecheck} & : & \isarmeth \\
+ @{attribute_def (ZF) TC} & : & \isaratt \\
+ \end{matharray}
+
+ \begin{rail}
+ 'TC' (() | 'add' | 'del')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command (ZF) "print_tcset"}] prints the collection of
+ typechecking rules of the current context.
+
+ \item [@{method (ZF) typecheck}] attempts to solve any pending
+ type-checking problems in subgoals.
+
+ \item [@{attribute (ZF) TC}] adds or deletes type-checking rules
+ from the context.
+
+ \end{descr}
+*}
+
+
+section {* (Co)Inductive sets and datatypes *}
+
+subsection {* Set definitions *}
+
+text {*
+ In ZF everything is a set. The generic inductive package also
+ provides a specific view for ``datatype'' specifications.
+ Coinductive definitions are available in both cases, too.
+
+ \begin{matharray}{rcl}
+ @{command_def (ZF) "inductive"} & : & \isartrans{theory}{theory} \\
+ @{command_def (ZF) "coinductive"} & : & \isartrans{theory}{theory} \\
+ @{command_def (ZF) "datatype"} & : & \isartrans{theory}{theory} \\
+ @{command_def (ZF) "codatatype"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('inductive' | 'coinductive') domains intros hints
+ ;
+
+ domains: 'domains' (term + '+') ('<=' | subseteq) term
+ ;
+ intros: 'intros' (thmdecl? prop +)
+ ;
+ hints: monos? condefs? typeintros? typeelims?
+ ;
+ monos: ('monos' thmrefs)?
+ ;
+ condefs: ('con\_defs' thmrefs)?
+ ;
+ typeintros: ('type\_intros' thmrefs)?
+ ;
+ typeelims: ('type\_elims' thmrefs)?
+ ;
+ \end{rail}
+
+ In the following syntax specification @{text "monos"}, @{text
+ typeintros}, and @{text typeelims} are the same as above.
+
+ \begin{rail}
+ ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
+ ;
+
+ domain: ('<=' | subseteq) term
+ ;
+ dtspec: term '=' (con + '|')
+ ;
+ con: name ('(' (term ',' +) ')')?
+ ;
+ hints: monos? typeintros? typeelims?
+ ;
+ \end{rail}
+
+ See \cite{isabelle-ZF} for further information on inductive
+ definitions in ZF, but note that this covers the old-style theory
+ format.
+*}
+
+
+subsection {* Primitive recursive functions *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def (ZF) "primrec"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'primrec' (thmdecl? prop +)
+ ;
+ \end{rail}
+*}
+
+
+subsection {* Cases and induction: emulating tactic scripts *}
+
+text {*
+ The following important tactical tools of Isabelle/ZF have been
+ ported to Isar. These should not be used in proper proof texts.
+
+ \begin{matharray}{rcl}
+ @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
+ @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
+ @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
+ @{command_def (ZF) "inductive_cases"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('case\_tac' | 'induct\_tac') goalspec? name
+ ;
+ indcases (prop +)
+ ;
+ inductivecases (thmdecl? (prop +) + 'and')
+ ;
+ \end{rail}
+*}
+
end
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Wed May 07 13:05:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Wed May 07 13:38:15 2008 +0200
@@ -12,17 +12,173 @@
\isacommand{theory}\isamarkupfalse%
\ ZF{\isacharunderscore}Specific\isanewline
\isakeyword{imports}\ ZF\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{ZF specific elements%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Type checking%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The ZF logic is essentially untyped, so the concept of ``type
+ checking'' is performed as logical reasoning about set-membership
+ statements. A special method assists users in this task; a version
+ of this is already declared as a ``solver'' in the standard
+ Simplifier setup.
+
+ \begin{matharray}{rcl}
+ \indexdef{ZF}{command}{print-tcset}\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{ZF}{method}{typecheck}\mbox{\isa{typecheck}} & : & \isarmeth \\
+ \indexdef{ZF}{attribute}{TC}\mbox{\isa{TC}} & : & \isaratt \\
+ \end{matharray}
+
+ \begin{rail}
+ 'TC' (() | 'add' | 'del')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}] prints the collection of
+ typechecking rules of the current context.
+
+ \item [\mbox{\isa{typecheck}}] attempts to solve any pending
+ type-checking problems in subgoals.
+
+ \item [\mbox{\isa{TC}}] adds or deletes type-checking rules
+ from the context.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{(Co)Inductive sets and datatypes%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Set definitions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In ZF everything is a set. The generic inductive package also
+ provides a specific view for ``datatype'' specifications.
+ Coinductive definitions are available in both cases, too.
+
+ \begin{matharray}{rcl}
+ \indexdef{ZF}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{ZF}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{ZF}{command}{datatype}\mbox{\isa{\isacommand{datatype}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{ZF}{command}{codatatype}\mbox{\isa{\isacommand{codatatype}}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('inductive' | 'coinductive') domains intros hints
+ ;
+
+ domains: 'domains' (term + '+') ('<=' | subseteq) term
+ ;
+ intros: 'intros' (thmdecl? prop +)
+ ;
+ hints: monos? condefs? typeintros? typeelims?
+ ;
+ monos: ('monos' thmrefs)?
+ ;
+ condefs: ('con\_defs' thmrefs)?
+ ;
+ typeintros: ('type\_intros' thmrefs)?
+ ;
+ typeelims: ('type\_elims' thmrefs)?
+ ;
+ \end{rail}
+
+ In the following syntax specification \isa{{\isachardoublequote}monos{\isachardoublequote}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
+
+ \begin{rail}
+ ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
+ ;
+
+ domain: ('<=' | subseteq) term
+ ;
+ dtspec: term '=' (con + '|')
+ ;
+ con: name ('(' (term ',' +) ')')?
+ ;
+ hints: monos? typeintros? typeelims?
+ ;
+ \end{rail}
+
+ See \cite{isabelle-ZF} for further information on inductive
+ definitions in ZF, but note that this covers the old-style theory
+ format.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Primitive recursive functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{ZF}{command}{primrec}\mbox{\isa{\isacommand{primrec}}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'primrec' (thmdecl? prop +)
+ ;
+ \end{rail}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Cases and induction: emulating tactic scripts%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The following important tactical tools of Isabelle/ZF have been
+ ported to Isar. These should not be used in proper proof texts.
+
+ \begin{matharray}{rcl}
+ \indexdef{ZF}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{ZF}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{ZF}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{ZF}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('case\_tac' | 'induct\_tac') goalspec? name
+ ;
+ indcases (prop +)
+ ;
+ inductivecases (thmdecl? (prop +) + 'and')
+ ;
+ \end{rail}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
-\isanewline
%
\endisadelimtheory
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/logics.tex Wed May 07 13:05:46 2008 +0200
+++ b/doc-src/IsarRef/logics.tex Wed May 07 13:38:15 2008 +0200
@@ -1049,147 +1049,6 @@
\end{descr}
-\section{ZF}
-
-\subsection{Type checking}
-
-The ZF logic is essentially untyped, so the concept of ``type checking'' is
-performed as logical reasoning about set-membership statements. A special
-method assists users in this task; a version of this is already declared as a
-``solver'' in the standard Simplifier setup.
-
-\indexisarcmdof{ZF}{print-tcset}\indexisarattof{ZF}{typecheck}\indexisarattof{ZF}{TC}
-
-\begin{matharray}{rcl}
- \isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\
- typecheck & : & \isarmeth \\
- TC & : & \isaratt \\
-\end{matharray}
-
-\begin{rail}
- 'TC' (() | 'add' | 'del')
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of
- the current context.
-
- Note that the component built into the Simplifier only knows about those
- rules being declared globally in the theory!
-
-\item [$typecheck$] attempts to solve any pending type-checking problems in
- subgoals.
-
-\item [$TC$] adds or deletes type-checking rules from the context.
-
-\end{descr}
-
-
-\subsection{(Co)Inductive sets and datatypes}
-
-\subsubsection{Set definitions}
-
-In ZF everything is a set. The generic inductive package also provides a
-specific view for ``datatype'' specifications. Coinductive definitions are
-available in both cases, too.
-
-\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
-\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}
-\begin{matharray}{rcl}
- \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
- \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
- \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
- \isarcmd{codatatype} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\railalias{CONDEFS}{con\_defs}
-\railterm{CONDEFS}
-
-\railalias{TYPEINTROS}{type\_intros}
-\railterm{TYPEINTROS}
-
-\railalias{TYPEELIMS}{type\_elims}
-\railterm{TYPEELIMS}
-
-\begin{rail}
- ('inductive' | 'coinductive') domains intros hints
- ;
-
- domains: 'domains' (term + '+') ('<=' | subseteq) term
- ;
- intros: 'intros' (thmdecl? prop +)
- ;
- hints: monos? condefs? typeintros? typeelims?
- ;
- monos: ('monos' thmrefs)?
- ;
- condefs: (CONDEFS thmrefs)?
- ;
- typeintros: (TYPEINTROS thmrefs)?
- ;
- typeelims: (TYPEELIMS thmrefs)?
- ;
-\end{rail}
-
-In the following diagram $monos$, $typeintros$, and $typeelims$ are the same
-as above.
-
-\begin{rail}
- ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
- ;
-
- domain: ('<=' | subseteq) term
- ;
- dtspec: term '=' (con + '|')
- ;
- con: name ('(' (term ',' +) ')')?
- ;
- hints: monos? typeintros? typeelims?
- ;
-\end{rail}
-
-See \cite{isabelle-ZF} for further information on inductive definitions in
-HOL, but note that this covers the old-style theory format.
-
-
-\subsubsection{Primitive recursive functions}
-
-\indexisarcmdof{ZF}{primrec}
-\begin{matharray}{rcl}
- \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\begin{rail}
- 'primrec' (thmdecl? prop +)
- ;
-\end{rail}
-
-
-\subsubsection{Cases and induction: emulating tactic scripts}
-
-The following important tactical tools of Isabelle/ZF have been ported to
-Isar. These should be never used in proper proof texts!
-
-\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac}
-\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases}
-\begin{matharray}{rcl}
- case_tac^* & : & \isarmeth \\
- induct_tac^* & : & \isarmeth \\
- ind_cases^* & : & \isarmeth \\
- \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\begin{rail}
- (casetac | inducttac) goalspec? name
- ;
- indcases (prop +)
- ;
- inductivecases (thmdecl? (prop +) + 'and')
- ;
-\end{rail}
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"