18537

1 


2 
(* $Id$ *)


3 


4 
theory tactic imports base begin


5 


6 
chapter {* Tactical theorem proving *}


7 


8 
text {* The basic idea of tactical theorem proving is to refine the


9 
initial claim in a backwards fashion, until a solved form is reached.


10 
An intermediate goal consists of several subgoals that need to be


11 
solved in order to achieve the main statement; zero subgoals means


12 
that the proof may be finished. Goal refinement operations are called


13 
tactics; combinators for composing tactics are called tacticals. *}


14 


15 


16 
section {* Goals \label{sec:tacticalgoals} *}


17 


18 
text {* Isabelle/Pure represents a goal\glossary{Tactical goal}{A


19 
theorem of \seeglossary{Horn Clause} form stating that a number of


20 
subgoals imply the main conclusion, which is marked as a protected


21 
proposition.} as a theorem stating that the subgoals imply the main


22 
goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}. The outermost goal


23 
structure is that of a Horn Clause\glossary{Horn Clause}{An iterated


24 
implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any


25 
outermost quantifiers. Strictly speaking, propositions @{text


26 
"A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits


27 
arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}


28 
connectives).}: an iterated implication without any


29 
quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is


30 
always represented via schematic variables in the body: @{text


31 
"\<phi>[?x]"}. These may get instantiated during the course of


32 
reasoning.}. For @{text "n = 0"} a goal is solved.


33 


34 
The structure of each subgoal @{text "A\<^sub>i"} is that of a general


35 
Heriditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow>


36 
\<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal form where any local


37 
@{text \<And>} is pulled before @{text \<Longrightarrow>}. Here @{text "x\<^sub>1, \<dots>,


38 
x\<^sub>k"} are goal parameters, i.e.\ arbitrarybutfixed entities of


39 
certain types, and @{text "H\<^sub>1, \<dots>, H\<^sub>m"} are goal


40 
hypotheses, i.e.\ facts that may be assumed locally. Together, this


41 
forms the goal context of the conclusion @{text B} to be established.


42 
The goal hypotheses may be again arbitrary Harrop Formulas, although


43 
the level of nesting rarely exceeds 12 in practice.


44 


45 
The main conclusion @{text C} is internally marked as a protected


46 
proposition\glossary{Protected proposition}{An arbitrarily structured


47 
proposition @{text "C"} which is forced to appear as atomic by


48 
wrapping it into a propositional identity operator; notation @{text


49 
"#C"}. Protecting a proposition prevents basic inferences from


50 
entering into that structure for the time being.}, which is


51 
occasionally represented explicitly by the notation @{text "#C"}.


52 
This ensures that the decomposition into subgoals and main conclusion


53 
is welldefined for arbitrarily structured claims.


54 


55 
\medskip Basic goal management is performed via the following


56 
Isabelle/Pure rules:


57 


58 
\[


59 
\infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad


60 
\infer[@{text "(finish)"}]{@{text "#C"}}{@{text "C"}}


61 
\]


62 


63 
\medskip The following lowlevel variants admit general reasoning


64 
with protected propositions:


65 


66 
\[


67 
\infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad


68 
\infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}


69 
\]


70 
*}


71 


72 
text %mlref {*


73 
\begin{mldecls}


74 
@{index_ML Goal.init: "cterm > thm"} \\


75 
@{index_ML Goal.finish: "thm > thm"} \\


76 
@{index_ML Goal.protect: "thm > thm"} \\


77 
@{index_ML Goal.conclude: "thm > thm"} \\


78 
\end{mldecls}


79 


80 
\begin{description}


81 


82 
\item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal with


83 
the typechecked proposition @{text \<phi>}.


84 


85 
\item @{ML "Goal.finish"}~@{text "th"} checks whether theorem @{text


86 
"th"} is a solved goal configuration (zero subgoals), and concludes


87 
the result by removing the goal protection.


88 


89 
\item @{ML "Goal.protect"}~@{text "th"} protects the whole statement


90 
of theorem @{text "th"}.


91 


92 
\item @{ML "Goal.conclude"}~@{text "th"} removes the goal protection


93 
for any number of pending subgoals.


94 


95 
\end{description}


96 
*}


