1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Feb 06 09:05:19 2009 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Feb 06 09:05:19 2009 +0100
     1.3 @@ -124,47 +124,47 @@
     1.4  subsubsection {* Logical intermediate layer *}
     1.5  
     1.6  definition new' where
     1.7 -  [code del]: "new' = Array.new o nat_of_index"
     1.8 +  [code del]: "new' = Array.new o Code_Index.nat_of"
     1.9  hide (open) const new'
    1.10  lemma [code]:
    1.11 -  "Array.new = Array.new' o index_of_nat"
    1.12 +  "Array.new = Array.new' o Code_Index.of_nat"
    1.13    by (simp add: new'_def o_def)
    1.14  
    1.15  definition of_list' where
    1.16 -  [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
    1.17 +  [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
    1.18  hide (open) const of_list'
    1.19  lemma [code]:
    1.20 -  "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
    1.21 +  "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
    1.22    by (simp add: of_list'_def)
    1.23  
    1.24  definition make' where
    1.25 -  [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
    1.26 +  [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
    1.27  hide (open) const make'
    1.28  lemma [code]:
    1.29 -  "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
    1.30 +  "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
    1.31    by (simp add: make'_def o_def)
    1.32  
    1.33  definition length' where
    1.34 -  [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
    1.35 +  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
    1.36  hide (open) const length'
    1.37  lemma [code]:
    1.38 -  "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
    1.39 +  "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
    1.40    by (simp add: length'_def monad_simp',
    1.41      simp add: liftM_def comp_def monad_simp,
    1.42      simp add: monad_simp')
    1.43  
    1.44  definition nth' where
    1.45 -  [code del]: "nth' a = Array.nth a o nat_of_index"
    1.46 +  [code del]: "nth' a = Array.nth a o Code_Index.nat_of"
    1.47  hide (open) const nth'
    1.48  lemma [code]:
    1.49 -  "Array.nth a n = Array.nth' a (index_of_nat n)"
    1.50 +  "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
    1.51    by (simp add: nth'_def)
    1.52  
    1.53  definition upd' where
    1.54 -  [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
    1.55 +  [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
    1.56  hide (open) const upd'
    1.57  lemma [code]:
    1.58 -  "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
    1.59 +  "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
    1.60    by (simp add: upd'_def monad_simp upd_return)
    1.61  
    1.62  

     2.1 --- a/src/HOL/Library/Code_Index.thy	Fri Feb 06 09:05:19 2009 +0100
     2.2 +++ b/src/HOL/Library/Code_Index.thy	Fri Feb 06 09:05:19 2009 +0100
     2.3 @@ -1,6 +1,4 @@
     2.4 -(*  ID:         $Id$
     2.5 -    Author:     Florian Haftmann, TU Muenchen
     2.6 -*)
     2.7 +(* Author: Florian Haftmann, TU Muenchen *)
     2.8  
     2.9  header {* Type of indices *}
    2.10  
    2.11 @@ -15,78 +13,77 @@
    2.12  
    2.13  subsection {* Datatype of indices *}
    2.14  
    2.15 -typedef index = "UNIV \<Colon> nat set"
    2.16 -  morphisms nat_of_index index_of_nat by rule
    2.17 +typedef (open) index = "UNIV \<Colon> nat set"
    2.18 +  morphisms nat_of of_nat by rule
    2.19  
    2.20 -lemma index_of_nat_nat_of_index [simp]:
    2.21 -  "index_of_nat (nat_of_index k) = k"
    2.22 -  by (rule nat_of_index_inverse)
    2.23 +lemma of_nat_nat_of [simp]:
    2.24 +  "of_nat (nat_of k) = k"
    2.25 +  by (rule nat_of_inverse)
    2.26  
    2.27 -lemma nat_of_index_index_of_nat [simp]:
    2.28 -  "nat_of_index (index_of_nat n) = n"
    2.29 -  by (rule index_of_nat_inverse) 
    2.30 -    (unfold index_def, rule UNIV_I)
    2.31 +lemma nat_of_of_nat [simp]:
    2.32 +  "nat_of (of_nat n) = n"
    2.33 +  by (rule of_nat_inverse) (rule UNIV_I)
    2.34  
    2.35  lemma [measure_function]:
    2.36 -  "is_measure nat_of_index" by (rule is_measure_trivial)
    2.37 +  "is_measure nat_of" by (rule is_measure_trivial)
    2.38  
    2.39  lemma index:
    2.40 -  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
    2.41 +  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
    2.42  proof
    2.43    fix n :: nat
    2.44    assume "\<And>n\<Colon>index. PROP P n"
    2.45 -  then show "PROP P (index_of_nat n)" .
    2.46 +  then show "PROP P (of_nat n)" .
    2.47  next
    2.48    fix n :: index
    2.49 -  assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)"
    2.50 -  then have "PROP P (index_of_nat (nat_of_index n))" .
    2.51 +  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
    2.52 +  then have "PROP P (of_nat (nat_of n))" .
    2.53    then show "PROP P n" by simp
    2.54  qed
    2.55  
    2.56  lemma index_case:
    2.57 -  assumes "\<And>n. k = index_of_nat n \<Longrightarrow> P"
    2.58 +  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
    2.59    shows P
    2.60 -  by (rule assms [of "nat_of_index k"]) simp
    2.61 +  by (rule assms [of "nat_of k"]) simp
    2.62  
    2.63  lemma index_induct_raw:
    2.64 -  assumes "\<And>n. P (index_of_nat n)"
    2.65 +  assumes "\<And>n. P (of_nat n)"
    2.66    shows "P k"
    2.67  proof -
    2.68 -  from assms have "P (index_of_nat (nat_of_index k))" .
    2.69 +  from assms have "P (of_nat (nat_of k))" .
    2.70    then show ?thesis by simp
    2.71  qed
    2.72  
    2.73 -lemma nat_of_index_inject [simp]:
    2.74 -  "nat_of_index k = nat_of_index l \<longleftrightarrow> k = l"
    2.75 -  by (rule nat_of_index_inject)
    2.76 +lemma nat_of_inject [simp]:
    2.77 +  "nat_of k = nat_of l \<longleftrightarrow> k = l"
    2.78 +  by (rule nat_of_inject)
    2.79  
    2.80 -lemma index_of_nat_inject [simp]:
    2.81 -  "index_of_nat n = index_of_nat m \<longleftrightarrow> n = m"
    2.82 -  by (auto intro!: index_of_nat_inject simp add: index_def)
    2.83 +lemma of_nat_inject [simp]:
    2.84 +  "of_nat n = of_nat m \<longleftrightarrow> n = m"
    2.85 +  by (rule of_nat_inject) (rule UNIV_I)+
    2.86  
    2.87  instantiation index :: zero
    2.88  begin
    2.89  
    2.90  definition [simp, code del]:
    2.91 -  "0 = index_of_nat 0"
    2.92 +  "0 = of_nat 0"
    2.93  
    2.94  instance ..
    2.95  
    2.96  end
    2.97  
    2.98  definition [simp]:
    2.99 -  "Suc_index k = index_of_nat (Suc (nat_of_index k))"
   2.100 +  "Suc_index k = of_nat (Suc (nat_of k))"
   2.101  
   2.102  rep_datatype "0 \<Colon> index" Suc_index
   2.103  proof -
   2.104    fix P :: "index \<Rightarrow> bool"
   2.105    fix k :: index
   2.106 -  assume "P 0" then have init: "P (index_of_nat 0)" by simp
   2.107 +  assume "P 0" then have init: "P (of_nat 0)" by simp
   2.108    assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
   2.109 -    then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" .
   2.110 -    then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp
   2.111 -  from init step have "P (index_of_nat (nat_of_index k))"
   2.112 -    by (induct "nat_of_index k") simp_all
   2.113 +    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
   2.114 +    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
   2.115 +  from init step have "P (of_nat (nat_of k))"
   2.116 +    by (induct "nat_of k") simp_all
   2.117    then show "P k" by simp
   2.118  qed simp_all
   2.119  
   2.120 @@ -96,25 +93,25 @@
   2.121  declare index.induct [case_names nat, induct type: index]
   2.122  
   2.123  lemma [code]:
   2.124 -  "index_size = nat_of_index"
   2.125 +  "index_size = nat_of"
   2.126  proof (rule ext)
   2.127    fix k
   2.128 -  have "index_size k = nat_size (nat_of_index k)"
   2.129 +  have "index_size k = nat_size (nat_of k)"
   2.130      by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
   2.131 -  also have "nat_size (nat_of_index k) = nat_of_index k" by (induct "nat_of_index k") simp_all
   2.132 -  finally show "index_size k = nat_of_index k" .
   2.133 +  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
   2.134 +  finally show "index_size k = nat_of k" .
   2.135  qed
   2.136  
   2.137  lemma [code]:
   2.138 -  "size = nat_of_index"
   2.139 +  "size = nat_of"
   2.140  proof (rule ext)
   2.141    fix k
   2.142 -  show "size k = nat_of_index k"
   2.143 +  show "size k = nat_of k"
   2.144    by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
   2.145  qed
   2.146  
   2.147  lemma [code]:
   2.148 -  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
   2.149 +  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
   2.150    by (cases k, cases l) (simp add: eq)
   2.151  
   2.152  lemma [code nbe]:
   2.153 @@ -128,14 +125,14 @@
   2.154  begin
   2.155  
   2.156  definition
   2.157 -  "number_of = index_of_nat o nat"
   2.158 +  "number_of = of_nat o nat"
   2.159  
   2.160  instance ..
   2.161  
   2.162  end
   2.163  
   2.164 -lemma nat_of_index_number [simp]:
   2.165 -  "nat_of_index (number_of k) = number_of k"
   2.166 +lemma nat_of_number [simp]:
   2.167 +  "nat_of (number_of k) = number_of k"
   2.168    by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
   2.169  
   2.170  code_datatype "number_of \<Colon> int \<Rightarrow> index"
   2.171 @@ -147,30 +144,31 @@
   2.172  begin
   2.173  
   2.174  definition [simp, code del]:
   2.175 -  "(1\<Colon>index) = index_of_nat 1"
   2.176 +  "(1\<Colon>index) = of_nat 1"
   2.177  
   2.178  definition [simp, code del]:
   2.179 -  "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
   2.180 +  "n + m = of_nat (nat_of n + nat_of m)"
   2.181  
   2.182  definition [simp, code del]:
   2.183 -  "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
   2.184 +  "n - m = of_nat (nat_of n - nat_of m)"
   2.185  
   2.186  definition [simp, code del]:
   2.187 -  "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
   2.188 +  "n * m = of_nat (nat_of n * nat_of m)"
   2.189  
   2.190  definition [simp, code del]:
   2.191 -  "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
   2.192 +  "n div m = of_nat (nat_of n div nat_of m)"
   2.193  
   2.194  definition [simp, code del]:
   2.195 -  "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
   2.196 +  "n mod m = of_nat (nat_of n mod nat_of m)"
   2.197  
   2.198  definition [simp, code del]:
   2.199 -  "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
   2.200 +  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
   2.201  
   2.202  definition [simp, code del]:
   2.203 -  "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
   2.204 +  "n < m \<longleftrightarrow> nat_of n < nat_of m"
   2.205  
   2.206 -instance by default (auto simp add: left_distrib index)
   2.207 +instance proof
   2.208 +qed (auto simp add: left_distrib)
   2.209  
   2.210  end
   2.211  
   2.212 @@ -187,14 +185,14 @@
   2.213    using one_index_code ..
   2.214  
   2.215  lemma plus_index_code [code nbe]:
   2.216 -  "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
   2.217 +  "of_nat n + of_nat m = of_nat (n + m)"
   2.218    by simp
   2.219  
   2.220  definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
   2.221    [simp, code del]: "subtract_index = op -"
   2.222  
   2.223  lemma subtract_index_code [code nbe]:
   2.224 -  "subtract_index (index_of_nat n) (index_of_nat m) = index_of_nat (n - m)"
   2.225 +  "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
   2.226    by simp
   2.227  
   2.228  lemma minus_index_code [code]:
   2.229 @@ -202,42 +200,42 @@
   2.230    by simp
   2.231  
   2.232  lemma times_index_code [code nbe]:
   2.233 -  "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
   2.234 +  "of_nat n * of_nat m = of_nat (n * m)"
   2.235    by simp
   2.236  
   2.237  lemma less_eq_index_code [code nbe]:
   2.238 -  "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
   2.239 +  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
   2.240    by simp
   2.241  
   2.242  lemma less_index_code [code nbe]:
   2.243 -  "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
   2.244 +  "of_nat n < of_nat m \<longleftrightarrow> n < m"
   2.245    by simp
   2.246  
   2.247  lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
   2.248  
   2.249 -lemma index_of_nat_code [code]:
   2.250 -  "index_of_nat = of_nat"
   2.251 +lemma of_nat_code [code]:
   2.252 +  "of_nat = Nat.of_nat"
   2.253  proof
   2.254    fix n :: nat
   2.255 -  have "of_nat n = index_of_nat n"
   2.256 +  have "Nat.of_nat n = of_nat n"
   2.257      by (induct n) simp_all
   2.258 -  then show "index_of_nat n = of_nat n"
   2.259 +  then show "of_nat n = Nat.of_nat n"
   2.260      by (rule sym)
   2.261  qed
   2.262  
   2.263 -lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
   2.264 +lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
   2.265    by (cases i) auto
   2.266  
   2.267 -definition nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   2.268 -  "nat_of_index_aux i n = nat_of_index i + n"
   2.269 +definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   2.270 +  "nat_of_aux i n = nat_of i + n"
   2.271  
   2.272 -lemma nat_of_index_aux_code [code]:
   2.273 -  "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))"
   2.274 -  by (auto simp add: nat_of_index_aux_def index_not_eq_zero)
   2.275 +lemma nat_of_aux_code [code]:
   2.276 +  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
   2.277 +  by (auto simp add: nat_of_aux_def index_not_eq_zero)
   2.278  
   2.279 -lemma nat_of_index_code [code]:
   2.280 -  "nat_of_index i = nat_of_index_aux i 0"
   2.281 -  by (simp add: nat_of_index_aux_def)
   2.282 +lemma nat_of_code [code]:
   2.283 +  "nat_of i = nat_of_aux i 0"
   2.284 +  by (simp add: nat_of_aux_def)
   2.285  
   2.286  definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
   2.287    [code del]: "div_mod_index n m = (n div m, n mod m)"
   2.288 @@ -254,6 +252,7 @@
   2.289    "n mod m = snd (div_mod_index n m)"
   2.290    unfolding div_mod_index_def by simp
   2.291  
   2.292 +hide (open) const of_nat nat_of
   2.293  
   2.294  subsection {* ML interface *}
   2.295  

     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Feb 06 09:05:19 2009 +0100
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Feb 06 09:05:19 2009 +0100
     3.3 @@ -376,12 +376,12 @@
     3.4  
     3.5  text {* Conversion from and to indices. *}
     3.6  
     3.7 -code_const index_of_nat
     3.8 +code_const Code_Index.of_nat
     3.9    (SML "IntInf.toInt")
    3.10    (OCaml "Big'_int.int'_of'_big'_int")
    3.11    (Haskell "fromEnum")
    3.12  
    3.13 -code_const nat_of_index
    3.14 +code_const Code_Index.nat_of
    3.15    (SML "IntInf.fromInt")
    3.16    (OCaml "Big'_int.big'_int'_of'_int")
    3.17    (Haskell "toEnum")

     4.1 --- a/src/HOL/Library/Random.thy	Fri Feb 06 09:05:19 2009 +0100
     4.2 +++ b/src/HOL/Library/Random.thy	Fri Feb 06 09:05:19 2009 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4 -(*  Author:     Florian Haftmann, TU Muenchen
     4.5 -*)
     4.6 +(* Author: Florian Haftmann, TU Muenchen *)
     4.7  
     4.8  header {* A HOL random engine *}
     4.9  
    4.10 @@ -77,7 +76,7 @@
    4.11    in range_aux (k - 1) (v + l * 2147483561) s')"
    4.12  by pat_completeness auto
    4.13  termination
    4.14 -  by (relation "measure (nat_of_index o fst)")
    4.15 +  by (relation "measure (Code_Index.nat_of o fst)")
    4.16      (auto simp add: index)
    4.17  
    4.18  definition
    4.19 @@ -103,19 +102,19 @@
    4.20    select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
    4.21  where
    4.22    "select xs = (do
    4.23 -     k \<leftarrow> range (index_of_nat (length xs));
    4.24 -     return (nth xs (nat_of_index k))
    4.25 +     k \<leftarrow> range (Code_Index.of_nat (length xs));
    4.26 +     return (nth xs (Code_Index.nat_of k))
    4.27     done)"
    4.28  
    4.29  lemma select:
    4.30    assumes "xs \<noteq> []"
    4.31    shows "fst (select xs s) \<in> set xs"
    4.32  proof -
    4.33 -  from assms have "index_of_nat (length xs) > 0" by simp
    4.34 +  from assms have "Code_Index.of_nat (length xs) > 0" by simp
    4.35    with range have
    4.36 -    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
    4.37 +    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
    4.38    then have
    4.39 -    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
    4.40 +    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
    4.41    then show ?thesis
    4.42      by (auto simp add: monad_collapse select_def)
    4.43  qed