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

src/Doc/Isar_Ref/Proof_Script.thy

author | wenzelm |

Mon Jun 15 14:10:41 2015 +0200 (2015-06-15) | |

changeset 60484 | 98ee86354354 |

child 60631 | 441fdbfbb2d3 |

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

moved sections;

1 theory Proof_Script

2 imports Base Main

3 begin

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

7 text \<open>

8 Interactive theorem proving is traditionally associated with ``proof

9 scripts'', but Isabelle/Isar is centered around structured \emph{proof

10 documents} instead (see also \chref{ch:proofs}).

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

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

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

15 proof methods that allow to refer to implicit goal state information that

16 is normally not accessible to structured Isar proofs (see

17 \secref{sec:tactics}).

18 \<close>

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

23 text \<open>

24 \begin{matharray}{rcl}

25 @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

26 @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

27 @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

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

29 @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

30 @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

31 @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

32 \end{matharray}

34 @{rail \<open>

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

36 ;

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

38 ;

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

40 ;

41 @@{command prefer} @{syntax nat}

42 \<close>}

44 \begin{description}

46 \item @{command "supply"} supports fact definitions during goal

47 refinement: it is similar to @{command "note"}, but it operates in

48 backwards mode and does not have any impact on chained facts.

50 \item @{command "apply"}~@{text m} applies proof method @{text m} in

51 initial position, but unlike @{command "proof"} it retains ``@{text

52 "proof(prove)"}'' mode. Thus consecutive method applications may be

53 given just as in tactic scripts.

55 Facts are passed to @{text m} as indicated by the goal's

56 forward-chain mode, and are \emph{consumed} afterwards. Thus any

57 further @{command "apply"} command would always work in a purely

58 backward manner.

60 \item @{command "apply_end"}~@{text "m"} applies proof method @{text

61 m} as if in terminal position. Basically, this simulates a

62 multi-step tactic script for @{command "qed"}, but may be given

63 anywhere within the proof body.

65 No facts are passed to @{text m} here. Furthermore, the static

66 context is that of the enclosing goal (as for actual @{command

67 "qed"}). Thus the proof method may not refer to any assumptions

68 introduced in the current body, for example.

70 \item @{command "done"} completes a proof script, provided that the

71 current goal state is solved completely. Note that actual

72 structured proof commands (e.g.\ ``@{command "."}'' or @{command

73 "sorry"}) may be used to conclude proof scripts as well.

75 \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}

76 shuffle the list of pending goals: @{command "defer"} puts off

77 sub-goal @{text n} to the end of the list (@{text "n = 1"} by

78 default), while @{command "prefer"} brings sub-goal @{text n} to the

79 front.

81 \item @{command "back"} does back-tracking over the result sequence

82 of the latest proof command. Any proof command may return multiple

83 results, and this command explores the possibilities step-by-step.

84 It is mainly useful for experimentation and interactive exploration,

85 and should be avoided in finished proofs.

87 \end{description}

88 \<close>

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

93 text \<open>

94 The following improper proof methods emulate traditional tactics.

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

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

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

98 scope of some subgoal.

100 \begin{warn}

101 Dynamic instantiations refer to universally quantified parameters

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

103 term abbreviations of a (static) Isar context.

104 \end{warn}

106 Tactic emulation methods, unlike their ML counterparts, admit

107 simultaneous instantiation from both dynamic and static contexts.

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

109 variables. Likewise, schematic variables refer to term

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

111 schematic variable is interpreted as a schematic variable and left

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

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

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

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

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

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

119 \secref{sec:pure-meth-att}).

121 \begin{matharray}{rcl}

122 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\

123 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\

124 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\

125 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\

126 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\

127 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\

128 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\

129 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\

130 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\

131 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\

132 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\

133 \end{matharray}

135 @{rail \<open>

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

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

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

139 ;

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

141 ;

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

143 ;

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

145 ;

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

147 ;

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

149 \<close>}

151 \begin{description}

153 \item @{method rule_tac} etc. do resolution of rules with explicit

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

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

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

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

159 @{cite "isabelle-implementation"}).

161 \item @{method cut_tac} inserts facts into the proof state as

162 assumption of a subgoal; instantiations may be given as well. Note

163 that the scope of schematic variables is spread over the main goal

164 statement and rule premises are turned into new subgoals. This is

165 in contrast to the regular method @{method insert} which inserts

166 closed rule statements.

168 \item @{method thin_tac}~@{text \<phi>} deletes the specified premise

169 from a subgoal. Note that @{text \<phi>} may contain schematic

170 variables, to abbreviate the intended proposition; the first

171 matching subgoal premise will be deleted. Removing useless premises

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

173 run faster.

175 \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions

176 @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same

177 as new subgoals (in the original context).

179 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a

180 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the

181 \emph{suffix} of variables.

183 \item @{method rotate_tac}~@{text n} rotates the premises of a

184 subgoal by @{text n} positions: from right to left if @{text n} is

185 positive, and from left to right if @{text n} is negative; the

186 default value is 1.

188 \item @{method tactic}~@{text "text"} produces a proof method from

189 any ML text of type @{ML_type tactic}. Apart from the usual ML

190 environment and the current proof context, the ML code may refer to

191 the locally bound values @{ML_text facts}, which indicates any

192 current facts used for forward-chaining.

194 \item @{method raw_tactic} is similar to @{method tactic}, but

195 presents the goal state in its raw internal form, where simultaneous

196 subgoals appear as conjunction of the logical framework instead of

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

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

199 appear in production theories.

201 \end{description}

202 \<close>

204 end