# HG changeset patch # User nipkow # Date 1026377310 -7200 # Node ID 867f876589e7aa9ded54b929110def8791d7d793 # Parent 6918b6d5192b31f0ee6123b4093e545938f8bc52 *** empty log message *** diff -r 6918b6d5192b -r 867f876589e7 doc-src/TutorialI/IsarOverview/Isar/Logic.thy --- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Thu Jul 11 09:47:15 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Thu Jul 11 10:48:30 2002 +0200 @@ -22,19 +22,20 @@ \begin{tabular}{@ {}ll} \isakeyword{proof}\\ \hspace*{3ex}\isakeyword{assume} @{text"\""}\emph{the-assm}@{text"\""}\\ -\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""} & -- intermediate result\\ +\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""} & --- intermediate result\\ \hspace*{3ex}\vdots\\ -\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""} & -- intermediate result\\ +\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""} & --- intermediate result\\ \hspace*{3ex}\isakeyword{show} @{text"\""}\emph{the-concl}@{text"\""}\\ \isakeyword{qed} \end{tabular} \end{center} It proves \emph{the-assm}~@{text"\"}~\emph{the-concl}. -Text starting with ``--'' is a comment. +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 in +Note that \emph{propositions} (following \isakeyword{assume} etc) +may but need not be +separated by \isakeyword{and}, whose purpose is to structure them +into possibly named blocks. For example in \begin{center} \isakeyword{assume} @{text"A:"} $A_1$ $A_2$ \isakeyword{and} @{text"B:"} $A_3$ \isakeyword{and} $A_4$ @@ -120,7 +121,7 @@ proof assume AB: "A \ B" show "B \ A" - proof (rule conjE[OF AB]) -- {*@{prop"(A \ B \ R) \ R"}*} + proof (rule conjE[OF AB]) -- {*@{text"conjE[OF AB]"}: @{thm conjE[OF AB]} *} assume A and B show ?thesis .. qed @@ -356,9 +357,9 @@ @{text"\"}. Here is a sample proof, annotated with the rules that are applied implicitly: *} lemma assumes P: "\x. P x" shows "\x. P(f x)" -proof -- "@{thm[source]allI}: @{thm allI[no_vars]}" +proof -- "@{thm[source]allI}: @{thm allI}" fix a - from P show "P(f a)" .. --"@{thm[source]allE}: @{thm allE[no_vars]}" + from P show "P(f a)" .. --"@{thm[source]allE}: @{thm allE}" 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 @@ -533,7 +534,7 @@ case Cons thus ?thesis by simp qed text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates -\isakeyword{assume}~@{prop"x = []"} and \isakeyword{case}~@{text Cons} +\isakeyword{assume}~@{prop"xs = []"} 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 obscure proofs) and have not even shown @@ -555,10 +556,7 @@ qed -subsection{*Induction*} - - -subsubsection{*Structural induction*} +subsection{*Structural induction*} text{* We start with a simple inductive proof where both cases are proved automatically: *} lemma "2 * (\im"} in the main \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}. *} +parameters in the @{term Suc} case are to be named @{text n} and @{text m}. *} -subsubsection{*Rule induction*} +subsection{*Rule induction*} text{* We define our own version of reflexive transitive closure of a relation *} @@ -704,9 +701,9 @@ subsection{*More induction*} text{* We close the section by demonstrating how arbitrary induction rules -are applied. As a simple example we have chose recursion induction, i.e.\ +are applied. As a simple example we have chosen recursion induction, i.e.\ induction based on a recursive function definition. The example is an unusual -definition of rotation of a list: *} +definition of rotation: *} consts rot :: "'a list \ 'a list" recdef rot "measure length" @@ -726,7 +723,8 @@ fix x y zs assume "?P (x#zs)" thus "?P (x#y#zs)" by simp qed -text{* This proof skeletons works for arbitrary induction rules, not just +text{*\noindent +This proof skeleton works for arbitrary induction rules, not just @{thm[source]rot.induct}. In the following proof we rely on a default naming scheme for cases: they are @@ -743,8 +741,10 @@ case 3 thus ?case by simp qed -text{*Of course both proofs are so simple that they can be condensed to*} +text{*\noindent Why can case 2 get away with \isakeyword{show} instead of +\isakeyword{thus}? + +Of course both proofs are so simple that they can be condensed to*} (*<*)lemma "xs \ [] \ rot xs = tl xs @ [hd xs]"(*>*) by (induct xs rule: rot.induct, simp_all) - (*<*)end(*>*) diff -r 6918b6d5192b -r 867f876589e7 doc-src/TutorialI/IsarOverview/Isar/document/root.tex --- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Thu Jul 11 09:47:15 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Thu Jul 11 10:48:30 2002 +0200 @@ -12,7 +12,7 @@ \title{A Compact Overview of Structured Proofs in Isar/HOL} \author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\ - \url{http://www.in.tum.de/~nipkow/}} + {\small\url{http://www.in.tum.de/~nipkow/}}} \date{} \maketitle @@ -31,9 +31,11 @@ %%% TeX-master: "root" %%% End: +{\small \paragraph{Acknowledgment} -I am deeply indebted to Markus Wenzel for conceiving Isar. Stefan Berghofer -and Markus Wenzel commented on this document. +I am deeply indebted to Markus Wenzel for conceiving Isar. Stefan Berghofer, +Gerwin Klein, Norbert Schirmer and Markus Wenzel commented on this document. +} \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing