272 \end{ttbox} |
272 \end{ttbox} |
273 \indexbold{*notE} |
273 \indexbold{*notE} |
274 |
274 |
275 \medskip |
275 \medskip |
276 Again, there is a simpler way of conducting this proof. The |
276 Again, there is a simpler way of conducting this proof. The |
277 \ttindex{goalw} command starts unfolds definitions in the premises, as well |
277 \ttindex{goalw} command unfolds definitions in the premises as well |
278 as the conclusion: |
278 as the conclusion: |
279 \begin{ttbox} |
279 \begin{ttbox} |
280 val [major,minor] = goalw FOL.thy [not_def] |
280 val [major,minor] = goalw FOL.thy [not_def] |
281 "[| ~P; P |] ==> R"; |
281 "[| ~P; P |] ==> R"; |
282 {\out val major = "P --> False [~ P]" : thm} |
282 {\out val major = "P --> False [~ P]" : thm} |
562 appear everywhere because 1000 is the highest precedence. On the other |
562 appear everywhere because 1000 is the highest precedence. On the other |
563 hand, |
563 hand, |
564 \begin{ttbox} |
564 \begin{ttbox} |
565 If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99) |
565 If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99) |
566 \end{ttbox} |
566 \end{ttbox} |
567 defines a conditional whose first argument cannot be a conditional because it |
567 defines concrete syntax for a |
568 must have a precedence of at least 100. Precedences only apply to |
568 conditional whose first argument cannot have the form $if~P~then~Q~else~R$ |
569 mixfix syntax: we may write $If(If(P,Q,R),S,T)$. |
569 because it must have a precedence of at least~100. Since expressions put in |
|
570 parentheses have maximal precedence, we may of course write |
|
571 \begin{quote} |
|
572 \it if (if P then Q else R) then S else T |
|
573 \end{quote} |
|
574 Conditional expressions can also be written using the constant {\tt If}. |
570 |
575 |
571 Binary type constructors, like products and sums, may also be declared as |
576 Binary type constructors, like products and sums, may also be declared as |
572 infixes. The type declaration below introduces a type constructor~$*$ with |
577 infixes. The type declaration below introduces a type constructor~$*$ with |
573 infix notation $\alpha*\beta$, together with the mixfix notation |
578 infix notation $\alpha*\beta$, together with the mixfix notation |
574 ${<}\_,\_{>}$ for pairs. |
579 ${<}\_,\_{>}$ for pairs. |
1187 by prolog_tac; |
1192 by prolog_tac; |
1188 {\out Level 1} |
1193 {\out Level 1} |
1189 {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)} |
1194 {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)} |
1190 {\out No subgoals!} |
1195 {\out No subgoals!} |
1191 \end{ttbox} |
1196 \end{ttbox} |
1192 Although Isabelle is much slower than a {\sc Prolog} system, many |
1197 Although Isabelle is much slower than a {\sc Prolog} system, Isabelle |
1193 Isabelle tactics exploit logic programming techniques. For instance, the |
1198 tactics can exploit logic programming techniques. |
1194 simplification tactics prove subgoals of the form $t=\Var{x}$, rewriting~$t$ |
1199 |
1195 and placing the normalised result in~$\Var{x}$. |
|
1196 % Local Variables: |
|
1197 % mode: latex |
|
1198 % TeX-master: t |
|
1199 % End: |
|