author  haftmann 
Fri, 10 Oct 2008 06:45:53 +0200  
changeset 28562  4e74209f113e 
parent 28351  abfc66969d1f 
child 28708  a1a436f09ec6 
permissions  rwrr 
24999  1 
(* ID: $Id$ 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* Type of indices *} 

6 

7 
theory Code_Index 

28228  8 
imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger" 
24999  9 
begin 
10 

11 
text {* 

25767  12 
Indices are isomorphic to HOL @{typ nat} but 
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

13 
mapped to targetlanguage builtin integers. 
24999  14 
*} 
15 

16 
subsection {* Datatype of indices *} 

17 

26140  18 
typedef index = "UNIV \<Colon> nat set" 
19 
morphisms nat_of_index index_of_nat by rule 

24999  20 

26140  21 
lemma index_of_nat_nat_of_index [simp]: 
22 
"index_of_nat (nat_of_index k) = k" 

23 
by (rule nat_of_index_inverse) 

24999  24 

26140  25 
lemma nat_of_index_index_of_nat [simp]: 
26 
"nat_of_index (index_of_nat n) = n" 

27 
by (rule index_of_nat_inverse) 

28 
(unfold index_def, rule UNIV_I) 

24999  29 

30 
lemma index: 

25767  31 
"(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))" 
24999  32 
proof 
25767  33 
fix n :: nat 
34 
assume "\<And>n\<Colon>index. PROP P n" 

35 
then show "PROP P (index_of_nat n)" . 

24999  36 
next 
25767  37 
fix n :: index 
38 
assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)" 

39 
then have "PROP P (index_of_nat (nat_of_index n))" . 

40 
then show "PROP P n" by simp 

24999  41 
qed 
42 

26140  43 
lemma index_case: 
44 
assumes "\<And>n. k = index_of_nat n \<Longrightarrow> P" 

45 
shows P 

46 
by (rule assms [of "nat_of_index k"]) simp 

47 

26304  48 
lemma index_induct_raw: 
26140  49 
assumes "\<And>n. P (index_of_nat n)" 
50 
shows "P k" 

51 
proof  

52 
from assms have "P (index_of_nat (nat_of_index k))" . 

53 
then show ?thesis by simp 

54 
qed 

55 

56 
lemma nat_of_index_inject [simp]: 

57 
"nat_of_index k = nat_of_index l \<longleftrightarrow> k = l" 

58 
by (rule nat_of_index_inject) 

59 

60 
lemma index_of_nat_inject [simp]: 

61 
"index_of_nat n = index_of_nat m \<longleftrightarrow> n = m" 

62 
by (auto intro!: index_of_nat_inject simp add: index_def) 

63 

64 
instantiation index :: zero 

65 
begin 

66 

28562  67 
definition [simp, code del]: 
26140  68 
"0 = index_of_nat 0" 
69 

70 
instance .. 

71 

72 
end 

73 

74 
definition [simp]: 

75 
"Suc_index k = index_of_nat (Suc (nat_of_index k))" 

76 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

77 
rep_datatype "0 \<Colon> index" Suc_index 
26140  78 
proof  
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

79 
fix P :: "index \<Rightarrow> bool" 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

80 
fix k :: index 
26140  81 
assume "P 0" then have init: "P (index_of_nat 0)" by simp 
82 
assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)" 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

83 
then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" . 
26140  84 
then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp 
85 
from init step have "P (index_of_nat (nat_of_index k))" 

86 
by (induct "nat_of_index k") simp_all 

87 
then show "P k" by simp 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

88 
qed simp_all 
26140  89 

28562  90 
lemmas [code del] = index.recs index.cases 
26140  91 

92 
declare index_case [case_names nat, cases type: index] 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

93 
declare index.induct [case_names nat, induct type: index] 
26140  94 

28562  95 
lemma [code]: 
26140  96 
"index_size = nat_of_index" 
97 
proof (rule ext) 

98 
fix k 

99 
have "index_size k = nat_size (nat_of_index k)" 

100 
by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) 

101 
also have "nat_size (nat_of_index k) = nat_of_index k" by (induct "nat_of_index k") simp_all 

102 
finally show "index_size k = nat_of_index k" . 

103 
qed 

104 

28562  105 
lemma [code]: 
26140  106 
"size = nat_of_index" 
107 
proof (rule ext) 

108 
fix k 

109 
show "size k = nat_of_index k" 

110 
by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) 

111 
qed 

112 

28562  113 
lemma [code]: 
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28228
diff
changeset

114 
"eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)" 
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28228
diff
changeset

