24999

1 
(* ID: $Id$


2 
Author: Florian Haftmann, TU Muenchen


3 
*)


4 


5 
header {* Type of indices *}


6 


7 
theory Code_Index

25691

8 
imports ATP_Linkup

24999

9 
begin


10 


11 
text {*

25767

12 
Indices are isomorphic to HOL @{typ nat} but

24999

13 
mapped to targetlanguage builtin integers


14 
*}


15 


16 
subsection {* Datatype of indices *}


17 

25767

18 
datatype index = index_of_nat nat

24999

19 

25967

20 
lemma [code func]:


21 
"index_size k = 0"


22 
by (cases k) simp


23 

24999

24 
lemmas [code func del] = index.recs index.cases


25 

25767

26 
primrec


27 
nat_of_index :: "index \<Rightarrow> nat"

24999

28 
where

25767

29 
"nat_of_index (index_of_nat k) = k"


30 
lemmas [code func del] = nat_of_index.simps

24999

31 


32 
lemma index_id [simp]:

25767

33 
"index_of_nat (nat_of_index n) = n"


34 
by (cases n) simp_all


35 


36 
lemma nat_of_index_inject [simp]:


37 
"nat_of_index n = nat_of_index m \<longleftrightarrow> n = m"


38 
by (cases n) auto

24999

39 


40 
lemma index:

25767

41 
"(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"

24999

42 
proof

25767

43 
fix n :: nat


44 
assume "\<And>n\<Colon>index. PROP P n"


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

24999

46 
next

25767

47 
fix n :: index


48 
assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)"


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


50 
then show "PROP P n" by simp

24999

51 
qed


52 

25767

53 
lemma [code func]: "size (n\<Colon>index) = 0"


54 
by (cases n) simp_all

24999

55 


56 

25767

57 
subsection {* Indices as datatype of ints *}


58 


59 
instantiation index :: number


60 
begin

24999

61 

25767

62 
definition


63 
"number_of = index_of_nat o nat"


64 


65 
instance ..


66 


67 
end

24999

68 


69 
code_datatype "number_of \<Colon> int \<Rightarrow> index"


70 


71 


72 
subsection {* Basic arithmetic *}


73 

25767

74 
instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"


75 
begin

24999

76 

25767

77 
definition [simp, code func del]:


78 
"(0\<Colon>index) = index_of_nat 0"

24999

79 


80 
lemma zero_index_code [code inline, code func]:


81 
"(0\<Colon>index) = Numeral0"

25767

82 
by (simp add: number_of_index_def Pls_def)

25967

83 
lemma [code post]: "Numeral0 = (0\<Colon>index)"


84 
using zero_index_code ..

25767

85 


86 
definition [simp, code func del]:


87 
"(1\<Colon>index) = index_of_nat 1"

24999

88 


89 
lemma one_index_code [code inline, code func]:


90 
"(1\<Colon>index) = Numeral1"

25767

91 
by (simp add: number_of_index_def Pls_def Bit_def)

25967

92 
lemma [code post]: "Numeral1 = (1\<Colon>index)"


93 
using one_index_code ..

25767

94 


95 
definition [simp, code func del]:


96 
"n + m = index_of_nat (nat_of_index n + nat_of_index m)"


97 


98 
lemma plus_index_code [code func]:


99 
"index_of_nat n + index_of_nat m = index_of_nat (n + m)"


100 
by simp


101 


102 
definition [simp, code func del]:


103 
"n  m = index_of_nat (nat_of_index n  nat_of_index m)"


104 


105 
definition [simp, code func del]:


106 
"n * m = index_of_nat (nat_of_index n * nat_of_index m)"


107 


108 
lemma times_index_code [code func]:


109 
"index_of_nat n * index_of_nat m = index_of_nat (n * m)"

24999

110 
by simp


111 

25767

112 
definition [simp, code func del]:


113 
"n div m = index_of_nat (nat_of_index n div nat_of_index m)"

24999

114 

25767

115 
definition [simp, code func del]:


116 
"n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"

24999

117 

25767

118 
lemma div_index_code [code func]:


119 
"index_of_nat n div index_of_nat m = index_of_nat (n div m)"


120 
by simp

25335

121 

25767

122 
lemma mod_index_code [code func]:


123 
"index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"


124 
by simp

24999

125 

25767

126 
definition [simp, code func del]:


127 
"n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"

24999

128 

25767

