# HG changeset patch # User wenzelm # Date 1210160295 -7200 # Node ID d86eb226ecba00ac2172342e94da1df0a5ee743f # Parent 46b6306c181ee99c24bf0767e019185c87521c04 converted ZF specific elements; diff -r 46b6306c181e -r d86eb226ecba doc-src/IsarRef/Thy/ZF_Specific.thy --- 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 diff -r 46b6306c181e -r d86eb226ecba doc-src/IsarRef/Thy/document/ZF_Specific.tex --- 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 diff -r 46b6306c181e -r d86eb226ecba doc-src/IsarRef/logics.tex --- 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"