author nipkow Wed Jul 10 07:20:02 2002 +0200 (2002-07-10) changeset 13329 53c4ec15cae0 parent 13328 703de709a64b child 13330 c9e9b6add754
*** empty log message ***
     1.1 --- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Tue Jul 09 23:05:26 2002 +0200
1.2 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 07:20:02 2002 +0200
1.3 @@ -33,13 +33,13 @@
1.4  Text starting with --'' is a comment.
1.5
1.6  Note that propositions in \isakeyword{assume} may but need not be
1.7 -separated by \isakeyword{and} whose purpose is to structure the
1.8 -assumptions into possibly named blocks, for example
1.9 +separated by \isakeyword{and}, whose purpose is to structure the
1.10 +assumptions into possibly named blocks. For example in
1.11  \begin{center}
1.12  \isakeyword{assume} @{text"A:"} $A_1$ $A_2$ \isakeyword{and} @{text"B:"} $A_3$
1.13  \isakeyword{and} $A_4$
1.14  \end{center}
1.15 -Here label @{text A} refers to the list of propositions $A_1$ $A_2$ and
1.16 +label @{text A} refers to the list of propositions $A_1$ $A_2$ and
1.17  label @{text B} to $A_3$.
1.18  *}
1.19
1.20 @@ -246,13 +246,15 @@
1.21    qed
1.22  qed
1.23  text{*\noindent Apart from demonstrating the strangeness of classical
1.24 -arguments by contradiction, this example also introduces three new constructs:
1.25 -\begin{itemize}
1.26 -\item \isakeyword{next} deals with multiple subgoals.  When showing
1.27 -@{term"A \<and> B"} we need to show both @{term A} and @{term B}.  Each subgoal
1.28 -is proved separately, in \emph{any} order. The individual proofs are
1.29 -separated by \isakeyword{next}.
1.30 -\end{itemize}
1.31 +arguments by contradiction, this example also introduces two new
1.32 +abbrebviations:
1.33 +\begin{center}
1.34 +\begin{tabular}{lcl}
1.35 +\isakeyword{hence} &=& \isakeyword{then} \isakeyword{have} \\
1.36 +\isakeyword{with}~\emph{facts} &=&
1.37 +\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
1.38 +\end{tabular}
1.39 +\end{center}
1.40  *}
1.41
1.42  subsection{*Avoiding duplication*}
1.43 @@ -269,7 +271,13 @@
1.44  text{*\noindent The \isakeyword{proof} always works on the conclusion,
1.45  @{prop"B \<and> A"} in our case, thus selecting $\land$-introduction. Hence
1.46  we must show @{prop B} and @{prop A}; both are proved by
1.47 -$\land$-elimination.
1.48 +$\land$-elimination and the proofs are separated by \isakeyword{next}:
1.49 +\begin{description}
1.50 +\item[\isakeyword{next}] deals with multiple subgoals. For example,
1.51 +when showing @{term"A \<and> B"} we need to show both @{term A} and @{term
1.52 +B}.  Each subgoal is proved separately, in \emph{any} order. The
1.53 +individual proofs are separated by \isakeyword{next}.
1.54 +\end{description}
1.55
1.56  This is all very well as long as formulae are small. Let us now look at some
1.57  devices to avoid repeating (possibly large) formulae. A very general method
1.58 @@ -384,9 +392,8 @@
1.59  \isakeyword{fix} and \isakeyword{assume} together with a soundness proof of
1.60  the elimination involved.
1.61
1.62 -Here is a proof of a well known tautology which employs another useful
1.63 -abbreviation: \isakeyword{hence} abbreviates \isakeyword{from}~@{text
1.64 -this}~\isakeyword{have}.  Figure out which rule is used where!  *}
1.65 +Here is a proof of a well known tautology.
1.66 +Figure out which rule is used where!  *}
1.67
1.68  lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
1.69  proof
1.70 @@ -418,7 +425,7 @@
1.71    qed
1.72  qed
1.73  text{*\noindent
1.74 -For a start, the example demonstrates three new language elements:
1.75 +For a start, the example demonstrates two new constructs:
1.76  \begin{itemize}
1.77  \item \isakeyword{let} introduces an abbreviation for a term, in our case
1.78  the witness for the claim, because the term occurs multiple times in the proof.
1.79 @@ -426,11 +433,6 @@
1.80  implicit what the two cases are: it is merely expected that the two subproofs
1.81  prove @{prop"P \<Longrightarrow> Q"} and @{prop"\<not>P \<Longrightarrow> Q"} for suitable @{term P} and
1.82  @{term Q}.
1.83 -\item \isakeyword{with} is an abbreviation:
1.84 -\begin{center}
1.86 -\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
1.87 -\end{center}
1.88  \end{itemize}
1.89  If you wonder how to \isakeyword{obtain} @{term y}:
1.90  via the predefined elimination rule @{thm rangeE[no_vars]}.
1.91 @@ -699,4 +701,20 @@
1.92  see very clearly how things fit together and permit ourselves the
1.93  obvious forward step @{text"IH[OF B]"}. *}
1.94
1.95 +consts rot :: "'a list \<Rightarrow> 'a list"
1.96 +recdef rot "measure length"
1.97 +"rot [] = []"
1.98 +"rot [x] = [x]"
1.99 +"rot (x#y#zs) = y # rot(x#zs)"
1.100 +
1.101 +lemma "length(rot xs) = length xs" (is "?P xs")
1.102 +proof (induct xs rule: rot.induct)
1.103 +  show "?P []" by simp
1.104 +next
1.105 +  fix x show "?P [x]" by simp
1.106 +next
1.107 +  fix x y zs assume "?P (x#zs)"
1.108 +  thus "?P (x#y#zs)" by simp
1.109 +qed
1.110 +
1.111  (*<*)end(*>*)

     2.1 --- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Tue Jul 09 23:05:26 2002 +0200
2.2 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Wed Jul 10 07:20:02 2002 +0200
2.3 @@ -32,8 +32,8 @@
2.4  %%% End:
2.5
2.6  \paragraph{Acknowledgment}
2.7 -I am deeply indebted to Markus Wenzel for conceiving Isar and for
2.8 -commenting on this document.
2.9 +I am deeply indebted to Markus Wenzel for conceiving Isar. Stefan Berghofer
2.10 +and Markus Wenzel commented on this document.
2.11
2.12  \begingroup
2.13  \bibliographystyle{plain} \small\raggedright\frenchspacing