String.literal replaces message_string, code_numeral replaces (code_)index
authorhaftmann
Tue May 19 16:54:55 2009 +0200 (2009-05-19 ago)
changeset 3120598370b26c2ce
parent 31204 46c0c741c8c2
child 31206 a9fa62683582
String.literal replaces message_string, code_numeral replaces (code_)index
doc-src/Codegen/Thy/Adaptation.thy
src/HOL/Code_Eval.thy
src/HOL/Code_Index.thy
src/HOL/Code_Numeral.thy
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/IsaMakefile
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Quickcheck.thy
src/HOL/Random.thy
src/HOL/Rational.thy
src/HOL/String.thy
src/HOL/Tools/hologic.ML
src/HOL/Tools/string_code.ML
src/HOL/Typerep.thy
     1.1 --- a/doc-src/Codegen/Thy/Adaptation.thy	Tue May 19 13:57:51 2009 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Adaptation.thy	Tue May 19 16:54:55 2009 +0200
     1.3 @@ -127,8 +127,8 @@
     1.4         Useful for code setups which involve e.g. indexing of
     1.5         target-language arrays.
     1.6      \item[@{theory "String"}] provides an additional datatype
     1.7 -       @{typ message_string} which is isomorphic to strings;
     1.8 -       @{typ message_string}s are mapped to target-language strings.
     1.9 +       @{typ String.literal} which is isomorphic to strings;
    1.10 +       @{typ String.literal}s are mapped to target-language strings.
    1.11         Useful for code setups which involve e.g. printing (error) messages.
    1.12  
    1.13    \end{description}
     2.1 --- a/src/HOL/Code_Eval.thy	Tue May 19 13:57:51 2009 +0200
     2.2 +++ b/src/HOL/Code_Eval.thy	Tue May 19 16:54:55 2009 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Term evaluation using the generic code generator *}
     2.5  
     2.6  theory Code_Eval
     2.7 -imports Plain Typerep Code_Index
     2.8 +imports Plain Typerep Code_Numeral
     2.9  begin
    2.10  
    2.11  subsection {* Term representation *}
    2.12 @@ -14,7 +14,7 @@
    2.13  
    2.14  datatype "term" = dummy_term
    2.15  
    2.16 -definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
    2.17 +definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    2.18    "Const _ _ = dummy_term"
    2.19  
    2.20  definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
    2.21 @@ -63,10 +63,7 @@
    2.22      let
    2.23        val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    2.24          andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    2.25 -    in
    2.26 -      thy
    2.27 -      |> need_inst ? add_term_of tyco raw_vs
    2.28 -    end;
    2.29 +    in if need_inst then add_term_of tyco raw_vs thy else thy end;
    2.30  in
    2.31    Code.type_interpretation ensure_term_of
    2.32  end
    2.33 @@ -102,10 +99,7 @@
    2.34    fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
    2.35      let
    2.36        val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    2.37 -    in
    2.38 -      thy
    2.39 -      |> has_inst ? add_term_of_code tyco raw_vs cs
    2.40 -    end;
    2.41 +    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
    2.42  in
    2.43    Code.type_interpretation ensure_term_of_code
    2.44  end
    2.45 @@ -119,7 +113,7 @@
    2.46  
    2.47  lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
    2.48  lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
    2.49 -lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
    2.50 +lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
    2.51  lemma [code, code del]:
    2.52    "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
    2.53  lemma [code, code del]:
    2.54 @@ -137,7 +131,7 @@
    2.55  code_const Const and App
    2.56    (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
    2.57  
    2.58 -code_const "term_of \<Colon> message_string \<Rightarrow> term"
    2.59 +code_const "term_of \<Colon> String.literal \<Rightarrow> term"
    2.60    (Eval "HOLogic.mk'_message'_string")
    2.61  
    2.62  code_reserved Eval HOLogic
    2.63 @@ -215,8 +209,8 @@
    2.64        else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
    2.65    by (simp only: term_of_anything)
    2.66  
    2.67 -lemma (in term_syntax) term_of_index_code [code]:
    2.68 -  "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
    2.69 +lemma (in term_syntax) term_of_code_numeral_code [code]:
    2.70 +  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
    2.71    by (simp only: term_of_anything)
    2.72  
    2.73  subsection {* Obfuscate *}
     3.1 --- a/src/HOL/Code_Index.thy	Tue May 19 13:57:51 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,325 +0,0 @@
     3.4 -(* Author: Florian Haftmann, TU Muenchen *)
     3.5 -
     3.6 -header {* Type of indices *}
     3.7 -
     3.8 -theory Code_Index
     3.9 -imports Nat_Numeral
    3.10 -begin
    3.11 -
    3.12 -text {*
    3.13 -  Indices are isomorphic to HOL @{typ nat} but
    3.14 -  mapped to target-language builtin integers.
    3.15 -*}
    3.16 -
    3.17 -subsection {* Datatype of indices *}
    3.18 -
    3.19 -typedef (open) index = "UNIV \<Colon> nat set"
    3.20 -  morphisms nat_of of_nat by rule
    3.21 -
    3.22 -lemma of_nat_nat_of [simp]:
    3.23 -  "of_nat (nat_of k) = k"
    3.24 -  by (rule nat_of_inverse)
    3.25 -
    3.26 -lemma nat_of_of_nat [simp]:
    3.27 -  "nat_of (of_nat n) = n"
    3.28 -  by (rule of_nat_inverse) (rule UNIV_I)
    3.29 -
    3.30 -lemma [measure_function]:
    3.31 -  "is_measure nat_of" by (rule is_measure_trivial)
    3.32 -
    3.33 -lemma index:
    3.34 -  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
    3.35 -proof
    3.36 -  fix n :: nat
    3.37 -  assume "\<And>n\<Colon>index. PROP P n"
    3.38 -  then show "PROP P (of_nat n)" .
    3.39 -next
    3.40 -  fix n :: index
    3.41 -  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
    3.42 -  then have "PROP P (of_nat (nat_of n))" .
    3.43 -  then show "PROP P n" by simp
    3.44 -qed
    3.45 -
    3.46 -lemma index_case:
    3.47 -  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
    3.48 -  shows P
    3.49 -  by (rule assms [of "nat_of k"]) simp
    3.50 -
    3.51 -lemma index_induct_raw:
    3.52 -  assumes "\<And>n. P (of_nat n)"
    3.53 -  shows "P k"
    3.54 -proof -
    3.55 -  from assms have "P (of_nat (nat_of k))" .
    3.56 -  then show ?thesis by simp
    3.57 -qed
    3.58 -
    3.59 -lemma nat_of_inject [simp]:
    3.60 -  "nat_of k = nat_of l \<longleftrightarrow> k = l"
    3.61 -  by (rule nat_of_inject)
    3.62 -
    3.63 -lemma of_nat_inject [simp]:
    3.64 -  "of_nat n = of_nat m \<longleftrightarrow> n = m"
    3.65 -  by (rule of_nat_inject) (rule UNIV_I)+
    3.66 -
    3.67 -instantiation index :: zero
    3.68 -begin
    3.69 -
    3.70 -definition [simp, code del]:
    3.71 -  "0 = of_nat 0"
    3.72 -
    3.73 -instance ..
    3.74 -
    3.75 -end
    3.76 -
    3.77 -definition [simp]:
    3.78 -  "Suc_index k = of_nat (Suc (nat_of k))"
    3.79 -
    3.80 -rep_datatype "0 \<Colon> index" Suc_index
    3.81 -proof -
    3.82 -  fix P :: "index \<Rightarrow> bool"
    3.83 -  fix k :: index
    3.84 -  assume "P 0" then have init: "P (of_nat 0)" by simp
    3.85 -  assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
    3.86 -    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
    3.87 -    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
    3.88 -  from init step have "P (of_nat (nat_of k))"
    3.89 -    by (induct "nat_of k") simp_all
    3.90 -  then show "P k" by simp
    3.91 -qed simp_all
    3.92 -
    3.93 -declare index_case [case_names nat, cases type: index]
    3.94 -declare index.induct [case_names nat, induct type: index]
    3.95 -
    3.96 -lemma index_decr [termination_simp]:
    3.97 -  "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
    3.98 -  by (cases k) simp
    3.99 -
   3.100 -lemma [simp, code]:
   3.101 -  "index_size = nat_of"
   3.102 -proof (rule ext)
   3.103 -  fix k
   3.104 -  have "index_size k = nat_size (nat_of k)"
   3.105 -    by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
   3.106 -  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
   3.107 -  finally show "index_size k = nat_of k" .
   3.108 -qed
   3.109 -
   3.110 -lemma [simp, code]:
   3.111 -  "size = nat_of"
   3.112 -proof (rule ext)
   3.113 -  fix k
   3.114 -  show "size k = nat_of k"
   3.115 -  by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
   3.116 -qed
   3.117 -
   3.118 -lemmas [code del] = index.recs index.cases
   3.119 -
   3.120 -lemma [code]:
   3.121 -  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
   3.122 -  by (cases k, cases l) (simp add: eq)
   3.123 -
   3.124 -lemma [code nbe]:
   3.125 -  "eq_class.eq (k::index) k \<longleftrightarrow> True"
   3.126 -  by (rule HOL.eq_refl)
   3.127 -
   3.128 -
   3.129 -subsection {* Indices as datatype of ints *}
   3.130 -
   3.131 -instantiation index :: number
   3.132 -begin
   3.133 -
   3.134 -definition
   3.135 -  "number_of = of_nat o nat"
   3.136 -
   3.137 -instance ..
   3.138 -
   3.139 -end
   3.140 -
   3.141 -lemma nat_of_number [simp]:
   3.142 -  "nat_of (number_of k) = number_of k"
   3.143 -  by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
   3.144 -
   3.145 -code_datatype "number_of \<Colon> int \<Rightarrow> index"
   3.146 -
   3.147 -
   3.148 -subsection {* Basic arithmetic *}
   3.149 -
   3.150 -instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
   3.151 -begin
   3.152 -
   3.153 -definition [simp, code del]:
   3.154 -  "(1\<Colon>index) = of_nat 1"
   3.155 -
   3.156 -definition [simp, code del]:
   3.157 -  "n + m = of_nat (nat_of n + nat_of m)"
   3.158 -
   3.159 -definition [simp, code del]:
   3.160 -  "n - m = of_nat (nat_of n - nat_of m)"
   3.161 -
   3.162 -definition [simp, code del]:
   3.163 -  "n * m = of_nat (nat_of n * nat_of m)"
   3.164 -
   3.165 -definition [simp, code del]:
   3.166 -  "n div m = of_nat (nat_of n div nat_of m)"
   3.167 -
   3.168 -definition [simp, code del]:
   3.169 -  "n mod m = of_nat (nat_of n mod nat_of m)"
   3.170 -
   3.171 -definition [simp, code del]:
   3.172 -  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
   3.173 -
   3.174 -definition [simp, code del]:
   3.175 -  "n < m \<longleftrightarrow> nat_of n < nat_of m"
   3.176 -
   3.177 -instance proof
   3.178 -qed (auto simp add: index left_distrib div_mult_self1)
   3.179 -
   3.180 -end
   3.181 -
   3.182 -lemma zero_index_code [code inline, code]:
   3.183 -  "(0\<Colon>index) = Numeral0"
   3.184 -  by (simp add: number_of_index_def Pls_def)
   3.185 -lemma [code post]: "Numeral0 = (0\<Colon>index)"
   3.186 -  using zero_index_code ..
   3.187 -
   3.188 -lemma one_index_code [code inline, code]:
   3.189 -  "(1\<Colon>index) = Numeral1"
   3.190 -  by (simp add: number_of_index_def Pls_def Bit1_def)
   3.191 -lemma [code post]: "Numeral1 = (1\<Colon>index)"
   3.192 -  using one_index_code ..
   3.193 -
   3.194 -lemma plus_index_code [code nbe]:
   3.195 -  "of_nat n + of_nat m = of_nat (n + m)"
   3.196 -  by simp
   3.197 -
   3.198 -definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
   3.199 -  [simp, code del]: "subtract_index = op -"
   3.200 -
   3.201 -lemma subtract_index_code [code nbe]:
   3.202 -  "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
   3.203 -  by simp
   3.204 -
   3.205 -lemma minus_index_code [code]:
   3.206 -  "n - m = subtract_index n m"
   3.207 -  by simp
   3.208 -
   3.209 -lemma times_index_code [code nbe]:
   3.210 -  "of_nat n * of_nat m = of_nat (n * m)"
   3.211 -  by simp
   3.212 -
   3.213 -lemma less_eq_index_code [code nbe]:
   3.214 -  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
   3.215 -  by simp
   3.216 -
   3.217 -lemma less_index_code [code nbe]:
   3.218 -  "of_nat n < of_nat m \<longleftrightarrow> n < m"
   3.219 -  by simp
   3.220 -
   3.221 -lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
   3.222 -
   3.223 -lemma of_nat_code [code]:
   3.224 -  "of_nat = Nat.of_nat"
   3.225 -proof
   3.226 -  fix n :: nat
   3.227 -  have "Nat.of_nat n = of_nat n"
   3.228 -    by (induct n) simp_all
   3.229 -  then show "of_nat n = Nat.of_nat n"
   3.230 -    by (rule sym)
   3.231 -qed
   3.232 -
   3.233 -lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
   3.234 -  by (cases i) auto
   3.235 -
   3.236 -definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   3.237 -  "nat_of_aux i n = nat_of i + n"
   3.238 -
   3.239 -lemma nat_of_aux_code [code]:
   3.240 -  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
   3.241 -  by (auto simp add: nat_of_aux_def index_not_eq_zero)
   3.242 -
   3.243 -lemma nat_of_code [code]:
   3.244 -  "nat_of i = nat_of_aux i 0"
   3.245 -  by (simp add: nat_of_aux_def)
   3.246 -
   3.247 -definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
   3.248 -  [code del]: "div_mod_index n m = (n div m, n mod m)"
   3.249 -
   3.250 -lemma [code]:
   3.251 -  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   3.252 -  unfolding div_mod_index_def by auto
   3.253 -
   3.254 -lemma [code]:
   3.255 -  "n div m = fst (div_mod_index n m)"
   3.256 -  unfolding div_mod_index_def by simp
   3.257 -
   3.258 -lemma [code]:
   3.259 -  "n mod m = snd (div_mod_index n m)"
   3.260 -  unfolding div_mod_index_def by simp
   3.261 -
   3.262 -definition int_of :: "index \<Rightarrow> int" where
   3.263 -  "int_of = Nat.of_nat o nat_of"
   3.264 -
   3.265 -lemma int_of_code [code]:
   3.266 -  "int_of k = (if k = 0 then 0
   3.267 -    else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
   3.268 -  by (auto simp add: int_of_def mod_div_equality')
   3.269 -
   3.270 -hide (open) const of_nat nat_of int_of
   3.271 -
   3.272 -
   3.273 -subsection {* Code generator setup *}
   3.274 -
   3.275 -text {* Implementation of indices by bounded integers *}
   3.276 -
   3.277 -code_type index
   3.278 -  (SML "int")
   3.279 -  (OCaml "int")
   3.280 -  (Haskell "Int")
   3.281 -
   3.282 -code_instance index :: eq
   3.283 -  (Haskell -)
   3.284 -
   3.285 -setup {*
   3.286 -  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
   3.287 -    false false) ["SML", "OCaml", "Haskell"]
   3.288 -*}
   3.289 -
   3.290 -code_reserved SML Int int
   3.291 -code_reserved OCaml Pervasives int
   3.292 -
   3.293 -code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   3.294 -  (SML "Int.+/ ((_),/ (_))")
   3.295 -  (OCaml "Pervasives.( + )")
   3.296 -  (Haskell infixl 6 "+")
   3.297 -
   3.298 -code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   3.299 -  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   3.300 -  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   3.301 -  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
   3.302 -
   3.303 -code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   3.304 -  (SML "Int.*/ ((_),/ (_))")
   3.305 -  (OCaml "Pervasives.( * )")
   3.306 -  (Haskell infixl 7 "*")
   3.307 -
   3.308 -code_const div_mod_index
   3.309 -  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
   3.310 -  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
   3.311 -  (Haskell "divMod")
   3.312 -
   3.313 -code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   3.314 -  (SML "!((_ : Int.int) = _)")
   3.315 -  (OCaml "!((_ : int) = _)")
   3.316 -  (Haskell infixl 4 "==")
   3.317 -
   3.318 -code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   3.319 -  (SML "Int.<=/ ((_),/ (_))")
   3.320 -  (OCaml "!((_ : int) <= _)")
   3.321 -  (Haskell infix 4 "<=")
   3.322 -
   3.323 -code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   3.324 -  (SML "Int.</ ((_),/ (_))")
   3.325 -  (OCaml "!((_ : int) < _)")
   3.326 -  (Haskell infix 4 "<")
   3.327 -
   3.328 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Code_Numeral.thy	Tue May 19 16:54:55 2009 +0200
     4.3 @@ -0,0 +1,325 @@
     4.4 +(* Author: Florian Haftmann, TU Muenchen *)
     4.5 +
     4.6 +header {* Type of target language numerals *}
     4.7 +
     4.8 +theory Code_Numeral
     4.9 +imports Nat_Numeral
    4.10 +begin
    4.11 +
    4.12 +text {*
    4.13 +  Code numerals are isomorphic to HOL @{typ nat} but
    4.14 +  mapped to target-language builtin numerals.
    4.15 +*}
    4.16 +
    4.17 +subsection {* Datatype of target language numerals *}
    4.18 +
    4.19 +typedef (open) code_numeral = "UNIV \<Colon> nat set"
    4.20 +  morphisms nat_of of_nat by rule
    4.21 +
    4.22 +lemma of_nat_nat_of [simp]:
    4.23 +  "of_nat (nat_of k) = k"
    4.24 +  by (rule nat_of_inverse)
    4.25 +
    4.26 +lemma nat_of_of_nat [simp]:
    4.27 +  "nat_of (of_nat n) = n"
    4.28 +  by (rule of_nat_inverse) (rule UNIV_I)
    4.29 +
    4.30 +lemma [measure_function]:
    4.31 +  "is_measure nat_of" by (rule is_measure_trivial)
    4.32 +
    4.33 +lemma code_numeral:
    4.34 +  "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
    4.35 +proof
    4.36 +  fix n :: nat
    4.37 +  assume "\<And>n\<Colon>code_numeral. PROP P n"
    4.38 +  then show "PROP P (of_nat n)" .
    4.39 +next
    4.40 +  fix n :: code_numeral
    4.41 +  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
    4.42 +  then have "PROP P (of_nat (nat_of n))" .
    4.43 +  then show "PROP P n" by simp
    4.44 +qed
    4.45 +
    4.46 +lemma code_numeral_case:
    4.47 +  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
    4.48 +  shows P
    4.49 +  by (rule assms [of "nat_of k"]) simp
    4.50 +
    4.51 +lemma code_numeral_induct_raw:
    4.52 +  assumes "\<And>n. P (of_nat n)"
    4.53 +  shows "P k"
    4.54 +proof -
    4.55 +  from assms have "P (of_nat (nat_of k))" .
    4.56 +  then show ?thesis by simp
    4.57 +qed
    4.58 +
    4.59 +lemma nat_of_inject [simp]:
    4.60 +  "nat_of k = nat_of l \<longleftrightarrow> k = l"
    4.61 +  by (rule nat_of_inject)
    4.62 +
    4.63 +lemma of_nat_inject [simp]:
    4.64 +  "of_nat n = of_nat m \<longleftrightarrow> n = m"
    4.65 +  by (rule of_nat_inject) (rule UNIV_I)+
    4.66 +
    4.67 +instantiation code_numeral :: zero
    4.68 +begin
    4.69 +
    4.70 +definition [simp, code del]:
    4.71 +  "0 = of_nat 0"
    4.72 +
    4.73 +instance ..
    4.74 +
    4.75 +end
    4.76 +
    4.77 +definition [simp]:
    4.78 +  "Suc_code_numeral k = of_nat (Suc (nat_of k))"
    4.79 +
    4.80 +rep_datatype "0 \<Colon> code_numeral" Suc_code_numeral
    4.81 +proof -
    4.82 +  fix P :: "code_numeral \<Rightarrow> bool"
    4.83 +  fix k :: code_numeral
    4.84 +  assume "P 0" then have init: "P (of_nat 0)" by simp
    4.85 +  assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
    4.86 +    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
    4.87 +    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
    4.88 +  from init step have "P (of_nat (nat_of k))"
    4.89 +    by (induct "nat_of k") simp_all
    4.90 +  then show "P k" by simp
    4.91 +qed simp_all
    4.92 +
    4.93 +declare code_numeral_case [case_names nat, cases type: code_numeral]
    4.94 +declare code_numeral.induct [case_names nat, induct type: code_numeral]
    4.95 +
    4.96 +lemma code_numeral_decr [termination_simp]:
    4.97 +  "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Suc 0 < nat_of k"
    4.98 +  by (cases k) simp
    4.99 +
   4.100 +lemma [simp, code]:
   4.101 +  "code_numeral_size = nat_of"
   4.102 +proof (rule ext)
   4.103 +  fix k
   4.104 +  have "code_numeral_size k = nat_size (nat_of k)"
   4.105 +    by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
   4.106 +  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
   4.107 +  finally show "code_numeral_size k = nat_of k" .
   4.108 +qed
   4.109 +
   4.110 +lemma [simp, code]:
   4.111 +  "size = nat_of"
   4.112 +proof (rule ext)
   4.113 +  fix k
   4.114 +  show "size k = nat_of k"
   4.115 +  by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
   4.116 +qed
   4.117 +
   4.118 +lemmas [code del] = code_numeral.recs code_numeral.cases
   4.119 +
   4.120 +lemma [code]:
   4.121 +  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
   4.122 +  by (cases k, cases l) (simp add: eq)
   4.123 +
   4.124 +lemma [code nbe]:
   4.125 +  "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
   4.126 +  by (rule HOL.eq_refl)
   4.127 +
   4.128 +
   4.129 +subsection {* Indices as datatype of ints *}
   4.130 +
   4.131 +instantiation code_numeral :: number
   4.132 +begin
   4.133 +
   4.134 +definition
   4.135 +  "number_of = of_nat o nat"
   4.136 +
   4.137 +instance ..
   4.138 +
   4.139 +end
   4.140 +
   4.141 +lemma nat_of_number [simp]:
   4.142 +  "nat_of (number_of k) = number_of k"
   4.143 +  by (simp add: number_of_code_numeral_def nat_number_of_def number_of_is_id)
   4.144 +
   4.145 +code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
   4.146 +
   4.147 +
   4.148 +subsection {* Basic arithmetic *}
   4.149 +
   4.150 +instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}"
   4.151 +begin
   4.152 +
   4.153 +definition [simp, code del]:
   4.154 +  "(1\<Colon>code_numeral) = of_nat 1"
   4.155 +
   4.156 +definition [simp, code del]:
   4.157 +  "n + m = of_nat (nat_of n + nat_of m)"
   4.158 +
   4.159 +definition [simp, code del]:
   4.160 +  "n - m = of_nat (nat_of n - nat_of m)"
   4.161 +
   4.162 +definition [simp, code del]:
   4.163 +  "n * m = of_nat (nat_of n * nat_of m)"
   4.164 +
   4.165 +definition [simp, code del]:
   4.166 +  "n div m = of_nat (nat_of n div nat_of m)"
   4.167 +
   4.168 +definition [simp, code del]:
   4.169 +  "n mod m = of_nat (nat_of n mod nat_of m)"
   4.170 +
   4.171 +definition [simp, code del]:
   4.172 +  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
   4.173 +
   4.174 +definition [simp, code del]:
   4.175 +  "n < m \<longleftrightarrow> nat_of n < nat_of m"
   4.176 +
   4.177 +instance proof
   4.178 +qed (auto simp add: code_numeral left_distrib div_mult_self1)
   4.179 +
   4.180 +end
   4.181 +
   4.182 +lemma zero_code_numeral_code [code inline, code]:
   4.183 +  "(0\<Colon>code_numeral) = Numeral0"
   4.184 +  by (simp add: number_of_code_numeral_def Pls_def)
   4.185 +lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
   4.186 +  using zero_code_numeral_code ..
   4.187 +
   4.188 +lemma one_code_numeral_code [code inline, code]:
   4.189 +  "(1\<Colon>code_numeral) = Numeral1"
   4.190 +  by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
   4.191 +lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
   4.192 +  using one_code_numeral_code ..
   4.193 +
   4.194 +lemma plus_code_numeral_code [code nbe]:
   4.195 +  "of_nat n + of_nat m = of_nat (n + m)"
   4.196 +  by simp
   4.197 +
   4.198 +definition subtract_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   4.199 +  [simp, code del]: "subtract_code_numeral = op -"
   4.200 +
   4.201 +lemma subtract_code_numeral_code [code nbe]:
   4.202 +  "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)"
   4.203 +  by simp
   4.204 +
   4.205 +lemma minus_code_numeral_code [code]:
   4.206 +  "n - m = subtract_code_numeral n m"
   4.207 +  by simp
   4.208 +
   4.209 +lemma times_code_numeral_code [code nbe]:
   4.210 +  "of_nat n * of_nat m = of_nat (n * m)"
   4.211 +  by simp
   4.212 +
   4.213 +lemma less_eq_code_numeral_code [code nbe]:
   4.214 +  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
   4.215 +  by simp
   4.216 +
   4.217 +lemma less_code_numeral_code [code nbe]:
   4.218 +  "of_nat n < of_nat m \<longleftrightarrow> n < m"
   4.219 +  by simp
   4.220 +
   4.221 +lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
   4.222 +
   4.223 +lemma of_nat_code [code]:
   4.224 +  "of_nat = Nat.of_nat"
   4.225 +proof
   4.226 +  fix n :: nat
   4.227 +  have "Nat.of_nat n = of_nat n"
   4.228 +    by (induct n) simp_all
   4.229 +  then show "of_nat n = Nat.of_nat n"
   4.230 +    by (rule sym)
   4.231 +qed
   4.232 +
   4.233 +lemma code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
   4.234 +  by (cases i) auto
   4.235 +
   4.236 +definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where
   4.237 +  "nat_of_aux i n = nat_of i + n"
   4.238 +
   4.239 +lemma nat_of_aux_code [code]:
   4.240 +  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
   4.241 +  by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
   4.242 +
   4.243 +lemma nat_of_code [code]:
   4.244 +  "nat_of i = nat_of_aux i 0"
   4.245 +  by (simp add: nat_of_aux_def)
   4.246 +
   4.247 +definition div_mod_code_numeral ::  "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
   4.248 +  [code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
   4.249 +
   4.250 +lemma [code]:
   4.251 +  "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   4.252 +  unfolding div_mod_code_numeral_def by auto
   4.253 +
   4.254 +lemma [code]:
   4.255 +  "n div m = fst (div_mod_code_numeral n m)"
   4.256 +  unfolding div_mod_code_numeral_def by simp
   4.257 +
   4.258 +lemma [code]:
   4.259 +  "n mod m = snd (div_mod_code_numeral n m)"
   4.260 +  unfolding div_mod_code_numeral_def by simp
   4.261 +
   4.262 +definition int_of :: "code_numeral \<Rightarrow> int" where
   4.263 +  "int_of = Nat.of_nat o nat_of"
   4.264 +
   4.265 +lemma int_of_code [code]:
   4.266 +  "int_of k = (if k = 0 then 0
   4.267 +    else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
   4.268 +  by (auto simp add: int_of_def mod_div_equality')
   4.269 +
   4.270 +hide (open) const of_nat nat_of int_of
   4.271 +
   4.272 +
   4.273 +subsection {* Code generator setup *}
   4.274 +
   4.275 +text {* Implementation of indices by bounded integers *}
   4.276 +
   4.277 +code_type code_numeral
   4.278 +  (SML "int")
   4.279 +  (OCaml "int")
   4.280 +  (Haskell "Int")
   4.281 +
   4.282 +code_instance code_numeral :: eq
   4.283 +  (Haskell -)
   4.284 +
   4.285 +setup {*
   4.286 +  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
   4.287 +    false false) ["SML", "OCaml", "Haskell"]
   4.288 +*}
   4.289 +
   4.290 +code_reserved SML Int int
   4.291 +code_reserved OCaml Pervasives int
   4.292 +
   4.293 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   4.294 +  (SML "Int.+/ ((_),/ (_))")
   4.295 +  (OCaml "Pervasives.( + )")
   4.296 +  (Haskell infixl 6 "+")
   4.297 +
   4.298 +code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   4.299 +  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   4.300 +  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   4.301 +  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
   4.302 +
   4.303 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   4.304 +  (SML "Int.*/ ((_),/ (_))")
   4.305 +  (OCaml "Pervasives.( * )")
   4.306 +  (Haskell infixl 7 "*")
   4.307 +
   4.308 +code_const div_mod_code_numeral
   4.309 +  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
   4.310 +  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
   4.311 +  (Haskell "divMod")
   4.312 +
   4.313 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   4.314 +  (SML "!((_ : Int.int) = _)")
   4.315 +  (OCaml "!((_ : int) = _)")
   4.316 +  (Haskell infixl 4 "==")
   4.317 +
   4.318 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   4.319 +  (SML "Int.<=/ ((_),/ (_))")
   4.320 +  (OCaml "!((_ : int) <= _)")
   4.321 +  (Haskell infix 4 "<=")
   4.322 +
   4.323 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   4.324 +  (SML "Int.</ ((_),/ (_))")
   4.325 +  (OCaml "!((_ : int) < _)")
   4.326 +  (Haskell infix 4 "<")
   4.327 +
   4.328 +end
     5.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue May 19 13:57:51 2009 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue May 19 16:54:55 2009 +0200
     5.3 @@ -115,47 +115,47 @@
     5.4  subsubsection {* Logical intermediate layer *}
     5.5  
     5.6  definition new' where
     5.7 -  [code del]: "new' = Array.new o Code_Index.nat_of"
     5.8 +  [code del]: "new' = Array.new o Code_Numeral.nat_of"
     5.9  hide (open) const new'
    5.10  lemma [code]:
    5.11 -  "Array.new = Array.new' o Code_Index.of_nat"
    5.12 +  "Array.new = Array.new' o Code_Numeral.of_nat"
    5.13    by (simp add: new'_def o_def)
    5.14  
    5.15  definition of_list' where
    5.16 -  [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
    5.17 +  [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
    5.18  hide (open) const of_list'
    5.19  lemma [code]:
    5.20 -  "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
    5.21 +  "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
    5.22    by (simp add: of_list'_def)
    5.23  
    5.24  definition make' where
    5.25 -  [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
    5.26 +  [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
    5.27  hide (open) const make'
    5.28  lemma [code]:
    5.29 -  "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
    5.30 +  "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
    5.31    by (simp add: make'_def o_def)
    5.32  
    5.33  definition length' where
    5.34 -  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
    5.35 +  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
    5.36  hide (open) const length'
    5.37  lemma [code]:
    5.38 -  "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
    5.39 +  "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
    5.40    by (simp add: length'_def monad_simp',
    5.41      simp add: liftM_def comp_def monad_simp,
    5.42      simp add: monad_simp')
    5.43  
    5.44  definition nth' where
    5.45 -  [code del]: "nth' a = Array.nth a o Code_Index.nat_of"
    5.46 +  [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
    5.47  hide (open) const nth'
    5.48  lemma [code]:
    5.49 -  "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
    5.50 +  "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
    5.51    by (simp add: nth'_def)
    5.52  
    5.53  definition upd' where
    5.54 -  [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
    5.55 +  [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
    5.56  hide (open) const upd'
    5.57  lemma [code]:
    5.58 -  "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
    5.59 +  "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
    5.60    by (simp add: upd'_def monad_simp upd_return)
    5.61  
    5.62  
     6.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Tue May 19 13:57:51 2009 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Tue May 19 16:54:55 2009 +0200
     6.3 @@ -28,11 +28,11 @@
     6.4  
     6.5  instance int :: heap ..
     6.6  
     6.7 -instance message_string :: countable
     6.8 -  by (rule countable_classI [of "message_string_case to_nat"])
     6.9 -   (auto split: message_string.splits)
    6.10 +instance String.literal :: countable
    6.11 +  by (rule countable_classI [of "String.literal_case to_nat"])
    6.12 +   (auto split: String.literal.splits)
    6.13  
    6.14 -instance message_string :: heap ..
    6.15 +instance String.literal :: heap ..
    6.16  
    6.17  text {* Reflected types themselves are heap-representable *}
    6.18  
     7.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 13:57:51 2009 +0200
     7.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 16:54:55 2009 +0200
     7.3 @@ -274,7 +274,7 @@
     7.4  subsubsection {* Logical intermediate layer *}
     7.5  
     7.6  definition
     7.7 -  Fail :: "message_string \<Rightarrow> exception"
     7.8 +  Fail :: "String.literal \<Rightarrow> exception"
     7.9  where
    7.10    [code del]: "Fail s = Exn"
    7.11  
     8.1 --- a/src/HOL/IsaMakefile	Tue May 19 13:57:51 2009 +0200
     8.2 +++ b/src/HOL/IsaMakefile	Tue May 19 16:54:55 2009 +0200
     8.3 @@ -206,7 +206,7 @@
     8.4  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
     8.5    ATP_Linkup.thy \
     8.6    Code_Eval.thy \
     8.7 -  Code_Index.thy \
     8.8 +  Code_Numeral.thy \
     8.9    Equiv_Relations.thy \
    8.10    Groebner_Basis.thy \
    8.11    Hilbert_Choice.thy \
     9.1 --- a/src/HOL/Library/Code_Integer.thy	Tue May 19 13:57:51 2009 +0200
     9.2 +++ b/src/HOL/Library/Code_Integer.thy	Tue May 19 16:54:55 2009 +0200
     9.3 @@ -91,7 +91,7 @@
     9.4    (OCaml "Big'_int.lt'_big'_int")
     9.5    (Haskell infix 4 "<")
     9.6  
     9.7 -code_const Code_Index.int_of
     9.8 +code_const Code_Numeral.int_of
     9.9    (SML "IntInf.fromInt")
    9.10    (OCaml "Big'_int.big'_int'_of'_int")
    9.11    (Haskell "toEnum")
    10.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue May 19 13:57:51 2009 +0200
    10.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue May 19 16:54:55 2009 +0200
    10.3 @@ -369,12 +369,12 @@
    10.4  
    10.5  text {* Conversion from and to indices. *}
    10.6  
    10.7 -code_const Code_Index.of_nat
    10.8 +code_const Code_Numeral.of_nat
    10.9    (SML "IntInf.toInt")
   10.10    (OCaml "Big'_int.int'_of'_big'_int")
   10.11    (Haskell "fromEnum")
   10.12  
   10.13 -code_const Code_Index.nat_of
   10.14 +code_const Code_Numeral.nat_of
   10.15    (SML "IntInf.fromInt")
   10.16    (OCaml "Big'_int.big'_int'_of'_int")
   10.17    (Haskell "toEnum")
    11.1 --- a/src/HOL/Quickcheck.thy	Tue May 19 13:57:51 2009 +0200
    11.2 +++ b/src/HOL/Quickcheck.thy	Tue May 19 16:54:55 2009 +0200
    11.3 @@ -13,7 +13,7 @@
    11.4  subsection {* The @{text random} class *}
    11.5  
    11.6  class random = typerep +
    11.7 -  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    11.8 +  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    11.9  
   11.10  
   11.11  subsection {* Quickcheck generator *}
   11.12 @@ -49,7 +49,7 @@
   11.13          (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
   11.14      fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
   11.15        (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
   11.16 -  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
   11.17 +  in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
   11.18  
   11.19  fun compile_generator_expr thy t =
   11.20    let
   11.21 @@ -84,7 +84,7 @@
   11.22  instantiation itself :: (typerep) random
   11.23  begin
   11.24  
   11.25 -definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   11.26 +definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   11.27    "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
   11.28  
   11.29  instance ..
   11.30 @@ -139,7 +139,7 @@
   11.31  instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   11.32  begin
   11.33  
   11.34 -definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   11.35 +definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   11.36    "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
   11.37  
   11.38  instance ..
   11.39 @@ -154,9 +154,9 @@
   11.40  instantiation nat :: random
   11.41  begin
   11.42  
   11.43 -definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
   11.44 +definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
   11.45    "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
   11.46 -     let n = Code_Index.nat_of k
   11.47 +     let n = Code_Numeral.nat_of k
   11.48       in (n, \<lambda>_. Code_Eval.term_of n)))"
   11.49  
   11.50  instance ..
   11.51 @@ -168,7 +168,7 @@
   11.52  
   11.53  definition
   11.54    "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
   11.55 -     let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
   11.56 +     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
   11.57       in (j, \<lambda>_. Code_Eval.term_of j)))"
   11.58  
   11.59  instance ..
    12.1 --- a/src/HOL/Random.thy	Tue May 19 13:57:51 2009 +0200
    12.2 +++ b/src/HOL/Random.thy	Tue May 19 16:54:55 2009 +0200
    12.3 @@ -3,7 +3,7 @@
    12.4  header {* A HOL random engine *}
    12.5  
    12.6  theory Random
    12.7 -imports Code_Index List
    12.8 +imports Code_Numeral List
    12.9  begin
   12.10  
   12.11  notation fcomp (infixl "o>" 60)
   12.12 @@ -12,21 +12,21 @@
   12.13  
   12.14  subsection {* Auxiliary functions *}
   12.15  
   12.16 -definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
   12.17 +definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   12.18    "inc_shift v k = (if v = k then 1 else k + 1)"
   12.19  
   12.20 -definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
   12.21 +definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   12.22    "minus_shift r k l = (if k < l then r + k - l else k - l)"
   12.23  
   12.24 -fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
   12.25 +fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   12.26    "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
   12.27  
   12.28  
   12.29  subsection {* Random seeds *}
   12.30  
   12.31 -types seed = "index \<times> index"
   12.32 +types seed = "code_numeral \<times> code_numeral"
   12.33  
   12.34 -primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
   12.35 +primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
   12.36    "next (v, w) = (let
   12.37       k =  v div 53668;
   12.38       v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
   12.39 @@ -55,10 +55,10 @@
   12.40  
   12.41  subsection {* Base selectors *}
   12.42  
   12.43 -fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   12.44 +fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   12.45    "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
   12.46  
   12.47 -definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
   12.48 +definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
   12.49    "range k = iterate (log 2147483561 k)
   12.50        (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
   12.51      o\<rightarrow> (\<lambda>v. Pair (v mod k))"
   12.52 @@ -68,23 +68,23 @@
   12.53    by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
   12.54  
   12.55  definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   12.56 -  "select xs = range (Code_Index.of_nat (length xs))
   12.57 -    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
   12.58 +  "select xs = range (Code_Numeral.of_nat (length xs))
   12.59 +    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
   12.60       
   12.61  lemma select:
   12.62    assumes "xs \<noteq> []"
   12.63    shows "fst (select xs s) \<in> set xs"
   12.64  proof -
   12.65 -  from assms have "Code_Index.of_nat (length xs) > 0" by simp
   12.66 +  from assms have "Code_Numeral.of_nat (length xs) > 0" by simp
   12.67    with range have
   12.68 -    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
   12.69 +    "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best
   12.70    then have
   12.71 -    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
   12.72 +    "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
   12.73    then show ?thesis
   12.74      by (simp add: scomp_apply split_beta select_def)
   12.75  qed
   12.76  
   12.77 -primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
   12.78 +primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
   12.79    "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
   12.80  
   12.81  lemma pick_member:
   12.82 @@ -96,14 +96,14 @@
   12.83    by (induct xs) (auto simp add: expand_fun_eq)
   12.84  
   12.85  lemma pick_same:
   12.86 -  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
   12.87 +  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
   12.88  proof (induct xs arbitrary: l)
   12.89    case Nil then show ?case by simp
   12.90  next
   12.91    case (Cons x xs) then show ?case by (cases l) simp_all
   12.92  qed
   12.93  
   12.94 -definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   12.95 +definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   12.96    "select_weight xs = range (listsum (map fst xs))
   12.97     o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
   12.98  
   12.99 @@ -130,16 +130,16 @@
  12.100    assumes "xs \<noteq> []"
  12.101    shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
  12.102  proof -
  12.103 -  have less: "\<And>s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
  12.104 +  have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
  12.105      using assms by (intro range) simp
  12.106 -  moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
  12.107 +  moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
  12.108      by (induct xs) simp_all
  12.109    ultimately show ?thesis
  12.110      by (auto simp add: select_weight_def select_def scomp_def split_def
  12.111        expand_fun_eq pick_same [symmetric])
  12.112  qed
  12.113  
  12.114 -definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
  12.115 +definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
  12.116    [code del]: "select_default k x y = range k
  12.117       o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
  12.118  
  12.119 @@ -153,7 +153,7 @@
  12.120      else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
  12.121  proof
  12.122    fix s
  12.123 -  have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
  12.124 +  have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
  12.125      by (simp add: range_def scomp_Pair scomp_apply split_beta)
  12.126    then show "select_default k x y s = (if k = 0
  12.127      then range 1 o\<rightarrow> (\<lambda>_. Pair y)
    13.1 --- a/src/HOL/Rational.thy	Tue May 19 13:57:51 2009 +0200
    13.2 +++ b/src/HOL/Rational.thy	Tue May 19 16:54:55 2009 +0200
    13.3 @@ -1013,7 +1013,7 @@
    13.4  
    13.5  definition
    13.6    "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
    13.7 -     let j = Code_Index.int_of (denom + 1)
    13.8 +     let j = Code_Numeral.int_of (denom + 1)
    13.9       in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
   13.10  
   13.11  instance ..
    14.1 --- a/src/HOL/String.thy	Tue May 19 13:57:51 2009 +0200
    14.2 +++ b/src/HOL/String.thy	Tue May 19 16:54:55 2009 +0200
    14.3 @@ -85,15 +85,14 @@
    14.4  
    14.5  subsection {* Strings as dedicated datatype *}
    14.6  
    14.7 -datatype message_string = STR string
    14.8 +datatype literal = STR string
    14.9  
   14.10 -lemmas [code del] =
   14.11 -  message_string.recs message_string.cases
   14.12 +lemmas [code del] = literal.recs literal.cases
   14.13  
   14.14 -lemma [code]: "size (s\<Colon>message_string) = 0"
   14.15 +lemma [code]: "size (s\<Colon>literal) = 0"
   14.16    by (cases s) simp_all
   14.17  
   14.18 -lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
   14.19 +lemma [code]: "literal_size (s\<Colon>literal) = 0"
   14.20    by (cases s) simp_all
   14.21  
   14.22  
   14.23 @@ -101,19 +100,19 @@
   14.24  
   14.25  use "Tools/string_code.ML"
   14.26  
   14.27 -code_type message_string
   14.28 +code_type literal
   14.29    (SML "string")
   14.30    (OCaml "string")
   14.31    (Haskell "String")
   14.32  
   14.33  setup {*
   14.34 -  fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
   14.35 +  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
   14.36  *}
   14.37  
   14.38 -code_instance message_string :: eq
   14.39 +code_instance literal :: eq
   14.40    (Haskell -)
   14.41  
   14.42 -code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
   14.43 +code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   14.44    (SML "!((_ : string) = _)")
   14.45    (OCaml "!((_ : string) = _)")
   14.46    (Haskell infixl 4 "==")
   14.47 @@ -147,4 +146,6 @@
   14.48  in Codegen.add_codegen "char_codegen" char_codegen end
   14.49  *}
   14.50  
   14.51 +hide (open) type literal
   14.52 +
   14.53  end
   14.54 \ No newline at end of file
    15.1 --- a/src/HOL/Tools/hologic.ML	Tue May 19 13:57:51 2009 +0200
    15.2 +++ b/src/HOL/Tools/hologic.ML	Tue May 19 16:54:55 2009 +0200
    15.3 @@ -87,7 +87,7 @@
    15.4    val dest_nat: term -> int
    15.5    val class_size: string
    15.6    val size_const: typ -> term
    15.7 -  val indexT: typ
    15.8 +  val code_numeralT: typ
    15.9    val intT: typ
   15.10    val pls_const: term
   15.11    val min_const: term
   15.12 @@ -116,9 +116,9 @@
   15.13    val stringT: typ
   15.14    val mk_string: string -> term
   15.15    val dest_string: term -> string
   15.16 -  val message_stringT: typ
   15.17 -  val mk_message_string: string -> term
   15.18 -  val dest_message_string: term -> string
   15.19 +  val literalT: typ
   15.20 +  val mk_literal: string -> term
   15.21 +  val dest_literal: term -> string
   15.22    val mk_typerep: typ -> term
   15.23    val mk_term_of: typ -> term -> term
   15.24    val reflect_term: term -> term
   15.25 @@ -461,9 +461,9 @@
   15.26  fun size_const T = Const ("Nat.size_class.size", T --> natT);
   15.27  
   15.28  
   15.29 -(* index *)
   15.30 +(* code numeral *)
   15.31  
   15.32 -val indexT = Type ("Code_Index.index", []);
   15.33 +val code_numeralT = Type ("Code_Numeral.code_numeral", []);
   15.34  
   15.35  
   15.36  (* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
   15.37 @@ -586,15 +586,15 @@
   15.38  val dest_string = implode o map (chr o dest_char) o dest_list;
   15.39  
   15.40  
   15.41 -(* message_string *)
   15.42 +(* literal *)
   15.43  
   15.44 -val message_stringT = Type ("String.message_string", []);
   15.45 +val literalT = Type ("String.literal", []);
   15.46  
   15.47 -fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
   15.48 +fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
   15.49        $ mk_string s;
   15.50 -fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
   15.51 +fun dest_literal (Const ("String.literal.STR", _) $ t) =
   15.52        dest_string t
   15.53 -  | dest_message_string t = raise TERM ("dest_message_string", [t]);
   15.54 +  | dest_literal t = raise TERM ("dest_literal", [t]);
   15.55  
   15.56  
   15.57  (* typerep and term *)
   15.58 @@ -609,8 +609,8 @@
   15.59  fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
   15.60  
   15.61  fun reflect_term (Const (c, T)) =
   15.62 -      Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
   15.63 -        $ mk_message_string c $ mk_typerep T
   15.64 +      Const ("Code_Eval.Const", literalT --> typerepT --> termT)
   15.65 +        $ mk_literal c $ mk_typerep T
   15.66    | reflect_term (t1 $ t2) =
   15.67        Const ("Code_Eval.App", termT --> termT --> termT)
   15.68          $ reflect_term t1 $ reflect_term t2
    16.1 --- a/src/HOL/Tools/string_code.ML	Tue May 19 13:57:51 2009 +0200
    16.2 +++ b/src/HOL/Tools/string_code.ML	Tue May 19 16:54:55 2009 +0200
    16.3 @@ -7,7 +7,7 @@
    16.4  sig
    16.5    val add_literal_list_string: string -> theory -> theory
    16.6    val add_literal_char: string -> theory -> theory
    16.7 -  val add_literal_message: string -> theory -> theory
    16.8 +  val add_literal_string: string -> theory -> theory
    16.9  end;
   16.10  
   16.11  structure String_Code : STRING_CODE =
   16.12 @@ -72,7 +72,7 @@
   16.13      @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
   16.14    end;
   16.15  
   16.16 -fun add_literal_message target =
   16.17 +fun add_literal_string target =
   16.18    let
   16.19      fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
   16.20        case List_Code.implode_list nil' cons' t
    17.1 --- a/src/HOL/Typerep.thy	Tue May 19 13:57:51 2009 +0200
    17.2 +++ b/src/HOL/Typerep.thy	Tue May 19 16:54:55 2009 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  imports Plain String
    17.5  begin
    17.6  
    17.7 -datatype typerep = Typerep message_string "typerep list"
    17.8 +datatype typerep = Typerep String.literal "typerep list"
    17.9  
   17.10  class typerep =
   17.11    fixes typerep :: "'a itself \<Rightarrow> typerep"
   17.12 @@ -45,7 +45,7 @@
   17.13      val ty = Type (tyco, map TFree vs);
   17.14      val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
   17.15        $ Free ("T", Term.itselfT ty);
   17.16 -    val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
   17.17 +    val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
   17.18        $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
   17.19      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   17.20    in