summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 26 Jan 2012 22:16:45 +0100 | |

changeset 46269 | e75181672150 |

parent 46268 | 45ce067a7562 |

child 46270 | 4ab175c85d57 |

updated "Control and search tacticals" (moved from ref to implementation);
discontinued odd trace flags that assume sequential TTY loop;
discontinued obscure DETERM_UNTIL_SOLVED;
discontinued obsolete chapter "Tacticals" (ref);

doc-src/IsarImplementation/Thy/Tactic.thy | file | annotate | diff | comparison | revisions | |

doc-src/IsarImplementation/Thy/document/Tactic.tex | file | annotate | diff | comparison | revisions | |

doc-src/Ref/Makefile | file | annotate | diff | comparison | revisions | |

doc-src/Ref/ref.tex | file | annotate | diff | comparison | revisions | |

doc-src/Ref/tctical.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 21:25:18 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 22:16:45 2012 +0100 @@ -404,9 +404,7 @@ sequential composition, disjunctive choice, iteration, or goal addressing. Various search strategies may be expressed via tacticals. - - \medskip The chapter on tacticals in old \cite{isabelle-ref} is - still applicable for further details. *} +*} subsection {* Combining tactics *} @@ -438,13 +436,13 @@ \begin{description} \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential - composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a - proof state, it returns all states reachable in two steps by - applying @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it - applies @{text "tac\<^sub>1"} to the proof state, getting a sequence of - possible next states; then, it applies @{text "tac\<^sub>2"} to each of - these and concatenates the results to produce again one flat - sequence of states. + composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a goal + state, it returns all states reachable in two steps by applying + @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it applies @{text + "tac\<^sub>1"} to the goal state, getting a sequence of possible next + states; then, it applies @{text "tac\<^sub>2"} to each of these and + concatenates the results to produce again one flat sequence of + states. \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it @@ -497,7 +495,7 @@ \begin{description} - \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the proof + \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal state and returns the resulting sequence, if non-empty; otherwise it returns the original state. Thus, it applies @{text "tac"} at most once. @@ -506,7 +504,7 @@ applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text "tac"}. There is no need for @{verbatim TRY'}. - \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the proof + \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal state and, recursively, to each element of the resulting sequence. The resulting sequence consists of those states that make @{text "tac"} fail. Thus, it applies @{text "tac"} as many times as @@ -519,7 +517,7 @@ is impossible. \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the - proof state and, recursively, to the head of the resulting sequence. + goal state and, recursively, to the head of the resulting sequence. It returns the first state to make @{text "tac"} fail. It is deterministic, discarding alternative outcomes. @@ -561,7 +559,7 @@ possible in each outcome. \begin{warn} - Note the explicit abstraction over the proof state in the ML + Note the explicit abstraction over the goal state in the ML definition of @{ML REPEAT}. Recursive tacticals must be coded in this awkward fashion to avoid infinite recursion of eager functional evaluation in Standard ML. The following attempt would make @{ML @@ -632,4 +630,177 @@ \end{description} *} + +subsection {* Control and search tacticals *} + +text {* A predicate on theorems @{ML_type "thm -> bool"} can test + whether a goal state enjoys some desirable property --- such as + having no subgoals. Tactics that search for satisfactory goal + states are easy to express. The main search procedures, + depth-first, breadth-first and best-first, are provided as + tacticals. They generate the search tree by repeatedly applying a + given tactic. *} + + +subsubsection {* Filtering a tactic's results *} + +text {* + \begin{mldecls} + @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\ + @{index_ML CHANGED: "tactic -> tactic"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the + goal state and returns a sequence consisting of those result goal + states that are satisfactory in the sense of @{text "sat"}. + + \item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal + state and returns precisely those states that differ from the + original state (according to @{ML Thm.eq_thm}). Thus @{ML + CHANGED}~@{text "tac"} always has some effect on the state. + + \end{description} +*} + + +subsubsection {* Depth-first search *} + +text {* + \begin{mldecls} + @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ + @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\ + @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if + @{text "sat"} returns true. Otherwise it applies @{text "tac"}, + then recursively searches from each element of the resulting + sequence. The code uses a stack for efficiency, in effect applying + @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to + the state. + + \item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to + search for states having no subgoals. + + \item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to + search for states having fewer subgoals than the given state. Thus, + it insists upon solving at least one subgoal. + + \end{description} +*} + + +subsubsection {* Other search strategies *} + +text {* + \begin{mldecls} + @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ + @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ + @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ + \end{mldecls} + + These search strategies will find a solution if one exists. + However, they do not enumerate all solutions; they terminate after + the first satisfactory result from @{text "tac"}. + + \begin{description} + + \item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first + search to find states for which @{text "sat"} is true. For most + applications, it is too slow. + + \item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic + search, using @{text "dist"} to estimate the distance from a + satisfactory state (in the sense of @{text "sat"}). It maintains a + list of states ordered by distance. It applies @{text "tac"} to the + head of this list; if the result contains any satisfactory states, + then it returns them. Otherwise, @{ML BEST_FIRST} adds the new + states to the list, and continues. + + The distance function is typically @{ML size_of_thm}, which computes + the size of the state. The smaller the state, the fewer and simpler + subgoals it has. + + \item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like + @{ML BEST_FIRST}, except that the priority queue initially contains + the result of applying @{text "tac\<^sub>0"} to the goal state. This + tactical permits separate tactics for starting the search and + continuing the search. + + \end{description} +*} + + +subsubsection {* Auxiliary tacticals for searching *} + +text {* + \begin{mldecls} + @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\ + @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\ + @{index_ML SOLVE: "tactic -> tactic"} \\ + @{index_ML DETERM: "tactic -> tactic"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to + the goal state if it satisfies predicate @{text "sat"}, and applies + @{text "tac\<^sub>2"}. It is a conditional tactical in that only one of + @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state. + However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated + because ML uses eager evaluation. + + \item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the + goal state if it has any subgoals, and simply returns the goal state + otherwise. Many common tactics, such as @{ML resolve_tac}, fail if + applied to a goal state that has no subgoals. + + \item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal + state and then fails iff there are subgoals left. + + \item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal + state and returns the head of the resulting sequence. @{ML DETERM} + limits the search space by making its argument deterministic. + + \end{description} +*} + + +subsubsection {* Predicates and functions useful for searching *} + +text {* + \begin{mldecls} + @{index_ML has_fewer_prems: "int -> thm -> bool"} \\ + @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\ + @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\ + @{index_ML size_of_thm: "thm -> int"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text + "thm"} has fewer than @{text "n"} premises. + + \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text + "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have + compatible background theories. Both theorems must have the same + conclusions, the same set of hypotheses, and the same set of sort + hypotheses. Names of bound variables are ignored as usual. + + \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether + the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. + Names of bound variables are ignored. + + \item @{ML size_of_thm}~@{text "thm"} computes the size of @{text + "thm"}, namely the number of variables, constants and abstractions + in its conclusion. It may serve as a distance function for + @{ML BEST_FIRST}. + + \end{description} +*} + end

--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 21:25:18 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 22:16:45 2012 +0100 @@ -480,10 +480,7 @@ complex tactics from simpler ones. Common tacticals perform sequential composition, disjunctive choice, iteration, or goal addressing. Various search strategies may be expressed via - tacticals. - - \medskip The chapter on tacticals in old \cite{isabelle-ref} is - still applicable for further details.% + tacticals.% \end{isamarkuptext}% \isamarkuptrue% % @@ -525,13 +522,12 @@ \begin{description} \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential - composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a - proof state, it returns all states reachable in two steps by - applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it - applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the proof state, getting a sequence of - possible next states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of - these and concatenates the results to produce again one flat - sequence of states. + composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a goal + state, it returns all states reachable in two steps by applying + \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the goal state, getting a sequence of possible next + states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and + concatenates the results to produce again one flat sequence of + states. \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it @@ -596,7 +592,7 @@ \begin{description} - \item \verb|TRY|~\isa{tac} applies \isa{tac} to the proof + \item \verb|TRY|~\isa{tac} applies \isa{tac} to the goal state and returns the resulting sequence, if non-empty; otherwise it returns the original state. Thus, it applies \isa{tac} at most once. @@ -604,7 +600,7 @@ Note that for tactics with subgoal addressing, the combinator can be applied via functional composition: \verb|TRY|~\verb|o|~\isa{tac}. There is no need for \verb|TRY'|. - \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the proof + \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the goal state and, recursively, to each element of the resulting sequence. The resulting sequence consists of those states that make \isa{tac} fail. Thus, it applies \isa{tac} as many times as possible (including zero times), and allows backtracking over each @@ -615,7 +611,7 @@ is impossible. \item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the - proof state and, recursively, to the head of the resulting sequence. + goal state and, recursively, to the head of the resulting sequence. It returns the first state to make \isa{tac} fail. It is deterministic, discarding alternative outcomes. @@ -690,7 +686,7 @@ possible in each outcome. \begin{warn} - Note the explicit abstraction over the proof state in the ML + Note the explicit abstraction over the goal state in the ML definition of \verb|REPEAT|. Recursive tacticals must be coded in this awkward fashion to avoid infinite recursion of eager functional evaluation in Standard ML. The following attempt would make \verb|REPEAT|~\isa{tac} loop: @@ -787,6 +783,189 @@ % \endisadelimmlref % +\isamarkupsubsection{Control and search tacticals% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +A predicate on theorems \verb|thm -> bool| can test + whether a goal state enjoys some desirable property --- such as + having no subgoals. Tactics that search for satisfactory goal + states are easy to express. The main search procedures, + depth-first, breadth-first and best-first, are provided as + tacticals. They generate the search tree by repeatedly applying a + given tactic.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Filtering a tactic's results% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{FILTER}\verb|FILTER: (thm -> bool) -> tactic -> tactic| \\ + \indexdef{}{ML}{CHANGED}\verb|CHANGED: tactic -> tactic| \\ + \end{mldecls} + + \begin{description} + + \item \verb|FILTER|~\isa{sat\ tac} applies \isa{tac} to the + goal state and returns a sequence consisting of those result goal + states that are satisfactory in the sense of \isa{sat}. + + \item \verb|CHANGED|~\isa{tac} applies \isa{tac} to the goal + state and returns precisely those states that differ from the + original state (according to \verb|Thm.eq_thm|). Thus \verb|CHANGED|~\isa{tac} always has some effect on the state. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Depth-first search% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{DEPTH\_FIRST}\verb|DEPTH_FIRST: (thm -> bool) -> tactic -> tactic| \\ + \indexdef{}{ML}{DEPTH\_SOLVE}\verb|DEPTH_SOLVE: tactic -> tactic| \\ + \indexdef{}{ML}{DEPTH\_SOLVE\_1}\verb|DEPTH_SOLVE_1: tactic -> tactic| \\ + \end{mldecls} + + \begin{description} + + \item \verb|DEPTH_FIRST|~\isa{sat\ tac} returns the goal state if + \isa{sat} returns true. Otherwise it applies \isa{tac}, + then recursively searches from each element of the resulting + sequence. The code uses a stack for efficiency, in effect applying + \isa{tac}~\verb|THEN|~\verb|DEPTH_FIRST|~\isa{sat\ tac} to + the state. + + \item \verb|DEPTH_SOLVE|\isa{tac} uses \verb|DEPTH_FIRST| to + search for states having no subgoals. + + \item \verb|DEPTH_SOLVE_1|~\isa{tac} uses \verb|DEPTH_FIRST| to + search for states having fewer subgoals than the given state. Thus, + it insists upon solving at least one subgoal. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Other search strategies% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{BREADTH\_FIRST}\verb|BREADTH_FIRST: (thm -> bool) -> tactic -> tactic| \\ + \indexdef{}{ML}{BEST\_FIRST}\verb|BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic| \\ + \indexdef{}{ML}{THEN\_BEST\_FIRST}\verb|THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic| \\ + \end{mldecls} + + These search strategies will find a solution if one exists. + However, they do not enumerate all solutions; they terminate after + the first satisfactory result from \isa{tac}. + + \begin{description} + + \item \verb|BREADTH_FIRST|~\isa{sat\ tac} uses breadth-first + search to find states for which \isa{sat} is true. For most + applications, it is too slow. + + \item \verb|BEST_FIRST|~\isa{{\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} does a heuristic + search, using \isa{dist} to estimate the distance from a + satisfactory state (in the sense of \isa{sat}). It maintains a + list of states ordered by distance. It applies \isa{tac} to the + head of this list; if the result contains any satisfactory states, + then it returns them. Otherwise, \verb|BEST_FIRST| adds the new + states to the list, and continues. + + The distance function is typically \verb|size_of_thm|, which computes + the size of the state. The smaller the state, the fewer and simpler + subgoals it has. + + \item \verb|THEN_BEST_FIRST|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} is like + \verb|BEST_FIRST|, except that the priority queue initially contains + the result of applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}} to the goal state. This + tactical permits separate tactics for starting the search and + continuing the search. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Auxiliary tacticals for searching% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{COND}\verb|COND: (thm -> bool) -> tactic -> tactic -> tactic| \\ + \indexdef{}{ML}{IF\_UNSOLVED}\verb|IF_UNSOLVED: tactic -> tactic| \\ + \indexdef{}{ML}{SOLVE}\verb|SOLVE: tactic -> tactic| \\ + \indexdef{}{ML}{DETERM}\verb|DETERM: tactic -> tactic| \\ + \end{mldecls} + + \begin{description} + + \item \verb|COND|~\isa{sat\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to + the goal state if it satisfies predicate \isa{sat}, and applies + \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. It is a conditional tactical in that only one of + \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is applied to a goal state. + However, both \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are evaluated + because ML uses eager evaluation. + + \item \verb|IF_UNSOLVED|~\isa{tac} applies \isa{tac} to the + goal state if it has any subgoals, and simply returns the goal state + otherwise. Many common tactics, such as \verb|resolve_tac|, fail if + applied to a goal state that has no subgoals. + + \item \verb|SOLVE|~\isa{tac} applies \isa{tac} to the goal + state and then fails iff there are subgoals left. + + \item \verb|DETERM|~\isa{tac} applies \isa{tac} to the goal + state and returns the head of the resulting sequence. \verb|DETERM| + limits the search space by making its argument deterministic. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Predicates and functions useful for searching% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{has\_fewer\_prems}\verb|has_fewer_prems: int -> thm -> bool| \\ + \indexdef{}{ML}{Thm.eq\_thm}\verb|Thm.eq_thm: thm * thm -> bool| \\ + \indexdef{}{ML}{Thm.eq\_thm\_prop}\verb|Thm.eq_thm_prop: thm * thm -> bool| \\ + \indexdef{}{ML}{size\_of\_thm}\verb|size_of_thm: thm -> int| \\ + \end{mldecls} + + \begin{description} + + \item \verb|has_fewer_prems|~\isa{n\ thm} reports whether \isa{thm} has fewer than \isa{n} premises. + + \item \verb|Thm.eq_thm|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal. Both theorems must have + compatible background theories. Both theorems must have the same + conclusions, the same set of hypotheses, and the same set of sort + hypotheses. Names of bound variables are ignored as usual. + + \item \verb|Thm.eq_thm_prop|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether + the propositions of \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal. + Names of bound variables are ignored. + + \item \verb|size_of_thm|~\isa{thm} computes the size of \isa{thm}, namely the number of variables, constants and abstractions + in its conclusion. It may serve as a distance function for + \verb|BEST_FIRST|. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isadelimtheory % \endisadelimtheory

--- a/doc-src/Ref/Makefile Thu Jan 26 21:25:18 2012 +0100 +++ b/doc-src/Ref/Makefile Thu Jan 26 22:16:45 2012 +0100 @@ -9,7 +9,7 @@ include ../Makefile.in NAME = ref -FILES = ref.tex tactic.tex tctical.tex thm.tex defining.tex syntax.tex \ +FILES = ref.tex tactic.tex thm.tex defining.tex syntax.tex \ substitution.tex simplifier.tex classical.tex ../proof.sty \ ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib

--- a/doc-src/Ref/ref.tex Thu Jan 26 21:25:18 2012 +0100 +++ b/doc-src/Ref/ref.tex Thu Jan 26 22:16:45 2012 +0100 @@ -48,7 +48,6 @@ \pagenumbering{roman} \tableofcontents \clearfirst \include{tactic} -\include{tctical} \include{thm} \include{defining} \include{syntax}

--- a/doc-src/Ref/tctical.tex Thu Jan 26 21:25:18 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ - -\chapter{Tacticals} - -\section{Control and search tacticals} -\index{search!tacticals|(} - -A predicate on theorems, namely a function of type \hbox{\tt thm->bool}, -can test whether a proof state enjoys some desirable property --- such as -having no subgoals. Tactics that search for satisfactory states are easy -to express. The main search procedures, depth-first, breadth-first and -best-first, are provided as tacticals. They generate the search tree by -repeatedly applying a given tactic. - - -\subsection{Filtering a tactic's results} -\index{tacticals!for filtering} -\index{tactics!filtering results of} -\begin{ttbox} -FILTER : (thm -> bool) -> tactic -> tactic -CHANGED : tactic -> tactic -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{FILTER} {\it p} $tac$] -applies $tac$ to the proof state and returns a sequence consisting of those -result states that satisfy~$p$. - -\item[\ttindexbold{CHANGED} {\it tac}] -applies {\it tac\/} to the proof state and returns precisely those states -that differ from the original state. Thus, \hbox{\tt CHANGED {\it tac}} -always has some effect on the state. -\end{ttdescription} - - -\subsection{Depth-first search} -\index{tacticals!searching} -\index{tracing!of searching tacticals} -\begin{ttbox} -DEPTH_FIRST : (thm->bool) -> tactic -> tactic -DEPTH_SOLVE : tactic -> tactic -DEPTH_SOLVE_1 : tactic -> tactic -trace_DEPTH_FIRST: bool ref \hfill{\bf initially false} -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}] -returns the proof state if {\it satp} returns true. Otherwise it applies -{\it tac}, then recursively searches from each element of the resulting -sequence. The code uses a stack for efficiency, in effect applying -\hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state. - -\item[\ttindexbold{DEPTH_SOLVE} {\it tac}] -uses {\tt DEPTH_FIRST} to search for states having no subgoals. - -\item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}] -uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the -given state. Thus, it insists upon solving at least one subgoal. - -\item[set \ttindexbold{trace_DEPTH_FIRST};] -enables interactive tracing for {\tt DEPTH_FIRST}. To view the -tracing options, type {\tt h} at the prompt. -\end{ttdescription} - - -\subsection{Other search strategies} -\index{tacticals!searching} -\index{tracing!of searching tacticals} -\begin{ttbox} -BREADTH_FIRST : (thm->bool) -> tactic -> tactic -BEST_FIRST : (thm->bool)*(thm->int) -> tactic -> tactic -THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic) - -> tactic \hfill{\bf infix 1} -trace_BEST_FIRST: bool ref \hfill{\bf initially false} -\end{ttbox} -These search strategies will find a solution if one exists. However, they -do not enumerate all solutions; they terminate after the first satisfactory -result from {\it tac}. -\begin{ttdescription} -\item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}] -uses breadth-first search to find states for which {\it satp\/} is true. -For most applications, it is too slow. - -\item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}] -does a heuristic search, using {\it distf\/} to estimate the distance from -a satisfactory state. It maintains a list of states ordered by distance. -It applies $tac$ to the head of this list; if the result contains any -satisfactory states, then it returns them. Otherwise, {\tt BEST_FIRST} -adds the new states to the list, and continues. - -The distance function is typically \ttindex{size_of_thm}, which computes -the size of the state. The smaller the state, the fewer and simpler -subgoals it has. - -\item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$] -is like {\tt BEST_FIRST}, except that the priority queue initially -contains the result of applying $tac@0$ to the proof state. This tactical -permits separate tactics for starting the search and continuing the search. - -\item[set \ttindexbold{trace_BEST_FIRST};] -enables an interactive tracing mode for the tactical {\tt BEST_FIRST}. To -view the tracing options, type {\tt h} at the prompt. -\end{ttdescription} - - -\subsection{Auxiliary tacticals for searching} -\index{tacticals!conditional} -\index{tacticals!deterministic} -\begin{ttbox} -COND : (thm->bool) -> tactic -> tactic -> tactic -IF_UNSOLVED : tactic -> tactic -SOLVE : tactic -> tactic -DETERM : tactic -> tactic -DETERM_UNTIL_SOLVED : tactic -> tactic -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] -applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$ -otherwise. It is a conditional tactical in that only one of $tac@1$ and -$tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are -evaluated because \ML{} uses eager evaluation. - -\item[\ttindexbold{IF_UNSOLVED} {\it tac}] -applies {\it tac\/} to the proof state if it has any subgoals, and simply -returns the proof state otherwise. Many common tactics, such as {\tt -resolve_tac}, fail if applied to a proof state that has no subgoals. - -\item[\ttindexbold{SOLVE} {\it tac}] -applies {\it tac\/} to the proof state and then fails iff there are subgoals -left. - -\item[\ttindexbold{DETERM} {\it tac}] -applies {\it tac\/} to the proof state and returns the head of the -resulting sequence. {\tt DETERM} limits the search space by making its -argument deterministic. - -\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}] -forces repeated deterministic application of {\it tac\/} to the proof state -until the goal is solved completely. -\end{ttdescription} - - -\subsection{Predicates and functions useful for searching} -\index{theorems!size of} -\index{theorems!equality of} -\begin{ttbox} -has_fewer_prems : int -> thm -> bool -eq_thm : thm * thm -> bool -eq_thm_prop : thm * thm -> bool -size_of_thm : thm -> int -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{has_fewer_prems} $n$ $thm$] -reports whether $thm$ has fewer than~$n$ premises. By currying, -\hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may -be given to the searching tacticals. - -\item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and - $thm@2$ are equal. Both theorems must have compatible signatures. Both - theorems must have the same conclusions, the same hypotheses (in the same - order), and the same set of sort hypotheses. Names of bound variables are - ignored. - -\item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the - propositions of $thm@1$ and $thm@2$ are equal. Names of bound variables are - ignored. - -\item[\ttindexbold{size_of_thm} $thm$] -computes the size of $thm$, namely the number of variables, constants and -abstractions in its conclusion. It may serve as a distance function for -\ttindex{BEST_FIRST}. -\end{ttdescription} - -\index{search!tacticals|)} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "ref" -%%% End: