author  haftmann 
Tue, 25 Sep 2007 21:08:34 +0200  
changeset 24715  f96d86cdbe5a 
parent 24630  351a308ab58d 
child 24994  c385c4eabb3b 
permissions  rwrr 
23854  1 
(* Title: HOL/Library/Efficient_Nat.thy 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer, TU Muenchen 

4 
*) 

5 

6 
header {* Implementation of natural numbers by integers *} 

7 

8 
theory Efficient_Nat 

9 
imports Main Pretty_Int 

10 
begin 

11 

12 
text {* 

13 
When generating code for functions on natural numbers, the canonical 

14 
representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for 

15 
computations involving large numbers. The efficiency of the generated 

16 
code can be improved drastically by implementing natural numbers by 

17 
integers. To do this, just include this theory. 

18 
*} 

19 

20 
subsection {* Logical rewrites *} 

21 

22 
text {* 

23 
An inttonat conversion 

24 
restricted to nonnegative ints (in contrast to @{const nat}). 

25 
Note that this restriction has no logical relevance and 

26 
is just a kind of proof hint  nothing prevents you from 

27 
writing nonsense like @{term "nat_of_int (4)"} 

28 
*} 

29 

30 
definition 

31 
nat_of_int :: "int \<Rightarrow> nat" where 

32 
"k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k" 

33 

34 
definition 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

35 
int_of_nat :: "nat \<Rightarrow> int" where 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

36 
"int_of_nat n = of_nat n" 
23854  37 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

38 
lemma int_of_nat_Suc [simp]: 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

39 
"int_of_nat (Suc n) = 1 + int_of_nat n" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

40 
unfolding int_of_nat_def by simp 
23854  41 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

42 
lemma int_of_nat_add: 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

43 
"int_of_nat (m + n) = int_of_nat m + int_of_nat n" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

44 
unfolding int_of_nat_def by (rule of_nat_add) 
23854  45 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

46 
lemma int_of_nat_mult: 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

47 
"int_of_nat (m * n) = int_of_nat m * int_of_nat n" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

48 
unfolding int_of_nat_def by (rule of_nat_mult) 
23854  49 

50 
lemma nat_of_int_of_number_of: 

51 
fixes k 

52 
assumes "k \<ge> 0" 

53 
shows "number_of k = nat_of_int (number_of k)" 

54 
unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id .. 

55 

56 
lemma nat_of_int_of_number_of_aux: 

57 
fixes k 

58 
assumes "Numeral.Pls \<le> k \<equiv> True" 

59 
shows "k \<ge> 0" 

60 
using assms unfolding Pls_def by simp 

61 

62 
lemma nat_of_int_int: 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

63 
"nat_of_int (int_of_nat n) = n" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

64 
using nat_of_int_def int_of_nat_def by simp 
23854  65 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

66 
lemma eq_nat_of_int: "int_of_nat n = x \<Longrightarrow> n = nat_of_int x" 
23854  67 
by (erule subst, simp only: nat_of_int_int) 
68 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24222
diff
changeset

69 
code_datatype nat_of_int 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24222
diff
changeset

70 

23854  71 
text {* 
72 
Case analysis on natural numbers is rephrased using a conditional 

73 
expression: 

74 
*} 

75 

76 
lemma [code unfold, code inline del]: 

77 
"nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n  1))" 

78 
proof  

79 
have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n  1))" 

80 
proof  

81 
fix f g n 

82 
show "nat_case f g n = (if n = 0 then f else g (n  1))" 

83 
by (cases n) simp_all 

84 
qed 

85 
show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n  1))" 

86 
by (rule eq_reflection ext rewrite)+ 

87 
qed 

88 

89 
lemma [code inline]: 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

90 
"nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int_of_nat n  1)))" 
23854  91 
proof (rule ext)+ 
92 
fix f g n 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

93 
show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int_of_nat n  1)))" 
23854  94 
by (cases n) (simp_all add: nat_of_int_int) 
95 
qed 

96 

97 
text {* 

98 
Most standard arithmetic functions on natural numbers are implemented 

99 
using their counterparts on the integers: 

100 
*} 

101 

102 
lemma [code func]: "0 = nat_of_int 0" 

103 
by (simp add: nat_of_int_def) 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

104 

