Two new examples; corrected a comment
authorpaulson
Fri Jun 06 10:19:20 1997 +0200 (1997-06-06)
changeset 3418f060dc3f15a8
parent 3417 58ccb80eb50a
child 3419 9092b79d86d5
Two new examples; corrected a comment
src/HOL/ex/Recdef.thy
     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"