--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Mon Aug 27 23:37:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,334 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{ZF{\isaliteral{5F}{\isacharunderscore}}Specific}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ ZF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
-\isakeyword{imports}\ Base\ Main\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Isabelle/ZF \label{ch:zf}%
-}
-\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}\hypertarget{command.ZF.print-tcset}{\hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}tcset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{method}{typecheck}\hypertarget{method.ZF.typecheck}{\hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}}} & : & \isa{method} \\
- \indexdef{ZF}{attribute}{TC}\hypertarget{attribute.ZF.TC}{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}} & : & \isa{attribute} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{add}}[]
-\rail@nextbar{2}
-\rail@term{\isa{del}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
-
- \begin{description}
-
- \item \hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}tcset}}}} prints the collection of
- typechecking rules of the current context.
-
- \item \hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}} attempts to solve any pending
- type-checking problems in subgoals.
-
- \item \hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}} adds or deletes type-checking rules from
- the context.
-
- \end{description}%
-\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}\hypertarget{command.ZF.inductive}{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{command}{coinductive}\hypertarget{command.ZF.coinductive}{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{command}{datatype}\hypertarget{command.ZF.datatype}{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{command}{codatatype}\hypertarget{command.ZF.codatatype}{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@bar
-\rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
-\rail@endbar
-\rail@nont{\isa{domains}}[]
-\rail@nont{\isa{intros}}[]
-\rail@nont{\isa{hints}}[]
-\rail@end
-\rail@begin{2}{\isa{domains}}
-\rail@term{\isa{\isakeyword{domains}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
-\rail@endplus
-\rail@bar
-\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@end
-\rail@begin{3}{\isa{intros}}
-\rail@term{\isa{\isakeyword{intros}}}[]
-\rail@plus
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{2}
-\rail@endplus
-\rail@end
-\rail@begin{5}{\isa{hints}}
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{condefs}}[]
-\rail@endbar
-\rail@cr{3}
-\rail@bar
-\rail@nextbar{4}
-\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{4}
-\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{\indexdef{ZF}{syntax}{monos}\hypertarget{syntax.ZF.monos}{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}}
-\rail@term{\isa{\isakeyword{monos}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\rail@begin{1}{\isa{condefs}}
-\rail@term{\isa{\isakeyword{con{\isaliteral{5F}{\isacharunderscore}}defs}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\rail@begin{1}{\indexdef{ZF}{syntax}{typeintros}\hypertarget{syntax.ZF.typeintros}{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}}
-\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}intros}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\rail@begin{1}{\indexdef{ZF}{syntax}{typeelims}\hypertarget{syntax.ZF.typeelims}{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}}
-\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}elims}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\end{railoutput}
-
-
- In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@bar
-\rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{domain}}[]
-\rail@endbar
-\rail@plus
-\rail@nont{\isa{dtspec}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{\isakeyword{and}}}[]
-\rail@endplus
-\rail@nont{\isa{hints}}[]
-\rail@end
-\rail@begin{2}{\isa{domain}}
-\rail@bar
-\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@end
-\rail@begin{2}{\isa{dtspec}}
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@plus
-\rail@nont{\isa{con}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
-\rail@endplus
-\rail@end
-\rail@begin{3}{\isa{con}}
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@term{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
-\rail@nextplus{2}
-\rail@endplus
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
-\rail@end
-\rail@begin{2}{\isa{hints}}
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
-
- 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}\hypertarget{command.ZF.primrec}{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
-\rail@plus
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{2}
-\rail@endplus
-\rail@end
-\end{railoutput}%
-\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}\hypertarget{method.ZF.case-tac}{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
- \indexdef{ZF}{method}{induct\_tac}\hypertarget{method.ZF.induct-tac}{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
- \indexdef{ZF}{method}{ind\_cases}\hypertarget{method.ZF.ind-cases}{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
- \indexdef{ZF}{command}{inductive\_cases}\hypertarget{command.ZF.inductive-cases}{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@bar
-\rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{3}{}
-\rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
-\rail@plus
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
-\rail@endbar
-\rail@plus
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@nextplus{2}
-\rail@cterm{\isa{\isakeyword{and}}}[]
-\rail@endplus
-\rail@end
-\end{railoutput}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: