author nipkow Wed, 31 Jul 2002 17:42:38 +0200 changeset 13439 2f98365f57a8 parent 13438 527811f00c56 child 13440 cdde97e1db1c
*** empty log message ***
--- a/doc-src/TutorialI/Datatype/Fundata.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -40,8 +40,7 @@
(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
apply(induct_tac T, rename_tac F)(*>*)
txt{*\noindent
-Because of the function type, the
-the proof state after induction looks unusual.
+Because of the function type, the proof state after induction looks unusual.
Notice the quantified induction hypothesis:
@{subgoals[display,indent=0]}
*}
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -51,8 +51,7 @@
%
\begin{isamarkuptxt}%
\noindent
-Because of the function type, the
-the proof state after induction looks unusual.
+Because of the function type, the proof state after induction looks unusual.
Notice the quantified induction hypothesis:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -118,7 +118,7 @@
output as @{text "A\<^sup>\<star>"}.

\medskip Replacing our definition of @{text xor} by the following
-  specifies a Isabelle symbol for the new operator:
+  specifies an Isabelle symbol for the new operator:
*}

(*<*)
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -122,7 +122,7 @@
output as \isa{A\isactrlsup {\isasymstar}}.

\medskip Replacing our definition of \isa{xor} by the following
-  specifies a Isabelle symbol for the new operator:%
+  specifies an Isabelle symbol for the new operator:%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
--- a/doc-src/TutorialI/Overview/IsaMakefile	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/IsaMakefile	Wed Jul 31 17:42:38 2002 +0200
@@ -14,7 +14,7 @@

LNCS: $(LOG)/HOL-LNCS.gz -$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/*.thy
+$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/document/root.bib LNCS/*.thy @$(USEDIR) HOL LNCS


--- a/doc-src/TutorialI/Overview/LNCS/FP0.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP0.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -15,17 +15,6 @@
"rev (x # xs)  = (rev xs) @ (x # [])"

theorem rev_rev [simp]: "rev(rev xs) = xs"
-(*<*)oops(*>*)
+(*<*)oops(*>*)text_raw{*\isanewline\isanewline*}

-text{*
-\begin{exercise}
-Define a datatype of binary trees and a function @{term mirror}
-that mirrors a binary tree by swapping subtrees recursively. Prove
-@{prop"mirror(mirror t) = t"}.
-
-Define a function @{term flatten} that flattens a tree into a list
-by traversing it in infix order. Prove
-@{prop"flatten(mirror t) = rev(flatten t)"}.
-\end{exercise}
-*}
end
--- a/doc-src/TutorialI/Overview/LNCS/Ind.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -61,11 +61,11 @@
consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*"  999)
inductive "r*"
intros
-rtc_refl[iff]:  "(x,x) \<in> r*"
-rtc_step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+refl[iff]:  "(x,x) \<in> r*"
+step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"

lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
-by(blast intro: rtc_step);
+by(blast intro: rtc.step);

lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
apply(erule rtc.induct)
@@ -75,12 +75,12 @@
"(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
apply(erule rtc.induct)
apply(blast);
-apply(blast intro: rtc_step);
+apply(blast intro: rtc.step);
done

text{*
\begin{exercise}
-Show that the converse of @{thm[source]rtc_step} also holds:
+Show that the converse of @{thm[source]rtc.step} also holds:
@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
\end{exercise}*}

--- a/doc-src/TutorialI/Overview/LNCS/document/root.bib	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/document/root.bib	Wed Jul 31 17:42:38 2002 +0200
@@ -3,4 +3,5 @@

@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}
+publisher=Springer,series=LNCS,volume=2283,year=2002,
+note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
--- a/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -11,7 +11,8 @@
\begin{document}

\title{A Compact Overview of Isabelle/HOL}
-\author{Tobias Nipkow}
+\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
+ \small\url{http://www.in.tum.de/~nipkow/}}
\date{}
\maketitle

@@ -28,6 +29,16 @@
\subsection{An Introductory Theory}
\input{FP0.tex}

+\begin{exercise}
+Define a datatype of binary trees and a function \isa{mirror}
+that mirrors a binary tree by swapping subtrees recursively. Prove
+\isa{mirror(mirror t) = t}.
+
+Define a function \isa{flatten} that flattens a tree into a list
+by traversing it in infix order. Prove
+\isa{flatten(mirror t) = rev(flatten t)}.
+\end{exercise}
+
\subsection{More Constructs}
\input{FP1.tex}

--- a/doc-src/TutorialI/Rules/rules.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -4,7 +4,7 @@

This chapter outlines the concepts and techniques that underlie reasoning
in Isabelle.  Until now, we have proved everything using only induction and
-simplification, but any serious verification project require more elaborate
+simplification, but any serious verification project requires more elaborate
forms of inference.  The chapter also introduces the fundamentals of
predicate logic.  The first examples in this chapter will consist of
detailed, low-level proof steps.  Later, we shall see how to automate such
--- a/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -11,7 +11,7 @@
function is a set, and the inverse image of a function maps sets to sets.

This chapter will be useful to anybody who plans to develop a substantial
-proof.  sets are convenient for formalizing  computer science concepts such
+proof.  Sets are convenient for formalizing  computer science concepts such
as grammars, logical calculi and state transition systems.  Isabelle can
prove many statements involving sets automatically.

@@ -610,7 +610,7 @@
general syntax for comprehension:
\begin{isabelle}
\isacommand{lemma}\ "fA\ \isasymunion\ gA\ =\ ({\isasymUnion}x{\isasymin}A.\ \isacharbraceleft f\ x,\ g\
-x\isacharbraceright)
+x\isacharbraceright)"
\par\smallskip
\isacommand{lemma}\ "f\ \ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ \isacharbraceleft f(x,y)\ \isacharbar\ x\ y.\ P\ x\
y\isacharbraceright"
--- a/doc-src/TutorialI/basics.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/basics.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -281,7 +281,7 @@
variables are automatically renamed to avoid clashes with free variables. In
addition, Isabelle has a third kind of variable, called a \textbf{schematic
variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
-which must a~\isa{?} as its first character.
+which must have a~\isa{?} as its first character.
Logically, an unknown is a free variable. But it may be
instantiated by another term during the proof process. For example, the
mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},`