# HG changeset patch # User nipkow # Date 1101995227 -3600 # Node ID 0c3891c3528f7030c6e01f68e690747ef42f5c9f # Parent 885a40edcdba6cff884c403a9f53215541ba0d77 *** empty log message *** diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Dec 02 14:47:07 2004 +0100 @@ -34,20 +34,20 @@ \newcommand{\mystar}{*% } \index{arithmetic operations!for \protect\isa{nat}}% -The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun}, -\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun}, +The arithmetic operations \isadxboldpos{+}{$HOL2arithfun}, +\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun}, \sdx{div}, \sdx{mod}, \cdx{min} and \cdx{max} are predefined, as are the relations -\indexboldpos{\isasymle}{$HOL2arithrel} and -\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if +\isadxboldpos{\isasymle}{$HOL2arithrel} and +\isadxboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if \isa{m\ {\isacharless}\ n}. There is even a least number operation \sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}. \begin{warn}\index{overloading} The constants \cdx{0} and \cdx{1} and the operations - \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, - \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min}, - \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and - \ttindexboldpos{<}{$HOL2arithrel} are overloaded: they are available + \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun}, + \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min}, + \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and + \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available not just for natural numbers but for other types as well. For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate that you are talking about natural numbers. Hence Isabelle can only infer @@ -65,6 +65,12 @@ overloaded operations. \end{warn} \begin{warn} + The symbols \isadxboldpos{>}{$HOL2arithrel} and + \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \isa{x\ {\isachargreater}\ y} + stands for \isa{y\ {\isacharless}\ x} and similary for \isa{{\isasymge}} and + \isa{{\isasymle}}. +\end{warn} +\begin{warn} Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to equal \isa{Suc\ {\isadigit{0}}}. This definition (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/Misc/natsum.thy --- a/doc-src/TutorialI/Misc/natsum.thy Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/Misc/natsum.thy Thu Dec 02 14:47:07 2004 +0100 @@ -23,20 +23,20 @@ text{*\newcommand{\mystar}{*% } \index{arithmetic operations!for \protect\isa{nat}}% -The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun}, -\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun}, +The arithmetic operations \isadxboldpos{+}{$HOL2arithfun}, +\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun}, \sdx{div}, \sdx{mod}, \cdx{min} and \cdx{max} are predefined, as are the relations -\indexboldpos{\isasymle}{$HOL2arithrel} and -\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if +\isadxboldpos{\isasymle}{$HOL2arithrel} and +\isadxboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if @{prop"m}{$HOL2arithrel} and + \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: @{text"x > y"} + stands for @{prop"y < x"} and similary for @{text"\"} and + @{text"\"}. +\end{warn} +\begin{warn} Constant @{text"1::nat"} is defined to equal @{term"Suc 0"}. This definition (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some tactics (like @{text auto}, @{text simp} and @{text arith}) but not by diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Dec 02 14:47:07 2004 +0100 @@ -634,7 +634,7 @@ as $\exists x.\,P$, they let us proceed with a proof. They can be filled in later, sometimes in stages and often automatically. -If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{* trace_unify_fail (flag)}, +If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{*trace_unify_fail (flag)}, which makes Isabelle show the cause of unification failures. For example, suppose we are trying to prove this subgoal by assumption: \begin{isabelle} \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a) diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Dec 02 14:47:07 2004 +0100 @@ -24,8 +24,8 @@ @{term"False"}. Because this notation quickly becomes unwieldy, the datatype declaration is annotated with an alternative syntax: instead of @{term[source]Nil} and \isa{Cons x xs} we can write -@{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and -@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this +@{term"[]"}\index{$HOL2list@\isa{[]}|bold} and +@{term"x # xs"}\index{$HOL2list@\isa{\#}|bold}. In fact, this alternative syntax is the familiar one. Thus the list \isa{Cons True (Cons False Nil)} becomes @{term"True # False # []"}. The annotation \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} @@ -56,7 +56,7 @@ restriction, the order of items in a theory file is unconstrained. Function @{text"app"} is annotated with concrete syntax too. Instead of the prefix syntax @{text"app xs ys"} the infix -@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred +@{term"xs @ ys"}\index{$HOL2list@\isa{\at}|bold} becomes the preferred form. Both functions are defined recursively: *} diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Dec 02 14:47:07 2004 +0100 @@ -29,8 +29,8 @@ \isa{False}. Because this notation quickly becomes unwieldy, the datatype declaration is annotated with an alternative syntax: instead of \isa{Nil} and \isa{Cons x xs} we can write -\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and -\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this +\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\isa{[]}|bold} and +\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this alternative syntax is the familiar one. Thus the list \isa{Cons True (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} @@ -61,7 +61,7 @@ restriction, the order of items in a theory file is unconstrained. Function \isa{app} is annotated with concrete syntax too. Instead of the prefix syntax \isa{app\ xs\ ys} the infix -\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred +\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred form. Both functions are defined recursively:% \end{isamarkuptext}% \isamarkuptrue% diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Dec 02 14:47:07 2004 +0100 @@ -300,7 +300,7 @@ FIELDS \begin{isabelle}% -a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b% +a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachargreater}a{\isachardot}\ r\ {\isacharless}\ b% \end{isabelle} \rulename{dense} diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/appendix.tex --- a/doc-src/TutorialI/appendix.tex Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/appendix.tex Thu Dec 02 14:47:07 2004 +0100 @@ -62,7 +62,7 @@ \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} & \verb$\!$\\ \indexboldpos{\isasymepsilon}{$HOL0ExSome} & -\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} & +\ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} & \verb$\$\\ \indexboldpos{\isasymcirc}{$HOL1} & \ttindexbold{o} & @@ -71,7 +71,7 @@ \ttindexbold{abs}& \verb$\ \$\\ \indexboldpos{\isasymle}{$HOL2arithrel}& -\ttindexboldpos{<=}{$HOL2arithrel}& +\isadxboldpos{<=}{$HOL2arithrel}& \verb$\$\\ \indexboldpos{\isasymtimes}{$Isatype}& \ttindexboldpos{*}{$HOL2arithfun} & diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/tutorial.sty --- a/doc-src/TutorialI/tutorial.sty Thu Dec 02 12:28:09 2004 +0100 +++ b/doc-src/TutorialI/tutorial.sty Thu Dec 02 14:47:07 2004 +0100 @@ -28,6 +28,7 @@ %%%% for indexing constants, symbols, theorems, ... \newcommand\cdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (constant)}} \newcommand\sdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (symbol)}} +\newcommand\sdxpos[2]{\isa{#1}\index{#2@\protect\isa{#1} (symbol)}} \newcommand\tdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)}} \newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}} @@ -51,6 +52,9 @@ \newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@} \newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@} +\newcommand{\isadxpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}}\@} +\newcommand{\isadxboldpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}|bold}\@} + %Commented-out the original versions to see what the index looks like without them. % In any event, they need to use \isa or \protect\isa rather than \texttt. %%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}