115 
by (cases k, cases l) (simp add: eq) 
24999  116 

28351  117 
lemma [code nbe]: 
118 
"eq_class.eq (k::index) k \<longleftrightarrow> True" 

119 
by (rule HOL.eq_refl) 

120 

24999  121 

25767  122 
subsection {* Indices as datatype of ints *} 
123 

124 
instantiation index :: number 

125 
begin 

24999  126 

25767  127 
definition 
128 
"number_of = index_of_nat o nat" 

129 

130 
instance .. 

131 

132 
end 

24999  133 

26264  134 
lemma nat_of_index_number [simp]: 
135 
"nat_of_index (number_of k) = number_of k" 

136 
by (simp add: number_of_index_def nat_number_of_def number_of_is_id) 

137 

24999  138 
code_datatype "number_of \<Colon> int \<Rightarrow> index" 
139 

140 

141 
subsection {* Basic arithmetic *} 

142 

25767  143 
instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" 
144 
begin 

24999  145 

28562  146 
lemma zero_index_code [code inline, code]: 
24999  147 
"(0\<Colon>index) = Numeral0" 
25767  148 
by (simp add: number_of_index_def Pls_def) 
25967  149 
lemma [code post]: "Numeral0 = (0\<Colon>index)" 
150 
using zero_index_code .. 

25767  151 

28562  152 
definition [simp, code del]: 
25767  153 
"(1\<Colon>index) = index_of_nat 1" 
24999  154 

28562  155 
lemma one_index_code [code inline, code]: 
24999  156 
"(1\<Colon>index) = Numeral1" 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset

157 
by (simp add: number_of_index_def Pls_def Bit1_def) 
25967  158 
lemma [code post]: "Numeral1 = (1\<Colon>index)" 
159 
using one_index_code .. 

25767  160 

28562  161 
definition [simp, code del]: 
25767  162 
"n + m = index_of_nat (nat_of_index n + nat_of_index m)" 
163 

28562  164 
lemma plus_index_code [code]: 
25767  165 
"index_of_nat n + index_of_nat m = index_of_nat (n + m)" 
166 
by simp 

167 

28562  168 
definition [simp, code del]: 
25767  169 
"n  m = index_of_nat (nat_of_index n  nat_of_index m)" 
170 

28562  171 
definition [simp, code del]: 
25767  172 
"n * m = index_of_nat (nat_of_index n * nat_of_index m)" 
173 

28562  174 
lemma times_index_code [code]: 
25767  175 
"index_of_nat n * index_of_nat m = index_of_nat (n * m)" 
24999  176 
by simp 
177 

28562  178 
definition [simp, code del]: 
25767  179 
"n div m = index_of_nat (nat_of_index n div nat_of_index m)" 
24999  180 

28562  181 
definition [simp, code del]: 
25767  182 
"n mod m = index_of_nat (nat_of_index n mod nat_of_index m)" 
24999  183 

28562  184 
lemma div_index_code [code]: 
25767  185 
"index_of_nat n div index_of_nat m = index_of_nat (n div m)" 
186 
by simp 

25335  187 

28562  188 
lemma mod_index_code [code]: 
25767  189 
"index_of_nat n mod index_of_nat m = index_of_nat (n mod m)" 
190 
by simp 

24999  191 

28562  192 
definition [simp, code del]: 
25767  193 
"n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m" 
24999  194 

28562  195 
definition [simp, code del]: 
25767  196 
"n < m \<longleftrightarrow> nat_of_index n < nat_of_index m" 
24999  197 

28562  198 
lemma less_eq_index_code [code]: 
25767  199 
"index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m" 
200 
by simp 

24999  201 

28562  202 
lemma less_index_code [code]: 
25767  203 
"index_of_nat n < index_of_nat m \<longleftrightarrow> n < m" 
204 
by simp 

24999  205 

25767  206 
instance by default (auto simp add: left_distrib index) 
207 

208 
end 

24999  209 

26140  210 
lemma Suc_index_minus_one: "Suc_index n  1 = n" by simp 
211 

25928  212 
lemma index_of_nat_code [code]: 
25918  213 
"index_of_nat = of_nat" 
214 
proof 

215 
fix n :: nat 

216 
have "of_nat n = index_of_nat n" 

217 
by (induct n) simp_all 

218 
then show "index_of_nat n = of_nat n" 

219 
by (rule sym) 

220 
qed 

221 

25928  222 
lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1" 
223 
by (cases i) auto 

224 

225 
definition 

226 
nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" 

227 
where 

228 
"nat_of_index_aux i n = nat_of_index i + n" 

