*** empty log message ***
authornipkow
Thu Jan 25 15:31:31 2001 +0100 (2001-01-25)
changeset 109785eebea8f359f
parent 10977 4b47d8aaf5af
child 10979 3da4543034e7
*** empty log message ***
doc-src/TutorialI/Advanced/document/simp.tex
doc-src/TutorialI/Advanced/simp.thy
doc-src/TutorialI/Ifexpr/Ifexpr.thy
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/Inductive/advanced-examples.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/ROOT.ML
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Trie/Trie.thy
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/Types/Overloading2.thy
doc-src/TutorialI/Types/document/Overloading2.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/Advanced/document/simp.tex	Thu Jan 25 11:59:52 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Advanced/document/simp.tex	Thu Jan 25 15:31:31 2001 +0100
     1.3 @@ -94,8 +94,8 @@
     1.4  once they apply, they can be used forever. The simplifier is aware of this
     1.5  danger and treats permutative rules by means of a special strategy, called
     1.6  \bfindex{ordered rewriting}: a permutative rewrite
     1.7 -rule is only applied if the term becomes ``smaller'' (with respect to a fixed
     1.8 -lexicographic ordering on terms). For example, commutativity rewrites
     1.9 +rule is only applied if the term becomes smaller with respect to a fixed
    1.10 +lexicographic ordering on terms. For example, commutativity rewrites
    1.11  \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly
    1.12  smaller than \isa{b\ {\isacharplus}\ a}.  Permutative rewrite rules can be turned into
    1.13  simplification rules in the usual manner via the \isa{simp} attribute; the
    1.14 @@ -150,7 +150,7 @@
    1.15  form (this will always be the case unless you have done something
    1.16  strange) where each occurrence of an unknown is of the form
    1.17  $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
    1.18 -variables. Thus all ``standard'' rewrite rules, where all unknowns are
    1.19 +variables. Thus all ordinary rewrite rules, where all unknowns are
    1.20  of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are OK: if an unknown is
    1.21  of base type, it cannot have any arguments. Additionally, the rule
    1.22  \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also OK, in
     2.1 --- a/doc-src/TutorialI/Advanced/simp.thy	Thu Jan 25 11:59:52 2001 +0100
     2.2 +++ b/doc-src/TutorialI/Advanced/simp.thy	Thu Jan 25 15:31:31 2001 +0100
     2.3 @@ -79,8 +79,8 @@
     2.4  once they apply, they can be used forever. The simplifier is aware of this
     2.5  danger and treats permutative rules by means of a special strategy, called
     2.6  \bfindex{ordered rewriting}: a permutative rewrite
     2.7 -rule is only applied if the term becomes ``smaller'' (with respect to a fixed
     2.8 -lexicographic ordering on terms). For example, commutativity rewrites
     2.9 +rule is only applied if the term becomes smaller with respect to a fixed
    2.10 +lexicographic ordering on terms. For example, commutativity rewrites
    2.11  @{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
    2.12  smaller than @{term"b+a"}.  Permutative rewrite rules can be turned into
    2.13  simplification rules in the usual manner via the @{text simp} attribute; the
    2.14 @@ -131,7 +131,7 @@
    2.15  form (this will always be the case unless you have done something
    2.16  strange) where each occurrence of an unknown is of the form
    2.17  $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
    2.18 -variables. Thus all ``standard'' rewrite rules, where all unknowns are
    2.19 +variables. Thus all ordinary rewrite rules, where all unknowns are
    2.20  of base type, for example @{thm add_assoc}, are OK: if an unknown is
    2.21  of base type, it cannot have any arguments. Additionally, the rule
    2.22  @{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also OK, in
     3.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jan 25 11:59:52 2001 +0100
     3.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jan 25 15:31:31 2001 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4  the constructs introduced above.
     3.5  *}
     3.6  
     3.7 -subsubsection{*How Can We Model Boolean Expressions?*}
     3.8 +subsubsection{*Modelling Boolean Expressions*}
     3.9  
    3.10  text{*
    3.11  We want to represent boolean expressions built up from variables and
    3.12 @@ -28,7 +28,7 @@
    3.13  For example, the formula $P@0 \land \neg P@1$ is represented by the term
    3.14  @{term"And (Var 0) (Neg(Var 1))"}.
    3.15  
    3.16 -\subsubsection{What is the Value of a Boolean Expression?}
    3.17 +\subsubsection{The Value of a Boolean Expression}
    3.18  
    3.19  The value of a boolean expression depends on the value of its variables.
    3.20  Hence the function @{text"value"} takes an additional parameter, an
    3.21 @@ -66,9 +66,8 @@
    3.22                                          else valif e env)";
    3.23  
    3.24  text{*
    3.25 -\subsubsection{Transformation Into and of If-Expressions}
    3.26 +\subsubsection{Converting Boolean and If-Expressions}
    3.27  
    3.28 -\REMARK{is this the title you wanted?}
    3.29  The type @{typ"boolex"} is close to the customary representation of logical
    3.30  formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to
    3.31  translate from @{typ"boolex"} into @{typ"ifex"}:
     4.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Jan 25 11:59:52 2001 +0100
     4.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Jan 25 15:31:31 2001 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4  the constructs introduced above.%
     4.5  \end{isamarkuptext}%
     4.6  %
     4.7 -\isamarkupsubsubsection{How Can We Model Boolean Expressions?%
     4.8 +\isamarkupsubsubsection{Modelling Boolean Expressions%
     4.9  }
    4.10  %
    4.11  \begin{isamarkuptext}%
    4.12 @@ -30,7 +30,7 @@
    4.13  For example, the formula $P@0 \land \neg P@1$ is represented by the term
    4.14  \isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}.
    4.15  
    4.16 -\subsubsection{What is the Value of a Boolean Expression?}
    4.17 +\subsubsection{The Value of a Boolean Expression}
    4.18  
    4.19  The value of a boolean expression depends on the value of its variables.
    4.20  Hence the function \isa{value} takes an additional parameter, an
    4.21 @@ -64,9 +64,8 @@
    4.22  {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
    4.23  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}%
    4.24  \begin{isamarkuptext}%
    4.25 -\subsubsection{Transformation Into and of If-Expressions}
    4.26 +\subsubsection{Converting Boolean and If-Expressions}
    4.27  
    4.28 -\REMARK{is this the title you wanted?}
    4.29  The type \isa{boolex} is close to the customary representation of logical
    4.30  formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
    4.31  translate from \isa{boolex} into \isa{ifex}:%
     5.1 --- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Thu Jan 25 11:59:52 2001 +0100
     5.2 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Thu Jan 25 15:31:31 2001 +0100
     5.3 @@ -137,7 +137,7 @@
     5.4  Applying this as an elimination rule yields one case where \isa{even.cases}
     5.5  would yield two.  Rule inversion works well when the conclusions of the
     5.6  introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
     5.7 -(list `cons'); freeness reasoning discards all but one or two cases.
     5.8 +(list ``cons''); freeness reasoning discards all but one or two cases.
     5.9  
    5.10  In the \isacommand{inductive\_cases} command we supplied an
    5.11  attribute, \isa{elim!}, indicating that this elimination rule can be applied
     6.1 --- a/doc-src/TutorialI/IsaMakefile	Thu Jan 25 11:59:52 2001 +0100
     6.2 +++ b/doc-src/TutorialI/IsaMakefile	Thu Jan 25 15:31:31 2001 +0100
     6.3 @@ -165,7 +165,7 @@
     6.4  $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
     6.5    Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
     6.6    Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
     6.7 -  Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
     6.8 +  Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
     6.9  	$(USEDIR) Misc
    6.10  	@rm -f tutorial.dvi
    6.11  
     7.1 --- a/doc-src/TutorialI/Misc/ROOT.ML	Thu Jan 25 11:59:52 2001 +0100
     7.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Thu Jan 25 15:31:31 2001 +0100
     7.3 @@ -11,3 +11,4 @@
     7.4  use_thy "simp";
     7.5  use_thy "Itrev";
     7.6  use_thy "AdvancedInd";
     7.7 +use_thy "appendix";
     8.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jan 25 11:59:52 2001 +0100
     8.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jan 25 15:31:31 2001 +0100
     8.3 @@ -43,8 +43,8 @@
     8.4    \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
     8.5    \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
     8.6    \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
     8.7 -  not just for natural numbers but at other types as well (see
     8.8 -  \S\ref{sec:overloading}). For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
     8.9 +  not just for natural numbers but at other types as well.
    8.10 +  For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
    8.11    there is nothing to indicate that you are talking about natural numbers.
    8.12    Hence Isabelle can only infer that \isa{x} is of some arbitrary type where
    8.13    \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
    8.14 @@ -54,6 +54,10 @@
    8.15    \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there is enough contextual information this
    8.16    may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies
    8.17    \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded.
    8.18 +
    8.19 +  For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
    8.20 +  Table~\ref{tab:overloading} in the appendix shows the most important overloaded
    8.21 +  operations.
    8.22  \end{warn}
    8.23  
    8.24  Simple arithmetic goals are proved automatically by both \isa{auto} and the
     9.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Thu Jan 25 11:59:52 2001 +0100
     9.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Thu Jan 25 15:31:31 2001 +0100
     9.3 @@ -41,8 +41,8 @@
     9.4    \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
     9.5    \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
     9.6    \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
     9.7 -  not just for natural numbers but at other types as well (see
     9.8 -  \S\ref{sec:overloading}). For example, given the goal @{prop"x+0 = x"},
     9.9 +  not just for natural numbers but at other types as well.
    9.10 +  For example, given the goal @{prop"x+0 = x"},
    9.11    there is nothing to indicate that you are talking about natural numbers.
    9.12    Hence Isabelle can only infer that @{term x} is of some arbitrary type where
    9.13    @{term 0} and @{text"+"} are declared. As a consequence, you will be unable
    9.14 @@ -52,6 +52,10 @@
    9.15    @{text"x+0 = (x::nat)"}. If there is enough contextual information this
    9.16    may not be necessary: @{prop"Suc x = x"} automatically implies
    9.17    @{text"x::nat"} because @{term Suc} is not overloaded.
    9.18 +
    9.19 +  For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
    9.20 +  Table~\ref{tab:overloading} in the appendix shows the most important overloaded
    9.21 +  operations.
    9.22  \end{warn}
    9.23  
    9.24  Simple arithmetic goals are proved automatically by both @{term auto} and the
    10.1 --- a/doc-src/TutorialI/Rules/rules.tex	Thu Jan 25 11:59:52 2001 +0100
    10.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Thu Jan 25 15:31:31 2001 +0100
    10.3 @@ -234,8 +234,8 @@
    10.4  Recall that the conjunction elimination rules --- whose Isabelle names are 
    10.5  \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
    10.6  of a conjunction.  Rules of this sort (where the conclusion is a subformula of a
    10.7 -premise) are called \textbf{destruction} rules, by analogy with the destructor
    10.8 -functions of functional programming.%
    10.9 +premise) are called \textbf{destruction} rules because they take apart and destroy
   10.10 +a premise.%
   10.11  \footnote{This Isabelle terminology has no counterpart in standard logic texts, 
   10.12  although the distinction between the two forms of elimination rule is well known. 
   10.13  Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules 
   10.14 @@ -365,7 +365,7 @@
   10.15  conclusion.  
   10.16  
   10.17  \medskip
   10.18 -\indexbold{by}
   10.19 +\indexbold{*by}
   10.20  The \isacommand{by} command is useful for proofs like these that use
   10.21  \isa{assumption} heavily.  It executes an
   10.22  \isacommand{apply} command, then tries to prove all remaining subgoals using
   10.23 @@ -781,7 +781,7 @@
   10.24  To see how this works, let us derive a rule about reducing 
   10.25  the scope of a universal quantifier.  In mathematical notation we write
   10.26  \[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
   10.27 -with the proviso `$x$ not free in~$P$.'  Isabelle's treatment of
   10.28 +with the proviso ``$x$ not free in~$P$.''  Isabelle's treatment of
   10.29  substitution makes the proviso unnecessary.  The conclusion is expressed as
   10.30  \isa{P\
   10.31  \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
   10.32 @@ -860,7 +860,7 @@
   10.33  \isacommand{apply}\ (rename_tac\ v\ w)\isanewline
   10.34  \ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
   10.35  \end{isabelle}
   10.36 -Recall that \isa{rule_tac}\index{rule_tac|and renaming} instantiates a
   10.37 +Recall that \isa{rule_tac}\index{*rule_tac!and renaming} instantiates a
   10.38  theorem with specified terms.  These terms may involve the goal's bound
   10.39  variables, but beware of referring to  variables
   10.40  like~\isa{xa}.  A future change to your theories could change the set of names
   10.41 @@ -1686,7 +1686,7 @@
   10.42  
   10.43  The next step is to put
   10.44  the theorem \isa{gcd_mult_0} into a simplified form, performing the steps 
   10.45 -$\gcd(1,n)=1$ and $k\times1=k$.  The \isa{simplified}\indexbold{simplified}
   10.46 +$\gcd(1,n)=1$ and $k\times1=k$.  The \isaindexbold{simplified}
   10.47  attribute takes a theorem
   10.48  and returns the result of simplifying it, with respect to the default
   10.49  simplification rules:
   10.50 @@ -1769,7 +1769,7 @@
   10.51  \end{isabelle}
   10.52  
   10.53  \medskip
   10.54 -The \isa{rule_format}\indexbold{rule_format} directive replaces a common usage
   10.55 +The \isaindexbold{rule_format} directive replaces a common usage
   10.56  of \isa{THEN}\@.  It is needed in proofs by induction when the induction formula must be
   10.57  expressed using
   10.58  \isa{\isasymlongrightarrow} and \isa{\isasymforall}.  For example, in 
    11.1 --- a/doc-src/TutorialI/Sets/sets.tex	Thu Jan 25 11:59:52 2001 +0100
    11.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Thu Jan 25 15:31:31 2001 +0100
    11.3 @@ -871,7 +871,7 @@
    11.4  Many familiar induction principles are instances of this rule. 
    11.5  For example, the predecessor relation on the natural numbers 
    11.6  is well-founded; induction over it is mathematical induction. 
    11.7 -The `tail of' relation on lists is well-founded; induction over 
    11.8 +The ``tail of'' relation on lists is well-founded; induction over 
    11.9  it is structural induction. 
   11.10  
   11.11  Well-foundedness can be difficult to show. The various 
    12.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Thu Jan 25 11:59:52 2001 +0100
    12.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Jan 25 15:31:31 2001 +0100
    12.3 @@ -177,7 +177,7 @@
    12.4  
    12.5  txt{*\noindent\index{*induct_tac}%
    12.6  This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
    12.7 -@{term"tac"} stands for ``tactic'', a synonym for ``theorem proving function''.
    12.8 +@{term"tac"} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
    12.9  By default, induction acts on the first subgoal. The new proof state contains
   12.10  two subgoals, namely the base case (@{term[source]Nil}) and the induction step
   12.11  (@{term[source]Cons}):
   12.12 @@ -207,7 +207,7 @@
   12.13  txt{*\noindent
   12.14  This command tells Isabelle to apply a proof strategy called
   12.15  @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
   12.16 -``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
   12.17 +simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks
   12.18  to the equation @{prop"rev [] = []"}) and disappears; the simplified version
   12.19  of subgoal~2 becomes the new subgoal~1:
   12.20  @{subgoals[display,indent=0,margin=70]}
    13.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jan 25 11:59:52 2001 +0100
    13.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jan 25 15:31:31 2001 +0100
    13.3 @@ -172,7 +172,7 @@
    13.4  \begin{isamarkuptxt}%
    13.5  \noindent\index{*induct_tac}%
    13.6  This tells Isabelle to perform induction on variable \isa{xs}. The suffix
    13.7 -\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
    13.8 +\isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
    13.9  By default, induction acts on the first subgoal. The new proof state contains
   13.10  two subgoals, namely the base case (\isa{Nil}) and the induction step
   13.11  (\isa{Cons}):
   13.12 @@ -204,7 +204,7 @@
   13.13  \noindent
   13.14  This command tells Isabelle to apply a proof strategy called
   13.15  \isa{auto} to all subgoals. Essentially, \isa{auto} tries to
   13.16 -``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
   13.17 +simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks
   13.18  to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
   13.19  of subgoal~2 becomes the new subgoal~1:
   13.20  \begin{isabelle}%
    14.1 --- a/doc-src/TutorialI/Trie/Trie.thy	Thu Jan 25 11:59:52 2001 +0100
    14.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Thu Jan 25 15:31:31 2001 +0100
    14.3 @@ -132,7 +132,7 @@
    14.4  proof states are invisible, and we rely on the (possibly brittle) magic of
    14.5  @{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
    14.6  of the induction up in such a way that case distinction on @{term bs} makes
    14.7 -sense and solves the proof. Part~\ref{Isar} shows you how to write readable
    14.8 +sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
    14.9  and stable proofs.
   14.10  *};
   14.11  
    15.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Thu Jan 25 11:59:52 2001 +0100
    15.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Thu Jan 25 15:31:31 2001 +0100
    15.3 @@ -122,7 +122,7 @@
    15.4  proof states are invisible, and we rely on the (possibly brittle) magic of
    15.5  \isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
    15.6  of the induction up in such a way that case distinction on \isa{bs} makes
    15.7 -sense and solves the proof. Part~\ref{Isar} shows you how to write readable
    15.8 +sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
    15.9  and stable proofs.%
   15.10  \end{isamarkuptext}%
   15.11  \end{isabellebody}%
    16.1 --- a/doc-src/TutorialI/Types/Overloading2.thy	Thu Jan 25 11:59:52 2001 +0100
    16.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Thu Jan 25 15:31:31 2001 +0100
    16.3 @@ -22,38 +22,10 @@
    16.4  
    16.5  text{*
    16.6  HOL comes with a number of overloaded constants and corresponding classes.
    16.7 -The most important ones are listed in Table~\ref{tab:overloading}. They are
    16.8 +The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
    16.9  defined on all numeric types and sometimes on other types as well, for example
   16.10  @{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
   16.11  
   16.12 -\begin{table}[htbp]
   16.13 -\begin{center}
   16.14 -\begin{tabular}{lll}
   16.15 -Constant & Type & Syntax \\
   16.16 -\hline
   16.17 -@{term 0} & @{text "'a::zero"} \\
   16.18 -@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
   16.19 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} &  (infixl 65) \\
   16.20 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
   16.21 -@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   16.22 -@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   16.23 -@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   16.24 -@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
   16.25 -@{text"/"}  & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   16.26 -@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
   16.27 -@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
   16.28 -@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
   16.29 -@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
   16.30 -@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
   16.31 -@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
   16.32 -@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
   16.33 -@{text LEAST}$~x.~P$
   16.34 -\end{tabular}
   16.35 -\caption{Overloaded Constants in HOL}
   16.36 -\label{tab:overloading}
   16.37 -\end{center}
   16.38 -\end{table}
   16.39 -
   16.40  In addition there is a special input syntax for bounded quantifiers:
   16.41  \begin{center}
   16.42  \begin{tabular}{lcl}
    17.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Thu Jan 25 11:59:52 2001 +0100
    17.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Thu Jan 25 15:31:31 2001 +0100
    17.3 @@ -24,38 +24,10 @@
    17.4  %
    17.5  \begin{isamarkuptext}%
    17.6  HOL comes with a number of overloaded constants and corresponding classes.
    17.7 -The most important ones are listed in Table~\ref{tab:overloading}. They are
    17.8 +The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
    17.9  defined on all numeric types and sometimes on other types as well, for example
   17.10  \isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
   17.11  
   17.12 -\begin{table}[htbp]
   17.13 -\begin{center}
   17.14 -\begin{tabular}{lll}
   17.15 -Constant & Type & Syntax \\
   17.16 -\hline
   17.17 -\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
   17.18 -\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
   17.19 -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\
   17.20 -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
   17.21 -\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   17.22 -\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   17.23 -\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   17.24 -\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
   17.25 -\isa{{\isacharslash}}  & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   17.26 -\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
   17.27 -\isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
   17.28 -\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
   17.29 -\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
   17.30 -\isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
   17.31 -\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
   17.32 -\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
   17.33 -\isa{LEAST}$~x.~P$
   17.34 -\end{tabular}
   17.35 -\caption{Overloaded Constants in HOL}
   17.36 -\label{tab:overloading}
   17.37 -\end{center}
   17.38 -\end{table}
   17.39 -
   17.40  In addition there is a special input syntax for bounded quantifiers:
   17.41  \begin{center}
   17.42  \begin{tabular}{lcl}
    18.1 --- a/doc-src/TutorialI/Types/numerics.tex	Thu Jan 25 11:59:52 2001 +0100
    18.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Thu Jan 25 15:31:31 2001 +0100
    18.3 @@ -6,7 +6,10 @@
    18.4  \isa{int} of \textbf{integers}, which lack induction but support true
    18.5  subtraction. The logic HOL-Real also has the type \isa{real} of real
    18.6  numbers.  Isabelle has no subtyping,  so the numeric types are distinct and
    18.7 -there are  functions to convert between them. 
    18.8 +there are  functions to convert between them. Fortunately most numeric
    18.9 +operations are overloaded: the same symbol can be used at all numeric types.
   18.10 +Table~\ref{tab:overloading} in the appendix shows the most important operations,
   18.11 +together with the priorities of the infix symbols.
   18.12  
   18.13  The integers are preferable to the natural  numbers for reasoning about
   18.14  complicated arithmetic expressions. For  example, a termination proof
    19.1 --- a/doc-src/TutorialI/appendix.tex	Thu Jan 25 11:59:52 2001 +0100
    19.2 +++ b/doc-src/TutorialI/appendix.tex	Thu Jan 25 15:31:31 2001 +0100
    19.3 @@ -3,7 +3,7 @@
    19.4  \chapter{Appendix}
    19.5  \label{sec:Appendix}
    19.6  
    19.7 -\begin{figure}[htbp]
    19.8 +\begin{table}[htbp]
    19.9  \begin{center}
   19.10  \begin{tabular}{|l|l|l|}
   19.11  \hline
   19.12 @@ -98,11 +98,13 @@
   19.13  \hline
   19.14  \end{tabular}
   19.15  \end{center}
   19.16 -\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
   19.17 -\label{fig:ascii}
   19.18 -\end{figure}\indexbold{ASCII symbols}
   19.19 +\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
   19.20 +\label{tab:ascii}
   19.21 +\end{table}\indexbold{ASCII symbols}
   19.22  
   19.23 -\begin{figure}[htbp]
   19.24 +\input{Misc/document/appendix.tex}
   19.25 +
   19.26 +\begin{table}[htbp]
   19.27  \begin{center}
   19.28  \begin{tabular}{|lllllllll|}
   19.29  \hline
   19.30 @@ -143,11 +145,11 @@
   19.31  \end{tabular}
   19.32  \end{center}
   19.33  \caption{Reserved words in HOL terms}
   19.34 -\label{fig:ReservedWords}
   19.35 -\end{figure}
   19.36 +\label{tab:ReservedWords}
   19.37 +\end{table}
   19.38  
   19.39  
   19.40 -%\begin{figure}[htbp]
   19.41 +%\begin{table}[htbp]
   19.42  %\begin{center}
   19.43  %\begin{tabular}{|lllll|}
   19.44  %\hline
   19.45 @@ -175,5 +177,5 @@
   19.46  %\end{tabular}
   19.47  %\end{center}
   19.48  %\caption{Minor keywords in HOL theories}
   19.49 -%\label{fig:keywords}
   19.50 -%\end{figure}
   19.51 +%\label{tab:keywords}
   19.52 +%\end{table}
    20.1 --- a/doc-src/TutorialI/basics.tex	Thu Jan 25 11:59:52 2001 +0100
    20.2 +++ b/doc-src/TutorialI/basics.tex	Thu Jan 25 15:31:31 2001 +0100
    20.3 @@ -62,7 +62,7 @@
    20.4  
    20.5  HOL's theory collection is available online at
    20.6  \begin{center}\small
    20.7 -    \url{http://isabelle.in.tum.de/library/}
    20.8 +    \url{http://isabelle.in.tum.de/library/HOL/}
    20.9  \end{center}
   20.10  and is recommended browsing. Note that most of the theories 
   20.11  are based on classical Isabelle without the Isar extension. This means that
   20.12 @@ -233,7 +233,7 @@
   20.13  \end{itemize}
   20.14  
   20.15  For the sake of readability the usual mathematical symbols are used throughout
   20.16 -the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
   20.17 +the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
   20.18  the appendix.
   20.19  
   20.20  
   20.21 @@ -279,7 +279,7 @@
   20.22  
   20.23  Some interfaces (including the shell level) offer special fonts with
   20.24  mathematical symbols. For those that do not, remember that ASCII-equivalents
   20.25 -are shown in figure~\ref{fig:ascii} in the appendix.
   20.26 +are shown in table~\ref{tab:ascii} in the appendix.
   20.27  
   20.28  Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
   20.29  Commands may but need not be terminated by semicolons.
    21.1 --- a/doc-src/TutorialI/fp.tex	Thu Jan 25 11:59:52 2001 +0100
    21.2 +++ b/doc-src/TutorialI/fp.tex	Thu Jan 25 15:31:31 2001 +0100
    21.3 @@ -129,10 +129,10 @@
    21.4    \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
    21.5    modified parent is reloaded automatically.
    21.6    
    21.7 -  The only time when you need to load a theory by hand is when you simply
    21.8 -  want to check if it loads successfully without wanting to make use of the
    21.9 -  theory itself. This you can do by typing
   21.10 -  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
   21.11 +%  The only time when you need to load a theory by hand is when you simply
   21.12 +%  want to check if it loads successfully without wanting to make use of the
   21.13 +%  theory itself. This you can do by typing
   21.14 +%  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
   21.15  \end{description}
   21.16  Further commands are found in the Isabelle/Isar Reference Manual.
   21.17  
   21.18 @@ -302,7 +302,7 @@
   21.19  section as well, in particular in order to understand what happened if things
   21.20  do not simplify as expected.
   21.21  
   21.22 -\subsubsection{What is Simplification?}
   21.23 +\subsubsection{What is Simplification}
   21.24  
   21.25  In its most basic form, simplification means repeated application of
   21.26  equations from left to right. For example, taking the rules for \isa{\at}
    22.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Jan 25 11:59:52 2001 +0100
    22.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Jan 25 15:31:31 2001 +0100
    22.3 @@ -91,6 +91,7 @@
    22.4  \chapter{Theory Presentation}
    22.5  \chapter{Case Study: Verifying a Cryptographic Protocol}
    22.6  \chapter{Structured Proofs}
    22.7 +\label{ch:Isar}
    22.8  %\chapter{Case Study: UNIX File-System Security}
    22.9  %\chapter{The Tricks of the Trade}
   22.10  \input{appendix}