summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 04 Jul 2002 11:13:56 +0200 | |

changeset 13294 | 5e2016d151bd |

parent 13293 | 09276ee04361 |

child 13295 | ca2e9b273472 |

*** empty log message ***

--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Thu Jul 04 10:54:04 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Thu Jul 04 11:13:56 2002 +0200 @@ -10,8 +10,9 @@ &$\mid$& \isacommand{by} \emph{method}\\[1ex] \emph{statement} &::= & \isacommand{fix} \emph{variables} \\ &$\mid$& \isacommand{assume} proposition* \\ - &$\mid$& \isacommand{then}$^?$ - (\isacommand{show} | \isacommand{have}) + &$\mid$& (\isacommand{from} \emph{label}$^*$ $\mid$ + \isacommand{then})$^?$ \\ + && (\isacommand{show} $\mid$ \isacommand{have}) \emph{proposition} \emph{proof} \\[1ex] \emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \end{tabular} @@ -23,20 +24,23 @@ \begin{center} \begin{tabular}{@ {}ll} \isacommand{proof}\\ -\hspace*{3ex}\isacommand{assume} "\dots"\\ +\hspace*{3ex}\isacommand{assume} "\emph{the-assm}"\\ \hspace*{3ex}\isacommand{have} "\dots" & -- "intermediate result"\\ \hspace*{3ex}\vdots\\ \hspace*{3ex}\isacommand{have} "\dots" & -- "intermediate result"\\ -\hspace*{3ex}\isacommand{show} "\dots" & --"the conclusion"\\ +\hspace*{3ex}\isacommand{show} "\emph{the-concl}"\\ \isacommand{qed} \end{tabular} \end{center} +It proves \emph{the-assm}~@{text"\<Longrightarrow>"}~\emph{the-concl}. *} section{*Logic*} subsection{*Propositional logic*} +subsubsection{*Introduction rules*} + lemma "A \<longrightarrow> A" proof (rule impI) assume A: "A" @@ -49,8 +53,8 @@ However, this text is much too detailled for comfort. Therefore Isar implements the following principle: \begin{quote}\em -Command \isacommand{proof} can automatically select an introduction rule based -on the goal and a predefined list of rules. +Command \isacommand{proof} automatically tries select an introduction rule +based on the goal and a predefined list of rules. \end{quote} Here @{thm[source]impI} is applied automatically: *} @@ -61,8 +65,9 @@ show "A" by(rule A) qed -(* Proof by assumption should be trivial. Method "." does just that (and a -bit more - see later). Thus naming of assumptions is often superfluous. *) +text{* Trivial proofs, in particular those by assumption, should be trivial +to perform. Method "." does just that (and a bit more --- see later). Thus +naming of assumptions is often superfluous: *} lemma "A \<longrightarrow> A" proof @@ -70,8 +75,9 @@ have "A" . qed -(* To hide proofs by assumption, by(method) first applies method and then -tries to solve all remaining subgoals by assumption. *) +text{* To hide proofs by assumption further, \isacommand{by}@{text"(method)"} +first applies @{text method} and then tries to solve all remaining subgoals +by assumption: *} lemma "A \<longrightarrow> A & A" proof @@ -79,103 +85,155 @@ show "A & A" by(rule conjI) qed -(* Proofs of the form by(rule <rule>) can be abbreviated to ".." if <rule> is -one of the predefined introduction rules (for user supplied rules see below). -Thus -*) +text{*\noindent A drawback of these implicit proofs by assumption is that it +is no longer obvious where an assumption is used. -lemma "A \<longrightarrow> A & A" +Proofs of the form \isacommand{by}@{text"(rule <name>)"} can be abbreviated +to ".." if @{text"<name>"} is one of the predefined introduction rules. Thus +*} + +lemma "A \<longrightarrow> A \<and> A" proof assume A - show "A & A" .. + show "A \<and> A" .. qed -(* What happens: applies "conj" (first "."), then solves the two subgoals by -assumptions (second ".") *) +text{*\noindent +What happens: first the matching introduction rule @{thm[source]conjI} +is applied (first "."), then the two subgoals are solved by assumption +(second "."). *} -(* Now: elimination *) +subsubsection{*Elimination rules*} -lemma "A & B \<longrightarrow> B & A" +text{*A typical elimination rule is @{thm[source]conjE}, $\land$-elimination: +@{thm[display,indent=5]conjE[no_vars]} In the following proof it is applied +by hand, after its first (``\emph{major}'') premise has been eliminated via +@{text"[OF AB]"}: *} + +lemma "A \<and> B \<longrightarrow> B \<and> A" proof - assume AB: "A & B" - show "B & A" + assume AB: "A \<and> B" + show "B \<and> A" proof (rule conjE[OF AB]) assume A and B - show ?thesis .. --"thesis = statement in previous show" + show ?thesis .. qed qed -(* Again: too much text. +text{*\noindent Note that the term @{text"?thesis"} always stands for the +``current goal'', i.e.\ the enclosing \isacommand{show} (or +\isacommand{have}). -Elimination rules are used to conclude new stuff from old. In Isar they are -triggered by propositions being fed INTO a proof block. Syntax: -from <previously proved propositions> show \<dots> -applies an elimination rule whose first premise matches one of the <previously proved propositions>. Thus: -*) +This is too much proof text. Elimination rules should be selected +automatically based on their major premise, the formula or rather connective +to be eliminated. In Isar they are triggered by propositions being fed +\emph{into} a proof block. Syntax: +\begin{center} +\isacommand{from} \emph{fact} \isacommand{show} \emph{proposition} +\end{center} +where \emph{fact} stands for the name of a previously proved proved +proposition, e.g.\ an assumption, an intermediate result or some global +theorem. The fact may also be modified with @{text of}, @{text OF} etc. +This command applies a elimination rule (from a predefined list) +whose first premise is solved by the fact. Thus: *} -lemma "A & B \<longrightarrow> B & A" +lemma "A \<and> B \<longrightarrow> B \<and> A" proof - assume AB: "A & B" - from AB show "B & A" + assume AB: "A \<and> B" + from AB show "B \<and> A" proof assume A and B show ?thesis .. qed qed -(* -2nd principle: try to arrange sequence of propositions in a UNIX like -pipe, such that the proof of the next proposition uses the previous -one. The previous proposition can be referred to via "this". -This greatly reduces the need for explicit naming of propositions. -*) -lemma "A & B \<longrightarrow> B & A" +text{* Now we come a second important principle: +\begin{quote}\em +Try to arrange the sequence of propositions in a UNIX-like pipe, +such that the proof of each proposition builds on the previous proposition. +\end{quote} +The previous proposition can be referred to via the fact @{text this}. +This greatly reduces the need for explicit naming of propositions: +*} + +lemma "A \<and> B \<longrightarrow> B \<and> A" proof - assume "A & B" - from this show "B & A" + assume "A \<and> B" + from this show "B \<and> A" proof assume A and B show ?thesis .. qed qed -(* Final simplification: "from this" = "thus". - -Alternative: pure forward reasoning: *) +text{*\noindent +A final simplification: \isacommand{from}~@{text this} can be +abbreviated to \isacommand{thus}. +\bigskip -lemma "A & B --> B & A" +Here is an alternative proof that operates purely by forward reasoning: *} + +lemma "A \<and> B \<longrightarrow> B \<and> A" proof - assume ab: "A & B" + assume ab: "A \<and> B" from ab have a: A .. from ab have b: B .. - from b a show "B & A" .. + from b a show "B \<and> A" .. qed -(* New: itermediate haves *) +text{*\noindent +It is worth examining this text in detail because it exhibits a number of new features. -(* The predefined introduction and elimination rules include all the usual -natural deduction rules for propositional logic. Here is a longer example: *) +For a start, this is the first time we have proved intermediate propositions +(\isacommand{have}) on the way to the final \isacommand{show}. This is the +norm in any nontrival proof where one cannot bridge the gap between the +assumptions and the conclusion in one step. Both \isacommand{have}s above are +proved automatically via @{thm[source]conjE} triggered by +\isacommand{from}~@{text ab}. -lemma "~(A & B) \<longrightarrow> ~A | ~B" +The \isacommand{show} command illustrates two things: +\begin{itemize} +\item \isacommand{from} can be followed by any number of facts. +Given \isacommand{from}~@{text f}$_1$~\dots~@{text f}$_n$, \isacommand{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 if we had written \isacommand{from}~@{text"a b"} +instead of \isacommand{from}~@{text"b a"}. + +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 \isacommand{by}@{text"(rule conjI)"}. + +Note Isar's predefined introduction and elimination rules include all the +usual natural deduction rules for propositional logic. We conclude this +section with an extended example --- which rules are used implicitly where? +Rule @{thm[source]ccontr} is @{thm ccontr[no_vars]}. +*} + +lemma "\<not>(A \<and> B) \<longrightarrow> \<not>A \<or> \<not>B" proof - assume n: "~(A & B)" - show "~A | ~B" + assume n: "\<not>(A \<and> B)" + show "\<not>A \<or> \<not>B" proof (rule ccontr) - assume nn: "~(~ A | ~B)" + assume nn: "\<not>(\<not> A \<or> \<not>B)" from n show False proof - show "A & B" + show "A \<and> B" proof show A proof (rule ccontr) - assume "~A" + assume "\<not>A" have "\<not> A \<or> \<not> B" .. from nn this show False .. qed next show B proof (rule ccontr) - assume "~B" + assume "\<not>B" have "\<not> A \<or> \<not> B" .. from nn this show False .. qed @@ -184,166 +242,233 @@ qed qed; -(* New: - -1. Multiple subgoals. When showing "A & B" we need to show both A and B. -Each subgoal is proved separately, in ANY order. The individual proofs are -separated by "next". - -2. "have" for proving an intermediate fact -*) +text{*\noindent Apart from demonstrating the strangeness of classical +arguments by contradiction, this example also introduces a new language +feature to deal with multiple subgoals: \isacommand{next}. When showing +@{term"A \<and> 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 \isacommand{next}. *} subsection{*Becoming more concise*} -(* Normally want to prove rules expressed with \<Longrightarrow>, not \<longrightarrow> *) +text{* So far our examples have been a bit unnatural: normally we want to +prove rules expressed with @{text"\<Longrightarrow>"}, not @{text"\<longrightarrow>"}. Here is an example: +*} lemma "\<lbrakk> A \<Longrightarrow> False \<rbrakk> \<Longrightarrow> \<not> A" proof - assume "A \<Longrightarrow> False" A + assume "A \<Longrightarrow> False" "A" thus False . qed -(* In this case the "proof" works on the "~A", thus selecting notI +text{*\noindent The \isacommand{proof} always works on the conclusion, +@{prop"\<not>A"} in our case, thus selecting $\neg$-introduction. Hence we can +additionally assume @{prop"A"}. -Now: avoid repeating formulae (which may be large). *) +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 \<Longrightarrow> False) \<Longrightarrow> ~ large_formula" +lemma "(large_formula \<Longrightarrow> False) \<Longrightarrow> \<not> large_formula" (is "(?P \<Longrightarrow> _) \<Longrightarrow> _") proof assume "?P \<Longrightarrow> False" ?P thus False . qed -(* Even better: can state assumptions directly *) +text{*\noindent Any formula may be followed by +@{text"("}\isacommand{is}~\emph{pattern}@{text")"} which causes the pattern +to be matched against the formula, instantiating the ?-variables in the +pattern. Subsequent uses of these variables in other terms simply causes them +to be replaced by the terms they stand for. + +We can simplify things even more by stating the theorem by means of the +\isacommand{assumes} and \isacommand{shows} primitives which allow direct +naming of assumptions: *} lemma assumes A: "large_formula \<Longrightarrow> False" - shows "~ large_formula" (is "~ ?P") + shows "\<not> large_formula" (is "\<not> ?P") proof assume ?P - from A show False . -qed; - - -(* Predicate calculus. Keyword fix introduces new local variables into a -proof. Corresponds to !! just like assume-show corresponds to \<Longrightarrow> *) - -lemma assumes P: "!x. P x" shows "!x. P(f x)" -proof --"allI" - fix x - from P show "P(f x)" .. --"allE" + with A show False . qed -lemma assumes Pf: "EX x. P (f x)" shows "EX y. P y" +text{*\noindent Here we have used the abbreviation +\begin{center} +\isacommand{with}~\emph{facts} \quad = \quad +\isacommand{from}~\emph{facts} \isacommand{and} @{text this} +\end{center} + +Sometimes it is necessary to supress the implicit application of rules in a +\isacommand{proof}. For example \isacommand{show}~@{prop"A \<or> B"} would +trigger $\lor$-introduction, requiring us to prove @{prop A}. A simple +``@{text"-"}'' prevents this \emph{faut pas}: *} + +lemma assumes AB: "A \<or> B" shows "B \<or> A" proof - - from Pf show ?thesis - proof --"exE" - fix a - assume "P(f a)" - show ?thesis .. --"exI" + from AB show ?thesis + proof + assume A show ?thesis .. + next + assume B show ?thesis .. qed qed -text {* - Explicit $\exists$-elimination as seen above can become quite - cumbersome in practice. The derived Isar language element - ``\isakeyword{obtain}'' provides a more handsome way to do - generalized existence reasoning. +subsection{*Predicate calculus*} + +text{* Command \isacommand{fix} introduces new local variables into a +proof. It corresponds to @{text"\<And>"} (the universal quantifier at the +meta-level) just like \isacommand{assume}-\isacommand{show} corresponds to +@{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are +applied implictly: *} + +lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P(f x)" +proof -- "@{thm[source]allI}: @{thm allI[no_vars]}" + fix a + from P show "P(f a)" .. --"@{thm[source]allE}: @{thm allE[no_vars]}" +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. + +Next we look at @{text"\<exists>"} which is a bit more tricky. *} -lemma assumes Pf: "EX x. P (f x)" shows "EX y. P y" +lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y" proof - - from Pf obtain a where "P (f a)" .. --"exE" - thus "EX y. P y" .. --"exI" + from Pf show ?thesis + proof -- "@{thm[source]exE}: @{thm exE[no_vars]}" + fix a + assume "P(f a)" + show ?thesis .. --"@{thm[source]exI}: @{thm exI[no_vars]}" + qed qed -text {* - 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. Also note that due to the nature of general existence - reasoning involved here, any result exported from the context of an - \isakeyword{obtain} statement may \emph{not} refer to the parameters - introduced there. +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 existence reasoning: *} -lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y" -proof --"allI" - fix y - from ex obtain x where "ALL y. P x y" .. --"exE" - from this have "P x y" .. --"allE" - thus "EX x. P x y" .. --"exI" +lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y" +proof - + from Pf obtain x where "P(f x)" .. + thus "\<exists>y. P y" .. qed -(* some example with blast, if . and .. fail *) +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. -theorem "EX S. S ~: range (f :: 'a => 'a set)" +Here is a proof of a well known tautology which employs another useful +abbreviation: \isakeyword{hence} abbreviates \isakeyword{from}~@{text +this}~\isakeyword{have}. Figure out which rule is used where! *} + +lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y" proof - let ?S = "{x. x ~: f x}" - show "?S ~: range f" + fix y + from ex obtain x where "\<forall>y. P x y" .. + hence "P x y" .. + thus "\<exists>x. P x y" .. +qed + +text{* So far we have confined ourselves to single step proofs. Of course +powerful automatic methods can be used just as well. Here is an example, +Cantor's theorem that there is no surjective function from a set to its +powerset: *} + +theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" +proof + let ?S = "{x. x \<notin> f x}" + show "?S \<notin> range f" proof - assume "?S : range f" + assume "?S \<in> range f" then obtain y where fy: "?S = f y" .. show False proof (cases) - assume "y : ?S" + assume "y \<in> ?S" with fy show False by blast next - assume "y ~: ?S" + assume "y \<notin> ?S" with fy show False by blast qed qed qed -theorem "EX S. S ~: range (f :: 'a => 'a set)" +text{*\noindent +For a start, the example demonstrates two 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. +\item Proof by @{text"(cases)"} starts a proof by cases. Note that it remains +implicit what the two cases are: it is merely expected that the two subproofs +prove @{prop"P \<Longrightarrow> Q"} and @{prop"\<not>P \<Longrightarrow> Q"} for suitable @{term P} and +@{term Q}. +\end{itemize} +If you wonder how to \isakeyword{obtain} @{term y}: +via the predefined elimination rule @{thm rangeE[no_vars]}. + +Method @{text blast} is used because the contradiction does not follow easily +by just a single rule. If you find the proof too cryptic for human +consumption, here is a more detailed version; the beginning up to +\isakeyword{obtain} stays unchanged. *} + +theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" proof - let ?S = "{x. x ~: f x}" - show "?S ~: range f" + let ?S = "{x. x \<notin> f x}" + show "?S \<notin> range f" proof - assume "?S : range f" - then obtain y where eq: "?S = f y" .. + assume "?S \<in> range f" + then obtain y where fy: "?S = f y" .. show False proof (cases) - assume A: "y : ?S" - hence isin: "y : f y" by(simp add:eq) - from A have "y ~: f y" by simp + assume A: "y \<in> ?S" + hence isin: "y \<in> f y" by(simp add:fy) + from A have "y \<notin> f y" by simp with isin show False by contradiction next - assume A: "y ~: ?S" - hence notin: "y ~: f y" by(simp add:eq) - from A have "y : f y" by simp + assume A: "y \<notin> ?S" + hence notin: "y \<notin> f y" by(simp add:fy) + from A have "y \<in> f y" by simp with notin show False by contradiction qed qed qed -text {* - How much creativity is required? As it happens, Isabelle can prove - this theorem automatically using best-first search. Depth-first - search would diverge, but best-first search successfully navigates - through the large search space. The context of Isabelle's classical - prover contains rules for the relevant constructs of HOL's set - theory. +text {*\noindent Method @{text contradiction} succeeds if both $P$ and +$\neg P$ are among the assumptions and the facts fed into that step. + +As it happens, Cantor's theorem can be proved automatically by best-first +search. Depth-first search would diverge, but best-first search successfully +navigates through the large search space: *} -theorem "EX S. S ~: range (f :: 'a => 'a set)" - by best +theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" +by best -(* Finally, whole scripts may appear in the leaves of the proof tree, -although this is best avoided. Here is a contrived example. *) +text{*\noindent Of course this only works in the context of HOL's carefully +constructed introduction and elimination rules for set theory. + +Finally, whole scripts may appear in the leaves of the proof tree, although +this is best avoided. Here is a contrived example: *} lemma "A \<longrightarrow> (A \<longrightarrow>B) \<longrightarrow> B" proof - assume A: A + assume a: A show "(A \<longrightarrow>B) \<longrightarrow> B" apply(rule impI) apply(erule impE) - apply(rule A) + apply(rule a) apply assumption done qed - -(* You may need to resort to this technique if an automatic step fails to -prove the desired proposition. *) - -end +text{*\noindent You may need to resort to this technique if an automatic step +fails to prove the desired proposition. *} +(*<*)end(*>*)

--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.bib Thu Jul 04 10:54:04 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.bib Thu Jul 04 11:13:56 2002 +0200 @@ -1,3 +1,10 @@ +@string{LNCS="Lect.\ Notes in Comp.\ Sci."} +@string{Springer="Springer-Verlag"} + +@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel}, +title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic", +publisher=Springer,series=LNCS,volume=2283,year=2002} + @phdthesis{Wenzel-PhD,author={Markus Wenzel},title={Isabelle/Isar --- A Versatile Environment for Human-Readable Formal Proof Documents}, school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},

--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Thu Jul 04 10:54:04 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Thu Jul 04 11:13:56 2002 +0200 @@ -17,8 +17,9 @@ \noindent This document is a very compact introduction to structured proofs in -Isar/HOL, an extension of Isabelle. A detailled exposition of this material -can be found in Markus Wenzel's PhD thesis~\cite{Wenzel-PhD}. +Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. A detailled +exposition of this material can be found in Markus Wenzel's PhD +thesis~\cite{Wenzel-PhD}. \input{Logic.tex}