author  haftmann 
Fri, 06 Feb 2009 09:05:19 +0100  
changeset 29815  9e94b7078fa5 
parent 28708  a1a436f09ec6 
child 29823  0ab754d13ccd 
permissions  rwrr 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

1 
(* Author: Florian Haftmann, TU Muenchen *) 
24999  2 

3 
header {* Type of indices *} 

4 

5 
theory Code_Index 

28228  6 
imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger" 
24999  7 
begin 
8 

9 
text {* 

25767  10 
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

11 
mapped to targetlanguage builtin integers. 
24999  12 
*} 
13 

14 
subsection {* Datatype of indices *} 

15 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

16 
typedef (open) index = "UNIV \<Colon> nat set" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

17 
morphisms nat_of of_nat by rule 
24999  18 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

19 
lemma of_nat_nat_of [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

20 
"of_nat (nat_of k) = k" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

21 
by (rule nat_of_inverse) 
24999  22 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

23 
lemma nat_of_of_nat [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

24 
"nat_of (of_nat n) = n" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

25 
by (rule of_nat_inverse) (rule UNIV_I) 
24999  26 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

27 
lemma [measure_function]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

28 
"is_measure nat_of" by (rule is_measure_trivial) 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

29 

24999  30 
lemma index: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

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

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

35 
then show "PROP P (of_nat n)" . 
24999  36 
next 
25767  37 
fix n :: index 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

38 
assume "\<And>n\<Colon>nat. PROP P (of_nat n)" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

39 
then have "PROP P (of_nat (nat_of n))" . 
25767  40 
then show "PROP P n" by simp 
24999  41 
qed 
42 

26140  43 
lemma index_case: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

44 
assumes "\<And>n. k = of_nat n \<Longrightarrow> P" 
26140  45 
shows P 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

46 
by (rule assms [of "nat_of k"]) simp 
26140  47 

26304  48 
lemma index_induct_raw: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

49 
assumes "\<And>n. P (of_nat n)" 
26140  50 
shows "P k" 
51 
proof  

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

52 
from assms have "P (of_nat (nat_of k))" . 
26140  53 
then show ?thesis by simp 
54 
qed 

55 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

56 
lemma nat_of_inject [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

57 
"nat_of k = nat_of l \<longleftrightarrow> k = l" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

58 
by (rule nat_of_inject) 
26140  59 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

60 
lemma of_nat_inject [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

61 
"of_nat n = of_nat m \<longleftrightarrow> n = m" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

62 
by (rule of_nat_inject) (rule UNIV_I)+ 
26140  63 

64 
instantiation index :: zero 

65 
begin 

66 

28562  67 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

68 
"0 = of_nat 0" 
26140  69 

70 
instance .. 

71 

72 
end 

73 

74 
definition [simp]: 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

75 
"Suc_index k = of_nat (Suc (nat_of k))" 
26140  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 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

81 
assume "P 0" then have init: "P (of_nat 0)" by simp 
26140  82 
assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)" 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

83 
then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" . 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

84 
then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

85 
from init step have "P (of_nat (nat_of k))" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

86 
by (induct "nat_of k") simp_all 
26140  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]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

96 
"index_size = nat_of" 
26140  97 
proof (rule ext) 
98 
fix k 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

99 
have "index_size k = nat_size (nat_of k)" 
26140  100 
by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

101 
also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

102 
finally show "index_size k = nat_of k" . 
26140  103 
qed 
104 

28562  105 
lemma [code]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

106 
"size = nat_of" 
26140  107 
proof (rule ext) 
108 
fix k 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

109 
show "size k = nat_of k" 
26140  110 
by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) 
111 
qed 

112 

28562  113 
lemma [code]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

114 
"eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)" 
28346
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 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

128 
"number_of = of_nat o nat" 
25767  129 

130 
instance .. 

131 

132 
end 

24999  133 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

134 
lemma nat_of_number [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

135 
"nat_of (number_of k) = number_of k" 
26264  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 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

147 
"(1\<Colon>index) = of_nat 1" 
24999  148 

28562  149 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

150 
"n + m = of_nat (nat_of n + nat_of m)" 
25767  151 

28562  152 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

153 
"n  m = of_nat (nat_of n  nat_of m)" 
25767  154 

28562  155 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

156 
"n * m = of_nat (nat_of n * nat_of m)" 
25767  157 

28562  158 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

159 
"n div m = of_nat (nat_of n div nat_of m)" 
24999  160 

28562  161 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

162 
"n mod m = of_nat (nat_of n mod nat_of m)" 
24999  163 

28562  164 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

165 
"n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m" 
24999  166 

28562  167 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

168 
"n < m \<longleftrightarrow> nat_of n < nat_of m" 
24999  169 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

170 
instance proof 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

171 
qed (auto simp add: left_distrib) 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

172 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

173 
end 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

174 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

175 
lemma zero_index_code [code inline, code]: 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

176 
"(0\<Colon>index) = Numeral0" 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

177 
by (simp add: number_of_index_def Pls_def) 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

178 
lemma [code post]: "Numeral0 = (0\<Colon>index)" 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

179 
using zero_index_code .. 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

180 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

181 
lemma one_index_code [code inline, code]: 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

182 
"(1\<Colon>index) = Numeral1" 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

183 
by (simp add: number_of_index_def Pls_def Bit1_def) 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

184 
lemma [code post]: "Numeral1 = (1\<Colon>index)" 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

185 
using one_index_code .. 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

186 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

187 
lemma plus_index_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

188 
"of_nat n + of_nat m = of_nat (n + m)" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

189 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

190 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

191 
definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

192 
[simp, code del]: "subtract_index = op " 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

193 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

194 
lemma subtract_index_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

195 
"subtract_index (of_nat n) (of_nat m) = of_nat (n  m)" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

196 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

197 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

198 
lemma minus_index_code [code]: 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

199 
"n  m = subtract_index n m" 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

200 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

201 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

202 
lemma times_index_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

203 
"of_nat n * of_nat m = of_nat (n * m)" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

204 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

205 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

206 
lemma less_eq_index_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

207 
"of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m" 
25767  208 
by simp 
24999  209 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

210 
lemma less_index_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

211 
"of_nat n < of_nat m \<longleftrightarrow> n < m" 
25767  212 
by simp 
24999  213 

26140  214 
lemma Suc_index_minus_one: "Suc_index n  1 = n" by simp 
215 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

216 
lemma of_nat_code [code]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

217 
"of_nat = Nat.of_nat" 
25918  218 
proof 
219 
fix n :: nat 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

220 
have "Nat.of_nat n = of_nat n" 
25918  221 
by (induct n) simp_all 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

222 
then show "of_nat n = Nat.of_nat n" 
25918  223 
by (rule sym) 
224 
qed 

225 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

226 
lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1" 
25928  227 
by (cases i) auto 
228 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

229 
definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

230 
"nat_of_aux i n = nat_of i + n" 
25928  231 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

232 
lemma nat_of_aux_code [code]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

233 
"nat_of_aux i n = (if i = 0 then n else nat_of_aux (i  1) (Suc n))" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

234 
by (auto simp add: nat_of_aux_def index_not_eq_zero) 
25928  235 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

236 
lemma nat_of_code [code]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

237 
"nat_of i = nat_of_aux i 0" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

238 
by (simp add: nat_of_aux_def) 
25918  239 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

240 
definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where 
28562  241 
[code del]: "div_mod_index n m = (n div m, n mod m)" 
26009  242 

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

246 

28562  247 
lemma [code]: 
26009  248 
"n div m = fst (div_mod_index n m)" 
249 
unfolding div_mod_index_def by simp 

250 

28562  251 
lemma [code]: 
26009  252 
"n mod m = snd (div_mod_index n m)" 
253 
unfolding div_mod_index_def by simp 

254 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

255 
hide (open) const of_nat nat_of 
26009  256 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

257 
subsection {* ML interface *} 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

258 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

259 
ML {* 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

260 
structure Index = 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

261 
struct 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

262 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

263 
fun mk k = HOLogic.mk_number @{typ index} k; 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

264 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

265 
end; 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

266 
*} 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

267 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

268 

28228  269 
subsection {* Code generator setup *} 
24999  270 

25767  271 
text {* Implementation of indices by bounded integers *} 
272 

24999  273 
code_type index 
274 
(SML "int") 

275 
(OCaml "int") 

25967  276 
(Haskell "Int") 
24999  277 

278 
code_instance index :: eq 

279 
(Haskell ) 

280 

281 
setup {* 

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

24999  284 
*} 
285 

25918  286 
code_reserved SML Int int 
287 
code_reserved OCaml Pervasives int 

24999  288 

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

25928  290 
(SML "Int.+/ ((_),/ (_))") 
25967  291 
(OCaml "Pervasives.( + )") 
24999  292 
(Haskell infixl 6 "+") 
293 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

294 
code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index" 
25918  295 
(SML "Int.max/ (_/ / _,/ 0 : int)") 
296 
(OCaml "Pervasives.max/ (_/ / _)/ (0 : int) ") 

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

24999  298 

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

25928  300 
(SML "Int.*/ ((_),/ (_))") 
25967  301 
(OCaml "Pervasives.( * )") 
24999  302 
(Haskell infixl 7 "*") 
303 

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

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

307 
(Haskell "divMod") 

25928  308 

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

309 
code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool" 
24999  310 
(SML "!((_ : Int.int) = _)") 
25967  311 
(OCaml "!((_ : int) = _)") 
24999  312 
(Haskell infixl 4 "==") 
313 

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

25928  315 
(SML "Int.<=/ ((_),/ (_))") 
25967  316 
(OCaml "!((_ : int) <= _)") 
24999  317 
(Haskell infix 4 "<=") 
318 

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

25928  320 
(SML "Int.</ ((_),/ (_))") 
25967  321 
(OCaml "!((_ : int) < _)") 
24999  322 
(Haskell infix 4 "<") 
323 

28228  324 
text {* Evaluation *} 
325 

28562  326 
lemma [code, code del]: 
28228  327 
"(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" .. 
328 

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

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

331 

24999  332 
end 