23854  105 
lemma [code func, code inline]: "1 = nat_of_int 1" 
106 
by (simp add: nat_of_int_def) 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

107 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

108 
lemma [code func]: "Suc n = nat_of_int (int_of_nat n + 1)" 
23854  109 
by (simp add: eq_nat_of_int) 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

110 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

111 
lemma [code]: "m + n = nat (int_of_nat m + int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

112 
by (simp add: int_of_nat_def nat_eq_iff2) 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

113 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

114 
lemma [code func, code inline]: "m + n = nat_of_int (int_of_nat m + int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

115 
by (simp add: eq_nat_of_int int_of_nat_add) 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

116 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

117 
lemma [code, code inline]: "m  n = nat (int_of_nat m  int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

118 
by (simp add: int_of_nat_def nat_eq_iff2 of_nat_diff) 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

119 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

120 
lemma [code]: "m * n = nat (int_of_nat m * int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

121 
unfolding int_of_nat_def 
23854  122 
by (simp add: of_nat_mult [symmetric] del: of_nat_mult) 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

123 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

124 
lemma [code func, code inline]: "m * n = nat_of_int (int_of_nat m * int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

125 
by (simp add: eq_nat_of_int int_of_nat_mult) 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

126 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

127 
lemma [code]: "m div n = nat (int_of_nat m div int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

128 
unfolding int_of_nat_def zdiv_int [symmetric] by simp 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

129 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

130 
lemma div_nat_code [code func]: 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

131 
"m div k = nat_of_int (fst (divAlg (int_of_nat m, int_of_nat k)))" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

132 
unfolding div_def [symmetric] int_of_nat_def zdiv_int [symmetric] 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

133 
unfolding int_of_nat_def [symmetric] nat_of_int_int .. 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

134 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

135 
lemma [code]: "m mod n = nat (int_of_nat m mod int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

136 
unfolding int_of_nat_def zmod_int [symmetric] by simp 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

137 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

138 
lemma mod_nat_code [code func]: 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

139 
"m mod k = nat_of_int (snd (divAlg (int_of_nat m, int_of_nat k)))" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

140 
unfolding mod_def [symmetric] int_of_nat_def zmod_int [symmetric] 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

141 
unfolding int_of_nat_def [symmetric] nat_of_int_int .. 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

142 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

143 
lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int_of_nat m < int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

144 
unfolding int_of_nat_def by simp 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

145 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

146 
lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int_of_nat m \<le> int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

147 
unfolding int_of_nat_def by simp 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

148 

f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

149 
lemma [code func, code inline]: "m = n \<longleftrightarrow> int_of_nat m = int_of_nat n" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

150 
unfolding int_of_nat_def by simp 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

151 

23854  152 
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)" 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

153 
by (cases "k < 0") (simp, simp add: nat_of_int_def) 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

154 

23854  155 
lemma [code func]: 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

156 
"int_aux n i = (if int_of_nat n = 0 then i else int_aux (nat_of_int (int_of_nat n  1)) (i + 1))" 
23854  157 
proof  
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

158 
have "0 < n \<Longrightarrow> int_of_nat n = 1 + int_of_nat (nat_of_int (int_of_nat n  1))" 
23854  159 
proof  
160 
assume prem: "n > 0" 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

161 
then have "int_of_nat n  1 \<ge> 0" unfolding int_of_nat_def by auto 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

162 
then have "nat_of_int (int_of_nat n  1) = nat (int_of_nat n  1)" by (simp add: nat_of_int_def) 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

163 
with prem show "int_of_nat n = 1 + int_of_nat (nat_of_int (int_of_nat n  1))" unfolding int_of_nat_def by simp 
23854  164 
qed 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

165 
then show ?thesis unfolding int_aux_def int_of_nat_def by auto 
23854  166 
qed 
167 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

168 
lemma ml_int_of_nat_code [code func, code inline]: 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

169 
"ml_int_of_nat n = ml_int_of_int (int_of_nat n)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

170 
unfolding ml_int_of_nat_def int_of_nat_def by simp 
23854  171 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

172 
lemma nat_of_mlt_int_code [code func, code inline]: 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

173 
"nat_of_ml_int k = nat (int_of_ml_int k)" 
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

174 
unfolding nat_of_ml_int_def by simp 
23854  175 

176 

177 
subsection {* Code generator setup for basic functions *} 

