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 

25918

136 
lemma index_of_nat_code [code func]:


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 


146 
lemma nat_of_index_code [code func]:


147 
"nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n  1)))"


148 
by (induct n) simp


149 

24999

150 


151 
subsection {* ML interface *}


152 


153 
ML {*


154 
structure Index =


155 
struct


156 

25767

157 
fun mk k = @{term index_of_nat} $ HOLogic.mk_number @{typ index} k;

24999

158 


159 
end;


160 
*}


161 


162 


163 
subsection {* Code serialization *}


164 

25767

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


166 

24999

167 
code_type index


168 
(SML "int")


169 
(OCaml "int")


170 
(Haskell "Integer")


171 


172 
code_instance index :: eq


173 
(Haskell )


174 


175 
setup {*

25918

176 
fold (fn target => CodeTarget.add_pretty_numeral target false

24999

177 
@{const_name number_index_inst.number_of_index}

25918

178 
@{const_name Int.B0} @{const_name Int.B1}


179 
@{const_name Int.Pls} @{const_name Int.Min}


180 
@{const_name Int.Bit}

24999

181 
) ["SML", "OCaml", "Haskell"]


182 
*}


183 

25918

184 
code_reserved SML Int int


185 
code_reserved OCaml Pervasives int

24999

186 


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


188 
(SML "Int.+ ((_), (_))")


189 
(OCaml "Pervasives.+")


190 
(Haskell infixl 6 "+")


191 

25918

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


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


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


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

24999

196 


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


198 
(SML "Int.* ((_), (_))")


199 
(OCaml "Pervasives.*")


200 
(Haskell infixl 7 "*")


201 


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


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


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


205 
(Haskell infixl 4 "==")


206 


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


208 
(SML "Int.<= ((_), (_))")


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


210 
(Haskell infix 4 "<=")


211 


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


213 
(SML "Int.< ((_), (_))")


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


215 
(Haskell infix 4 "<")


216 

25767

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


218 
(SML "IntInf.div ((_), (_))")


219 
(OCaml "Big'_int.div'_big'_int")


220 
(Haskell "div")


221 


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


223 
(SML "IntInf.mod ((_), (_))")


224 
(OCaml "Big'_int.mod'_big'_int")


225 
(Haskell "mod")


226 

24999

227 
end
