*** empty log message ***
authornipkow
Wed Jul 31 17:42:38 2002 +0200 (2002-07-31)
changeset 134392f98365f57a8
parent 13438 527811f00c56
child 13440 cdde97e1db1c
*** empty log message ***
doc-src/TutorialI/Datatype/Fundata.thy
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Documents/Documents.thy
doc-src/TutorialI/Documents/document/Documents.tex
doc-src/TutorialI/Overview/IsaMakefile
doc-src/TutorialI/Overview/LNCS/FP0.thy
doc-src/TutorialI/Overview/LNCS/Ind.thy
doc-src/TutorialI/Overview/LNCS/document/root.bib
doc-src/TutorialI/Overview/LNCS/document/root.tex
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/basics.tex
     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[2] 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"   ("_*" [1000] 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}\ "f`A\ \isasymunion\ g`A\ =\ ({\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},