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 


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


21 

25767

22 
primrec


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

24999

24 
where

25767

25 
"nat_of_index (index_of_nat k) = k"


26 
lemmas [code func del] = nat_of_index.simps

24999

27 


28 
lemma index_id [simp]:

25767

29 
"index_of_nat (nat_of_index n) = n"


30 
by (cases n) simp_all


31 


32 
lemma nat_of_index_inject [simp]:


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


34 
by (cases n) auto

24999

35 


36 
lemma index:

25767

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

24999

38 
proof

25767

39 
fix n :: nat


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


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

24999

42 
next

25767

43 
fix n :: index


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


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


46 
then show "PROP P n" by simp

24999

47 
qed


48 

25767

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


50 
by (cases n) simp_all

24999

51 


52 

25767

53 
subsection {* Indices as datatype of ints *}


54 


55 
instantiation index :: number


56 
begin

24999

57 

25767

58 
definition


59 
"number_of = index_of_nat o nat"


60 


61 
instance ..


62 


63 
end

24999

64 


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


66 


67 


68 
subsection {* Basic arithmetic *}


69 

25767

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


71 
begin

24999

72 

25767

73 
definition [simp, code func del]:


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

24999

75 


76 
lemma zero_index_code [code inline, code func]:


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

25767

78 
by (simp add: number_of_index_def Pls_def)


79 


80 
definition [simp, code func del]:


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

24999

82 


83 
lemma one_index_code [code inline, code func]:


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

25767

85 
by (simp add: number_of_index_def Pls_def Bit_def)


86 


87 
definition [simp, code func del]:


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


89 


90 
lemma plus_index_code [code func]:


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


92 
by simp


93 


94 
definition [simp, code func del]:


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


96 


97 
definition [simp, code func del]:


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


99 


100 
lemma times_index_code [code func]:


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

24999

102 
by simp


103 

25767

104 
definition [simp, code func del]:


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

24999

106 

25767

107 
definition [simp, code func del]:


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

24999

109 

25767

110 
lemma div_index_code [code func]:


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


112 
by simp

25335

113 

25767

114 
lemma mod_index_code [code func]:


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


116 
by simp

24999

117 

25767

118 
definition [simp, code func del]:


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

24999

120 

25767

121 
definition [simp, code func del]:


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

24999

123 

25767

124 
lemma less_eq_index_code [code func]:


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


126 
by simp

24999

127 

25767

128 
lemma less_index_code [code func]:


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


130 
by simp

24999

131 

25767

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


133 


134 
end

24999

135 

25928

136 
lemma index_of_nat_code [code]:

25918

137 
"index_of_nat = of_nat"


138 
proof


139 
fix n :: nat


140 
have "of_nat n = index_of_nat n"


141 
by (induct n) simp_all


142 
then show "index_of_nat n = of_nat n"


143 
by (rule sym)


144 
qed


145 

25928

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


147 
by (cases i) auto


148 


149 
definition


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


151 
where


152 
"nat_of_index_aux i n = nat_of_index i + n"


153 


154 
lemma nat_of_index_aux_code [code]:


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


156 
by (auto simp add: nat_of_index_aux_def index_not_eq_zero)


157 


158 
lemma nat_of_index_code [code]:


159 
"nat_of_index i = nat_of_index_aux i 0"


160 
by (simp add: nat_of_index_aux_def)

25918

161 

24999

162 


163 
subsection {* ML interface *}


164 


165 
ML {*


166 
structure Index =


167 
struct


168 

25928

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

24999

170 


171 
end;


172 
*}


173 


174 


175 
subsection {* Code serialization *}


176 

25767

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


178 

24999

179 
code_type index


180 
(SML "int")


181 
(OCaml "int")


182 
(Haskell "Integer")


183 


184 
code_instance index :: eq


185 
(Haskell )


186 


187 
setup {*

25928

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


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

24999

190 
*}


191 

25918

192 
code_reserved SML Int int


193 
code_reserved OCaml Pervasives int

24999

194 


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

25928

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

24999

197 
(OCaml "Pervasives.+")


198 
(Haskell infixl 6 "+")


199 

25918

200 
code_const "op  \<Colon> index \<Rightarrow> index \<Rightarrow> index"


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


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


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

24999

204 


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

25928

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

24999

207 
(OCaml "Pervasives.*")


208 
(Haskell infixl 7 "*")


209 

25928

210 
code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"


211 
(SML "Int.div/ ((_),/ (_))")


212 
(OCaml "Pervasives.div")


213 
(Haskell "div")


214 


215 
code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"


216 
(SML "Int.mod/ ((_),/ (_))")


217 
(OCaml "Pervasives.mod")


218 
(Haskell "mod")


219 

24999

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


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


222 
(OCaml "!((_ : Pervasives.int) = _)")


223 
(Haskell infixl 4 "==")


224 


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

25928

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

24999

227 
(OCaml "!((_ : Pervasives.int) <= _)")


228 
(Haskell infix 4 "<=")


229 


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

25928

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

24999

232 
(OCaml "!((_ : Pervasives.int) < _)")


233 
(Haskell infix 4 "<")


234 


235 
end
