author paulson Fri Jun 06 10:19:20 1997 +0200 (1997-06-06) changeset 3418 f060dc3f15a8 parent 3417 58ccb80eb50a child 3419 9092b79d86d5
Two new examples; corrected a comment
 src/HOL/ex/Recdef.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/ex/Recdef.thy	Fri Jun 06 10:18:46 1997 +0200
1.2 +++ b/src/HOL/ex/Recdef.thy	Fri Jun 06 10:19:20 1997 +0200
1.3 @@ -8,8 +8,16 @@
1.4
1.5  Recdef = WF_Rel + List +
1.6
1.7 +consts fact :: "nat => nat"
1.8 +recdef fact "less_than"
1.9 +    "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
1.10 +
1.11 +consts Fact :: "nat => nat"
1.12 +recdef Fact "less_than"
1.13 +    "Fact 0 = 1"
1.14 +    "Fact (Suc x) = (Fact x * Suc x)"
1.15 +
1.16  consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
1.17 -
1.18  recdef map2 "measure(%(f,l1,l2).size l1)"
1.19      "map2(f, [], [])  = []"
1.20      "map2(f, h#t, []) = []"
1.21 @@ -42,7 +50,7 @@
1.22      "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)
1.23                                         else gcd(Suc x, y - x))"
1.24
1.25 -(*Not handled automatically.  In fact, g is the identity function.*)
1.26 +(*Not handled automatically.  In fact, g is the zero constant function.*)
1.27  consts g   :: "nat => nat"
1.28  recdef g "less_than"
1.29      "g 0 = 0"
```