author  wenzelm 
Sun, 26 Jan 2014 14:01:19 +0100  
changeset 55152  a56099a6447a 
parent 55112  b1a5d603fd12 
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} 

52060  34 
@{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\ 
26782  35 
\end{matharray} 
36 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

37 
@{rail \<open> 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

38 
@{syntax name} ('=' ('true'  'false'  @{syntax int}  @{syntax float}  @{syntax name}))? 
55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

39 
\<close>} 
26782  40 

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

41 
\begin{description} 
26782  42 

52060  43 
\item @{command "print_options"} prints the available configuration 
28760
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 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

73 
@{rail \<open> 
42596
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}? 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

80 
\<close>} 
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 no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\ 
26782  136 
\end{matharray} 
137 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

138 
@{rail \<open> 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

139 
@@{attribute tagged} @{syntax name} @{syntax name} 
26782  140 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

141 
@@{attribute untagged} @{syntax name} 
26782  142 
; 
48205  143 
@@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref} 
26782  144 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

145 
(@@{attribute unfolded}  @@{attribute folded}) @{syntax thmrefs} 
26782  146 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

147 
@@{attribute rotated} @{syntax int}? 
55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

148 
\<close>} 
26782  149 

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

150 
\begin{description} 
26782  151 

28764  152 
\item @{attribute tagged}~@{text "name value"} and @{attribute 
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

153 
untagged}~@{text name} add and remove \emph{tags} of some theorem. 
26782  154 
Tags may be any list of string pairs that serve as formal comment. 
28764  155 
The first string is considered the tag name, the second its value. 
156 
Note that @{attribute untagged} removes any tags of the same name. 

26782  157 

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

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

161 
\cite{isabelleimplementation}. 

26782  162 

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

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

164 
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

165 
definitions throughout a rule. 
26782  166 

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

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

170 
for objectlogic equality. 

171 

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

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

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

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

176 
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

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

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

180 
its own version of this operation. 

181 

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

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

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

185 
\end{description} 
26782  186 
*} 
187 

188 

27044  189 
subsection {* Lowlevel equational reasoning *} 
190 

191 
text {* 

192 
\begin{matharray}{rcl} 

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

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

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

195 
@{method_def split} & : & @{text method} \\ 
27044  196 
\end{matharray} 
197 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

198 
@{rail \<open> 
55029
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
52060
diff
changeset

199 
@@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref} 
27044  200 
; 
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

201 
@@{method split} @{syntax thmrefs} 
55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

202 
\<close>} 
27044  203 

204 
These methods provide lowlevel facilities for equational reasoning 

205 
that are intended for specialized applications only. Normally, 

206 
single step calculations would be performed in a structured text 

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

208 
provide the canonical way for automated normalization (see 

209 
\secref{sec:simplifier}). 

210 

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

211 
\begin{description} 
27044  212 

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

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

214 
using rule @{text eq}, which may be either a meta or object 
27044  215 
equality. 
216 

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

217 
\item @{method subst}~@{text "(asm) eq"} substitutes in an 
27044  218 
assumption. 
219 

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

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

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

224 
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

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

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

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

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

230 
assume all substitutions are performed simultaneously. Otherwise 

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

232 

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

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

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

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

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

27044  239 

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

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

243 

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

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

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

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

247 
structure of the rule. 
27044  248 

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

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

250 
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

251 
@{attribute split}, for example. 
27044  252 

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

253 
\end{description} 
27044  254 
*} 
255 

256 

26782  257 
subsection {* Further tactic emulations \label{sec:tactics} *} 
258 

259 
text {* 

260 
The following improper proof methods emulate traditional tactics. 

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

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

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

264 
scope of some subgoal. 

265 

266 
\begin{warn} 

267 
Dynamic instantiations refer to universally quantified parameters 

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

269 
term abbreviations of a (static) Isar context. 

270 
\end{warn} 

271 

272 
Tactic emulation methods, unlike their ML counterparts, admit 

273 
simultaneous instantiation from both dynamic and static contexts. 

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

275 
variables. Likewise, schematic variables refer to term 

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

277 
schematic variable is interpreted as a schematic variable and left 

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

279 

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

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

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

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

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

285 
\secref{sec:puremethatt}). 

