author  krauss 
Mon, 05 Jun 2006 14:26:07 +0200  
changeset 19770  be5c23ebe1eb 
parent 19736  d8d0f8f51d69 
child 19782  48c4632e2c28 
permissions  rwrr 
19568  1 
(* Title: HOL/ex/Fundefs.thy 
2 
ID: $Id$ 

3 
Author: Alexander Krauss, TU Muenchen 

4 

5 
Examples of function definitions using the new "function" package. 

6 
*) 

7 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

8 
theory Fundefs 
19568  9 
imports Main 
10 
begin 

11 

12 
section {* Very basic *} 

13 

14 
consts fib :: "nat \<Rightarrow> nat" 

19736  15 
function 
19568  16 
"fib 0 = 1" 
17 
"fib (Suc 0) = 1" 

18 
"fib (Suc (Suc n)) = fib n + fib (Suc n)" 

19736  19 
by pat_completeness  {* shows that the patterns are complete *} 
20 
auto  {* shows that the patterns are compatible *} 

19568  21 

19736  22 
text {* we get partial simp and induction rules: *} 
19568  23 
thm fib.psimps 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

24 
thm pinduct 
19568  25 

19736  26 
text {* There is also a cases rule to distinguish cases along the definition *} 
19568  27 
thm fib.cases 
28 

19736  29 
text {* Now termination: *} 
19568  30 
termination fib 
19736  31 
by (auto_term "less_than") 
19568  32 

33 
thm fib.simps 

34 
thm fib.induct 

35 

36 

37 
section {* Currying *} 

38 

19736  39 
consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
19568  40 
function 
41 
"add 0 y = y" 

42 
"add (Suc x) y = Suc (add x y)" 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

43 
thm add_rel.cases 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

44 

19568  45 
by pat_completeness auto 
19736  46 
termination 
19568  47 
by (auto_term "measure fst") 
48 

19736  49 
thm add.induct  {* Note the curried induction predicate *} 
19568  50 

51 

52 
section {* Nested recursion *} 

53 

54 
consts nz :: "nat \<Rightarrow> nat" 

55 
function 

56 
"nz 0 = 0" 

57 
"nz (Suc x) = nz (nz x)" 

58 
by pat_completeness auto 

59 

19736  60 
lemma nz_is_zero:  {* A lemma we need to prove termination *} 
19583
c5fa77b03442
functionpackage: Changed record usage to make sml/nj happy...
krauss
parents:
19568
diff
changeset

61 
assumes trm: "x \<in> nz_dom" 
19568  62 
shows "nz x = 0" 
63 
using trm 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

64 
apply induct 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

65 
apply auto 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

66 
done 
19568  67 

68 
termination nz 

19736  69 
apply (auto_term "less_than")  {* Oops, it left us something to prove *} 
19568  70 
by (auto simp:nz_is_zero) 
71 

72 
thm nz.simps 

73 
thm nz.induct 

74 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

75 
text {* Here comes McCarthy's 91function *} 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

76 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

77 
consts f91 :: "nat => nat" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

78 
function 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

79 
"f91 n = (if 100 < n then n  10 else f91 (f91 (n + 11)))" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

80 
by pat_completeness auto 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

81 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

82 
(* Prove a lemma before attempting a termination proof *) 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

83 
lemma f91_estimate: 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

84 
assumes trm: "n : f91_dom" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

85 
shows "n < f91 n + 11" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

86 
using trm by induct auto 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

87 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

88 
(* Now go for termination *) 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

89 
termination 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

90 
proof 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

91 
let ?R = "measure (%x. 101  x)" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

92 
show "wf ?R" .. 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

93 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

94 
fix n::nat assume "~ 100 < n" (* Inner call *) 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

95 
thus "(n + 11, n) : ?R" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

96 
by simp arith 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

97 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

98 
assume inner_trm: "n + 11 : f91_dom" (* Outer call *) 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

99 
with f91_estimate have "n + 11 < f91 (n + 11) + 11" . 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

100 
with `~ 100 < n` show "(f91 (n + 11), n) : ?R" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

101 
by simp arith 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

102 
qed 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

103 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

104 

19568  105 

106 
section {* More general patterns *} 

107 

19736  108 
text {* Currently, patterns must always be compatible with each other, since 
19568  109 
no automatich splitting takes place. But the following definition of 
19736  110 
gcd is ok, although patterns overlap: *} 
19568  111 

112 
consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

19736  113 
function 
19568  114 
"gcd2 x 0 = x" 
115 
"gcd2 0 y = y" 

116 
"gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y  x) 

117 
else gcd2 (x  y) (Suc y))" 

118 
by pat_completeness auto 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

119 
termination 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

120 
by (auto_term "measure (\<lambda>(x,y). x + y)") 
19568  121 

122 
thm gcd2.simps 

123 
thm gcd2.induct 

124 

125 

19736  126 
text {* General patterns allow even strange definitions: *} 
19568  127 
consts ev :: "nat \<Rightarrow> bool" 
19736  128 
function 
19568  129 
"ev (2 * n) = True" 
130 
"ev (2 * n + 1) = False" 

19736  131 
proof   {* completeness is more difficult here \dots *} 
19568  132 
assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P" 
133 
and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P" 

134 
have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto 

135 
show "P" 

19736  136 
proof cases 
19568  137 
assume "x mod 2 = 0" 
138 
with divmod have "x = 2 * (x div 2)" by simp 

139 
with c1 show "P" . 

140 
next 

141 
assume "x mod 2 \<noteq> 0" 

142 
hence "x mod 2 = 1" by simp 

143 
with divmod have "x = 2 * (x div 2) + 1" by simp 

144 
with c2 show "P" . 

145 
qed 

19736  146 
qed presburger+  {* solve compatibility with presburger *} 
19568  147 
termination by (auto_term "{}") 
148 

149 
thm ev.simps 

150 
thm ev.induct 

151 
thm ev.cases 

152 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

153 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

154 
section {* Mutual Recursion *} 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

155 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

156 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

157 
consts 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

158 
evn :: "nat \<Rightarrow> bool" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

159 
od :: "nat \<Rightarrow> bool" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

160 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

161 
function 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

162 
"evn 0 = True" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

163 
"evn (Suc n) = od n" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

164 
and 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

165 
"od 0 = False" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

166 
"od (Suc n) = evn n" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

167 
by pat_completeness auto 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

168 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

169 
thm evn.psimps 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

170 
thm od.psimps 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

171 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

172 
thm evn_od.pinduct 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

173 
thm evn_od.termination 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

174 
thm evn_od.domintros 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

175 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

176 
termination 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

177 
by (auto_term "measure (sum_case (%n. n) (%n. n))") 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

178 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

179 
thm evn.simps 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

180 
thm od.simps 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

181 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

182 

19736  183 
end 