author | wenzelm |
Tue, 03 May 2011 15:07:36 +0200 | |
changeset 42651 | e3fdb7c96be5 |
parent 42596 | 6c621a9d612a |
child 42704 | 3f19e324ff59 |
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 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
65 |
hints: @{syntax (ZF) \"monos\"}? condefs? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? |
26845 | 66 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
67 |
@{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs} |
26845 | 68 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
69 |
condefs: @'con_defs' @{syntax thmrefs} |
26845 | 70 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
71 |
@{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs} |
26845 | 72 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
73 |
@{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
74 |
"} |
26845 | 75 |
|
76 |
In the following syntax specification @{text "monos"}, @{text |
|
77 |
typeintros}, and @{text typeelims} are the same as above. |
|
78 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
79 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
80 |
(@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints |
26845 | 81 |
; |
82 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
83 |
domain: ('<=' | '\<subseteq>') @{syntax term} |
26845 | 84 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
85 |
dtspec: @{syntax term} '=' (con + '|') |
26845 | 86 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
87 |
con: @{syntax name} ('(' (@{syntax term} ',' +) ')')? |
26845 | 88 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
89 |
hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
90 |
"} |
26845 | 91 |
|
92 |
See \cite{isabelle-ZF} for further information on inductive |
|
93 |
definitions in ZF, but note that this covers the old-style theory |
|
94 |
format. |
|
95 |
*} |
|
96 |
||
97 |
||
98 |
subsection {* Primitive recursive functions *} |
|
99 |
||
100 |
text {* |
|
101 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
102 |
@{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 103 |
\end{matharray} |
104 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
105 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
106 |
@@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
107 |
"} |
26845 | 108 |
*} |
109 |
||
110 |
||
111 |
subsection {* Cases and induction: emulating tactic scripts *} |
|
112 |
||
113 |
text {* |
|
114 |
The following important tactical tools of Isabelle/ZF have been |
|
115 |
ported to Isar. These should not be used in proper proof texts. |
|
116 |
||
117 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
118 |
@{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
|
119 |
@{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
|
120 |
@{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
|
121 |
@{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 122 |
\end{matharray} |
123 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
124 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
125 |
(@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goalspec}? @{syntax name} |
26845 | 126 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
127 |
@@{method (ZF) ind_cases} (@{syntax prop} +) |
26845 | 128 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
129 |
@@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and') |
26845 | 130 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
131 |
"} |
26845 | 132 |
*} |
133 |
||
26840 | 134 |
end |