286 

287 
\begin{matharray}{rcl} 

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

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

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

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

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

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

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

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

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

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

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

298 
@{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ 
26782  299 
\end{matharray} 
300 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

301 
@{rail \<open> 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

302 
(@@{method rule_tac}  @@{method erule_tac}  @@{method drule_tac}  
55029
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
52060
diff
changeset

303 
@@{method frule_tac}  @@{method cut_tac}  @@{method thin_tac}) @{syntax goal_spec}? \<newline> 
42617  304 
( dynamic_insts @'in' @{syntax thmref}  @{syntax thmrefs} ) 
26782  305 
; 
42705  306 
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

307 
; 
42705  308 
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +) 
26782  309 
; 
42705  310 
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}? 
26782  311 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

312 
(@@{method tactic}  @@{method raw_tactic}) @{syntax text} 
26782  313 
; 
314 

42617  315 
dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') 
55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

316 
\<close>} 
26782  317 

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

318 
\begin{description} 
26782  319 

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

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

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

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

30397  326 
\cite{isabelleimplementation}). 
26782  327 

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

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

329 
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

330 
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

331 
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

332 
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

333 
closed rule statements. 
26782  334 

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

337 
variables, to abbreviate the intended proposition; the first 

338 
matching subgoal premise will be deleted. Removing useless premises 

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

340 
run faster. 

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

341 

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

344 
as new subgoals (in the original context). 

26782  345 

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

346 
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

347 
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

348 
\emph{suffix} of variables. 
26782  349 

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

26782  352 
positive, and from left to right if @{text n} is negative; the 
46274  353 
default value is 1. 
26782  354 

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

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

359 
current facts used for forwardchaining. 

26782  360 

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

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

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

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

366 
appear in production theories. 

26782  367 

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

368 
\end{description} 
26782  369 
*} 
370 

371 

27040  372 
section {* The Simplifier \label{sec:simplifier} *} 
26782  373 

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

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

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

378 
There are several general hooks that allow to modify the 

379 
simplification strategy, or incorporate other proof tools that solve 

380 
subproblems, produce rewrite rules on demand etc. 

381 

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

384 
Conditions in conditional rewrite rules are solved recursively 

385 
before the rewrite rule is applied. 

386 

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

389 
engaging into the internal structures. Thus it serves as 

390 
generalpurpose proof tool with the main focus on equational 

50075  391 
reasoning, and a bit more than that. 
392 
*} 

50063  393 

394 

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

26782  396 

397 
text {* 

398 
\begin{matharray}{rcl} 

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

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

400 
@{method_def simp_all} & : & @{text method} \\ 
26782  401 
\end{matharray} 
402 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

403 
@{rail \<open> 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

404 
(@@{method simp}  @@{method simp_all}) opt? (@{syntax simpmod} * ) 
26782  405 
; 
406 

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

407 
opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use'  'asm_lr' ) ')' 
26782  408 
; 
50063  409 
@{syntax_def simpmod}: ('add'  'del'  'only'  'split' (()  'add'  'del')  
410 
'cong' (()  'add'  'del')) ':' @{syntax thmrefs} 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

411 
\<close>} 
26782  412 

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

413 
\begin{description} 
26782  414 

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

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

418 
The proof method fails if the subgoal remains unchanged after 

419 
simplification. 

26782  420 

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

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

424 
to extract rewrite rules from theorems, without further 

425 
simplification. This may lead to slightly different behavior in 

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

427 
boundary situations to perform the intended simplification step! 

428 

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

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

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

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

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

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

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

436 
compared to English! 

26782  437 

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

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

442 
ZF do this already). 

443 

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

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

447 
split: thms)"}''. 

448 

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

451 
to add. 

452 

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

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

456 
schematic variables, so simplification might actually be performed 

457 
in parallel here.} 

458 

459 
Chained facts are inserted into all subgoals, before the 

460 
simplification process starts. Further rule declarations are the 

461 
same as for @{method simp}. 

462 

463 
The proof method fails if all subgoals remain unchanged after 

464 
simplification. 

26782  465 

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

