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

src/Doc/Isar_Ref/Proof_Script.thy

author | wenzelm |

Sun Feb 07 19:32:35 2016 +0100 (2016-02-07) | |

changeset 62269 | c56cff1c0e73 |

parent 61866 | 6fa60a4f7e48 |

child 62271 | 4cfe65cfd369 |

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

tuned;

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}).

18 There are also various proof methods that allow to refer to implicit goal

19 state information that is not accessible to structured Isar proofs (see

20 \secref{sec:tactics}). Note that the @{command subgoal}

21 (\secref{sec:subgoal}) command usually eliminates the need for implicit goal

22 state references.

23 \<close>

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

28 text \<open>

29 \begin{matharray}{rcl}

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

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

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

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

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

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

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

37 \end{matharray}

39 @{rail \<open>

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

41 ;

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

43 ;

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

45 ;

46 @@{command prefer} @{syntax nat}

47 \<close>}

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

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

51 not have any impact on chained facts.

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

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

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

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

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

59 would always work in a purely backward manner.

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

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

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

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

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

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

68 example.

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

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

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

73 proof scripts as well.

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

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

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

78 the front.

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

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

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

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

84 finished proofs.

85 \<close>

88 section \<open>Explicit subgoal structure \label{sec:subgoal}\<close>

90 text \<open>

91 \begin{matharray}{rcl}

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

93 \end{matharray}

95 @{rail \<open>

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

97 ;

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

99 ;

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

101 \<close>}

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

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

105 apply} sequences.

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

108 configuration, is turned into a proof context and remaining conclusion.

109 This corresponds to @{command fix}~/ @{command assume}~/ @{command show} in

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

111 is not given explicitly.

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

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

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

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

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

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

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

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

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

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

124 premises of an arbitrary goal context in proof scripts.

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

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

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

131 Here are some abstract examples:

132 \<close>

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

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

136 subgoal sorry

137 subgoal sorry

138 done

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

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

142 subgoal for x y z sorry

143 subgoal for u v sorry

144 done

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

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

148 subgoal premises for x y z

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

150 sorry

151 subgoal premises for u v

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

153 sorry

154 done

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

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

158 subgoal r premises prems for x y z

159 proof -

160 have "A x" by (fact prems)

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

162 ultimately show ?thesis sorry

163 qed

164 subgoal premises prems for u v

165 proof -

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

167 moreover

168 have "X u" by (fact prems)

169 ultimately show ?thesis sorry

170 qed

171 done

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

174 subgoal premises prems for \<dots> z

175 proof -

176 from prems show "C z" sorry

177 qed

178 done

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

183 text \<open>

184 The following improper proof methods emulate traditional tactics. These

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

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

187 and dynamic instantiation within the scope of some subgoal.

189 \begin{warn}

190 Dynamic instantiations refer to universally quantified parameters of a

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

192 abbreviations of a (static) Isar context.

193 \end{warn}

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

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

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

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

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

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

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

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

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

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

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

208 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

220 \end{matharray}

222 @{rail \<open>

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

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

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

226 ;

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

228 ;

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

230 ;

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

232 ;

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

234 ;

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

236 \<close>}

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

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

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

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

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

244 "isabelle-implementation"}).

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

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

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

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

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

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

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

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

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

256 search tactics run faster.

258 \<^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

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

260 original context).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

279 \<close>

281 end