author | wenzelm |
Wed, 12 Mar 2014 14:17:13 +0100 | |
changeset 56059 | 2390391584c2 |
parent 55112 | b1a5d603fd12 |
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 |
(*>*) |
|
8 |
||
9 |
chapter {* Some Isar language elements *} |
|
26845 | 10 |
|
11 |
section {* Type checking *} |
|
12 |
||
13 |
text {* |
|
14 |
The ZF logic is essentially untyped, so the concept of ``type |
|
15 |
checking'' is performed as logical reasoning about set-membership |
|
16 |
statements. A special method assists users in this task; a version |
|
17 |
of this is already declared as a ``solver'' in the standard |
|
18 |
Simplifier setup. |
|
19 |
||
20 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
21 |
@{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
|
22 |
@{method_def (ZF) typecheck} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
23 |
@{attribute_def (ZF) TC} & : & @{text attribute} \\ |
26845 | 24 |
\end{matharray} |
25 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
26 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
27 |
@@{attribute (ZF) TC} (() | 'add' | 'del') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
28 |
\<close>} |
26845 | 29 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
30 |
\begin{description} |
26845 | 31 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
32 |
\item @{command (ZF) "print_tcset"} prints the collection of |
26845 | 33 |
typechecking rules of the current context. |
34 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
35 |
\item @{method (ZF) typecheck} attempts to solve any pending |
26845 | 36 |
type-checking problems in subgoals. |
37 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
38 |
\item @{attribute (ZF) TC} adds or deletes type-checking rules from |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
39 |
the context. |
26845 | 40 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
26894
diff
changeset
|
41 |
\end{description} |
26845 | 42 |
*} |
43 |
||
44 |
||
45 |
section {* (Co)Inductive sets and datatypes *} |
|
46 |
||
47 |
subsection {* Set definitions *} |
|
48 |
||
49 |
text {* |
|
50 |
In ZF everything is a set. The generic inductive package also |
|
51 |
provides a specific view for ``datatype'' specifications. |
|
52 |
Coinductive definitions are available in both cases, too. |
|
53 |
||
54 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
55 |
@{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
|
56 |
@{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
|
57 |
@{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
|
58 |
@{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 59 |
\end{matharray} |
60 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
61 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
62 |
(@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints |
26845 | 63 |
; |
64 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
65 |
domains: @'domains' (@{syntax term} + '+') ('<=' | '\<subseteq>') @{syntax term} |
26845 | 66 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
67 |
intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +) |
26845 | 68 |
; |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
69 |
hints: @{syntax (ZF) "monos"}? condefs? \<newline> |
42704 | 70 |
@{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? |
26845 | 71 |
; |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
72 |
@{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs} |
26845 | 73 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
74 |
condefs: @'con_defs' @{syntax thmrefs} |
26845 | 75 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
76 |
@{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs} |
26845 | 77 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
78 |
@{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
79 |
\<close>} |
26845 | 80 |
|
81 |
In the following syntax specification @{text "monos"}, @{text |
|
82 |
typeintros}, and @{text typeelims} are the same as above. |
|
83 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
84 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
85 |
(@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints |
26845 | 86 |
; |
87 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
88 |
domain: ('<=' | '\<subseteq>') @{syntax term} |
26845 | 89 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
90 |
dtspec: @{syntax term} '=' (con + '|') |
26845 | 91 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
92 |
con: @{syntax name} ('(' (@{syntax term} ',' +) ')')? |
26845 | 93 |
; |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
94 |
hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? |
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
95 |
\<close>} |
26845 | 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} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
107 |
@{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 108 |
\end{matharray} |
109 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
110 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
111 |
@@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +) |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
112 |
\<close>} |
26845 | 113 |
*} |
114 |
||
115 |
||
116 |
subsection {* Cases and induction: emulating tactic scripts *} |
|
117 |
||
118 |
text {* |
|
119 |
The following important tactical tools of Isabelle/ZF have been |
|
120 |
ported to Isar. These should not be used in proper proof texts. |
|
121 |
||
122 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
123 |
@{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
|
124 |
@{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
|
125 |
@{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
|
126 |
@{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\ |
26845 | 127 |
\end{matharray} |
128 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
129 |
@{rail \<open> |
42705 | 130 |
(@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name} |
26845 | 131 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
132 |
@@{method (ZF) ind_cases} (@{syntax prop} +) |
26845 | 133 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40255
diff
changeset
|
134 |
@@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
135 |
\<close>} |
26845 | 136 |
*} |
137 |
||
26840 | 138 |
end |