178 

179 
text {* 

180 
@{typ nat} is no longer a datatype but embedded into the integers. 

181 
*} 

182 

183 
code_type nat 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24423
diff
changeset

184 
(SML "int") 
23854  185 
(OCaml "Big'_int.big'_int") 
186 
(Haskell "Integer") 

187 

188 
types_code 

189 
nat ("int") 

190 
attach (term_of) {* 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24423
diff
changeset

191 
val term_of_nat = HOLogic.mk_number HOLogic.natT; 
23854  192 
*} 
193 
attach (test) {* 

194 
fun gen_nat i = random_range 0 i; 

195 
*} 

196 

197 
consts_code 

198 
"0 \<Colon> nat" ("0") 

199 
Suc ("(_ + 1)") 

200 

201 
text {* 

202 
Since natural numbers are implemented 

203 
using integers, the coercion function @{const "int"} of type 

204 
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function, 

205 
likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}. 

206 
For the @{const "nat"} function for converting an integer to a natural 

207 
number, we give a specific implementation using an ML function that 

208 
returns its input value, provided that it is nonnegative, and otherwise 

209 
returns @{text "0"}. 

210 
*} 

211 

212 
consts_code 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

213 
int_of_nat ("(_)") 
23854  214 
nat ("\<module>nat") 
215 
attach {* 

216 
fun nat i = if i < 0 then 0 else i; 

217 
*} 

218 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

219 
code_const int_of_nat 
23854  220 
(SML "_") 
221 
(OCaml "_") 

222 
(Haskell "_") 

223 

224 
code_const nat_of_int 

225 
(SML "_") 

226 
(OCaml "_") 

227 
(Haskell "_") 

228 

229 

230 
subsection {* Preprocessors *} 

231 

232 
text {* 

233 
Natural numerals should be expressed using @{const nat_of_int}. 

234 
*} 

235 

236 
lemmas [code inline del] = nat_number_of_def 

237 

238 
ML {* 

239 
fun nat_of_int_of_number_of thy cts = 

240 
let 

241 
val simplify_less = Simplifier.rewrite 

242 
(HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code})); 

243 
fun mk_rew (t, ty) = 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24423
diff
changeset

244 
if ty = HOLogic.natT andalso 0 <= HOLogic.dest_numeral t then 
23854  245 
Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t) 
246 
> simplify_less 

247 
> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm]) 

248 
> (fn thm => @{thm nat_of_int_of_number_of} OF [thm]) 

249 
> (fn thm => @{thm eq_reflection} OF [thm]) 

250 
> SOME 

251 
else NONE 

252 
in 

253 
fold (HOLogic.add_numerals o Thm.term_of) cts [] 

254 
> map_filter mk_rew 

255 
end; 

256 
*} 

257 

258 
setup {* 

24222  259 
Code.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of) 
23854  260 
*} 
261 

262 
text {* 

263 
In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer 

264 
a constructor term. Therefore, all occurrences of this term in a position 

265 
where a pattern is expected (i.e.\ on the lefthand side of a recursion 

266 
equation or in the arguments of an inductive relation in an introduction 

267 
rule) must be eliminated. 

268 
This can be accomplished by applying the following transformation rules: 

269 
*} 

270 

271 
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow> 

272 
f n = (if n = 0 then g else h (n  1))" 

273 
by (case_tac n) simp_all 

274 

275 
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n  1) n" 

276 
by (case_tac n) simp_all 

277 

278 
text {* 

279 
The rules above are built into a preprocessor that is plugged into 

280 
the code generator. Since the preprocessor for introduction rules 

281 
does not know anything about modes, some of the modes that worked 

282 
for the canonical representation of natural numbers may no longer work. 

283 
*} 

284 

285 
(*<*) 

286 

