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