doc-src/TutorialI/Recdef/examples.thy
 changeset 9933 9feb1e0c4cb3 parent 9792 bbefb6ce5cb2 child 10362 c6b197ccf1f1
     1.1 --- a/doc-src/TutorialI/Recdef/examples.thy	Tue Sep 12 14:59:44 2000 +0200
1.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Sep 12 15:43:15 2000 +0200
1.3 @@ -6,8 +6,8 @@
1.4  Here is a simple example, the Fibonacci function:
1.5  *}
1.6
1.7 -consts fib :: "nat \\<Rightarrow> nat";
1.8 -recdef fib "measure(\\<lambda>n. n)"
1.9 +consts fib :: "nat \<Rightarrow> nat";
1.10 +recdef fib "measure(\<lambda>n. n)"
1.11    "fib 0 = 0"
1.12    "fib 1 = 1"
1.13    "fib (Suc(Suc x)) = fib x + fib (Suc x)";
1.14 @@ -26,8 +26,8 @@
1.15  between any two elements of a list:
1.16  *}
1.17
1.18 -consts sep :: "'a * 'a list \\<Rightarrow> 'a list";
1.19 -recdef sep "measure (\\<lambda>(a,xs). length xs)"
1.20 +consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
1.21 +recdef sep "measure (\<lambda>(a,xs). length xs)"
1.22    "sep(a, [])     = []"
1.23    "sep(a, [x])    = [x]"
1.24    "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
1.25 @@ -39,8 +39,8 @@
1.26  Pattern matching need not be exhaustive:
1.27  *}
1.28
1.29 -consts last :: "'a list \\<Rightarrow> 'a";
1.30 -recdef last "measure (\\<lambda>xs. length xs)"
1.31 +consts last :: "'a list \<Rightarrow> 'a";
1.32 +recdef last "measure (\<lambda>xs. length xs)"
1.33    "last [x]      = x"
1.34    "last (x#y#zs) = last (y#zs)";
1.35
1.36 @@ -49,8 +49,8 @@
1.37  account, just as in functional programming:
1.38  *}
1.39
1.40 -consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";
1.41 -recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
1.42 +consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
1.43 +recdef sep1 "measure (\<lambda>(a,xs). length xs)"
1.44    "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
1.45    "sep1(a, xs)     = xs";
1.46
1.47 @@ -67,17 +67,17 @@
1.48    arguments as in the following definition:
1.49  \end{warn}
1.50  *}
1.51 -consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";
1.52 +consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
1.53  recdef sep2 "measure length"
1.54 -  "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"
1.55 -  "sep2 xs       = (\\<lambda>a. xs)";
1.56 +  "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)"
1.57 +  "sep2 xs       = (\<lambda>a. xs)";
1.58
1.59  text{*
1.60  Because of its pattern-matching syntax, \isacommand{recdef} is also useful
1.61  for the definition of non-recursive functions:
1.62  *}
1.63
1.64 -consts swap12 :: "'a list \\<Rightarrow> 'a list";
1.65 +consts swap12 :: "'a list \<Rightarrow> 'a list";
1.66  recdef swap12 "{}"
1.67    "swap12 (x#y#zs) = y#x#zs"
1.68    "swap12 zs       = zs";