# HG changeset patch
# User haftmann
# Date 1242744895 -7200
# Node ID 98370b26c2ce5b11406f65b388c8fe6aaf05878b
# Parent  46c0c741c8c2d61b243bb0380587b80534e0aa43
String.literal replaces message_string, code_numeral replaces (code_)index

diff -r 46c0c741c8c2 -r 98370b26c2ce doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Tue May 19 13:57:51 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Tue May 19 16:54:55 2009 +0200
@@ -127,8 +127,8 @@
        Useful for code setups which involve e.g. indexing of
        target-language arrays.
     \item[@{theory "String"}] provides an additional datatype
-       @{typ message_string} which is isomorphic to strings;
-       @{typ message_string}s are mapped to target-language strings.
+       @{typ String.literal} which is isomorphic to strings;
+       @{typ String.literal}s are mapped to target-language strings.
        Useful for code setups which involve e.g. printing (error) messages.
 
   \end{description}
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Tue May 19 16:54:55 2009 +0200
@@ -5,7 +5,7 @@
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Eval
-imports Plain Typerep Code_Index
+imports Plain Typerep Code_Numeral
 begin
 
 subsection {* Term representation *}
@@ -14,7 +14,7 @@
 
 datatype "term" = dummy_term
 
-definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
+definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
   "Const _ _ = dummy_term"
 
 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
@@ -63,10 +63,7 @@
     let
       val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
         andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
-    in
-      thy
-      |> need_inst ? add_term_of tyco raw_vs
-    end;
+    in if need_inst then add_term_of tyco raw_vs thy else thy end;
 in
   Code.type_interpretation ensure_term_of
 end
@@ -102,10 +99,7 @@
   fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
     let
       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
-    in
-      thy
-      |> has_inst ? add_term_of_code tyco raw_vs cs
-    end;
+    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
 in
   Code.type_interpretation ensure_term_of_code
 end
@@ -119,7 +113,7 @@
 
 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
 lemma [code, code del]:
   "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
 lemma [code, code del]:
