7 chapter {* Isabelle/ZF \label{ch:zf} *}
9 section {* Type checking *}
12 The ZF logic is essentially untyped, so the concept of ``type
13 checking'' is performed as logical reasoning about set-membership
14 statements. A special method assists users in this task; a version
15 of this is already declared as a ``solver'' in the standard
18 \begin{matharray}{rcl}
19 @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
20 @{method_def (ZF) typecheck} & : & \isarmeth \\
21 @{attribute_def (ZF) TC} & : & \isaratt \\
25 'TC' (() | 'add' | 'del')
31 \item [@{command (ZF) "print_tcset"}] prints the collection of
32 typechecking rules of the current context.
34 \item [@{method (ZF) typecheck}] attempts to solve any pending
35 type-checking problems in subgoals.
37 \item [@{attribute (ZF) TC}] adds or deletes type-checking rules
44 section {* (Co)Inductive sets and datatypes *}
46 subsection {* Set definitions *}
49 In ZF everything is a set. The generic inductive package also
50 provides a specific view for ``datatype'' specifications.
51 Coinductive definitions are available in both cases, too.
53 \begin{matharray}{rcl}
54 @{command_def (ZF) "inductive"} & : & \isartrans{theory}{theory} \\
55 @{command_def (ZF) "coinductive"} & : & \isartrans{theory}{theory} \\
56 @{command_def (ZF) "datatype"} & : & \isartrans{theory}{theory} \\
57 @{command_def (ZF) "codatatype"} & : & \isartrans{theory}{theory} \\
61 ('inductive' | 'coinductive') domains intros hints
64 domains: 'domains' (term + '+') ('<=' | subseteq) term
66 intros: 'intros' (thmdecl? prop +)
68 hints: monos? condefs? typeintros? typeelims?
70 monos: ('monos' thmrefs)?
72 condefs: ('con\_defs' thmrefs)?
74 typeintros: ('type\_intros' thmrefs)?
76 typeelims: ('type\_elims' thmrefs)?
80 In the following syntax specification @{text "monos"}, @{text
81 typeintros}, and @{text typeelims} are the same as above.
84 ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
87 domain: ('<=' | subseteq) term
89 dtspec: term '=' (con + '|')
91 con: name ('(' (term ',' +) ')')?
93 hints: monos? typeintros? typeelims?
97 See \cite{isabelle-ZF} for further information on inductive
98 definitions in ZF, but note that this covers the old-style theory
103 subsection {* Primitive recursive functions *}
106 \begin{matharray}{rcl}
107 @{command_def (ZF) "primrec"} & : & \isartrans{theory}{theory} \\
111 'primrec' (thmdecl? prop +)
117 subsection {* Cases and induction: emulating tactic scripts *}
120 The following important tactical tools of Isabelle/ZF have been
121 ported to Isar. These should not be used in proper proof texts.
123 \begin{matharray}{rcl}
124 @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
125 @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
126 @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
127 @{command_def (ZF) "inductive_cases"} & : & \isartrans{theory}{theory} \\
131 ('case\_tac' | 'induct\_tac') goalspec? name
135 inductivecases (thmdecl? (prop +) + 'and')