466 
\end{description} 
26782  467 

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

470 
normalization process, or simplifying assumptions themselves. 

471 
Further options allow to finetune the behavior of the Simplifier 

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

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

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

475 

476 
\begin{center} 

477 
\small 

50065  478 
\begin{supertabular}{llp{0.3\textwidth}} 
50063  479 
\hline 
480 
Isar method & ML tactic & behavior \\\hline 

481 

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

483 
completely \\\hline 

26782  484 

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

487 
themselves simplified \\\hline 

488 

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

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

491 
or the conclusion \\\hline 

26782  492 

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

495 
assumptions \\\hline 

496 

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

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

499 
are to the right of it \\\hline 

500 

50065  501 
\end{supertabular} 
50063  502 
\end{center} 
26782  503 
*} 
504 

505 

50064  506 
subsubsection {* Examples *} 
507 

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

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

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

511 
*} 

512 

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

514 

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

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

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

518 
types are required to get access to certain standard simplifications 

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

520 

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

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

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

524 

525 
text {* 

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

527 
the simplification process. For example: 

528 
*} 

529 

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

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

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

533 

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

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

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

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

538 
different reasons. 

539 

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

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

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

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

544 
terminate. The Simplifier notices certain simple forms of 

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

546 
nonetheless, by ignoring assumptions via special options as 

547 
explained before: 

548 
*} 

549 

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

551 
by (simp (no_asm)) 

552 

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

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

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

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

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

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

559 
local proof body as follows: 

560 
*} 

561 

562 
lemma 

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

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

565 

566 
notepad 

567 
begin 

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

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

570 
end 

571 

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

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

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

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

576 
\[ 

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

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

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

580 
\] 

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

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

583 
*} 

584 

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

586 
apply simp 

587 
oops 

588 

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

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

591 
rewrite systems. 

592 
*} 

593 

594 

50063  595 
subsection {* Declaring rules \label{sec:simprules} *} 
26782  596 

