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