1.1 --- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Wed May 07 13:05:46 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Wed May 07 13:38:15 2008 +0200
     1.3 @@ -4,4 +4,137 @@
     1.4  imports ZF
     1.5  begin
     1.6  
     1.7 +chapter {* ZF specific elements *}
     1.8 +
     1.9 +section {* Type checking *}
    1.10 +
    1.11 +text {*
    1.12 +  The ZF logic is essentially untyped, so the concept of ``type
    1.13 +  checking'' is performed as logical reasoning about set-membership
    1.14 +  statements.  A special method assists users in this task; a version
    1.15 +  of this is already declared as a ``solver'' in the standard
    1.16 +  Simplifier setup.
    1.17 +
    1.18 +  \begin{matharray}{rcl}
    1.19 +    @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
    1.20 +    @{method_def (ZF) typecheck} & : & \isarmeth \\
    1.21 +    @{attribute_def (ZF) TC} & : & \isaratt \\
    1.22 +  \end{matharray}
    1.23 +
    1.24 +  \begin{rail}
    1.25 +    'TC' (() | 'add' | 'del')
    1.26 +    ;
    1.27 +  \end{rail}
    1.28 +
    1.29 +  \begin{descr}
    1.30 +  
    1.31 +  \item [@{command (ZF) "print_tcset"}] prints the collection of
    1.32 +  typechecking rules of the current context.
    1.33 +  
    1.34 +  \item [@{method (ZF) typecheck}] attempts to solve any pending
    1.35 +  type-checking problems in subgoals.
    1.36 +  
    1.37 +  \item [@{attribute (ZF) TC}] adds or deletes type-checking rules
    1.38 +  from the context.
    1.39 +
    1.40 +  \end{descr}
    1.41 +*}
    1.42 +
    1.43 +
    1.44 +section {* (Co)Inductive sets and datatypes *}
    1.45 +
    1.46 +subsection {* Set definitions *}
    1.47 +
    1.48 +text {*
    1.49 +  In ZF everything is a set.  The generic inductive package also
    1.50 +  provides a specific view for ``datatype'' specifications.
    1.51 +  Coinductive definitions are available in both cases, too.
    1.52 +
    1.53 +  \begin{matharray}{rcl}
    1.54 +    @{command_def (ZF) "inductive"} & : & \isartrans{theory}{theory} \\
    1.55 +    @{command_def (ZF) "coinductive"} & : & \isartrans{theory}{theory} \\
    1.56 +    @{command_def (ZF) "datatype"} & : & \isartrans{theory}{theory} \\
    1.57 +    @{command_def (ZF) "codatatype"} & : & \isartrans{theory}{theory} \\
    1.58 +  \end{matharray}
    1.59 +
    1.60 +  \begin{rail}
    1.61 +    ('inductive' | 'coinductive') domains intros hints
    1.62 +    ;
    1.63 +
    1.64 +    domains: 'domains' (term + '+') ('<=' | subseteq) term
    1.65 +    ;
    1.66 +    intros: 'intros' (thmdecl? prop +)
    1.67 +    ;
    1.68 +    hints: monos? condefs? typeintros? typeelims?
    1.69 +    ;
    1.70 +    monos: ('monos' thmrefs)?
    1.71 +    ;
    1.72 +    condefs: ('con\_defs' thmrefs)?
    1.73 +    ;
    1.74 +    typeintros: ('type\_intros' thmrefs)?
    1.75 +    ;
    1.76 +    typeelims: ('type\_elims' thmrefs)?
    1.77 +    ;
    1.78 +  \end{rail}
    1.79 +
    1.80 +  In the following syntax specification @{text "monos"}, @{text
    1.81 +  typeintros}, and @{text typeelims} are the same as above.
    1.82 +
    1.83 +  \begin{rail}
    1.84 +    ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
    1.85 +    ;
    1.86 +
    1.87 +    domain: ('<=' | subseteq) term
    1.88 +    ;
    1.89 +    dtspec: term '=' (con + '|')
    1.90 +    ;
    1.91 +    con: name ('(' (term ',' +) ')')?  
    1.92 +    ;
    1.93 +    hints: monos? typeintros? typeelims?
    1.94 +    ;
    1.95 +  \end{rail}
    1.96 +
    1.97 +  See \cite{isabelle-ZF} for further information on inductive
    1.98 +  definitions in ZF, but note that this covers the old-style theory
    1.99 +  format.
   1.100 +*}
   1.101 +
   1.102 +
   1.103 +subsection {* Primitive recursive functions *}
   1.104 +
   1.105 +text {*
   1.106 +  \begin{matharray}{rcl}
   1.107 +    @{command_def (ZF) "primrec"} & : & \isartrans{theory}{theory} \\
   1.108 +  \end{matharray}
   1.109 +
   1.110 +  \begin{rail}
   1.111 +    'primrec' (thmdecl? prop +)
   1.112 +    ;
   1.113 +  \end{rail}
   1.114 +*}
   1.115 +
   1.116 +
   1.117 +subsection {* Cases and induction: emulating tactic scripts *}
   1.118 +
   1.119 +text {*
   1.120 +  The following important tactical tools of Isabelle/ZF have been
   1.121 +  ported to Isar.  These should not be used in proper proof texts.
   1.122 +
   1.123 +  \begin{matharray}{rcl}
   1.124 +    @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
   1.125 +    @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
   1.126 +    @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
   1.127 +    @{command_def (ZF) "inductive_cases"} & : & \isartrans{theory}{theory} \\
   1.128 +  \end{matharray}
   1.129 +
   1.130 +  \begin{rail}
   1.131 +    ('case\_tac' | 'induct\_tac') goalspec? name
   1.132 +    ;
   1.133 +    indcases (prop +)
   1.134 +    ;
   1.135 +    inductivecases (thmdecl? (prop +) + 'and')
   1.136 +    ;
   1.137 +  \end{rail}
   1.138 +*}
   1.139 +
   1.140  end