1 %% $Id$ |
1 %% $Id$ |
2 \part{Getting Started with Isabelle}\label{chap:getting} |
2 \part{Getting Started with Isabelle}\label{chap:getting} |
3 Let us consider how to perform simple proofs using Isabelle. At present, |
3 Let us consider how to perform simple proofs using Isabelle. At |
4 Isabelle's user interface is \ML. Proofs are conducted by applying certain |
4 present, Isabelle's user interface is \ML. Proofs are conducted by |
5 \ML{} functions, which update a stored proof state. All syntax must be |
5 applying certain \ML{} functions, which update a stored proof state. |
6 expressed using {\sc ascii} characters. Menu-driven graphical interfaces |
6 Basically, all syntax must be expressed using plain {\sc ascii} |
7 are under construction, but Isabelle users will always need to know some |
7 characters. There are also mechanisms built into Isabelle that support |
8 \ML, at least to use tacticals. |
8 alternative syntaxes, for example using mathematical symbols from a |
9 |
9 special screen font. The meta-logic and major object-logics already |
10 Object-logics are built upon Pure Isabelle, which implements the meta-logic |
10 provide such fancy output as an option. |
11 and provides certain fundamental data structures: types, terms, signatures, |
11 |
12 theorems and theories, tactics and tacticals. These data structures have |
12 %FIXME remove |
13 the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm}, |
13 %Menu-driven graphical interfaces are under construction, but Isabelle |
14 {\tt theory} and {\tt tactic}; tacticals have function types such as {\tt |
14 %users will always need to know some \ML, at least to use tacticals. |
15 tactic->tactic}. Isabelle users can operate on these data structures by |
15 |
16 writing \ML{} programs. |
16 Object-logics are built upon Pure Isabelle, which implements the |
|
17 meta-logic and provides certain fundamental data structures: types, |
|
18 terms, signatures, theorems and theories, tactics and tacticals. |
|
19 These data structures have the corresponding \ML{} types {\tt typ}, |
|
20 {\tt term}, {\tt Sign.sg}, {\tt thm}, {\tt theory} and {\tt tactic}; |
|
21 tacticals have function types such as {\tt tactic->tactic}. Isabelle |
|
22 users can operate on these data structures by writing \ML{} programs. |
17 |
23 |
18 \section{Forward proof}\label{sec:forward} \index{forward proof|(} |
24 \section{Forward proof}\label{sec:forward} \index{forward proof|(} |
19 This section describes the concrete syntax for types, terms and theorems, |
25 This section describes the concrete syntax for types, terms and theorems, |
20 and demonstrates forward proof. |
26 and demonstrates forward proof. |
21 |
27 |
63 |
69 |
64 Classes are denoted by identifiers; the built-in class \cldx{logic} |
70 Classes are denoted by identifiers; the built-in class \cldx{logic} |
65 contains the `logical' types. Sorts are lists of classes enclosed in |
71 contains the `logical' types. Sorts are lists of classes enclosed in |
66 braces~\} and \{; singleton sorts may be abbreviated by dropping the braces. |
72 braces~\} and \{; singleton sorts may be abbreviated by dropping the braces. |
67 |
73 |
68 \index{types!syntax of|bold}\index{sort constraints} |
74 \index{types!syntax of|bold}\index{sort constraints} Types are written |
69 Types are written with a syntax like \ML's. The built-in type \tydx{prop} |
75 with a syntax like \ML's. The built-in type \tydx{prop} is the type |
70 is the type of propositions. Type variables can be constrained to particular |
76 of propositions. Type variables can be constrained to particular |
71 classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}. |
77 classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\ttlbrace |
|
78 ord, arith\ttrbrace}. |
72 \[\dquotes |
79 \[\dquotes |
73 \index{*:: symbol}\index{*=> symbol} |
80 \index{*:: symbol}\index{*=> symbol} |
74 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} |
81 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} |
75 \index{*[ symbol}\index{*] symbol} |
82 \index{*[ symbol}\index{*] symbol} |
76 \begin{array}{lll} |
83 \begin{array}{lll} |
77 \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline |
84 \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline |
78 \alpha "::" C & \alpha :: C & \hbox{class constraint} \\ |
85 \alpha "::" C & \alpha :: C & \hbox{class constraint} \\ |
79 \alpha "::" "\{" C@1 "," \ldots "," C@n "\}" & |
86 \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" & |
80 \alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\ |
87 \alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\ |
81 \sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\ |
88 \sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\ |
82 "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau & |
89 "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau & |
83 [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\ |
90 [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\ |
84 "(" \tau@1"," \ldots "," \tau@n ")" tycon & |
91 "(" \tau@1"," \ldots "," \tau@n ")" tycon & |
116 \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\ |
123 \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\ |
117 "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & |
124 "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & |
118 \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\ |
125 \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\ |
119 "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\ |
126 "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\ |
120 "!!" x@1\ldots x@n "." \phi & |
127 "!!" x@1\ldots x@n "." \phi & |
121 \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification} |
128 \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification} |
122 \end{array} |
129 \end{array} |
123 \] |
130 \] |
124 Flex-flex constraints are meta-equalities arising from unification; they |
131 Flex-flex constraints are meta-equalities arising from unification; they |
125 require special treatment. See~\S\ref{flexflex}. |
132 require special treatment. See~\S\ref{flexflex}. |
126 \index{flex-flex constraints} |
133 \index{flex-flex constraints} |
136 it with the symbol {\tt PROP}:\index{*PROP symbol} |
143 it with the symbol {\tt PROP}:\index{*PROP symbol} |
137 \begin{ttbox} |
144 \begin{ttbox} |
138 PROP ?psi ==> PROP ?theta |
145 PROP ?psi ==> PROP ?theta |
139 \end{ttbox} |
146 \end{ttbox} |
140 |
147 |
141 Symbols of object-logics also must be rendered into {\sc ascii}, typically |
148 Symbols of object-logics are typically rendered into {\sc ascii} as |
142 as follows: |
149 follows: |
143 \[ \begin{tabular}{l@{\quad}l@{\quad}l} |
150 \[ \begin{tabular}{l@{\quad}l@{\quad}l} |
144 \tt True & $\top$ & true \\ |
151 \tt True & $\top$ & true \\ |
145 \tt False & $\bot$ & false \\ |
152 \tt False & $\bot$ & false \\ |
146 \tt $P$ \& $Q$ & $P\conj Q$ & conjunction \\ |
153 \tt $P$ \& $Q$ & $P\conj Q$ & conjunction \\ |
147 \tt $P$ | $Q$ & $P\disj Q$ & disjunction \\ |
154 \tt $P$ | $Q$ & $P\disj Q$ & disjunction \\ |
152 \tt EX $x\,y\,z$ .\ $P$ & $\exists x\,y\,z.P$ & there exists |
159 \tt EX $x\,y\,z$ .\ $P$ & $\exists x\,y\,z.P$ & there exists |
153 \end{tabular} |
160 \end{tabular} |
154 \] |
161 \] |
155 To illustrate the notation, consider two axioms for first-order logic: |
162 To illustrate the notation, consider two axioms for first-order logic: |
156 $$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ |
163 $$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ |
157 $$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ |
164 $$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ |
158 Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates into |
165 $({\conj}I)$ translates into {\sc ascii} characters as |
159 {\sc ascii} characters as |
|
160 \begin{ttbox} |
166 \begin{ttbox} |
161 [| ?P; ?Q |] ==> ?P & ?Q |
167 [| ?P; ?Q |] ==> ?P & ?Q |
162 \end{ttbox} |
168 \end{ttbox} |
163 The schematic variables let unification instantiate the rule. To avoid |
169 The schematic variables let unification instantiate the rule. To avoid |
164 cluttering logic definitions with question marks, Isabelle converts any |
170 cluttering logic definitions with question marks, Isabelle converts any |
404 |
410 |
405 \item[\ttindex{by} {\it tactic}; ] |
411 \item[\ttindex{by} {\it tactic}; ] |
406 applies the {\it tactic\/} to the current proof |
412 applies the {\it tactic\/} to the current proof |
407 state, raising an exception if the tactic fails. |
413 state, raising an exception if the tactic fails. |
408 |
414 |
409 \item[\ttindex{undo}(); ] |
415 \item[\ttindex{undo}(); ] |
410 reverts to the previous proof state. Undo can be repeated but cannot be |
416 reverts to the previous proof state. Undo can be repeated but cannot be |
411 undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely |
417 undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely |
412 causes \ML\ to echo the value of that function. |
418 causes \ML\ to echo the value of that function. |
413 |
419 |
414 \item[\ttindex{result}()] |
420 \item[\ttindex{result}();] |
415 returns the theorem just proved, in a standard format. It fails if |
421 returns the theorem just proved, in a standard format. It fails if |
416 unproved subgoals are left, etc. |
422 unproved subgoals are left, etc. |
|
423 |
|
424 \item[\ttindex{qed} {\it name};] is the usual way of ending a proof. |
|
425 It gets the theorem using {\tt result}, stores it in Isabelle's |
|
426 theorem database and binds it to an \ML{} identifier. |
|
427 |
417 \end{ttdescription} |
428 \end{ttdescription} |
418 The commands and tactics given above are cumbersome for interactive use. |
429 The commands and tactics given above are cumbersome for interactive use. |
419 Although our examples will use the full commands, you may prefer Isabelle's |
430 Although our examples will use the full commands, you may prefer Isabelle's |
420 shortcuts: |
431 shortcuts: |
421 \begin{center} \tt |
432 \begin{center} \tt |
492 {\out Level 5} |
503 {\out Level 5} |
493 {\out P | P --> P} |
504 {\out P | P --> P} |
494 {\out No subgoals!} |
505 {\out No subgoals!} |
495 \end{ttbox} |
506 \end{ttbox} |
496 Isabelle tells us that there are no longer any subgoals: the proof is |
507 Isabelle tells us that there are no longer any subgoals: the proof is |
497 complete. Calling {\tt result} returns the theorem. |
508 complete. Calling {\tt qed} stores the theorem. |
498 \begin{ttbox} |
509 \begin{ttbox} |
499 val mythm = result(); |
510 qed "mythm"; |
500 {\out val mythm = "?P | ?P --> ?P" : thm} |
511 {\out val mythm = "?P | ?P --> ?P" : thm} |
501 \end{ttbox} |
512 \end{ttbox} |
502 Isabelle has replaced the free variable~{\tt P} by the scheme |
513 Isabelle has replaced the free variable~{\tt P} by the scheme |
503 variable~{\tt?P}\@. Free variables in the proof state remain fixed |
514 variable~{\tt?P}\@. Free variables in the proof state remain fixed |
504 throughout the proof. Isabelle finally converts them to scheme variables |
515 throughout the proof. Isabelle finally converts them to scheme variables |
662 Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we |
673 Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we |
663 have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}. |
674 have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}. |
664 The reflexivity axiom does not unify with subgoal~1. |
675 The reflexivity axiom does not unify with subgoal~1. |
665 \begin{ttbox} |
676 \begin{ttbox} |
666 by (resolve_tac [refl] 1); |
677 by (resolve_tac [refl] 1); |
667 {\out by: tactic returned no results} |
678 {\out by: tactic failed} |
668 \end{ttbox} |
679 \end{ttbox} |
669 There can be no proof of $\exists y.\forall x.x=y$ by the soundness of |
680 There can be no proof of $\exists y.\forall x.x=y$ by the soundness of |
670 first-order logic. I have elsewhere proved the faithfulness of Isabelle's |
681 first-order logic. I have elsewhere proved the faithfulness of Isabelle's |
671 encoding of first-order logic~\cite{paulson-found}; there could, of course, be |
682 encoding of first-order logic~\cite{paulson-found}; there could, of course, be |
672 faults in the implementation. |
683 faults in the implementation. |
725 instances of~{\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances |
736 instances of~{\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances |
726 of {\tt?y3(z)} can only contain~{\tt z}. Due to the restriction on~{\tt ?x1}, |
737 of {\tt?y3(z)} can only contain~{\tt z}. Due to the restriction on~{\tt ?x1}, |
727 proof by assumption will fail. |
738 proof by assumption will fail. |
728 \begin{ttbox} |
739 \begin{ttbox} |
729 by (assume_tac 1); |
740 by (assume_tac 1); |
730 {\out by: tactic returned no results} |
741 {\out by: tactic failed} |
731 {\out uncaught exception ERROR} |
742 {\out uncaught exception ERROR} |
732 \end{ttbox} |
743 \end{ttbox} |
733 |
744 |
734 \paragraph{The right approach.} |
745 \paragraph{The right approach.} |
735 To do this proof, the rules must be applied in the correct order. |
746 To do this proof, the rules must be applied in the correct order. |