author | wenzelm |
Thu, 05 May 2011 23:15:11 +0200 | |
changeset 42704 | 3f19e324ff59 |
parent 42651 | e3fdb7c96be5 |
child 42705 | 528a2ba8fa74 |
permissions | -rw-r--r-- |
26840 | 1 |
theory ZF_Specific |
42651 | 2 |
imports Base Main |
26840 | 3 |
begin |
4 |
||
26852 | 5 |
chapter {* Isabelle/ZF \label{ch:zf} *} |
26845 | 6 |
|
7 |
section {* Type checking *} |
|
8 |
||
9 |
text {* |
|
10 |
The ZF logic is essentially untyped, so the concept of ``type |
|
11 |
checking'' is performed as logical reasoning about set-membership |
|
12 |
statements. A special method assists users in this task; a version |
|
13 |
of this is already declared as a ``solver'' in the standard |
|
14 |
Simplifier setup. |
|
15 |
||
16 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
17 |
@{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
18 |
@{method_def (ZF) typecheck} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
19 |
@{attribute_def (ZF) TC} & : & @{text attribute} \\ |
26845 | 20 |
\end{matharray} |
21 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
22 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
23 |
@@{attribute (ZF) TC} (() | 'add' | 'del') |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
24 |
"} |
26845 | 25 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
26 |
\begin{description} |
26845 | 27 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
28 |
\item @{command (ZF) "print_tcset"} prints the collection of |
26845 | 29 |
typechecking rules of the current context. |
30 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
31 |
\item @{method (ZF) typecheck} attempts to solve any pending |
26845 | 32 |
type-checking problems in subgoals. |
33 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
34 |
\item @{attribute (ZF) TC} adds or deletes type-checking rules from |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
35 |
the context. |
26845 | 36 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
37 |
\end{description} |
26845 | 38 |
*} |
39 |
||
40 |
||
41 |
section {* (Co)Inductive sets and datatypes *} |
|
42 |
||
43 |
subsection {* Set definitions *} |
|
44 |
||
45 |
text {* |
|
46 |
In ZF everything is a set. The generic inductive package also |
|
47 |
provides a specific view for ``datatype'' specifications. |
|
48 |
Coinductive definitions are available in both cases, too. |
|
49 |
||
50 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
51 |
@{command_def (ZF) "inductive"} & : & @{text "theory \<rightarrow> theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
52 |
@{command_def (ZF) "coinductive"} & : & @{text "theory \<rightarrow> theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
53 |
@{command_def (ZF) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
54 |
@{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 55 |
\end{matharray} |
56 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
57 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
58 |
(@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints |
26845 | 59 |
; |
60 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
61 |
domains: @'domains' (@{syntax term} + '+') ('<=' | '\<subseteq>') @{syntax term} |
26845 | 62 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
63 |
intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +) |
26845 | 64 |
; |
42704 | 65 |
hints: @{syntax (ZF) \"monos\"}? condefs? \\ |
66 |
@{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? |
|
26845 | 67 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
68 |
@{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs} |
26845 | 69 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
70 |
condefs: @'con_defs' @{syntax thmrefs} |
26845 | 71 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
72 |
@{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs} |
26845 | 73 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
74 |
@{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
75 |
"} |
26845 | 76 |
|
77 |
In the following syntax specification @{text "monos"}, @{text |
|
78 |
typeintros}, and @{text typeelims} are the same as above. |
|
79 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
80 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
81 |
(@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints |
26845 | 82 |
; |
83 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
84 |
domain: ('<=' | '\<subseteq>') @{syntax term} |
26845 | 85 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
86 |
dtspec: @{syntax term} '=' (con + '|') |
26845 | 87 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
88 |
con: @{syntax name} ('(' (@{syntax term} ',' +) ')')? |
26845 | 89 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
90 |
hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
91 |
"} |
26845 | 92 |
|
93 |
See \cite{isabelle-ZF} for further information on inductive |
|
94 |
definitions in ZF, but note that this covers the old-style theory |
|
95 |
format. |
|
96 |
*} |
|
97 |
||
98 |
||
99 |
subsection {* Primitive recursive functions *} |
|
100 |
||
101 |
text {* |
|
102 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
103 |
@{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 104 |
\end{matharray} |
105 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
106 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
107 |
@@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
108 |
"} |
26845 | 109 |
*} |
110 |
||
111 |
||
112 |
subsection {* Cases and induction: emulating tactic scripts *} |
|
113 |
||
114 |
text {* |
|
115 |
The following important tactical tools of Isabelle/ZF have been |
|
116 |
ported to Isar. These should not be used in proper proof texts. |
|
117 |
||
118 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
119 |
@{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
120 |
@{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
121 |
@{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
122 |
@{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 123 |
\end{matharray} |
124 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
125 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
126 |
(@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goalspec}? @{syntax name} |
26845 | 127 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
128 |
@@{method (ZF) ind_cases} (@{syntax prop} +) |
26845 | 129 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
130 |
@@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and') |
26845 | 131 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
132 |
"} |
26845 | 133 |
*} |
134 |
||
26840 | 135 |
end |