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";