doc-src/IsarRef/Thy/document/ZF_Specific.tex

added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")

%
\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: