auto update
authorpaulson
Wed Jul 13 15:19:13 2005 +0200 (2005-07-13)
changeset 167976109d4020420
parent 16796 140f1e0ea846
child 16798 36d34186741b
auto update
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/isabellesym.sty
     1.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jul 13 15:06:20 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jul 13 15:19:13 2005 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4  \begin{isamarkuptext}%
     1.5  \noindent
     1.6  For efficiency's sake, this built-in prover ignores quantified formulae,
     1.7 -logical connectives, and all arithmetic operations apart from addition.
     1.8 +many logical connectives, and all arithmetic operations apart from addition.
     1.9  In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
    1.10  \end{isamarkuptext}%
    1.11  \isamarkuptrue%
    1.12 @@ -135,7 +135,7 @@
    1.13  \isa{k}~\sdx{dvd} are also supported, where the former two are eliminated
    1.14  by case distinctions, again blowing up the running time.
    1.15  
    1.16 -If the formula involves explicit quantifiers, \isa{arith} may take
    1.17 +If the formula involves quantifiers, \isa{arith} may take
    1.18  super-exponential time and space.
    1.19  \end{warn}%
    1.20  \end{isamarkuptext}%
     2.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Jul 13 15:06:20 2005 +0200
     2.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Jul 13 15:19:13 2005 +0200
     2.3 @@ -35,17 +35,17 @@
     2.4  condition simplifies to \isa{True} or \isa{False}.  For
     2.5  example, simplification reduces
     2.6  \begin{isabelle}%
     2.7 -\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
     2.8 +\ \ \ \ \ simplification{\isachardot}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
     2.9  \end{isabelle}
    2.10  in one step to
    2.11  \begin{isabelle}%
    2.12 -\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
    2.13 +\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
    2.14  \end{isabelle}
    2.15  where the condition cannot be reduced further, and splitting leads to
    2.16  \begin{isabelle}%
    2.17 -\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
    2.18 +\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
    2.19  \end{isabelle}
    2.20 -Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
    2.21 +Since the recursive call \isa{simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
    2.22  an \isa{if}, it is unfolded again, which leads to an infinite chain of
    2.23  simplification steps. Fortunately, this problem can be avoided in many
    2.24  different ways.
    2.25 @@ -57,7 +57,7 @@
    2.26  \isa{if} is involved.
    2.27  
    2.28  If possible, the definition should be given by pattern matching on the left
    2.29 -rather than \isa{if} on the right. In the case of \isa{gcd} the
    2.30 +rather than \isa{if} on the right. In the case of \isa{simplification{\isachardot}gcd} the
    2.31  following alternative definition suggests itself:%
    2.32  \end{isamarkuptext}%
    2.33  \isamarkuptrue%
    2.34 @@ -88,7 +88,7 @@
    2.35  always available.
    2.36  
    2.37  A final alternative is to replace the offending simplification rules by
    2.38 -derived conditional ones. For \isa{gcd} it means we have to prove
    2.39 +derived conditional ones. For \isa{simplification{\isachardot}gcd} it means we have to prove
    2.40  these lemmas:%
    2.41  \end{isamarkuptext}%
    2.42  \isamarkuptrue%
     3.1 --- a/doc-src/TutorialI/isabellesym.sty	Wed Jul 13 15:06:20 2005 +0200
     3.2 +++ b/doc-src/TutorialI/isabellesym.sty	Wed Jul 13 15:19:13 2005 +0200
     3.3 @@ -359,3 +359,4 @@
     3.4  \newcommand{\isasymcedilla}{\isatext{\c\relax}}
     3.5  \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
     3.6  \newcommand{\isasymspacespace}{\isamath{~~}}
     3.7 +\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}