Subject: FormalContent

Keywords: ::Refiner
          ::tactic

Title: Tactic Expressions

--------------------------------------------------

Tactic is the type: proof -> (proof list # (proof list -> proof)).
We think of the proof list as the subgoals produced by the tactic
and the proof list -> proof function we call the validation which 
constructs a new proof structure whose leaves are the subgoals.
There are technical reasons to separate the production and construction
phases of tactic execution which are describe in more detail in the book.
Colloquially, we think of a tactic taking a goal, ie the sequent of a proof,
and producing a list of subgoals.

Functions which evaluate to a tactic when supplied with appropriate
arguments are called tactic functions. For example, the Hyp tactic
function when supplied with an interger argument has type tactic.
Tacticals are kinds of tactic functions which primarily combine tactics
to produce a single tactic. For example, the tactical THEN takes two
tactics and applies the first to the goal and then the second to each
of the resulting subgoals and returns the concatenation of the subgoals
produced by the second tactic. Even though a tactical is technically 
a tactic function, we normally reserve the phrase tactic function to refer
to functions that are not tacticals. Even so there are some tactic functions
which do take a tactic argument, but in such cases those tactics are
meant to finish the less interesting subgoals. The intent is that a
single tactic function progresses the proof in some non trivial way,
while tacticals combine the tactics to allow a proof or tactic author
to accomplish a larger more interesting step.    

A tactic expression is an ML expression of type tactic. In general
a tactic expression consists of a tree of tacticals and tactics. However,
any ML expression is allowed as long as it has type tactic.
Tactic expressions occur directly in proofs, but also in code to define
new tactics.

See Also Proofs as Data⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home