26840
|
1 |
(* $Id$ *)
|
|
2 |
|
|
3 |
theory ZF_Specific
|
26894
|
4 |
imports Main
|
26840
|
5 |
begin
|
|
6 |
|
26852
|
7 |
chapter {* Isabelle/ZF \label{ch:zf} *}
|
26845
|
8 |
|
|
9 |
section {* Type checking *}
|
|
10 |
|
|
11 |
text {*
|
|
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
|
|
16 |
Simplifier setup.
|
|
17 |
|
|
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 \\
|
|
22 |
\end{matharray}
|
|
23 |
|
|
24 |
\begin{rail}
|
|
25 |
'TC' (() | 'add' | 'del')
|
|
26 |
;
|
|
27 |
\end{rail}
|
|
28 |
|
|
29 |
\begin{descr}
|
|
30 |
|
|
31 |
\item [@{command (ZF) "print_tcset"}] prints the collection of
|
|
32 |
typechecking rules of the current context.
|
|
33 |
|
|
34 |
\item [@{method (ZF) typecheck}] attempts to solve any pending
|
|
35 |
type-checking problems in subgoals.
|
|
36 |
|
|
37 |
\item [@{attribute (ZF) TC}] adds or deletes type-checking rules
|
|
38 |
from the context.
|
|
39 |
|
|
40 |
\end{descr}
|
|
41 |
*}
|
|
42 |
|
|
43 |
|
|
44 |
section {* (Co)Inductive sets and datatypes *}
|
|
45 |
|
|
46 |
subsection {* Set definitions *}
|
|
47 |
|
|
48 |
text {*
|
|
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.
|
|
52 |
|
|
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} \\
|
|
58 |
\end{matharray}
|
|
59 |
|
|
60 |
\begin{rail}
|
|
61 |
('inductive' | 'coinductive') domains intros hints
|
|
62 |
;
|
|
63 |
|
|
64 |
domains: 'domains' (term + '+') ('<=' | subseteq) term
|
|
65 |
;
|
|
66 |
intros: 'intros' (thmdecl? prop +)
|
|
67 |
;
|
|
68 |
hints: monos? condefs? typeintros? typeelims?
|
|
69 |
;
|
|
70 |
monos: ('monos' thmrefs)?
|
|
71 |
;
|
|
72 |
condefs: ('con\_defs' thmrefs)?
|
|
73 |
;
|
|
74 |
typeintros: ('type\_intros' thmrefs)?
|
|
75 |
;
|
|
76 |
typeelims: ('type\_elims' thmrefs)?
|
|
77 |
;
|
|
78 |
\end{rail}
|
|
79 |
|
|
80 |
In the following syntax specification @{text "monos"}, @{text
|
|
81 |
typeintros}, and @{text typeelims} are the same as above.
|
|
82 |
|
|
83 |
\begin{rail}
|
|
84 |
('datatype' | 'codatatype') domain? (dtspec + 'and') hints
|
|
85 |
;
|
|
86 |
|
|
87 |
domain: ('<=' | subseteq) term
|
|
88 |
;
|
|
89 |
dtspec: term '=' (con + '|')
|
|
90 |
;
|
|
91 |
con: name ('(' (term ',' +) ')')?
|
|
92 |
;
|
|
93 |
hints: monos? typeintros? typeelims?
|
|
94 |
;
|
|
95 |
\end{rail}
|
|
96 |
|
|
97 |
See \cite{isabelle-ZF} for further information on inductive
|
|
98 |
definitions in ZF, but note that this covers the old-style theory
|
|
99 |
format.
|
|
100 |
*}
|
|
101 |
|
|
102 |
|
|
103 |
subsection {* Primitive recursive functions *}
|
|
104 |
|
|
105 |
text {*
|
|
106 |
\begin{matharray}{rcl}
|
|
107 |
@{command_def (ZF) "primrec"} & : & \isartrans{theory}{theory} \\
|
|
108 |
\end{matharray}
|
|
109 |
|
|
110 |
\begin{rail}
|
|
111 |
'primrec' (thmdecl? prop +)
|
|
112 |
;
|
|
113 |
\end{rail}
|
|
114 |
*}
|
|
115 |
|
|
116 |
|
|
117 |
subsection {* Cases and induction: emulating tactic scripts *}
|
|
118 |
|
|
119 |
text {*
|
|
120 |
The following important tactical tools of Isabelle/ZF have been
|
|
121 |
ported to Isar. These should not be used in proper proof texts.
|
|
122 |
|
|
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} \\
|
|
128 |
\end{matharray}
|
|
129 |
|
|
130 |
\begin{rail}
|
|
131 |
('case\_tac' | 'induct\_tac') goalspec? name
|
|
132 |
;
|
|
133 |
indcases (prop +)
|
|
134 |
;
|
|
135 |
inductivecases (thmdecl? (prop +) + 'and')
|
|
136 |
;
|
|
137 |
\end{rail}
|
|
138 |
*}
|
|
139 |
|
26840
|
140 |
end
|