@@ -137,7 +131,7 @@
 code_const Const and App
   (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
 
-code_const "term_of \<Colon> message_string \<Rightarrow> term"
+code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   (Eval "HOLogic.mk'_message'_string")
 
 code_reserved Eval HOLogic
@@ -215,8 +209,8 @@
       else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
   by (simp only: term_of_anything)
 
-lemma (in term_syntax) term_of_index_code [code]:
-  "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
+lemma (in term_syntax) term_of_code_numeral_code [code]:
+  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
   by (simp only: term_of_anything)
 
 subsection {* Obfuscate *}
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Code_Index.thy
--- a/src/HOL/Code_Index.thy	Tue May 19 13:57:51 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,325 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Type of indices *}
-
-theory Code_Index
-imports Nat_Numeral
-begin
-
-text {*
-  Indices are isomorphic to HOL @{typ nat} but
-  mapped to target-language builtin integers.
-*}
-
-subsection {* Datatype of indices *}
-
-typedef (open) index = "UNIV \<Colon> nat set"
-  morphisms nat_of of_nat by rule
-
-lemma of_nat_nat_of [simp]:
-  "of_nat (nat_of k) = k"
-  by (rule nat_of_inverse)
-
-lemma nat_of_of_nat [simp]:
-  "nat_of (of_nat n) = n"
-  by (rule of_nat_inverse) (rule UNIV_I)
-
-lemma [measure_function]:
-  "is_measure nat_of" by (rule is_measure_trivial)
-
-lemma index:
-  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
-proof
-  fix n :: nat
-  assume "\<And>n\<Colon>index. PROP P n"
-  then show "PROP P (of_nat n)" .
-next
-  fix n :: index
-  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
-  then have "PROP P (of_nat (nat_of n))" .
-  then show "PROP P n" by simp
-qed
-
-lemma index_case:
-  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
-  shows P
-  by (rule assms [of "nat_of k"]) simp
-
-lemma index_induct_raw:
-  assumes "\<And>n. P (of_nat n)"
-  shows "P k"
-proof -
-  from assms have "P (of_nat (nat_of k))" .
-  then show ?thesis by simp
-qed
-
-lemma nat_of_inject [simp]:
-  "nat_of k = nat_of l \<longleftrightarrow> k = l"
-  by (rule nat_of_inject)
-
-lemma of_nat_inject [simp]:
-  "of_nat n = of_nat m \<longleftrightarrow> n = m"
-  by (rule of_nat_inject) (rule UNIV_I)+
-
-instantiation index :: zero
-begin
-
-definition [simp, code del]:
-  "0 = of_nat 0"
-
-instance ..
-
-end
-
-definition [simp]:
-  "Suc_index k = of_nat (Suc (nat_of k))"
-
-rep_datatype "0 \<Colon> index" Suc_index
-proof -
-  fix P :: "index \<Rightarrow> bool"
-  fix k :: index
-  assume "P 0" then have init: "P (of_nat 0)" by simp
-  assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
-    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
-    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
-  from init step have "P (of_nat (nat_of k))"
-    by (induct "nat_of k") simp_all
-  then show "P k" by simp
-qed simp_all
-
-declare index_case [case_names nat, cases type: index]
-declare index.induct [case_names nat, induct type: index]
-
-lemma index_decr [termination_simp]:
-  "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
-  by (cases k) simp
-
-lemma [simp, code]:
-  "index_size = nat_of"
-proof (rule ext)
-  fix k
-  have "index_size k = nat_size (nat_of k)"
-    by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
-  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
-  finally show "index_size k = nat_of k" .
-qed
-
-lemma [simp, code]:
-  "size = nat_of"
-proof (rule ext)
-  fix k
-  show "size k = nat_of k"
-  by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
-qed
-
-lemmas [code del] = index.recs index.cases
-
-lemma [code]:
-  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
-  by (cases k, cases l) (simp add: eq)
-
-lemma [code nbe]:
-  "eq_class.eq (k::index) k \<longleftrightarrow> True"
-  by (rule HOL.eq_refl)
-
-
-subsection {* Indices as datatype of ints *}
-
-instantiation index :: number
-begin
-
-definition
-  "number_of = of_nat o nat"
-
-instance ..
-
-end
-
-lemma nat_of_number [simp]:
-  "nat_of (number_of k) = number_of k"
-  by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
-
-code_datatype "number_of \<Colon> int \<Rightarrow> index"
-
-
-subsection {* Basic arithmetic *}
-
-instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
-begin
-
-definition [simp, code del]:
-  "(1\<Colon>index) = of_nat 1"
-
-definition [simp, code del]:
-  "n + m = of_nat (nat_of n + nat_of m)"
-
-definition [simp, code del]:
-  "n - m = of_nat (nat_of n - nat_of m)"
-
-definition [simp, code del]:
-  "n * m = of_nat (nat_of n * nat_of m)"
-
-definition [simp, code del]:
-  "n div m = of_nat (nat_of n div nat_of m)"
-
-definition [simp, code del]:
-  "n mod m = of_nat (nat_of n mod nat_of m)"
-
-definition [simp, code del]:
-  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
-
-definition [simp, code del]:
-  "n < m \<longleftrightarrow> nat_of n < nat_of m"
-
-instance proof
-qed (auto simp add: index left_distrib div_mult_self1)
-
-end
-
-lemma zero_index_code [code inline, code]:
-  "(0\<Colon>index) = Numeral0"
-  by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
-  using zero_index_code ..
-
-lemma one_index_code [code inline, code]:
-  "(1\<Colon>index) = Numeral1"
-  by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>index)"
-  using one_index_code ..
-
-lemma plus_index_code [code nbe]:
-  "of_nat n + of_nat m = of_nat (n + m)"
-  by simp
-
-definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
-  [simp, code del]: "subtract_index = op -"
-
-lemma subtract_index_code [code nbe]:
-  "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
-  by simp
-
-lemma minus_index_code [code]:
-  "n - m = subtract_index n m"
-  by simp
-
-lemma times_index_code [code nbe]:
-  "of_nat n * of_nat m = of_nat (n * m)"
-  by simp
-
-lemma less_eq_index_code [code nbe]:
-  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
-  by simp
-
-lemma less_index_code [code nbe]:
-  "of_nat n < of_nat m \<longleftrightarrow> n < m"
-  by simp
-
-lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
-
-lemma of_nat_code [code]:
-  "of_nat = Nat.of_nat"
-proof
-  fix n :: nat
-  have "Nat.of_nat n = of_nat n"
-    by (induct n) simp_all
-  then show "of_nat n = Nat.of_nat n"
-    by (rule sym)
-qed
-
-lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
-  by (cases i) auto
-
-definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
-  "nat_of_aux i n = nat_of i + n"
-
-lemma nat_of_aux_code [code]:
-  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
-  by (auto simp add: nat_of_aux_def index_not_eq_zero)
-
-lemma nat_of_code [code]:
-  "nat_of i = nat_of_aux i 0"
-  by (simp add: nat_of_aux_def)
-
-definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
-  [code del]: "div_mod_index n m = (n div m, n mod m)"
-
-lemma [code]:
-  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
-  unfolding div_mod_index_def by auto
-
-lemma [code]:
-  "n div m = fst (div_mod_index n m)"
-  unfolding div_mod_index_def by simp
-
-lemma [code]:
-  "n mod m = snd (div_mod_index n m)"
-  unfolding div_mod_index_def by simp
-
-definition int_of :: "index \<Rightarrow> int" where
-  "int_of = Nat.of_nat o nat_of"
-
-lemma int_of_code [code]:
-  "int_of k = (if k = 0 then 0
-    else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
-  by (auto simp add: int_of_def mod_div_equality')
-
-hide (open) const of_nat nat_of int_of
-
-
-subsection {* Code generator setup *}
-
-text {* Implementation of indices by bounded integers *}
-
-code_type index
-  (SML "int")
-  (OCaml "int")
-  (Haskell "Int")
-
-code_instance index :: eq
-  (Haskell -)
-
-setup {*
-  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
-    false false) ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML Int int
-code_reserved OCaml Pervasives int
-
-code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.+/ ((_),/ (_))")
-  (OCaml "Pervasives.( + )")
-  (Haskell infixl 6 "+")
-
-code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
-  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
-  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
-
-code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.*/ ((_),/ (_))")
-  (OCaml "Pervasives.( * )")
-  (Haskell infixl 7 "*")
-
-code_const div_mod_index
-  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
-  (Haskell "divMod")
-
-code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "!((_ : Int.int) = _)")
-  (OCaml "!((_ : int) = _)")
-  (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "Int.<=/ ((_),/ (_))")
-  (OCaml "!((_ : int) <= _)")
-  (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "Int.</ ((_),/ (_))")
-  (OCaml "!((_ : int) < _)")
-  (Haskell infix 4 "<")
-
-end
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Code_Numeral.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Numeral.thy	Tue May 19 16:54:55 2009 +0200
@@ -0,0 +1,325 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Type of target language numerals *}
+
+theory Code_Numeral
+imports Nat_Numeral
+begin
+
+text {*
+  Code numerals are isomorphic to HOL @{typ nat} but
+  mapped to target-language builtin numerals.
+*}
+
+subsection {* Datatype of target language numerals *}
+
+typedef (open) code_numeral = "UNIV \<Colon> nat set"
+  morphisms nat_of of_nat by rule
+
+lemma of_nat_nat_of [simp]:
+  "of_nat (nat_of k) = k"
+  by (rule nat_of_inverse)
+
+lemma nat_of_of_nat [simp]:
+  "nat_of (of_nat n) = n"
+  by (rule of_nat_inverse) (rule UNIV_I)
+
+lemma [measure_function]:
+  "is_measure nat_of" by (rule is_measure_trivial)
+
+lemma code_numeral:
+  "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
+proof
+  fix n :: nat
+  assume "\<And>n\<Colon>code_numeral. PROP P n"
+  then show "PROP P (of_nat n)" .
+next
+  fix n :: code_numeral
+  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
+  then have "PROP P (of_nat (nat_of n))" .
+  then show "PROP P n" by simp
+qed
+
+lemma code_numeral_case:
+  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
+  shows P
+  by (rule assms [of "nat_of k"]) simp
+
+lemma code_numeral_induct_raw:
+  assumes "\<And>n. P (of_nat n)"
+  shows "P k"
+proof -
+  from assms have "P (of_nat (nat_of k))" .
+  then show ?thesis by simp
+qed
+
+lemma nat_of_inject [simp]:
+  "nat_of k = nat_of l \<longleftrightarrow> k = l"
+  by (rule nat_of_inject)
+
+lemma of_nat_inject [simp]:
+  "of_nat n = of_nat m \<longleftrightarrow> n = m"
+  by (rule of_nat_inject) (rule UNIV_I)+
+
+instantiation code_numeral :: zero
+begin
+
+definition [simp, code del]:
+  "0 = of_nat 0"
+
+instance ..
+
+end
+
+definition [simp]:
+  "Suc_code_numeral k = of_nat (Suc (nat_of k))"
+
+rep_datatype "0 \<Colon> code_numeral" Suc_code_numeral
+proof -
+  fix P :: "code_numeral \<Rightarrow> bool"
+  fix k :: code_numeral
+  assume "P 0" then have init: "P (of_nat 0)" by simp
+  assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
+    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
+    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
+  from init step have "P (of_nat (nat_of k))"
+    by (induct "nat_of k") simp_all
+  then show "P k" by simp
+qed simp_all
+
+declare code_numeral_case [case_names nat, cases type: code_numeral]
+declare code_numeral.induct [case_names nat, induct type: code_numeral]
+
+lemma code_numeral_decr [termination_simp]:
+  "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Suc 0 < nat_of k"
+  by (cases k) simp
+
+lemma [simp, code]:
+  "code_numeral_size = nat_of"
+proof (rule ext)
+  fix k
+  have "code_numeral_size k = nat_size (nat_of k)"
+    by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+  finally show "code_numeral_size k = nat_of k" .
+qed
+
+lemma [simp, code]:
+  "size = nat_of"
+proof (rule ext)
+  fix k
+  show "size k = nat_of k"
+  by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+qed
+
+lemmas [code del] = code_numeral.recs code_numeral.cases
+
+lemma [code]:
+  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
+  by (cases k, cases l) (simp add: eq)
+
+lemma [code nbe]:
+  "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
+
+
+subsection {* Indices as datatype of ints *}
+
+instantiation code_numeral :: number
+begin
+
+definition
+  "number_of = of_nat o nat"
+
+instance ..
+
+end
+
+lemma nat_of_number [simp]:
+  "nat_of (number_of k) = number_of k"
+  by (simp add: number_of_code_numeral_def nat_number_of_def number_of_is_id)
+
+code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
+
+
+subsection {* Basic arithmetic *}
+
+instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}"
+begin
+
+definition [simp, code del]:
+  "(1\<Colon>code_numeral) = of_nat 1"
+
+definition [simp, code del]:
+  "n + m = of_nat (nat_of n + nat_of m)"
+
+definition [simp, code del]:
+  "n - m = of_nat (nat_of n - nat_of m)"
+
+definition [simp, code del]:
+  "n * m = of_nat (nat_of n * nat_of m)"
+
+definition [simp, code del]:
+  "n div m = of_nat (nat_of n div nat_of m)"
+
+definition [simp, code del]:
+  "n mod m = of_nat (nat_of n mod nat_of m)"
+
+definition [simp, code del]:
+  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
+
+definition [simp, code del]:
+  "n < m \<longleftrightarrow> nat_of n < nat_of m"
+
+instance proof
+qed (auto simp add: code_numeral left_distrib div_mult_self1)
+
+end
+
+lemma zero_code_numeral_code [code inline, code]:
+  "(0\<Colon>code_numeral) = Numeral0"
+  by (simp add: number_of_code_numeral_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
+  using zero_code_numeral_code ..
+
+lemma one_code_numeral_code [code inline, code]:
+  "(1\<Colon>code_numeral) = Numeral1"
+  by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
+  using one_code_numeral_code ..
+
+lemma plus_code_numeral_code [code nbe]:
+  "of_nat n + of_nat m = of_nat (n + m)"
+  by simp
+
+definition subtract_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+  [simp, code del]: "subtract_code_numeral = op -"
+
+lemma subtract_code_numeral_code [code nbe]:
+  "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)"
+  by simp
+
+lemma minus_code_numeral_code [code]:
+  "n - m = subtract_code_numeral n m"
+  by simp
+
+lemma times_code_numeral_code [code nbe]:
+  "of_nat n * of_nat m = of_nat (n * m)"
+  by simp
+
+lemma less_eq_code_numeral_code [code nbe]:
+  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
+  by simp
+
+lemma less_code_numeral_code [code nbe]:
+  "of_nat n < of_nat m \<longleftrightarrow> n < m"
+  by simp
+
+lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
+
+lemma of_nat_code [code]:
+  "of_nat = Nat.of_nat"
+proof
+  fix n :: nat
+  have "Nat.of_nat n = of_nat n"
+    by (induct n) simp_all
+  then show "of_nat n = Nat.of_nat n"
+    by (rule sym)
+qed
+
+lemma code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
+  by (cases i) auto
+
+definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where
+  "nat_of_aux i n = nat_of i + n"
+
+lemma nat_of_aux_code [code]:
+  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
+  by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
+
+lemma nat_of_code [code]:
+  "nat_of i = nat_of_aux i 0"
+  by (simp add: nat_of_aux_def)
+
+definition div_mod_code_numeral ::  "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
+  [code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
+
+lemma [code]:
+  "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))"
+  unfolding div_mod_code_numeral_def by auto
+
+lemma [code]:
+  "n div m = fst (div_mod_code_numeral n m)"
+  unfolding div_mod_code_numeral_def by simp
+
+lemma [code]:
+  "n mod m = snd (div_mod_code_numeral n m)"
+  unfolding div_mod_code_numeral_def by simp
+
+definition int_of :: "code_numeral \<Rightarrow> int" where
+  "int_of = Nat.of_nat o nat_of"
+
+lemma int_of_code [code]:
+  "int_of k = (if k = 0 then 0
+    else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
+  by (auto simp add: int_of_def mod_div_equality')
+
+hide (open) const of_nat nat_of int_of
+
+
+subsection {* Code generator setup *}
+
+text {* Implementation of indices by bounded integers *}
+
+code_type code_numeral
+  (SML "int")
+  (OCaml "int")
+  (Haskell "Int")
+
+code_instance code_numeral :: eq
+  (Haskell -)
+
+setup {*
+  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false false) ["SML", "OCaml", "Haskell"]
+*}
+
+code_reserved SML Int int
+code_reserved OCaml Pervasives int
+
+code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+  (SML "Int.+/ ((_),/ (_))")
+  (OCaml "Pervasives.( + )")
+  (Haskell infixl 6 "+")
+
+code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
+  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+
+code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+  (SML "Int.*/ ((_),/ (_))")
+  (OCaml "Pervasives.( * )")
+  (Haskell infixl 7 "*")
+
+code_const div_mod_code_numeral
+  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
+  (Haskell "divMod")
+
+code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+  (SML "!((_ : Int.int) = _)")
+  (OCaml "!((_ : int) = _)")
+  (Haskell infixl 4 "==")
+
+code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+  (SML "Int.<=/ ((_),/ (_))")
+  (OCaml "!((_ : int) <= _)")
+  (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+  (SML "Int.</ ((_),/ (_))")
+  (OCaml "!((_ : int) < _)")
+  (Haskell infix 4 "<")
+
+end
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue May 19 16:54:55 2009 +0200
@@ -115,47 +115,47 @@
 subsubsection {* Logical intermediate layer *}
 
 definition new' where
-  [code del]: "new' = Array.new o Code_Index.nat_of"
+  [code del]: "new' = Array.new o Code_Numeral.nat_of"
 hide (open) const new'
 lemma [code]:
-  "Array.new = Array.new' o Code_Index.of_nat"
+  "Array.new = Array.new' o Code_Numeral.of_nat"
   by (simp add: new'_def o_def)
 
 definition of_list' where
-  [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
+  [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
 hide (open) const of_list'
 lemma [code]:
-  "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
+  "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
   by (simp add: of_list'_def)
 
 definition make' where
-  [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
+  [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
 hide (open) const make'
 lemma [code]:
-  "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
+  "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
   by (simp add: make'_def o_def)
 
 definition length' where
-  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
+  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
 hide (open) const length'
 lemma [code]:
-  "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
+  "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
   by (simp add: length'_def monad_simp',
     simp add: liftM_def comp_def monad_simp,
     simp add: monad_simp')
 
 definition nth' where
-  [code del]: "nth' a = Array.nth a o Code_Index.nat_of"
+  [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
 hide (open) const nth'
 lemma [code]:
-  "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
+  "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
   by (simp add: nth'_def)
 
 definition upd' where
-  [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
+  [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
 hide (open) const upd'
 lemma [code]:
-  "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
+  "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
   by (simp add: upd'_def monad_simp upd_return)
 
 
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Tue May 19 16:54:55 2009 +0200
@@ -28,11 +28,11 @@
 
 instance int :: heap ..
 
-instance message_string :: countable
-  by (rule countable_classI [of "message_string_case to_nat"])
-   (auto split: message_string.splits)
+instance String.literal :: countable
+  by (rule countable_classI [of "String.literal_case to_nat"])
+   (auto split: String.literal.splits)
 
-instance message_string :: heap ..
+instance String.literal :: heap ..
 
 text {* Reflected types themselves are heap-representable *}
 
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 16:54:55 2009 +0200
@@ -274,7 +274,7 @@
 subsubsection {* Logical intermediate layer *}
 
 definition
-  Fail :: "message_string \<Rightarrow> exception"
+  Fail :: "String.literal \<Rightarrow> exception"
 where
   [code del]: "Fail s = Exn"
 
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/IsaMakefile	Tue May 19 16:54:55 2009 +0200
@@ -206,7 +206,7 @@
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
   ATP_Linkup.thy \
   Code_Eval.thy \
-  Code_Index.thy \
+  Code_Numeral.thy \
   Equiv_Relations.thy \
   Groebner_Basis.thy \
   Hilbert_Choice.thy \
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Tue May 19 16:54:55 2009 +0200
@@ -91,7 +91,7 @@
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
 
-code_const Code_Index.int_of
+code_const Code_Numeral.int_of
   (SML "IntInf.fromInt")
   (OCaml "Big'_int.big'_int'_of'_int")
   (Haskell "toEnum")
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue May 19 16:54:55 2009 +0200
@@ -369,12 +369,12 @@
 
 text {* Conversion from and to indices. *}
 
-code_const Code_Index.of_nat
+code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
   (OCaml "Big'_int.int'_of'_big'_int")
   (Haskell "fromEnum")
 
-code_const Code_Index.nat_of
+code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "Big'_int.big'_int'_of'_int")
   (Haskell "toEnum")
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Quickcheck.thy	Tue May 19 16:54:55 2009 +0200
@@ -13,7 +13,7 @@
 subsection {* The @{text random} class *}
 
 class random = typerep +
-  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
 
 
 subsection {* Quickcheck generator *}
@@ -49,7 +49,7 @@
         (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
     fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
       (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
-  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
+  in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
 
 fun compile_generator_expr thy t =
   let
@@ -84,7 +84,7 @@
 instantiation itself :: (typerep) random
 begin
 
-definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
 
 instance ..
@@ -139,7 +139,7 @@
 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
 begin
 
-definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
 
 instance ..
@@ -154,9 +154,9 @@
 instantiation nat :: random
 begin
 
-definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
   "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
-     let n = Code_Index.nat_of k
+     let n = Code_Numeral.nat_of k
      in (n, \<lambda>_. Code_Eval.term_of n)))"
 
 instance ..
@@ -168,7 +168,7 @@
 
 definition
   "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
-     let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
+     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
      in (j, \<lambda>_. Code_Eval.term_of j)))"
 
 instance ..
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Random.thy
--- a/src/HOL/Random.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Random.thy	Tue May 19 16:54:55 2009 +0200
@@ -3,7 +3,7 @@
 header {* A HOL random engine *}
 
 theory Random
-imports Code_Index List
+imports Code_Numeral List
 begin
 
 notation fcomp (infixl "o>" 60)
@@ -12,21 +12,21 @@
 
 subsection {* Auxiliary functions *}
 
-definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
+definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "inc_shift v k = (if v = k then 1 else k + 1)"
 
-definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
+definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "minus_shift r k l = (if k < l then r + k - l else k - l)"
 
-fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
+fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
 
 
 subsection {* Random seeds *}
 
-types seed = "index \<times> index"
+types seed = "code_numeral \<times> code_numeral"
 
-primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
+primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
   "next (v, w) = (let
      k =  v div 53668;
      v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
@@ -55,10 +55,10 @@
 
 subsection {* Base selectors *}
 
-fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
 
-definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
   "range k = iterate (log 2147483561 k)
       (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
     o\<rightarrow> (\<lambda>v. Pair (v mod k))"
@@ -68,23 +68,23 @@
   by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
 
 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
-  "select xs = range (Code_Index.of_nat (length xs))
-    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
+  "select xs = range (Code_Numeral.of_nat (length xs))
+    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
      
 lemma select:
   assumes "xs \<noteq> []"
   shows "fst (select xs s) \<in> set xs"
 proof -
-  from assms have "Code_Index.of_nat (length xs) > 0" by simp
+  from assms have "Code_Numeral.of_nat (length xs) > 0" by simp
   with range have
-    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
+    "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best
   then have
-    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
+    "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
   then show ?thesis
     by (simp add: scomp_apply split_beta select_def)
 qed
 
-primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
+primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
   "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
 
 lemma pick_member:
@@ -96,14 +96,14 @@
   by (induct xs) (auto simp add: expand_fun_eq)
 
 lemma pick_same:
-  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
+  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
 proof (induct xs arbitrary: l)
   case Nil then show ?case by simp
 next
   case (Cons x xs) then show ?case by (cases l) simp_all
 qed
 
-definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   "select_weight xs = range (listsum (map fst xs))
    o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
 
@@ -130,16 +130,16 @@
   assumes "xs \<noteq> []"
   shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
 proof -
-  have less: "\<And>s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
+  have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
     using assms by (intro range) simp
-  moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
+  moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
     by (induct xs) simp_all
   ultimately show ?thesis
     by (auto simp add: select_weight_def select_def scomp_def split_def
       expand_fun_eq pick_same [symmetric])
 qed
 
-definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   [code del]: "select_default k x y = range k
      o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
 
@@ -153,7 +153,7 @@
     else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
 proof
   fix s
-  have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
+  have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
     by (simp add: range_def scomp_Pair scomp_apply split_beta)
   then show "select_default k x y s = (if k = 0
     then range 1 o\<rightarrow> (\<lambda>_. Pair y)
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Rational.thy	Tue May 19 16:54:55 2009 +0200
@@ -1013,7 +1013,7 @@
 
 definition
   "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
-     let j = Code_Index.int_of (denom + 1)
+     let j = Code_Numeral.int_of (denom + 1)
      in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
 
 instance ..
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/String.thy
--- a/src/HOL/String.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/String.thy	Tue May 19 16:54:55 2009 +0200
@@ -85,15 +85,14 @@
 
 subsection {* Strings as dedicated datatype *}
 
-datatype message_string = STR string
+datatype literal = STR string
 
-lemmas [code del] =
-  message_string.recs message_string.cases
+lemmas [code del] = literal.recs literal.cases
 
-lemma [code]: "size (s\<Colon>message_string) = 0"
+lemma [code]: "size (s\<Colon>literal) = 0"
   by (cases s) simp_all
 
-lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
+lemma [code]: "literal_size (s\<Colon>literal) = 0"
   by (cases s) simp_all
 
 
@@ -101,19 +100,19 @@
 
 use "Tools/string_code.ML"
 
-code_type message_string
+code_type literal
   (SML "string")
   (OCaml "string")
   (Haskell "String")
 
 setup {*
-  fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
+  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
 *}
 
-code_instance message_string :: eq
+code_instance literal :: eq
   (Haskell -)
 
-code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
   (OCaml "!((_ : string) = _)")
   (Haskell infixl 4 "==")
@@ -147,4 +146,6 @@
 in Codegen.add_codegen "char_codegen" char_codegen end
 *}
 
+hide (open) type literal
+
 end
\ No newline at end of file
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Tue May 19 16:54:55 2009 +0200
@@ -87,7 +87,7 @@
   val dest_nat: term -> int
   val class_size: string
   val size_const: typ -> term
-  val indexT: typ
+  val code_numeralT: typ
   val intT: typ
   val pls_const: term
   val min_const: term
@@ -116,9 +116,9 @@
   val stringT: typ
   val mk_string: string -> term
   val dest_string: term -> string
-  val message_stringT: typ
-  val mk_message_string: string -> term
-  val dest_message_string: term -> string
+  val literalT: typ
+  val mk_literal: string -> term
+  val dest_literal: term -> string
   val mk_typerep: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
@@ -461,9 +461,9 @@
 fun size_const T = Const ("Nat.size_class.size", T --> natT);
 
 
-(* index *)
+(* code numeral *)
 
-val indexT = Type ("Code_Index.index", []);
+val code_numeralT = Type ("Code_Numeral.code_numeral", []);
 
 
 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
@@ -586,15 +586,15 @@
 val dest_string = implode o map (chr o dest_char) o dest_list;
 
 
-(* message_string *)
+(* literal *)
 
-val message_stringT = Type ("String.message_string", []);
+val literalT = Type ("String.literal", []);
 
-fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
+fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
       $ mk_string s;
-fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
+fun dest_literal (Const ("String.literal.STR", _) $ t) =
       dest_string t
-  | dest_message_string t = raise TERM ("dest_message_string", [t]);
+  | dest_literal t = raise TERM ("dest_literal", [t]);
 
 
 (* typerep and term *)
@@ -609,8 +609,8 @@
 fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
 
 fun reflect_term (Const (c, T)) =
-      Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
-        $ mk_message_string c $ mk_typerep T
+      Const ("Code_Eval.Const", literalT --> typerepT --> termT)
+        $ mk_literal c $ mk_typerep T
   | reflect_term (t1 $ t2) =
       Const ("Code_Eval.App", termT --> termT --> termT)
         $ reflect_term t1 $ reflect_term t2
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Tools/string_code.ML
--- a/src/HOL/Tools/string_code.ML	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Tools/string_code.ML	Tue May 19 16:54:55 2009 +0200
@@ -7,7 +7,7 @@
 sig
   val add_literal_list_string: string -> theory -> theory
   val add_literal_char: string -> theory -> theory
-  val add_literal_message: string -> theory -> theory
+  val add_literal_string: string -> theory -> theory
 end;
 
 structure String_Code : STRING_CODE =
@@ -72,7 +72,7 @@
     @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
   end;
 
-fun add_literal_message target =
+fun add_literal_string target =
   let
     fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
       case List_Code.implode_list nil' cons' t
diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Typerep.thy	Tue May 19 16:54:55 2009 +0200
@@ -6,7 +6,7 @@
 imports Plain String
 begin
 
-datatype typerep = Typerep message_string "typerep list"
+datatype typerep = Typerep String.literal "typerep list"
 
 class typerep =
   fixes typerep :: "'a itself \<Rightarrow> typerep"
@@ -45,7 +45,7 @@
     val ty = Type (tyco, map TFree vs);
     val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
       $ Free ("T", Term.itselfT ty);
-    val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
+    val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
       $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in