97 


98 


99 
section {* Tactics *}


100 


101 
text {*


102 


103 
FIXME


104 


105 
\glossary{Tactic}{Any function that maps a \seeglossary{tactical goal}


106 
to a lazy sequence of possible sucessors. This scheme subsumes


107 
failure (empty result sequence), as well as lazy enumeration of proof


108 
search results. Error conditions are usually mapped to an empty


109 
result, which gives further tactics a chance to try in turn.


110 
Commonly, tactics either take an argument to address a particular


111 
subgoal, or operate on a certain range of subgoals in a uniform


112 
fashion. In any case, the main conclusion is normally left untouched,


113 
apart from instantiating \seeglossary{schematic variables}.}


114 


115 


116 
*}


117 


118 
section {* Tacticals *}


119 


120 
text {*


121 


122 
FIXME


123 


124 
\glossary{Tactical}{A functional combinator for building up complex


125 
tactics from simpler ones. Typical tactical perform sequential


126 
composition, disjunction (choice), iteration, or goal addressing.


127 
Various search strategies may be expressed via tacticals.}


128 


129 
*}


130 


131 
section {* Programmed proofs *}


132 


133 
text {*


134 
In order to perform a complete tactical proof under program control,


135 
one needs to set up an initial goal configuration, apply a tactic,


136 
and finish the result, cf.\ the rules given in


137 
\secref{sec:tacticalgoals}. Further checks are required to ensure


138 
that the result is actually an instance of the original claim 


139 
illbehaved tactics could have destroyed that information.


140 


141 
Several simultaneous claims may be handled within a single goal


142 
statement by using metalevel conjunction internally.\footnote{This


143 
is merely syntax for certain derived statements within


144 
Isabelle/Pure, there is no need to introduce a separate conjunction


145 
operator.} The whole configuration may be considered within a


146 
context of arbitrarybutfixed parameters and hypotheses, which will


147 
be available as local facts during the proof and discharged into


148 
implications in the result.


149 


150 
All of these administrative tasks are packaged into a separate


151 
operation, such that the user merely needs to provide the statement


152 
and tactic to be applied.


153 
*}


154 


155 
text %mlref {*


156 
\begin{mldecls}

20042

157 
@{index_ML Goal.prove: "Proof.context > string list > term list > term >

18537

158 
(thm list > tactic) > thm"} \\

20042

159 
@{index_ML Goal.prove_multi: "Proof.context > string list > term list > term list >

18537

160 
(thm list > tactic) > thm list"} \\

20042

161 
@{index_ML Goal.prove_global: "theory > string list > term list > term >


162 
(thm list > tactic) > thm"} \\

18537

163 
\end{mldecls}


164 


165 
\begin{description}


166 

20042

167 
\item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text

18537

168 
"C"} in the context of arbitrarybutfixed parameters @{text "xs"}


169 
and hypotheses @{text "As"} and applies tactic @{text "tac"} to


170 
solve it. The latter may depend on the local assumptions being


171 
presented as facts. The result is essentially @{text "\<And>xs. As \<Longrightarrow>


172 
C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}


173 
(the conclusion @{text "C"} itself may be a rule statement), turning


174 
the quantifier prefix into schematic variables, and generalizing


175 
implicit typevariables.


176 


177 
\item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but


178 
states several conclusions simultaneously. @{ML


179 
Tactic.conjunction_tac} may be used to split these into individual


180 
subgoals before commencing the actual proof.


181 

20042

182 
\item @{ML Goal.prove_global} is a degraded version of @{ML


183 
Goal.prove} for theory level goals; it includes a global @{ML


184 
Drule.standard} for the result.


185 

18537

186 
\end{description}


187 
*}


188 


189 
end


190 
