16 your successors who are going to maintain and modify it will\\ |
16 your successors who are going to maintain and modify it will\\ |
17 understand it.''}\\[1ex] |
17 understand it.''}\\[1ex] |
18 Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996. |
18 Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996. |
19 \end{flushright} |
19 \end{flushright} |
20 |
20 |
21 One of the main reason for descending to the ML-level of Isabelle is to be |
21 One of the main reason for descending to the ML-level of Isabelle is to |
22 able to implement automatic proof procedures. Such proof procedures can |
22 implement automatic proof procedures. Such proof procedures can |
23 considerably lessen the burden of manual reasoning. They are centred around |
23 considerably lessen the burden of manual reasoning. They are centred around |
24 the idea of refining a goal state using tactics. This is similar to the |
24 the idea of refining a goal state using tactics. This is similar to the |
25 \isacommand{apply}-style reasoning at the user-level, where goals are |
25 \isacommand{apply}-style reasoning at the user-level, where goals are |
26 modified in a sequence of proof steps until all of them are discharged. |
26 modified in a sequence of proof steps until all of them are discharged. |
27 In this chapter we will explain simple tactics and how to combine them using |
27 In this chapter we explain how to implement simple tactics and how to combine them using |
28 tactic combinators. We also describe the simplifier, simprocs and conversions. |
28 tactic combinators. We also describe the simplifier, simprocs and conversions. |
29 *} |
29 *} |
30 |
30 |
31 section {* Basics of Reasoning with Tactics\label{sec:basictactics}*} |
31 section {* Basics of Reasoning with Tactics\label{sec:basictactics}*} |
32 |
32 |
111 done |
111 done |
112 |
112 |
113 text {* |
113 text {* |
114 By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the |
114 By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the |
115 user-level of Isabelle the tactic @{ML foo_tac} or |
115 user-level of Isabelle the tactic @{ML foo_tac} or |
116 any other function that returns a tactic. There are some goal transformation |
116 any other function that returns a tactic. There are some goal transformations |
117 that are performed by @{text "tactic"}. They can be avoided by using |
117 that are performed by @{text "tactic"}. They can be avoided by using |
118 @{text "raw_tactic"} instead. |
118 @{text "raw_tactic"} instead. |
119 |
119 |
120 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed |
120 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed |
121 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} |
121 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} |
136 where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in |
136 where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in |
137 Tactical}. (For most combinators that combine tactics---@{ML THEN} is only |
137 Tactical}. (For most combinators that combine tactics---@{ML THEN} is only |
138 one such combinator---a ``primed'' version exists.) With @{ML foo_tac'} you |
138 one such combinator---a ``primed'' version exists.) With @{ML foo_tac'} you |
139 can give the number for the subgoal explicitly when the tactic is called. So |
139 can give the number for the subgoal explicitly when the tactic is called. So |
140 in the next proof you can first discharge the second subgoal, and |
140 in the next proof you can first discharge the second subgoal, and |
141 subsequently the first. |
141 then the first. |
142 *} |
142 *} |
143 |
143 |
144 lemma |
144 lemma |
145 shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1" |
145 shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1" |
146 and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2" |
146 and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2" |
150 |
150 |
151 text {* |
151 text {* |
152 This kind of addressing is more difficult to achieve when the goal is |
152 This kind of addressing is more difficult to achieve when the goal is |
153 hard-coded inside the tactic. |
153 hard-coded inside the tactic. |
154 |
154 |
155 The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for analysing |
155 The tactics @{ML foo_tac} and @{ML foo_tac'} are specific |
156 goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of |
156 to goals of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of |
157 this form, then these tactics return the error message:\footnote{To be |
157 this form, then these tactics return the error message:\footnote{To be |
158 precise, tactics do not produce this error message; the message originates from the |
158 precise, tactics do not produce this error message; the message originates from the |
159 \isacommand{apply} wrapper that calls the tactic.} |
159 \isacommand{apply} wrapper that calls the tactic.} |
160 |
160 |
161 |
161 |
171 |
171 |
172 ML %grayML{*type tactic = thm -> thm Seq.seq*} |
172 ML %grayML{*type tactic = thm -> thm Seq.seq*} |
173 |
173 |
174 text {* |
174 text {* |
175 By convention, if a tactic fails, then it should return the empty sequence. |
175 By convention, if a tactic fails, then it should return the empty sequence. |
176 Therefore, if you write your own tactics, they should not raise exceptions |
176 Therefore, your own tactics should not raise exceptions |
177 willy-nilly; only in very grave failure situations should a tactic raise the |
177 willy-nilly; only in very grave failure situations should a tactic raise the |
178 exception @{text THM}. |
178 exception @{text THM}. |
179 |
179 |
180 The simplest tactics are @{ML_ind no_tac in Tactical} and |
180 The simplest tactics are @{ML_ind no_tac in Tactical} and |
181 @{ML_ind all_tac in Tactical}. The first returns the empty sequence and |
181 @{ML_ind all_tac in Tactical}. The first returns the empty sequence and |
182 is defined as |
182 is defined as |