105 216d6ed87399 Initial revision lcp parents: diff changeset  1 %% $Id$  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  2 \part{Advanced Methods}  105 216d6ed87399 Initial revision lcp parents: diff changeset  3 Before continuing, it might be wise to try some of your own examples in  216d6ed87399 Initial revision lcp parents: diff changeset  4 Isabelle, reinforcing your knowledge of the basic functions.  216d6ed87399 Initial revision lcp parents: diff changeset  5 216d6ed87399 Initial revision lcp parents: diff changeset  6 Look through {\em Isabelle's Object-Logics\/} and try proving some simple  216d6ed87399 Initial revision lcp parents: diff changeset  7 theorems. You probably should begin with first-order logic ({\tt FOL}  216d6ed87399 Initial revision lcp parents: diff changeset  8 or~{\tt LK}). Try working some of the examples provided, and others from  216d6ed87399 Initial revision lcp parents: diff changeset  9 the literature. Set theory~({\tt ZF}) and Constructive Type Theory~({\tt  216d6ed87399 Initial revision lcp parents: diff changeset  10  CTT}) form a richer world for mathematical reasoning and, again, many  216d6ed87399 Initial revision lcp parents: diff changeset  11 examples are in the literature. Higher-order logic~({\tt HOL}) is  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  12 Isabelle's most sophisticated logic because its types and functions are  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  13 identified with those of the meta-logic.  105 216d6ed87399 Initial revision lcp parents: diff changeset  14 216d6ed87399 Initial revision lcp parents: diff changeset  15 Choose a logic that you already understand. Isabelle is a proof  216d6ed87399 Initial revision lcp parents: diff changeset  16 tool, not a teaching tool; if you do not know how to do a particular proof  216d6ed87399 Initial revision lcp parents: diff changeset  17 on paper, then you certainly will not be able to do it on the machine.  216d6ed87399 Initial revision lcp parents: diff changeset  18 Even experienced users plan large proofs on paper.  216d6ed87399 Initial revision lcp parents: diff changeset  19 216d6ed87399 Initial revision lcp parents: diff changeset  20 We have covered only the bare essentials of Isabelle, but enough to perform  216d6ed87399 Initial revision lcp parents: diff changeset  21 substantial proofs. By occasionally dipping into the {\em Reference  216d6ed87399 Initial revision lcp parents: diff changeset  22 Manual}, you can learn additional tactics, subgoal commands and tacticals.  216d6ed87399 Initial revision lcp parents: diff changeset  23 216d6ed87399 Initial revision lcp parents: diff changeset  24 216d6ed87399 Initial revision lcp parents: diff changeset  25 \section{Deriving rules in Isabelle}  216d6ed87399 Initial revision lcp parents: diff changeset  26 \index{rules!derived}  216d6ed87399 Initial revision lcp parents: diff changeset  27 A mathematical development goes through a progression of stages. Each  216d6ed87399 Initial revision lcp parents: diff changeset  28 stage defines some concepts and derives rules about them. We shall see how  216d6ed87399 Initial revision lcp parents: diff changeset  29 to derive rules, perhaps involving definitions, using Isabelle. The  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  30 following section will explain how to declare types, constants, rules and  105 216d6ed87399 Initial revision lcp parents: diff changeset  31 definitions.  216d6ed87399 Initial revision lcp parents: diff changeset  32 216d6ed87399 Initial revision lcp parents: diff changeset  33 296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  34 \subsection{Deriving a rule using tactics and meta-level assumptions}  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  35 \label{deriving-example}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  36 \index{examples!of deriving rules}\index{assumptions!of main goal}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  37 307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  38 The subgoal module supports the derivation of rules, as discussed in  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  39 \S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  40 form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  41 as the initial proof state and returns a list consisting of the theorems  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  42 ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  43 are also recorded internally, allowing {\tt result} to discharge them  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  44 in the original order.  105 216d6ed87399 Initial revision lcp parents: diff changeset  45 307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  46 Let us derive $\conj$ elimination using Isabelle.  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  47 Until now, calling {\tt goal} has returned an empty list, which we have  105 216d6ed87399 Initial revision lcp parents: diff changeset  48 thrown away. In this example, the list contains the two premises of the  216d6ed87399 Initial revision lcp parents: diff changeset  49 rule. We bind them to the \ML\ identifiers {\tt major} and {\tt  216d6ed87399 Initial revision lcp parents: diff changeset  50 minor}:\footnote{Some ML compilers will print a message such as {\em  216d6ed87399 Initial revision lcp parents: diff changeset  51 binding not exhaustive}. This warns that {\tt goal} must return a  216d6ed87399 Initial revision lcp parents: diff changeset  52 2-element list. Otherwise, the pattern-match will fail; ML will  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  53 raise exception \xdx{Match}.}  105 216d6ed87399 Initial revision lcp parents: diff changeset  54 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  55 val [major,minor] = goal FOL.thy  216d6ed87399 Initial revision lcp parents: diff changeset  56  "[| P&Q; [| P; Q |] ==> R |] ==> R";  216d6ed87399 Initial revision lcp parents: diff changeset  57 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  58 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  59 {\out 1. R}  216d6ed87399 Initial revision lcp parents: diff changeset  60 {\out val major = "P & Q [P & Q]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  61 {\out val minor = "[| P; Q |] ==> R [[| P; Q |] ==> R]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  62 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  63 Look at the minor premise, recalling that meta-level assumptions are  216d6ed87399 Initial revision lcp parents: diff changeset  64 shown in brackets. Using {\tt minor}, we reduce $R$ to the subgoals  216d6ed87399 Initial revision lcp parents: diff changeset  65 $P$ and~$Q$:  216d6ed87399 Initial revision lcp parents: diff changeset  66 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  67 by (resolve_tac [minor] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  68 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  69 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  70 {\out 1. P}  216d6ed87399 Initial revision lcp parents: diff changeset  71 {\out 2. Q}  216d6ed87399 Initial revision lcp parents: diff changeset  72 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  73 Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the  216d6ed87399 Initial revision lcp parents: diff changeset  74 assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.  216d6ed87399 Initial revision lcp parents: diff changeset  75 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  76 major RS conjunct1;  216d6ed87399 Initial revision lcp parents: diff changeset  77 {\out val it = "P [P & Q]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  78 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  79 by (resolve_tac [major RS conjunct1] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  80 {\out Level 2}  216d6ed87399 Initial revision lcp parents: diff changeset  81 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  82 {\out 1. Q}  216d6ed87399 Initial revision lcp parents: diff changeset  83 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  84 Similarly, we solve the subgoal involving~$Q$.  216d6ed87399 Initial revision lcp parents: diff changeset  85 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  86 major RS conjunct2;  216d6ed87399 Initial revision lcp parents: diff changeset  87 {\out val it = "Q [P & Q]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  88 by (resolve_tac [major RS conjunct2] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  89 {\out Level 3}  216d6ed87399 Initial revision lcp parents: diff changeset  90 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  91 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  92 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  93 Calling \ttindex{topthm} returns the current proof state as a theorem.  216d6ed87399 Initial revision lcp parents: diff changeset  94 Note that it contains assumptions. Calling \ttindex{result} discharges the  216d6ed87399 Initial revision lcp parents: diff changeset  95 assumptions --- both occurrences of $P\conj Q$ are discharged as one ---  216d6ed87399 Initial revision lcp parents: diff changeset  96 and makes the variables schematic.  216d6ed87399 Initial revision lcp parents: diff changeset  97 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  98 topthm();  216d6ed87399 Initial revision lcp parents: diff changeset  99 {\out val it = "R [P & Q, P & Q, [| P; Q |] ==> R]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  100 val conjE = result();  216d6ed87399 Initial revision lcp parents: diff changeset  101 {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  102 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  103 216d6ed87399 Initial revision lcp parents: diff changeset  104 216d6ed87399 Initial revision lcp parents: diff changeset  105 \subsection{Definitions and derived rules} \label{definitions}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  106 \index{rules!derived}\index{definitions!and derived rules|(}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  107 105 216d6ed87399 Initial revision lcp parents: diff changeset  108 Definitions are expressed as meta-level equalities. Let us define negation  216d6ed87399 Initial revision lcp parents: diff changeset  109 and the if-and-only-if connective:  216d6ed87399 Initial revision lcp parents: diff changeset  110 \begin{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  111  \neg \Var{P} & \equiv & \Var{P}\imp\bot \\  216d6ed87399 Initial revision lcp parents: diff changeset  112  \Var{P}\bimp \Var{Q} & \equiv &  216d6ed87399 Initial revision lcp parents: diff changeset  113  (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})  216d6ed87399 Initial revision lcp parents: diff changeset  114 \end{eqnarray*}  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  115 \index{meta-rewriting}%  105 216d6ed87399 Initial revision lcp parents: diff changeset  116 Isabelle permits {\bf meta-level rewriting} using definitions such as  216d6ed87399 Initial revision lcp parents: diff changeset  117 these. {\bf Unfolding} replaces every instance  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  118 of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For  105 216d6ed87399 Initial revision lcp parents: diff changeset  119 example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to  216d6ed87399 Initial revision lcp parents: diff changeset  120 $\forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.$  216d6ed87399 Initial revision lcp parents: diff changeset  121 {\bf Folding} a definition replaces occurrences of the right-hand side by  216d6ed87399 Initial revision lcp parents: diff changeset  122 the left. The occurrences need not be free in the entire formula.  216d6ed87399 Initial revision lcp parents: diff changeset  123 216d6ed87399 Initial revision lcp parents: diff changeset  124 When you define new concepts, you should derive rules asserting their  216d6ed87399 Initial revision lcp parents: diff changeset  125 abstract properties, and then forget their definitions. This supports  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  126 modularity: if you later change the definitions without affecting their  105 216d6ed87399 Initial revision lcp parents: diff changeset  127 abstract properties, then most of your proofs will carry through without  216d6ed87399 Initial revision lcp parents: diff changeset  128 change. Indiscriminate unfolding makes a subgoal grow exponentially,  216d6ed87399 Initial revision lcp parents: diff changeset  129 becoming unreadable.  216d6ed87399 Initial revision lcp parents: diff changeset  130 216d6ed87399 Initial revision lcp parents: diff changeset  131 Taking this point of view, Isabelle does not unfold definitions  216d6ed87399 Initial revision lcp parents: diff changeset  132 automatically during proofs. Rewriting must be explicit and selective.  216d6ed87399 Initial revision lcp parents: diff changeset  133 Isabelle provides tactics and meta-rules for rewriting, and a version of  216d6ed87399 Initial revision lcp parents: diff changeset  134 the {\tt goal} command that unfolds the conclusion and premises of the rule  216d6ed87399 Initial revision lcp parents: diff changeset  135 being derived.  216d6ed87399 Initial revision lcp parents: diff changeset  136 216d6ed87399 Initial revision lcp parents: diff changeset  137 For example, the intuitionistic definition of negation given above may seem  216d6ed87399 Initial revision lcp parents: diff changeset  138 peculiar. Using Isabelle, we shall derive pleasanter negation rules:  216d6ed87399 Initial revision lcp parents: diff changeset  139 $\infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad  216d6ed87399 Initial revision lcp parents: diff changeset  140  \infer[({\neg}E)]{Q}{\neg P & P}$  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  141 This requires proving the following meta-formulae:  105 216d6ed87399 Initial revision lcp parents: diff changeset  142 $$(P\Imp\bot) \Imp \neg P \eqno(\neg I)$$  216d6ed87399 Initial revision lcp parents: diff changeset  143 $$\List{\neg P; P} \Imp Q. \eqno(\neg E)$$  216d6ed87399 Initial revision lcp parents: diff changeset  144 216d6ed87399 Initial revision lcp parents: diff changeset  145 296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  146 \subsection{Deriving the $\neg$ introduction rule}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  147 To derive $(\neg I)$, we may call {\tt goal} with the appropriate  105 216d6ed87399 Initial revision lcp parents: diff changeset  148 formula. Again, {\tt goal} returns a list consisting of the rule's  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  149 premises. We bind this one-element list to the \ML\ identifier {\tt  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  150  prems}.  105 216d6ed87399 Initial revision lcp parents: diff changeset  151 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  152 val prems = goal FOL.thy "(P ==> False) ==> ~P";  216d6ed87399 Initial revision lcp parents: diff changeset  153 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  154 {\out ~P}  216d6ed87399 Initial revision lcp parents: diff changeset  155 {\out 1. ~P}  216d6ed87399 Initial revision lcp parents: diff changeset  156 {\out val prems = ["P ==> False [P ==> False]"] : thm list}  216d6ed87399 Initial revision lcp parents: diff changeset  157 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  158 Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the  105 216d6ed87399 Initial revision lcp parents: diff changeset  159 definition of negation, unfolds that definition in the subgoals. It leaves  216d6ed87399 Initial revision lcp parents: diff changeset  160 the main goal alone.  216d6ed87399 Initial revision lcp parents: diff changeset  161 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  162 not_def;  216d6ed87399 Initial revision lcp parents: diff changeset  163 {\out val it = "~?P == ?P --> False" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  164 by (rewrite_goals_tac [not_def]);  216d6ed87399 Initial revision lcp parents: diff changeset  165 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  166 {\out ~P}  216d6ed87399 Initial revision lcp parents: diff changeset  167 {\out 1. P --> False}  216d6ed87399 Initial revision lcp parents: diff changeset  168 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  169 Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:  105 216d6ed87399 Initial revision lcp parents: diff changeset  170 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  171 by (resolve_tac [impI] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  172 {\out Level 2}  216d6ed87399 Initial revision lcp parents: diff changeset  173 {\out ~P}  216d6ed87399 Initial revision lcp parents: diff changeset  174 {\out 1. P ==> False}  216d6ed87399 Initial revision lcp parents: diff changeset  175 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  176 by (resolve_tac prems 1);  216d6ed87399 Initial revision lcp parents: diff changeset  177 {\out Level 3}  216d6ed87399 Initial revision lcp parents: diff changeset  178 {\out ~P}  216d6ed87399 Initial revision lcp parents: diff changeset  179 {\out 1. P ==> P}  216d6ed87399 Initial revision lcp parents: diff changeset  180 \end{ttbox}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  181 The rest of the proof is routine. Note the form of the final result.  105 216d6ed87399 Initial revision lcp parents: diff changeset  182 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  183 by (assume_tac 1);  216d6ed87399 Initial revision lcp parents: diff changeset  184 {\out Level 4}  216d6ed87399 Initial revision lcp parents: diff changeset  185 {\out ~P}  216d6ed87399 Initial revision lcp parents: diff changeset  186 {\out No subgoals!}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  187 \ttbreak  105 216d6ed87399 Initial revision lcp parents: diff changeset  188 val notI = result();  216d6ed87399 Initial revision lcp parents: diff changeset  189 {\out val notI = "(?P ==> False) ==> ~?P" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  190 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  191 \indexbold{*notI theorem}  105 216d6ed87399 Initial revision lcp parents: diff changeset  192 216d6ed87399 Initial revision lcp parents: diff changeset  193 There is a simpler way of conducting this proof. The \ttindex{goalw}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  194 command starts a backward proof, as does {\tt goal}, but it also  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  195 unfolds definitions. Thus there is no need to call  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  196 \ttindex{rewrite_goals_tac}:  105 216d6ed87399 Initial revision lcp parents: diff changeset  197 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  198 val prems = goalw FOL.thy [not_def]  216d6ed87399 Initial revision lcp parents: diff changeset  199  "(P ==> False) ==> ~P";  216d6ed87399 Initial revision lcp parents: diff changeset  200 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  201 {\out ~P}  216d6ed87399 Initial revision lcp parents: diff changeset  202 {\out 1. P --> False}  216d6ed87399 Initial revision lcp parents: diff changeset  203 {\out val prems = ["P ==> False [P ==> False]"] : thm list}  216d6ed87399 Initial revision lcp parents: diff changeset  204 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  205 216d6ed87399 Initial revision lcp parents: diff changeset  206 296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  207 \subsection{Deriving the $\neg$ elimination rule}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  208 Let us derive the rule $(\neg E)$. The proof follows that of~{\tt conjE}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  209 above, with an additional step to unfold negation in the major premise.  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  210 Although the {\tt goalw} command is best for this, let us  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  211 try~{\tt goal} to see another way of unfolding definitions. After  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  212 binding the premises to \ML\ identifiers, we apply \tdx{FalseE}:  105 216d6ed87399 Initial revision lcp parents: diff changeset  213 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  214 val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R";  216d6ed87399 Initial revision lcp parents: diff changeset  215 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  216 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  217 {\out 1. R}  216d6ed87399 Initial revision lcp parents: diff changeset  218 {\out val major = "~ P [~ P]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  219 {\out val minor = "P [P]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  220 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  221 by (resolve_tac [FalseE] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  222 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  223 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  224 {\out 1. False}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  225 \end{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  226 Everything follows from falsity. And we can prove falsity using the  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  227 premises and Modus Ponens:  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  228 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  229 by (resolve_tac [mp] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  230 {\out Level 2}  216d6ed87399 Initial revision lcp parents: diff changeset  231 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  232 {\out 1. ?P1 --> False}  216d6ed87399 Initial revision lcp parents: diff changeset  233 {\out 2. ?P1}  216d6ed87399 Initial revision lcp parents: diff changeset  234 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  235 For subgoal~1, we transform the major premise from~$\neg P$  216d6ed87399 Initial revision lcp parents: diff changeset  236 to~${P\imp\bot}$. The function \ttindex{rewrite_rule}, given a list of  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  237 definitions, unfolds them in a theorem. Rewriting does not  105 216d6ed87399 Initial revision lcp parents: diff changeset  238 affect the theorem's hypothesis, which remains~$\neg P$:  216d6ed87399 Initial revision lcp parents: diff changeset  239 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  240 rewrite_rule [not_def] major;  216d6ed87399 Initial revision lcp parents: diff changeset  241 {\out val it = "P --> False [~P]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  242 by (resolve_tac [it] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  243 {\out Level 3}  216d6ed87399 Initial revision lcp parents: diff changeset  244 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  245 {\out 1. P}  216d6ed87399 Initial revision lcp parents: diff changeset  246 \end{ttbox}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  247 The subgoal {\tt?P1} has been instantiated to~{\tt P}, which we can prove  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  248 using the minor premise:  105 216d6ed87399 Initial revision lcp parents: diff changeset  249 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  250 by (resolve_tac [minor] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  251 {\out Level 4}  216d6ed87399 Initial revision lcp parents: diff changeset  252 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  253 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  254 val notE = result();  216d6ed87399 Initial revision lcp parents: diff changeset  255 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  256 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  257 \indexbold{*notE theorem}  105 216d6ed87399 Initial revision lcp parents: diff changeset  258 216d6ed87399 Initial revision lcp parents: diff changeset  259 \medskip  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  260 Again, there is a simpler way of conducting this proof. Recall that  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  261 the \ttindex{goalw} command unfolds definitions the conclusion; it also  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  262 unfolds definitions in the premises:  105 216d6ed87399 Initial revision lcp parents: diff changeset  263 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  264 val [major,minor] = goalw FOL.thy [not_def]  216d6ed87399 Initial revision lcp parents: diff changeset  265  "[| ~P; P |] ==> R";  216d6ed87399 Initial revision lcp parents: diff changeset  266 {\out val major = "P --> False [~ P]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  267 {\out val minor = "P [P]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  268 \end{ttbox}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  269 Observe the difference in {\tt major}; the premises are unfolded without  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  270 calling~\ttindex{rewrite_rule}. Incidentally, the four calls to  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  271 \ttindex{resolve_tac} above can be collapsed to one, with the help  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  272 of~\ttindex{RS}; this is a typical example of forward reasoning from a  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  273 complex premise.  105 216d6ed87399 Initial revision lcp parents: diff changeset  274 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  275 minor RS (major RS mp RS FalseE);  216d6ed87399 Initial revision lcp parents: diff changeset  276 {\out val it = "?P [P, ~P]" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  277 by (resolve_tac [it] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  278 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  279 {\out R}  216d6ed87399 Initial revision lcp parents: diff changeset  280 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  281 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  282 \index{definitions!and derived rules|)}  105 216d6ed87399 Initial revision lcp parents: diff changeset  283 310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  284 \goodbreak\medskip\index{*"!"! symbol!in main goal}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  285 Finally, here is a trick that is sometimes useful. If the goal  105 216d6ed87399 Initial revision lcp parents: diff changeset  286 has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  287 do not return the rule's premises in the list of theorems; instead, the  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  288 premises become assumptions in subgoal~1.  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  289 %%%It does not matter which variables are quantified over.  105 216d6ed87399 Initial revision lcp parents: diff changeset  290 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  291 goalw FOL.thy [not_def] "!!P R. [| ~P; P |] ==> R";  216d6ed87399 Initial revision lcp parents: diff changeset  292 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  293 {\out !!P R. [| ~ P; P |] ==> R}  216d6ed87399 Initial revision lcp parents: diff changeset  294 {\out 1. !!P R. [| P --> False; P |] ==> R}  216d6ed87399 Initial revision lcp parents: diff changeset  295 val it = [] : thm list  216d6ed87399 Initial revision lcp parents: diff changeset  296 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  297 The proof continues as before. But instead of referring to \ML\  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  298 identifiers, we refer to assumptions using {\tt eresolve_tac} or  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  299 {\tt assume_tac}:  105 216d6ed87399 Initial revision lcp parents: diff changeset  300 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  301 by (resolve_tac [FalseE] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  302 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  303 {\out !!P R. [| ~ P; P |] ==> R}  216d6ed87399 Initial revision lcp parents: diff changeset  304 {\out 1. !!P R. [| P --> False; P |] ==> False}  216d6ed87399 Initial revision lcp parents: diff changeset  305 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  306 by (eresolve_tac [mp] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  307 {\out Level 2}  216d6ed87399 Initial revision lcp parents: diff changeset  308 {\out !!P R. [| ~ P; P |] ==> R}  216d6ed87399 Initial revision lcp parents: diff changeset  309 {\out 1. !!P R. P ==> P}  216d6ed87399 Initial revision lcp parents: diff changeset  310 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  311 by (assume_tac 1);  216d6ed87399 Initial revision lcp parents: diff changeset  312 {\out Level 3}  216d6ed87399 Initial revision lcp parents: diff changeset  313 {\out !!P R. [| ~ P; P |] ==> R}  216d6ed87399 Initial revision lcp parents: diff changeset  314 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  315 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  316 Calling \ttindex{result} strips the meta-quantifiers, so the resulting  216d6ed87399 Initial revision lcp parents: diff changeset  317 theorem is the same as before.  216d6ed87399 Initial revision lcp parents: diff changeset  318 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  319 val notE = result();  216d6ed87399 Initial revision lcp parents: diff changeset  320 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}  216d6ed87399 Initial revision lcp parents: diff changeset  321 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  322 Do not use the {\tt!!}\ trick if the premises contain meta-level  216d6ed87399 Initial revision lcp parents: diff changeset  323 connectives, because \ttindex{eresolve_tac} and \ttindex{assume_tac} would  216d6ed87399 Initial revision lcp parents: diff changeset  324 not be able to handle the resulting assumptions. The trick is not suitable  216d6ed87399 Initial revision lcp parents: diff changeset  325 for deriving the introduction rule~$(\neg I)$.  216d6ed87399 Initial revision lcp parents: diff changeset  326 216d6ed87399 Initial revision lcp parents: diff changeset  327 284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  328 \section{Defining theories}\label{sec:defining-theories}  105 216d6ed87399 Initial revision lcp parents: diff changeset  329 \index{theories!defining|(}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  330 105 216d6ed87399 Initial revision lcp parents: diff changeset  331 Isabelle makes no distinction between simple extensions of a logic --- like  216d6ed87399 Initial revision lcp parents: diff changeset  332 defining a type~$bool$ with constants~$true$ and~$false$ --- and defining  216d6ed87399 Initial revision lcp parents: diff changeset  333 an entire logic. A theory definition has the form  216d6ed87399 Initial revision lcp parents: diff changeset  334 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  335 $$T$$ = $$S@1$$ + $$\cdots$$ + $$S@n$$ +  216d6ed87399 Initial revision lcp parents: diff changeset  336 classes {\it class declarations}  216d6ed87399 Initial revision lcp parents: diff changeset  337 default {\it sort}  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  338 types {\it type declarations and synonyms}  105 216d6ed87399 Initial revision lcp parents: diff changeset  339 arities {\it arity declarations}  216d6ed87399 Initial revision lcp parents: diff changeset  340 consts {\it constant declarations}  216d6ed87399 Initial revision lcp parents: diff changeset  341 rules {\it rule declarations}  216d6ed87399 Initial revision lcp parents: diff changeset  342 translations {\it translation declarations}  216d6ed87399 Initial revision lcp parents: diff changeset  343 end  216d6ed87399 Initial revision lcp parents: diff changeset  344 ML {\it ML code}  216d6ed87399 Initial revision lcp parents: diff changeset  345 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  346 This declares the theory $T$ to extend the existing theories  216d6ed87399 Initial revision lcp parents: diff changeset  347 $S@1$,~\ldots,~$S@n$. It may declare new classes, types, arities  216d6ed87399 Initial revision lcp parents: diff changeset  348 (overloadings of existing types), constants and rules; it can specify the  216d6ed87399 Initial revision lcp parents: diff changeset  349 default sort for type variables. A constant declaration can specify an  216d6ed87399 Initial revision lcp parents: diff changeset  350 associated concrete syntax. The translations section specifies rewrite  216d6ed87399 Initial revision lcp parents: diff changeset  351 rules on abstract syntax trees, for defining notations and abbreviations.  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  352 \index{*ML section}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  353 The {\tt ML} section contains code to perform arbitrary syntactic  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  354 transformations. The main declaration forms are discussed below.  303 0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  355 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  356  appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.  105 216d6ed87399 Initial revision lcp parents: diff changeset  357 216d6ed87399 Initial revision lcp parents: diff changeset  358 All the declaration parts can be omitted. In the simplest case, $T$ is  216d6ed87399 Initial revision lcp parents: diff changeset  359 just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one  216d6ed87399 Initial revision lcp parents: diff changeset  360 or more other theories, inheriting their types, constants, syntax, etc.  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  361 The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.  105 216d6ed87399 Initial revision lcp parents: diff changeset  362 331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  363 Each theory definition must reside in a separate file, whose name is the  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  364 theory's with {\tt.thy} appended. For example, theory {\tt ListFn} resides  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  365 on a file named {\tt ListFn.thy}. Isabelle uses this convention to locate the  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  366 file containing a given theory; \ttindexbold{use_thy} automatically loads a  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  367 theory's parents before loading the theory itself.  105 216d6ed87399 Initial revision lcp parents: diff changeset  368 331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  369 Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  370 file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  371 {\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  372 occurred. This declares the {\ML} structure~$T$, which contains a component  109 0872fd327440 adapted "Defining theories" to new use_thy clasohm parents: 105 diff changeset  373 {\tt thy} denoting the new theory, a component for each rule, and everything  0872fd327440 adapted "Defining theories" to new use_thy clasohm parents: 105 diff changeset  374 declared in {\it ML code}.  105 216d6ed87399 Initial revision lcp parents: diff changeset  375 216d6ed87399 Initial revision lcp parents: diff changeset  376 Errors may arise during the translation to {\ML} (say, a misspelled keyword)  216d6ed87399 Initial revision lcp parents: diff changeset  377 or during creation of the new theory (say, a type error in a rule). But if  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  378 all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if  105 216d6ed87399 Initial revision lcp parents: diff changeset  379 it exists. This file typically begins with the {\ML} declaration {\tt  216d6ed87399 Initial revision lcp parents: diff changeset  380 open}~$T$ and contains proofs that refer to the components of~$T$.  216d6ed87399 Initial revision lcp parents: diff changeset  381 296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  382 When a theory file is modified, many theories may have to be reloaded.  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  383 Isabelle records the modification times and dependencies of theory files.  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  384 See  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  385 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%  13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  386  {\S\ref{sec:reloading-theories}}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  387 for more details.  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  388 105 216d6ed87399 Initial revision lcp parents: diff changeset  389 216d6ed87399 Initial revision lcp parents: diff changeset  390 \subsection{Declaring constants and rules}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  391 \indexbold{constants!declaring}\index{rules!declaring}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  392 296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  393 Most theories simply declare constants and rules. The {\bf constant  105 216d6ed87399 Initial revision lcp parents: diff changeset  394 declaration part} has the form  216d6ed87399 Initial revision lcp parents: diff changeset  395 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  396 consts $$c@1$$ :: "$$\tau@1$$"  216d6ed87399 Initial revision lcp parents: diff changeset  397  \vdots  216d6ed87399 Initial revision lcp parents: diff changeset  398  $$c@n$$ :: "$$\tau@n$$"  216d6ed87399 Initial revision lcp parents: diff changeset  399 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  400 where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are  216d6ed87399 Initial revision lcp parents: diff changeset  401 types. Each type {\em must\/} be enclosed in quotation marks. Each  216d6ed87399 Initial revision lcp parents: diff changeset  402 constant must be enclosed in quotation marks unless it is a valid  216d6ed87399 Initial revision lcp parents: diff changeset  403 identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,  216d6ed87399 Initial revision lcp parents: diff changeset  404 the $n$ declarations may be abbreviated to a single line:  216d6ed87399 Initial revision lcp parents: diff changeset  405 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  406  $$c@1$$, \ldots, $$c@n$$ :: "$$\tau$$"  216d6ed87399 Initial revision lcp parents: diff changeset  407 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  408 The {\bf rule declaration part} has the form  216d6ed87399 Initial revision lcp parents: diff changeset  409 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  410 rules $$id@1$$ "$$rule@1$$"  216d6ed87399 Initial revision lcp parents: diff changeset  411  \vdots  216d6ed87399 Initial revision lcp parents: diff changeset  412  $$id@n$$ "$$rule@n$$"  216d6ed87399 Initial revision lcp parents: diff changeset  413 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  414 where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  415 $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  416 enclosed in quotation marks.  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  417 310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  418 \indexbold{definitions}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  419 {\bf Definitions} are rules of the form $t\equiv u$. Normally definitions  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  420 should be conservative, serving only as abbreviations. As of this writing,  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  421 Isabelle does not provide a separate declaration part for definitions; it  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  422 is your responsibility to ensure that your definitions are conservative.  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  423 However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  424 variables free in~$u$ are also free in~$t$.  105 216d6ed87399 Initial revision lcp parents: diff changeset  425 216d6ed87399 Initial revision lcp parents: diff changeset  426 \index{examples!of theories}  216d6ed87399 Initial revision lcp parents: diff changeset  427 This theory extends first-order logic with two constants {\em nand} and  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  428 {\em xor}, and declares rules to define them:  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  429 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  430 Gate = FOL +  216d6ed87399 Initial revision lcp parents: diff changeset  431 consts nand,xor :: "[o,o] => o"  216d6ed87399 Initial revision lcp parents: diff changeset  432 rules nand_def "nand(P,Q) == ~(P & Q)"  216d6ed87399 Initial revision lcp parents: diff changeset  433  xor_def "xor(P,Q) == P & ~Q | ~P & Q"  216d6ed87399 Initial revision lcp parents: diff changeset  434 end  216d6ed87399 Initial revision lcp parents: diff changeset  435 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  436 216d6ed87399 Initial revision lcp parents: diff changeset  437 216d6ed87399 Initial revision lcp parents: diff changeset  438 \subsection{Declaring type constructors}  303 0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  439 \indexbold{types!declaring}\indexbold{arities!declaring}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  440 %  105 216d6ed87399 Initial revision lcp parents: diff changeset  441 Types are composed of type variables and {\bf type constructors}. Each  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  442 type constructor takes a fixed number of arguments. They are declared  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  443 with an \ML-like syntax. If $list$ takes one type argument, $tree$ takes  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  444 two arguments and $nat$ takes no arguments, then these type constructors  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  445 can be declared by  105 216d6ed87399 Initial revision lcp parents: diff changeset  446 \begin{ttbox}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  447 types 'a list  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  448  ('a,'b) tree  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  449  nat  105 216d6ed87399 Initial revision lcp parents: diff changeset  450 \end{ttbox}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  451 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  452 The {\bf type declaration part} has the general form  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  453 \begin{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  454 types $$tids@1$$ $$id@1$$  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  455  \vdots  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  456  $$tids@1$$ $$id@n$$  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  457 \end{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  458 where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  459 are type argument lists as shown in the example above. It declares each  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  460 $id@i$ as a type constructor with the specified number of argument places.  105 216d6ed87399 Initial revision lcp parents: diff changeset  461 216d6ed87399 Initial revision lcp parents: diff changeset  462 The {\bf arity declaration part} has the form  216d6ed87399 Initial revision lcp parents: diff changeset  463 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  464 arities $$tycon@1$$ :: $$arity@1$$  216d6ed87399 Initial revision lcp parents: diff changeset  465  \vdots  216d6ed87399 Initial revision lcp parents: diff changeset  466  $$tycon@n$$ :: $$arity@n$$  216d6ed87399 Initial revision lcp parents: diff changeset  467 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  468 where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,  216d6ed87399 Initial revision lcp parents: diff changeset  469 $arity@n$ are arities. Arity declarations add arities to existing  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  470 types; they do not declare the types themselves.  105 216d6ed87399 Initial revision lcp parents: diff changeset  471 In the simplest case, for an 0-place type constructor, an arity is simply  216d6ed87399 Initial revision lcp parents: diff changeset  472 the type's class. Let us declare a type~$bool$ of class $term$, with  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  473 constants $tt$ and~$ff$. (In first-order logic, booleans are  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  474 distinct from formulae, which have type $o::logic$.)  105 216d6ed87399 Initial revision lcp parents: diff changeset  475 \index{examples!of theories}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  476 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  477 Bool = FOL +  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  478 types bool  105 216d6ed87399 Initial revision lcp parents: diff changeset  479 arities bool :: term  216d6ed87399 Initial revision lcp parents: diff changeset  480 consts tt,ff :: "bool"  216d6ed87399 Initial revision lcp parents: diff changeset  481 end  216d6ed87399 Initial revision lcp parents: diff changeset  482 \end{ttbox}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  483 A $k$-place type constructor may have arities of the form  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  484 $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  485 Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  486 where $c@1$, \dots,~$c@m$ are classes. Mostly we deal with singleton  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  487 sorts, and may abbreviate them by dropping the braces. The arity  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  488 $(term)term$ is short for $(\{term\})term$. Recall the discussion in  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  489 \S\ref{polymorphic}.  105 216d6ed87399 Initial revision lcp parents: diff changeset  490 216d6ed87399 Initial revision lcp parents: diff changeset  491 A type constructor may be overloaded (subject to certain conditions) by  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  492 appearing in several arity declarations. For instance, the function type  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  493 constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order  105 216d6ed87399 Initial revision lcp parents: diff changeset  494 logic, it is declared also to have arity $(term,term)term$.  216d6ed87399 Initial revision lcp parents: diff changeset  495 216d6ed87399 Initial revision lcp parents: diff changeset  496 Theory {\tt List} declares the 1-place type constructor $list$, gives  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  497 it arity $(term)term$, and declares constants $Nil$ and $Cons$ with  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  498 polymorphic types:%  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  499 \footnote{In the {\tt consts} part, type variable {\tt'a} has the default  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  500  sort, which is {\tt term}. See the {\em Reference Manual\/}  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  501 \iflabelundefined{sec:ref-defining-theories}{}%  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  502 {(\S\ref{sec:ref-defining-theories})} for more information.}  105 216d6ed87399 Initial revision lcp parents: diff changeset  503 \index{examples!of theories}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  504 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  505 List = FOL +  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  506 types 'a list  105 216d6ed87399 Initial revision lcp parents: diff changeset  507 arities list :: (term)term  216d6ed87399 Initial revision lcp parents: diff changeset  508 consts Nil :: "'a list"  216d6ed87399 Initial revision lcp parents: diff changeset  509  Cons :: "['a, 'a list] => 'a list"  216d6ed87399 Initial revision lcp parents: diff changeset  510 end  216d6ed87399 Initial revision lcp parents: diff changeset  511 \end{ttbox}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  512 Multiple arity declarations may be abbreviated to a single line:  105 216d6ed87399 Initial revision lcp parents: diff changeset  513 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  514 arities $$tycon@1$$, \ldots, $$tycon@n$$ :: $$arity$$  216d6ed87399 Initial revision lcp parents: diff changeset  515 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  516 216d6ed87399 Initial revision lcp parents: diff changeset  517 \begin{warn}  216d6ed87399 Initial revision lcp parents: diff changeset  518 Arity declarations resemble constant declarations, but there are {\it no\/}  216d6ed87399 Initial revision lcp parents: diff changeset  519 quotation marks! Types and rules must be quoted because the theory  216d6ed87399 Initial revision lcp parents: diff changeset  520 translator passes them verbatim to the {\ML} output file.  216d6ed87399 Initial revision lcp parents: diff changeset  521 \end{warn}  216d6ed87399 Initial revision lcp parents: diff changeset  522 331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  523 \subsection{Type synonyms}\indexbold{type synonyms}  303 0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  524 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  525 to those found in \ML. Such synonyms are defined in the type declaration part  303 0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  526 and are fairly self explanatory:  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  527 \begin{ttbox}  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  528 types gate = "[o,o] => o"  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  529  'a pred = "'a => o"  303 0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  530  ('a,'b)nuf = "'b => 'a"  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  531 \end{ttbox}  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  532 Type declarations and synonyms can be mixed arbitrarily:  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  533 \begin{ttbox}  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  534 types nat  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  535  'a stream = "nat => 'a"  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  536  signal = "nat stream"  303 0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  537  'a list  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  538 \end{ttbox}  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  539 A synonym is merely an abbreviation for some existing type expression. Hence  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  540 synonyms may not be recursive! Internally all synonyms are fully expanded. As  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  541 a consequence Isabelle output never contains synonyms. Their main purpose is  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  542 to improve the readability of theories. Synonyms can be used just like any  303 0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  543 other type:  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  544 \begin{ttbox}  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  545 consts and,or :: "gate"  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  546  negate :: "signal => signal"  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  547 \end{ttbox}  0746399cfd44 added section on type synonyms nipkow parents: 296 diff changeset  548 348 1f5a94209c97 post-CRC corrections lcp parents: 331 diff changeset  549 \subsection{Infix and mixfix operators}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  550 \index{infixes}\index{examples!of theories}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  551 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  552 Infix or mixfix syntax may be attached to constants. Consider the  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  553 following theory:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  554 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  555 Gate2 = FOL +  216d6ed87399 Initial revision lcp parents: diff changeset  556 consts "~&" :: "[o,o] => o" (infixl 35)  216d6ed87399 Initial revision lcp parents: diff changeset  557  "#" :: "[o,o] => o" (infixl 30)  216d6ed87399 Initial revision lcp parents: diff changeset  558 rules nand_def "P ~& Q == ~(P & Q)"  216d6ed87399 Initial revision lcp parents: diff changeset  559  xor_def "P # Q == P & ~Q | ~P & Q"  216d6ed87399 Initial revision lcp parents: diff changeset  560 end  216d6ed87399 Initial revision lcp parents: diff changeset  561 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  562 The constant declaration part declares two left-associating infix operators  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  563 with their priorities, or precedences; they are $\nand$ of priority~35 and  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  564 $\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  565 \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$. Note the quotation  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  566 marks in \verb|"~&"| and \verb|"#"|.  105 216d6ed87399 Initial revision lcp parents: diff changeset  567 216d6ed87399 Initial revision lcp parents: diff changeset  568 The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared  216d6ed87399 Initial revision lcp parents: diff changeset  569 automatically, just as in \ML. Hence you may write propositions like  216d6ed87399 Initial revision lcp parents: diff changeset  570 \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda  216d6ed87399 Initial revision lcp parents: diff changeset  571 Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.  216d6ed87399 Initial revision lcp parents: diff changeset  572 310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  573 \bigskip\index{mixfix declarations}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  574 {\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  575 add a line to the constant declaration part:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  576 \begin{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  577  If :: "[o,o,o] => o" ("if _ then _ else _")  105 216d6ed87399 Initial revision lcp parents: diff changeset  578 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  579 This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  580  if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  581 denote argument positions.  105 216d6ed87399 Initial revision lcp parents: diff changeset  582 310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  583 The declaration above does not allow the {\tt if}-{\tt then}-{\tt else}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  584 construct to be split across several lines, even if it is too long to fit  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  585 on one line. Pretty-printing information can be added to specify the  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  586 layout of mixfix operators. For details, see  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  587 \iflabelundefined{Defining-Logics}%  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  588  {the {\it Reference Manual}, chapter Defining Logics'}%  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  589  {Chap.\ts\ref{Defining-Logics}}.  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  590 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  591 Mixfix declarations can be annotated with priorities, just like  105 216d6ed87399 Initial revision lcp parents: diff changeset  592 infixes. The example above is just a shorthand for  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  593 \begin{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  594  If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)  105 216d6ed87399 Initial revision lcp parents: diff changeset  595 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  596 The numeric components determine priorities. The list of integers  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  597 defines, for each argument position, the minimal priority an expression  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  598 at that position must have. The final integer is the priority of the  105 216d6ed87399 Initial revision lcp parents: diff changeset  599 construct itself. In the example above, any argument expression is  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  600 acceptable because priorities are non-negative, and conditionals may  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  601 appear everywhere because 1000 is the highest priority. On the other  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  602 hand, the declaration  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  603 \begin{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  604  If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)  105 216d6ed87399 Initial revision lcp parents: diff changeset  605 \end{ttbox}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  606 defines concrete syntax for a conditional whose first argument cannot have  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  607 the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  608 of at least~100. We may of course write  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  609 \begin{quote}\tt  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  610 if (if $P$ then $Q$ else $R$) then $S$ else $T$  156 ab4dcb9285e0 Corrected errors found by Marcus Wenzel. lcp parents: 109 diff changeset  611 \end{quote}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  612 because expressions in parentheses have maximal priority.  105 216d6ed87399 Initial revision lcp parents: diff changeset  613 216d6ed87399 Initial revision lcp parents: diff changeset  614 Binary type constructors, like products and sums, may also be declared as  216d6ed87399 Initial revision lcp parents: diff changeset  615 infixes. The type declaration below introduces a type constructor~$*$ with  216d6ed87399 Initial revision lcp parents: diff changeset  616 infix notation $\alpha*\beta$, together with the mixfix notation  216d6ed87399 Initial revision lcp parents: diff changeset  617 ${<}\_,\_{>}$ for pairs.  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  618 \index{examples!of theories}\index{mixfix declarations}  105 216d6ed87399 Initial revision lcp parents: diff changeset  619 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  620 Prod = FOL +  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  621 types ('a,'b) "*" (infixl 20)  105 216d6ed87399 Initial revision lcp parents: diff changeset  622 arities "*" :: (term,term)term  216d6ed87399 Initial revision lcp parents: diff changeset  623 consts fst :: "'a * 'b => 'a"  216d6ed87399 Initial revision lcp parents: diff changeset  624  snd :: "'a * 'b => 'b"  216d6ed87399 Initial revision lcp parents: diff changeset  625  Pair :: "['a,'b] => 'a * 'b" ("(1<_,/_>)")  216d6ed87399 Initial revision lcp parents: diff changeset  626 rules fst "fst() = a"  216d6ed87399 Initial revision lcp parents: diff changeset  627  snd "snd() = b"  216d6ed87399 Initial revision lcp parents: diff changeset  628 end  216d6ed87399 Initial revision lcp parents: diff changeset  629 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  630 216d6ed87399 Initial revision lcp parents: diff changeset  631 \begin{warn}  216d6ed87399 Initial revision lcp parents: diff changeset  632 The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would  216d6ed87399 Initial revision lcp parents: diff changeset  633 be in the case of an infix constant. Only infix type constructors can have  216d6ed87399 Initial revision lcp parents: diff changeset  634 symbolic names like~{\tt *}. There is no general mixfix syntax for types.  216d6ed87399 Initial revision lcp parents: diff changeset  635 \end{warn}  216d6ed87399 Initial revision lcp parents: diff changeset  636 216d6ed87399 Initial revision lcp parents: diff changeset  637 216d6ed87399 Initial revision lcp parents: diff changeset  638 \subsection{Overloading}  216d6ed87399 Initial revision lcp parents: diff changeset  639 \index{overloading}\index{examples!of theories}  216d6ed87399 Initial revision lcp parents: diff changeset  640 The {\bf class declaration part} has the form  216d6ed87399 Initial revision lcp parents: diff changeset  641 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  642 classes $$id@1$$ < $$c@1$$  216d6ed87399 Initial revision lcp parents: diff changeset  643  \vdots  216d6ed87399 Initial revision lcp parents: diff changeset  644  $$id@n$$ < $$c@n$$  216d6ed87399 Initial revision lcp parents: diff changeset  645 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  646 where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are  216d6ed87399 Initial revision lcp parents: diff changeset  647 existing classes. It declares each $id@i$ as a new class, a subclass  216d6ed87399 Initial revision lcp parents: diff changeset  648 of~$c@i$. In the general case, an identifier may be declared to be a  216d6ed87399 Initial revision lcp parents: diff changeset  649 subclass of $k$ existing classes:  216d6ed87399 Initial revision lcp parents: diff changeset  650 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  651  $$id$$ < $$c@1$$, \ldots, $$c@k$$  216d6ed87399 Initial revision lcp parents: diff changeset  652 \end{ttbox}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  653 Type classes allow constants to be overloaded. As suggested in  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  654 \S\ref{polymorphic}, let us define the class $arith$ of arithmetic  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  655 types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  656 \alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  657 $term$ and add the three polymorphic constants of this class.  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  658 \index{examples!of theories}\index{constants!overloaded}  105 216d6ed87399 Initial revision lcp parents: diff changeset  659 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  660 Arith = FOL +  216d6ed87399 Initial revision lcp parents: diff changeset  661 classes arith < term  216d6ed87399 Initial revision lcp parents: diff changeset  662 consts "0" :: "'a::arith" ("0")  216d6ed87399 Initial revision lcp parents: diff changeset  663  "1" :: "'a::arith" ("1")  216d6ed87399 Initial revision lcp parents: diff changeset  664  "+" :: "['a::arith,'a] => 'a" (infixl 60)  216d6ed87399 Initial revision lcp parents: diff changeset  665 end  216d6ed87399 Initial revision lcp parents: diff changeset  666 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  667 No rules are declared for these constants: we merely introduce their  216d6ed87399 Initial revision lcp parents: diff changeset  668 names without specifying properties. On the other hand, classes  216d6ed87399 Initial revision lcp parents: diff changeset  669 with rules make it possible to prove {\bf generic} theorems. Such  216d6ed87399 Initial revision lcp parents: diff changeset  670 theorems hold for all instances, all types in that class.  216d6ed87399 Initial revision lcp parents: diff changeset  671 216d6ed87399 Initial revision lcp parents: diff changeset  672 We can now obtain distinct versions of the constants of $arith$ by  216d6ed87399 Initial revision lcp parents: diff changeset  673 declaring certain types to be of class $arith$. For example, let us  216d6ed87399 Initial revision lcp parents: diff changeset  674 declare the 0-place type constructors $bool$ and $nat$:  216d6ed87399 Initial revision lcp parents: diff changeset  675 \index{examples!of theories}  216d6ed87399 Initial revision lcp parents: diff changeset  676 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  677 BoolNat = Arith +  348 1f5a94209c97 post-CRC corrections lcp parents: 331 diff changeset  678 types bool nat  1f5a94209c97 post-CRC corrections lcp parents: 331 diff changeset  679 arities bool, nat :: arith  105 216d6ed87399 Initial revision lcp parents: diff changeset  680 consts Suc :: "nat=>nat"  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  681 \ttbreak  105 216d6ed87399 Initial revision lcp parents: diff changeset  682 rules add0 "0 + n = n::nat"  216d6ed87399 Initial revision lcp parents: diff changeset  683  addS "Suc(m)+n = Suc(m+n)"  216d6ed87399 Initial revision lcp parents: diff changeset  684  nat1 "1 = Suc(0)"  216d6ed87399 Initial revision lcp parents: diff changeset  685  or0l "0 + x = x::bool"  216d6ed87399 Initial revision lcp parents: diff changeset  686  or0r "x + 0 = x::bool"  216d6ed87399 Initial revision lcp parents: diff changeset  687  or1l "1 + x = 1::bool"  216d6ed87399 Initial revision lcp parents: diff changeset  688  or1r "x + 1 = 1::bool"  216d6ed87399 Initial revision lcp parents: diff changeset  689 end  216d6ed87399 Initial revision lcp parents: diff changeset  690 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  691 Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at  216d6ed87399 Initial revision lcp parents: diff changeset  692 either type. The type constraints in the axioms are vital. Without  216d6ed87399 Initial revision lcp parents: diff changeset  693 constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$  216d6ed87399 Initial revision lcp parents: diff changeset  694 and the axiom would hold for any type of class $arith$. This would  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  695 collapse $nat$ to a trivial type:  105 216d6ed87399 Initial revision lcp parents: diff changeset  696 $Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1!$  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  697 105 216d6ed87399 Initial revision lcp parents: diff changeset  698 296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  699 \section{Theory example: the natural numbers}  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  700 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  701 We shall now work through a small example of formalized mathematics  105 216d6ed87399 Initial revision lcp parents: diff changeset  702 demonstrating many of the theory extension features.  216d6ed87399 Initial revision lcp parents: diff changeset  703 216d6ed87399 Initial revision lcp parents: diff changeset  704 216d6ed87399 Initial revision lcp parents: diff changeset  705 \subsection{Extending first-order logic with the natural numbers}  216d6ed87399 Initial revision lcp parents: diff changeset  706 \index{examples!of theories}  216d6ed87399 Initial revision lcp parents: diff changeset  707 284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  708 Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  709 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  710 Let us introduce the Peano axioms for mathematical induction and the  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  711 freeness of $0$ and~$Suc$:\index{axioms!Peano}  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  712 $\vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}  105 216d6ed87399 Initial revision lcp parents: diff changeset  713  \qquad \parbox{4.5cm}{provided x is not free in any assumption except~P}  216d6ed87399 Initial revision lcp parents: diff changeset  714 $  216d6ed87399 Initial revision lcp parents: diff changeset  715 $\infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad  216d6ed87399 Initial revision lcp parents: diff changeset  716  \infer[(Suc\_neq\_0)]{R}{Suc(m)=0}  216d6ed87399 Initial revision lcp parents: diff changeset  717 $  216d6ed87399 Initial revision lcp parents: diff changeset  718 Mathematical induction asserts that $P(n)$ is true, for any $n::nat$,  216d6ed87399 Initial revision lcp parents: diff changeset  719 provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$.  216d6ed87399 Initial revision lcp parents: diff changeset  720 Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.  216d6ed87399 Initial revision lcp parents: diff changeset  721 To avoid making induction require the presence of other connectives, we  216d6ed87399 Initial revision lcp parents: diff changeset  722 formalize mathematical induction as  216d6ed87399 Initial revision lcp parents: diff changeset  723 $$\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct)$$  216d6ed87399 Initial revision lcp parents: diff changeset  724 216d6ed87399 Initial revision lcp parents: diff changeset  725 \noindent  216d6ed87399 Initial revision lcp parents: diff changeset  726 Similarly, to avoid expressing the other rules using~$\forall$, $\imp$  216d6ed87399 Initial revision lcp parents: diff changeset  727 and~$\neg$, we take advantage of the meta-logic;\footnote  216d6ed87399 Initial revision lcp parents: diff changeset  728 {On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$  216d6ed87399 Initial revision lcp parents: diff changeset  729 and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work  216d6ed87399 Initial revision lcp parents: diff changeset  730 better with Isabelle's simplifier.}  216d6ed87399 Initial revision lcp parents: diff changeset  731 $(Suc\_neq\_0)$ is  216d6ed87399 Initial revision lcp parents: diff changeset  732 an elimination rule for $Suc(m)=0$:  216d6ed87399 Initial revision lcp parents: diff changeset  733 $$Suc(m)=Suc(n) \Imp m=n \eqno(Suc\_inject)$$  216d6ed87399 Initial revision lcp parents: diff changeset  734 $$Suc(m)=0 \Imp R \eqno(Suc\_neq\_0)$$  216d6ed87399 Initial revision lcp parents: diff changeset  735 216d6ed87399 Initial revision lcp parents: diff changeset  736 \noindent  216d6ed87399 Initial revision lcp parents: diff changeset  737 We shall also define a primitive recursion operator, $rec$. Traditionally,  216d6ed87399 Initial revision lcp parents: diff changeset  738 primitive recursion takes a natural number~$a$ and a 2-place function~$f$,  216d6ed87399 Initial revision lcp parents: diff changeset  739 and obeys the equations  216d6ed87399 Initial revision lcp parents: diff changeset  740 \begin{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  741  rec(0,a,f) & = & a \\  216d6ed87399 Initial revision lcp parents: diff changeset  742  rec(Suc(m),a,f) & = & f(m, rec(m,a,f))  216d6ed87399 Initial revision lcp parents: diff changeset  743 \end{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  744 Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$,  216d6ed87399 Initial revision lcp parents: diff changeset  745 should satisfy  216d6ed87399 Initial revision lcp parents: diff changeset  746 \begin{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  747  0+n & = & n \\  216d6ed87399 Initial revision lcp parents: diff changeset  748  Suc(m)+n & = & Suc(m+n)  216d6ed87399 Initial revision lcp parents: diff changeset  749 \end{eqnarray*}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  750 Primitive recursion appears to pose difficulties: first-order logic has no  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  751 function-valued expressions. We again take advantage of the meta-logic,  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  752 which does have functions. We also generalise primitive recursion to be  105 216d6ed87399 Initial revision lcp parents: diff changeset  753 polymorphic over any type of class~$term$, and declare the addition  216d6ed87399 Initial revision lcp parents: diff changeset  754 function:  216d6ed87399 Initial revision lcp parents: diff changeset  755 \begin{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  756  rec & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\  216d6ed87399 Initial revision lcp parents: diff changeset  757  + & :: & [nat,nat]\To nat  216d6ed87399 Initial revision lcp parents: diff changeset  758 \end{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  759 216d6ed87399 Initial revision lcp parents: diff changeset  760 216d6ed87399 Initial revision lcp parents: diff changeset  761 \subsection{Declaring the theory to Isabelle}  216d6ed87399 Initial revision lcp parents: diff changeset  762 \index{examples!of theories}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  763 Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,  105 216d6ed87399 Initial revision lcp parents: diff changeset  764 which contains only classical logic with no natural numbers. We declare  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  765 the 0-place type constructor $nat$ and the associated constants. Note that  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  766 the constant~0 requires a mixfix annotation because~0 is not a legal  994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  767 identifier, and could not otherwise be written in terms:  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  768 \begin{ttbox}\index{mixfix declarations}  105 216d6ed87399 Initial revision lcp parents: diff changeset  769 Nat = FOL +  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  770 types nat  105 216d6ed87399 Initial revision lcp parents: diff changeset  771 arities nat :: term  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  772 consts "0" :: "nat" ("0")  105 216d6ed87399 Initial revision lcp parents: diff changeset  773  Suc :: "nat=>nat"  216d6ed87399 Initial revision lcp parents: diff changeset  774  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  775  "+" :: "[nat, nat] => nat" (infixl 60)  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  776 rules Suc_inject "Suc(m)=Suc(n) ==> m=n"  105 216d6ed87399 Initial revision lcp parents: diff changeset  777  Suc_neq_0 "Suc(m)=0 ==> R"  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  778  induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"  105 216d6ed87399 Initial revision lcp parents: diff changeset  779  rec_0 "rec(0,a,f) = a"  216d6ed87399 Initial revision lcp parents: diff changeset  780  rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))"  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  781  add_def "m+n == rec(m, n, \%x y. Suc(y))"  105 216d6ed87399 Initial revision lcp parents: diff changeset  782 end  216d6ed87399 Initial revision lcp parents: diff changeset  783 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  784 In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$.  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  785 Loading this theory file creates the \ML\ structure {\tt Nat}, which  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  786 contains the theory and axioms. Opening structure {\tt Nat} lets us write  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  787 {\tt induct} instead of {\tt Nat.induct}, and so forth.  105 216d6ed87399 Initial revision lcp parents: diff changeset  788 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  789 open Nat;  216d6ed87399 Initial revision lcp parents: diff changeset  790 \end{ttbox}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  791 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  792 \subsection{Proving some recursion equations}  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  793 File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the  105 216d6ed87399 Initial revision lcp parents: diff changeset  794 natural numbers. As a trivial example, let us derive recursion equations  216d6ed87399 Initial revision lcp parents: diff changeset  795 for \verb$+$. Here is the zero case:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  796 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  797 goalw Nat.thy [add_def] "0+n = n";  216d6ed87399 Initial revision lcp parents: diff changeset  798 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  799 {\out 0 + n = n}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  800 {\out 1. rec(0,n,\%x y. Suc(y)) = n}  105 216d6ed87399 Initial revision lcp parents: diff changeset  801 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  802 by (resolve_tac [rec_0] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  803 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  804 {\out 0 + n = n}  216d6ed87399 Initial revision lcp parents: diff changeset  805 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  806 val add_0 = result();  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  807 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  808 And here is the successor case:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  809 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  810 goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";  216d6ed87399 Initial revision lcp parents: diff changeset  811 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  812 {\out Suc(m) + n = Suc(m + n)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  813 {\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}  105 216d6ed87399 Initial revision lcp parents: diff changeset  814 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  815 by (resolve_tac [rec_Suc] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  816 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  817 {\out Suc(m) + n = Suc(m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  818 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  819 val add_Suc = result();  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  820 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  821 The induction rule raises some complications, which are discussed next.  216d6ed87399 Initial revision lcp parents: diff changeset  822 \index{theories!defining|)}  216d6ed87399 Initial revision lcp parents: diff changeset  823 216d6ed87399 Initial revision lcp parents: diff changeset  824 216d6ed87399 Initial revision lcp parents: diff changeset  825 \section{Refinement with explicit instantiation}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  826 \index{resolution!with instantiation}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  827 \index{instantiation|(}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  828 105 216d6ed87399 Initial revision lcp parents: diff changeset  829 In order to employ mathematical induction, we need to refine a subgoal by  216d6ed87399 Initial revision lcp parents: diff changeset  830 the rule~$(induct)$. The conclusion of this rule is $\Var{P}(\Var{n})$,  216d6ed87399 Initial revision lcp parents: diff changeset  831 which is highly ambiguous in higher-order unification. It matches every  216d6ed87399 Initial revision lcp parents: diff changeset  832 way that a formula can be regarded as depending on a subterm of type~$nat$.  216d6ed87399 Initial revision lcp parents: diff changeset  833 To get round this problem, we could make the induction rule conclude  216d6ed87399 Initial revision lcp parents: diff changeset  834 $\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires  216d6ed87399 Initial revision lcp parents: diff changeset  835 refinement by~$(\forall E)$, which is equally hard!  216d6ed87399 Initial revision lcp parents: diff changeset  836 216d6ed87399 Initial revision lcp parents: diff changeset  837 The tactic {\tt res_inst_tac}, like {\tt resolve_tac}, refines a subgoal by  216d6ed87399 Initial revision lcp parents: diff changeset  838 a rule. But it also accepts explicit instantiations for the rule's  216d6ed87399 Initial revision lcp parents: diff changeset  839 schematic variables.  216d6ed87399 Initial revision lcp parents: diff changeset  840 \begin{description}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  841 \item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]  105 216d6ed87399 Initial revision lcp parents: diff changeset  842 instantiates the rule {\it thm} with the instantiations {\it insts}, and  216d6ed87399 Initial revision lcp parents: diff changeset  843 then performs resolution on subgoal~$i$.  216d6ed87399 Initial revision lcp parents: diff changeset  844 310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  845 \item[\ttindex{eres_inst_tac}]  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  846 and \ttindex{dres_inst_tac} are similar, but perform elim-resolution  105 216d6ed87399 Initial revision lcp parents: diff changeset  847 and destruct-resolution, respectively.  216d6ed87399 Initial revision lcp parents: diff changeset  848 \end{description}  216d6ed87399 Initial revision lcp parents: diff changeset  849 The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,  216d6ed87399 Initial revision lcp parents: diff changeset  850 where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---  307 994dbab40849 modifications towards final draft lcp parents: 303 diff changeset  851 with no leading question marks! --- and $e@1$, \ldots, $e@n$ are  105 216d6ed87399 Initial revision lcp parents: diff changeset  852 expressions giving their instantiations. The expressions are type-checked  216d6ed87399 Initial revision lcp parents: diff changeset  853 in the context of a particular subgoal: free variables receive the same  216d6ed87399 Initial revision lcp parents: diff changeset  854 types as they have in the subgoal, and parameters may appear. Type  216d6ed87399 Initial revision lcp parents: diff changeset  855 variable instantiations may appear in~{\it insts}, but they are seldom  216d6ed87399 Initial revision lcp parents: diff changeset  856 required: {\tt res_inst_tac} instantiates type variables automatically  216d6ed87399 Initial revision lcp parents: diff changeset  857 whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.  216d6ed87399 Initial revision lcp parents: diff changeset  858 216d6ed87399 Initial revision lcp parents: diff changeset  859 \subsection{A simple proof by induction}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  860 \index{examples!of induction}  105 216d6ed87399 Initial revision lcp parents: diff changeset  861 Let us prove that no natural number~$k$ equals its own successor. To  216d6ed87399 Initial revision lcp parents: diff changeset  862 use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good  216d6ed87399 Initial revision lcp parents: diff changeset  863 instantiation for~$\Var{P}$.  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  864 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  865 goal Nat.thy "~ (Suc(k) = k)";  216d6ed87399 Initial revision lcp parents: diff changeset  866 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  867 {\out ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  868 {\out 1. ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  869 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  870 by (res_inst_tac [("n","k")] induct 1);  216d6ed87399 Initial revision lcp parents: diff changeset  871 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  872 {\out ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  873 {\out 1. ~Suc(0) = 0}  216d6ed87399 Initial revision lcp parents: diff changeset  874 {\out 2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  875 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  876 We should check that Isabelle has correctly applied induction. Subgoal~1  216d6ed87399 Initial revision lcp parents: diff changeset  877 is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step,  216d6ed87399 Initial revision lcp parents: diff changeset  878 with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  879 The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  880 other rules of theory {\tt Nat}. The base case holds by~\ttindex{Suc_neq_0}:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  881 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  882 by (resolve_tac [notI] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  883 {\out Level 2}  216d6ed87399 Initial revision lcp parents: diff changeset  884 {\out ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  885 {\out 1. Suc(0) = 0 ==> False}  216d6ed87399 Initial revision lcp parents: diff changeset  886 {\out 2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}  216d6ed87399 Initial revision lcp parents: diff changeset  887 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  888 by (eresolve_tac [Suc_neq_0] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  889 {\out Level 3}  216d6ed87399 Initial revision lcp parents: diff changeset  890 {\out ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  891 {\out 1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  892 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  893 The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  894 Negation rules transform the subgoal into that of proving $Suc(x)=x$ from  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  895 $Suc(Suc(x)) = Suc(x)$:  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  896 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  897 by (resolve_tac [notI] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  898 {\out Level 4}  216d6ed87399 Initial revision lcp parents: diff changeset  899 {\out ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  900 {\out 1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}  216d6ed87399 Initial revision lcp parents: diff changeset  901 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  902 by (eresolve_tac [notE] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  903 {\out Level 5}  216d6ed87399 Initial revision lcp parents: diff changeset  904 {\out ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  905 {\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}  216d6ed87399 Initial revision lcp parents: diff changeset  906 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  907 by (eresolve_tac [Suc_inject] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  908 {\out Level 6}  216d6ed87399 Initial revision lcp parents: diff changeset  909 {\out ~Suc(k) = k}  216d6ed87399 Initial revision lcp parents: diff changeset  910 {\out No subgoals!}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  911 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  912 216d6ed87399 Initial revision lcp parents: diff changeset  913 216d6ed87399 Initial revision lcp parents: diff changeset  914 \subsection{An example of ambiguity in {\tt resolve_tac}}  216d6ed87399 Initial revision lcp parents: diff changeset  915 \index{examples!of induction}\index{unification!higher-order}  216d6ed87399 Initial revision lcp parents: diff changeset  916 If you try the example above, you may observe that {\tt res_inst_tac} is  216d6ed87399 Initial revision lcp parents: diff changeset  917 not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right  216d6ed87399 Initial revision lcp parents: diff changeset  918 instantiation for~$(induct)$ to yield the desired next state. With more  216d6ed87399 Initial revision lcp parents: diff changeset  919 complex formulae, our luck fails.  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  920 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  921 goal Nat.thy "(k+m)+n = k+(m+n)";  216d6ed87399 Initial revision lcp parents: diff changeset  922 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  923 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  924 {\out 1. k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  925 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  926 by (resolve_tac [induct] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  927 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  928 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  929 {\out 1. k + m + n = 0}  216d6ed87399 Initial revision lcp parents: diff changeset  930 {\out 2. !!x. k + m + n = x ==> k + m + n = Suc(x)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  931 \end{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  932 This proof requires induction on~$k$. The occurrence of~0 in subgoal~1  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  933 indicates that induction has been applied to the term~$k+(m+n)$; this  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  934 application is sound but will not lead to a proof here. Fortunately,  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  935 Isabelle can (lazily!) generate all the valid applications of induction.  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  936 The \ttindex{back} command causes backtracking to an alternative outcome of  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  937 the tactic.  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  938 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  939 back();  216d6ed87399 Initial revision lcp parents: diff changeset  940 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  941 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  942 {\out 1. k + m + n = k + 0}  216d6ed87399 Initial revision lcp parents: diff changeset  943 {\out 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  944 \end{ttbox}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  945 Now induction has been applied to~$m+n$. This is equally useless. Let us  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  946 call \ttindex{back} again.  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  947 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  948 back();  216d6ed87399 Initial revision lcp parents: diff changeset  949 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  950 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  951 {\out 1. k + m + 0 = k + (m + 0)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  952 {\out 2. !!x. k + m + x = k + (m + x) ==>}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  953 {\out k + m + Suc(x) = k + (m + Suc(x))}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  954 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  955 Now induction has been applied to~$n$. What is the next alternative?  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  956 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  957 back();  216d6ed87399 Initial revision lcp parents: diff changeset  958 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  959 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  960 {\out 1. k + m + n = k + (m + 0)}  216d6ed87399 Initial revision lcp parents: diff changeset  961 {\out 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  962 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  963 Inspecting subgoal~1 reveals that induction has been applied to just the  216d6ed87399 Initial revision lcp parents: diff changeset  964 second occurrence of~$n$. This perfectly legitimate induction is useless  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  965 here.  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  966 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  967 The main goal admits fourteen different applications of induction. The  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  968 number is exponential in the size of the formula.  105 216d6ed87399 Initial revision lcp parents: diff changeset  969 216d6ed87399 Initial revision lcp parents: diff changeset  970 \subsection{Proving that addition is associative}  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  971 Let us invoke the induction rule properly, using~{\tt  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  972  res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  973 simplification tactics, which are described in  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  974 \iflabelundefined{simp-chap}%  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  975  {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  976 310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  977 \index{simplification}\index{examples!of simplification}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  978 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  979 Isabelle's simplification tactics repeatedly apply equations to a subgoal,  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  980 perhaps proving it. For efficiency, the rewrite rules must be  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  981 packaged into a {\bf simplification set},\index{simplification sets}  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  982 or {\bf simpset}. We take the standard simpset for first-order logic and  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  983 insert the equations proved in the previous section, namely  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  984 $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  985 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  986 val add_ss = FOL_ss addrews [add_0, add_Suc];  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  987 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  988 We state the goal for associativity of addition, and  216d6ed87399 Initial revision lcp parents: diff changeset  989 use \ttindex{res_inst_tac} to invoke induction on~$k$:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  990 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  991 goal Nat.thy "(k+m)+n = k+(m+n)";  216d6ed87399 Initial revision lcp parents: diff changeset  992 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  993 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  994 {\out 1. k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  995 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  996 by (res_inst_tac [("n","k")] induct 1);  216d6ed87399 Initial revision lcp parents: diff changeset  997 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  998 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  999 {\out 1. 0 + m + n = 0 + (m + n)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1000 {\out 2. !!x. x + m + n = x + (m + n) ==>}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1001 {\out Suc(x) + m + n = Suc(x) + (m + n)}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1002 \end{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  1003 The base case holds easily; both sides reduce to $m+n$. The  216d6ed87399 Initial revision lcp parents: diff changeset  1004 tactic~\ttindex{simp_tac} rewrites with respect to the given simplification  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  1005 set, applying the rewrite rules for addition:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1006 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  1007 by (simp_tac add_ss 1);  216d6ed87399 Initial revision lcp parents: diff changeset  1008 {\out Level 2}  216d6ed87399 Initial revision lcp parents: diff changeset  1009 {\out k + m + n = k + (m + n)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1010 {\out 1. !!x. x + m + n = x + (m + n) ==>}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1011 {\out Suc(x) + m + n = Suc(x) + (m + n)}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1012 \end{ttbox}  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  1013 The inductive step requires rewriting by the equations for addition  105 216d6ed87399 Initial revision lcp parents: diff changeset  1014 together the induction hypothesis, which is also an equation. The  216d6ed87399 Initial revision lcp parents: diff changeset  1015 tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any  216d6ed87399 Initial revision lcp parents: diff changeset  1016 useful assumptions:  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1017 \begin{ttbox}  105 216d6ed87399 Initial revision lcp parents: diff changeset  1018 by (asm_simp_tac add_ss 1);  216d6ed87399 Initial revision lcp parents: diff changeset  1019 {\out Level 3}  216d6ed87399 Initial revision lcp parents: diff changeset  1020 {\out k + m + n = k + (m + n)}  216d6ed87399 Initial revision lcp parents: diff changeset  1021 {\out No subgoals!}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1022 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1023 \index{instantiation|)}  105 216d6ed87399 Initial revision lcp parents: diff changeset  1024 216d6ed87399 Initial revision lcp parents: diff changeset  1025 284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1026 \section{A Prolog interpreter}  105 216d6ed87399 Initial revision lcp parents: diff changeset  1027 \index{Prolog interpreter|bold}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1028 To demonstrate the power of tacticals, let us construct a Prolog  105 216d6ed87399 Initial revision lcp parents: diff changeset  1029 interpreter and execute programs involving lists.\footnote{To run these  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  1030 examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program  105 216d6ed87399 Initial revision lcp parents: diff changeset  1031 consists of a theory. We declare a type constructor for lists, with an  216d6ed87399 Initial revision lcp parents: diff changeset  1032 arity declaration to say that $(\tau)list$ is of class~$term$  216d6ed87399 Initial revision lcp parents: diff changeset  1033 provided~$\tau$ is:  216d6ed87399 Initial revision lcp parents: diff changeset  1034 \begin{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  1035  list & :: & (term)term  216d6ed87399 Initial revision lcp parents: diff changeset  1036 \end{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  1037 We declare four constants: the empty list~$Nil$; the infix list  216d6ed87399 Initial revision lcp parents: diff changeset  1038 constructor~{:}; the list concatenation predicate~$app$; the list reverse  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1039 predicate~$rev$. (In Prolog, functions on lists are expressed as  105 216d6ed87399 Initial revision lcp parents: diff changeset  1040 predicates.)  216d6ed87399 Initial revision lcp parents: diff changeset  1041 \begin{eqnarray*}  216d6ed87399 Initial revision lcp parents: diff changeset  1042  Nil & :: & \alpha list \\  216d6ed87399 Initial revision lcp parents: diff changeset  1043  {:} & :: & [\alpha,\alpha list] \To \alpha list \\  216d6ed87399 Initial revision lcp parents: diff changeset  1044  app & :: & [\alpha list,\alpha list,\alpha list] \To o \\  216d6ed87399 Initial revision lcp parents: diff changeset  1045  rev & :: & [\alpha list,\alpha list] \To o  216d6ed87399 Initial revision lcp parents: diff changeset  1046 \end{eqnarray*}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1047 The predicate $app$ should satisfy the Prolog-style rules  105 216d6ed87399 Initial revision lcp parents: diff changeset  1048 ${app(Nil,ys,ys)} \qquad  216d6ed87399 Initial revision lcp parents: diff changeset  1049  {app(xs,ys,zs) \over app(x:xs, ys, x:zs)}$  216d6ed87399 Initial revision lcp parents: diff changeset  1050 We define the naive version of $rev$, which calls~$app$:  216d6ed87399 Initial revision lcp parents: diff changeset  1051 ${rev(Nil,Nil)} \qquad  216d6ed87399 Initial revision lcp parents: diff changeset  1052  {rev(xs,ys)\quad app(ys, x:Nil, zs) \over  216d6ed87399 Initial revision lcp parents: diff changeset  1053  rev(x:xs, zs)}  216d6ed87399 Initial revision lcp parents: diff changeset  1054 $  216d6ed87399 Initial revision lcp parents: diff changeset  1055 216d6ed87399 Initial revision lcp parents: diff changeset  1056 \index{examples!of theories}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1057 Theory \thydx{Prolog} extends first-order logic in order to make use  105 216d6ed87399 Initial revision lcp parents: diff changeset  1058 of the class~$term$ and the type~$o$. The interpreter does not use the  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1059 rules of~{\tt FOL}.  105 216d6ed87399 Initial revision lcp parents: diff changeset  1060 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1061 Prolog = FOL +  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  1062 types 'a list  105 216d6ed87399 Initial revision lcp parents: diff changeset  1063 arities list :: (term)term  216d6ed87399 Initial revision lcp parents: diff changeset  1064 consts Nil :: "'a list"  216d6ed87399 Initial revision lcp parents: diff changeset  1065  ":" :: "['a, 'a list]=> 'a list" (infixr 60)  216d6ed87399 Initial revision lcp parents: diff changeset  1066  app :: "['a list, 'a list, 'a list] => o"  216d6ed87399 Initial revision lcp parents: diff changeset  1067  rev :: "['a list, 'a list] => o"  216d6ed87399 Initial revision lcp parents: diff changeset  1068 rules appNil "app(Nil,ys,ys)"  216d6ed87399 Initial revision lcp parents: diff changeset  1069  appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"  216d6ed87399 Initial revision lcp parents: diff changeset  1070  revNil "rev(Nil,Nil)"  216d6ed87399 Initial revision lcp parents: diff changeset  1071  revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"  216d6ed87399 Initial revision lcp parents: diff changeset  1072 end  216d6ed87399 Initial revision lcp parents: diff changeset  1073 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1074 \subsection{Simple executions}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1075 Repeated application of the rules solves Prolog goals. Let us  105 216d6ed87399 Initial revision lcp parents: diff changeset  1076 append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the  216d6ed87399 Initial revision lcp parents: diff changeset  1077 answer builds up in~{\tt ?x}.  216d6ed87399 Initial revision lcp parents: diff changeset  1078 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1079 goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)";  216d6ed87399 Initial revision lcp parents: diff changeset  1080 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  1081 {\out app(a : b : c : Nil, d : e : Nil, ?x)}  216d6ed87399 Initial revision lcp parents: diff changeset  1082 {\out 1. app(a : b : c : Nil, d : e : Nil, ?x)}  216d6ed87399 Initial revision lcp parents: diff changeset  1083 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1084 by (resolve_tac [appNil,appCons] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  1085 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1086 {\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)}  216d6ed87399 Initial revision lcp parents: diff changeset  1087 {\out 1. app(b : c : Nil, d : e : Nil, ?zs1)}  216d6ed87399 Initial revision lcp parents: diff changeset  1088 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1089 by (resolve_tac [appNil,appCons] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  1090 {\out Level 2}  216d6ed87399 Initial revision lcp parents: diff changeset  1091 {\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)}  216d6ed87399 Initial revision lcp parents: diff changeset  1092 {\out 1. app(c : Nil, d : e : Nil, ?zs2)}  216d6ed87399 Initial revision lcp parents: diff changeset  1093 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1094 At this point, the first two elements of the result are~$a$ and~$b$.  216d6ed87399 Initial revision lcp parents: diff changeset  1095 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1096 by (resolve_tac [appNil,appCons] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  1097 {\out Level 3}  216d6ed87399 Initial revision lcp parents: diff changeset  1098 {\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)}  216d6ed87399 Initial revision lcp parents: diff changeset  1099 {\out 1. app(Nil, d : e : Nil, ?zs3)}  216d6ed87399 Initial revision lcp parents: diff changeset  1100 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1101 by (resolve_tac [appNil,appCons] 1);  216d6ed87399 Initial revision lcp parents: diff changeset  1102 {\out Level 4}  216d6ed87399 Initial revision lcp parents: diff changeset  1103 {\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1104 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1105 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1106 284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1107 Prolog can run functions backwards. Which list can be appended  105 216d6ed87399 Initial revision lcp parents: diff changeset  1108 with $[c,d]$ to produce $[a,b,c,d]$?  216d6ed87399 Initial revision lcp parents: diff changeset  1109 Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:  216d6ed87399 Initial revision lcp parents: diff changeset  1110 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1111 goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)";  216d6ed87399 Initial revision lcp parents: diff changeset  1112 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  1113 {\out app(?x, c : d : Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1114 {\out 1. app(?x, c : d : Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1115 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1116 by (REPEAT (resolve_tac [appNil,appCons] 1));  216d6ed87399 Initial revision lcp parents: diff changeset  1117 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1118 {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1119 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1120 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1121 216d6ed87399 Initial revision lcp parents: diff changeset  1122 310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1123 \subsection{Backtracking}\index{backtracking!Prolog style}  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  1124 Prolog backtracking can answer questions that have multiple solutions.  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  1125 Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$? This  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  1126 question has five solutions. Using \ttindex{REPEAT} to apply the rules, we  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  1127 quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$:  105 216d6ed87399 Initial revision lcp parents: diff changeset  1128 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1129 goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)";  216d6ed87399 Initial revision lcp parents: diff changeset  1130 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  1131 {\out app(?x, ?y, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1132 {\out 1. app(?x, ?y, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1133 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1134 by (REPEAT (resolve_tac [appNil,appCons] 1));  216d6ed87399 Initial revision lcp parents: diff changeset  1135 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1136 {\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1137 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1138 \end{ttbox}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1139 Isabelle can lazily generate all the possibilities. The \ttindex{back}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1140 command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:  105 216d6ed87399 Initial revision lcp parents: diff changeset  1141 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1142 back();  216d6ed87399 Initial revision lcp parents: diff changeset  1143 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1144 {\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1145 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1146 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1147 The other solutions are generated similarly.  216d6ed87399 Initial revision lcp parents: diff changeset  1148 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1149 back();  216d6ed87399 Initial revision lcp parents: diff changeset  1150 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1151 {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1152 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1153 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1154 back();  216d6ed87399 Initial revision lcp parents: diff changeset  1155 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1156 {\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1157 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1158 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1159 back();  216d6ed87399 Initial revision lcp parents: diff changeset  1160 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1161 {\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1162 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1163 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1164 216d6ed87399 Initial revision lcp parents: diff changeset  1165 216d6ed87399 Initial revision lcp parents: diff changeset  1166 \subsection{Depth-first search}  216d6ed87399 Initial revision lcp parents: diff changeset  1167 \index{search!depth-first}  216d6ed87399 Initial revision lcp parents: diff changeset  1168 Now let us try $rev$, reversing a list.  216d6ed87399 Initial revision lcp parents: diff changeset  1169 Bundle the rules together as the \ML{} identifier {\tt rules}. Naive  216d6ed87399 Initial revision lcp parents: diff changeset  1170 reverse requires 120 inferences for this 14-element list, but the tactic  216d6ed87399 Initial revision lcp parents: diff changeset  1171 terminates in a few seconds.  216d6ed87399 Initial revision lcp parents: diff changeset  1172 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1173 goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";  216d6ed87399 Initial revision lcp parents: diff changeset  1174 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  1175 {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1176 {\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1177 {\out ?w)}  1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1178 \ttbreak  105 216d6ed87399 Initial revision lcp parents: diff changeset  1179 val rules = [appNil,appCons,revNil,revCons];  216d6ed87399 Initial revision lcp parents: diff changeset  1180 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1181 by (REPEAT (resolve_tac rules 1));  216d6ed87399 Initial revision lcp parents: diff changeset  1182 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1183 {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}  216d6ed87399 Initial revision lcp parents: diff changeset  1184 {\out n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1185 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1186 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1187 We may execute $rev$ backwards. This, too, should reverse a list. What  216d6ed87399 Initial revision lcp parents: diff changeset  1188 is the reverse of $[a,b,c]$?  216d6ed87399 Initial revision lcp parents: diff changeset  1189 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1190 goal Prolog.thy "rev(?x, a:b:c:Nil)";  216d6ed87399 Initial revision lcp parents: diff changeset  1191 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  1192 {\out rev(?x, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1193 {\out 1. rev(?x, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1194 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1195 by (REPEAT (resolve_tac rules 1));  216d6ed87399 Initial revision lcp parents: diff changeset  1196 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1197 {\out rev(?x1 : Nil, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1198 {\out 1. app(Nil, ?x1 : Nil, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1199 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1200 The tactic has failed to find a solution! It reached a dead end at  331 13660d5f6a77 final Springer copy lcp parents: 310 diff changeset  1201 subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$  105 216d6ed87399 Initial revision lcp parents: diff changeset  1202 equals~$[a,b,c]$. Backtracking explores other outcomes.  216d6ed87399 Initial revision lcp parents: diff changeset  1203 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1204 back();  216d6ed87399 Initial revision lcp parents: diff changeset  1205 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1206 {\out rev(?x1 : a : Nil, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1207 {\out 1. app(Nil, ?x1 : Nil, b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1208 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1209 This too is a dead end, but the next outcome is successful.  216d6ed87399 Initial revision lcp parents: diff changeset  1210 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1211 back();  216d6ed87399 Initial revision lcp parents: diff changeset  1212 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1213 {\out rev(c : b : a : Nil, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1214 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1215 \end{ttbox}  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1216 \ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1217 search tactical. {\tt REPEAT} stops when it cannot continue, regardless of  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1218 which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a  66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1219 satisfactory state, as specified by an \ML{} predicate. Below,  105 216d6ed87399 Initial revision lcp parents: diff changeset  1220 \ttindex{has_fewer_prems} specifies that the proof state should have no  310 66fc71f3a347 penultimate Springer draft lcp parents: 307 diff changeset  1221 subgoals.  105 216d6ed87399 Initial revision lcp parents: diff changeset  1222 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1223 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)  216d6ed87399 Initial revision lcp parents: diff changeset  1224  (resolve_tac rules 1);  216d6ed87399 Initial revision lcp parents: diff changeset  1225 \end{ttbox}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1226 Since Prolog uses depth-first search, this tactic is a (slow!)  296 e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  1227 Prolog interpreter. We return to the start of the proof using  e1f6cd9f682e revisions to first Springer draft lcp parents: 284 diff changeset  1228 \ttindex{choplev}, and apply {\tt prolog_tac}:  105 216d6ed87399 Initial revision lcp parents: diff changeset  1229 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1230 choplev 0;  216d6ed87399 Initial revision lcp parents: diff changeset  1231 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  1232 {\out rev(?x, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1233 {\out 1. rev(?x, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1234 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1235 by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1));  216d6ed87399 Initial revision lcp parents: diff changeset  1236 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1237 {\out rev(c : b : a : Nil, a : b : c : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1238 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1239 \end{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1240 Let us try {\tt prolog_tac} on one more example, containing four unknowns:  216d6ed87399 Initial revision lcp parents: diff changeset  1241 \begin{ttbox}  216d6ed87399 Initial revision lcp parents: diff changeset  1242 goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)";  216d6ed87399 Initial revision lcp parents: diff changeset  1243 {\out Level 0}  216d6ed87399 Initial revision lcp parents: diff changeset  1244 {\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}  216d6ed87399 Initial revision lcp parents: diff changeset  1245 {\out 1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}  216d6ed87399 Initial revision lcp parents: diff changeset  1246 \ttbreak  216d6ed87399 Initial revision lcp parents: diff changeset  1247 by prolog_tac;  216d6ed87399 Initial revision lcp parents: diff changeset  1248 {\out Level 1}  216d6ed87399 Initial revision lcp parents: diff changeset  1249 {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}  216d6ed87399 Initial revision lcp parents: diff changeset  1250 {\out No subgoals!}  216d6ed87399 Initial revision lcp parents: diff changeset  1251 \end{ttbox}  284 1072b18b2caa First draft of Springer book lcp parents: 156 diff changeset  1252 Although Isabelle is much slower than a Prolog system, Isabelle  156 ab4dcb9285e0 Corrected errors found by Marcus Wenzel. lcp parents: 109 diff changeset  1253 tactics can exploit logic programming techniques.  ab4dcb9285e0 Corrected errors found by Marcus Wenzel. lcp parents: 109 diff changeset  1254`