author | nipkow |
Tue, 13 Sep 2011 07:13:49 +0200 | |
changeset 44911 | 884d27ede438 |
parent 44094 | f7bbfdf4b4a7 |
child 45645 | 4014bc2a09ff |
permissions | -rw-r--r-- |
26782 | 1 |
theory Generic |
42651 | 2 |
imports Base Main |
26782 | 3 |
begin |
4 |
||
5 |
chapter {* Generic tools and packages \label{ch:gen-tools} *} |
|
6 |
||
42655 | 7 |
section {* Configuration options \label{sec:config} *} |
26782 | 8 |
|
40291 | 9 |
text {* Isabelle/Pure maintains a record of named configuration |
10 |
options within the theory or proof context, with values of type |
|
11 |
@{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type |
|
12 |
string}. Tools may declare options in ML, and then refer to these |
|
13 |
values (relative to the context). Thus global reference variables |
|
14 |
are easily avoided. The user may change the value of a |
|
15 |
configuration option by means of an associated attribute of the same |
|
16 |
name. This form of context declaration works particularly well with |
|
42655 | 17 |
commands such as @{command "declare"} or @{command "using"} like |
18 |
this: |
|
19 |
*} |
|
20 |
||
21 |
declare [[show_main_goal = false]] |
|
26782 | 22 |
|
42655 | 23 |
notepad |
24 |
begin |
|
25 |
note [[show_main_goal = true]] |
|
26 |
end |
|
27 |
||
28 |
text {* For historical reasons, some tools cannot take the full proof |
|
26782 | 29 |
context into account and merely refer to the background theory. |
30 |
This is accommodated by configuration options being declared as |
|
31 |
``global'', which may not be changed within a local context. |
|
32 |
||
33 |
\begin{matharray}{rcll} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
34 |
@{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\ |
26782 | 35 |
\end{matharray} |
36 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
37 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
38 |
@{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))? |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
39 |
"} |
26782 | 40 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
41 |
\begin{description} |
26782 | 42 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
43 |
\item @{command "print_configs"} prints the available configuration |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
44 |
options, with names, types, and current values. |
26782 | 45 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
46 |
\item @{text "name = value"} as an attribute expression modifies the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
attempt to change a global option in a local context is ignored. |
26782 | 50 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
51 |
\end{description} |
26782 | 52 |
*} |
53 |
||
54 |
||
27040 | 55 |
section {* Basic proof tools *} |
26782 | 56 |
|
57 |
subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *} |
|
58 |
||
59 |
text {* |
|
60 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
61 |
@{method_def unfold} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
62 |
@{method_def fold} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
63 |
@{method_def insert} & : & @{text method} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
64 |
@{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
65 |
@{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
66 |
@{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\ |
43365 | 67 |
@{method_def intro} & : & @{text method} \\ |
68 |
@{method_def elim} & : & @{text method} \\ |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
69 |
@{method_def succeed} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
70 |
@{method_def fail} & : & @{text method} \\ |
26782 | 71 |
\end{matharray} |
72 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
73 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
74 |
(@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs} |
26782 | 75 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
76 |
(@@{method erule} | @@{method drule} | @@{method frule}) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
77 |
('(' @{syntax nat} ')')? @{syntax thmrefs} |
43365 | 78 |
; |
79 |
(@@{method intro} | @@{method elim}) @{syntax thmrefs}? |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
80 |
"} |
26782 | 81 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
82 |
\begin{description} |
26782 | 83 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
84 |
\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
|
85 |
"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
|
86 |
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
|
87 |
subject to rewriting as well. |
26782 | 88 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
89 |
\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
|
90 |
into all goals of the proof state. Note that current facts |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
91 |
indicated for forward chaining are ignored. |
26782 | 92 |
|
30397 | 93 |
\item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method |
94 |
drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text |
|
95 |
"a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule} |
|
96 |
method (see \secref{sec:pure-meth-att}), but apply rules by |
|
97 |
elim-resolution, destruct-resolution, and forward-resolution, |
|
98 |
respectively \cite{isabelle-implementation}. The optional natural |
|
99 |
number argument (default 0) specifies additional assumption steps to |
|
100 |
be performed here. |
|
26782 | 101 |
|
102 |
Note that these methods are improper ones, mainly serving for |
|
103 |
experimentation and tactic script emulation. Different modes of |
|
104 |
basic rule application are usually expressed in Isar at the proof |
|
105 |
language level, rather than via implicit proof state manipulations. |
|
106 |
For example, a proper single-step elimination would be done using |
|
107 |
the plain @{method rule} method, with forward chaining of current |
|
108 |
facts. |
|
109 |
||
43365 | 110 |
\item @{method intro} and @{method elim} repeatedly refine some goal |
111 |
by intro- or elim-resolution, after having inserted any chained |
|
112 |
facts. Exactly the rules given as arguments are taken into account; |
|
113 |
this allows fine-tuned decomposition of a proof problem, in contrast |
|
114 |
to common automated tools. |
|
115 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
116 |
\item @{method succeed} yields a single (unchanged) result; it is |
26782 | 117 |
the identity of the ``@{text ","}'' method combinator (cf.\ |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27248
diff
changeset
|
118 |
\secref{sec:proof-meth}). |
26782 | 119 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
120 |
\item @{method fail} yields an empty result sequence; it is the |
26782 | 121 |
identity of the ``@{text "|"}'' method combinator (cf.\ |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27248
diff
changeset
|
122 |
\secref{sec:proof-meth}). |
26782 | 123 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
124 |
\end{description} |
26782 | 125 |
|
126 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
127 |
@{attribute_def tagged} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
128 |
@{attribute_def untagged} & : & @{text attribute} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
129 |
@{attribute_def THEN} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
130 |
@{attribute_def COMP} & : & @{text attribute} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
131 |
@{attribute_def unfolded} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
132 |
@{attribute_def folded} & : & @{text attribute} \\[0.5ex] |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
133 |
@{attribute_def rotated} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
134 |
@{attribute_def (Pure) elim_format} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
135 |
@{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
136 |
@{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\ |
26782 | 137 |
\end{matharray} |
138 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
139 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
140 |
@@{attribute tagged} @{syntax name} @{syntax name} |
26782 | 141 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
142 |
@@{attribute untagged} @{syntax name} |
26782 | 143 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
144 |
(@@{attribute THEN} | @@{attribute COMP}) ('[' @{syntax nat} ']')? @{syntax thmref} |
26782 | 145 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
146 |
(@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs} |
26782 | 147 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
148 |
@@{attribute rotated} @{syntax int}? |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
149 |
"} |
26782 | 150 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
151 |
\begin{description} |
26782 | 152 |
|
28764 | 153 |
\item @{attribute tagged}~@{text "name value"} and @{attribute |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
154 |
untagged}~@{text name} add and remove \emph{tags} of some theorem. |
26782 | 155 |
Tags may be any list of string pairs that serve as formal comment. |
28764 | 156 |
The first string is considered the tag name, the second its value. |
157 |
Note that @{attribute untagged} removes any tags of the same name. |
|
26782 | 158 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
159 |
\item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a} |
26782 | 160 |
compose rules by resolution. @{attribute THEN} resolves with the |
161 |
first premise of @{text a} (an alternative position may be also |
|
162 |
specified); the @{attribute COMP} version skips the automatic |
|
30462 | 163 |
lifting process that is normally intended (cf.\ @{ML "op RS"} and |
164 |
@{ML "op COMP"} in \cite{isabelle-implementation}). |
|
26782 | 165 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
166 |
\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
|
167 |
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
|
168 |
definitions throughout a rule. |
26782 | 169 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
170 |
\item @{attribute rotated}~@{text n} rotate the premises of a |
26782 | 171 |
theorem by @{text n} (default 1). |
172 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
173 |
\item @{attribute (Pure) elim_format} turns a destruction rule into |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
174 |
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
|
175 |
(PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}. |
26782 | 176 |
|
177 |
Note that the Classical Reasoner (\secref{sec:classical}) provides |
|
178 |
its own version of this operation. |
|
179 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
180 |
\item @{attribute standard} puts a theorem into the standard form of |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
181 |
object-rules at the outermost theory level. Note that this |
26782 | 182 |
operation violates the local proof context (including active |
183 |
locales). |
|
184 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
185 |
\item @{attribute no_vars} replaces schematic variables by free |
26782 | 186 |
ones; this is mainly for tuning output of pretty printed theorems. |
187 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
188 |
\end{description} |
26782 | 189 |
*} |
190 |
||
191 |
||
27044 | 192 |
subsection {* Low-level equational reasoning *} |
193 |
||
194 |
text {* |
|
195 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
196 |
@{method_def subst} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
197 |
@{method_def hypsubst} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
198 |
@{method_def split} & : & @{text method} \\ |
27044 | 199 |
\end{matharray} |
200 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
201 |
@{rail " |
42704 | 202 |
@@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} |
27044 | 203 |
; |
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset
|
204 |
@@{method split} @{syntax thmrefs} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
205 |
"} |
27044 | 206 |
|
207 |
These methods provide low-level facilities for equational reasoning |
|
208 |
that are intended for specialized applications only. Normally, |
|
209 |
single step calculations would be performed in a structured text |
|
210 |
(see also \secref{sec:calculation}), while the Simplifier methods |
|
211 |
provide the canonical way for automated normalization (see |
|
212 |
\secref{sec:simplifier}). |
|
213 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
214 |
\begin{description} |
27044 | 215 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
216 |
\item @{method subst}~@{text eq} performs a single substitution step |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
217 |
using rule @{text eq}, which may be either a meta or object |
27044 | 218 |
equality. |
219 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
220 |
\item @{method subst}~@{text "(asm) eq"} substitutes in an |
27044 | 221 |
assumption. |
222 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
223 |
\item @{method subst}~@{text "(i \<dots> j) eq"} performs several |
27044 | 224 |
substitutions in the conclusion. The numbers @{text i} to @{text j} |
225 |
indicate the positions to substitute at. Positions are ordered from |
|
226 |
the top of the term tree moving down from left to right. For |
|
227 |
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
|
228 |
where commutativity of @{text "+"} is applicable: 1 refers to @{text |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
229 |
"a + b"}, 2 to the whole term, and 3 to @{text "c + d"}. |
27044 | 230 |
|
231 |
If the positions in the list @{text "(i \<dots> j)"} are non-overlapping |
|
232 |
(e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may |
|
233 |
assume all substitutions are performed simultaneously. Otherwise |
|
234 |
the behaviour of @{text subst} is not specified. |
|
235 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
236 |
\item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the |
27071 | 237 |
substitutions in the assumptions. The positions refer to the |
238 |
assumptions in order from left to right. For example, given in a |
|
239 |
goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of |
|
240 |
commutativity of @{text "+"} is the subterm @{text "a + b"} and |
|
241 |
position 2 is the subterm @{text "c + d"}. |
|
27044 | 242 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
243 |
\item @{method hypsubst} performs substitution using some |
27044 | 244 |
assumption; this only works for equations of the form @{text "x = |
245 |
t"} where @{text x} is a free or bound variable. |
|
246 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
247 |
\item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case |
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset
|
248 |
splitting using the given rules. Splitting is performed in the |
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset
|
249 |
conclusion or some assumption of the subgoal, depending of the |
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset
|
250 |
structure of the rule. |
27044 | 251 |
|
252 |
Note that the @{method simp} method already involves repeated |
|
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset
|
253 |
application of split rules as declared in the current context, using |
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset
|
254 |
@{attribute split}, for example. |
27044 | 255 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
256 |
\end{description} |
27044 | 257 |
*} |
258 |
||
259 |
||
26782 | 260 |
subsection {* Further tactic emulations \label{sec:tactics} *} |
261 |
||
262 |
text {* |
|
263 |
The following improper proof methods emulate traditional tactics. |
|
264 |
These admit direct access to the goal state, which is normally |
|
265 |
considered harmful! In particular, this may involve both numbered |
|
266 |
goal addressing (default 1), and dynamic instantiation within the |
|
267 |
scope of some subgoal. |
|
268 |
||
269 |
\begin{warn} |
|
270 |
Dynamic instantiations refer to universally quantified parameters |
|
271 |
of a subgoal (the dynamic context) rather than fixed variables and |
|
272 |
term abbreviations of a (static) Isar context. |
|
273 |
\end{warn} |
|
274 |
||
275 |
Tactic emulation methods, unlike their ML counterparts, admit |
|
276 |
simultaneous instantiation from both dynamic and static contexts. |
|
277 |
If names occur in both contexts goal parameters hide locally fixed |
|
278 |
variables. Likewise, schematic variables refer to term |
|
279 |
abbreviations, if present in the static context. Otherwise the |
|
280 |
schematic variable is interpreted as a schematic variable and left |
|
281 |
to be solved by unification with certain parts of the subgoal. |
|
282 |
||
283 |
Note that the tactic emulation proof methods in Isabelle/Isar are |
|
284 |
consistently named @{text foo_tac}. Note also that variable names |
|
285 |
occurring on left hand sides of instantiations must be preceded by a |
|
286 |
question mark if they coincide with a keyword or contain dots. This |
|
287 |
is consistent with the attribute @{attribute "where"} (see |
|
288 |
\secref{sec:pure-meth-att}). |
|
289 |
||
290 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
291 |
@{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
|
292 |
@{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
|
293 |
@{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
|
294 |
@{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
|
295 |
@{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
|
296 |
@{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
|
297 |
@{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
|
298 |
@{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
|
299 |
@{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
|
300 |
@{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
301 |
@{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
26782 | 302 |
\end{matharray} |
303 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
304 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
305 |
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | |
42705 | 306 |
@@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\ |
42617 | 307 |
( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} ) |
26782 | 308 |
; |
42705 | 309 |
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
310 |
; |
42705 | 311 |
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +) |
26782 | 312 |
; |
42705 | 313 |
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}? |
26782 | 314 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
315 |
(@@{method tactic} | @@{method raw_tactic}) @{syntax text} |
26782 | 316 |
; |
317 |
||
42617 | 318 |
dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') |
319 |
"} |
|
26782 | 320 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
321 |
\begin{description} |
26782 | 322 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
323 |
\item @{method rule_tac} etc. do resolution of rules with explicit |
26782 | 324 |
instantiation. This works the same way as the ML tactics @{ML |
30397 | 325 |
res_inst_tac} etc. (see \cite{isabelle-implementation}) |
26782 | 326 |
|
327 |
Multiple rules may be only given if there is no instantiation; then |
|
328 |
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see |
|
30397 | 329 |
\cite{isabelle-implementation}). |
26782 | 330 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
331 |
\item @{method cut_tac} inserts facts into the proof state as |
27209 | 332 |
assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in |
30397 | 333 |
\cite{isabelle-implementation}. Note that the scope of schematic |
26782 | 334 |
variables is spread over the main goal statement. Instantiations |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
335 |
may be given as well, see also ML tactic @{ML cut_inst_tac} in |
30397 | 336 |
\cite{isabelle-implementation}. |
26782 | 337 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
338 |
\item @{method thin_tac}~@{text \<phi>} deletes the specified assumption |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
339 |
from a subgoal; note that @{text \<phi>} may contain schematic variables. |
30397 | 340 |
See also @{ML thin_tac} in \cite{isabelle-implementation}. |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
341 |
|
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
342 |
\item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an |
27239 | 343 |
assumption to a subgoal. See also @{ML subgoal_tac} and @{ML |
30397 | 344 |
subgoals_tac} in \cite{isabelle-implementation}. |
26782 | 345 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
346 |
\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
|
347 |
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
|
348 |
\emph{suffix} of variables. |
26782 | 349 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
350 |
\item @{method rotate_tac}~@{text n} rotates the assumptions of a |
26782 | 351 |
goal by @{text n} positions: from right to left if @{text n} is |
352 |
positive, and from left to right if @{text n} is negative; the |
|
353 |
default value is 1. See also @{ML rotate_tac} in |
|
30397 | 354 |
\cite{isabelle-implementation}. |
26782 | 355 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
356 |
\item @{method tactic}~@{text "text"} produces a proof method from |
26782 | 357 |
any ML text of type @{ML_type tactic}. Apart from the usual ML |
27223 | 358 |
environment and the current proof context, the ML code may refer to |
359 |
the locally bound values @{ML_text facts}, which indicates any |
|
360 |
current facts used for forward-chaining. |
|
26782 | 361 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
362 |
\item @{method raw_tactic} is similar to @{method tactic}, but |
27223 | 363 |
presents the goal state in its raw internal form, where simultaneous |
364 |
subgoals appear as conjunction of the logical framework instead of |
|
365 |
the usual split into several subgoals. While feature this is useful |
|
366 |
for debugging of complex method definitions, it should not never |
|
367 |
appear in production theories. |
|
26782 | 368 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
369 |
\end{description} |
26782 | 370 |
*} |
371 |
||
372 |
||
27040 | 373 |
section {* The Simplifier \label{sec:simplifier} *} |
26782 | 374 |
|
27040 | 375 |
subsection {* Simplification methods *} |
26782 | 376 |
|
377 |
text {* |
|
378 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
379 |
@{method_def simp} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
380 |
@{method_def simp_all} & : & @{text method} \\ |
26782 | 381 |
\end{matharray} |
382 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
383 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
384 |
(@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * ) |
26782 | 385 |
; |
386 |
||
40255
9ffbc25e1606
eliminated obsolete \_ escapes in rail environments;
wenzelm
parents:
35613
diff
changeset
|
387 |
opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')' |
26782 | 388 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
389 |
@{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
390 |
'split' (() | 'add' | 'del')) ':' @{syntax thmrefs} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
391 |
"} |
26782 | 392 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
393 |
\begin{description} |
26782 | 394 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
395 |
\item @{method simp} invokes the Simplifier, after declaring |
26782 | 396 |
additional rules according to the arguments given. Note that the |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
397 |
@{text only} modifier first removes all other rewrite rules, |
26782 | 398 |
congruences, and looper tactics (including splits), and then behaves |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
399 |
like @{text add}. |
26782 | 400 |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
401 |
\medskip The @{text cong} modifiers add or delete Simplifier |
26782 | 402 |
congruence rules (see also \cite{isabelle-ref}), the default is to |
403 |
add. |
|
404 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
405 |
\medskip The @{text split} modifiers add or delete rules for the |
26782 | 406 |
Splitter (see also \cite{isabelle-ref}), the default is to add. |
407 |
This works only if the Simplifier method has been properly setup to |
|
408 |
include the Splitter (all major object logics such HOL, HOLCF, FOL, |
|
409 |
ZF do this already). |
|
410 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
411 |
\item @{method simp_all} is similar to @{method simp}, but acts on |
26782 | 412 |
all goals (backwards from the last to the first one). |
413 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
414 |
\end{description} |
26782 | 415 |
|
416 |
By default the Simplifier methods take local assumptions fully into |
|
417 |
account, using equational assumptions in the subsequent |
|
418 |
normalization process, or simplifying assumptions themselves (cf.\ |
|
30397 | 419 |
@{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured |
420 |
proofs this is usually quite well behaved in practice: just the |
|
421 |
local premises of the actual goal are involved, additional facts may |
|
422 |
be inserted via explicit forward-chaining (via @{command "then"}, |
|
35613 | 423 |
@{command "from"}, @{command "using"} etc.). |
26782 | 424 |
|
425 |
Additional Simplifier options may be specified to tune the behavior |
|
426 |
further (mostly for unstructured scripts with many accidental local |
|
427 |
facts): ``@{text "(no_asm)"}'' means assumptions are ignored |
|
428 |
completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means |
|
429 |
assumptions are used in the simplification of the conclusion but are |
|
430 |
not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text |
|
431 |
"(no_asm_use)"}'' means assumptions are simplified but are not used |
|
432 |
in the simplification of each other or the conclusion (cf.\ @{ML |
|
433 |
full_simp_tac}). For compatibility reasons, there is also an option |
|
434 |
``@{text "(asm_lr)"}'', which means that an assumption is only used |
|
435 |
for simplifying assumptions which are to the right of it (cf.\ @{ML |
|
436 |
asm_lr_simp_tac}). |
|
437 |
||
27092 | 438 |
The configuration option @{text "depth_limit"} limits the number of |
26782 | 439 |
recursive invocations of the simplifier during conditional |
440 |
rewriting. |
|
441 |
||
442 |
\medskip The Splitter package is usually configured to work as part |
|
443 |
of the Simplifier. The effect of repeatedly applying @{ML |
|
444 |
split_tac} can be simulated by ``@{text "(simp only: split: |
|
445 |
a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split} |
|
446 |
method available for single-step case splitting. |
|
447 |
*} |
|
448 |
||
449 |
||
27040 | 450 |
subsection {* Declaring rules *} |
26782 | 451 |
|
452 |
text {* |
|
453 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
454 |
@{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
|
455 |
@{attribute_def simp} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
456 |
@{attribute_def cong} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
457 |
@{attribute_def split} & : & @{text attribute} \\ |
26782 | 458 |
\end{matharray} |
459 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
460 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
461 |
(@@{attribute simp} | @@{attribute cong} | @@{attribute split}) (() | 'add' | 'del') |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
462 |
"} |
26782 | 463 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
464 |
\begin{description} |
26782 | 465 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
466 |
\item @{command "print_simpset"} prints the collection of rules |
26782 | 467 |
declared to the Simplifier, which is also known as ``simpset'' |
468 |
internally \cite{isabelle-ref}. |
|
469 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
470 |
\item @{attribute simp} declares simplification rules. |
26782 | 471 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
472 |
\item @{attribute cong} declares congruence rules. |
26782 | 473 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
474 |
\item @{attribute split} declares case split rules. |
26782 | 475 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
476 |
\end{description} |
26782 | 477 |
*} |
478 |
||
479 |
||
27040 | 480 |
subsection {* Simplification procedures *} |
26782 | 481 |
|
42925 | 482 |
text {* Simplification procedures are ML functions that produce proven |
483 |
rewrite rules on demand. They are associated with higher-order |
|
484 |
patterns that approximate the left-hand sides of equations. The |
|
485 |
Simplifier first matches the current redex against one of the LHS |
|
486 |
patterns; if this succeeds, the corresponding ML function is |
|
487 |
invoked, passing the Simplifier context and redex term. Thus rules |
|
488 |
may be specifically fashioned for particular situations, resulting |
|
489 |
in a more powerful mechanism than term rewriting by a fixed set of |
|
490 |
rules. |
|
491 |
||
492 |
Any successful result needs to be a (possibly conditional) rewrite |
|
493 |
rule @{text "t \<equiv> u"} that is applicable to the current redex. The |
|
494 |
rule will be applied just as any ordinary rewrite rule. It is |
|
495 |
expected to be already in \emph{internal form}, bypassing the |
|
496 |
automatic preprocessing of object-level equivalences. |
|
497 |
||
26782 | 498 |
\begin{matharray}{rcl} |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
499 |
@{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
|
500 |
simproc & : & @{text attribute} \\ |
26782 | 501 |
\end{matharray} |
502 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
503 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
504 |
@@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '=' |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
505 |
@{syntax text} \\ (@'identifier' (@{syntax nameref}+))? |
26782 | 506 |
; |
507 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
508 |
@@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
509 |
"} |
26782 | 510 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
511 |
\begin{description} |
26782 | 512 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
513 |
\item @{command "simproc_setup"} defines a named simplification |
26782 | 514 |
procedure that is invoked by the Simplifier whenever any of the |
515 |
given term patterns match the current redex. The implementation, |
|
516 |
which is provided as ML source text, needs to be of type @{ML_type |
|
517 |
"morphism -> simpset -> cterm -> thm option"}, where the @{ML_type |
|
518 |
cterm} represents the current redex @{text r} and the result is |
|
519 |
supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a |
|
520 |
generalized version), or @{ML NONE} to indicate failure. The |
|
521 |
@{ML_type simpset} argument holds the full context of the current |
|
522 |
Simplifier invocation, including the actual Isar proof context. The |
|
523 |
@{ML_type morphism} informs about the difference of the original |
|
524 |
compilation context wrt.\ the one of the actual application later |
|
525 |
on. The optional @{keyword "identifier"} specifies theorems that |
|
526 |
represent the logical content of the abstract theory of this |
|
527 |
simproc. |
|
528 |
||
529 |
Morphisms and identifiers are only relevant for simprocs that are |
|
530 |
defined within a local target context, e.g.\ in a locale. |
|
531 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
532 |
\item @{text "simproc add: name"} and @{text "simproc del: name"} |
26782 | 533 |
add or delete named simprocs to the current Simplifier context. The |
534 |
default is to add a simproc. Note that @{command "simproc_setup"} |
|
535 |
already adds the new simproc to the subsequent context. |
|
536 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
537 |
\end{description} |
26782 | 538 |
*} |
539 |
||
540 |
||
42925 | 541 |
subsubsection {* Example *} |
542 |
||
543 |
text {* The following simplification procedure for @{thm |
|
544 |
[source=false, show_types] unit_eq} in HOL performs fine-grained |
|
545 |
control over rule application, beyond higher-order pattern matching. |
|
546 |
Declaring @{thm unit_eq} as @{attribute simp} directly would make |
|
547 |
the simplifier loop! Note that a version of this simplification |
|
548 |
procedure is already active in Isabelle/HOL. *} |
|
549 |
||
550 |
simproc_setup unit ("x::unit") = {* |
|
551 |
fn _ => fn _ => fn ct => |
|
552 |
if HOLogic.is_unit (term_of ct) then NONE |
|
553 |
else SOME (mk_meta_eq @{thm unit_eq}) |
|
554 |
*} |
|
555 |
||
556 |
text {* Since the Simplifier applies simplification procedures |
|
557 |
frequently, it is important to make the failure check in ML |
|
558 |
reasonably fast. *} |
|
559 |
||
560 |
||
27040 | 561 |
subsection {* Forward simplification *} |
26782 | 562 |
|
563 |
text {* |
|
564 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
565 |
@{attribute_def simplified} & : & @{text attribute} \\ |
26782 | 566 |
\end{matharray} |
567 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
568 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
569 |
@@{attribute simplified} opt? @{syntax thmrefs}? |
26782 | 570 |
; |
571 |
||
40255
9ffbc25e1606
eliminated obsolete \_ escapes in rail environments;
wenzelm
parents:
35613
diff
changeset
|
572 |
opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')' |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
573 |
"} |
26782 | 574 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
575 |
\begin{description} |
26782 | 576 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
577 |
\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
|
578 |
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
|
579 |
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
|
580 |
The result is fully simplified by default, including assumptions and |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
581 |
conclusion; the options @{text no_asm} etc.\ tune the Simplifier in |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
582 |
the same way as the for the @{text simp} method. |
26782 | 583 |
|
584 |
Note that forward simplification restricts the simplifier to its |
|
585 |
most basic operation of term rewriting; solver and looper tactics |
|
586 |
\cite{isabelle-ref} are \emph{not} involved here. The @{text |
|
587 |
simplified} attribute should be only rarely required under normal |
|
588 |
circumstances. |
|
589 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
590 |
\end{description} |
26782 | 591 |
*} |
592 |
||
593 |
||
27040 | 594 |
section {* The Classical Reasoner \label{sec:classical} *} |
26782 | 595 |
|
42930 | 596 |
subsection {* Basic concepts *} |
42927
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
597 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
598 |
text {* Although Isabelle is generic, many users will be working in |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
599 |
some extension of classical first-order logic. Isabelle/ZF is built |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
600 |
upon theory FOL, while Isabelle/HOL conceptually contains |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
601 |
first-order logic as a fragment. Theorem-proving in predicate logic |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
602 |
is undecidable, but many automated strategies have been developed to |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
603 |
assist in this task. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
604 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
605 |
Isabelle's classical reasoner is a generic package that accepts |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
606 |
certain information about a logic and delivers a suite of automatic |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
607 |
proof tools, based on rules that are classified and declared in the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
608 |
context. These proof procedures are slow and simplistic compared |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
609 |
with high-end automated theorem provers, but they can save |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
610 |
considerable time and effort in practice. They can prove theorems |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
611 |
such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
612 |
milliseconds (including full proof reconstruction): *} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
613 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
614 |
lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)" |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
615 |
by blast |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
616 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
617 |
lemma "(\<forall>z. \<exists>y. \<forall>x. f x y \<longleftrightarrow> f x z \<and> \<not> f x x) \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)" |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
618 |
by blast |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
619 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
620 |
text {* The proof tools are generic. They are not restricted to |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
621 |
first-order logic, and have been heavily used in the development of |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
622 |
the Isabelle/HOL library and applications. The tactics can be |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
623 |
traced, and their components can be called directly; in this manner, |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
624 |
any proof can be viewed interactively. *} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
625 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
626 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
627 |
subsubsection {* The sequent calculus *} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
628 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
629 |
text {* Isabelle supports natural deduction, which is easy to use for |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
630 |
interactive proof. But natural deduction does not easily lend |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
631 |
itself to automation, and has a bias towards intuitionism. For |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
632 |
certain proofs in classical logic, it can not be called natural. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
633 |
The \emph{sequent calculus}, a generalization of natural deduction, |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
634 |
is easier to automate. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
635 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
636 |
A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
637 |
and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
638 |
logic, sequents can equivalently be made from lists or multisets of |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
639 |
formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
640 |
\textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or> |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
641 |
Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
642 |
is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
643 |
sequent is \textbf{basic} if its left and right sides have a common |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
644 |
formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
645 |
valid. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
646 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
647 |
Sequent rules are classified as \textbf{right} or \textbf{left}, |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
648 |
indicating which side of the @{text "\<turnstile>"} symbol they operate on. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
649 |
Rules that operate on the right side are analogous to natural |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
650 |
deduction's introduction rules, and left rules are analogous to |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
651 |
elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
652 |
is the rule |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
653 |
\[ |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
654 |
\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
655 |
\] |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
656 |
Applying the rule backwards, this breaks down some implication on |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
657 |
the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
658 |
the sets of formulae that are unaffected by the inference. The |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
659 |
analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
660 |
single rule |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
661 |
\[ |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
662 |
\infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
663 |
\] |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
664 |
This breaks down some disjunction on the right side, replacing it by |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
665 |
both disjuncts. Thus, the sequent calculus is a kind of |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
666 |
multiple-conclusion logic. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
667 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
668 |
To illustrate the use of multiple formulae on the right, let us |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
669 |
prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}. Working |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
670 |
backwards, we reduce this formula to a basic sequent: |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
671 |
\[ |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
672 |
\infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
673 |
{\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
674 |
{\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
675 |
{@{text "P, Q \<turnstile> Q, P"}}}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
676 |
\] |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
677 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
678 |
This example is typical of the sequent calculus: start with the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
679 |
desired theorem and apply rules backwards in a fairly arbitrary |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
680 |
manner. This yields a surprisingly effective proof procedure. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
681 |
Quantifiers add only few complications, since Isabelle handles |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
682 |
parameters and schematic variables. See \cite[Chapter |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
683 |
10]{paulson-ml2} for further discussion. *} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
684 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
685 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
686 |
subsubsection {* Simulating sequents by natural deduction *} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
687 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
688 |
text {* Isabelle can represent sequents directly, as in the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
689 |
object-logic LK. But natural deduction is easier to work with, and |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
690 |
most object-logics employ it. Fortunately, we can simulate the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
691 |
sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
692 |
@{text "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>2 \<Longrightarrow> ... \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> Q\<^sub>1"} where the order of |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
693 |
the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
694 |
Elim-resolution plays a key role in simulating sequent proofs. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
695 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
696 |
We can easily handle reasoning on the left. Elim-resolution with |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
697 |
the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
698 |
a similar effect as the corresponding sequent rules. For the other |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
699 |
connectives, we use sequent-style elimination rules instead of |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
700 |
destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
701 |
But note that the rule @{text "(\<not>L)"} has no effect under our |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
702 |
representation of sequents! |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
703 |
\[ |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
704 |
\infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
705 |
\] |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
706 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
707 |
What about reasoning on the right? Introduction rules can only |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
708 |
affect the formula in the conclusion, namely @{text "Q\<^sub>1"}. The |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
709 |
other right-side formulae are represented as negated assumptions, |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
710 |
@{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}. In order to operate on one of these, it |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
711 |
must first be exchanged with @{text "Q\<^sub>1"}. Elim-resolution with the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
712 |
@{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
713 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
714 |
To ensure that swaps occur only when necessary, each introduction |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
715 |
rule is converted into a swapped form: it is resolved with the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
716 |
second premise of @{text "(swap)"}. The swapped form of @{text |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
717 |
"(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
718 |
@{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
719 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
720 |
Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
721 |
@{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
722 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
723 |
Swapped introduction rules are applied using elim-resolution, which |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
724 |
deletes the negated formula. Our representation of sequents also |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
725 |
requires the use of ordinary introduction rules. If we had no |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
726 |
regard for readability of intermediate goal states, we could treat |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
727 |
the right side more uniformly by representing sequents as @{text |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
728 |
[display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
729 |
*} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
730 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
731 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
732 |
subsubsection {* Extra rules for the sequent calculus *} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
733 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
734 |
text {* As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
735 |
@{text "(\<forall>E)"} must be replaced by sequent-style elimination rules. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
736 |
In addition, we need rules to embody the classical equivalence |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
737 |
between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}. The introduction |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
738 |
rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
739 |
@{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
740 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
741 |
The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display] |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
742 |
"(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
743 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
744 |
Quantifier replication also requires special rules. In classical |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
745 |
logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"}; |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
746 |
the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual: |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
747 |
\[ |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
748 |
\infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
749 |
\qquad |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
750 |
\infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
751 |
\] |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
752 |
Thus both kinds of quantifier may be replicated. Theorems requiring |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
753 |
multiple uses of a universal formula are easy to invent; consider |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
754 |
@{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
755 |
@{text "n > 1"}. Natural examples of the multiple use of an |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
756 |
existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
757 |
\<longrightarrow> P y"}. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
758 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
759 |
Forgoing quantifier replication loses completeness, but gains |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
760 |
decidability, since the search space becomes finite. Many useful |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
761 |
theorems can be proved without replication, and the search generally |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
762 |
delivers its verdict in a reasonable time. To adopt this approach, |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
763 |
represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
764 |
@{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"}, |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
765 |
respectively, and put @{text "(\<forall>E)"} into elimination form: @{text |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
766 |
[display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
767 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
768 |
Elim-resolution with this rule will delete the universal formula |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
769 |
after a single use. To replicate universal quantifiers, replace the |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
770 |
rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
771 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
772 |
To replicate existential quantifiers, replace @{text "(\<exists>I)"} by |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
773 |
@{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
774 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
775 |
All introduction rules mentioned above are also useful in swapped |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
776 |
form. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
777 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
778 |
Replication makes the search space infinite; we must apply the rules |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
779 |
with care. The classical reasoner distinguishes between safe and |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
780 |
unsafe rules, applying the latter only when there is no alternative. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
781 |
Depth-first search may well go down a blind alley; best-first search |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
782 |
is better behaved in an infinite search space. However, quantifier |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
783 |
replication is too expensive to prove any but the simplest theorems. |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
784 |
*} |
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
785 |
|
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset
|
786 |
|
42928
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
787 |
subsection {* Rule declarations *} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
788 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
789 |
text {* The proof tools of the Classical Reasoner depend on |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
790 |
collections of rules declared in the context, which are classified |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
791 |
as introduction, elimination or destruction and as \emph{safe} or |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
792 |
\emph{unsafe}. In general, safe rules can be attempted blindly, |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
793 |
while unsafe rules must be used with care. A safe rule must never |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
794 |
reduce a provable goal to an unprovable set of subgoals. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
795 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
796 |
The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
797 |
\<or> Q"} to @{text "P"}, which might turn out as premature choice of an |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
798 |
unprovable subgoal. Any rule is unsafe whose premises contain new |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
799 |
unknowns. The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
800 |
unsafe, since it is applied via elim-resolution, which discards the |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
801 |
assumption @{text "\<forall>x. P x"} and replaces it by the weaker |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
802 |
assumption @{text "P t"}. The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
803 |
unsafe for similar reasons. The quantifier duplication rule @{text |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
804 |
"\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense: |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
805 |
since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
806 |
looping. In classical first-order logic, all rules are safe except |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
807 |
those mentioned above. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
808 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
809 |
The safe~/ unsafe distinction is vague, and may be regarded merely |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
810 |
as a way of giving some rules priority over others. One could argue |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
811 |
that @{text "(\<or>E)"} is unsafe, because repeated application of it |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
812 |
could generate exponentially many subgoals. Induction rules are |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
813 |
unsafe because inductive proofs are difficult to set up |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
814 |
automatically. Any inference is unsafe that instantiates an unknown |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
815 |
in the proof state --- thus matching must be used, rather than |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
816 |
unification. Even proof by assumption is unsafe if it instantiates |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
817 |
unknowns shared with other subgoals. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
818 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
819 |
\begin{matharray}{rcl} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
820 |
@{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
821 |
@{attribute_def intro} & : & @{text attribute} \\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
822 |
@{attribute_def elim} & : & @{text attribute} \\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
823 |
@{attribute_def dest} & : & @{text attribute} \\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
824 |
@{attribute_def rule} & : & @{text attribute} \\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
825 |
@{attribute_def iff} & : & @{text attribute} \\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
826 |
@{attribute_def swapped} & : & @{text attribute} \\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
827 |
\end{matharray} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
828 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
829 |
@{rail " |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
830 |
(@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}? |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
831 |
; |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
832 |
@@{attribute rule} 'del' |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
833 |
; |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
834 |
@@{attribute iff} (((() | 'add') '?'?) | 'del') |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
835 |
"} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
836 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
837 |
\begin{description} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
838 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
839 |
\item @{command "print_claset"} prints the collection of rules |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
840 |
declared to the Classical Reasoner, i.e.\ the @{ML_type claset} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
841 |
within the context. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
842 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
843 |
\item @{attribute intro}, @{attribute elim}, and @{attribute dest} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
844 |
declare introduction, elimination, and destruction rules, |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
845 |
respectively. By default, rules are considered as \emph{unsafe} |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
846 |
(i.e.\ not applied blindly without backtracking), while ``@{text |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
847 |
"!"}'' classifies as \emph{safe}. Rule declarations marked by |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
848 |
``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\ |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
849 |
\secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
850 |
of the @{method rule} method). The optional natural number |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
851 |
specifies an explicit weight argument, which is ignored by the |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
852 |
automated reasoning tools, but determines the search order of single |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
853 |
rule steps. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
854 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
855 |
Introduction rules are those that can be applied using ordinary |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
856 |
resolution. Their swapped forms are generated internally, which |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
857 |
will be applied using elim-resolution. Elimination rules are |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
858 |
applied using elim-resolution. Rules are sorted by the number of |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
859 |
new subgoals they will yield; rules that generate the fewest |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
860 |
subgoals will be tried first. Otherwise, later declarations take |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
861 |
precedence over earlier ones. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
862 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
863 |
Rules already present in the context with the same classification |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
864 |
are ignored. A warning is printed if the rule has already been |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
865 |
added with some other classification, but the rule is added anyway |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
866 |
as requested. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
867 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
868 |
\item @{attribute rule}~@{text del} deletes all occurrences of a |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
869 |
rule from the classical context, regardless of its classification as |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
870 |
introduction~/ elimination~/ destruction and safe~/ unsafe. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
871 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
872 |
\item @{attribute iff} declares logical equivalences to the |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
873 |
Simplifier and the Classical reasoner at the same time. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
874 |
Non-conditional rules result in a safe introduction and elimination |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
875 |
pair; conditional ones are considered unsafe. Rules with negative |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
876 |
conclusion are automatically inverted (using @{text "\<not>"}-elimination |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
877 |
internally). |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
878 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
879 |
The ``@{text "?"}'' version of @{attribute iff} declares rules to |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
880 |
the Isabelle/Pure context only, and omits the Simplifier |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
881 |
declaration. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
882 |
|
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
883 |
\item @{attribute swapped} turns an introduction rule into an |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
884 |
elimination, by resolving with the classical swap principle @{text |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
885 |
"\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
886 |
illustrative purposes: the Classical Reasoner already swaps rules |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
887 |
internally as explained above. |
9d946de41120
updated and re-unified classical rule declarations;
wenzelm
parents:
42927
diff
changeset
|
888 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
889 |
\end{description} |
26782 | 890 |
*} |
891 |
||
892 |
||
43365 | 893 |
subsection {* Structured methods *} |
894 |
||
895 |
text {* |
|
896 |
\begin{matharray}{rcl} |
|
897 |
@{method_def rule} & : & @{text method} \\ |
|
898 |
@{method_def contradiction} & : & @{text method} \\ |
|
899 |
\end{matharray} |
|
900 |
||
901 |
@{rail " |
|
902 |
@@{method rule} @{syntax thmrefs}? |
|
903 |
"} |
|
904 |
||
905 |
\begin{description} |
|
906 |
||
907 |
\item @{method rule} as offered by the Classical Reasoner is a |
|
908 |
refinement over the Pure one (see \secref{sec:pure-meth-att}). Both |
|
909 |
versions work the same, but the classical version observes the |
|
910 |
classical rule context in addition to that of Isabelle/Pure. |
|
911 |
||
912 |
Common object logics (HOL, ZF, etc.) declare a rich collection of |
|
913 |
classical rules (even if these would qualify as intuitionistic |
|
914 |
ones), but only few declarations to the rule context of |
|
915 |
Isabelle/Pure (\secref{sec:pure-meth-att}). |
|
916 |
||
917 |
\item @{method contradiction} solves some goal by contradiction, |
|
918 |
deriving any result from both @{text "\<not> A"} and @{text A}. Chained |
|
919 |
facts, which are guaranteed to participate, may appear in either |
|
920 |
order. |
|
921 |
||
922 |
\end{description} |
|
923 |
*} |
|
924 |
||
925 |
||
27040 | 926 |
subsection {* Automated methods *} |
26782 | 927 |
|
928 |
text {* |
|
929 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
930 |
@{method_def blast} & : & @{text method} \\ |
42930 | 931 |
@{method_def auto} & : & @{text method} \\ |
932 |
@{method_def force} & : & @{text method} \\ |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
933 |
@{method_def fast} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
934 |
@{method_def slow} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
935 |
@{method_def best} & : & @{text method} \\ |
44911 | 936 |
@{method_def fastforce} & : & @{text method} \\ |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
937 |
@{method_def slowsimp} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
938 |
@{method_def bestsimp} & : & @{text method} \\ |
43367 | 939 |
@{method_def deepen} & : & @{text method} \\ |
26782 | 940 |
\end{matharray} |
941 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
942 |
@{rail " |
42930 | 943 |
@@{method blast} @{syntax nat}? (@{syntax clamod} * ) |
944 |
; |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
945 |
@@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * ) |
26782 | 946 |
; |
42930 | 947 |
@@{method force} (@{syntax clasimpmod} * ) |
948 |
; |
|
949 |
(@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * ) |
|
26782 | 950 |
; |
44911 | 951 |
(@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp}) |
42930 | 952 |
(@{syntax clasimpmod} * ) |
953 |
; |
|
43367 | 954 |
@@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * ) |
955 |
; |
|
42930 | 956 |
@{syntax_def clamod}: |
957 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs} |
|
958 |
; |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
959 |
@{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') | |
26782 | 960 |
('cong' | 'split') (() | 'add' | 'del') | |
961 |
'iff' (((() | 'add') '?'?) | 'del') | |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
962 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
963 |
"} |
26782 | 964 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
965 |
\begin{description} |
26782 | 966 |
|
42930 | 967 |
\item @{method blast} is a separate classical tableau prover that |
968 |
uses the same classical rule declarations as explained before. |
|
969 |
||
970 |
Proof search is coded directly in ML using special data structures. |
|
971 |
A successful proof is then reconstructed using regular Isabelle |
|
972 |
inferences. It is faster and more powerful than the other classical |
|
973 |
reasoning tools, but has major limitations too. |
|
974 |
||
975 |
\begin{itemize} |
|
976 |
||
977 |
\item It does not use the classical wrapper tacticals, such as the |
|
44911 | 978 |
integration with the Simplifier of @{method fastforce}. |
42930 | 979 |
|
980 |
\item It does not perform higher-order unification, as needed by the |
|
981 |
rule @{thm [source=false] rangeI} in HOL. There are often |
|
982 |
alternatives to such rules, for example @{thm [source=false] |
|
983 |
range_eqI}. |
|
984 |
||
985 |
\item Function variables may only be applied to parameters of the |
|
986 |
subgoal. (This restriction arises because the prover does not use |
|
987 |
higher-order unification.) If other function variables are present |
|
988 |
then the prover will fail with the message \texttt{Function Var's |
|
989 |
argument not a bound variable}. |
|
990 |
||
991 |
\item Its proof strategy is more general than @{method fast} but can |
|
992 |
be slower. If @{method blast} fails or seems to be running forever, |
|
993 |
try @{method fast} and the other proof tools described below. |
|
994 |
||
995 |
\end{itemize} |
|
996 |
||
997 |
The optional integer argument specifies a bound for the number of |
|
998 |
unsafe steps used in a proof. By default, @{method blast} starts |
|
999 |
with a bound of 0 and increases it successively to 20. In contrast, |
|
1000 |
@{text "(blast lim)"} tries to prove the goal using a search bound |
|
1001 |
of @{text "lim"}. Sometimes a slow proof using @{method blast} can |
|
1002 |
be made much faster by supplying the successful search bound to this |
|
1003 |
proof method instead. |
|
1004 |
||
1005 |
\item @{method auto} combines classical reasoning with |
|
1006 |
simplification. It is intended for situations where there are a lot |
|
1007 |
of mostly trivial subgoals; it proves all the easy ones, leaving the |
|
1008 |
ones it cannot prove. Occasionally, attempting to prove the hard |
|
1009 |
ones may take a long time. |
|
1010 |
||
43332 | 1011 |
The optional depth arguments in @{text "(auto m n)"} refer to its |
1012 |
builtin classical reasoning procedures: @{text m} (default 4) is for |
|
1013 |
@{method blast}, which is tried first, and @{text n} (default 2) is |
|
1014 |
for a slower but more general alternative that also takes wrappers |
|
1015 |
into account. |
|
42930 | 1016 |
|
1017 |
\item @{method force} is intended to prove the first subgoal |
|
1018 |
completely, using many fancy proof tools and performing a rather |
|
1019 |
exhaustive search. As a result, proof attempts may take rather long |
|
1020 |
or diverge easily. |
|
1021 |
||
1022 |
\item @{method fast}, @{method best}, @{method slow} attempt to |
|
1023 |
prove the first subgoal using sequent-style reasoning as explained |
|
1024 |
before. Unlike @{method blast}, they construct proofs directly in |
|
1025 |
Isabelle. |
|
26782 | 1026 |
|
42930 | 1027 |
There is a difference in search strategy and back-tracking: @{method |
1028 |
fast} uses depth-first search and @{method best} uses best-first |
|
1029 |
search (guided by a heuristic function: normally the total size of |
|
1030 |
the proof state). |
|
1031 |
||
1032 |
Method @{method slow} is like @{method fast}, but conducts a broader |
|
1033 |
search: it may, when backtracking from a failed proof attempt, undo |
|
1034 |
even the step of proving a subgoal by assumption. |
|
1035 |
||
44911 | 1036 |
\item @{method fastforce}, @{method slowsimp}, @{method bestsimp} are |
42930 | 1037 |
like @{method fast}, @{method slow}, @{method best}, respectively, |
44911 | 1038 |
but use the Simplifier as additional wrapper. The name @{method fastforce}, |
1039 |
as opposed to @{text fastsimp}, reflects the behaviour of this popular |
|
1040 |
method better without requiring an understanding of its implementation. |
|
42930 | 1041 |
|
43367 | 1042 |
\item @{method deepen} works by exhaustive search up to a certain |
1043 |
depth. The start depth is 4 (unless specified explicitly), and the |
|
1044 |
depth is increased iteratively up to 10. Unsafe rules are modified |
|
1045 |
to preserve the formula they act on, so that it be used repeatedly. |
|
1046 |
This method can prove more goals than @{method fast}, but is much |
|
1047 |
slower, for example if the assumptions have many universal |
|
1048 |
quantifiers. |
|
1049 |
||
42930 | 1050 |
\end{description} |
1051 |
||
1052 |
Any of the above methods support additional modifiers of the context |
|
1053 |
of classical (and simplifier) rules, but the ones related to the |
|
1054 |
Simplifier are explicitly prefixed by @{text simp} here. The |
|
1055 |
semantics of these ad-hoc rule declarations is analogous to the |
|
1056 |
attributes given before. Facts provided by forward chaining are |
|
1057 |
inserted into the goal before commencing proof search. |
|
1058 |
*} |
|
1059 |
||
1060 |
||
1061 |
subsection {* Semi-automated methods *} |
|
1062 |
||
1063 |
text {* These proof methods may help in situations when the |
|
1064 |
fully-automated tools fail. The result is a simpler subgoal that |
|
1065 |
can be tackled by other means, such as by manual instantiation of |
|
1066 |
quantifiers. |
|
1067 |
||
1068 |
\begin{matharray}{rcl} |
|
1069 |
@{method_def safe} & : & @{text method} \\ |
|
1070 |
@{method_def clarify} & : & @{text method} \\ |
|
1071 |
@{method_def clarsimp} & : & @{text method} \\ |
|
1072 |
\end{matharray} |
|
1073 |
||
1074 |
@{rail " |
|
1075 |
(@@{method safe} | @@{method clarify}) (@{syntax clamod} * ) |
|
1076 |
; |
|
1077 |
@@{method clarsimp} (@{syntax clasimpmod} * ) |
|
1078 |
"} |
|
1079 |
||
1080 |
\begin{description} |
|
1081 |
||
1082 |
\item @{method safe} repeatedly performs safe steps on all subgoals. |
|
1083 |
It is deterministic, with at most one outcome. |
|
1084 |
||
43366 | 1085 |
\item @{method clarify} performs a series of safe steps without |
1086 |
splitting subgoals; see also @{ML clarify_step_tac}. |
|
42930 | 1087 |
|
1088 |
\item @{method clarsimp} acts like @{method clarify}, but also does |
|
1089 |
simplification. Note that if the Simplifier context includes a |
|
1090 |
splitter for the premises, the subgoal may still be split. |
|
26782 | 1091 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1092 |
\end{description} |
26782 | 1093 |
*} |
1094 |
||
1095 |
||
43366 | 1096 |
subsection {* Single-step tactics *} |
1097 |
||
1098 |
text {* |
|
1099 |
\begin{matharray}{rcl} |
|
1100 |
@{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1101 |
@{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1102 |
@{index_ML step_tac: "Proof.context -> int -> tactic"} \\ |
|
1103 |
@{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1104 |
@{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1105 |
\end{matharray} |
|
1106 |
||
1107 |
These are the primitive tactics behind the (semi)automated proof |
|
1108 |
methods of the Classical Reasoner. By calling them yourself, you |
|
1109 |
can execute these procedures one step at a time. |
|
1110 |
||
1111 |
\begin{description} |
|
1112 |
||
1113 |
\item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on |
|
1114 |
subgoal @{text i}. The safe wrapper tacticals are applied to a |
|
1115 |
tactic that may include proof by assumption or Modus Ponens (taking |
|
1116 |
care not to instantiate unknowns), or substitution. |
|
1117 |
||
1118 |
\item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows |
|
1119 |
unknowns to be instantiated. |
|
1120 |
||
1121 |
\item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof |
|
1122 |
procedure. The unsafe wrapper tacticals are applied to a tactic |
|
1123 |
that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe |
|
1124 |
rule from the context. |
|
1125 |
||
1126 |
\item @{ML slow_step_tac} resembles @{ML step_tac}, but allows |
|
1127 |
backtracking between using safe rules with instantiation (@{ML |
|
1128 |
inst_step_tac}) and using unsafe rules. The resulting search space |
|
1129 |
is larger. |
|
1130 |
||
1131 |
\item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step |
|
1132 |
on subgoal @{text i}. No splitting step is applied; for example, |
|
1133 |
the subgoal @{text "A \<and> B"} is left as a conjunction. Proof by |
|
1134 |
assumption, Modus Ponens, etc., may be performed provided they do |
|
1135 |
not instantiate unknowns. Assumptions of the form @{text "x = t"} |
|
1136 |
may be eliminated. The safe wrapper tactical is applied. |
|
1137 |
||
1138 |
\end{description} |
|
1139 |
*} |
|
1140 |
||
1141 |
||
27044 | 1142 |
section {* Object-logic setup \label{sec:object-logic} *} |
26790 | 1143 |
|
1144 |
text {* |
|
1145 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1146 |
@{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1147 |
@{method_def atomize} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1148 |
@{attribute_def atomize} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1149 |
@{attribute_def rule_format} & : & @{text attribute} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1150 |
@{attribute_def rulify} & : & @{text attribute} \\ |
26790 | 1151 |
\end{matharray} |
1152 |
||
1153 |
The very starting point for any Isabelle object-logic is a ``truth |
|
1154 |
judgment'' that links object-level statements to the meta-logic |
|
1155 |
(with its minimal language of @{text prop} that covers universal |
|
1156 |
quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}). |
|
1157 |
||
1158 |
Common object-logics are sufficiently expressive to internalize rule |
|
1159 |
statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own |
|
1160 |
language. This is useful in certain situations where a rule needs |
|
1161 |
to be viewed as an atomic statement from the meta-level perspective, |
|
1162 |
e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}. |
|
1163 |
||
1164 |
From the following language elements, only the @{method atomize} |
|
1165 |
method and @{attribute rule_format} attribute are occasionally |
|
1166 |
required by end-users, the rest is for those who need to setup their |
|
1167 |
own object-logic. In the latter case existing formulations of |
|
1168 |
Isabelle/FOL or Isabelle/HOL may be taken as realistic examples. |
|
1169 |
||
1170 |
Generic tools may refer to the information provided by object-logic |
|
1171 |
declarations internally. |
|
1172 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
1173 |
@{rail " |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
1174 |
@@{command judgment} @{syntax constdecl} |
26790 | 1175 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
1176 |
@@{attribute atomize} ('(' 'full' ')')? |
26790 | 1177 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
1178 |
@@{attribute rule_format} ('(' 'noasm' ')')? |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset
|
1179 |
"} |
26790 | 1180 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1181 |
\begin{description} |
26790 | 1182 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1183 |
\item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1184 |
@{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
|
1185 |
type @{text \<sigma>} should specify a coercion of the category of |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1186 |
object-level propositions to @{text prop} of the Pure meta-logic; |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1187 |
the mixfix annotation @{text "(mx)"} would typically just link the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1188 |
object language (internally of syntactic category @{text logic}) |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1189 |
with that of @{text prop}. Only one @{command "judgment"} |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1190 |
declaration may be given in any theory development. |
26790 | 1191 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1192 |
\item @{method atomize} (as a method) rewrites any non-atomic |
26790 | 1193 |
premises of a sub-goal, using the meta-level equations declared via |
1194 |
@{attribute atomize} (as an attribute) beforehand. As a result, |
|
1195 |
heavily nested goals become amenable to fundamental operations such |
|
42626 | 1196 |
as resolution (cf.\ the @{method (Pure) rule} method). Giving the ``@{text |
26790 | 1197 |
"(full)"}'' option here means to turn the whole subgoal into an |
1198 |
object-statement (if possible), including the outermost parameters |
|
1199 |
and assumptions as well. |
|
1200 |
||
1201 |
A typical collection of @{attribute atomize} rules for a particular |
|
1202 |
object-logic would provide an internalization for each of the |
|
1203 |
connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}. |
|
1204 |
Meta-level conjunction should be covered as well (this is |
|
1205 |
particularly important for locales, see \secref{sec:locale}). |
|
1206 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1207 |
\item @{attribute rule_format} rewrites a theorem by the equalities |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1208 |
declared as @{attribute rulify} rules in the current object-logic. |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1209 |
By default, the result is fully normalized, including assumptions |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1210 |
and conclusions at any depth. The @{text "(no_asm)"} option |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1211 |
restricts the transformation to the conclusion of a rule. |
26790 | 1212 |
|
1213 |
In common object-logics (HOL, FOL, ZF), the effect of @{attribute |
|
1214 |
rule_format} is to replace (bounded) universal quantification |
|
1215 |
(@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding |
|
1216 |
rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}. |
|
1217 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset
|
1218 |
\end{description} |
26790 | 1219 |
*} |
1220 |
||
26782 | 1221 |
end |