229 

230 
lemma nat_of_index_aux_code [code]: 

231 
"nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i  1) (Suc n))" 

232 
by (auto simp add: nat_of_index_aux_def index_not_eq_zero) 

233 

234 
lemma nat_of_index_code [code]: 

235 
"nat_of_index i = nat_of_index_aux i 0" 

236 
by (simp add: nat_of_index_aux_def) 

25918  237 

24999  238 

28042  239 
text {* Measure function (for termination proofs) *} 
240 

28228  241 
lemma [measure_function]: 
242 
"is_measure nat_of_index" by (rule is_measure_trivial) 

28042  243 

24999  244 
subsection {* ML interface *} 
245 

246 
ML {* 

247 
structure Index = 

248 
struct 

249 

25928  250 
fun mk k = HOLogic.mk_number @{typ index} k; 
24999  251 

252 
end; 

253 
*} 

254 

255 

26009  256 
subsection {* Specialized @{term "op  \<Colon> index \<Rightarrow> index \<Rightarrow> index"}, 
257 
@{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"} 

258 
operations *} 

259 

260 
definition 

261 
minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index" 

262 
where 

28562  263 
[code del]: "minus_index_aux = op " 
26009  264 

28562  265 
lemma [code]: "op  = minus_index_aux" 
26009  266 
using minus_index_aux_def .. 
267 

268 
definition 

269 
div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" 

270 
where 

28562  271 
[code del]: "div_mod_index n m = (n div m, n mod m)" 
26009  272 

28562  273 
lemma [code]: 
26009  274 
"div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))" 
275 
unfolding div_mod_index_def by auto 

276 

28562  277 
lemma [code]: 
26009  278 
"n div m = fst (div_mod_index n m)" 
279 
unfolding div_mod_index_def by simp 

280 

28562  281 
lemma [code]: 
26009  282 
"n mod m = snd (div_mod_index n m)" 
283 
unfolding div_mod_index_def by simp 

284 

285 

28228  286 
subsection {* Code generator setup *} 
24999  287 

25767  288 
text {* Implementation of indices by bounded integers *} 
289 

24999  290 
code_type index 
291 
(SML "int") 

292 
(OCaml "int") 

25967  293 
(Haskell "Int") 
24999  294 

295 
code_instance index :: eq 

296 
(Haskell ) 

297 

298 
setup {* 

25928  299 
fold (Numeral.add_code @{const_name number_index_inst.number_of_index} 
300 
false false) ["SML", "OCaml", "Haskell"] 

24999  301 
*} 
302 

25918  303 
code_reserved SML Int int 
304 
code_reserved OCaml Pervasives int 

24999  305 

306 
code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index" 

25928  307 
(SML "Int.+/ ((_),/ (_))") 
25967  308 
(OCaml "Pervasives.( + )") 
24999  309 
(Haskell infixl 6 "+") 
310 

26009  311 
code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index" 
25918  312 
(SML "Int.max/ (_/ / _,/ 0 : int)") 
313 
(OCaml "Pervasives.max/ (_/ / _)/ (0 : int) ") 

314 
(Haskell "max/ (_/ / _)/ (0 :: Int)") 

24999  315 

316 
code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index" 

25928  317 
(SML "Int.*/ ((_),/ (_))") 
25967  318 
(OCaml "Pervasives.( * )") 
24999  319 
(Haskell infixl 7 "*") 
320 

26009  321 
code_const div_mod_index 
322 
(SML "(fn n => fn m =>/ (n div m, n mod m))") 

323 
(OCaml "(fun n > fun m >/ (n '/ m, n mod m))") 

324 
(Haskell "divMod") 

25928  325 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28228
diff
changeset

326 
code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool" 
24999  327 
(SML "!((_ : Int.int) = _)") 
25967  328 
(OCaml "!((_ : int) = _)") 
24999  329 
(Haskell infixl 4 "==") 
330 

331 
code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool" 

25928  332 
(SML "Int.<=/ ((_),/ (_))") 
25967  333 
(OCaml "!((_ : int) <= _)") 
24999  334 
(Haskell infix 4 "<=") 
335 

336 
code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool" 

25928  337 
(SML "Int.</ ((_),/ (_))") 
25967  338 
(OCaml "!((_ : int) < _)") 
24999  339 
(Haskell infix 4 "<") 
340 

28228  341 
text {* Evaluation *} 
342 

28562  343 
lemma [code, code del]: 
28228  344 
"(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" .. 
345 

346 
code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term" 

347 
(SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)") 

348 

24999  349 
end 