diff -r 70a5d5fc081a -r 3323ecc0b97c doc-src/TutorialI/IsarOverview/Isar/Logic.thy --- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Tue Jul 09 11:55:46 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Tue Jul 09 13:41:38 2002 +0200 @@ -1,6 +1,6 @@ (*<*)theory Logic = Main:(*>*) text{* We begin by looking at a simplified grammar for Isar proofs -where paranthesis are used for grouping and $^?$ indicates an optional item: +where parentheses are used for grouping and $^?$ indicates an optional item: \begin{center} \begin{tabular}{lrl} \emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$ @@ -8,13 +8,12 @@ \isakeyword{qed} \\ &$\mid$& \isakeyword{by} \emph{method}\\[1ex] \emph{statement} &::= & \isakeyword{fix} \emph{variables} \\ - &$\mid$& \isakeyword{assume} \emph{proposition} - (\isakeyword{and} \emph{proposition})*\\ - &$\mid$& (\isakeyword{from} \emph{label}$^*$ $\mid$ - \isakeyword{then})$^?$ + &$\mid$& \isakeyword{assume} \emph{propositions} \\ + &$\mid$& (\isakeyword{from} \emph{facts})$^?$ (\isakeyword{show} $\mid$ \isakeyword{have}) - \emph{string} \emph{proof} \\[1ex] -\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} + \emph{propositions} \emph{proof} \\[1ex] +\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex] +\emph{fact} &::=& \emph{label} \end{tabular} \end{center} @@ -32,6 +31,16 @@ \end{center} It proves \emph{the-assm}~@{text"\"}~\emph{the-concl}. Text starting with ``--'' is a comment. + +Note that propositions in \isakeyword{assume} may but need not be +separated by \isakeyword{and} whose purpose is to structure the +assumptions into possibly named blocks, for example +\begin{center} +\isakeyword{assume} @{text"A:"} $A_1$ $A_2$ \isakeyword{and} @{text"B:"} $A_3$ +\isakeyword{and} $A_4$ +\end{center} +Here label @{text A} refers to the list of propositions $A_1$ $A_2$ and +label @{text B} to $A_3$. *} section{*Logic*} @@ -67,7 +76,7 @@ qed text{* Trivial proofs, in particular those by assumption, should be trivial -to perform. Method ``.'' does just that (and a bit more --- see later). Thus +to perform. Proof ``.'' does just that (and a bit more). Thus naming of assumptions is often superfluous: *} lemma "A \ A" proof @@ -88,7 +97,7 @@ Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} can be abbreviated to ``..'' -if \emph{name} is one of the predefined introduction rules: +if \emph{name} refers to one of the predefined introduction rules: *} lemma "A \ A \ A" @@ -118,7 +127,7 @@ qed text{*\noindent Note that the term @{text"?thesis"} always stands for the ``current goal'', i.e.\ the enclosing \isakeyword{show} (or -\isakeyword{have}). +\isakeyword{have}) statement. This is too much proof text. Elimination rules should be selected automatically based on their major premise, the formula or rather connective @@ -161,9 +170,14 @@ qed qed -text{*\noindent -A final simplification: \isakeyword{from}~@{text this} can be -abbreviated to \isakeyword{thus}. +text{*\noindent Because of the frequency of \isakeyword{from}~@{text +this} Isar provides two abbreviations: +\begin{center} +\begin{tabular}{rcl} +\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: *} @@ -175,7 +189,7 @@ from b a show "B \ A" .. qed text{*\noindent -It is worth examining this text in detail because it exhibits a number of new features. +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 @@ -187,7 +201,8 @@ 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$, \isakeyword{show} +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, @@ -203,7 +218,7 @@ with \isakeyword{by}@{text"(rule conjI)"}. Note that Isar's predefined introduction and elimination rules include all the -usual natural deduction rules for propositional logic. We conclude this +usual natural deduction rules. We conclude this section with an extended example --- which rules are used implicitly where? Rule @{thm[source]ccontr} is @{thm ccontr[no_vars]}. *} @@ -247,27 +262,27 @@ text{* So far our examples have been a bit unnatural: normally we want to prove rules expressed with @{text"\"}, not @{text"\"}. Here is an example: *} -lemma "(A \ False) \ \ A" +lemma "A \ B \ B \ A" proof - assume "A \ False" "A" - thus False . + assume "A \ B" thus "B" .. +next + assume "A \ B" thus "A" .. qed text{*\noindent The \isakeyword{proof} always works on the conclusion, -@{prop"\A"} in our case, thus selecting $\neg$-introduction. Hence we can -additionally assume @{prop"A"}. Why does ``.'' prove @{prop False}? Because -``.'' tries any of the assumptions, including proper rules (here: @{prop"A \ -False"}), such that all of its premises can be solved directly by some other -assumption (here: @{prop A}). +@{prop"B \ A"} in our case, thus selecting $\land$-introduction. Hence +we must show @{prop B} and @{prop A}; both are proved by +$\land$-elimination. This is all very well as long as formulae are small. Let us now look at some devices to avoid repeating (possibly large) formulae. A very general method is pattern matching: *} -lemma "(large_formula \ False) \ \ large_formula" - (is "(?P \ _) \ _") +lemma "large_A \ large_B \ large_B \ large_A" + (is "?AB \ ?B \ ?A") proof - assume "?P \ False" ?P - thus False . + assume ?AB thus ?B .. +next + assume ?AB thus ?A .. qed text{*\noindent Any formula may be followed by @{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern @@ -276,20 +291,39 @@ them to be replaced by the terms they stand for. We can simplify things even more by stating the theorem by means of the -\isakeyword{assumes} and \isakeyword{shows} primitives which allow direct +\isakeyword{assumes} and \isakeyword{shows} elements which allow direct naming of assumptions: *} -lemma assumes A: "large_formula \ False" - shows "\ large_formula" (is "\ ?P") +lemma assumes AB: "large_A \ large_B" + shows "large_B \ large_A" (is "?B \ ?A") proof - assume ?P - with A show False . + from AB show ?B .. +next + from AB show ?A .. qed -text{*\noindent Here we have used the abbreviation +text{*\noindent Note the difference between @{text ?AB}, a term, and +@{text AB}, a fact. + +Finally we want to start the proof with $\land$-elimination so we +don't have to perform it twice, as above. Here is a slick way to +achieve this: *} + +lemma assumes AB: "large_A \ large_B" + shows "large_B \ large_A" (is "?B \ ?A") +using AB +proof + assume ?A and ?B show ?thesis .. +qed +text{*\noindent Command \isakeyword{using} can appear before a proof +and adds further facts to those piped into the proof. Here @{text AB} +is the only such fact and it triggers $\land$-elimination. Another +frequent usage is as follows: \begin{center} -\isakeyword{with}~\emph{facts} \quad = \quad -\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this} +\isakeyword{from} \emph{important facts} +\isakeyword{show} \emph{something} +\isakeyword{using} \emph{minor facts} \end{center} +\medskip Sometimes it is necessary to supress the implicit application of rules in a \isakeyword{proof}. For example \isakeyword{show}~@{prop"A \ B"} would @@ -305,12 +339,13 @@ assume B show ?thesis .. qed qed - +text{*\noindent Could \isakeyword{using} help to eliminate this ``@{text"-"}''? *} subsection{*Predicate calculus*} text{* Command \isakeyword{fix} introduces new local variables into a -proof. It corresponds to @{text"\"} (the universal quantifier at the +proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to @{text"\"} +(the universal quantifier at the meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to @{text"\"}. Here is a sample proof, annotated with the rules that are applied implictly: *} @@ -321,7 +356,7 @@ qed text{*\noindent Note that in the proof we have chosen to call the bound variable @{term a} instead of @{term x} merely to show that the choice of -names is irrelevant. +local names is irrelevant. Next we look at @{text"\"} which is a bit more tricky. *} @@ -337,20 +372,19 @@ qed text{*\noindent Explicit $\exists$-elimination as seen above can become cumbersome in practice. The derived Isar language element -\isakeyword{obtain} provides a more handsome way to perform generalized +\isakeyword{obtain} provides a more appealing form of generalized existence reasoning: *} lemma assumes Pf: "\x. P(f x)" shows "\y. P y" proof - - from Pf obtain a where "P(f a)" .. + from Pf obtain x where "P(f x)" .. thus "\y. P y" .. qed text{*\noindent Note how the proof text follows the usual mathematical style of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$ as a new local variable. Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and \isakeyword{assume} together with a soundness proof of -the elimination involved. Thus it behaves similar to any other forward proof -element. +the elimination involved. Here is a proof of a well known tautology which employs another useful abbreviation: \isakeyword{hence} abbreviates \isakeyword{from}~@{text @@ -386,7 +420,7 @@ qed qed text{*\noindent -For a start, the example demonstrates two new language elements: +For a start, the example demonstrates three new language elements: \begin{itemize} \item \isakeyword{let} introduces an abbreviation for a term, in our case the witness for the claim, because the term occurs multiple times in the proof. @@ -394,6 +428,11 @@ implicit what the two cases are: it is merely expected that the two subproofs prove @{prop"P \ Q"} and @{prop"\P \ Q"} for suitable @{term P} and @{term Q}. +\item \isakeyword{with} is an abbreviation: +\begin{center} +\isakeyword{with}~\emph{facts} \quad = \quad +\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this} +\end{center} \end{itemize} If you wonder how to \isakeyword{obtain} @{term y}: via the predefined elimination rule @{thm rangeE[no_vars]}. @@ -425,7 +464,7 @@ qed qed text{*\noindent Method @{text contradiction} succeeds if both $P$ and -$\neg P$ are among the assumptions and the facts fed into that step. +$\neg P$ are among the assumptions and the facts fed into that step, in any order. As it happens, Cantor's theorem can be proved automatically by best-first search. Depth-first search would diverge, but best-first search successfully @@ -440,7 +479,7 @@ Finally, whole scripts may appear in the leaves of the proof tree, although this is best avoided. Here is a contrived example: *} -lemma "A \ (A \B) \ B" +lemma "A \ (A \ B) \ B" proof assume a: A show "(A \B) \ B" @@ -466,7 +505,7 @@ next assume "\ P" thus ?thesis .. qed -text{*\noindent As always, the cases can be tackled in any order. +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 don't want to repeat it. This can be avoided by @@ -481,13 +520,12 @@ text{*\noindent which is simply a shorthand for the previous proof. More precisely, the phrases \isakeyword{case}~@{prop True}/@{prop False} abbreviate the corresponding assumptions @{prop P} -and @{prop"\P"}. +and @{prop"\P"}. In contrast to the previous proof we can prove the cases +in arbitrary order. The same game can be played with other datatypes, for example lists: *} - (*<*)declare length_tl[simp del](*>*) - lemma "length(tl xs) = length xs - 1" proof (cases xs) case Nil thus ?thesis by simp @@ -498,10 +536,10 @@ \isakeyword{assume}~@{prop"x = []"} and \isakeyword{case}~@{text Cons} abbreviates \isakeyword{assume}~@{text"xs = _ # _"}. The names of the head and tail of @{text xs} have been chosen by the system. Therefore we cannot -refer to them (this would lead to brittle proofs) and have not even shown -them. Luckily, the proof is simple enough we do not need to refer to them. +refer to them (this would lead to obscure proofs) and have not even shown +them. Luckily, this proof is simple enough we do not need to refer to them. However, in general one may have to. Hence Isar offers a simple scheme for -naming those variables: Replace the anonymous @{text Cons} by, for example, +naming those variables: replace the anonymous @{text Cons} by, for example, @{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"} \isakeyword{assume}~@{text"xs = Cons y ys"}, i.e.\ @{prop"xs = y # ys"}. Here is a (somewhat contrived) example: *} @@ -515,8 +553,7 @@ by simp thus ?thesis by simp qed -text{* New case distincion rules can be declared any time, even with -named cases. *} + subsection{*Induction*} @@ -552,7 +589,7 @@ corresponding case to be proved, i.e.\ @{text"?P 0"} in the first case and @{text"?P(Suc n)"} in the second case. Context \isakeyword{case}~@{text 0} is empty whereas \isakeyword{case}~@{text Suc} assumes @{text"?P n"}. Again we -have the same problem as with case distinctions: we cannot refer to @{term n} +have the same problem as with case distinctions: we cannot refer to an anonymous @{term n} in the induction step because it has not been introduced via \isakeyword{fix} (in contrast to the previous proof). The solution is the same as above: replace @{term Suc} by @{text"(Suc i)"}: *} @@ -609,7 +646,7 @@ name (here: @{term Suc}) are the names of the parameters of that subgoal. So far the only parameters where the arguments to the constructor, but now we have an additonal parameter coming from the @{text"\m"} in the main -\isakeyword{shows} clause. Thus Thus @{text"(Suc n m)"} does not mean that +\isakeyword{shows} clause. Thus @{text"(Suc n m)"} does not mean that constructor @{term Suc} is applied to two arguments but that the two parameters in the @{term Suc} case are to be named @{text n} and @{text m}. *} @@ -625,39 +662,20 @@ step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" text{* \noindent and prove that @{term"r*"} is indeed transitive: *} -lemma assumes A: "(x,y) \ r*" - shows "(y,z) \ r* \ (x,z) \ r*" (is "PROP ?P x y") +lemma assumes A: "(x,y) \ r*" shows "(y,z) \ r* \ (x,z) \ r*" using A proof induct case refl thus ?case . next case step thus ?case by(blast intro: rtc.step) qed -(* -lemma assumes A: "(x,y) \ r*" - shows "(y,z) \ r* \ (x,z) \ r*" (is "PROP ?P x y") -proof - - from A show "PROP ?P x y" - proof induct - fix x show "PROP ?P x x" . - next - fix x' x y - assume "(x',x) \ r" - "PROP ?P x y" -- "induction hypothesis" - thus "PROP ?P x' y" by(blast intro: rtc.step) - qed -qed -*) -text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) \in R$ -piped into the proof, here \isakeyword{from}~@{text A}. The proof itself -follows the two rules of the inductive definition very closely. The only -surprising thing should be the keyword @{text PROP}: because of certain -syntactic subleties it is required in front of terms of type @{typ prop} (the -type of meta-level propositions) which are not obviously of type @{typ prop} -(e.g.\ @{text"?P x y"}) because they do not contain a tell-tale constant such -as @{text"\"} or @{text"\"}. +text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) +\in R$ piped into the proof, here \isakeyword{using}~@{text A}. The +proof itself follows the inductive definition very +closely: there is one case for each rule, and it has the same name as +the rule, analogous to structural induction. -However, the proof is rather terse. Here is a more readable version: +However, this proof is rather terse. Here is a more readable version: *} lemma assumes A: "(x,y) \ r*" and B: "(y,z) \ r*" @@ -675,14 +693,12 @@ from 1 IH[OF B] show "(x',z) \ r*" by(rule rtc.step) qed qed - text{*\noindent We start the proof with \isakeyword{from}~@{text"A -B"}. Only @{text A} is ``consumed'' by the first proof step, here -induction. Since @{text B} is left over we don't just prove @{text -?thesis} but @{text"B \ ?thesis"}, just as in the previous -proof, only more elegantly. The base case is trivial. In the -assumptions for the induction step we can see very clearly how things -fit together and permit ourselves the obvious forward step -@{text"IH[OF B]"}. *} +B"}. Only @{text A} is ``consumed'' by the induction step. +Since @{text B} is left over we don't just prove @{text +?thesis} but @{text"B \ ?thesis"}, just as in the previous proof. The +base case is trivial. In the assumptions for the induction step we can +see very clearly how things fit together and permit ourselves the +obvious forward step @{text"IH[OF B]"}. *} (*<*)end(*>*)