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 |
|
11024
|
9 |
header {* Examples of recdef definitions *}
|
|
10 |
|
|
11 |
theory Recdefs = Main:
|
5124
|
12 |
|
|
13 |
consts fact :: "nat => nat"
|
11024
|
14 |
recdef fact less_than
|
|
15 |
"fact x = (if x = 0 then 1 else x * fact (x - 1))"
|
5124
|
16 |
|
|
17 |
consts Fact :: "nat => nat"
|
11024
|
18 |
recdef Fact less_than
|
|
19 |
"Fact 0 = 1"
|
|
20 |
"Fact (Suc x) = Fact x * Suc x"
|
5124
|
21 |
|
|
22 |
consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
|
11024
|
23 |
recdef map2 "measure(\<lambda>(f, l1, l2). size l1)"
|
|
24 |
"map2 (f, [], []) = []"
|
|
25 |
"map2 (f, h # t, []) = []"
|
|
26 |
"map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)"
|
5124
|
27 |
|
11024
|
28 |
consts finiteRchain :: "('a => 'a => bool) * 'a list => bool"
|
|
29 |
recdef finiteRchain "measure (\<lambda>(R, l). size l)"
|
|
30 |
"finiteRchain(R, []) = True"
|
|
31 |
"finiteRchain(R, [x]) = True"
|
|
32 |
"finiteRchain(R, x # y # rst) = (R x y \<and> finiteRchain (R, y # rst))"
|
5124
|
33 |
|
11024
|
34 |
text {* Not handled automatically: too complicated. *}
|
5124
|
35 |
consts variant :: "nat * nat list => nat"
|
11024
|
36 |
recdef variant "measure (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> y) ns))"
|
|
37 |
"variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
|
5124
|
38 |
|
|
39 |
consts gcd :: "nat * nat => nat"
|
11024
|
40 |
recdef gcd "measure (\<lambda>(x, y). x + y)"
|
|
41 |
"gcd (0, y) = y"
|
|
42 |
"gcd (Suc x, 0) = Suc x"
|
|
43 |
"gcd (Suc x, Suc y) =
|
|
44 |
(if y \<le> x then gcd (x - y, Suc y) else gcd (Suc x, y - x))"
|
|
45 |
|
|
46 |
|
|
47 |
text {*
|
|
48 |
\medskip The silly @{term g} function: example of nested recursion.
|
|
49 |
Not handled automatically. In fact, @{term g} is the zero constant
|
|
50 |
function.
|
|
51 |
*}
|
5124
|
52 |
|
11024
|
53 |
consts g :: "nat => nat"
|
|
54 |
recdef g less_than
|
|
55 |
"g 0 = 0"
|
|
56 |
"g (Suc x) = g (g x)"
|
|
57 |
|
|
58 |
lemma g_terminates: "g x < Suc x"
|
|
59 |
apply (induct x rule: g.induct)
|
|
60 |
apply (auto simp add: g.simps)
|
|
61 |
done
|
|
62 |
|
|
63 |
lemma g_zero: "g x = 0"
|
|
64 |
apply (induct x rule: g.induct)
|
|
65 |
apply (simp_all add: g.simps g_terminates)
|
|
66 |
done
|
|
67 |
|
5124
|
68 |
|
|
69 |
consts Div :: "nat * nat => nat * nat"
|
11024
|
70 |
recdef Div "measure fst"
|
|
71 |
"Div (0, x) = (0, 0)"
|
|
72 |
"Div (Suc x, y) =
|
|
73 |
(let (q, r) = Div (x, y)
|
|
74 |
in if y \<le> Suc r then (Suc q, 0) else (q, Suc r))"
|
|
75 |
|
|
76 |
text {*
|
|
77 |
\medskip Not handled automatically. Should be the predecessor
|
|
78 |
function, but there is an unnecessary "looping" recursive call in
|
|
79 |
@{term "k 1"}.
|
|
80 |
*}
|
5124
|
81 |
|
11024
|
82 |
consts k :: "nat => nat"
|
|
83 |
recdef k less_than
|
|
84 |
"k 0 = 0"
|
|
85 |
"k (Suc n) =
|
|
86 |
(let x = k 1
|
|
87 |
in if 0 = 1 then k (Suc 1) else n)"
|
|
88 |
|
|
89 |
consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
|
|
90 |
recdef part "measure (\<lambda>(P, l, l1, l2). size l)"
|
|
91 |
"part (P, [], l1, l2) = (l1, l2)"
|
|
92 |
"part (P, h # rst, l1, l2) =
|
|
93 |
(if P h then part (P, rst, h # l1, l2)
|
|
94 |
else part (P, rst, l1, h # l2))"
|
5124
|
95 |
|
11024
|
96 |
consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
|
|
97 |
recdef fqsort "measure (size o snd)"
|
|
98 |
"fqsort (ord, []) = []"
|
|
99 |
"fqsort (ord, x # rst) =
|
|
100 |
(let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
|
|
101 |
in fqsort (ord, less) @ [x] @ fqsort (ord, more))"
|
|
102 |
|
|
103 |
text {*
|
|
104 |
\medskip Silly example which demonstrates the occasional need for
|
|
105 |
additional congruence rules (here: @{thm [source] map_cong}). If
|
|
106 |
the congruence rule is removed, an unprovable termination condition
|
|
107 |
is generated! Termination not proved automatically. TFL requires
|
|
108 |
@{term [source] "\<lambda>x. mapf x"} instead of @{term [source] mapf}.
|
|
109 |
*}
|
5124
|
110 |
|
11024
|
111 |
consts mapf :: "nat => nat list"
|
|
112 |
recdef mapf "measure (\<lambda>m. m)"
|
|
113 |
"mapf 0 = []"
|
|
114 |
"mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
|
|
115 |
(hints cong: map_cong)
|
5124
|
116 |
|
11024
|
117 |
recdef_tc mapf_tc: mapf
|
|
118 |
apply (rule allI)
|
|
119 |
apply (case_tac "n = 0")
|
|
120 |
apply simp_all
|
|
121 |
done
|
|
122 |
|
|
123 |
text {* Removing the termination condition from the generated thms: *}
|
|
124 |
|
|
125 |
lemma "mapf (Suc n) = concat (map mapf (replicate n n))"
|
|
126 |
apply (simp add: mapf.simps mapf_tc)
|
|
127 |
done
|
|
128 |
|
|
129 |
lemmas mapf_induct = mapf.induct [OF mapf_tc]
|
5124
|
130 |
|
|
131 |
end
|