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 |
3 Let us consider how to perform simple proofs using Isabelle. At |
4 present, Isabelle's user interface is \ML. Proofs are conducted by |
4 present, Isabelle's user interface is \ML. Proofs are conducted by |
5 applying certain \ML{} functions, which update a stored proof state. |
5 applying certain \ML{} functions, which update a stored proof state. |
6 Basically, all syntax must be expressed using plain {\sc ascii} |
6 Basically, all syntax must be expressed using plain {\sc ascii} |
7 characters. There are also mechanisms built into Isabelle that support |
7 characters. There are also mechanisms built into Isabelle that support |
8 alternative syntaxes, for example using mathematical symbols from a |
8 alternative syntaxes, for example using mathematical symbols from a |
9 special screen font. The meta-logic and major object-logics already |
9 special screen font. The meta-logic and major object-logics already |
10 provide such fancy output as an option. |
10 provide such fancy output as an option. |
11 |
11 |
12 Object-logics are built upon Pure Isabelle, which implements the |
12 Object-logics are built upon Pure Isabelle, which implements the |
13 meta-logic and provides certain fundamental data structures: types, |
13 meta-logic and provides certain fundamental data structures: types, |
14 terms, signatures, theorems and theories, tactics and tacticals. |
14 terms, signatures, theorems and theories, tactics and tacticals. |
597 \index{examples!with quantifiers} |
597 \index{examples!with quantifiers} |
598 Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an |
598 Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an |
599 attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former |
599 attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former |
600 proof succeeds, and the latter fails, because of the scope of quantified |
600 proof succeeds, and the latter fails, because of the scope of quantified |
601 variables~\cite{paulson-found}. Unification helps even in these trivial |
601 variables~\cite{paulson-found}. Unification helps even in these trivial |
602 proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$, |
602 proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$, |
603 but we need never say so. This choice is forced by the reflexive law for |
603 but we need never say so. This choice is forced by the reflexive law for |
604 equality, and happens automatically. |
604 equality, and happens automatically. |
605 |
605 |
606 \paragraph{The successful proof.} |
606 \paragraph{The successful proof.} |
607 The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules |
607 The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules |
608 $(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$: |
608 $(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$: |