597 
text {* 

598 
\begin{matharray}{rcl} 

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

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

600 
@{attribute_def split} & : & @{text attribute} \\ 
50063  601 
@{attribute_def cong} & : & @{text attribute} \\ 
50077  602 
@{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
26782  603 
\end{matharray} 
604 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

605 
@{rail \<open> 
50063  606 
(@@{attribute simp}  @@{attribute split}  @@{attribute cong}) 
607 
(()  'add'  'del') 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

608 
\<close>} 
26782  609 

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

610 
\begin{description} 
26782  611 

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

616 

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

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

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

620 

621 
\smallskip 

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

623 
also permitted; the conditions can be arbitrary formulas. 

624 

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

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

627 
simpset contains a function for extracting equalities from arbitrary 

628 
theorems, which is usually installed when the objectlogic is 

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

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

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

632 
uniformly in this respect. 

633 

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

635 
term: 

636 

637 
\begin{enumerate} 

50065  638 

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

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

642 
For example: 

643 

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

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

646 

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

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

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

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

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

652 

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

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

655 
higherorder pattern. 

656 

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

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

659 
variables are treated like quasiconstant term material. 

660 

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

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

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

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

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

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

667 
rewrite rule of the second category since conditions can be 

668 
arbitrary terms. 

669 

670 
\end{enumerate} 

26782  671 

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

672 
\item @{attribute split} declares case split rules. 
26782  673 

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

676 

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

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

679 

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

681 
example, some arguments can be simplified under additional 

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

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

684 

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

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

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

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

689 

690 
%FIXME 

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

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

693 

694 
\medskip The following congruence rule for bounded quantifiers also 

695 
supplies contextual information  about the bound variable: 

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

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

698 

699 
\medskip This congruence rule for conditional expressions can 

700 
supply contextual information for simplifying the arms: 

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

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

703 

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

705 
arguments. Here is an alternative congruence rule for conditional 

706 
expressions that conforms to nonstrict functional evaluation: 

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

708 

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

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

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

50063  712 

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

715 
internally. 

716 

717 
For historical reasons, simpsets may occur independently from the 

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

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

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

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

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

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

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

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

726 
unexpected results. 

727 

50063  728 
\end{description} 
50065  729 

730 
The implicit simpset of the theory context is propagated 

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

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

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

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

735 
declare Simplifier rules to the target context, while plain 

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

737 
anything. 

738 

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

740 
by explicitly adding or deleting theorems as simplification rules, 

741 
or installing other tools via simplification procedures 

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

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

744 
candidates for the implicit simpset, unless a special 

745 
nonnormalizing behavior of certain operations is intended. More 

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

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

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

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

750 
designed simpset. 

751 

752 
\begin{warn} 

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

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

755 
ancestors have deleted simplification rules because they are no 

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

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

758 
in the theory body. 

759 
\end{warn} 

45645  760 
*} 
761 

762 

50080  763 
subsection {* Ordered rewriting with permutative rules *} 
764 

765 
text {* A rewrite rule is \emph{permutative} if the lefthand side and 

766 
righthand side are the equal up to renaming of variables. The most 

767 
common permutative rule is commutativity: @{text "?x + ?y = ?y + 

768 
?x"}. Other examples include @{text "(?x  ?y)  ?z = (?x  ?z)  

769 
?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y 

770 
(insert ?x ?A)"} for sets. Such rules are common enough to merit 

771 
special attention. 

772 

773 
Because ordinary rewriting loops given such rules, the Simplifier 

774 
employs a special strategy, called \emph{ordered rewriting}. 

775 
Permutative rules are detected and only applied if the rewriting 

776 
step decreases the redex wrt.\ a given term ordering. For example, 

777 
commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then 

778 
stops, because the redex cannot be decreased further in the sense of 

779 
the term ordering. 

780 

781 
The default is lexicographic ordering of term structure, but this 

782 
could be also changed locally for special applications via 

783 
@{index_ML Simplifier.set_termless} in Isabelle/ML. 

784 

785 
\medskip Permutative rewrite rules are declared to the Simplifier 

786 
just like other rewrite rules. Their special status is recognized 

787 
automatically, and their application is guarded by the term ordering 

788 
accordingly. *} 

789 

790 

791 
subsubsection {* Rewriting with AC operators *} 

792 

793 
text {* Ordered rewriting is particularly effective in the case of 

794 
associativecommutative operators. (Associativity by itself is not 

795 
permutative.) When dealing with an ACoperator @{text "f"}, keep 

796 
the following points in mind: 

797 

798 
\begin{itemize} 

799 

800 
\item The associative law must always be oriented from left to 

801 
right, namely @{text "f (f x y) z = f x (f y z)"}. The opposite 

802 
orientation, if used with commutativity, leads to looping in 

803 
conjunction with the standard term order. 

804 

805 
\item To complete your set of rewrite rules, you must add not just 

806 
associativity (A) and commutativity (C) but also a derived rule 

807 
\emph{leftcommutativity} (LC): @{text "f x (f y z) = f y (f x z)"}. 

808 

809 
\end{itemize} 

810 

811 
Ordered rewriting with the combination of A, C, and LC sorts a term 

812 
lexicographically  the rewriting engine imitates bubblesort. 

813 
*} 

814 

815 
locale AC_example = 

816 
fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<bullet>" 60) 

817 
assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)" 

818 
assumes commute: "x \<bullet> y = y \<bullet> x" 

819 
begin 

820 

821 
lemma left_commute: "x \<bullet> (y \<bullet> z) = y \<bullet> (x \<bullet> z)" 

822 
proof  

823 
have "(x \<bullet> y) \<bullet> z = (y \<bullet> x) \<bullet> z" by (simp only: commute) 

824 
then show ?thesis by (simp only: assoc) 

825 
qed 

826 

827 
lemmas AC_rules = assoc commute left_commute 

828 

829 
text {* Thus the Simplifier is able to establish equalities with 

830 
arbitrary permutations of subterms, by normalizing to a common 

831 
standard form. For example: *} 

832 

833 
lemma "(b \<bullet> c) \<bullet> a = xxx" 

834 
apply (simp only: AC_rules) 

835 
txt {* @{subgoals} *} 

836 
oops 

837 

838 
lemma "(b \<bullet> c) \<bullet> a = a \<bullet> (b \<bullet> c)" by (simp only: AC_rules) 

839 
lemma "(b \<bullet> c) \<bullet> a = c \<bullet> (b \<bullet> a)" by (simp only: AC_rules) 

840 
lemma "(b \<bullet> c) \<bullet> a = (c \<bullet> b) \<bullet> a" by (simp only: AC_rules) 

841 

842 
end 

843 

844 
text {* Martin and Nipkow \cite{martinnipkow} discuss the theory and 

845 
give many examples; other algebraic structures are amenable to 

846 
ordered rewriting, such as boolean rings. The BoyerMoore theorem 

847 
prover \cite{bm88book} also employs ordered rewriting. 

848 
*} 

849 

850 

851 
subsubsection {* Reorienting equalities *} 

852 

853 
text {* Another application of ordered rewriting uses the derived rule 

854 
@{thm [source] eq_commute}: @{thm [source = false] eq_commute} to 

855 
reverse equations. 

856 

857 
This is occasionally useful to reorient local assumptions according 

858 
to the term ordering, when other builtin mechanisms of 

859 
reorientation and mutual simplification fail to apply. *} 

860 

861 

50063  862 
subsection {* Configuration options \label{sec:simpconfig} *} 
863 

864 
text {* 

865 
\begin{tabular}{rcll} 

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

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

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

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

870 
\end{tabular} 

871 
\medskip 

872 

873 
These configurations options control further aspects of the Simplifier. 

874 
See also \secref{sec:config}. 

875 

876 
\begin{description} 

877 

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

879 
invocations of the Simplifier during conditional rewriting. 

880 

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

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

883 
modifications of the simpset. 

884 

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

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

887 
invocations (when solving conditions of rewrite rules). 

888 

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

890 
information about internal operations. This includes any attempted 

891 
invocation of simplification procedures. 

892 

893 
\end{description} 

894 
*} 

895 

896 

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

26782  898 

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

901 
patterns that approximate the lefthand sides of equations. The 

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

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

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

905 
may be specifically fashioned for particular situations, resulting 

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

907 
rules. 

908 

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

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

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

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

913 
automatic preprocessing of objectlevel equivalences. 

914 

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

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

917 
simproc & : & @{text attribute} \\ 
26782  918 
\end{matharray} 
919 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

920 
@{rail \<open> 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

921 
@@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '') ')' '=' 
55029
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
52060
diff
changeset

922 
@{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))? 
26782  923 
; 
924 

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

