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

author | nipkow |

Wed, 02 Oct 2002 15:26:07 +0200 | |

changeset 13620 | 61a23a43b783 |

parent 13619 | 584291949c23 |

child 13621 | 75ae05e894fa |

*** empty log message ***

--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Tue Oct 01 20:54:17 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Wed Oct 02 15:26:07 2002 +0200 @@ -147,7 +147,7 @@ case 0 thus ?case by simp next case (Suc n) -- {*\isakeyword{fix} @{term m} \isakeyword{assume} @{text Suc}: @{text[source]"?m < n \<Longrightarrow> P ?m"} @{prop[source]"m < Suc n"}*} - show ?case -- {*@{term ?case}*} + show ?case -- {*@{term ?case}*} proof cases assume eq: "m = n" from Suc and A have "P n" by blast @@ -165,7 +165,7 @@ The statement of the lemma is interesting because it deviates from the style in the Tutorial~\cite{LNCS2283}, which suggests to introduce @{text"\<forall>"} or -@{text"\<longrightarrow>"} into a theorem to strengthen it for induction. In structured Isar +@{text"\<longrightarrow>"} into a theorem to strengthen it for induction. In Isar proofs we can use @{text"\<And>"} and @{text"\<Longrightarrow>"} instead. This simplifies the proof and means we do not have to convert between the two kinds of connectives. @@ -174,7 +174,7 @@ subsection{*Rule induction*} text{* HOL also supports inductively defined sets. See \cite{LNCS2283} -for details. As an example we define our own version of reflexive +for details. As an example we define our own version of the reflexive transitive closure of a relation --- HOL provides a predefined one as well.*} consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) inductive "r*" @@ -227,9 +227,9 @@ see very clearly how things fit together and permit ourselves the obvious forward step @{text"IH[OF B]"}. -The notation \isakeyword{case}~\isa{(constructor} \emph{vars}\isa{)} -is also supported for inductive definitions. The constructor is (the -names of) the rule and the \emph{vars} fix the free variables in the +The notation `\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}' +is also supported for inductive definitions. The \emph{constructor} is (the +name of) the rule and the \emph{vars} fix the free variables in the rule; the order of the \emph{vars} must correspond to the \emph{alphabetical order} of the variables as they appear in the rule. For example, we could start the above detailed proof of the induction @@ -291,7 +291,7 @@ The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01} for how to reason with chains of equations) to demonstrate that the -\isakeyword{case}~\isa{(constructor} \emph{vars}\isa{)} notation also +`\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}' notation also works for arbitrary induction theorems with numbered cases. The order of the \emph{vars} corresponds to the order of the @{text"\<And>"}-quantified variables in each case of the induction

