author krauss Mon, 13 Nov 2006 21:52:14 +0100 changeset 21346 c8aa120fa05d parent 21345 a18e60f597b6 child 21347 fccc48e844f5
updated
--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Mon Nov 13 20:10:02 2006 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Mon Nov 13 21:52:14 2006 +0100
@@ -24,8 +24,6 @@
| "fib (Suc 0) = 1"
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"

-(*<*)termination by lexicographic_order(*>*)
-
text {*
The function always terminates, since the argument of gets smaller in every
recursive call. Termination is an
@@ -55,7 +53,6 @@
where
"sep a (x#y#xs) = x # a # sep a (y # xs)"
| "sep a xs       = xs"
-(*<*)termination by lexicographic_order(*>*)

text {*
Overlapping patterns are interpreted as "increments" to what is
@@ -165,11 +162,11 @@
@{text "N + 1 - i"} decreases in every recursive call.

We can use this expression as a measure function to construct a
-  wellfounded relation, which is a proof of termination:
+  wellfounded relation, which can prove termination.
*}

termination
-  by (auto_term "measure (\<lambda>(i,N). N + 1 - i)")
+  by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto

text {*
Note that the two (curried) function arguments appear as a pair in
@@ -199,7 +196,7 @@
*}

termination
-  by (auto_term "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]")
+  by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto

section {* Mutual Recursion *}
@@ -208,7 +205,6 @@
If two or more functions call one another mutually, they have to be defined
in one step. The simplest example are probably @{text "even"} and @{text "odd"}:
*}
-(*<*)hide const even odd(*>*)

function even odd :: "nat \<Rightarrow> bool"
where
@@ -228,7 +224,7 @@
*}

termination
-  by (auto_term "measure (sum_case (%n. n) (%n. n))")
+  by (relation "measure (sum_case (%n. n) (%n. n))") auto


--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 13 20:10:02 2006 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 13 21:52:14 2006 +0100
@@ -42,21 +42,7 @@
\isakeyword{where}\isanewline
-{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-%
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-%
-%
+{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The function always terminates, since the argument of gets smaller in every
recursive call. Termination is an
@@ -90,19 +76,6 @@
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}sep\ a\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
-%
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-%
-%
\begin{isamarkuptext}%
Overlapping patterns are interpreted as "increments" to what is
already there: The second equation is only meant for the cases where
@@ -281,7 +254,7 @@
\isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} decreases in every recursive call.

We can use this expression as a measure function to construct a
-  wellfounded relation, which is a proof of termination:%
+  wellfounded relation, which can prove termination.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
@@ -293,7 +266,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
@@ -351,7 +324,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measures\ {\isacharbrackleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N{\isacharcomma}\ {\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measures\ {\isacharbrackleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N{\isacharcomma}\ {\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
@@ -368,7 +341,6 @@
in one step. The simplest example are probably \isa{even} and \isa{odd}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isacommand{function}\isamarkupfalse%
\ even\ odd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
@@ -409,7 +381,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}sum{\isacharunderscore}case\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}sum{\isacharunderscore}case\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%