925 
@@{attribute simproc} (('add' ':')?  'del' ':') (@{syntax name}+) 
55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

926 
\<close>} 
26782  927 

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

928 
\begin{description} 
26782  929 

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

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

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

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

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

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

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

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

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

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

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

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

943 
represent the logical content of the abstract theory of this 

944 
simproc. 

945 

946 
Morphisms and identifiers are only relevant for simprocs that are 

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

948 

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

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

952 
already adds the new simproc to the subsequent context. 

953 

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

954 
\end{description} 
26782  955 
*} 
956 

957 

42925  958 
subsubsection {* Example *} 
959 

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

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

962 
control over rule application, beyond higherorder pattern matching. 

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

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

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

966 

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

968 
fn _ => fn _ => fn ct => 

969 
if HOLogic.is_unit (term_of ct) then NONE 

970 
else SOME (mk_meta_eq @{thm unit_eq}) 

971 
*} 

972 

973 
text {* Since the Simplifier applies simplification procedures 

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

975 
reasonably fast. *} 

976 

977 

50079  978 
subsection {* Configurable Simplifier strategies \label{sec:simpstrategies} *} 
979 

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

981 
used in combination with some addon components that modify the 

982 
strategy and allow to integrate other nonSimplifier proof tools. 

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

984 
default strategies of objectlogics like Isabelle/HOL are used 

985 
unchanged, it helps to understand how the standard Simplifier 

986 
strategies work. *} 

987 

988 

989 
subsubsection {* The subgoaler *} 

990 

