--- 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