index now a copy of nat rather than int
authorhaftmann
Wed Jan 02 15:14:23 2008 +0100 (2008-01-02)
changeset 25767852bce03412a
parent 25766 6960410f134d
child 25768 1c1ca4b20ec6
index now a copy of nat rather than int
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Library/Code_Index.thy	Wed Jan 02 15:14:22 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Index.thy	Wed Jan 02 15:14:23 2008 +0100
     1.3 @@ -9,190 +9,129 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 -  Indices are isomorphic to HOL @{typ int} but
     1.8 +  Indices are isomorphic to HOL @{typ nat} but
     1.9    mapped to target-language builtin integers
    1.10  *}
    1.11  
    1.12  subsection {* Datatype of indices *}
    1.13  
    1.14 -datatype index = index_of_int int
    1.15 +datatype index = index_of_nat nat
    1.16  
    1.17  lemmas [code func del] = index.recs index.cases
    1.18  
    1.19 -fun
    1.20 -  int_of_index :: "index \<Rightarrow> int"
    1.21 +primrec
    1.22 +  nat_of_index :: "index \<Rightarrow> nat"
    1.23  where
    1.24 -  "int_of_index (index_of_int k) = k"
    1.25 -lemmas [code func del] = int_of_index.simps
    1.26 +  "nat_of_index (index_of_nat k) = k"
    1.27 +lemmas [code func del] = nat_of_index.simps
    1.28  
    1.29  lemma index_id [simp]:
    1.30 -  "index_of_int (int_of_index k) = k"
    1.31 -  by (cases k) simp_all
    1.32 +  "index_of_nat (nat_of_index n) = n"
    1.33 +  by (cases n) simp_all
    1.34 +
    1.35 +lemma nat_of_index_inject [simp]:
    1.36 +  "nat_of_index n = nat_of_index m \<longleftrightarrow> n = m"
    1.37 +  by (cases n) auto
    1.38  
    1.39  lemma index:
    1.40 -  "(\<And>k\<Colon>index. PROP P k) \<equiv> (\<And>k\<Colon>int. PROP P (index_of_int k))"
    1.41 +  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
    1.42  proof
    1.43 -  fix k :: int
    1.44 -  assume "\<And>k\<Colon>index. PROP P k"
    1.45 -  then show "PROP P (index_of_int k)" .
    1.46 +  fix n :: nat
    1.47 +  assume "\<And>n\<Colon>index. PROP P n"
    1.48 +  then show "PROP P (index_of_nat n)" .
    1.49  next
    1.50 -  fix k :: index
    1.51 -  assume "\<And>k\<Colon>int. PROP P (index_of_int k)"
    1.52 -  then have "PROP P (index_of_int (int_of_index k))" .
    1.53 -  then show "PROP P k" by simp
    1.54 +  fix n :: index
    1.55 +  assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)"
    1.56 +  then have "PROP P (index_of_nat (nat_of_index n))" .
    1.57 +  then show "PROP P n" by simp
    1.58  qed
    1.59  
    1.60 -lemma [code func]: "size (k\<Colon>index) = 0"
    1.61 -  by (cases k) simp_all
    1.62 +lemma [code func]: "size (n\<Colon>index) = 0"
    1.63 +  by (cases n) simp_all
    1.64  
    1.65  
    1.66 -subsection {* Built-in integers as datatype on numerals *}
    1.67 +subsection {* Indices as datatype of ints *}
    1.68 +
    1.69 +instantiation index :: number
    1.70 +begin
    1.71  
    1.72 -instance index :: number
    1.73 -  "number_of \<equiv> index_of_int" ..
    1.74 +definition
    1.75 +  "number_of = index_of_nat o nat"
    1.76 +
    1.77 +instance ..
    1.78 +
    1.79 +end
    1.80  
    1.81  code_datatype "number_of \<Colon> int \<Rightarrow> index"
    1.82  
    1.83 -lemma number_of_index_id [simp]:
    1.84 -  "number_of (int_of_index k) = k"
    1.85 -  unfolding number_of_index_def by simp
    1.86 -
    1.87 -lemma number_of_index_shift:
    1.88 -  "number_of k = index_of_int (number_of k)"
    1.89 -  by (simp add: number_of_is_id number_of_index_def)
    1.90 -
    1.91 -lemma int_of_index_number_of [simp]:
    1.92 -  "int_of_index (number_of k) = number_of k"
    1.93 -  unfolding number_of_index_def number_of_is_id by simp
    1.94 -
    1.95  
    1.96  subsection {* Basic arithmetic *}
    1.97  
    1.98 -instance index :: zero
    1.99 -  [simp]: "0 \<equiv> index_of_int 0" ..
   1.100 -lemmas [code func del] = zero_index_def
   1.101 -
   1.102 -instance index :: one
   1.103 -  [simp]: "1 \<equiv> index_of_int 1" ..
   1.104 -lemmas [code func del] = one_index_def
   1.105 -
   1.106 -instance index :: plus
   1.107 -  [simp]: "k + l \<equiv> index_of_int (int_of_index k + int_of_index l)" ..
   1.108 -lemmas [code func del] = plus_index_def
   1.109 -lemma plus_index_code [code func]:
   1.110 -  "index_of_int k + index_of_int l = index_of_int (k + l)"
   1.111 -  unfolding plus_index_def by simp
   1.112 -
   1.113 -instance index :: minus
   1.114 -  [simp]: "- k \<equiv> index_of_int (- int_of_index k)"
   1.115 -  [simp]: "k - l \<equiv> index_of_int (int_of_index k - int_of_index l)" ..
   1.116 -lemmas [code func del] = uminus_index_def minus_index_def
   1.117 -lemma uminus_index_code [code func]:
   1.118 -  "- index_of_int k \<equiv> index_of_int (- k)"
   1.119 -  unfolding uminus_index_def by simp
   1.120 -lemma minus_index_code [code func]:
   1.121 -  "index_of_int k - index_of_int l = index_of_int (k - l)"
   1.122 -  unfolding minus_index_def by simp
   1.123 -
   1.124 -instance index :: times
   1.125 -  [simp]: "k * l \<equiv> index_of_int (int_of_index k * int_of_index l)" ..
   1.126 -lemmas [code func del] = times_index_def
   1.127 -lemma times_index_code [code func]:
   1.128 -  "index_of_int k * index_of_int l = index_of_int (k * l)"
   1.129 -  unfolding times_index_def by simp
   1.130 +instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
   1.131 +begin
   1.132  
   1.133 -instance index :: ord
   1.134 -  [simp]: "k \<le> l \<equiv> int_of_index k \<le> int_of_index l"
   1.135 -  [simp]: "k < l \<equiv> int_of_index k < int_of_index l" ..
   1.136 -lemmas [code func del] = less_eq_index_def less_index_def
   1.137 -lemma less_eq_index_code [code func]:
   1.138 -  "index_of_int k \<le> index_of_int l \<longleftrightarrow> k \<le> l"
   1.139 -  unfolding less_eq_index_def by simp
   1.140 -lemma less_index_code [code func]:
   1.141 -  "index_of_int k < index_of_int l \<longleftrightarrow> k < l"
   1.142 -  unfolding less_index_def by simp
   1.143 -
   1.144 -instance index :: "Divides.div"
   1.145 -  [simp]: "k div l \<equiv> index_of_int (int_of_index k div int_of_index l)"
   1.146 -  [simp]: "k mod l \<equiv> index_of_int (int_of_index k mod int_of_index l)" ..
   1.147 -
   1.148 -instance index :: ring_1
   1.149 -  by default (auto simp add: left_distrib right_distrib)
   1.150 -
   1.151 -lemma of_nat_index: "of_nat n = index_of_int (of_nat n)"
   1.152 -proof (induct n)
   1.153 -  case 0 show ?case by simp
   1.154 -next
   1.155 -  case (Suc n)
   1.156 -  then have "int_of_index (index_of_int (int n))
   1.157 -    = int_of_index (of_nat n)" by simp
   1.158 -  then have "int n = int_of_index (of_nat n)" by simp
   1.159 -  then show ?case by simp
   1.160 -qed
   1.161 -
   1.162 -instance index :: number_ring
   1.163 -  by default
   1.164 -    (simp_all add: left_distrib number_of_index_def of_int_of_nat of_nat_index)
   1.165 +definition [simp, code func del]:
   1.166 +  "(0\<Colon>index) = index_of_nat 0"
   1.167  
   1.168  lemma zero_index_code [code inline, code func]:
   1.169    "(0\<Colon>index) = Numeral0"
   1.170 -  by simp
   1.171 +  by (simp add: number_of_index_def Pls_def)
   1.172 +
   1.173 +definition [simp, code func del]:
   1.174 +  "(1\<Colon>index) = index_of_nat 1"
   1.175  
   1.176  lemma one_index_code [code inline, code func]:
   1.177    "(1\<Colon>index) = Numeral1"
   1.178 +  by (simp add: number_of_index_def Pls_def Bit_def)
   1.179 +
   1.180 +definition [simp, code func del]:
   1.181 +  "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
   1.182 +
   1.183 +lemma plus_index_code [code func]:
   1.184 +  "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
   1.185 +  by simp
   1.186 +
   1.187 +definition [simp, code func del]:
   1.188 +  "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
   1.189 +
   1.190 +definition [simp, code func del]:
   1.191 +  "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
   1.192 +
   1.193 +lemma times_index_code [code func]:
   1.194 +  "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
   1.195    by simp
   1.196  
   1.197 -instance index :: abs
   1.198 -  "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" ..
   1.199 +definition [simp, code func del]:
   1.200 +  "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
   1.201  
   1.202 -lemma index_of_int [code func]:
   1.203 -  "index_of_int k = (if k = 0 then 0
   1.204 -    else if k = -1 then -1
   1.205 -    else let (l, m) = divAlg (k, 2) in 2 * index_of_int l +
   1.206 -      (if m = 0 then 0 else 1))"
   1.207 -  by (simp add: number_of_index_shift Let_def split_def divAlg_mod_div) arith
   1.208 +definition [simp, code func del]:
   1.209 +  "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
   1.210  
   1.211 -lemma int_of_index [code func]:
   1.212 -  "int_of_index k = (if k = 0 then 0
   1.213 -    else if k = -1 then -1
   1.214 -    else let l = k div 2; m = k mod 2 in 2 * int_of_index l +
   1.215 -      (if m = 0 then 0 else 1))"
   1.216 -  by (auto simp add: number_of_index_shift Let_def split_def) arith
   1.217 +lemma div_index_code [code func]:
   1.218 +  "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
   1.219 +  by simp
   1.220  
   1.221 -
   1.222 -subsection {* Conversion to and from @{typ nat} *}
   1.223 -
   1.224 -definition
   1.225 -  nat_of_index :: "index \<Rightarrow> nat"
   1.226 -where
   1.227 -  [code func del]: "nat_of_index = nat o int_of_index"
   1.228 +lemma mod_index_code [code func]:
   1.229 +  "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
   1.230 +  by simp
   1.231  
   1.232 -definition
   1.233 -  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   1.234 -  [code func del]: "nat_of_index_aux i n = nat_of_index i + n"
   1.235 +definition [simp, code func del]:
   1.236 +  "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
   1.237  
   1.238 -lemma nat_of_index_aux_code [code]:
   1.239 -  "nat_of_index_aux i n = (if i \<le> 0 then n else nat_of_index_aux (i - 1) (Suc n))"
   1.240 -  by (auto simp add: nat_of_index_aux_def nat_of_index_def)
   1.241 -
   1.242 -lemma nat_of_index_code [code]:
   1.243 -  "nat_of_index i = nat_of_index_aux i 0"
   1.244 -  by (simp add: nat_of_index_aux_def)
   1.245 +definition [simp, code func del]:
   1.246 +  "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
   1.247  
   1.248 -definition
   1.249 -  index_of_nat :: "nat \<Rightarrow> index"
   1.250 -where
   1.251 -  [code func del]: "index_of_nat = index_of_int o of_nat"
   1.252 +lemma less_eq_index_code [code func]:
   1.253 +  "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
   1.254 +  by simp
   1.255  
   1.256 -lemma index_of_nat [code func]:
   1.257 -  "index_of_nat 0 = 0"
   1.258 -  "index_of_nat (Suc n) = index_of_nat n + 1"
   1.259 -  unfolding index_of_nat_def by simp_all
   1.260 +lemma less_index_code [code func]:
   1.261 +  "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
   1.262 +  by simp
   1.263  
   1.264 -lemma index_nat_id [simp]:
   1.265 -  "nat_of_index (index_of_nat n) = n"
   1.266 -  "index_of_nat (nat_of_index i) = (if i \<le> 0 then 0 else i)"
   1.267 -  unfolding index_of_nat_def nat_of_index_def by simp_all
   1.268 +instance by default (auto simp add: left_distrib index)
   1.269 +
   1.270 +end
   1.271  
   1.272  
   1.273  subsection {* ML interface *}
   1.274 @@ -201,7 +140,7 @@
   1.275  structure Index =
   1.276  struct
   1.277  
   1.278 -fun mk k = @{term index_of_int} $ HOLogic.mk_number @{typ index} k;
   1.279 +fun mk k = @{term index_of_nat} $ HOLogic.mk_number @{typ index} k;
   1.280  
   1.281  end;
   1.282  *}
   1.283 @@ -209,6 +148,20 @@
   1.284  
   1.285  subsection {* Code serialization *}
   1.286  
   1.287 +text {* Pecularity for operations with potentially negative result *}
   1.288 +
   1.289 +definition
   1.290 +  minus_index' :: "index \<Rightarrow> index \<Rightarrow> index"
   1.291 +where
   1.292 +  [code func del]: "minus_index' = op -"
   1.293 +
   1.294 +lemma minus_index_code [code func]:
   1.295 +  "n - m = (let q = minus_index' n m
   1.296 +    in if q < 0 then 0 else q)"
   1.297 +  by (simp add: minus_index'_def Let_def)
   1.298 +
   1.299 +text {* Implementation of indices by bounded integers *}
   1.300 +
   1.301  code_type index
   1.302    (SML "int")
   1.303    (OCaml "int")
   1.304 @@ -234,12 +187,7 @@
   1.305    (OCaml "Pervasives.+")
   1.306    (Haskell infixl 6 "+")
   1.307  
   1.308 -code_const "uminus \<Colon> index \<Rightarrow> index"
   1.309 -  (SML "Int.~")
   1.310 -  (OCaml "Pervasives.~-")
   1.311 -  (Haskell "negate")
   1.312 -
   1.313 -code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.314 +code_const "minus_index' \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.315    (SML "Int.- ((_), (_))")
   1.316    (OCaml "Pervasives.-")
   1.317    (Haskell infixl 6 "-")
   1.318 @@ -264,6 +212,16 @@
   1.319    (OCaml "!((_ : Pervasives.int) < _)")
   1.320    (Haskell infix 4 "<")
   1.321  
   1.322 +code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.323 +  (SML "IntInf.div ((_), (_))")
   1.324 +  (OCaml "Big'_int.div'_big'_int")
   1.325 +  (Haskell "div")
   1.326 +
   1.327 +code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.328 +  (SML "IntInf.mod ((_), (_))")
   1.329 +  (OCaml "Big'_int.mod'_big'_int")
   1.330 +  (Haskell "mod")
   1.331 +
   1.332  code_reserved SML Int
   1.333  code_reserved OCaml Pervasives
   1.334  
     2.1 --- a/src/HOL/Library/Code_Integer.thy	Wed Jan 02 15:14:22 2008 +0100
     2.2 +++ b/src/HOL/Library/Code_Integer.thy	Wed Jan 02 15:14:23 2008 +0100
     2.3 @@ -88,10 +88,10 @@
     2.4    (OCaml "Big'_int.lt'_big'_int")
     2.5    (Haskell infix 4 "<")
     2.6  
     2.7 -code_const index_of_int and int_of_index
     2.8 +(*code_const index_of_int and int_of_index
     2.9    (SML "IntInf.toInt" and "IntInf.fromInt")
    2.10    (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
    2.11 -  (Haskell "_" and "_")
    2.12 +  (Haskell "_" and "_") FIXME perhaps recover this if neccessary *)
    2.13  
    2.14  code_reserved SML IntInf
    2.15  code_reserved OCaml Big_int
     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Jan 02 15:14:22 2008 +0100
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jan 02 15:14:23 2008 +0100
     3.3 @@ -165,14 +165,6 @@
     3.4    then show ?thesis unfolding int_aux_def int_of_nat_def by auto
     3.5  qed
     3.6  
     3.7 -lemma index_of_nat_code [code func, code inline]:
     3.8 -  "index_of_nat n = index_of_int (int_of_nat n)"
     3.9 -  unfolding index_of_nat_def int_of_nat_def by simp
    3.10 -
    3.11 -lemma nat_of_index_code [code func, code inline]:
    3.12 -  "nat_of_index k = nat (int_of_index k)"
    3.13 -  unfolding nat_of_index_def by simp
    3.14 -
    3.15  
    3.16  subsection {* Code generator setup for basic functions *}
    3.17  
    3.18 @@ -221,11 +213,22 @@
    3.19    (OCaml "_")
    3.20    (Haskell "_")
    3.21  
    3.22 +code_const index_of_nat
    3.23 +  (SML "_")
    3.24 +  (OCaml "_")
    3.25 +  (Haskell "_")
    3.26 +
    3.27  code_const nat_of_int
    3.28    (SML "_")
    3.29    (OCaml "_")
    3.30    (Haskell "_")
    3.31  
    3.32 +code_const nat_of_index
    3.33 +  (SML "_")
    3.34 +  (OCaml "_")
    3.35 +  (Haskell "_")
    3.36 +
    3.37 +
    3.38  text {* Using target language div and mod *}
    3.39  
    3.40  code_const "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"