summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Isar_Ref/Proof_Script.thy

author | wenzelm |

Fri Nov 13 15:06:58 2015 +0100 (2015-11-13) | |

changeset 61657 | 5b878bc6ae98 |

parent 61656 | cfabbc083977 |

child 61866 | 6fa60a4f7e48 |

permissions | -rw-r--r-- |

tuned whitespace;

1 (*:maxLineLen=78:*)

3 theory Proof_Script

4 imports Base Main

5 begin

7 chapter \<open>Proof scripts\<close>

9 text \<open>

10 Interactive theorem proving is traditionally associated with ``proof

11 scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof

12 documents\<close> instead (see also \chref{ch:proofs}).

14 Nonetheless, it is possible to emulate proof scripts by sequential

15 refinements of a proof state in backwards mode, notably with the @{command

16 apply} command (see \secref{sec:tactic-commands}). There are also various

17 proof methods that allow to refer to implicit goal state information that is

18 normally not accessible to structured Isar proofs (see

19 \secref{sec:tactics}).

20 \<close>

23 section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>

25 text \<open>

26 \begin{matharray}{rcl}

27 @{command_def "supply"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\

28 @{command_def "apply"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\

29 @{command_def "apply_end"}\<open>\<^sup>*\<close> & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

30 @{command_def "done"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\

31 @{command_def "defer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\

32 @{command_def "prefer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\

33 @{command_def "back"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\

34 \end{matharray}

36 @{rail \<open>

37 @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')

38 ;

39 ( @@{command apply} | @@{command apply_end} ) @{syntax method}

40 ;

41 @@{command defer} @{syntax nat}?

42 ;

43 @@{command prefer} @{syntax nat}

44 \<close>}

46 \<^descr> @{command "supply"} supports fact definitions during goal refinement: it

47 is similar to @{command "note"}, but it operates in backwards mode and does

48 not have any impact on chained facts.

50 \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in initial position, but

51 unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus

52 consecutive method applications may be given just as in tactic scripts.

54 Facts are passed to \<open>m\<close> as indicated by the goal's forward-chain mode, and

55 are \<^emph>\<open>consumed\<close> afterwards. Thus any further @{command "apply"} command

56 would always work in a purely backward manner.

58 \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal

59 position. Basically, this simulates a multi-step tactic script for @{command

60 "qed"}, but may be given anywhere within the proof body.

62 No facts are passed to \<open>m\<close> here. Furthermore, the static context is that of

63 the enclosing goal (as for actual @{command "qed"}). Thus the proof method

64 may not refer to any assumptions introduced in the current body, for

65 example.

67 \<^descr> @{command "done"} completes a proof script, provided that the current goal

68 state is solved completely. Note that actual structured proof commands

69 (e.g.\ ``@{command "."}'' or @{command "sorry"}) may be used to conclude

70 proof scripts as well.

72 \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close> shuffle the list of

73 pending goals: @{command "defer"} puts off sub-goal \<open>n\<close> to the end of the

74 list (\<open>n = 1\<close> by default), while @{command "prefer"} brings sub-goal \<open>n\<close> to

75 the front.

77 \<^descr> @{command "back"} does back-tracking over the result sequence of the

78 latest proof command. Any proof command may return multiple results, and

79 this command explores the possibilities step-by-step. It is mainly useful

80 for experimentation and interactive exploration, and should be avoided in

81 finished proofs.

82 \<close>

85 section \<open>Explicit subgoal structure\<close>

87 text \<open>

88 \begin{matharray}{rcl}

89 @{command_def "subgoal"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\

90 \end{matharray}

92 @{rail \<open>

93 @@{command subgoal} @{syntax thmbind}? prems? params?

94 ;

95 prems: @'premises' @{syntax thmbind}?

96 ;

97 params: @'for' '\<dots>'? (('_' | @{syntax name})+)

98 \<close>}

100 \<^descr> @{command "subgoal"} allows to impose some structure on backward

101 refinements, to avoid proof scripts degenerating into long of @{command

102 apply} sequences.

104 The current goal state, which is essentially a hidden part of the Isar/VM

105 configurtation, is turned into a proof context and remaining conclusion.

106 This correponds to @{command fix}~/ @{command assume}~/ @{command show} in

107 structured proofs, but the text of the parameters, premises and conclusion

108 is not given explicitly.

110 Goal parameters may be specified separately, in order to allow referring to

111 them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x y z\<close>''

112 names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword "for"}~\<open>\<dots> x y z\<close>''

113 names a \<^emph>\<open>suffix\<close> of goal parameters. The latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol

114 as notation. Parameter positions may be skipped via dummies (underscore).

115 Unspecified names remain internal, and thus inaccessible in the proof text.

117 ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that goal

118 premises should be turned into assumptions of the context (otherwise the

119 remaining conclusion is a Pure implication). The fact name and attributes

120 are optional; the particular name ``\<open>prems\<close>'' is a common convention for the

121 premises of an arbitrary goal context in proof scripts.

123 ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result of a

124 proven subgoal. Thus it may be re-used in further reasoning, similar to the

125 result of @{command show} in structured Isar proofs.

128 Here are some abstract examples:

129 \<close>

131 lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"

132 and "\<And>u v. X u \<Longrightarrow> Y v"

133 subgoal sorry

134 subgoal sorry

135 done

137 lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"

138 and "\<And>u v. X u \<Longrightarrow> Y v"

139 subgoal for x y z sorry

140 subgoal for u v sorry

141 done

143 lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"

144 and "\<And>u v. X u \<Longrightarrow> Y v"

145 subgoal premises for x y z

146 using \<open>A x\<close> \<open>B y\<close>

147 sorry

148 subgoal premises for u v

149 using \<open>X u\<close>

150 sorry

151 done

153 lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"

154 and "\<And>u v. X u \<Longrightarrow> Y v"

155 subgoal r premises prems for x y z

156 proof -

157 have "A x" by (fact prems)

158 moreover have "B y" by (fact prems)

159 ultimately show ?thesis sorry

160 qed

161 subgoal premises prems for u v

162 proof -

163 have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)

164 moreover

165 have "X u" by (fact prems)

166 ultimately show ?thesis sorry

167 qed

168 done

170 lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"

171 subgoal premises prems for \<dots> z

172 proof -

173 from prems show "C z" sorry

174 qed

175 done

178 section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>

180 text \<open>

181 The following improper proof methods emulate traditional tactics. These

182 admit direct access to the goal state, which is normally considered harmful!

183 In particular, this may involve both numbered goal addressing (default 1),

184 and dynamic instantiation within the scope of some subgoal.

186 \begin{warn}

187 Dynamic instantiations refer to universally quantified parameters of a

188 subgoal (the dynamic context) rather than fixed variables and term

189 abbreviations of a (static) Isar context.

190 \end{warn}

192 Tactic emulation methods, unlike their ML counterparts, admit simultaneous

193 instantiation from both dynamic and static contexts. If names occur in both

194 contexts goal parameters hide locally fixed variables. Likewise, schematic

195 variables refer to term abbreviations, if present in the static context.

196 Otherwise the schematic variable is interpreted as a schematic variable and

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

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

200 consistently named \<open>foo_tac\<close>. Note also that variable names occurring on

201 left hand sides of instantiations must be preceded by a question mark if

202 they coincide with a keyword or contain dots. This is consistent with the

203 attribute @{attribute "where"} (see \secref{sec:pure-meth-att}).

205 \begin{matharray}{rcl}

206 @{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

207 @{method_def erule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

208 @{method_def drule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

209 @{method_def frule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

210 @{method_def cut_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

211 @{method_def thin_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

212 @{method_def subgoal_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

213 @{method_def rename_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

214 @{method_def rotate_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

215 @{method_def tactic}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

216 @{method_def raw_tactic}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\

217 \end{matharray}

219 @{rail \<open>

220 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |

221 @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>

222 (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )

223 ;

224 @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}

225 ;

226 @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}

227 ;

228 @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)

229 ;

230 @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?

231 ;

232 (@@{method tactic} | @@{method raw_tactic}) @{syntax text}

233 \<close>}

235 \<^descr> @{method rule_tac} etc. do resolution of rules with explicit

236 instantiation. This works the same way as the ML tactics @{ML

237 Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).

239 Multiple rules may be only given if there is no instantiation; then @{method

240 rule_tac} is the same as @{ML resolve_tac} in ML (see @{cite

241 "isabelle-implementation"}).

243 \<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a

244 subgoal; instantiations may be given as well. Note that the scope of

245 schematic variables is spread over the main goal statement and rule premises

246 are turned into new subgoals. This is in contrast to the regular method

247 @{method insert} which inserts closed rule statements.

249 \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise from a subgoal. Note

250 that \<open>\<phi>\<close> may contain schematic variables, to abbreviate the intended

251 proposition; the first matching subgoal premise will be deleted. Removing

252 useless premises from a subgoal increases its readability and can make

253 search tactics run faster.

255 \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as

256 local premises to a subgoal, and poses the same as new subgoals (in the

257 original context).

259 \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a goal according to

260 the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the \<^emph>\<open>suffix\<close> of variables.

262 \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a subgoal by \<open>n\<close>

263 positions: from right to left if \<open>n\<close> is positive, and from left to right if

264 \<open>n\<close> is negative; the default value is 1.

266 \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from any ML text of type

267 @{ML_type tactic}. Apart from the usual ML environment and the current proof

268 context, the ML code may refer to the locally bound values @{ML_text facts},

269 which indicates any current facts used for forward-chaining.

271 \<^descr> @{method raw_tactic} is similar to @{method tactic}, but presents the goal

272 state in its raw internal form, where simultaneous subgoals appear as

273 conjunction of the logical framework instead of the usual split into several

274 subgoals. While feature this is useful for debugging of complex method

275 definitions, it should not never appear in production theories.

276 \<close>

278 end