author | wenzelm |
Thu, 13 Nov 2008 21:59:02 +0100 | |
changeset 28774 | 0e25ef17b06b |
parent 28764 | b65194fe4434 |
child 30168 | 9a20be5be90b |
permissions | -rw-r--r-- |
26782 | 1 |
(* $Id$ *) |
2 |
||
3 |
theory Generic |
|
26894 | 4 |
imports Main |
26782 | 5 |
begin |
6 |
||
7 |
chapter {* Generic tools and packages \label{ch:gen-tools} *} |
|
8 |
||
27040 | 9 |
section {* Configuration options *} |
26782 | 10 |
|
11 |
text {* |
|
12 |
Isabelle/Pure maintains a record of named configuration options |
|
13 |
within the theory or proof context, with values of type @{ML_type |
|
14 |
bool}, @{ML_type int}, or @{ML_type string}. Tools may declare |
|
15 |
options in ML, and then refer to these values (relative to the |
|
16 |
context). Thus global reference variables are easily avoided. The |
|
17 |
user may change the value of a configuration option by means of an |
|
18 |
associated attribute of the same name. This form of context |
|
19 |
declaration works particularly well with commands such as @{command |
|
20 |
"declare"} or @{command "using"}. |
|
21 |
||
22 |
For historical reasons, some tools cannot take the full proof |
|
23 |
context into account and merely refer to the background theory. |
|
24 |
This is accommodated by configuration options being declared as |
|
25 |
``global'', which may not be changed within a local context. |
|
26 |
||
27 |
\begin{matharray}{rcll} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
28 |
@{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\ |
26782 | 29 |
\end{matharray} |
30 |
||
31 |
\begin{rail} |
|
32 |
name ('=' ('true' | 'false' | int | name))? |
|
33 |
\end{rail} |
|
34 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
35 |
\begin{description} |
26782 | 36 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
37 |
\item @{command "print_configs"} prints the available configuration |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
38 |
options, with names, types, and current values. |
26782 | 39 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
40 |
\item @{text "name = value"} as an attribute expression modifies the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
41 |
named option, with the syntax of the value depending on the option's |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
42 |
type. For @{ML_type bool} the default value is @{text true}. Any |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
43 |
attempt to change a global option in a local context is ignored. |
26782 | 44 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
45 |
\end{description} |
26782 | 46 |
*} |
47 |
||
48 |
||
27040 | 49 |
section {* Basic proof tools *} |
26782 | 50 |
|
51 |
subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *} |
|
52 |
||
53 |
text {* |
|
54 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
55 |
@{method_def unfold} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
56 |
@{method_def fold} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
57 |
@{method_def insert} & : & @{text method} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
58 |
@{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
59 |
@{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
60 |
@{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
61 |
@{method_def succeed} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
62 |
@{method_def fail} & : & @{text method} \\ |
26782 | 63 |
\end{matharray} |
64 |
||
65 |
\begin{rail} |
|
66 |
('fold' | 'unfold' | 'insert') thmrefs |
|
67 |
; |
|
68 |
('erule' | 'drule' | 'frule') ('('nat')')? thmrefs |
|
69 |
; |
|
70 |
\end{rail} |
|
71 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
72 |
\begin{description} |
26782 | 73 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
74 |
\item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
75 |
"a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
76 |
all goals; any chained facts provided are inserted into the goal and |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
77 |
subject to rewriting as well. |
26782 | 78 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
79 |
\item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
80 |
into all goals of the proof state. Note that current facts |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
81 |
indicated for forward chaining are ignored. |
26782 | 82 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
83 |
\item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method drule}~@{text "a\<^sub>1 |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
84 |
\<dots> a\<^sub>n"}, and @{method frule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
85 |
basic @{method rule} method (see \secref{sec:pure-meth-att}), but |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
86 |
apply rules by elim-resolution, destruct-resolution, and |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
87 |
forward-resolution, respectively \cite{isabelle-ref}. The optional |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
88 |
natural number argument (default 0) specifies additional assumption |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
89 |
steps to be performed here. |
26782 | 90 |
|
91 |
Note that these methods are improper ones, mainly serving for |
|
92 |
experimentation and tactic script emulation. Different modes of |
|
93 |
basic rule application are usually expressed in Isar at the proof |
|
94 |
language level, rather than via implicit proof state manipulations. |
|
95 |
For example, a proper single-step elimination would be done using |
|
96 |
the plain @{method rule} method, with forward chaining of current |
|
97 |
facts. |
|
98 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
99 |
\item @{method succeed} yields a single (unchanged) result; it is |
26782 | 100 |
the identity of the ``@{text ","}'' method combinator (cf.\ |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27248
diff
changeset
|
101 |
\secref{sec:proof-meth}). |
26782 | 102 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
103 |
\item @{method fail} yields an empty result sequence; it is the |
26782 | 104 |
identity of the ``@{text "|"}'' method combinator (cf.\ |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27248
diff
changeset
|
105 |
\secref{sec:proof-meth}). |
26782 | 106 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
107 |
\end{description} |
26782 | 108 |
|
109 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
110 |
@{attribute_def tagged} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
111 |
@{attribute_def untagged} & : & @{text attribute} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
112 |
@{attribute_def THEN} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
113 |
@{attribute_def COMP} & : & @{text attribute} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
114 |
@{attribute_def unfolded} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
115 |
@{attribute_def folded} & : & @{text attribute} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
116 |
@{attribute_def rotated} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
117 |
@{attribute_def (Pure) elim_format} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
118 |
@{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
119 |
@{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\ |
26782 | 120 |
\end{matharray} |
121 |
||
122 |
\begin{rail} |
|
28764 | 123 |
'tagged' name name |
26782 | 124 |
; |
125 |
'untagged' name |
|
126 |
; |
|
127 |
('THEN' | 'COMP') ('[' nat ']')? thmref |
|
128 |
; |
|
129 |
('unfolded' | 'folded') thmrefs |
|
130 |
; |
|
131 |
'rotated' ( int )? |
|
132 |
\end{rail} |
|
133 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
134 |
\begin{description} |
26782 | 135 |
|
28764 | 136 |
\item @{attribute tagged}~@{text "name value"} and @{attribute |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
137 |
untagged}~@{text name} add and remove \emph{tags} of some theorem. |
26782 | 138 |
Tags may be any list of string pairs that serve as formal comment. |
28764 | 139 |
The first string is considered the tag name, the second its value. |
140 |
Note that @{attribute untagged} removes any tags of the same name. |
|
26782 | 141 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
142 |
\item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a} |
26782 | 143 |
compose rules by resolution. @{attribute THEN} resolves with the |
144 |
first premise of @{text a} (an alternative position may be also |
|
145 |
specified); the @{attribute COMP} version skips the automatic |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
146 |
lifting process that is normally intended (cf.\ @{ML [source=false] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
147 |
"op RS"} and @{ML [source=false] "op COMP"} in |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
148 |
\cite[\S5]{isabelle-ref}). |
26782 | 149 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
150 |
\item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
151 |
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
152 |
definitions throughout a rule. |
26782 | 153 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
154 |
\item @{attribute rotated}~@{text n} rotate the premises of a |
26782 | 155 |
theorem by @{text n} (default 1). |
156 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
157 |
\item @{attribute (Pure) elim_format} turns a destruction rule into |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
158 |
elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow> |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
159 |
(PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}. |
26782 | 160 |
|
161 |
Note that the Classical Reasoner (\secref{sec:classical}) provides |
|
162 |
its own version of this operation. |
|
163 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
164 |
\item @{attribute standard} puts a theorem into the standard form of |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
165 |
object-rules at the outermost theory level. Note that this |
26782 | 166 |
operation violates the local proof context (including active |
167 |
locales). |
|
168 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
169 |
\item @{attribute no_vars} replaces schematic variables by free |
26782 | 170 |
ones; this is mainly for tuning output of pretty printed theorems. |
171 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
172 |
\end{description} |
26782 | 173 |
*} |
174 |
||
175 |
||
27044 | 176 |
subsection {* Low-level equational reasoning *} |
177 |
||
178 |
text {* |
|
179 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
180 |
@{method_def subst} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
181 |
@{method_def hypsubst} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
182 |
@{method_def split} & : & @{text method} \\ |
27044 | 183 |
\end{matharray} |
184 |
||
185 |
\begin{rail} |
|
186 |
'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref |
|
187 |
; |
|
188 |
'split' ('(' 'asm' ')')? thmrefs |
|
189 |
; |
|
190 |
\end{rail} |
|
191 |
||
192 |
These methods provide low-level facilities for equational reasoning |
|
193 |
that are intended for specialized applications only. Normally, |
|
194 |
single step calculations would be performed in a structured text |
|
195 |
(see also \secref{sec:calculation}), while the Simplifier methods |
|
196 |
provide the canonical way for automated normalization (see |
|
197 |
\secref{sec:simplifier}). |
|
198 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
199 |
\begin{description} |
27044 | 200 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
201 |
\item @{method subst}~@{text eq} performs a single substitution step |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
202 |
using rule @{text eq}, which may be either a meta or object |
27044 | 203 |
equality. |
204 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
205 |
\item @{method subst}~@{text "(asm) eq"} substitutes in an |
27044 | 206 |
assumption. |
207 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
208 |
\item @{method subst}~@{text "(i \<dots> j) eq"} performs several |
27044 | 209 |
substitutions in the conclusion. The numbers @{text i} to @{text j} |
210 |
indicate the positions to substitute at. Positions are ordered from |
|
211 |
the top of the term tree moving down from left to right. For |
|
212 |
example, in @{text "(a + b) + (c + d)"} there are three positions |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
213 |
where commutativity of @{text "+"} is applicable: 1 refers to @{text |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
214 |
"a + b"}, 2 to the whole term, and 3 to @{text "c + d"}. |
27044 | 215 |
|
216 |
If the positions in the list @{text "(i \<dots> j)"} are non-overlapping |
|
217 |
(e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may |
|
218 |
assume all substitutions are performed simultaneously. Otherwise |
|
219 |
the behaviour of @{text subst} is not specified. |
|
220 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
221 |
\item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the |
27071 | 222 |
substitutions in the assumptions. The positions refer to the |
223 |
assumptions in order from left to right. For example, given in a |
|
224 |
goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of |
|
225 |
commutativity of @{text "+"} is the subterm @{text "a + b"} and |
|
226 |
position 2 is the subterm @{text "c + d"}. |
|
27044 | 227 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
228 |
\item @{method hypsubst} performs substitution using some |
27044 | 229 |
assumption; this only works for equations of the form @{text "x = |
230 |
t"} where @{text x} is a free or bound variable. |
|
231 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
232 |
\item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
233 |
splitting using the given rules. By default, splitting is performed |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
234 |
in the conclusion of a goal; the @{text "(asm)"} option indicates to |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
235 |
operate on assumptions instead. |
27044 | 236 |
|
237 |
Note that the @{method simp} method already involves repeated |
|
238 |
application of split rules as declared in the current context. |
|
239 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
240 |
\end{description} |
27044 | 241 |
*} |
242 |
||
243 |
||
26782 | 244 |
subsection {* Further tactic emulations \label{sec:tactics} *} |
245 |
||
246 |
text {* |
|
247 |
The following improper proof methods emulate traditional tactics. |
|
248 |
These admit direct access to the goal state, which is normally |
|
249 |
considered harmful! In particular, this may involve both numbered |
|
250 |
goal addressing (default 1), and dynamic instantiation within the |
|
251 |
scope of some subgoal. |
|
252 |
||
253 |
\begin{warn} |
|
254 |
Dynamic instantiations refer to universally quantified parameters |
|
255 |
of a subgoal (the dynamic context) rather than fixed variables and |
|
256 |
term abbreviations of a (static) Isar context. |
|
257 |
\end{warn} |
|
258 |
||
259 |
Tactic emulation methods, unlike their ML counterparts, admit |
|
260 |
simultaneous instantiation from both dynamic and static contexts. |
|
261 |
If names occur in both contexts goal parameters hide locally fixed |
|
262 |
variables. Likewise, schematic variables refer to term |
|
263 |
abbreviations, if present in the static context. Otherwise the |
|
264 |
schematic variable is interpreted as a schematic variable and left |
|
265 |
to be solved by unification with certain parts of the subgoal. |
|
266 |
||
267 |
Note that the tactic emulation proof methods in Isabelle/Isar are |
|
268 |
consistently named @{text foo_tac}. Note also that variable names |
|
269 |
occurring on left hand sides of instantiations must be preceded by a |
|
270 |
question mark if they coincide with a keyword or contain dots. This |
|
271 |
is consistent with the attribute @{attribute "where"} (see |
|
272 |
\secref{sec:pure-meth-att}). |
|
273 |
||
274 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
275 |
@{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
276 |
@{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
277 |
@{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
278 |
@{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
279 |
@{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
280 |
@{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
281 |
@{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
282 |
@{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
283 |
@{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
284 |
@{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
285 |
@{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
26782 | 286 |
\end{matharray} |
287 |
||
288 |
\begin{rail} |
|
289 |
( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec? |
|
290 |
( insts thmref | thmrefs ) |
|
291 |
; |
|
292 |
'subgoal\_tac' goalspec? (prop +) |
|
293 |
; |
|
294 |
'rename\_tac' goalspec? (name +) |
|
295 |
; |
|
296 |
'rotate\_tac' goalspec? int? |
|
297 |
; |
|
27223 | 298 |
('tactic' | 'raw_tactic') text |
26782 | 299 |
; |
300 |
||
301 |
insts: ((name '=' term) + 'and') 'in' |
|
302 |
; |
|
303 |
\end{rail} |
|
304 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
305 |
\begin{description} |
26782 | 306 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
307 |
\item @{method rule_tac} etc. do resolution of rules with explicit |
26782 | 308 |
instantiation. This works the same way as the ML tactics @{ML |
27239 | 309 |
res_inst_tac} etc. (see \cite[\S3]{isabelle-ref}) |
26782 | 310 |
|
311 |
Multiple rules may be only given if there is no instantiation; then |
|
312 |
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see |
|
313 |
\cite[\S3]{isabelle-ref}). |
|
314 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
315 |
\item @{method cut_tac} inserts facts into the proof state as |
27209 | 316 |
assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in |
26782 | 317 |
\cite[\S3]{isabelle-ref}. Note that the scope of schematic |
318 |
variables is spread over the main goal statement. Instantiations |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
319 |
may be given as well, see also ML tactic @{ML cut_inst_tac} in |
27209 | 320 |
\cite[\S3]{isabelle-ref}. |
26782 | 321 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
322 |
\item @{method thin_tac}~@{text \<phi>} deletes the specified assumption |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
323 |
from a subgoal; note that @{text \<phi>} may contain schematic variables. |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
324 |
See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}. |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
325 |
|
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
326 |
\item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an |
27239 | 327 |
assumption to a subgoal. See also @{ML subgoal_tac} and @{ML |
328 |
subgoals_tac} in \cite[\S3]{isabelle-ref}. |
|
26782 | 329 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
330 |
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
331 |
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
332 |
\emph{suffix} of variables. |
26782 | 333 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
334 |
\item @{method rotate_tac}~@{text n} rotates the assumptions of a |
26782 | 335 |
goal by @{text n} positions: from right to left if @{text n} is |
336 |
positive, and from left to right if @{text n} is negative; the |
|
337 |
default value is 1. See also @{ML rotate_tac} in |
|
338 |
\cite[\S3]{isabelle-ref}. |
|
339 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
340 |
\item @{method tactic}~@{text "text"} produces a proof method from |
26782 | 341 |
any ML text of type @{ML_type tactic}. Apart from the usual ML |
27223 | 342 |
environment and the current proof context, the ML code may refer to |
343 |
the locally bound values @{ML_text facts}, which indicates any |
|
344 |
current facts used for forward-chaining. |
|
26782 | 345 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
346 |
\item @{method raw_tactic} is similar to @{method tactic}, but |
27223 | 347 |
presents the goal state in its raw internal form, where simultaneous |
348 |
subgoals appear as conjunction of the logical framework instead of |
|
349 |
the usual split into several subgoals. While feature this is useful |
|
350 |
for debugging of complex method definitions, it should not never |
|
351 |
appear in production theories. |
|
26782 | 352 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
353 |
\end{description} |
26782 | 354 |
*} |
355 |
||
356 |
||
27040 | 357 |
section {* The Simplifier \label{sec:simplifier} *} |
26782 | 358 |
|
27040 | 359 |
subsection {* Simplification methods *} |
26782 | 360 |
|
361 |
text {* |
|
362 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
363 |
@{method_def simp} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
364 |
@{method_def simp_all} & : & @{text method} \\ |
26782 | 365 |
\end{matharray} |
366 |
||
367 |
\indexouternonterm{simpmod} |
|
368 |
\begin{rail} |
|
369 |
('simp' | 'simp\_all') ('!' ?) opt? (simpmod *) |
|
370 |
; |
|
371 |
||
27092 | 372 |
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')' |
26782 | 373 |
; |
374 |
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
|
375 |
'split' (() | 'add' | 'del')) ':' thmrefs |
|
376 |
; |
|
377 |
\end{rail} |
|
378 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
379 |
\begin{description} |
26782 | 380 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
381 |
\item @{method simp} invokes the Simplifier, after declaring |
26782 | 382 |
additional rules according to the arguments given. Note that the |
383 |
\railtterm{only} modifier first removes all other rewrite rules, |
|
384 |
congruences, and looper tactics (including splits), and then behaves |
|
385 |
like \railtterm{add}. |
|
386 |
||
387 |
\medskip The \railtterm{cong} modifiers add or delete Simplifier |
|
388 |
congruence rules (see also \cite{isabelle-ref}), the default is to |
|
389 |
add. |
|
390 |
||
391 |
\medskip The \railtterm{split} modifiers add or delete rules for the |
|
392 |
Splitter (see also \cite{isabelle-ref}), the default is to add. |
|
393 |
This works only if the Simplifier method has been properly setup to |
|
394 |
include the Splitter (all major object logics such HOL, HOLCF, FOL, |
|
395 |
ZF do this already). |
|
396 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
397 |
\item @{method simp_all} is similar to @{method simp}, but acts on |
26782 | 398 |
all goals (backwards from the last to the first one). |
399 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
400 |
\end{description} |
26782 | 401 |
|
402 |
By default the Simplifier methods take local assumptions fully into |
|
403 |
account, using equational assumptions in the subsequent |
|
404 |
normalization process, or simplifying assumptions themselves (cf.\ |
|
405 |
@{ML asm_full_simp_tac} in \cite[\S10]{isabelle-ref}). In |
|
406 |
structured proofs this is usually quite well behaved in practice: |
|
407 |
just the local premises of the actual goal are involved, additional |
|
408 |
facts may be inserted via explicit forward-chaining (via @{command |
|
409 |
"then"}, @{command "from"}, @{command "using"} etc.). The full |
|
410 |
context of premises is only included if the ``@{text "!"}'' (bang) |
|
411 |
argument is given, which should be used with some care, though. |
|
412 |
||
413 |
Additional Simplifier options may be specified to tune the behavior |
|
414 |
further (mostly for unstructured scripts with many accidental local |
|
415 |
facts): ``@{text "(no_asm)"}'' means assumptions are ignored |
|
416 |
completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means |
|
417 |
assumptions are used in the simplification of the conclusion but are |
|
418 |
not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text |
|
419 |
"(no_asm_use)"}'' means assumptions are simplified but are not used |
|
420 |
in the simplification of each other or the conclusion (cf.\ @{ML |
|
421 |
full_simp_tac}). For compatibility reasons, there is also an option |
|
422 |
``@{text "(asm_lr)"}'', which means that an assumption is only used |
|
423 |
for simplifying assumptions which are to the right of it (cf.\ @{ML |
|
424 |
asm_lr_simp_tac}). |
|
425 |
||
27092 | 426 |
The configuration option @{text "depth_limit"} limits the number of |
26782 | 427 |
recursive invocations of the simplifier during conditional |
428 |
rewriting. |
|
429 |
||
430 |
\medskip The Splitter package is usually configured to work as part |
|
431 |
of the Simplifier. The effect of repeatedly applying @{ML |
|
432 |
split_tac} can be simulated by ``@{text "(simp only: split: |
|
433 |
a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split} |
|
434 |
method available for single-step case splitting. |
|
435 |
*} |
|
436 |
||
437 |
||
27040 | 438 |
subsection {* Declaring rules *} |
26782 | 439 |
|
440 |
text {* |
|
441 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
442 |
@{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
443 |
@{attribute_def simp} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
444 |
@{attribute_def cong} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
445 |
@{attribute_def split} & : & @{text attribute} \\ |
26782 | 446 |
\end{matharray} |
447 |
||
448 |
\begin{rail} |
|
449 |
('simp' | 'cong' | 'split') (() | 'add' | 'del') |
|
450 |
; |
|
451 |
\end{rail} |
|
452 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
453 |
\begin{description} |
26782 | 454 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
455 |
\item @{command "print_simpset"} prints the collection of rules |
26782 | 456 |
declared to the Simplifier, which is also known as ``simpset'' |
457 |
internally \cite{isabelle-ref}. |
|
458 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
459 |
\item @{attribute simp} declares simplification rules. |
26782 | 460 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
461 |
\item @{attribute cong} declares congruence rules. |
26782 | 462 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
463 |
\item @{attribute split} declares case split rules. |
26782 | 464 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
465 |
\end{description} |
26782 | 466 |
*} |
467 |
||
468 |
||
27040 | 469 |
subsection {* Simplification procedures *} |
26782 | 470 |
|
471 |
text {* |
|
472 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
473 |
@{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
474 |
simproc & : & @{text attribute} \\ |
26782 | 475 |
\end{matharray} |
476 |
||
477 |
\begin{rail} |
|
478 |
'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))? |
|
479 |
; |
|
480 |
||
481 |
'simproc' (('add' ':')? | 'del' ':') (name+) |
|
482 |
; |
|
483 |
\end{rail} |
|
484 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
485 |
\begin{description} |
26782 | 486 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
487 |
\item @{command "simproc_setup"} defines a named simplification |
26782 | 488 |
procedure that is invoked by the Simplifier whenever any of the |
489 |
given term patterns match the current redex. The implementation, |
|
490 |
which is provided as ML source text, needs to be of type @{ML_type |
|
491 |
"morphism -> simpset -> cterm -> thm option"}, where the @{ML_type |
|
492 |
cterm} represents the current redex @{text r} and the result is |
|
493 |
supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a |
|
494 |
generalized version), or @{ML NONE} to indicate failure. The |
|
495 |
@{ML_type simpset} argument holds the full context of the current |
|
496 |
Simplifier invocation, including the actual Isar proof context. The |
|
497 |
@{ML_type morphism} informs about the difference of the original |
|
498 |
compilation context wrt.\ the one of the actual application later |
|
499 |
on. The optional @{keyword "identifier"} specifies theorems that |
|
500 |
represent the logical content of the abstract theory of this |
|
501 |
simproc. |
|
502 |
||
503 |
Morphisms and identifiers are only relevant for simprocs that are |
|
504 |
defined within a local target context, e.g.\ in a locale. |
|
505 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
506 |
\item @{text "simproc add: name"} and @{text "simproc del: name"} |
26782 | 507 |
add or delete named simprocs to the current Simplifier context. The |
508 |
default is to add a simproc. Note that @{command "simproc_setup"} |
|
509 |
already adds the new simproc to the subsequent context. |
|
510 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
511 |
\end{description} |
26782 | 512 |
*} |
513 |
||
514 |
||
27040 | 515 |
subsection {* Forward simplification *} |
26782 | 516 |
|
517 |
text {* |
|
518 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
519 |
@{attribute_def simplified} & : & @{text attribute} \\ |
26782 | 520 |
\end{matharray} |
521 |
||
522 |
\begin{rail} |
|
523 |
'simplified' opt? thmrefs? |
|
524 |
; |
|
525 |
||
26789 | 526 |
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')' |
26782 | 527 |
; |
528 |
\end{rail} |
|
529 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
530 |
\begin{description} |
26782 | 531 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
532 |
\item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
533 |
be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>, |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
534 |
a\<^sub>n"}, or the implicit Simplifier context if no arguments are given. |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
535 |
The result is fully simplified by default, including assumptions and |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
536 |
conclusion; the options @{text no_asm} etc.\ tune the Simplifier in |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
537 |
the same way as the for the @{text simp} method. |
26782 | 538 |
|
539 |
Note that forward simplification restricts the simplifier to its |
|
540 |
most basic operation of term rewriting; solver and looper tactics |
|
541 |
\cite{isabelle-ref} are \emph{not} involved here. The @{text |
|
542 |
simplified} attribute should be only rarely required under normal |
|
543 |
circumstances. |
|
544 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
545 |
\end{description} |
26782 | 546 |
*} |
547 |
||
548 |
||
27040 | 549 |
section {* The Classical Reasoner \label{sec:classical} *} |
26782 | 550 |
|
27040 | 551 |
subsection {* Basic methods *} |
26782 | 552 |
|
553 |
text {* |
|
554 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
555 |
@{method_def rule} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
556 |
@{method_def contradiction} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
557 |
@{method_def intro} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
558 |
@{method_def elim} & : & @{text method} \\ |
26782 | 559 |
\end{matharray} |
560 |
||
561 |
\begin{rail} |
|
562 |
('rule' | 'intro' | 'elim') thmrefs? |
|
563 |
; |
|
564 |
\end{rail} |
|
565 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
566 |
\begin{description} |
26782 | 567 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
568 |
\item @{method rule} as offered by the Classical Reasoner is a |
26782 | 569 |
refinement over the primitive one (see \secref{sec:pure-meth-att}). |
570 |
Both versions essentially work the same, but the classical version |
|
571 |
observes the classical rule context in addition to that of |
|
572 |
Isabelle/Pure. |
|
573 |
||
574 |
Common object logics (HOL, ZF, etc.) declare a rich collection of |
|
575 |
classical rules (even if these would qualify as intuitionistic |
|
576 |
ones), but only few declarations to the rule context of |
|
577 |
Isabelle/Pure (\secref{sec:pure-meth-att}). |
|
578 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
579 |
\item @{method contradiction} solves some goal by contradiction, |
26782 | 580 |
deriving any result from both @{text "\<not> A"} and @{text A}. Chained |
581 |
facts, which are guaranteed to participate, may appear in either |
|
582 |
order. |
|
583 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
584 |
\item @{method intro} and @{method elim} repeatedly refine some goal |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
585 |
by intro- or elim-resolution, after having inserted any chained |
26901 | 586 |
facts. Exactly the rules given as arguments are taken into account; |
587 |
this allows fine-tuned decomposition of a proof problem, in contrast |
|
588 |
to common automated tools. |
|
26782 | 589 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
590 |
\end{description} |
26782 | 591 |
*} |
592 |
||
593 |
||
27040 | 594 |
subsection {* Automated methods *} |
26782 | 595 |
|
596 |
text {* |
|
597 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
598 |
@{method_def blast} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
599 |
@{method_def fast} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
600 |
@{method_def slow} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
601 |
@{method_def best} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
602 |
@{method_def safe} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
603 |
@{method_def clarify} & : & @{text method} \\ |
26782 | 604 |
\end{matharray} |
605 |
||
606 |
\indexouternonterm{clamod} |
|
607 |
\begin{rail} |
|
608 |
'blast' ('!' ?) nat? (clamod *) |
|
609 |
; |
|
610 |
('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *) |
|
611 |
; |
|
612 |
||
613 |
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs |
|
614 |
; |
|
615 |
\end{rail} |
|
616 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
617 |
\begin{description} |
26782 | 618 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
619 |
\item @{method blast} refers to the classical tableau prover (see |
26782 | 620 |
@{ML blast_tac} in \cite[\S11]{isabelle-ref}). The optional |
621 |
argument specifies a user-supplied search bound (default 20). |
|
622 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
623 |
\item @{method fast}, @{method slow}, @{method best}, @{method |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
624 |
safe}, and @{method clarify} refer to the generic classical |
26782 | 625 |
reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML |
626 |
safe_tac}, and @{ML clarify_tac} in \cite[\S11]{isabelle-ref} for |
|
627 |
more information. |
|
628 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
629 |
\end{description} |
26782 | 630 |
|
631 |
Any of the above methods support additional modifiers of the context |
|
632 |
of classical rules. Their semantics is analogous to the attributes |
|
633 |
given before. Facts provided by forward chaining are inserted into |
|
634 |
the goal before commencing proof search. The ``@{text |
|
635 |
"!"}''~argument causes the full context of assumptions to be |
|
636 |
included as well. |
|
637 |
*} |
|
638 |
||
639 |
||
27040 | 640 |
subsection {* Combined automated methods \label{sec:clasimp} *} |
26782 | 641 |
|
642 |
text {* |
|
643 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
644 |
@{method_def auto} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
645 |
@{method_def force} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
646 |
@{method_def clarsimp} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
647 |
@{method_def fastsimp} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
648 |
@{method_def slowsimp} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
649 |
@{method_def bestsimp} & : & @{text method} \\ |
26782 | 650 |
\end{matharray} |
651 |
||
652 |
\indexouternonterm{clasimpmod} |
|
653 |
\begin{rail} |
|
654 |
'auto' '!'? (nat nat)? (clasimpmod *) |
|
655 |
; |
|
656 |
('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *) |
|
657 |
; |
|
658 |
||
659 |
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | |
|
660 |
('cong' | 'split') (() | 'add' | 'del') | |
|
661 |
'iff' (((() | 'add') '?'?) | 'del') | |
|
662 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs |
|
663 |
\end{rail} |
|
664 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
665 |
\begin{description} |
26782 | 666 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
667 |
\item @{method auto}, @{method force}, @{method clarsimp}, @{method |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
668 |
fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
669 |
to Isabelle's combined simplification and classical reasoning |
26782 | 670 |
tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML |
671 |
clarsimp_tac}, and Classical Reasoner tactics with the Simplifier |
|
672 |
added as wrapper, see \cite[\S11]{isabelle-ref} for more |
|
673 |
information. The modifier arguments correspond to those given in |
|
674 |
\secref{sec:simplifier} and \secref{sec:classical}. Just note that |
|
675 |
the ones related to the Simplifier are prefixed by \railtterm{simp} |
|
676 |
here. |
|
677 |
||
678 |
Facts provided by forward chaining are inserted into the goal before |
|
679 |
doing the search. The ``@{text "!"}'' argument causes the full |
|
680 |
context of assumptions to be included as well. |
|
681 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
682 |
\end{description} |
26782 | 683 |
*} |
684 |
||
685 |
||
27040 | 686 |
subsection {* Declaring rules *} |
26782 | 687 |
|
688 |
text {* |
|
689 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
690 |
@{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
691 |
@{attribute_def intro} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
692 |
@{attribute_def elim} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
693 |
@{attribute_def dest} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
694 |
@{attribute_def rule} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
695 |
@{attribute_def iff} & : & @{text attribute} \\ |
26782 | 696 |
\end{matharray} |
697 |
||
698 |
\begin{rail} |
|
699 |
('intro' | 'elim' | 'dest') ('!' | () | '?') nat? |
|
700 |
; |
|
701 |
'rule' 'del' |
|
702 |
; |
|
703 |
'iff' (((() | 'add') '?'?) | 'del') |
|
704 |
; |
|
705 |
\end{rail} |
|
706 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
707 |
\begin{description} |
26782 | 708 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
709 |
\item @{command "print_claset"} prints the collection of rules |
26782 | 710 |
declared to the Classical Reasoner, which is also known as |
711 |
``claset'' internally \cite{isabelle-ref}. |
|
712 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
713 |
\item @{attribute intro}, @{attribute elim}, and @{attribute dest} |
26782 | 714 |
declare introduction, elimination, and destruction rules, |
715 |
respectively. By default, rules are considered as \emph{unsafe} |
|
716 |
(i.e.\ not applied blindly without backtracking), while ``@{text |
|
717 |
"!"}'' classifies as \emph{safe}. Rule declarations marked by |
|
718 |
``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\ |
|
719 |
\secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
|
720 |
of the @{method rule} method). The optional natural number |
|
721 |
specifies an explicit weight argument, which is ignored by automated |
|
722 |
tools, but determines the search order of single rule steps. |
|
723 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
724 |
\item @{attribute rule}~@{text del} deletes introduction, |
26782 | 725 |
elimination, or destruction rules from the context. |
726 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
727 |
\item @{attribute iff} declares logical equivalences to the |
26782 | 728 |
Simplifier and the Classical reasoner at the same time. |
729 |
Non-conditional rules result in a ``safe'' introduction and |
|
730 |
elimination pair; conditional ones are considered ``unsafe''. Rules |
|
731 |
with negative conclusion are automatically inverted (using @{text |
|
26789 | 732 |
"\<not>"}-elimination internally). |
26782 | 733 |
|
734 |
The ``@{text "?"}'' version of @{attribute iff} declares rules to |
|
735 |
the Isabelle/Pure context only, and omits the Simplifier |
|
736 |
declaration. |
|
737 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
738 |
\end{description} |
26782 | 739 |
*} |
740 |
||
741 |
||
27040 | 742 |
subsection {* Classical operations *} |
26782 | 743 |
|
744 |
text {* |
|
745 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
746 |
@{attribute_def swapped} & : & @{text attribute} \\ |
26782 | 747 |
\end{matharray} |
748 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
749 |
\begin{description} |
26782 | 750 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
751 |
\item @{attribute swapped} turns an introduction rule into an |
26782 | 752 |
elimination, by resolving with the classical swap principle @{text |
753 |
"(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}. |
|
754 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
755 |
\end{description} |
26782 | 756 |
*} |
757 |
||
758 |
||
27044 | 759 |
section {* Object-logic setup \label{sec:object-logic} *} |
26790 | 760 |
|
761 |
text {* |
|
762 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
763 |
@{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
764 |
@{method_def atomize} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
765 |
@{attribute_def atomize} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
766 |
@{attribute_def rule_format} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
767 |
@{attribute_def rulify} & : & @{text attribute} \\ |
26790 | 768 |
\end{matharray} |
769 |
||
770 |
The very starting point for any Isabelle object-logic is a ``truth |
|
771 |
judgment'' that links object-level statements to the meta-logic |
|
772 |
(with its minimal language of @{text prop} that covers universal |
|
773 |
quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}). |
|
774 |
||
775 |
Common object-logics are sufficiently expressive to internalize rule |
|
776 |
statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own |
|
777 |
language. This is useful in certain situations where a rule needs |
|
778 |
to be viewed as an atomic statement from the meta-level perspective, |
|
779 |
e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}. |
|
780 |
||
781 |
From the following language elements, only the @{method atomize} |
|
782 |
method and @{attribute rule_format} attribute are occasionally |
|
783 |
required by end-users, the rest is for those who need to setup their |
|
784 |
own object-logic. In the latter case existing formulations of |
|
785 |
Isabelle/FOL or Isabelle/HOL may be taken as realistic examples. |
|
786 |
||
787 |
Generic tools may refer to the information provided by object-logic |
|
788 |
declarations internally. |
|
789 |
||
790 |
\begin{rail} |
|
791 |
'judgment' constdecl |
|
792 |
; |
|
793 |
'atomize' ('(' 'full' ')')? |
|
794 |
; |
|
795 |
'rule\_format' ('(' 'noasm' ')')? |
|
796 |
; |
|
797 |
\end{rail} |
|
798 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
799 |
\begin{description} |
26790 | 800 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
801 |
\item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
802 |
@{text c} as the truth judgment of the current object-logic. Its |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
803 |
type @{text \<sigma>} should specify a coercion of the category of |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
804 |
object-level propositions to @{text prop} of the Pure meta-logic; |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
805 |
the mixfix annotation @{text "(mx)"} would typically just link the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
806 |
object language (internally of syntactic category @{text logic}) |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
807 |
with that of @{text prop}. Only one @{command "judgment"} |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
808 |
declaration may be given in any theory development. |
26790 | 809 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
810 |
\item @{method atomize} (as a method) rewrites any non-atomic |
26790 | 811 |
premises of a sub-goal, using the meta-level equations declared via |
812 |
@{attribute atomize} (as an attribute) beforehand. As a result, |
|
813 |
heavily nested goals become amenable to fundamental operations such |
|
814 |
as resolution (cf.\ the @{method rule} method). Giving the ``@{text |
|
815 |
"(full)"}'' option here means to turn the whole subgoal into an |
|
816 |
object-statement (if possible), including the outermost parameters |
|
817 |
and assumptions as well. |
|
818 |
||
819 |
A typical collection of @{attribute atomize} rules for a particular |
|
820 |
object-logic would provide an internalization for each of the |
|
821 |
connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}. |
|
822 |
Meta-level conjunction should be covered as well (this is |
|
823 |
particularly important for locales, see \secref{sec:locale}). |
|
824 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
825 |
\item @{attribute rule_format} rewrites a theorem by the equalities |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
826 |
declared as @{attribute rulify} rules in the current object-logic. |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
827 |
By default, the result is fully normalized, including assumptions |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
828 |
and conclusions at any depth. The @{text "(no_asm)"} option |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
829 |
restricts the transformation to the conclusion of a rule. |
26790 | 830 |
|
831 |
In common object-logics (HOL, FOL, ZF), the effect of @{attribute |
|
832 |
rule_format} is to replace (bounded) universal quantification |
|
833 |
(@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding |
|
834 |
rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}. |
|
835 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
836 |
\end{description} |
26790 | 837 |
*} |
838 |
||
26782 | 839 |
end |