991 
text {* 

992 
\begin{mldecls} 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

993 
@{index_ML Simplifier.set_subgoaler: "(Proof.context > int > tactic) > 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

994 
Proof.context > Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

995 
@{index_ML Simplifier.prems_of: "Proof.context > thm list"} \\ 
50079  996 
\end{mldecls} 
997 

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

999 
conditional rewrite rules or congruence rules. The default should 

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

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

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

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

1004 

1005 
\begin{description} 

1006 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1007 
\item @{ML Simplifier.set_subgoaler}~@{text "tac ctxt"} sets the 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1008 
subgoaler of the context to @{text "tac"}. The tactic will 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1009 
be applied to the context of the running Simplifier instance. 
50079  1010 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1011 
\item @{ML Simplifier.prems_of}~@{text "ctxt"} retrieves the current 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1012 
set of premises from the context. This may be nonempty only if 
50079  1013 
the Simplifier has been told to utilize local assumptions in the 
1014 
first place (cf.\ the options in \secref{sec:simpmeth}). 

1015 

1016 
\end{description} 

1017 

1018 
As an example, consider the following alternative subgoaler: 

1019 
*} 

1020 

1021 
ML {* 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1022 
fun subgoaler_tac ctxt = 
50079  1023 
assume_tac ORELSE' 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1024 
resolve_tac (Simplifier.prems_of ctxt) ORELSE' 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1025 
asm_simp_tac ctxt 
50079  1026 
*} 
1027 

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

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

1030 
only if that fails. *} 

1031 

1032 

1033 
subsubsection {* The solver *} 

1034 