--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Tue Oct 01 20:54:17 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Wed Oct 02 15:26:07 2002 +0200 @@ -97,9 +97,9 @@ \end{center} where \emph{fact} stands for the name of a previously proved proposition, e.g.\ an assumption, an intermediate result or some global -theorem, which may also be modified with @{text of}, @{text OF} etc. +theorem, which may also be modified with @{text OF} etc. The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it -how it choses. If the \emph{proof} starts with a plain \isakeyword{proof}, +how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof}, an elimination rule (from a predefined list) is applied whose first premise is solved by the \emph{fact}. Thus the proof above is equivalent to the following one: *} @@ -201,7 +201,7 @@ for \isakeyword{from}~@{term A1}~\dots~@{term An}. This avoids having to introduce names for all of the sequence elements. *} -text{* Although we have only seen a few introduction and elemination rules so +text{* Although we have only seen a few introduction and elimination rules so far, Isar's predefined rules include all the usual natural deduction rules. We conclude our exposition of propositional logic with an extended example --- which rules are used implicitly where? *} @@ -278,7 +278,7 @@ text{*\noindent Any formula may be followed by @{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern to be matched against the formula, instantiating the @{text"?"}-variables in -the pattern. Subsequent uses of these variables in other terms simply causes +the pattern. Subsequent uses of these variables in other terms 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 @@ -440,12 +440,12 @@ assume "y \<in> ?S" hence "y \<notin> f y" by simp hence "y \<notin> ?S" by(simp add:fy) - thus False by contradiction + thus False by contradiction next assume "y \<notin> ?S" hence "y \<in> f y" by simp hence "y \<in> ?S" by(simp add:fy) - thus False by contradiction + thus False by contradiction qed qed qed @@ -546,7 +546,7 @@ text{*\noindent You may need to resort to this technique if an automatic step fails to prove the desired proposition. -When converting a proof from tactic-style into Isar you can proceeed +When converting a proof from tactic-style into Isar you can proceed in a top-down manner: parts of the proof can be left in script form while to outer structure is already expressed in Isar. *}

--- a/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex Tue Oct 01 20:54:17 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex Wed Oct 02 15:26:07 2002 +0200 @@ -8,7 +8,7 @@ language but concentrate on the essentials. Neither do we give a formal semantics of Isar. Instead we introduce Isar by example. Again this is intentional: we believe that the language ``speaks for -itself'' in the same way that traditional mathamtical proofs do, which +itself'' in the same way that traditional mathematical proofs do, which are also introduced by example rather than by teaching students logic first. A detailed exposition of Isar can be found in Markus Wenzel's PhD thesis~\cite{Wenzel-PhD} and the Isar reference @@ -27,26 +27,23 @@ tactics. A radically different approach was taken by the Mizar -system -%~\cite{Mizar} -where proofs are written a stylized 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 be readable. From a system development point of view there is -a second important argument against tactic-style proofs: they are much -harder to maintain when the system is modified. The reason is as -follows. Since it is usually quite unclear what exactly is proved at -some point in the middle of a command sequence, updating a failed -proof often requires executing the proof up to the point of failure -using the old version of the system. In contrast, mathematics-like -proofs contain enough information to tell you what is proved at any -point. +system~\cite{Rudnicki92} where proofs are written in a stylized 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 +be readable. From a system development point of view there is a second +important argument against tactic-style proofs: they are much harder to +maintain when the system is modified. The reason is as follows. Since it is +usually quite unclear what exactly is proved at some point in the middle of a +command sequence, updating a failed proof often requires executing the proof +up to the point of failure using the old version of the system. In contrast, +mathematics-like proofs contain enough information to tell you what is proved +at any point. For these reasons the Isabelle system, originally firmly in the LCF-tradition, was extended with a language for writing structured proofs in a mathematics-like style. As the name already indicates, -Isar was certainly inspired by Mizar. However, there are very many +Isar was certainly inspired by Mizar. However, there are many differences. For a start, Isar is generic: only a few of the language constructs described below are specific to HOL; many are generic and thus available for any logic defined in Isabelle, e.g.\ ZF. @@ -86,9 +83,8 @@ \end{center} A proof can be either compound (\isakeyword{proof} -- \isakeyword{qed}) or atomic (\isakeyword{by}). A \emph{method} is a -proof method offered by the underlying theorem prover, for example -\isa{rule} or \isa{simp} in Isabelle. Thus this grammar is -generic both w.r.t.\ the logic and the theorem prover. +proof method (tactic) offered by the underlying theorem prover. +Thus this grammar is generic both w.r.t.\ the logic and the theorem prover. This is a typical proof skeleton: \begin{center} @@ -114,18 +110,18 @@ 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_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$. -Free variables that may be instantiated (``logical variables'' in -Prolog parlance) are prefixed with a \isa{?}. Typically, theorems are -stated with ordinary free variables but after the proof those are -replaced by \isa{?}-variables. Thus the theorem can be used with -arbitrary instances of its free variables. +Free variables that may be instantiated (``logical variables'' in Prolog +parlance) are prefixed with a \isa{?}. Typically, theorems are stated with +ordinary free variables but after the proof those are automatically replaced +by \isa{?}-variables. Thus the theorem can be used with arbitrary instances +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 @@ -141,12 +137,11 @@ natural deduction. Section~\ref{sec:Induct} is dedicated to induction, the key reasoning principle for computer science applications. -There are at least two further areas where Isar provides specific -support, but which we do not document here: reasoning by chains of -(in)equations is described elsewhere~\cite{BauerW-TPHOLs01}, whereas -reasoning about axiomatically defined structures by means of so called -``locales'' \cite{KWP-TPHOLs99} is only described in a very early -form and has evolved much since then. +There are at least two further areas where Isar provides specific support, +but which we do not document here. Reasoning by chains of (in)equations is +described elsewhere~\cite{BauerW-TPHOLs01}. Reasoning about axiomatically +defined structures by means of so called ``locales'' was first described in +\cite{KWP-TPHOLs99} but has evolved much since then. Do not be mislead by the simplicity of the formulae being proved, especially in the beginning. Isar has been used very successfully in

--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.bib Tue Oct 01 20:54:17 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.bib Wed Oct 02 15:26:07 2002 +0200 @@ -6,7 +6,7 @@ title={Calculational Reasoning Revisited --- an {Isabelle/Isar} Experience}, booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001}, editor={R. Boulton and P. Jackson}, -year=2001,publisher=Springer,series=LNCS,volume=2152} +year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"} @book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth", title="Edinburgh {LCF}: a Mechanised Logic of Computation", @@ -24,6 +24,15 @@ publisher=Springer,series=LNCS,volume=2283,year=2002, note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}} +@article{KleinN-TCS,author={Gerwin Klein and Tobias Nipkow}, +title={Verified Bytecode Verifiers}, +journal=TCS,year=2002,note={To appear}} + +@InProceedings{Rudnicki92,author={P. Rudnicki}, +title={An Overview of the {Mizar} Project}, +booktitle={Workshop on Types for Proofs and Programs}, +year=1992,organization={Chalmers University of Technology}} + @manual{Isar-Ref-Man,author="Markus Wenzel", title="The Isabelle/Isar Reference Manual", organization={Technische Universit{\"a}t M{\"u}nchen},year=2002,