287 
ML {* 

288 
fun remove_suc thy thms = 

289 
let 

290 
val vname = Name.variant (map fst 

291 
(fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; 

292 
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); 

293 
fun lhs_of th = snd (Thm.dest_comb 

294 
(fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); 

295 
fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); 

296 
fun find_vars ct = (case term_of ct of 

297 
(Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] 

298 
 _ $ _ => 

299 
let val (ct1, ct2) = Thm.dest_comb ct 

300 
in 

301 
map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ 

302 
map (apfst (Thm.capply ct1)) (find_vars ct2) 

303 
end 

304 
 _ => []); 

305 
val eqs = maps 

306 
(fn th => map (pair th) (find_vars (lhs_of th))) thms; 

307 
fun mk_thms (th, (ct, cv')) = 

308 
let 

309 
val th' = 

310 
Thm.implies_elim 

311 
(Conv.fconv_rule (Thm.beta_conversion true) 

312 
(Drule.instantiate' 

313 
[SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), 

314 
SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] 

24222  315 
@{thm Suc_if_eq})) (Thm.forall_intr cv' th) 
23854  316 
in 
317 
case map_filter (fn th'' => 

318 
SOME (th'', singleton 

319 
(Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'') 

320 
handle THM _ => NONE) thms of 

321 
[] => NONE 

322 
 thps => 

323 
let val (ths1, ths2) = split_list thps 

324 
in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end 

325 
end 

326 
in 

327 
case get_first mk_thms eqs of 

328 
NONE => thms 

329 
 SOME x => remove_suc thy x 

330 
end; 

331 

332 
fun eqn_suc_preproc thy ths = 

333 
let 

24222  334 
val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of; 
335 
fun contains_suc t = member (op =) (term_consts t) @{const_name Suc}; 

23854  336 
in 
337 
if forall (can dest) ths andalso 

338 
exists (contains_suc o dest) ths 

339 
then remove_suc thy ths else ths 

340 
end; 

341 

342 
fun remove_suc_clause thy thms = 

343 
let 

344 
val vname = Name.variant (map fst 

345 
(fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; 

24222  346 
fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v) 
23854  347 
 find_var (t $ u) = (case find_var t of NONE => find_var u  x => x) 
348 
 find_var _ = NONE; 

349 
fun find_thm th = 

350 
let val th' = Conv.fconv_rule ObjectLogic.atomize th 

351 
in Option.map (pair (th, th')) (find_var (prop_of th')) end 

352 
in 

353 
case get_first find_thm thms of 

354 
NONE => thms 

355 
 SOME ((th, th'), (Sucv, v)) => 

356 
let 

357 
val cert = cterm_of (Thm.theory_of_thm th); 

358 
val th'' = ObjectLogic.rulify (Thm.implies_elim 

359 
(Conv.fconv_rule (Thm.beta_conversion true) 

360 
(Drule.instantiate' [] 

361 
[SOME (cert (lambda v (Abs ("x", HOLogic.natT, 

362 
abstract_over (Sucv, 

363 
HOLogic.dest_Trueprop (prop_of th')))))), 

24222  364 
SOME (cert v)] @{thm Suc_clause})) 
23854  365 
(Thm.forall_intr (cert v) th')) 
366 
in 

367 
remove_suc_clause thy (map (fn th''' => 

368 
if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) 

369 
end 

370 
end; 

371 

372 
fun clause_suc_preproc thy ths = 

373 
let 

374 
val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop 

375 
in 

376 
if forall (can (dest o concl_of)) ths andalso 

377 
exists (fn th => member (op =) (foldr add_term_consts 

378 
[] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths 

379 
then remove_suc_clause thy ths else ths 

380 
end; 

381 

382 
fun lift_obj_eq f thy = 

383 
map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) 

384 
#> f thy 

385 
#> map (fn thm => thm RS @{thm eq_reflection}) 

386 
#> map (Conv.fconv_rule Drule.beta_eta_conversion) 

387 
*} 

388 

389 
setup {* 

390 
Codegen.add_preprocessor eqn_suc_preproc 

391 
#> Codegen.add_preprocessor clause_suc_preproc 

24222  392 
#> Code.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc) 
393 
#> Code.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc) 

23854  394 
*} 
395 
(*>*) 

396 

397 

398 
subsection {* Module names *} 

399 

400 
code_modulename SML 

401 
Nat Integer 

402 
Divides Integer 

403 
Efficient_Nat Integer 

404 

405 
code_modulename OCaml 

406 
Nat Integer 

407 
Divides Integer 

408 
Efficient_Nat Integer 

409 

410 
code_modulename Haskell 

411 
Nat Integer 

24195  412 
Divides Integer 
23854  413 
Efficient_Nat Integer 
414 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

415 
hide const nat_of_int int_of_nat 
23854  416 

417 
end 