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