wenzelm@26840: (* $Id$ *)
wenzelm@26840: 
wenzelm@26840: theory ZF_Specific
wenzelm@26840: imports ZF
wenzelm@26840: begin
wenzelm@26840: 
wenzelm@26852: chapter {* Isabelle/ZF \label{ch:zf} *}
wenzelm@26845: 
wenzelm@26845: section {* Type checking *}
wenzelm@26845: 
wenzelm@26845: text {*
wenzelm@26845:   The ZF logic is essentially untyped, so the concept of ``type
wenzelm@26845:   checking'' is performed as logical reasoning about set-membership
wenzelm@26845:   statements.  A special method assists users in this task; a version
wenzelm@26845:   of this is already declared as a ``solver'' in the standard
wenzelm@26845:   Simplifier setup.
wenzelm@26845: 
wenzelm@26845:   \begin{matharray}{rcl}
wenzelm@26845:     @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
wenzelm@26845:     @{method_def (ZF) typecheck} & : & \isarmeth \\
wenzelm@26845:     @{attribute_def (ZF) TC} & : & \isaratt \\
wenzelm@26845:   \end{matharray}
wenzelm@26845: 
wenzelm@26845:   \begin{rail}
wenzelm@26845:     'TC' (() | 'add' | 'del')
wenzelm@26845:     ;
wenzelm@26845:   \end{rail}
wenzelm@26845: 
wenzelm@26845:   \begin{descr}
wenzelm@26845:   
wenzelm@26845:   \item [@{command (ZF) "print_tcset"}] prints the collection of
wenzelm@26845:   typechecking rules of the current context.
wenzelm@26845:   
wenzelm@26845:   \item [@{method (ZF) typecheck}] attempts to solve any pending
wenzelm@26845:   type-checking problems in subgoals.
wenzelm@26845:   
wenzelm@26845:   \item [@{attribute (ZF) TC}] adds or deletes type-checking rules
wenzelm@26845:   from the context.
wenzelm@26845: 
wenzelm@26845:   \end{descr}
wenzelm@26845: *}
wenzelm@26845: 
wenzelm@26845: 
wenzelm@26845: section {* (Co)Inductive sets and datatypes *}
wenzelm@26845: 
wenzelm@26845: subsection {* Set definitions *}
wenzelm@26845: 
wenzelm@26845: text {*
wenzelm@26845:   In ZF everything is a set.  The generic inductive package also
wenzelm@26845:   provides a specific view for ``datatype'' specifications.
wenzelm@26845:   Coinductive definitions are available in both cases, too.
wenzelm@26845: 
wenzelm@26845:   \begin{matharray}{rcl}
wenzelm@26845:     @{command_def (ZF) "inductive"} & : & \isartrans{theory}{theory} \\
wenzelm@26845:     @{command_def (ZF) "coinductive"} & : & \isartrans{theory}{theory} \\
wenzelm@26845:     @{command_def (ZF) "datatype"} & : & \isartrans{theory}{theory} \\
wenzelm@26845:     @{command_def (ZF) "codatatype"} & : & \isartrans{theory}{theory} \\
wenzelm@26845:   \end{matharray}
wenzelm@26845: 
wenzelm@26845:   \begin{rail}
wenzelm@26845:     ('inductive' | 'coinductive') domains intros hints
wenzelm@26845:     ;
wenzelm@26845: 
wenzelm@26845:     domains: 'domains' (term + '+') ('<=' | subseteq) term
wenzelm@26845:     ;
wenzelm@26845:     intros: 'intros' (thmdecl? prop +)
wenzelm@26845:     ;
wenzelm@26845:     hints: monos? condefs? typeintros? typeelims?
wenzelm@26845:     ;
wenzelm@26845:     monos: ('monos' thmrefs)?
wenzelm@26845:     ;
wenzelm@26845:     condefs: ('con\_defs' thmrefs)?
wenzelm@26845:     ;
wenzelm@26845:     typeintros: ('type\_intros' thmrefs)?
wenzelm@26845:     ;
wenzelm@26845:     typeelims: ('type\_elims' thmrefs)?
wenzelm@26845:     ;
wenzelm@26845:   \end{rail}
wenzelm@26845: 
wenzelm@26845:   In the following syntax specification @{text "monos"}, @{text
wenzelm@26845:   typeintros}, and @{text typeelims} are the same as above.
wenzelm@26845: 
wenzelm@26845:   \begin{rail}
wenzelm@26845:     ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
wenzelm@26845:     ;
wenzelm@26845: 
wenzelm@26845:     domain: ('<=' | subseteq) term
wenzelm@26845:     ;
wenzelm@26845:     dtspec: term '=' (con + '|')
wenzelm@26845:     ;
wenzelm@26845:     con: name ('(' (term ',' +) ')')?  
wenzelm@26845:     ;
wenzelm@26845:     hints: monos? typeintros? typeelims?
wenzelm@26845:     ;
wenzelm@26845:   \end{rail}
wenzelm@26845: 
wenzelm@26845:   See \cite{isabelle-ZF} for further information on inductive
wenzelm@26845:   definitions in ZF, but note that this covers the old-style theory
wenzelm@26845:   format.
wenzelm@26845: *}
wenzelm@26845: 
wenzelm@26845: 
wenzelm@26845: subsection {* Primitive recursive functions *}
wenzelm@26845: 
wenzelm@26845: text {*
wenzelm@26845:   \begin{matharray}{rcl}
wenzelm@26845:     @{command_def (ZF) "primrec"} & : & \isartrans{theory}{theory} \\
wenzelm@26845:   \end{matharray}
wenzelm@26845: 
wenzelm@26845:   \begin{rail}
wenzelm@26845:     'primrec' (thmdecl? prop +)
wenzelm@26845:     ;
wenzelm@26845:   \end{rail}
wenzelm@26845: *}
wenzelm@26845: 
wenzelm@26845: 
wenzelm@26845: subsection {* Cases and induction: emulating tactic scripts *}
wenzelm@26845: 
wenzelm@26845: text {*
wenzelm@26845:   The following important tactical tools of Isabelle/ZF have been
wenzelm@26845:   ported to Isar.  These should not be used in proper proof texts.
wenzelm@26845: 
wenzelm@26845:   \begin{matharray}{rcl}
wenzelm@26845:     @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
wenzelm@26845:     @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
wenzelm@26845:     @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
wenzelm@26845:     @{command_def (ZF) "inductive_cases"} & : & \isartrans{theory}{theory} \\
wenzelm@26845:   \end{matharray}
wenzelm@26845: 
wenzelm@26845:   \begin{rail}
wenzelm@26845:     ('case\_tac' | 'induct\_tac') goalspec? name
wenzelm@26845:     ;
wenzelm@26845:     indcases (prop +)
wenzelm@26845:     ;
wenzelm@26845:     inductivecases (thmdecl? (prop +) + 'and')
wenzelm@26845:     ;
wenzelm@26845:   \end{rail}
wenzelm@26845: *}
wenzelm@26845: 
wenzelm@26840: end