129 
definition [simp, code func del]:


130 
"n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"

24999

131 

25767

132 
lemma less_eq_index_code [code func]:


133 
"index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"


134 
by simp

24999

135 

25767

136 
lemma less_index_code [code func]:


137 
"index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"


138 
by simp

24999

139 

25767

140 
instance by default (auto simp add: left_distrib index)


141 


142 
end

24999

143 

25928

144 
lemma index_of_nat_code [code]:

25918

145 
"index_of_nat = of_nat"


146 
proof


147 
fix n :: nat


148 
have "of_nat n = index_of_nat n"


149 
by (induct n) simp_all


150 
then show "index_of_nat n = of_nat n"


151 
by (rule sym)


152 
qed


153 

25928

154 
lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"


155 
by (cases i) auto


156 


157 
definition


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


159 
where


160 
"nat_of_index_aux i n = nat_of_index i + n"


161 


162 
lemma nat_of_index_aux_code [code]:


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


164 
by (auto simp add: nat_of_index_aux_def index_not_eq_zero)


165 


166 
lemma nat_of_index_code [code]:


167 
"nat_of_index i = nat_of_index_aux i 0"


168 
by (simp add: nat_of_index_aux_def)

25918

169 

24999

170 


171 
subsection {* ML interface *}


172 


173 
ML {*


174 
structure Index =


175 
struct


176 

25928

177 
fun mk k = HOLogic.mk_number @{typ index} k;

24999

178 


179 
end;


180 
*}


181 


182 

26009

183 
subsection {* Specialized @{term "op  \<Colon> index \<Rightarrow> index \<Rightarrow> index"},


184 
@{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"}


185 
operations *}


186 


187 
definition


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


189 
where


190 
[code func del]: "minus_index_aux = op "


191 


192 
lemma [code func]: "op  = minus_index_aux"


193 
using minus_index_aux_def ..


194 


195 
definition


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


197 
where


198 
[code func del]: "div_mod_index n m = (n div m, n mod m)"


199 


200 
lemma [code func]:


201 
"div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"


202 
unfolding div_mod_index_def by auto


203 


204 
lemma [code func]:


205 
"n div m = fst (div_mod_index n m)"


206 
unfolding div_mod_index_def by simp


207 


208 
lemma [code func]:


209 
"n mod m = snd (div_mod_index n m)"


210 
unfolding div_mod_index_def by simp


211 


212 

24999

213 
subsection {* Code serialization *}


214 

25767

215 
text {* Implementation of indices by bounded integers *}


216 

24999

217 
code_type index


218 
(SML "int")


219 
(OCaml "int")

25967

220 
(Haskell "Int")

24999

221 


222 
code_instance index :: eq


223 
(Haskell )


224 


225 
setup {*

25928

226 
fold (Numeral.add_code @{const_name number_index_inst.number_of_index}


227 
false false) ["SML", "OCaml", "Haskell"]

24999

228 
*}


229 

25918

230 
code_reserved SML Int int


231 
code_reserved OCaml Pervasives int

24999

232 


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

25928

234 
(SML "Int.+/ ((_),/ (_))")

25967

235 
(OCaml "Pervasives.( + )")

24999

236 
(Haskell infixl 6 "+")


237 

26009

238 
code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index"

25918

239 
(SML "Int.max/ (_/ / _,/ 0 : int)")


240 
(OCaml "Pervasives.max/ (_/ / _)/ (0 : int) ")


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

24999

242 


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

25928

244 
(SML "Int.*/ ((_),/ (_))")

25967

245 
(OCaml "Pervasives.( * )")

24999

246 
(Haskell infixl 7 "*")


247 

26009

248 
code_const div_mod_index


249 
(SML "(fn n => fn m =>/ (n div m, n mod m))")


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


251 
(Haskell "divMod")

25928

252 

24999

253 
code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"


254 
(SML "!((_ : Int.int) = _)")

25967

255 
(OCaml "!((_ : int) = _)")

24999

256 
(Haskell infixl 4 "==")


257 


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

25928

259 
(SML "Int.<=/ ((_),/ (_))")

25967

260 
(OCaml "!((_ : int) <= _)")

24999

261 
(Haskell infix 4 "<=")


262 


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

25928

264 
(SML "Int.</ ((_),/ (_))")

25967

265 
(OCaml "!((_ : int) < _)")

24999

266 
(Haskell infix 4 "<")


267 


268 
end
