*** empty log message ***
authornipkow
Wed Jul 10 07:20:02 2002 +0200 (2002-07-10)
changeset 1332953c4ec15cae0
parent 13328 703de709a64b
child 13330 c9e9b6add754
*** empty log message ***
doc-src/TutorialI/IsarOverview/Isar/Logic.thy
doc-src/TutorialI/IsarOverview/Isar/document/root.tex
     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.85 -\isakeyword{with}~\emph{facts} \quad = \quad
    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