author nipkow Wed Jul 31 17:42:38 2002 +0200 (2002-07-31) changeset 13439 2f98365f57a8 parent 13438 527811f00c56 child 13440 cdde97e1db1c
*** empty log message ***
     1.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy	Wed Jul 31 16:10:24 2002 +0200
1.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy	Wed Jul 31 17:42:38 2002 +0200
1.3 @@ -40,8 +40,7 @@
1.4  (*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
1.5  apply(induct_tac T, rename_tac F)(*>*)
1.6  txt{*\noindent
1.7 -Because of the function type, the
1.8 -the proof state after induction looks unusual.
1.9 +Because of the function type, the proof state after induction looks unusual.
1.10  Notice the quantified induction hypothesis:
1.11  @{subgoals[display,indent=0]}
1.12  *}

     2.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jul 31 16:10:24 2002 +0200
2.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jul 31 17:42:38 2002 +0200
2.3 @@ -51,8 +51,7 @@
2.4  %
2.5  \begin{isamarkuptxt}%
2.6  \noindent
2.7 -Because of the function type, the
2.8 -the proof state after induction looks unusual.
2.9 +Because of the function type, the proof state after induction looks unusual.
2.10  Notice the quantified induction hypothesis:
2.11  \begin{isabelle}%
2.12  \ {\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

     3.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 16:10:24 2002 +0200
3.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 17:42:38 2002 +0200
3.3 @@ -118,7 +118,7 @@
3.4    output as @{text "A\<^sup>\<star>"}.
3.5
3.6    \medskip Replacing our definition of @{text xor} by the following
3.7 -  specifies a Isabelle symbol for the new operator:
3.8 +  specifies an Isabelle symbol for the new operator:
3.9  *}
3.10
3.11  (*<*)

     4.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 16:10:24 2002 +0200
4.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 17:42:38 2002 +0200
4.3 @@ -122,7 +122,7 @@
4.4    output as \isa{A\isactrlsup {\isasymstar}}.
4.5
4.6    \medskip Replacing our definition of \isa{xor} by the following
4.7 -  specifies a Isabelle symbol for the new operator:%
4.8 +  specifies an Isabelle symbol for the new operator:%
4.9  \end{isamarkuptext}%
4.10  \isamarkuptrue%
4.11  \isamarkupfalse%

     5.1 --- a/doc-src/TutorialI/Overview/IsaMakefile	Wed Jul 31 16:10:24 2002 +0200
5.2 +++ b/doc-src/TutorialI/Overview/IsaMakefile	Wed Jul 31 17:42:38 2002 +0200
5.3 @@ -14,7 +14,7 @@
5.4
5.5  LNCS: $(LOG)/HOL-LNCS.gz 5.6 5.7 -$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/*.thy
5.8 +$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/document/root.bib LNCS/*.thy 5.9 @$(USEDIR) HOL LNCS
5.10
5.11

     6.1 --- a/doc-src/TutorialI/Overview/LNCS/FP0.thy	Wed Jul 31 16:10:24 2002 +0200
6.2 +++ b/doc-src/TutorialI/Overview/LNCS/FP0.thy	Wed Jul 31 17:42:38 2002 +0200
6.3 @@ -15,17 +15,6 @@
6.4  "rev (x # xs)  = (rev xs) @ (x # [])"
6.5
6.6  theorem rev_rev [simp]: "rev(rev xs) = xs"
6.7 -(*<*)oops(*>*)
6.8 +(*<*)oops(*>*)text_raw{*\isanewline\isanewline*}
6.9
6.10 -text{*
6.11 -\begin{exercise}
6.12 -Define a datatype of binary trees and a function @{term mirror}
6.13 -that mirrors a binary tree by swapping subtrees recursively. Prove
6.14 -@{prop"mirror(mirror t) = t"}.
6.15 -
6.16 -Define a function @{term flatten} that flattens a tree into a list
6.17 -by traversing it in infix order. Prove
6.18 -@{prop"flatten(mirror t) = rev(flatten t)"}.
6.19 -\end{exercise}
6.20 -*}
6.21  end

     7.1 --- a/doc-src/TutorialI/Overview/LNCS/Ind.thy	Wed Jul 31 16:10:24 2002 +0200
7.2 +++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy	Wed Jul 31 17:42:38 2002 +0200
7.3 @@ -61,11 +61,11 @@
7.4  consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*"  999)
7.5  inductive "r*"
7.6  intros
7.7 -rtc_refl[iff]:  "(x,x) \<in> r*"
7.8 -rtc_step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
7.9 +refl[iff]:  "(x,x) \<in> r*"
7.10 +step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
7.11
7.12  lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
7.13 -by(blast intro: rtc_step);
7.14 +by(blast intro: rtc.step);
7.15
7.16  lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
7.17  apply(erule rtc.induct)
7.18 @@ -75,12 +75,12 @@
7.19    "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
7.20  apply(erule rtc.induct)
7.21   apply(blast);
7.22 -apply(blast intro: rtc_step);
7.23 +apply(blast intro: rtc.step);
7.24  done
7.25
7.26  text{*
7.27  \begin{exercise}
7.28 -Show that the converse of @{thm[source]rtc_step} also holds:
7.29 +Show that the converse of @{thm[source]rtc.step} also holds:
7.30  @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
7.31  \end{exercise}*}
7.32

     8.1 --- a/doc-src/TutorialI/Overview/LNCS/document/root.bib	Wed Jul 31 16:10:24 2002 +0200
8.2 +++ b/doc-src/TutorialI/Overview/LNCS/document/root.bib	Wed Jul 31 17:42:38 2002 +0200
8.3 @@ -3,4 +3,5 @@
8.4
8.5  @book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
8.6  title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
8.7 -publisher=Springer,series=LNCS,volume=2283,year=2002}
8.8 +publisher=Springer,series=LNCS,volume=2283,year=2002,
8.9 +note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}

     9.1 --- a/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 16:10:24 2002 +0200
9.2 +++ b/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 17:42:38 2002 +0200
9.3 @@ -11,7 +11,8 @@
9.4  \begin{document}
9.5
9.6  \title{A Compact Overview of Isabelle/HOL}
9.7 -\author{Tobias Nipkow}
9.8 +\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
9.9 + \small\url{http://www.in.tum.de/~nipkow/}}
9.10  \date{}
9.11  \maketitle
9.12
9.13 @@ -28,6 +29,16 @@
9.14  \subsection{An Introductory Theory}
9.15  \input{FP0.tex}
9.16
9.17 +\begin{exercise}
9.18 +Define a datatype of binary trees and a function \isa{mirror}
9.19 +that mirrors a binary tree by swapping subtrees recursively. Prove
9.20 +\isa{mirror(mirror t) = t}.
9.21 +
9.22 +Define a function \isa{flatten} that flattens a tree into a list
9.23 +by traversing it in infix order. Prove
9.24 +\isa{flatten(mirror t) = rev(flatten t)}.
9.25 +\end{exercise}
9.26 +
9.27  \subsection{More Constructs}
9.28  \input{FP1.tex}
9.29

    10.1 --- a/doc-src/TutorialI/Rules/rules.tex	Wed Jul 31 16:10:24 2002 +0200
10.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jul 31 17:42:38 2002 +0200
10.3 @@ -4,7 +4,7 @@
10.4
10.5  This chapter outlines the concepts and techniques that underlie reasoning
10.6  in Isabelle.  Until now, we have proved everything using only induction and
10.7 -simplification, but any serious verification project require more elaborate
10.8 +simplification, but any serious verification project requires more elaborate
10.9  forms of inference.  The chapter also introduces the fundamentals of
10.10  predicate logic.  The first examples in this chapter will consist of
10.11  detailed, low-level proof steps.  Later, we shall see how to automate such

    11.1 --- a/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 16:10:24 2002 +0200
11.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 17:42:38 2002 +0200
11.3 @@ -11,7 +11,7 @@
11.4  function is a set, and the inverse image of a function maps sets to sets.
11.5
11.6  This chapter will be useful to anybody who plans to develop a substantial
11.7 -proof.  sets are convenient for formalizing  computer science concepts such
11.8 +proof.  Sets are convenient for formalizing  computer science concepts such
11.9  as grammars, logical calculi and state transition systems.  Isabelle can
11.10  prove many statements involving sets automatically.
11.11
11.12 @@ -610,7 +610,7 @@
11.13  general syntax for comprehension:
11.14  \begin{isabelle}
11.15  \isacommand{lemma}\ "fA\ \isasymunion\ gA\ =\ ({\isasymUnion}x{\isasymin}A.\ \isacharbraceleft f\ x,\ g\
11.16 -x\isacharbraceright)
11.17 +x\isacharbraceright)"
11.18  \par\smallskip
11.19  \isacommand{lemma}\ "f\ \ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ \isacharbraceleft f(x,y)\ \isacharbar\ x\ y.\ P\ x\
11.20  y\isacharbraceright"

    12.1 --- a/doc-src/TutorialI/basics.tex	Wed Jul 31 16:10:24 2002 +0200
12.2 +++ b/doc-src/TutorialI/basics.tex	Wed Jul 31 17:42:38 2002 +0200
12.3 @@ -281,7 +281,7 @@
12.4  variables are automatically renamed to avoid clashes with free variables. In
12.5  addition, Isabelle has a third kind of variable, called a \textbf{schematic
12.6    variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
12.7 -which must a~\isa{?} as its first character.
12.8 +which must have a~\isa{?} as its first character.
12.9  Logically, an unknown is a free variable. But it may be
12.10  instantiated by another term during the proof process. For example, the
12.11  mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
`