# HG changeset patch # User nipkow # Date 1041148584 -3600 # Node ID fb78ee03c391cd376e5d7dd57572a439085179f3 # Parent e3c444e805c4046fab457b9be51224521dacb4db *** empty log message *** diff -r e3c444e805c4 -r fb78ee03c391 doc-src/TutorialI/IsarOverview/Isar/Induction.thy --- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Mon Dec 23 12:01:47 2002 +0100 +++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Sun Dec 29 08:56:24 2002 +0100 @@ -12,34 +12,43 @@ text{* We have already met the @{text cases} method for performing binary case splits. Here is another example: *} -lemma "P \ \ P" +lemma "\ A \ A" proof cases - assume "P" thus ?thesis .. + assume "A" thus ?thesis .. next - assume "\ P" thus ?thesis .. + assume "\ A" thus ?thesis .. qed -text{*\noindent Note that the two cases must come in this order. -This form is appropriate if @{term P} is textually small. However, if -@{term P} is large, we do not want to repeat it. This can be avoided by -the following idiom *} +text{*\noindent The two cases must come in this order because @{text +cases} merely abbreviates @{text"(rule case_split_thm)"} where +@{thm[source] case_split_thm} is @{thm case_split_thm}. If we reverse +the order of the two cases in the proof, the first case would prove +@{prop"\ A \ \ A \ A"} which would solve the first premise of +@{thm[source] case_split_thm}, instantiating @{text ?P} with @{term "\ +A"}, thus making the second premise @{prop"\ \ A \ \ A \ A"}. +Therefore the order of subgoals is not always completely arbitrary. -lemma "P \ \ P" -proof (cases "P") +The above proof is appropriate if @{term A} is textually small. +However, if @{term A} is large, we do not want to repeat it. This can +be avoided by the following idiom *} + +lemma "\ A \ A" +proof (cases "A") case True thus ?thesis .. next case False thus ?thesis .. qed -text{*\noindent which is simply a shorthand for the previous -proof. More precisely, the phrase `\isakeyword{case}~@{text True}' -abbreviates `\isakeyword{assume}~@{text"True: P"}' -and analogously for @{text"False"} and @{prop"\P"}. -In contrast to the previous proof we can prove the cases -in arbitrary order. +text{*\noindent which is like the previous proof but instantiates +@{text ?P} right away with @{term A}. Thus we could prove the two +cases in any order. The phrase `\isakeyword{case}~@{text True}' +abbreviates `\isakeyword{assume}~@{text"True: A"}' and analogously for +@{text"False"} and @{prop"\A"}. -The same game can be played with other datatypes, for example lists: -\tweakskip +The same game can be played with other datatypes, for example lists, +where @{term tl} is the tail of a list, and @{text length} returns a +natual number: +\Tweakskip *} (*<*)declare length_tl[simp del](*>*) lemma "length(tl xs) = length xs - 1" @@ -60,27 +69,15 @@ However, sometimes one may have to. Hence Isar offers a simple scheme for naming those variables: replace the anonymous @{text Cons} by @{text"(Cons y ys)"}, which abbreviates `\isakeyword{fix}~@{text"y ys"} -\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}'. Here -is a (somewhat contrived) example: *} - -lemma "length(tl xs) = length xs - 1" -proof (cases xs) - case Nil thus ?thesis by simp -next - case (Cons y ys) - hence "length(tl xs) = length ys \ length xs = length ys + 1" - by simp - thus ?thesis by simp -qed - -text{* Note that in each \isakeyword{case} the assumption can be +\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}'. +In each \isakeyword{case} the assumption can be referred to inside the proof by the name of the constructor. In Section~\ref{sec:full-Ind} below we will come across an example of this. *} subsection{*Structural induction*} -text{* We start with a simple inductive proof where both cases are proved automatically: *} +text{* We start with an inductive proof where both cases are proved automatically: *} lemma "2 * (\in. (\m. m < n \ P m) \ P n)" @@ -173,7 +170,7 @@ Note that in a nested induction over the same data type, the inner case labels hide the outer ones of the same name. If you want to refer -to the outer ones inside, you need to name them on the outside: +to the outer ones inside, you need to name them on the outside, e.g.\ \isakeyword{note}~@{text"outer_IH = Suc"}. *} subsection{*Rule induction*} @@ -293,10 +290,4 @@ (*<*)lemma "xs \ [] \ rot xs = tl xs @ [hd xs]"(*>*) by (induct xs rule: rot.induct, simp_all) -text{*\small -\paragraph{Acknowledgment} -I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin, -Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer, -Markus Wenzel and three referees commented on and improved this document. -*} (*<*)end(*>*) diff -r e3c444e805c4 -r fb78ee03c391 doc-src/TutorialI/IsarOverview/Isar/Logic.thy --- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Mon Dec 23 12:01:47 2002 +0100 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Sun Dec 29 08:56:24 2002 +0100 @@ -14,26 +14,27 @@ show "A" by(rule a) qed text{*\noindent -The operational reading: the \isakeyword{assume}-\isakeyword{show} block -proves @{prop"A \ A"}, -which rule @{thm[source]impI} (@{thm impI}) -turns into the desired @{prop"A \ A"}. -However, this text is much too detailed for comfort. Therefore Isar -implements the following principle: -\begin{quote}\em -Command \isakeyword{proof} automatically tries to select an introduction rule -based on the goal and a predefined list of rules. -\end{quote} -Here @{thm[source]impI} is applied automatically: -*} +The operational reading: the \isakeyword{assume}-\isakeyword{show} +block proves @{prop"A \ A"} (@{term a} is a degenerate rule (no +assumptions) that proves @{term A} outright), which rule +@{thm[source]impI} (@{thm impI}) turns into the desired @{prop"A \ +A"}. However, this text is much too detailed for comfort. Therefore +Isar implements the following principle: \begin{quote}\em Command +\isakeyword{proof} automatically tries to select an introduction rule +based on the goal and a predefined list of rules. \end{quote} Here +@{thm[source]impI} is applied automatically: *} lemma "A \ A" proof - assume a: "A" - show "A" by(rule a) + assume a: A + show A by(rule a) qed -text{* Trivial proofs, in particular those by assumption, should be trivial +text{*\noindent Single-identifier formulae such as @{term A} need not +be enclosed in double quotes. However, we will continue to do so for +uniformity. + +Trivial proofs, in particular those by assumption, should be trivial to perform. Proof ``.'' does just that (and a bit more). Thus naming of assumptions is often superfluous: *} lemma "A \ A" @@ -54,10 +55,9 @@ A drawback of implicit proofs by assumption is that it is no longer obvious where an assumption is used. -Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} can be -abbreviated to ``..'' -if \emph{name} refers to one of the predefined introduction rules: -*} +Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} +can be abbreviated to ``..'' if \emph{name} refers to one of the +predefined introduction rules (or elimination rules, see below): *} lemma "A \ A \ A" proof @@ -133,14 +133,13 @@ qed text{*\noindent Because of the frequency of \isakeyword{from}~@{text -this} Isar provides two abbreviations: +this}, Isar provides two abbreviations: \begin{center} -\begin{tabular}{rcl} -\isakeyword{then} &=& \isakeyword{from} @{text this} \\ -\isakeyword{thus} &=& \isakeyword{then} \isakeyword{show} +\begin{tabular}{r@ {\quad=\quad}l} +\isakeyword{then} & \isakeyword{from} @{text this} \\ +\isakeyword{thus} & \isakeyword{then} \isakeyword{show} \end{tabular} \end{center} -\medskip Here is an alternative proof that operates purely by forward reasoning: *} lemma "A \ B \ B \ A" @@ -150,35 +149,41 @@ from ab have b: "B" .. from b a show "B \ A" .. qed -text{*\noindent -It is worth examining this text in detail because it exhibits a number of new concepts. -For a start, this is the first time we have proved intermediate propositions -(\isakeyword{have}) on the way to the final \isakeyword{show}. This is the -norm in any nontrivial proof where one cannot bridge the gap between the -assumptions and the conclusion in one step. Both \isakeyword{have}s above are -proved automatically via @{thm[source]conjE} triggered by -\isakeyword{from}~@{text ab}. +text{*\noindent It is worth examining this text in detail because it +exhibits a number of new concepts. For a start, it is the first time +we have proved intermediate propositions (\isakeyword{have}) on the +way to the final \isakeyword{show}. This is the norm in nontrivial +proofs where one cannot bridge the gap between the assumptions and the +conclusion in one step. To understand how the proof works we need to +explain more Isar details. -The \isakeyword{show} command illustrates two things: -\begin{itemize} -\item \isakeyword{from} can be followed by any number of facts. -Given \isakeyword{from}~@{text f}$_1$~\dots~@{text f}$_n$, the -\isakeyword{proof} step after \isakeyword{show} -tries to find an elimination rule whose first $n$ premises can be proved -by the given facts in the given order. -\item If there is no matching elimination rule, introduction rules are tried, -again using the facts to prove the premises. -\end{itemize} -In this case, the proof succeeds with @{thm[source]conjI}. Note that the proof -would fail had we written \isakeyword{from}~@{text"a b"} -instead of \isakeyword{from}~@{text"b a"}. +Method @{text rule} can be given a list of rules, in which case +@{text"(rule"}~\textit{rules}@{text")"} applies the first matching +rule in the list \textit{rules}. Command \isakeyword{from} can be +followed by any number of facts. Given \isakeyword{from}~@{text +f}$_1$~\dots~@{text f}$_n$, the proof step +@{text"(rule"}~\textit{rules}@{text")"} following a \isakeyword{have} +or \isakeyword{show} searches \textit{rules} for a rule whose first +$n$ premises can be proved by @{text f}$_1$~\dots~@{text f}$_n$ in the +given order. Finally one needs to know that ``..'' is short for +@{text"by(rule"}~\textit{elim-rules intro-rules}@{text")"} (or +@{text"by(rule"}~\textit{intro-rules}@{text")"} if there are no facts +fed into the proof), i.e.\ elimination rules are tried before +introduction rules. -This treatment of facts fed into a proof is not restricted to implicit -application of introduction and elimination rules but applies to explicit -application of rules as well. Thus you could replace the final ``..'' above -with \isakeyword{by}@{text"(rule conjI)"}. -*} +Thus in the above proof both \isakeyword{have}s are proved via +@{thm[source]conjE} triggered by \isakeyword{from}~@{text ab} whereas +in the \isakeyword{show} step no elimination rule is applicable and +the proof succeeds with @{thm[source]conjI}. The latter would fail had +we written \isakeyword{from}~@{text"a b"} instead of +\isakeyword{from}~@{text"b a"}. + +Proofs starting with a plain @{text proof} behave the same because the +latter is short for @{text"proof (rule"}~\textit{elim-rules +intro-rules}@{text")"} (or @{text"proof +(rule"}~\textit{intro-rules}@{text")"} if there are no facts fed into +the proof). *} subsection{*More constructs*} @@ -234,9 +239,9 @@ arguments by contradiction, this example also introduces two new abbreviations: \begin{center} -\begin{tabular}{lcl} -\isakeyword{hence} &=& \isakeyword{then} \isakeyword{have} \\ -\isakeyword{with}~\emph{facts} &=& +\begin{tabular}{l@ {\quad=\quad}l} +\isakeyword{hence} & \isakeyword{then} \isakeyword{have} \\ +\isakeyword{with}~\emph{facts} & \isakeyword{from}~\emph{facts} @{text this} \end{tabular} \end{center} @@ -262,6 +267,11 @@ when showing @{term"A \ B"} we need to show both @{term A} and @{term B}. Each subgoal is proved separately, in \emph{any} order. The individual proofs are separated by \isakeyword{next}. + +Strictly speaking \isakeyword{next} is only required if the subgoals +are proved in different assumption contexts which need to be +separated, which is not the case above. For clarity we +have employed \isakeyword{next} anyway and will continue to do so. \end{description} This is all very well as long as formulae are small. Let us now look at some @@ -315,7 +325,6 @@ \isakeyword{using} \emph{minor-facts}~ \emph{proof} \end{center} -\medskip Sometimes it is necessary to suppress the implicit application of rules in a \isakeyword{proof}. For example \isakeyword{show}~@{prop"A \ B"} would @@ -379,7 +388,7 @@ the elimination involved. Here is a proof of a well known tautology. -Figure out which rule is used where! *} +Which rule is used where? *} lemma assumes ex: "\x. \y. P x y" shows "\y. \x. P x y" proof @@ -470,6 +479,7 @@ @{text blast} to achieve bigger proof steps, there may still be the tendency to use the default introduction and elimination rules to decompose goals and facts. This can lead to very tedious proofs: +\Tweakskip *} (*<*)ML"set quick_and_dirty"(*>*) lemma "\x y. A x y \ B x y \ C x y" @@ -554,10 +564,10 @@ text{* If you want to remember intermediate fact(s) that cannot be named directly, use \isakeyword{note}. For example the result of raw proof block can be named by following it with -\isakeyword{note}~@{text"note some_name = this"}. As a side effect +\isakeyword{note}~@{text"some_name = this"}. As a side effect, @{text this} is set to the list of facts on the right-hand side. You can also say @{text"note some_fact"}, which simply sets @{text this}, -i.e.\ recalls @{text"some_fact"}. *} +i.e.\ recalls @{text"some_fact"}, e.g.\ in a \isakeyword{moreover} sequence. *} subsubsection{*\isakeyword{fixes}*} @@ -587,7 +597,8 @@ by(simp add: comm mono) text{*\noindent The concrete syntax is dropped at the end of the proof and the -theorem becomes @{thm[display,margin=60]comm_mono} *} +theorem becomes @{thm[display,margin=60]comm_mono} +\tweakskip *} subsubsection{*\isakeyword{obtain}*} diff -r e3c444e805c4 -r fb78ee03c391 doc-src/TutorialI/IsarOverview/Isar/document/intro.tex --- a/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex Mon Dec 23 12:01:47 2002 +0100 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex Sun Dec 29 08:56:24 2002 +0100 @@ -1,9 +1,11 @@ \section{Introduction} -Isar is an extension of Isabelle with structured proofs in a stylized -language of mathematics. These proofs are readable for both a human -and a machine. This document is a compact introduction to structured -proofs in Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. We +Isabelle is a generic proof assistant. Isar is an extension of +Isabelle with structured proofs in a stylised language of mathematics. +These proofs are readable for both a human and a machine. +Isabelle/HOL~\cite{LNCS2283} is a specialisation of Isabelle with +higher-order logic (HOL). This paper is a compact introduction to +structured proofs in Isar/HOL, an extension of Isabelle/HOL. We intentionally do not present the full language but concentrate on the essentials. Neither do we give a formal semantics of Isar. Instead we introduce Isar by example. We believe that the language ``speaks for @@ -26,7 +28,7 @@ tactics. A radically different approach was taken by the Mizar -system~\cite{Rudnicki92} where proofs are written in a stylized language akin +system~\cite{Rudnicki92} where proofs are written in a stylised language akin to that used in ordinary mathematics texts. The most important argument in favour of a mathematics-like proof language is communication: as soon as not just the theorem but also the proof becomes an object of interest, it should @@ -94,13 +96,16 @@ \subsection{Bits of Isabelle} -In order to make this paper self-contained we recall some basic -notions and notation from Isabelle~\cite{LNCS2283}. Isabelle's -meta-logic offers an implication $\Longrightarrow$ and a universal quantifier $\bigwedge$ -for expressing inference rules and generality. Iterated implications -$A_1 \Longrightarrow \dots A_n \Longrightarrow A$ may be abbreviated to $[\![ A_1; \dots; A_n -]\!] \Longrightarrow A$. Applying a theorem $A \Longrightarrow B$ (named \isa{T}) to a theorem -$A$ (named \isa{U}) is written \isa{T[OF U]} and yields theorem $B$. +We recall some basic notions and notation from Isabelle. For more +details and for instructions how to run examples see +elsewhere~\cite{LNCS2283}. + +Isabelle's meta-logic comes with a type of \emph{propositions} with +implication $\Longrightarrow$ and a universal quantifier $\bigwedge$ for expressing +inference rules and generality. Iterated implications $A_1 \Longrightarrow \dots +A_n \Longrightarrow A$ may be abbreviated to $[\![ A_1; \dots; A_n ]\!] \Longrightarrow A$. +Applying a theorem $A \Longrightarrow B$ (named \isa{T}) to a theorem $A$ (named +\isa{U}) is written \isa{T[OF U]} and yields theorem $B$. Isabelle terms are simply typed. Function types are written $\tau_1 \Rightarrow \tau_2$. @@ -112,7 +117,12 @@ of its free variables. Isabelle/HOL offers all the usual logical symbols like $\longrightarrow$, $\land$, -$\forall$ etc. Proof methods include \isa{rule} (which performs a backwards +$\forall$ etc. HOL formulae are propositions, e.g.\ $\forall$ can appear below +$\Longrightarrow$, but not the other way around. Beware that $\longrightarrow$ binds more +tightly than $\Longrightarrow$: in $\forall x. P \longrightarrow Q$ the $\forall x$ covers $P \longrightarrow Q$, whereas +in $\forall x. P \Longrightarrow Q$ it covers only $P$. + +Proof methods include \isa{rule} (which performs a backwards step with a given rule, unifying the conclusion of the rule with the current subgoal and replacing the subgoal by the premises of the rule), \isa{simp} (for simplification) and \isa{blast} (for predicate @@ -146,5 +156,5 @@ %Do not be mislead by the simplicity of the formulae being proved, %especially in the beginning. Isar has been used very successfully in -%large applications, for example the formalization of Java, in +%large applications, for example the formalisation of Java, in %particular the verification of the bytecode verifier~\cite{KleinN-TCS}. diff -r e3c444e805c4 -r fb78ee03c391 doc-src/TutorialI/IsarOverview/Isar/document/root.tex --- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Mon Dec 23 12:01:47 2002 +0100 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Sun Dec 29 08:56:24 2002 +0100 @@ -13,7 +13,8 @@ \begin{document} -\title{A Compact Introduction to Structured Proofs in Isar/HOL} +\title{%A Compact Introduction to +Structured Proofs in Isar/HOL} \author{Tobias Nipkow} \institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\ {\small\url{http://www.in.tum.de/~nipkow/}}} @@ -35,7 +36,12 @@ \input{Induction.tex} \Tweakskip -\Tweakskip +\small +\paragraph{Acknowledgement} +I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin, +Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer, +Markus Wenzel and Freek Wiedijk commented on and improved this paper. + \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing \bibliography{root}