1 |
|
2 \chapter{The Classical Reasoner}\label{chap:classical} |
|
3 \index{classical reasoner|(} |
|
4 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}} |
|
5 |
|
6 \section{Classical rule sets} |
|
7 \index{classical sets} |
|
8 |
|
9 For elimination and destruction rules there are variants of the add operations |
|
10 adding a rule in a way such that it is applied only if also its second premise |
|
11 can be unified with an assumption of the current proof state: |
|
12 \indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2} |
|
13 \begin{ttbox} |
|
14 addSE2 : claset * (string * thm) -> claset \hfill{\bf infix 4} |
|
15 addSD2 : claset * (string * thm) -> claset \hfill{\bf infix 4} |
|
16 addE2 : claset * (string * thm) -> claset \hfill{\bf infix 4} |
|
17 addD2 : claset * (string * thm) -> claset \hfill{\bf infix 4} |
|
18 \end{ttbox} |
|
19 \begin{warn} |
|
20 A rule to be added in this special way must be given a name, which is used |
|
21 to delete it again -- when desired -- using \texttt{delSWrappers} or |
|
22 \texttt{delWrappers}, respectively. This is because these add operations |
|
23 are implemented as wrappers (see \ref{sec:modifying-search} below). |
|
24 \end{warn} |
|
25 |
|
26 |
|
27 \subsection{Modifying the search step} |
|
28 \label{sec:modifying-search} |
|
29 For a given classical set, the proof strategy is simple. Perform as many safe |
|
30 inferences as possible; or else, apply certain safe rules, allowing |
|
31 instantiation of unknowns; or else, apply an unsafe rule. The tactics also |
|
32 eliminate assumptions of the form $x=t$ by substitution if they have been set |
|
33 up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classical-setup} below). |
|
34 They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$ |
|
35 and~$P$, then replace $P\imp Q$ by~$Q$. |
|
36 |
|
37 The classical reasoning tactics --- except \texttt{blast_tac}! --- allow |
|
38 you to modify this basic proof strategy by applying two lists of arbitrary |
|
39 {\bf wrapper tacticals} to it. |
|
40 The first wrapper list, which is considered to contain safe wrappers only, |
|
41 affects \ttindex{safe_step_tac} and all the tactics that call it. |
|
42 The second one, which may contain unsafe wrappers, affects the unsafe parts |
|
43 of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them. |
|
44 A wrapper transforms each step of the search, for example |
|
45 by attempting other tactics before or after the original step tactic. |
|
46 All members of a wrapper list are applied in turn to the respective step tactic. |
|
47 |
|
48 Initially the two wrapper lists are empty, which means no modification of the |
|
49 step tactics. Safe and unsafe wrappers are added to a claset |
|
50 with the functions given below, supplying them with wrapper names. |
|
51 These names may be used to selectively delete wrappers. |
|
52 |
|
53 \begin{ttbox} |
|
54 type wrapper = (int -> tactic) -> (int -> tactic); |
|
55 |
|
56 addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4} |
|
57 addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
|
58 addSafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
|
59 delSWrapper : claset * string -> claset \hfill{\bf infix 4} |
|
60 |
|
61 addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4} |
|
62 addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
|
63 addafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
|
64 delWrapper : claset * string -> claset \hfill{\bf infix 4} |
|
65 |
|
66 addSss : claset * simpset -> claset \hfill{\bf infix 4} |
|
67 addss : claset * simpset -> claset \hfill{\bf infix 4} |
|
68 \end{ttbox} |
|
69 % |
|
70 |
|
71 \begin{ttdescription} |
|
72 \item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper} |
|
73 adds a new wrapper, which should yield a safe tactic, |
|
74 to modify the existing safe step tactic. |
|
75 |
|
76 \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore} |
|
77 adds the given tactic as a safe wrapper, such that it is tried |
|
78 {\em before} each safe step of the search. |
|
79 |
|
80 \item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter} |
|
81 adds the given tactic as a safe wrapper, such that it is tried |
|
82 when a safe step of the search would fail. |
|
83 |
|
84 \item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper} |
|
85 deletes the safe wrapper with the given name. |
|
86 |
|
87 \item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper} |
|
88 adds a new wrapper to modify the existing (unsafe) step tactic. |
|
89 |
|
90 \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore} |
|
91 adds the given tactic as an unsafe wrapper, such that it its result is |
|
92 concatenated {\em before} the result of each unsafe step. |
|
93 |
|
94 \item[$cs$ addafter $(name,tac)$] \indexbold{*addafter} |
|
95 adds the given tactic as an unsafe wrapper, such that it its result is |
|
96 concatenated {\em after} the result of each unsafe step. |
|
97 |
|
98 \item[$cs$ delWrapper $name$] \indexbold{*delWrapper} |
|
99 deletes the unsafe wrapper with the given name. |
|
100 |
|
101 \item[$cs$ addSss $ss$] \indexbold{*addss} |
|
102 adds the simpset~$ss$ to the classical set. The assumptions and goal will be |
|
103 simplified, in a rather safe way, after each safe step of the search. |
|
104 |
|
105 \item[$cs$ addss $ss$] \indexbold{*addss} |
|
106 adds the simpset~$ss$ to the classical set. The assumptions and goal will be |
|
107 simplified, before the each unsafe step of the search. |
|
108 |
|
109 \end{ttdescription} |
|
110 |
|
111 \index{simplification!from classical reasoner} |
|
112 Strictly speaking, the operators \texttt{addss} and \texttt{addSss} |
|
113 are not part of the classical reasoner. |
|
114 , which are used as primitives |
|
115 for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are |
|
116 implemented as wrapper tacticals. |
|
117 they |
|
118 \begin{warn} |
|
119 Being defined as wrappers, these operators are inappropriate for adding more |
|
120 than one simpset at a time: the simpset added last overwrites any earlier ones. |
|
121 When a simpset combined with a claset is to be augmented, this should done |
|
122 {\em before} combining it with the claset. |
|
123 \end{warn} |
|
124 |
|
125 |
|
126 \section{The classical tactics} |
|
127 |
|
128 \subsection{Other classical tactics} |
|
129 \begin{ttbox} |
|
130 slow_best_tac : claset -> int -> tactic |
|
131 \end{ttbox} |
|
132 |
|
133 \begin{ttdescription} |
|
134 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with |
|
135 best-first search to prove subgoal~$i$. |
|
136 \end{ttdescription} |
|
137 |
|
138 |
|
139 \subsection{Other useful tactics} |
|
140 \index{tactics!for contradiction} |
|
141 \index{tactics!for Modus Ponens} |
|
142 \begin{ttbox} |
|
143 contr_tac : int -> tactic |
|
144 mp_tac : int -> tactic |
|
145 eq_mp_tac : int -> tactic |
|
146 swap_res_tac : thm list -> int -> tactic |
|
147 \end{ttbox} |
|
148 These can be used in the body of a specialized search. |
|
149 \begin{ttdescription} |
|
150 \item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory} |
|
151 solves subgoal~$i$ by detecting a contradiction among two assumptions of |
|
152 the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The |
|
153 tactic can produce multiple outcomes, enumerating all possible |
|
154 contradictions. |
|
155 |
|
156 \item[\ttindexbold{mp_tac} {\it i}] |
|
157 is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in |
|
158 subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces |
|
159 $P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do |
|
160 nothing. |
|
161 |
|
162 \item[\ttindexbold{eq_mp_tac} {\it i}] |
|
163 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it |
|
164 is safe. |
|
165 |
|
166 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of |
|
167 the proof state using {\it thms}, which should be a list of introduction |
|
168 rules. First, it attempts to prove the goal using \texttt{assume_tac} or |
|
169 \texttt{contr_tac}. It then attempts to apply each rule in turn, attempting |
|
170 resolution and also elim-resolution with the swapped form. |
|
171 \end{ttdescription} |
|
172 |
|
173 |
|
174 \section{Setting up the classical reasoner}\label{sec:classical-setup} |
|
175 \index{classical reasoner!setting up} |
|
176 Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, |
|
177 have the classical reasoner already set up. |
|
178 When defining a new classical logic, you should set up the reasoner yourself. |
|
179 It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the |
|
180 argument signature \texttt{CLASSICAL_DATA}: |
|
181 \begin{ttbox} |
|
182 signature CLASSICAL_DATA = |
|
183 sig |
|
184 val mp : thm |
|
185 val not_elim : thm |
|
186 val swap : thm |
|
187 val sizef : thm -> int |
|
188 val hyp_subst_tacs : (int -> tactic) list |
|
189 end; |
|
190 \end{ttbox} |
|
191 Thus, the functor requires the following items: |
|
192 \begin{ttdescription} |
|
193 \item[\tdxbold{mp}] should be the Modus Ponens rule |
|
194 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. |
|
195 |
|
196 \item[\tdxbold{not_elim}] should be the contradiction rule |
|
197 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$. |
|
198 |
|
199 \item[\tdxbold{swap}] should be the swap rule |
|
200 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$. |
|
201 |
|
202 \item[\ttindexbold{sizef}] is the heuristic function used for best-first |
|
203 search. It should estimate the size of the remaining subgoals. A good |
|
204 heuristic function is \ttindex{size_of_thm}, which measures the size of the |
|
205 proof state. Another size function might ignore certain subgoals (say, |
|
206 those concerned with type-checking). A heuristic function might simply |
|
207 count the subgoals. |
|
208 |
|
209 \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in |
|
210 the hypotheses, typically created by \ttindex{HypsubstFun} (see |
|
211 Chapter~\ref{substitution}). This list can, of course, be empty. The |
|
212 tactics are assumed to be safe! |
|
213 \end{ttdescription} |
|
214 The functor is not at all sensitive to the formalization of the |
|
215 object-logic. It does not even examine the rules, but merely applies |
|
216 them according to its fixed strategy. The functor resides in {\tt |
|
217 Provers/classical.ML} in the Isabelle sources. |
|
218 |
|
219 \index{classical reasoner|)} |
|
220 |
|
221 %%% Local Variables: |
|
222 %%% mode: latex |
|
223 %%% TeX-master: "ref" |
|
224 %%% End: |
|