6481

1 
(* Title: HOL/ex/Recdefs.thy

5124

2 
ID: $Id$


3 
Author: Konrad Slind and Lawrence C Paulson


4 
Copyright 1996 University of Cambridge


5 


6 
Examples of recdef definitions. Most, but not all, are handled automatically.


7 
*)


8 

6455

9 
Recdefs = Main +

5124

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 


20 
consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"


21 
recdef map2 "measure(%(f,l1,l2).size l1)"


22 
"map2(f, [], []) = []"


23 
"map2(f, h#t, []) = []"


24 
"map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"


25 


26 
consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"


27 
recdef finiteRchain "measure (%(R,l).size l)"


28 
"finiteRchain(R, []) = True"


29 
"finiteRchain(R, [x]) = True"


30 
"finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))"


31 


32 
(*Not handled automatically: too complicated.*)


33 
consts variant :: "nat * nat list => nat"


34 
recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))"


35 
"variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"


36 


37 
consts gcd :: "nat * nat => nat"


38 
recdef gcd "measure (%(x,y).x+y)"


39 
"gcd (0,y) = y"


40 
"gcd (Suc x, 0) = Suc x"


41 
"gcd (Suc x, Suc y) = (if (y <= x) then gcd(x  y, Suc y)


42 
else gcd(Suc x, y  x))"


43 


44 
(*Not handled automatically. In fact, g is the zero constant function.*)


45 
consts g :: "nat => nat"


46 
recdef g "less_than"


47 
"g 0 = 0"


48 
"g(Suc x) = g(g x)"


49 


50 
consts Div :: "nat * nat => nat * nat"


51 
recdef Div "measure fst"


52 
"Div(0,x) = (0,0)"


53 
"Div(Suc x, y) =


54 
(let (q,r) = Div(x,y)


55 
in


56 
if (y <= Suc r) then (Suc q,0) else (q, Suc r))"


57 


58 
(*Not handled automatically. Should be the predecessor function, but there


59 
is an unnecessary "looping" recursive call in k(1) *)


60 
consts k :: "nat => nat"


61 
recdef k "less_than"


62 
"k 0 = 0"


63 
"k (Suc n) = (let x = k 1


64 
in if (0=1) then k (Suc 1) else n)"


65 


66 
consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"


67 
recdef part "measure (%(P,l,l1,l2).size l)"


68 
"part(P, [], l1,l2) = (l1,l2)"


69 
"part(P, h#rst, l1,l2) =


70 
(if P h then part(P,rst, h#l1, l2)


71 
else part(P,rst, l1, h#l2))"


72 


73 
consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"


74 
recdef fqsort "measure (size o snd)"


75 
"fqsort(ord,[]) = []"


76 
"fqsort(ord, x#rst) =


77 
(let (less,more) = part((%y. ord y x), rst, ([],[]))


78 
in


79 
fqsort(ord,less)@[x]@fqsort(ord,more))"


80 


81 
(* silly example which demonstrates the occasional need for additional


82 
congruence rules (here: map_cong from List). If the congruence rule is


83 
removed, an unprovable termination condition is generated!


84 
Termination not proved automatically; see the ML file.


85 
TFL requires (%x.mapf x) instead of mapf.


86 
*)


87 
consts mapf :: nat => nat list


88 
recdef mapf "measure(%m. m)"

6481

89 
congs map_cong

5124

90 
"mapf 0 = []"


91 
"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"


92 


93 
end