1035 
text {* 

1036 
\begin{mldecls} 

1037 
@{index_ML_type solver} \\ 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1038 
@{index_ML Simplifier.mk_solver: "string > 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1039 
(Proof.context > int > tactic) > solver"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1040 
@{index_ML_op setSolver: "Proof.context * solver > Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1041 
@{index_ML_op addSolver: "Proof.context * solver > Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1042 
@{index_ML_op setSSolver: "Proof.context * solver > Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1043 
@{index_ML_op addSSolver: "Proof.context * solver > Proof.context"} \\ 
50079  1044 
\end{mldecls} 
1045 

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

1047 
simplification. Its core functionality is to prove trivial subgoals 

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

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

1050 
version of linear arithmetic here. 

1051 

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

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

1054 

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

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

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

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

1059 
way the Simplifier can handle a conditional rewrite rule whose 

1060 
condition contains extra variables. When a simplification tactic is 

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

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

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

1064 

1065 
The standard simplification strategy solely uses the unsafe solver, 

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

1067 
the simplification process is not allowed to instantiate unknowns 

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

1069 
still apply the ordinary unsafe one in nested simplifications for 

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

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

1072 
also in other subgoals. 

1073 

1074 
\begin{description} 

1075 

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

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

1078 
comment and has no further significance. 

1079 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1080 
\item @{text "ctxt setSSolver solver"} installs @{text "solver"} as 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1081 
the safe solver of @{text "ctxt"}. 
50079  1082 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1083 
\item @{text "ctxt addSSolver solver"} adds @{text "solver"} as an 
50079  1084 
additional safe solver; it will be tried after the solvers which had 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1085 
already been present in @{text "ctxt"}. 
50079  1086 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1087 
\item @{text "ctxt setSolver solver"} installs @{text "solver"} as the 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1088 
unsafe solver of @{text "ctxt"}. 
50079  1089 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1090 
\item @{text "ctxt addSolver solver"} adds @{text "solver"} as an 
50079  1091 
additional unsafe solver; it will be tried after the solvers which 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1092 
had already been present in @{text "ctxt"}. 
50079  1093 

1094 
\end{description} 

1095 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1096 
\medskip The solver tactic is invoked with the context of the 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1097 
running Simplifier. Further operations 
50079  1098 
may be used to retrieve relevant information, such as the list of 
1099 
local Simplifier premises via @{ML Simplifier.prems_of}  this 

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

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

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

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

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

1105 
premises at the moment. 

1106 

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

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

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

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

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

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

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

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

1115 
of the fancy automated proof tools. 

1116 

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

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

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

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

1121 
objectlogic. 

1122 

1123 
\medskip 

1124 

1125 
\begin{warn} 

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

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

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

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

1130 
or possibly the subgoaler or solver, is faulty. 

1131 
\end{warn} 

1132 
*} 

1133 

1134 

1135 
subsubsection {* The looper *} 

1136 

1137 
text {* 

1138 
\begin{mldecls} 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1139 
@{index_ML_op setloop: "Proof.context * 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1140 
(Proof.context > int > tactic) > Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1141 
@{index_ML_op addloop: "Proof.context * 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1142 
(string * (Proof.context > int > tactic)) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1143 
> Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1144 
@{index_ML_op delloop: "Proof.context * string > Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1145 
@{index_ML Splitter.add_split: "thm > Proof.context > Proof.context"} \\ 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1146 
@{index_ML Splitter.del_split: "thm > Proof.context > Proof.context"} \\ 
50079  1147 
\end{mldecls} 
1148 

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

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

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

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

1153 
attacked in turn, in reverse order. 

1154 

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

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

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

1158 

1159 
\begin{description} 

1160 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1161 
\item @{text "ctxt setloop tac"} installs @{text "tac"} as the only 
52037  1162 
looper tactic of @{text "ctxt"}. 
50079  1163 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1164 
\item @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an 
50079  1165 
additional looper tactic with name @{text "name"}, which is 
1166 
significant for managing the collection of loopers. The tactic will 

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

52037  1168 
@{text "ctxt"}. 
50079  1169 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1170 
\item @{text "ctxt delloop name"} deletes the looper tactic that was 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1171 
associated with @{text "name"} from @{text "ctxt"}. 
50079  1172 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1173 
\item @{ML Splitter.add_split}~@{text "thm ctxt"} adds split tactics 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1174 
for @{text "thm"} as additional looper tactics of @{text "ctxt"}. 
50079  1175 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1176 
\item @{ML Splitter.del_split}~@{text "thm ctxt"} deletes the split 
50079  1177 
tactic corresponding to @{text thm} from the looper tactics of 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

1178 
@{text "ctxt"}. 
50079  1179 

1180 
\end{description} 

1181 

1182 
The splitter replaces applications of a given function; the 

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

1184 
here is a splitting rule for conditional expressions: 

1185 

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

1187 

1188 
Another example is the elimination operator for Cartesian products 

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

1190 

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

1192 

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

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

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

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

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

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

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

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

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

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

1203 
syntax in the Isar source language. 

1204 

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

1206 
expensive and hard to control. Casesplitting on ifexpressions in 

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

1208 
Isabelle/HOL and Isabelle/FOL/ZF. 

1209 

1210 
\begin{warn} 

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

1212 
Simplifier may split subgoals! This might cause unexpected problems 

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

1214 
simplification. 

1215 
\end{warn} 

1216 
*} 

1217 

1218 

50063  1219 
subsection {* Forward simplification \label{sec:simpforward} *} 
26782  1220 

1221 
text {* 

1222 
\begin{matharray}{rcl} 

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

1223 
@{attribute_def simplified} & : & @{text attribute} \\ 
26782  1224 
\end{matharray} 
1225 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

1226 
@{rail \<open> 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1227 
@@{attribute simplified} opt? @{syntax thmrefs}? 
26782  1228 
; 
1229 

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

1230 
opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use') ')' 
55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
55029
diff
changeset

1231 
\<close>} 
26782  1232 

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

1233 
\begin{description} 
26782  1234 

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

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

1236 
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

1237 
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

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

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

1240 
the same way as the for the @{text simp} method. 
26782  1241 

1242 
Note that forward simplification restricts the simplifier to its 

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

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

1246 
under normal circumstances. 

26782  1247 

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

1248 
\end{description} 
26782  1249 
*} 
1250 

1251 

27040  1252 
section {* The Classical Reasoner \label{sec:classical} *} 
26782  1253 

42930  1254 
subsection {* Basic concepts *} 
42927
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 
text {* Although Isabelle is generic, many users will be working in 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

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

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

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

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

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

1262 

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

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

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

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

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

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

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

1269 
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

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

1271 

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

1272 
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

1273 
by blast 
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 
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

1276 
by blast 
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 
text {* The proof tools are generic. They are not restricted to 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

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

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

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

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

1283 

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

1284 

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

1285 
subsubsection {* The sequent calculus *} 