6 Examples of recdef definitions. Most, but not all, are handled automatically. |
6 Examples of recdef definitions. Most, but not all, are handled automatically. |
7 *) |
7 *) |
8 |
8 |
9 Recdef = WF_Rel + List + |
9 Recdef = WF_Rel + List + |
10 |
10 |
|
11 consts fact :: "nat => nat" |
|
12 recdef fact "less_than" |
|
13 "fact x = (if (x = 0) then 1 else x * fact (x - 1))" |
|
14 |
|
15 consts Fact :: "nat => nat" |
|
16 recdef Fact "less_than" |
|
17 "Fact 0 = 1" |
|
18 "Fact (Suc x) = (Fact x * Suc x)" |
|
19 |
11 consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list" |
20 consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list" |
12 |
|
13 recdef map2 "measure(%(f,l1,l2).size l1)" |
21 recdef map2 "measure(%(f,l1,l2).size l1)" |
14 "map2(f, [], []) = []" |
22 "map2(f, [], []) = []" |
15 "map2(f, h#t, []) = []" |
23 "map2(f, h#t, []) = []" |
16 "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)" |
24 "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)" |
17 |
25 |
40 "gcd (0,y) = y" |
48 "gcd (0,y) = y" |
41 "gcd (Suc x, 0) = Suc x" |
49 "gcd (Suc x, 0) = Suc x" |
42 "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y) |
50 "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y) |
43 else gcd(Suc x, y - x))" |
51 else gcd(Suc x, y - x))" |
44 |
52 |
45 (*Not handled automatically. In fact, g is the identity function.*) |
53 (*Not handled automatically. In fact, g is the zero constant function.*) |
46 consts g :: "nat => nat" |
54 consts g :: "nat => nat" |
47 recdef g "less_than" |
55 recdef g "less_than" |
48 "g 0 = 0" |
56 "g 0 = 0" |
49 "g(Suc x) = g(g x)" |
57 "g(Suc x) = g(g x)" |
50 |
58 |