author  wenzelm 
Sat, 10 Nov 2012 20:16:16 +0100  
changeset 50079  5c36db9db335 
parent 50077  1edd0db7b6c4 
child 50080  200f749c96db 
permissions  rwrr 
26782  1 
theory Generic 
42651  2 
imports Base Main 
26782  3 
begin 
4 

5 
chapter {* Generic tools and packages \label{ch:gentools} *} 

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:miscmethatt} *} 

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:puremethatt}), but apply rules by 

97 
elimresolution, destructresolution, and forwardresolution, 

98 
respectively \cite{isabelleimplementation}. 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 singlestep 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 elimresolution, after having inserted any chained 

112 
facts. Exactly the rules given as arguments are taken into account; 

113 
this allows finetuned 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:proofmeth}). 
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:proofmeth}). 
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 unfolded} & : & @{text attribute} \\ 
47497  131 
@{attribute_def folded} & : & @{text attribute} \\ 
132 
@{attribute_def abs_def} & : & @{text attribute} \\[0.5ex] 

28761
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 
; 
48205  144 
@@{attribute THEN} ('[' @{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 

48205  159 
\item @{attribute THEN}~@{text a} composes rules by resolution; it 
160 
resolves with the first premise of @{text a} (an alternative 

161 
position may be also specified). See also @{ML_op "RS"} in 

162 
\cite{isabelleimplementation}. 

26782  163 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

164 
\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

165 
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

166 
definitions throughout a rule. 
26782  167 

47497  168 
\item @{attribute abs_def} turns an equation of the form @{prop "f x 
169 
y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method 

170 
simp} or @{method unfold} steps always expand it. This also works 

171 
for objectlogic equality. 

172 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

173 
\item @{attribute rotated}~@{text n} rotate the premises of a 
26782  174 
theorem by @{text n} (default 1). 
175 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

176 
\item @{attribute (Pure) elim_format} turns a destruction rule into 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

177 
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

178 
(PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}. 
26782  179 

180 
Note that the Classical Reasoner (\secref{sec:classical}) provides 

181 
its own version of this operation. 

182 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

183 
\item @{attribute standard} puts a theorem into the standard form of 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

184 
objectrules at the outermost theory level. Note that this 
26782  185 
operation violates the local proof context (including active 
186 
locales). 

187 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

188 
\item @{attribute no_vars} replaces schematic variables by free 
26782  189 
ones; this is mainly for tuning output of pretty printed theorems. 
190 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

191 
\end{description} 
26782  192 
*} 
193 

194 

27044  195 
subsection {* Lowlevel equational reasoning *} 
196 

197 
text {* 

198 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

199 
@{method_def subst} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

200 
@{method_def hypsubst} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

201 
@{method_def split} & : & @{text method} \\ 
27044  202 
\end{matharray} 
203 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

204 
@{rail " 
42704  205 
@@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} 
27044  206 
; 
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

207 
@@{method split} @{syntax thmrefs} 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

208 
"} 
27044  209 

210 
These methods provide lowlevel facilities for equational reasoning 

211 
that are intended for specialized applications only. Normally, 

212 
single step calculations would be performed in a structured text 

213 
(see also \secref{sec:calculation}), while the Simplifier methods 

214 
provide the canonical way for automated normalization (see 

215 
\secref{sec:simplifier}). 

216 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

217 
\begin{description} 
27044  218 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

219 
\item @{method subst}~@{text eq} performs a single substitution step 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

220 
using rule @{text eq}, which may be either a meta or object 
27044  221 
equality. 
222 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

223 
\item @{method subst}~@{text "(asm) eq"} substitutes in an 
27044  224 
assumption. 
225 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

226 
\item @{method subst}~@{text "(i \<dots> j) eq"} performs several 
27044  227 
substitutions in the conclusion. The numbers @{text i} to @{text j} 
228 
indicate the positions to substitute at. Positions are ordered from 

229 
the top of the term tree moving down from left to right. For 

230 
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

231 
where commutativity of @{text "+"} is applicable: 1 refers to @{text 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

232 
"a + b"}, 2 to the whole term, and 3 to @{text "c + d"}. 
27044  233 

234 
If the positions in the list @{text "(i \<dots> j)"} are nonoverlapping 

235 
(e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may 

236 
assume all substitutions are performed simultaneously. Otherwise 

237 
the behaviour of @{text subst} is not specified. 

238 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

239 
\item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the 
27071  240 
substitutions in the assumptions. The positions refer to the 
241 
assumptions in order from left to right. For example, given in a 

242 
goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of 

243 
commutativity of @{text "+"} is the subterm @{text "a + b"} and 

244 
position 2 is the subterm @{text "c + d"}. 

27044  245 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

246 
\item @{method hypsubst} performs substitution using some 
27044  247 
assumption; this only works for equations of the form @{text "x = 
248 
t"} where @{text x} is a free or bound variable. 

249 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

250 
\item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs singlestep case 
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

251 
splitting using the given rules. Splitting is performed in the 
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

252 
conclusion or some assumption of the subgoal, depending of the 
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

253 
structure of the rule. 
27044  254 

255 
Note that the @{method simp} method already involves repeated 

44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

256 
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

257 
@{attribute split}, for example. 
27044  258 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

259 
\end{description} 
27044  260 
*} 
261 

262 

26782  263 
subsection {* Further tactic emulations \label{sec:tactics} *} 
264 

265 
text {* 

266 
The following improper proof methods emulate traditional tactics. 

267 
These admit direct access to the goal state, which is normally 

268 
considered harmful! In particular, this may involve both numbered 

269 
goal addressing (default 1), and dynamic instantiation within the 

270 
scope of some subgoal. 

271 

272 
\begin{warn} 

273 
Dynamic instantiations refer to universally quantified parameters 

274 
of a subgoal (the dynamic context) rather than fixed variables and 

275 
term abbreviations of a (static) Isar context. 

276 
\end{warn} 

277 

278 
Tactic emulation methods, unlike their ML counterparts, admit 

279 
simultaneous instantiation from both dynamic and static contexts. 

280 
If names occur in both contexts goal parameters hide locally fixed 

281 
variables. Likewise, schematic variables refer to term 

282 
abbreviations, if present in the static context. Otherwise the 

283 
schematic variable is interpreted as a schematic variable and left 

284 
to be solved by unification with certain parts of the subgoal. 

285 

286 
Note that the tactic emulation proof methods in Isabelle/Isar are 

287 
consistently named @{text foo_tac}. Note also that variable names 

288 
occurring on left hand sides of instantiations must be preceded by a 

289 
question mark if they coincide with a keyword or contain dots. This 

290 
is consistent with the attribute @{attribute "where"} (see 

291 
\secref{sec:puremethatt}). 

292 

293 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

294 
@{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

295 
@{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

296 
@{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

297 
@{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

298 
@{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

299 
@{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

300 
@{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

301 
@{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

302 
@{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

303 
@{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

304 
@{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ 
26782  305 
\end{matharray} 
306 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

307 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

308 
(@@{method rule_tac}  @@{method erule_tac}  @@{method drule_tac}  
42705  309 
@@{method frule_tac}  @@{method cut_tac}  @@{method thin_tac}) @{syntax goal_spec}? \\ 
42617  310 
( dynamic_insts @'in' @{syntax thmref}  @{syntax thmrefs} ) 
26782  311 
; 
42705  312 
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

313 
; 
42705  314 
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +) 
26782  315 
; 
42705  316 
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}? 
26782  317 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

318 
(@@{method tactic}  @@{method raw_tactic}) @{syntax text} 
26782  319 
; 
320 

42617  321 
dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') 
322 
"} 

26782  323 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

324 
\begin{description} 
26782  325 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

326 
\item @{method rule_tac} etc. do resolution of rules with explicit 
26782  327 
instantiation. This works the same way as the ML tactics @{ML 
30397  328 
res_inst_tac} etc. (see \cite{isabelleimplementation}) 
26782  329 

330 
Multiple rules may be only given if there is no instantiation; then 

331 
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see 

30397  332 
\cite{isabelleimplementation}). 
26782  333 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

334 
\item @{method cut_tac} inserts facts into the proof state as 
46706
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

335 
assumption of a subgoal; instantiations may be given as well. Note 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

336 
that the scope of schematic variables is spread over the main goal 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

337 
statement and rule premises are turned into new subgoals. This is 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

338 
in contrast to the regular method @{method insert} which inserts 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

339 
closed rule statements. 
26782  340 

46277  341 
\item @{method thin_tac}~@{text \<phi>} deletes the specified premise 
342 
from a subgoal. Note that @{text \<phi>} may contain schematic 

343 
variables, to abbreviate the intended proposition; the first 

344 
matching subgoal premise will be deleted. Removing useless premises 

345 
from a subgoal increases its readability and can make search tactics 

346 
run faster. 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

347 

46271  348 
\item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions 
349 
@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same 

350 
as new subgoals (in the original context). 

26782  351 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

352 
\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

353 
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

354 
\emph{suffix} of variables. 
26782  355 

46274  356 
\item @{method rotate_tac}~@{text n} rotates the premises of a 
357 
subgoal by @{text n} positions: from right to left if @{text n} is 

26782  358 
positive, and from left to right if @{text n} is negative; the 
46274  359 
default value is 1. 
26782  360 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

361 
\item @{method tactic}~@{text "text"} produces a proof method from 
26782  362 
any ML text of type @{ML_type tactic}. Apart from the usual ML 
27223  363 
environment and the current proof context, the ML code may refer to 
364 
the locally bound values @{ML_text facts}, which indicates any 

365 
current facts used for forwardchaining. 

26782  366 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

367 
\item @{method raw_tactic} is similar to @{method tactic}, but 
27223  368 
presents the goal state in its raw internal form, where simultaneous 
369 
subgoals appear as conjunction of the logical framework instead of 

370 
the usual split into several subgoals. While feature this is useful 

371 
for debugging of complex method definitions, it should not never 

372 
appear in production theories. 

26782  373 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

374 
\end{description} 
26782  375 
*} 
376 

377 

27040  378 
section {* The Simplifier \label{sec:simplifier} *} 
26782  379 

50063  380 
text {* The Simplifier performs conditional and unconditional 
381 
rewriting and uses contextual information: rule declarations in the 

382 
background theory or local proof context are taken into account, as 

383 
well as chained facts and subgoal premises (``local assumptions''). 

384 
There are several general hooks that allow to modify the 

385 
simplification strategy, or incorporate other proof tools that solve 

386 
subproblems, produce rewrite rules on demand etc. 

387 

50075  388 
The rewriting strategy is always strictly bottom up, except for 
389 
congruence rules, which are applied while descending into a term. 

390 
Conditions in conditional rewrite rules are solved recursively 

391 
before the rewrite rule is applied. 

392 

50063  393 
The default Simplifier setup of major object logics (HOL, HOLCF, 
394 
FOL, ZF) makes the Simplifier ready for immediate use, without 

395 
engaging into the internal structures. Thus it serves as 

396 
generalpurpose proof tool with the main focus on equational 

50075  397 
reasoning, and a bit more than that. 
398 
*} 

50063  399 

400 

401 
subsection {* Simplification methods \label{sec:simpmeth} *} 

26782  402 

403 
text {* 

404 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

405 
@{method_def simp} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

406 
@{method_def simp_all} & : & @{text method} \\ 
26782  407 
\end{matharray} 
408 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

409 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

410 
(@@{method simp}  @@{method simp_all}) opt? (@{syntax simpmod} * ) 
26782  411 
; 
412 

40255
9ffbc25e1606
eliminated obsolete \_ escapes in rail environments;
wenzelm
parents:
35613
diff
changeset

413 
opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use'  'asm_lr' ) ')' 
26782  414 
; 
50063  415 
@{syntax_def simpmod}: ('add'  'del'  'only'  'split' (()  'add'  'del')  
416 
'cong' (()  'add'  'del')) ':' @{syntax thmrefs} 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

417 
"} 
26782  418 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

419 
\begin{description} 
26782  420 

50063  421 
\item @{method simp} invokes the Simplifier on the first subgoal, 
422 
after inserting chained facts as additional goal premises; further 

423 
rule declarations may be included via @{text "(simp add: facts)"}. 

424 
The proof method fails if the subgoal remains unchanged after 

425 
simplification. 

26782  426 

50063  427 
Note that the original goal premises and chained facts are subject 
428 
to simplification themselves, while declarations via @{text 

429 
"add"}/@{text "del"} merely follow the policies of the objectlogic 

430 
to extract rewrite rules from theorems, without further 

431 
simplification. This may lead to slightly different behavior in 

432 
either case, which might be required precisely like that in some 

433 
boundary situations to perform the intended simplification step! 

434 

435 
\medskip The @{text only} modifier first removes all other rewrite 

436 
rules, looper tactics (including split rules), congruence rules, and 

437 
then behaves like @{text add}. Implicit solvers remain, which means 

438 
that trivial rules like reflexivity or introduction of @{text 

439 
"True"} are available to solve the simplified subgoals, but also 

440 
nontrivial tools like linear arithmetic in HOL. The latter may 

441 
lead to some surprise of the meaning of ``only'' in Isabelle/HOL 

442 
compared to English! 

26782  443 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

444 
\medskip The @{text split} modifiers add or delete rules for the 
50079  445 
Splitter (see also \secref{sec:simpstrategies} on the looper). 
26782  446 
This works only if the Simplifier method has been properly setup to 
447 
include the Splitter (all major object logics such HOL, HOLCF, FOL, 

448 
ZF do this already). 

449 

50065  450 
There is also a separate @{method_ref split} method available for 
451 
singlestep case splitting. The effect of repeatedly applying 

452 
@{text "(split thms)"} can be imitated by ``@{text "(simp only: 

453 
split: thms)"}''. 

454 

50063  455 
\medskip The @{text cong} modifiers add or delete Simplifier 
456 
congruence rules (see also \secref{sec:simprules}); the default is 

457 
to add. 

458 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

459 
\item @{method simp_all} is similar to @{method simp}, but acts on 
50063  460 
all goals, working backwards from the last to the first one as usual 
461 
in Isabelle.\footnote{The order is irrelevant for goals without 

462 
schematic variables, so simplification might actually be performed 

463 
in parallel here.} 

464 

465 
Chained facts are inserted into all subgoals, before the 

466 
simplification process starts. Further rule declarations are the 

467 
same as for @{method simp}. 

468 

469 
The proof method fails if all subgoals remain unchanged after 

470 
simplification. 

26782  471 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

472 
\end{description} 
26782  473 

50063  474 
By default the Simplifier methods above take local assumptions fully 
475 
into account, using equational assumptions in the subsequent 

476 
normalization process, or simplifying assumptions themselves. 

477 
Further options allow to finetune the behavior of the Simplifier 

478 
in this respect, corresponding to a variety of ML tactics as 

479 
follows.\footnote{Unlike the corresponding Isar proof methods, the 

480 
ML tactics do not insist in changing the goal state.} 

481 

482 
\begin{center} 

483 
\small 

50065  484 
\begin{supertabular}{llp{0.3\textwidth}} 
50063  485 
\hline 
486 
Isar method & ML tactic & behavior \\\hline 

487 

488 
@{text "(simp (no_asm))"} & @{ML simp_tac} & assumptions are ignored 

489 
completely \\\hline 

26782  490 

50063  491 
@{text "(simp (no_asm_simp))"} & @{ML asm_simp_tac} & assumptions 
492 
are used in the simplification of the conclusion but are not 

493 
themselves simplified \\\hline 

494 

495 
@{text "(simp (no_asm_use))"} & @{ML full_simp_tac} & assumptions 

496 
are simplified but are not used in the simplification of each other 

497 
or the conclusion \\\hline 

26782  498 

50063  499 
@{text "(simp)"} & @{ML asm_full_simp_tac} & assumptions are used in 
500 
the simplification of the conclusion and to simplify other 

501 
assumptions \\\hline 

502 

503 
@{text "(simp (asm_lr))"} & @{ML asm_lr_simp_tac} & compatibility 

504 
mode: an assumption is only used for simplifying assumptions which 

505 
are to the right of it \\\hline 

506 

50065  507 
\end{supertabular} 
50063  508 
\end{center} 
26782  509 
*} 
510 

511 

50064  512 
subsubsection {* Examples *} 
513 

514 
text {* We consider basic algebraic simplifications in Isabelle/HOL. 

515 
The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like 

516 
a good candidate to be solved by a single call of @{method simp}: 

517 
*} 

518 

519 
lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops 

520 

521 
text {* The above attempt \emph{fails}, because @{term "0"} and @{term 

522 
"op +"} in the HOL library are declared as generic type class 

523 
operations, without stating any algebraic laws yet. More specific 

524 
types are required to get access to certain standard simplifications 

525 
of the theory context, e.g.\ like this: *} 

526 

527 
lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp 

528 
lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp 

529 
lemma fixes x :: "'a :: monoid_add" shows "0 + (x + 0) = x + 0 + 0" by simp 

530 

531 
text {* 

532 
\medskip In many cases, assumptions of a subgoal are also needed in 

533 
the simplification process. For example: 

534 
*} 

535 

536 
lemma fixes x :: nat shows "x = 0 \<Longrightarrow> x + x = 0" by simp 

537 
lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops 

538 
lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp 

539 

540 
text {* As seen above, local assumptions that shall contribute to 

541 
simplification need to be part of the subgoal already, or indicated 

542 
explicitly for use by the subsequent method invocation. Both too 

543 
little or too much information can make simplification fail, for 

544 
different reasons. 

545 

546 
In the next example the malicious assumption @{prop "\<And>x::nat. f x = 

547 
g (f (g x))"} does not contribute to solve the problem, but makes 

548 
the default @{method simp} method loop: the rewrite rule @{text "f 

549 
?x \<equiv> g (f (g ?x))"} extracted from the assumption does not 

550 
terminate. The Simplifier notices certain simple forms of 

551 
nontermination, but not this one. The problem can be solved 

552 
nonetheless, by ignoring assumptions via special options as 

553 
explained before: 

554 
*} 

555 

556 
lemma "(\<And>x::nat. f x = g (f (g x))) \<Longrightarrow> f 0 = f 0 + 0" 

557 
by (simp (no_asm)) 

558 

559 
text {* The latter form is typical for long unstructured proof 

560 
scripts, where the control over the goal content is limited. In 

561 
structured proofs it is usually better to avoid pushing too many 

562 
facts into the goal state in the first place. Assumptions in the 

563 
Isar proof context do not intrude the reasoning if not used 

564 
explicitly. This is illustrated for a toplevel statement and a 

565 
local proof body as follows: 

566 
*} 

567 

568 
lemma 

569 
assumes "\<And>x::nat. f x = g (f (g x))" 

570 
shows "f 0 = f 0 + 0" by simp 

571 

572 
notepad 

573 
begin 

574 
assume "\<And>x::nat. f x = g (f (g x))" 

575 
have "f 0 = f 0 + 0" by simp 

576 
end 

577 

578 
text {* \medskip Because assumptions may simplify each other, there 

579 
can be very subtle cases of nontermination. For example, the regular 

580 
@{method simp} method applied to @{prop "P (f x) \<Longrightarrow> y = x \<Longrightarrow> f x = f y 

581 
\<Longrightarrow> Q"} gives rise to the infinite reduction sequence 

582 
\[ 

583 
@{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto} 

584 
@{text "P (f y)"} \stackrel{@{text "y \<equiv> x"}}{\longmapsto} 

585 
@{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto} \cdots 

586 
\] 

587 
whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> 

588 
Q"} terminates (without solving the goal): 

589 
*} 

590 

591 
lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q" 

592 
apply simp 

593 
oops 

594 

595 
text {* See also \secref{sec:simpconfig} for options to enable 

596 
Simplifier trace mode, which often helps to diagnose problems with 

597 
rewrite systems. 

598 
*} 

599 

600 

50063  601 
subsection {* Declaring rules \label{sec:simprules} *} 
26782  602 

603 
text {* 

604 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

605 
@{attribute_def simp} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

606 
@{attribute_def split} & : & @{text attribute} \\ 
50063  607 
@{attribute_def cong} & : & @{text attribute} \\ 
50077  608 
@{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
26782  609 
\end{matharray} 
610 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

611 
@{rail " 
50063  612 
(@@{attribute simp}  @@{attribute split}  @@{attribute cong}) 
613 
(()  'add'  'del') 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

614 
"} 
26782  615 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

616 
\begin{description} 
26782  617 

50076  618 
\item @{attribute simp} declares rewrite rules, by adding or 
50065  619 
deleting them from the simpset within the theory or proof context. 
50076  620 
Rewrite rules are theorems expressing some form of equality, for 
621 
example: 

622 

623 
@{text "Suc ?m + ?n = ?m + Suc ?n"} \\ 

624 
@{text "?P \<and> ?P \<longleftrightarrow> ?P"} \\ 

625 
@{text "?A \<union> ?B \<equiv> {x. x \<in> ?A \<or> x \<in> ?B}"} 

626 

627 
\smallskip 

628 
Conditional rewrites such as @{text "?m < ?n \<Longrightarrow> ?m div ?n = 0"} are 

629 
also permitted; the conditions can be arbitrary formulas. 

630 

631 
\medskip Internally, all rewrite rules are translated into Pure 

632 
equalities, theorems with conclusion @{text "lhs \<equiv> rhs"}. The 

633 
simpset contains a function for extracting equalities from arbitrary 

634 
theorems, which is usually installed when the objectlogic is 

635 
configured initially. For example, @{text "\<not> ?x \<in> {}"} could be 

636 
turned into @{text "?x \<in> {} \<equiv> False"}. Theorems that are declared as 

637 
@{attribute simp} and local assumptions within a goal are treated 

638 
uniformly in this respect. 

639 

640 
The Simplifier accepts the following formats for the @{text "lhs"} 

641 
term: 

642 

643 
\begin{enumerate} 

50065  644 

50076  645 
\item Firstorder patterns, considering the sublanguage of 
646 
application of constant operators to variable operands, without 

647 
@{text "\<lambda>"}abstractions or functional variables. 

648 
For example: 

649 

650 
@{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\ 

651 
@{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"} 

652 

653 
\item Higherorder patterns in the sense of \cite{nipkowpatterns}. 

654 
These are terms in @{text "\<beta>"}normal form (this will always be the 

655 
case unless you have done something strange) where each occurrence 

656 
of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the 

657 
@{text "x\<^sub>i"} are distinct bound variables. 

658 

659 
For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)"} 

660 
or its symmetric form, since the @{text "rhs"} is also a 

661 
higherorder pattern. 

662 

663 
\item Physical firstorder patterns over raw @{text "\<lambda>"}term 

664 
structure without @{text "\<alpha>\<beta>\<eta>"}equality; abstractions and bound 

665 
variables are treated like quasiconstant term material. 

666 

667 
For example, the rule @{text "?f ?x \<in> range ?f = True"} rewrites the 

668 
term @{text "g a \<in> range g"} to @{text "True"}, but will fail to 

669 
match @{text "g (h b) \<in> range (\<lambda>x. g (h x))"}. However, offending 

670 
subterms (in our case @{text "?f ?x"}, which is not a pattern) can 

671 
be replaced by adding new variables and conditions like this: @{text 

672 
"?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is acceptable as a conditional 

673 
rewrite rule of the second category since conditions can be 

674 
arbitrary terms. 

675 

676 
\end{enumerate} 

26782  677 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

678 
\item @{attribute split} declares case split rules. 
26782  679 

45645  680 
\item @{attribute cong} declares congruence rules to the Simplifier 
681 
context. 

682 

683 
Congruence rules are equalities of the form @{text [display] 

684 
"\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"} 

685 

686 
This controls the simplification of the arguments of @{text f}. For 

687 
example, some arguments can be simplified under additional 

688 
assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow> 

689 
(?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"} 

690 

691 
Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts 

692 
rewrite rules from it when simplifying @{text "?P\<^sub>2"}. Such local 

693 
assumptions are effective for rewriting formulae such as @{text "x = 

694 
0 \<longrightarrow> y + x = y"}. 

695 

696 
%FIXME 

697 
%The local assumptions are also provided as theorems to the solver; 

698 
%see \secref{sec:simpsolver} below. 

699 

700 
\medskip The following congruence rule for bounded quantifiers also 

701 
supplies contextual information  about the bound variable: 

702 
@{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow> 

703 
(\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"} 

704 

705 
\medskip This congruence rule for conditional expressions can 

706 
supply contextual information for simplifying the arms: 

707 
@{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow> 

708 
(if ?p then ?a else ?b) = (if ?q then ?c else ?d)"} 

709 

710 
A congruence rule can also \emph{prevent} simplification of some 

711 
arguments. Here is an alternative congruence rule for conditional 

712 
expressions that conforms to nonstrict functional evaluation: 

713 
@{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"} 

714 

715 
Only the first argument is simplified; the others remain unchanged. 

716 
This can make simplification much faster, but may require an extra 

717 
case split over the condition @{text "?q"} to prove the goal. 

50063  718 

50077  719 
\item @{command "print_simpset"} prints the collection of rules 
720 
declared to the Simplifier, which is also known as ``simpset'' 

721 
internally. 

722 

723 
For historical reasons, simpsets may occur independently from the 

724 
current context, but are conceptually dependent on it. When the 

725 
Simplifier is invoked via one of its main entry points in the Isar 

726 
source language (as proof method \secref{sec:simpmeth} or rule 

727 
attribute \secref{sec:simpmeth}), its simpset is derived from the 

728 
current proof context, and carries a backreference to that for 

729 
other tools that might get invoked internally (e.g.\ simplification 

730 
procedures \secref{sec:simproc}). A mismatch of the context of the 

731 
simpset and the context of the problem being simplified may lead to 

732 
unexpected results. 

733 

50063  734 
\end{description} 
50065  735 

736 
The implicit simpset of the theory context is propagated 

737 
monotonically through the theory hierarchy: forming a new theory, 

738 
the union of the simpsets of its imports are taken as starting 

739 
point. Also note that definitional packages like @{command 

740 
"datatype"}, @{command "primrec"}, @{command "fun"} routinely 

741 
declare Simplifier rules to the target context, while plain 

742 
@{command "definition"} is an exception in \emph{not} declaring 

743 
anything. 

744 

745 
\medskip It is up the user to manipulate the current simpset further 

746 
by explicitly adding or deleting theorems as simplification rules, 

747 
or installing other tools via simplification procedures 

748 
(\secref{sec:simproc}). Good simpsets are hard to design. Rules 

749 
that obviously simplify, like @{text "?n + 0 \<equiv> ?n"} are good 

750 
candidates for the implicit simpset, unless a special 

751 
nonnormalizing behavior of certain operations is intended. More 

752 
specific rules (such as distributive laws, which duplicate subterms) 

753 
should be added only for specific proof steps. Conversely, 

754 
sometimes a rule needs to be deleted just for some part of a proof. 

755 
The need of frequent additions or deletions may indicate a poorly 

756 
designed simpset. 

757 

758 
\begin{warn} 

759 
The union of simpsets from theory imports (as described above) is 

760 
not always a good starting point for the new theory. If some 

761 
ancestors have deleted simplification rules because they are no 

762 
longer wanted, while others have left those rules in, then the union 

763 
will contain the unwanted rules, and thus have to be deleted again 

764 
in the theory body. 

765 
\end{warn} 

45645  766 
*} 
767 

768 

50063  769 
subsection {* Configuration options \label{sec:simpconfig} *} 
770 

771 
text {* 

772 
\begin{tabular}{rcll} 

773 
@{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\ 

774 
@{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\ 

775 
@{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\ 

776 
@{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\ 

777 
\end{tabular} 

778 
\medskip 

779 

780 
These configurations options control further aspects of the Simplifier. 

781 
See also \secref{sec:config}. 

782 

783 
\begin{description} 

784 

785 
\item @{attribute simp_depth_limit} limits the number of recursive 

786 
invocations of the Simplifier during conditional rewriting. 

787 

788 
\item @{attribute simp_trace} makes the Simplifier output internal 

789 
operations. This includes rewrite steps, but also bookkeeping like 

790 
modifications of the simpset. 

791 

792 
\item @{attribute simp_trace_depth_limit} limits the effect of 

793 
@{attribute simp_trace} to the given depth of recursive Simplifier 

794 
invocations (when solving conditions of rewrite rules). 

795 

796 
\item @{attribute simp_debug} makes the Simplifier output some extra 

797 
information about internal operations. This includes any attempted 

798 
invocation of simplification procedures. 

799 

800 
\end{description} 

801 
*} 

802 

803 

804 
subsection {* Simplification procedures \label{sec:simproc} *} 

26782  805 

42925  806 
text {* Simplification procedures are ML functions that produce proven 
807 
rewrite rules on demand. They are associated with higherorder 

808 
patterns that approximate the lefthand sides of equations. The 

809 
Simplifier first matches the current redex against one of the LHS 

810 
patterns; if this succeeds, the corresponding ML function is 

811 
invoked, passing the Simplifier context and redex term. Thus rules 

812 
may be specifically fashioned for particular situations, resulting 

813 
in a more powerful mechanism than term rewriting by a fixed set of 

814 
rules. 

815 

816 
Any successful result needs to be a (possibly conditional) rewrite 

817 
rule @{text "t \<equiv> u"} that is applicable to the current redex. The 

818 
rule will be applied just as any ordinary rewrite rule. It is 

819 
expected to be already in \emph{internal form}, bypassing the 

820 
automatic preprocessing of objectlevel equivalences. 

821 

26782  822 
\begin{matharray}{rcl} 
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

823 
@{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

824 
simproc & : & @{text attribute} \\ 
26782  825 
\end{matharray} 
826 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

827 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

828 
@@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '') ')' '=' 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

829 
@{syntax text} \\ (@'identifier' (@{syntax nameref}+))? 
26782  830 
; 
831 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

832 
@@{attribute simproc} (('add' ':')?  'del' ':') (@{syntax name}+) 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

833 
"} 
26782  834 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

835 
\begin{description} 
26782  836 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

837 
\item @{command "simproc_setup"} defines a named simplification 
26782  838 
procedure that is invoked by the Simplifier whenever any of the 
839 
given term patterns match the current redex. The implementation, 

840 
which is provided as ML source text, needs to be of type @{ML_type 

841 
"morphism > simpset > cterm > thm option"}, where the @{ML_type 

842 
cterm} represents the current redex @{text r} and the result is 

843 
supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a 

844 
generalized version), or @{ML NONE} to indicate failure. The 

845 
@{ML_type simpset} argument holds the full context of the current 

846 
Simplifier invocation, including the actual Isar proof context. The 

847 
@{ML_type morphism} informs about the difference of the original 

848 
compilation context wrt.\ the one of the actual application later 

849 
on. The optional @{keyword "identifier"} specifies theorems that 

850 
represent the logical content of the abstract theory of this 

851 
simproc. 

852 

853 
Morphisms and identifiers are only relevant for simprocs that are 

854 
defined within a local target context, e.g.\ in a locale. 

855 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

856 
\item @{text "simproc add: name"} and @{text "simproc del: name"} 
26782  857 
add or delete named simprocs to the current Simplifier context. The 
858 
default is to add a simproc. Note that @{command "simproc_setup"} 

859 
already adds the new simproc to the subsequent context. 

860 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

861 
\end{description} 
26782  862 
*} 
863 

864 

42925  865 
subsubsection {* Example *} 
866 

867 
text {* The following simplification procedure for @{thm 

868 
[source=false, show_types] unit_eq} in HOL performs finegrained 

869 
control over rule application, beyond higherorder pattern matching. 

870 
Declaring @{thm unit_eq} as @{attribute simp} directly would make 

871 
the simplifier loop! Note that a version of this simplification 

872 
procedure is already active in Isabelle/HOL. *} 

873 

874 
simproc_setup unit ("x::unit") = {* 

875 
fn _ => fn _ => fn ct => 

876 
if HOLogic.is_unit (term_of ct) then NONE 

877 
else SOME (mk_meta_eq @{thm unit_eq}) 

878 
*} 

879 

880 
text {* Since the Simplifier applies simplification procedures 

881 
frequently, it is important to make the failure check in ML 

882 
reasonably fast. *} 

883 

884 

50079  885 
subsection {* Configurable Simplifier strategies \label{sec:simpstrategies} *} 
886 

887 
text {* The core termrewriting engine of the Simplifier is normally 

888 
used in combination with some addon components that modify the 

889 
strategy and allow to integrate other nonSimplifier proof tools. 

890 
These may be reconfigured in ML as explained below. Even if the 

891 
default strategies of objectlogics like Isabelle/HOL are used 

892 
unchanged, it helps to understand how the standard Simplifier 

893 
strategies work. *} 

894 

895 

896 
subsubsection {* The subgoaler *} 

897 

898 
text {* 

899 
\begin{mldecls} 

900 
@{index_ML Simplifier.set_subgoaler: "(simpset > int > tactic) > 

901 
simpset > simpset"} \\ 

902 
@{index_ML Simplifier.prems_of: "simpset > thm list"} \\ 

903 
\end{mldecls} 

904 

905 
The subgoaler is the tactic used to solve subgoals arising out of 

906 
conditional rewrite rules or congruence rules. The default should 

907 
be simplification itself. In rare situations, this strategy may 

908 
need to be changed. For example, if the premise of a conditional 

909 
rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \<Longrightarrow> 

910 
?m < ?n"}, the default strategy could loop. % FIXME !?? 

911 

912 
\begin{description} 

913 

914 
\item @{ML Simplifier.set_subgoaler}~@{text "ss tac"} sets the 

915 
subgoaler of simpset @{text "ss"} to @{text "tac"}. The tactic will 

916 
be applied to the context of the running Simplifier instance, 

917 
expressed as a simpset. 

918 

919 
\item @{ML Simplifier.prems_of}~@{text "ss"} retrieves the current 

920 
set of premises from simpset @{text "ss"} that represents the 

921 
context of the running Simplifier. This may be nonempty only if 

922 
the Simplifier has been told to utilize local assumptions in the 

923 
first place (cf.\ the options in \secref{sec:simpmeth}). 

924 

925 
\end{description} 

926 

927 
As an example, consider the following alternative subgoaler: 

928 
*} 

929 

930 
ML {* 

931 
fun subgoaler_tac ss = 

932 
assume_tac ORELSE' 

933 
resolve_tac (Simplifier.prems_of ss) ORELSE' 

934 
asm_simp_tac ss 

935 
*} 

936 

937 
text {* This tactic first tries to solve the subgoal by assumption or 

938 
by resolving with with one of the premises, calling simplification 

939 
only if that fails. *} 

940 

941 

942 
subsubsection {* The solver *} 

943 

944 
text {* 

945 
\begin{mldecls} 

946 
@{index_ML_type solver} \\ 

947 
@{index_ML Simplifier.mk_solver: "string > (simpset > int > tactic) > 

948 
solver"} \\ 

949 
@{index_ML_op setSolver: "simpset * solver > simpset"} \\ 

950 
@{index_ML_op addSolver: "simpset * solver > simpset"} \\ 

951 
@{index_ML_op setSSolver: "simpset * solver > simpset"} \\ 

952 
@{index_ML_op addSSolver: "simpset * solver > simpset"} \\ 

953 
\end{mldecls} 

954 

955 
A solver is a tactic that attempts to solve a subgoal after 

956 
simplification. Its core functionality is to prove trivial subgoals 

957 
such as @{prop "True"} and @{text "t = t"}, but objectlogics might 

958 
be more ambitious. For example, Isabelle/HOL performs a restricted 

959 
version of linear arithmetic here. 

960 

961 
Solvers are packaged up in abstract type @{ML_type solver}, with 

962 
@{ML Simplifier.mk_solver} as the only operation to create a solver. 

963 

964 
\medskip Rewriting does not instantiate unknowns. For example, 

965 
rewriting alone cannot prove @{text "a \<in> ?A"} since this requires 

966 
instantiating @{text "?A"}. The solver, however, is an arbitrary 

967 
tactic and may instantiate unknowns as it pleases. This is the only 

968 
way the Simplifier can handle a conditional rewrite rule whose 

969 
condition contains extra variables. When a simplification tactic is 

970 
to be combined with other provers, especially with the Classical 

971 
Reasoner, it is important whether it can be considered safe or not. 

972 
For this reason a simpset contains two solvers: safe and unsafe. 

973 

974 
The standard simplification strategy solely uses the unsafe solver, 

975 
which is appropriate in most cases. For special applications where 

976 
the simplification process is not allowed to instantiate unknowns 

977 
within the goal, simplification starts with the safe solver, but may 

978 
still apply the ordinary unsafe one in nested simplifications for 

979 
conditional rules or congruences. Note that in this way the overall 

980 
tactic is not totally safe: it may instantiate unknowns that appear 

981 
also in other subgoals. 

982 

983 
\begin{description} 

984 

985 
\item @{ML Simplifier.mk_solver}~@{text "name tac"} turns @{text 

986 
"tac"} into a solver; the @{text "name"} is only attached as a 

987 
comment and has no further significance. 

988 

989 
\item @{text "ss setSSolver solver"} installs @{text "solver"} as 

990 
the safe solver of @{text "ss"}. 

991 

992 
\item @{text "ss addSSolver solver"} adds @{text "solver"} as an 

993 
additional safe solver; it will be tried after the solvers which had 

994 
already been present in @{text "ss"}. 

995 

996 
\item @{text "ss setSolver solver"} installs @{text "solver"} as the 

997 
unsafe solver of @{text "ss"}. 

998 

999 
\item @{text "ss addSolver solver"} adds @{text "solver"} as an 

1000 
additional unsafe solver; it will be tried after the solvers which 

1001 
had already been present in @{text "ss"}. 

1002 

1003 
\end{description} 

1004 

1005 
\medskip The solver tactic is invoked with a simpset that represents 

1006 
the context of the running Simplifier. Further simpset operations 

1007 
may be used to retrieve relevant information, such as the list of 

1008 
local Simplifier premises via @{ML Simplifier.prems_of}  this 

1009 
list may be nonempty only if the Simplifier runs in a mode that 

1010 
utilizes local assumptions (see also \secref{sec:simpmeth}). The 

1011 
solver is also presented the full goal including its assumptions in 

1012 
any case. Thus it can use these (e.g.\ by calling @{ML 

1013 
assume_tac}), even if the Simplifier proper happens to ignore local 

1014 
premises at the moment. 

1015 

1016 
\medskip As explained before, the subgoaler is also used to solve 

1017 
the premises of congruence rules. These are usually of the form 

1018 
@{text "s = ?x"}, where @{text "s"} needs to be simplified and 

1019 
@{text "?x"} needs to be instantiated with the result. Typically, 

1020 
the subgoaler will invoke the Simplifier at some point, which will 

1021 
eventually call the solver. For this reason, solver tactics must be 

1022 
prepared to solve goals of the form @{text "t = ?x"}, usually by 

1023 
reflexivity. In particular, reflexivity should be tried before any 

1024 
of the fancy automated proof tools. 

1025 

1026 
It may even happen that due to simplification the subgoal is no 

1027 
longer an equality. For example, @{text "False \<longleftrightarrow> ?Q"} could be 

1028 
rewritten to @{text "\<not> ?Q"}. To cover this case, the solver could 

1029 
try resolving with the theorem @{text "\<not> False"} of the 

1030 
objectlogic. 

1031 

1032 
\medskip 

1033 

1034 
\begin{warn} 

1035 
If a premise of a congruence rule cannot be proved, then the 

1036 
congruence is ignored. This should only happen if the rule is 

1037 
\emph{conditional}  that is, contains premises not of the form 

1038 
@{text "t = ?x"}. Otherwise it indicates that some congruence rule, 

1039 
or possibly the subgoaler or solver, is faulty. 

1040 
\end{warn} 

1041 
*} 

1042 

1043 

1044 
subsubsection {* The looper *} 

1045 

1046 
text {* 

1047 
\begin{mldecls} 

1048 
@{index_ML_op setloop: "simpset * (int > tactic) > simpset"} \\ 

1049 
@{index_ML_op setloop': "simpset * (simpset > int > tactic) > simpset"} \\ 

1050 
@{index_ML_op addloop: "simpset * (string * (int > tactic)) > simpset"} \\ 

1051 
@{index_ML_op addloop': "simpset * (string * (simpset > int > tactic)) 

1052 
> simpset"} \\ 

1053 
@{index_ML_op delloop: "simpset * string > simpset"} \\ 

1054 
@{index_ML_op Splitter.add_split: "thm > simpset > simpset"} \\ 

1055 
@{index_ML_op Splitter.del_split: "thm > simpset > simpset"} \\ 

1056 
\end{mldecls} 

1057 

1058 
The looper is a list of tactics that are applied after 

1059 
simplification, in case the solver failed to solve the simplified 

1060 
goal. If the looper succeeds, the simplification process is started 

1061 
all over again. Each of the subgoals generated by the looper is 

1062 
attacked in turn, in reverse order. 

1063 

1064 
A typical looper is \emph{case splitting}: the expansion of a 

1065 
conditional. Another possibility is to apply an elimination rule on 

1066 
the assumptions. More adventurous loopers could start an induction. 

1067 

1068 
\begin{description} 

1069 

1070 
\item @{text "ss setloop tac"} installs @{text "tac"} as the only 

1071 
looper tactic of @{text "ss"}. The variant @{text "setloop'"} 

1072 
allows the tactic to depend on the running Simplifier context, which 

1073 
is represented as simpset. 

1074 

1075 
\item @{text "ss addloop (name, tac)"} adds @{text "tac"} as an 

1076 
additional looper tactic with name @{text "name"}, which is 

1077 
significant for managing the collection of loopers. The tactic will 

1078 
be tried after the looper tactics that had already been present in 

1079 
@{text "ss"}. The variant @{text "addloop'"} allows the tactic to 

1080 
depend on the running Simplifier context, which is represented as 

1081 
simpset. 

1082 

1083 
\item @{text "ss delloop name"} deletes the looper tactic that was 

1084 
associated with @{text "name"} from @{text "ss"}. 

1085 

1086 
\item @{ML Splitter.add_split}~@{text "thm ss"} adds split tactics 

1087 
for @{text "thm"} as additional looper tactics of @{text "ss"}. 

1088 

1089 
\item @{ML Splitter.del_split}~@{text "thm ss"} deletes the split 

1090 
tactic corresponding to @{text thm} from the looper tactics of 

1091 
@{text "ss"}. 

1092 

1093 
\end{description} 

1094 

1095 
The splitter replaces applications of a given function; the 

1096 
righthand side of the replacement can be anything. For example, 

1097 
here is a splitting rule for conditional expressions: 

1098 

1099 
@{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"} 

1100 

1101 
Another example is the elimination operator for Cartesian products 

1102 
(which happens to be called @{text split} in Isabelle/HOL: 

1103 

1104 
@{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"} 

1105 

1106 
For technical reasons, there is a distinction between case splitting 

1107 
in the conclusion and in the premises of a subgoal. The former is 

1108 
done by @{ML Splitter.split_tac} with rules like @{thm [source] 

1109 
split_if} or @{thm [source] option.split}, which do not split the 

1110 
subgoal, while the latter is done by @{ML Splitter.split_asm_tac} 

1111 
with rules like @{thm [source] split_if_asm} or @{thm [source] 

1112 
option.split_asm}, which split the subgoal. The function @{ML 

1113 
Splitter.add_split} automatically takes care of which tactic to 

1114 
call, analyzing the form of the rules given as argument; it is the 

1115 
same operation behind @{text "split"} attribute or method modifier 

1116 
syntax in the Isar source language. 

1117 

1118 
Case splits should be allowed only when necessary; they are 

1119 
expensive and hard to control. Casesplitting on ifexpressions in 

1120 
the conclusion is usually beneficial, so it is enabled by default in 

1121 
Isabelle/HOL and Isabelle/FOL/ZF. 

1122 

1123 
\begin{warn} 

1124 
With @{ML Splitter.split_asm_tac} as looper component, the 

1125 
Simplifier may split subgoals! This might cause unexpected problems 

1126 
in tactic expressions that silently assume 0 or 1 subgoals after 

1127 
simplification. 

1128 
\end{warn} 

1129 
*} 

1130 

1131 

50063  1132 
subsection {* Forward simplification \label{sec:simpforward} *} 
26782  1133 

1134 
text {* 

1135 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1136 
@{attribute_def simplified} & : & @{text attribute} \\ 
26782  1137 
\end{matharray} 
1138 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1139 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1140 
@@{attribute simplified} opt? @{syntax thmrefs}? 
26782  1141 
; 
1142 

40255
9ffbc25e1606
eliminated obsolete \_ escapes in rail environments;
wenzelm
parents:
35613
diff
changeset

1143 
opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use') ')' 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1144 
"} 
26782  1145 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

1146 
\begin{description} 
26782  1147 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

1148 
\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

1149 
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

1150 
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

1151 
The result is fully simplified by default, including assumptions and 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

1152 
conclusion; the options @{text no_asm} etc.\ tune the Simplifier in 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

1153 
the same way as the for the @{text simp} method. 
26782  1154 

1155 
Note that forward simplification restricts the simplifier to its 

1156 
most basic operation of term rewriting; solver and looper tactics 

50079  1157 
(\secref{sec:simpstrategies}) are \emph{not} involved here. The 
1158 
@{attribute simplified} attribute should be only rarely required 

1159 
under normal circumstances. 

26782  1160 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

1161 
\end{description} 
26782  1162 
*} 
1163 

1164 

27040  1165 
section {* The Classical Reasoner \label{sec:classical} *} 
26782  1166 

42930  1167 
subsection {* Basic concepts *} 
42927
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1168 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1169 
text {* Although Isabelle is generic, many users will be working in 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1170 
some extension of classical firstorder logic. Isabelle/ZF is built 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1171 
upon theory FOL, while Isabelle/HOL conceptually contains 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1172 
firstorder logic as a fragment. Theoremproving in predicate logic 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1173 
is undecidable, but many automated strategies have been developed to 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1174 
assist in this task. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1175 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1176 
Isabelle's classical reasoner is a generic package that accepts 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1177 
certain information about a logic and delivers a suite of automatic 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1178 
proof tools, based on rules that are classified and declared in the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1179 
context. These proof procedures are slow and simplistic compared 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1180 
with highend automated theorem provers, but they can save 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1181 
considerable time and effort in practice. They can prove theorems 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1182 
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

1183 
milliseconds (including full proof reconstruction): *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1184 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1185 
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

1186 
by blast 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1187 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1188 
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

1189 
by blast 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1190 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1191 
text {* The proof tools are generic. They are not restricted to 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1192 
firstorder logic, and have been heavily used in the development of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1193 
the Isabelle/HOL library and applications. The tactics can be 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1194 
traced, and their components can be called directly; in this manner, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1195 
any proof can be viewed interactively. *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1196 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1197 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1198 
subsubsection {* The sequent calculus *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1199 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1200 
text {* Isabelle supports natural deduction, which is easy to use for 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1201 
interactive proof. But natural deduction does not easily lend 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1202 
itself to automation, and has a bias towards intuitionism. For 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1203 
certain proofs in classical logic, it can not be called natural. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1204 
The \emph{sequent calculus}, a generalization of natural deduction, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1205 
is easier to automate. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1206 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1207 
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

1208 
and @{text "\<Delta>"} are sets of formulae.\footnote{For firstorder 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1209 
logic, sequents can equivalently be made from lists or multisets of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1210 
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

1211 
\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

1212 
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

1213 
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

1214 
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

1215 
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

1216 
valid. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1217 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1218 
Sequent rules are classified as \textbf{right} or \textbf{left}, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1219 
indicating which side of the @{text "\<turnstile>"} symbol they operate on. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1220 
Rules that operate on the right side are analogous to natural 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1221 
deduction's introduction rules, and left rules are analogous to 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1222 
elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1223 
is the rule 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1224 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1225 
\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

1226 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1227 
Applying the rule backwards, this breaks down some implication on 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1228 
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

1229 
the sets of formulae that are unaffected by the inference. The 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1230 
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

1231 
single rule 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1232 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1233 
\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

1234 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1235 
This breaks down some disjunction on the right side, replacing it by 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1236 
both disjuncts. Thus, the sequent calculus is a kind of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1237 
multipleconclusion logic. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1238 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1239 
To illustrate the use of multiple formulae on the right, let us 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1240 
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

1241 
backwards, we reduce this formula to a basic sequent: 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1242 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1243 
\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

1244 
{\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1245 
{\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1246 
{@{text "P, Q \<turnstile> Q, P"}}}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1247 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1248 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1249 
This example is typical of the sequent calculus: start with the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1250 
desired theorem and apply rules backwards in a fairly arbitrary 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1251 
manner. This yields a surprisingly effective proof procedure. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1252 
Quantifiers add only few complications, since Isabelle handles 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1253 
parameters and schematic variables. See \cite[Chapter 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1254 
10]{paulsonml2} for further discussion. *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1255 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1256 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1257 
subsubsection {* Simulating sequents by natural deduction *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1258 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1259 
text {* Isabelle can represent sequents directly, as in the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1260 
objectlogic LK. But natural deduction is easier to work with, and 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1261 
most objectlogics employ it. Fortunately, we can simulate the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1262 
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

1263 
@{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

1264 
the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1265 
Elimresolution plays a key role in simulating sequent proofs. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1266 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1267 
We can easily handle reasoning on the left. Elimresolution with 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1268 
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

1269 
a similar effect as the corresponding sequent rules. For the other 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1270 
connectives, we use sequentstyle elimination rules instead of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1271 
destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1272 
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

1273 
representation of sequents! 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1274 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1275 
\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

1276 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1277 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1278 
What about reasoning on the right? Introduction rules can only 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1279 
affect the formula in the conclusion, namely @{text "Q\<^sub>1"}. The 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1280 
other rightside formulae are represented as negated assumptions, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1281 
@{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

1282 
must first be exchanged with @{text "Q\<^sub>1"}. Elimresolution with the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1283 
@{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

1284 
