22 \isamarkupchapter{Tactical reasoning% |
22 \isamarkupchapter{Tactical reasoning% |
23 } |
23 } |
24 \isamarkuptrue% |
24 \isamarkuptrue% |
25 % |
25 % |
26 \begin{isamarkuptext}% |
26 \begin{isamarkuptext}% |
27 The basic idea of tactical theorem proving is to refine the initial |
27 Tactical reasoning works by refining the initial claim in a |
28 claim in a backwards fashion, until a solved form is reached. An |
28 backwards fashion, until a solved form is reached. A \isa{goal} |
29 intermediate goal consists of several subgoals that need to be |
29 consists of several subgoals that need to be solved in order to |
30 solved in order to achieve the main statement; zero subgoals means |
30 achieve the main statement; zero subgoals means that the proof may |
31 that the proof may be finished. A \isa{tactic} is a refinement |
31 be finished. A \isa{tactic} is a refinement operation that maps |
32 operation that maps a goal to a lazy sequence of potential |
32 a goal to a lazy sequence of potential successors. A \isa{tactical} is a combinator for composing tactics.% |
33 successors. A \isa{tactical} is a combinator for composing |
|
34 tactics.% |
|
35 \end{isamarkuptext}% |
33 \end{isamarkuptext}% |
36 \isamarkuptrue% |
34 \isamarkuptrue% |
37 % |
35 % |
38 \isamarkupsection{Goals \label{sec:tactical-goals}% |
36 \isamarkupsection{Goals \label{sec:tactical-goals}% |
39 } |
37 } |
53 quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is |
51 quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is |
54 always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These variables may get instantiated during the course of |
52 always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These variables may get instantiated during the course of |
55 reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is called ``solved''. |
53 reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is called ``solved''. |
56 |
54 |
57 The structure of each subgoal \isa{A\isactrlsub i} is that of a |
55 The structure of each subgoal \isa{A\isactrlsub i} is that of a |
58 general Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} according to the normal |
56 general Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} in normal form where. |
59 form where any local \isa{{\isasymAnd}} is pulled before \isa{{\isasymLongrightarrow}}. Here |
57 Here \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\ |
60 \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\ |
|
61 arbitrary-but-fixed entities of certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal hypotheses, i.e.\ facts that may |
58 arbitrary-but-fixed entities of certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal hypotheses, i.e.\ facts that may |
62 be assumed locally. Together, this forms the goal context of the |
59 be assumed locally. Together, this forms the goal context of the |
63 conclusion \isa{B} to be established. The goal hypotheses may be |
60 conclusion \isa{B} to be established. The goal hypotheses may be |
64 again Hereditary Harrop Formulas, although the level of nesting |
61 again arbitrary Hereditary Harrop Formulas, although the level of |
65 rarely exceeds 1--2 in practice. |
62 nesting rarely exceeds 1--2 in practice. |
66 |
63 |
67 The main conclusion \isa{C} is internally marked as a protected |
64 The main conclusion \isa{C} is internally marked as a protected |
68 proposition\glossary{Protected proposition}{An arbitrarily |
65 proposition\glossary{Protected proposition}{An arbitrarily |
69 structured proposition \isa{C} which is forced to appear as |
66 structured proposition \isa{C} which is forced to appear as |
70 atomic by wrapping it into a propositional identity operator; |
67 atomic by wrapping it into a propositional identity operator; |
71 notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic |
68 notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic |
72 inferences from entering into that structure for the time being.}, |
69 inferences from entering into that structure for the time being.}, |
73 which is occasionally represented explicitly by the notation \isa{{\isacharhash}C}. This ensures that the decomposition into subgoals and main |
70 which is represented explicitly by the notation \isa{{\isacharhash}C}. This |
74 conclusion is well-defined for arbitrarily structured claims. |
71 ensures that the decomposition into subgoals and main conclusion is |
|
72 well-defined for arbitrarily structured claims. |
75 |
73 |
76 \medskip Basic goal management is performed via the following |
74 \medskip Basic goal management is performed via the following |
77 Isabelle/Pure rules: |
75 Isabelle/Pure rules: |
78 |
76 |
79 \[ |
77 \[ |
105 \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\ |
103 \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\ |
106 \end{mldecls} |
104 \end{mldecls} |
107 |
105 |
108 \begin{description} |
106 \begin{description} |
109 |
107 |
110 \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal from |
108 \item \verb|Goal.init|~\isa{C} initializes a tactical goal from |
111 the type-checked proposition \isa{{\isasymphi}}. |
109 the well-formed proposition \isa{C}. |
112 |
110 |
113 \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (no subgoals), and concludes |
111 \item \verb|Goal.finish|~\isa{thm} checks whether theorem |
114 the result by removing the goal protection. |
112 \isa{thm} is a solved goal (no subgoals), and concludes the |
|
113 result by removing the goal protection. |
115 |
114 |
116 \item \verb|Goal.protect|~\isa{th} protects the full statement |
115 \item \verb|Goal.protect|~\isa{thm} protects the full statement |
117 of theorem \isa{th}. |
116 of theorem \isa{thm}. |
118 |
117 |
119 \item \verb|Goal.conclude|~\isa{th} removes the goal protection |
118 \item \verb|Goal.conclude|~\isa{thm} removes the goal |
120 for any number of pending subgoals. |
119 protection, even if there are pending subgoals. |
121 |
120 |
122 \end{description}% |
121 \end{description}% |
123 \end{isamarkuptext}% |
122 \end{isamarkuptext}% |
124 \isamarkuptrue% |
123 \isamarkuptrue% |
125 % |
124 % |