# HG changeset patch
# User haftmann
# Date 1457816692 -3600
# Node ID b3f2b8c906a69e82dffbcc2d473c792191724b4c
# Parent  cf79f8866bc310328e3cb5c811194c360aa87a89
model characters directly as range 0..255
* * *
operate on syntax terms rather than asts

diff -r cf79f8866bc3 -r b3f2b8c906a6 NEWS
--- a/NEWS	Fri Mar 11 17:20:14 2016 +0100
+++ b/NEWS	Sat Mar 12 22:04:52 2016 +0100
@@ -53,6 +53,30 @@
 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
 resemble the f.split naming convention, INCOMPATIBILITY.
 
+* Characters (type char) are modelled as finite algebraic type
+corresponding to {0..255}.
+
+  - Logical representation:
+    * 0 is instantiated to the ASCII zero character.
+    * All other characters are represented as »Char n«
+      with n being a raw numeral expression less than 256.
+    * Expressions of the form »Char n« with n greater than 255
+      are non-canonical.
+  - Printing and parsing:
+    * Printable characters are printed and parsed as »CHR ''…''«
+      (as before).
+    * The ASCII zero character is printed and parsed as »0«.
+    * All other canonical characters are printed as »CHAR 0xXX«
+      with XX being the hexadecimal character code.  »CHAR n«
+      is parsable for every numeral expression n.
+    * Non-canonial characters have no special syntax and are
+      printed as their logical representation.
+  - Explicit conversions from and to the natural numbers are
+    provided as char_of_nat, nat_of_char (as before).
+  - The auxiliary nibble type has been discontinued.
+
+INCOMPATIBILITY.
+
 * Multiset membership is now expressed using set_mset rather than count.
 
   - Expressions "count M a > 0" and similar simplify to membership
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Code_Evaluation.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -105,12 +105,14 @@
   "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
   "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
 
-lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
-  "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
-   Code_Evaluation.App (Code_Evaluation.App
-    (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
-      (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
-  by (subst term_of_anything) rule 
+definition case_char :: "'a \<Rightarrow> (num \<Rightarrow> 'a) \<Rightarrow> char \<Rightarrow> 'a"
+  where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))"
+
+lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]:
+  "term_of =
+    case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char)))
+    (\<lambda>k. App (Const (STR ''String.Char'') (TYPEREP(num \<Rightarrow> char))) (term_of k))"
+  by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq])
 
 lemma term_of_string [code]:
    "term_of s = App (Const (STR ''STR'')
@@ -133,7 +135,7 @@
    else
      App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer))
        (term_of (- i)))"
-by(rule term_of_anything[THEN meta_eq_to_obj_eq])
+  by (rule term_of_anything [THEN meta_eq_to_obj_eq])
 
 code_reserved Eval HOLogic
 
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Divides.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -1635,6 +1635,37 @@
   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   by (simp_all add: snd_divmod)
 
+lemma cut_eq_simps: -- \<open>rewriting equivalence on @{text "n mod 2 ^ q"}\<close>
+  fixes m n q :: num
+  shows
+    "numeral n mod numeral Num.One = (0::nat)
+      \<longleftrightarrow> True"
+    "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
+      \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
+    "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
+      \<longleftrightarrow> False"
+    "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
+      \<longleftrightarrow> True"
+    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> True"
+    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> False"
+    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
+    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> False"
+    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
+    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> False"
+    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
+    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> False"
+    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
+      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
+  by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
+
 
 subsection \<open>Division on @{typ int}\<close>
 
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/HOLCF/Library/Char_Discrete.thy
--- a/src/HOL/HOLCF/Library/Char_Discrete.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -8,52 +8,6 @@
 imports HOLCF
 begin
 
-subsection \<open>Discrete cpo instance for @{typ nibble}.\<close>
-
-instantiation nibble :: discrete_cpo
-begin
-
-definition below_nibble_def:
-  "(x::nibble) \<sqsubseteq> y \<longleftrightarrow> x = y"
-
-instance proof
-qed (rule below_nibble_def)
-
-end
-
-text \<open>
-  TODO: implement a command to automate discrete predomain instances.
-\<close>
-
-instantiation nibble :: predomain
-begin
-
-definition
-  "(liftemb :: nibble u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
-
-definition
-  "(liftprj :: udom u \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
-
-definition
-  "liftdefl \<equiv> (\<lambda>(t::nibble itself). LIFTDEFL(nibble discr))"
-
-instance proof
-  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nibble u)"
-    unfolding liftemb_nibble_def liftprj_nibble_def
-    apply (rule ep_pair_comp)
-    apply (rule ep_pair_u_map)
-    apply (simp add: ep_pair.intro)
-    apply (rule predomain_ep)
-    done
-  show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom u \<rightarrow> nibble u)"
-    unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def
-    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
-    apply (simp add: ID_def [symmetric] u_map_ID)
-    done
-qed
-
-end
-
 subsection \<open>Discrete cpo instance for @{typ char}.\<close>
 
 instantiation char :: discrete_cpo
@@ -100,146 +54,4 @@
 
 end
 
-subsection \<open>Using chars with Fixrec\<close>
-
-definition match_Char :: "char \<rightarrow> (nibble \<rightarrow> nibble \<rightarrow> 'a match) \<rightarrow> 'a match"
-  where "match_Char = (\<Lambda> c k. case c of Char a b \<Rightarrow> k\<cdot>a\<cdot>b)"
-
-lemma match_Char_simps [simp]:
-  "match_Char\<cdot>(Char a b)\<cdot>k = k\<cdot>a\<cdot>b"
-by (simp add: match_Char_def)
-
-definition match_Nibble0 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble0 = (\<Lambda> c k. if c = Nibble0 then k else Fixrec.fail)"
-
-definition match_Nibble1 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble1 = (\<Lambda> c k. if c = Nibble1 then k else Fixrec.fail)"
-
-definition match_Nibble2 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble2 = (\<Lambda> c k. if c = Nibble2 then k else Fixrec.fail)"
-
-definition match_Nibble3 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble3 = (\<Lambda> c k. if c = Nibble3 then k else Fixrec.fail)"
-
-definition match_Nibble4 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble4 = (\<Lambda> c k. if c = Nibble4 then k else Fixrec.fail)"
-
-definition match_Nibble5 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble5 = (\<Lambda> c k. if c = Nibble5 then k else Fixrec.fail)"
-
-definition match_Nibble6 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble6 = (\<Lambda> c k. if c = Nibble6 then k else Fixrec.fail)"
-
-definition match_Nibble7 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble7 = (\<Lambda> c k. if c = Nibble7 then k else Fixrec.fail)"
-
-definition match_Nibble8 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble8 = (\<Lambda> c k. if c = Nibble8 then k else Fixrec.fail)"
-
-definition match_Nibble9 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_Nibble9 = (\<Lambda> c k. if c = Nibble9 then k else Fixrec.fail)"
-
-definition match_NibbleA :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_NibbleA = (\<Lambda> c k. if c = NibbleA then k else Fixrec.fail)"
-
-definition match_NibbleB :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_NibbleB = (\<Lambda> c k. if c = NibbleB then k else Fixrec.fail)"
-
-definition match_NibbleC :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_NibbleC = (\<Lambda> c k. if c = NibbleC then k else Fixrec.fail)"
-
-definition match_NibbleD :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_NibbleD = (\<Lambda> c k. if c = NibbleD then k else Fixrec.fail)"
-
-definition match_NibbleE :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_NibbleE = (\<Lambda> c k. if c = NibbleE then k else Fixrec.fail)"
-
-definition match_NibbleF :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
-  where "match_NibbleF = (\<Lambda> c k. if c = NibbleF then k else Fixrec.fail)"
-
-lemma match_Nibble0_simps [simp]:
-  "match_Nibble0\<cdot>c\<cdot>k = (if c = Nibble0 then k else Fixrec.fail)"
-by (simp add: match_Nibble0_def)
-
-lemma match_Nibble1_simps [simp]:
-  "match_Nibble1\<cdot>c\<cdot>k = (if c = Nibble1 then k else Fixrec.fail)"
-by (simp add: match_Nibble1_def)
-
-lemma match_Nibble2_simps [simp]:
-  "match_Nibble2\<cdot>c\<cdot>k = (if c = Nibble2 then k else Fixrec.fail)"
-by (simp add: match_Nibble2_def)
-
-lemma match_Nibble3_simps [simp]:
-  "match_Nibble3\<cdot>c\<cdot>k = (if c = Nibble3 then k else Fixrec.fail)"
-by (simp add: match_Nibble3_def)
-
-lemma match_Nibble4_simps [simp]:
-  "match_Nibble4\<cdot>c\<cdot>k = (if c = Nibble4 then k else Fixrec.fail)"
-by (simp add: match_Nibble4_def)
-
-lemma match_Nibble5_simps [simp]:
-  "match_Nibble5\<cdot>c\<cdot>k = (if c = Nibble5 then k else Fixrec.fail)"
-by (simp add: match_Nibble5_def)
-
-lemma match_Nibble6_simps [simp]:
-  "match_Nibble6\<cdot>c\<cdot>k = (if c = Nibble6 then k else Fixrec.fail)"
-by (simp add: match_Nibble6_def)
-
-lemma match_Nibble7_simps [simp]:
-  "match_Nibble7\<cdot>c\<cdot>k = (if c = Nibble7 then k else Fixrec.fail)"
-by (simp add: match_Nibble7_def)
-
-lemma match_Nibble8_simps [simp]:
-  "match_Nibble8\<cdot>c\<cdot>k = (if c = Nibble8 then k else Fixrec.fail)"
-by (simp add: match_Nibble8_def)
-
-lemma match_Nibble9_simps [simp]:
-  "match_Nibble9\<cdot>c\<cdot>k = (if c = Nibble9 then k else Fixrec.fail)"
-by (simp add: match_Nibble9_def)
-
-lemma match_NibbleA_simps [simp]:
-  "match_NibbleA\<cdot>c\<cdot>k = (if c = NibbleA then k else Fixrec.fail)"
-by (simp add: match_NibbleA_def)
-
-lemma match_NibbleB_simps [simp]:
-  "match_NibbleB\<cdot>c\<cdot>k = (if c = NibbleB then k else Fixrec.fail)"
-by (simp add: match_NibbleB_def)
-
-lemma match_NibbleC_simps [simp]:
-  "match_NibbleC\<cdot>c\<cdot>k = (if c = NibbleC then k else Fixrec.fail)"
-by (simp add: match_NibbleC_def)
-
-lemma match_NibbleD_simps [simp]:
-  "match_NibbleD\<cdot>c\<cdot>k = (if c = NibbleD then k else Fixrec.fail)"
-by (simp add: match_NibbleD_def)
-
-lemma match_NibbleE_simps [simp]:
-  "match_NibbleE\<cdot>c\<cdot>k = (if c = NibbleE then k else Fixrec.fail)"
-by (simp add: match_NibbleE_def)
-
-lemma match_NibbleF_simps [simp]:
-  "match_NibbleF\<cdot>c\<cdot>k = (if c = NibbleF then k else Fixrec.fail)"
-by (simp add: match_NibbleF_def)
-
-setup \<open>
-  Fixrec.add_matchers
-    [ (@{const_name Char}, @{const_name match_Char}),
-      (@{const_name Nibble0}, @{const_name match_Nibble0}),
-      (@{const_name Nibble1}, @{const_name match_Nibble1}),
-      (@{const_name Nibble2}, @{const_name match_Nibble2}),
-      (@{const_name Nibble3}, @{const_name match_Nibble3}),
-      (@{const_name Nibble4}, @{const_name match_Nibble4}),
-      (@{const_name Nibble5}, @{const_name match_Nibble5}),
-      (@{const_name Nibble6}, @{const_name match_Nibble6}),
-      (@{const_name Nibble7}, @{const_name match_Nibble7}),
-      (@{const_name Nibble8}, @{const_name match_Nibble8}),
-      (@{const_name Nibble9}, @{const_name match_Nibble9}),
-      (@{const_name NibbleA}, @{const_name match_NibbleA}),
-      (@{const_name NibbleB}, @{const_name match_NibbleB}),
-      (@{const_name NibbleC}, @{const_name match_NibbleC}),
-      (@{const_name NibbleD}, @{const_name match_NibbleD}),
-      (@{const_name NibbleE}, @{const_name match_NibbleE}),
-      (@{const_name NibbleF}, @{const_name match_NibbleF}) ]
-\<close>
-
 end
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Library/Cardinality.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -149,15 +149,6 @@
   finally show ?thesis .
 qed
 
-lemma card_nibble: "CARD(nibble) = 16"
-unfolding UNIV_nibble by simp
-
-lemma card_UNIV_char: "CARD(char) = 256"
-proof -
-  have "inj (\<lambda>(x, y). Char x y)" by(auto intro: injI)
-  thus ?thesis unfolding UNIV_char by(simp add: card_image card_nibble)
-qed
-
 lemma card_literal: "CARD(String.literal) = 0"
 by(simp add: card_eq_0_iff infinite_literal)
 
@@ -263,12 +254,6 @@
 instance by(intro_classes)(simp_all add: card_UNIV_bool_def finite_UNIV_bool_def)
 end
 
-instantiation nibble :: card_UNIV begin
-definition "finite_UNIV = Phantom(nibble) True"
-definition "card_UNIV = Phantom(nibble) 16"
-instance by(intro_classes)(simp_all add: card_UNIV_nibble_def card_nibble finite_UNIV_nibble_def)
-end
-
 instantiation char :: card_UNIV begin
 definition "finite_UNIV = Phantom(char) True"
 definition "card_UNIV = Phantom(char) 256"
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Library/Char_ord.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -8,28 +8,6 @@
 imports Main
 begin
 
-instantiation nibble :: linorder
-begin
-
-definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
-definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
-
-instance
-  by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
-
-end
-
-instantiation nibble :: distrib_lattice
-begin
-
-definition "(inf :: nibble \<Rightarrow> _) = min"
-definition "(sup :: nibble \<Rightarrow> _) = max"
-
-instance
-  by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
-
-end
-
 instantiation char :: linorder
 begin
 
@@ -37,40 +15,22 @@
 definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
 
 instance
-  by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
+  by standard (auto simp add: less_eq_char_def less_char_def)
 
 end
 
-lemma less_eq_char_Char:
-  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
-proof -
-  {
-    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
-      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
-    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
-    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
-  }
-  note * = this
-  show ?thesis
-    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
-    by (auto simp add: less_eq_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
-qed
+lemma less_eq_char_simps:
+  "(0 :: char) \<le> c"
+  "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
+  "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
+  by (simp_all add: Char_def less_eq_char_def)
 
-lemma less_char_Char:
-  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
-proof -
-  {
-    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
-      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
-    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
-    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
-  }
-  note * = this
-  show ?thesis
-    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
-    by (auto simp add: less_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
-qed
-
+lemma less_char_simps:
+  "\<not> c < (0 :: char)"
+  "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
+  "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
+  by (simp_all add: Char_def less_char_def)
+  
 instantiation char :: distrib_lattice
 begin
 
@@ -111,14 +71,4 @@
 lifting_update literal.lifting
 lifting_forget literal.lifting
 
-text \<open>Legacy aliasses\<close>
-
-lemmas nibble_less_eq_def = less_eq_nibble_def
-lemmas nibble_less_def = less_nibble_def
-lemmas char_less_eq_def = less_eq_char_def
-lemmas char_less_def = less_char_def
-lemmas char_less_eq_simp = less_eq_char_Char
-lemmas char_less_simp = less_char_Char
-
 end
-
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Library/Code_Char.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -21,7 +21,17 @@
 \<close>
 
 code_printing
-  class_instance char :: equal \<rightharpoonup>
+  constant integer_of_char \<rightharpoonup>
+    (SML) "!(IntInf.fromInt o Char.ord)"
+    and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
+    and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
+    and (Scala) "BigInt(_.toInt)"
+| constant char_of_integer \<rightharpoonup>
+    (SML) "!(Char.chr o IntInf.toInt)"
+    and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
+    and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
+    and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))"
+| class_instance char :: equal \<rightharpoonup>
     (Haskell) -
 | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : char) = _)"
@@ -54,45 +64,8 @@
     and (Haskell) "_"
     and (Scala) "!(_.toList)"
 
-
-definition integer_of_char :: "char \<Rightarrow> integer"
-where
-  "integer_of_char = integer_of_nat o nat_of_char"
-
-definition char_of_integer :: "integer \<Rightarrow> char"
-where
-  "char_of_integer = char_of_nat \<circ> nat_of_integer"
-
-lemma [code]:
-  "nat_of_char = nat_of_integer o integer_of_char"
-  by (simp add: integer_of_char_def fun_eq_iff)
-
-lemma [code]:
-  "char_of_nat = char_of_integer o integer_of_nat"
-  by (simp add: char_of_integer_def fun_eq_iff)
-
-lemmas integer_of_char_code [code] =
-  nat_of_char_simps[
-    THEN arg_cong[where f="integer_of_nat"],
-    unfolded integer_of_nat_numeral integer_of_nat_1 integer_of_nat_0,
-    folded fun_cong[OF integer_of_char_def, unfolded o_apply]]
-
-lemma char_of_integer_code [code]:
-  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
-  by (simp add: char_of_integer_def enum_char_unfold)
-
 code_printing
-  constant integer_of_char \<rightharpoonup>
-    (SML) "!(IntInf.fromInt o Char.ord)"
-    and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
-    and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
-    and (Scala) "BigInt(_.toInt)"
-| constant char_of_integer \<rightharpoonup>
-    (SML) "!(Char.chr o IntInf.toInt)"
-    and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
-    and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
-    and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))"
-| constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
+  constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : char) <= _)"
     and (OCaml) "!((_ : char) <= _)"
     and (Haskell) infix 4 "<="
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Library/Code_Test.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -83,8 +83,8 @@
 
 definition list where "list f xs = map (node \<circ> f) xs"
 
-definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])"
-definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])"
+definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])"
+definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])"
 definition XY :: yxml_of_term where "XY = yot_append X Y"
 definition XYX :: yxml_of_term where "XYX = yot_append XY X"
 
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -52,6 +52,8 @@
 
 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close>
 setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close>
+setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Char}]\<close>
+setup \<open>Predicate_Compile_Data.keep_functions [@{const_name Char}]\<close>
 
 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}]\<close>
 
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -14,6 +14,11 @@
 nitpick_params [verbose, card = 1-8, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
+datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3
+  | Nibble4 | Nibble5 | Nibble6 | Nibble7
+  | Nibble8 | Nibble9 | NibbleA | NibbleB
+  | NibbleC | NibbleD | NibbleE | NibbleF
+
 primrec rot where
 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
 "rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Num.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -297,12 +297,9 @@
 
 typed_print_translation \<open>
   let
-    fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
-      | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
-      | dest_num (Const (@{const_syntax One}, _)) = 1;
     fun num_tr' ctxt T [n] =
       let
-        val k = dest_num n;
+        val k = Numeral.dest_num_syntax n;
         val t' =
           Syntax.const @{syntax_const "_Numeral"} $
             Syntax.free (string_of_int k);
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Parity.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -180,6 +180,21 @@
   "odd (n :: nat) \<Longrightarrow> 0 < n"
   by (auto elim: oddE)
 
+lemma Suc_double_not_eq_double:
+  fixes m n :: nat
+  shows "Suc (2 * m) \<noteq> 2 * n"
+proof
+  assume "Suc (2 * m) = 2 * n"
+  moreover have "odd (Suc (2 * m))" and "even (2 * n)"
+    by simp_all
+  ultimately show False by simp
+qed
+
+lemma double_not_eq_Suc_double:
+  fixes m n :: nat
+  shows "2 * m \<noteq> Suc (2 * n)"
+  using Suc_double_not_eq_double [of n m] by simp
+
 lemma even_diff_iff [simp]:
   fixes k l :: int
   shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -379,42 +379,13 @@
 
 end
 
-instantiation nibble :: check_all
+(* FIXME instantiation char :: check_all
 begin
 
 definition
-  "check_all f =
-    f (Code_Evaluation.valtermify Nibble0) orelse
-    f (Code_Evaluation.valtermify Nibble1) orelse
-    f (Code_Evaluation.valtermify Nibble2) orelse
-    f (Code_Evaluation.valtermify Nibble3) orelse
-    f (Code_Evaluation.valtermify Nibble4) orelse
-    f (Code_Evaluation.valtermify Nibble5) orelse
-    f (Code_Evaluation.valtermify Nibble6) orelse
-    f (Code_Evaluation.valtermify Nibble7) orelse
-    f (Code_Evaluation.valtermify Nibble8) orelse
-    f (Code_Evaluation.valtermify Nibble9) orelse
-    f (Code_Evaluation.valtermify NibbleA) orelse
-    f (Code_Evaluation.valtermify NibbleB) orelse
-    f (Code_Evaluation.valtermify NibbleC) orelse
-    f (Code_Evaluation.valtermify NibbleD) orelse
-    f (Code_Evaluation.valtermify NibbleE) orelse
-    f (Code_Evaluation.valtermify NibbleF)"
-
-definition enum_term_of_nibble :: "nibble itself => unit => term list"
-where
-  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
-
-instance ..
-
-end
-
-
-instantiation char :: check_all
-begin
-
-definition
-  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
+  "check_all f = check_all (%(x, t1). check_all (%(y, t2).
+     f (Char x y, %_. Code_Evaluation.App
+       (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
 
 definition enum_term_of_char :: "char itself => unit => term list"
 where
@@ -422,8 +393,7 @@
 
 instance ..
 
-end
-
+end *)
 
 instantiation option :: (check_all) check_all
 begin
@@ -624,13 +594,7 @@
 
 ML_file "Tools/Quickcheck/abstract_generators.ML"
 
-lemma check_all_char [code]:
-  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
-     f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
-       (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
-  by (simp add: check_all_char_def)
-
-instantiation char :: full_exhaustive
+(* FIXME instantiation char :: full_exhaustive
 begin
 
 definition full_exhaustive_char
@@ -648,7 +612,7 @@
 
 instance ..
 
-end
+end *)
 
 hide_fact (open) orelse_def
 no_notation orelse (infixr "orelse" 55)
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sat Mar 12 22:04:52 2016 +0100
@@ -77,7 +77,8 @@
 
 fun string_eq_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt
-    addsimps (@{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms simp_thms})
+    addsimps @{thms list.inject list.distinct Char_eq_Char_iff
+      cut_eq_simps simp_thms}
     addsimprocs [lazy_conj_simproc]
     |> Simplifier.add_cong @{thm block_conj_cong});
 
@@ -85,7 +86,7 @@
 
 val lookup_ss =
   simpset_of (put_simpset HOL_basic_ss @{context}
-    addsimps (@{thms list.inject} @ @{thms char.inject}
+    addsimps (@{thms list.inject} @ @{thms Char_eq_Char_iff}
       @ @{thms list.distinct} @ @{thms simp_thms}
       @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
         @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
@@ -162,7 +163,7 @@
 val meta_ext = @{thm StateFun.meta_ext};
 val ss' =
   simpset_of (put_simpset HOL_ss @{context} addsimps
-    (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
+    (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms Char_eq_Char_iff}
       @ @{thms list.distinct})
     addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
     |> fold Simplifier.add_cong @{thms block_conj_cong});
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/String.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -56,7 +56,7 @@
   by (simp add: char_of_nat_def Abs_char_inject)
 
 lemma inj_on_char_of_nat [simp]:
-  "inj_on char_of_nat {0..<256}"
+  "inj_on char_of_nat {..<256}"
   by (rule inj_onI) simp
 
 lemma nat_of_char_mod_256 [simp]:
@@ -72,197 +72,143 @@
 qed
 
 lemma UNIV_char_of_nat:
-  "UNIV = char_of_nat ` {0..<256}"
+  "UNIV = char_of_nat ` {..<256}"
 proof -
   { fix c
-    have "c \<in> char_of_nat ` {0..<256}"
+    have "c \<in> char_of_nat ` {..<256}"
       by (cases c) auto
   } then show ?thesis by auto
 qed
 
-
-subsubsection \<open>Traditional concrete representation of characters\<close>
-
-datatype (plugins del: transfer) nibble =
-    Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
-  | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
+lemma card_UNIV_char:
+  "card (UNIV :: char set) = 256"
+  by (auto simp add: UNIV_char_of_nat card_image)
 
-lemma UNIV_nibble:
-  "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
-    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
-proof (rule UNIV_eq_I)
-  fix x show "x \<in> ?A" by (cases x) simp_all
-qed
+lemma range_nat_of_char:
+  "range nat_of_char = {..<256}"
+  by (auto simp add: UNIV_char_of_nat image_image image_def)
 
-lemma size_nibble [code, simp]:
-  "size_nibble (x::nibble) = 0"
-  "size (x::nibble) = 0"
-  by (cases x, simp_all)+
 
-instantiation nibble :: enum
+subsubsection \<open>Character literals as variant of numerals\<close>
+
+instantiation char :: zero
 begin
 
-definition
-  "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
-    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
+definition zero_char :: char
+  where "0 = char_of_nat 0"
 
-definition
-  "Enum.enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
-     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
-
-definition
-  "Enum.enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
-     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
-
-instance proof
-qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
+instance ..
 
 end
 
-lemma card_UNIV_nibble:
-  "card (UNIV :: nibble set) = 16"
-  by (simp add: card_UNIV_length_enum enum_nibble_def)
+definition Char :: "num \<Rightarrow> char"
+  where "Char k = char_of_nat (numeral k)"
+
+code_datatype "0 :: char" Char
+
+lemma nat_of_char_zero [simp]:
+  "nat_of_char 0 = 0"
+  by (simp add: zero_char_def)
+
+lemma nat_of_char_Char [simp]:
+  "nat_of_char (Char k) = numeral k mod 256"
+  by (simp add: Char_def)
 
-primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
+lemma Char_eq_Char_iff [simp]:
+  "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
+proof -
+  have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
+    by (rule sym, rule inj_eq) (fact inj_nat_of_char)
+  also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
+    by (simp only: Char_def nat_of_char_of_nat)
+  finally show ?thesis .
+qed
+
+lemma zero_eq_Char_iff [simp]:
+  "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
+  by (auto simp add: zero_char_def Char_def)
+
+lemma Char_eq_zero_iff [simp]:
+  "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
+  by (auto simp add: zero_char_def Char_def) 
+
+definition integer_of_char :: "char \<Rightarrow> integer"
 where
-  "nat_of_nibble Nibble0 = 0"
-| "nat_of_nibble Nibble1 = 1"
-| "nat_of_nibble Nibble2 = 2"
-| "nat_of_nibble Nibble3 = 3"
-| "nat_of_nibble Nibble4 = 4"
-| "nat_of_nibble Nibble5 = 5"
-| "nat_of_nibble Nibble6 = 6"
-| "nat_of_nibble Nibble7 = 7"
-| "nat_of_nibble Nibble8 = 8"
-| "nat_of_nibble Nibble9 = 9"
-| "nat_of_nibble NibbleA = 10"
-| "nat_of_nibble NibbleB = 11"
-| "nat_of_nibble NibbleC = 12"
-| "nat_of_nibble NibbleD = 13"
-| "nat_of_nibble NibbleE = 14"
-| "nat_of_nibble NibbleF = 15"
+  "integer_of_char = integer_of_nat \<circ> nat_of_char"
 
-definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
-  "nibble_of_nat n = Enum.enum ! (n mod 16)"
+definition char_of_integer :: "integer \<Rightarrow> char"
+where
+  "char_of_integer = char_of_nat \<circ> nat_of_integer"
+
+lemma integer_of_char_zero [simp, code]:
+  "integer_of_char 0 = 0"
+  by (simp add: integer_of_char_def integer_of_nat_def)
 
-lemma nibble_of_nat_simps [simp]:
-  "nibble_of_nat  0 = Nibble0"
-  "nibble_of_nat  1 = Nibble1"
-  "nibble_of_nat  2 = Nibble2"
-  "nibble_of_nat  3 = Nibble3"
-  "nibble_of_nat  4 = Nibble4"
-  "nibble_of_nat  5 = Nibble5"
-  "nibble_of_nat  6 = Nibble6"
-  "nibble_of_nat  7 = Nibble7"
-  "nibble_of_nat  8 = Nibble8"
-  "nibble_of_nat  9 = Nibble9"
-  "nibble_of_nat 10 = NibbleA"
-  "nibble_of_nat 11 = NibbleB"
-  "nibble_of_nat 12 = NibbleC"
-  "nibble_of_nat 13 = NibbleD"
-  "nibble_of_nat 14 = NibbleE"
-  "nibble_of_nat 15 = NibbleF"
-  unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
+lemma integer_of_char_Char [simp]:
+  "integer_of_char (Char k) = numeral k mod 256"
+  by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
+    id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
 
-lemma nibble_of_nat_of_nibble [simp]:
-  "nibble_of_nat (nat_of_nibble x) = x"
-  by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
+lemma less_256_integer_of_char_Char:
+  assumes "numeral k < (256 :: integer)"
+  shows "integer_of_char (Char k) = numeral k"
+proof -
+  have "numeral k mod 256 = (numeral k :: integer)"
+    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
+  then show ?thesis using integer_of_char_Char [of k]
+    by (simp only:)
+qed
 
-lemma nat_of_nibble_of_nat [simp]:
-  "nat_of_nibble (nibble_of_nat n) = n mod 16"
-  by (cases "nibble_of_nat n")
-     (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
-
-lemma inj_nat_of_nibble:
-  "inj nat_of_nibble"
-  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
+setup \<open>
+let
+  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
+  val simpset =
+    put_simpset HOL_ss @{context}
+      addsimps @{thms numeral_less_iff less_num_simps};
+  fun mk_code_eqn ct =
+    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
+    |> full_simplify simpset;
+  val code_eqns = map mk_code_eqn chars;
+in
+  Global_Theory.note_thmss ""
+    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
+  #> snd
+end
+\<close>
 
-lemma nat_of_nibble_eq_iff:
-  "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
-  by (rule inj_eq) (rule inj_nat_of_nibble)
+declare integer_of_char_simps [code]
+
+lemma nat_of_char_code [code]:
+  "nat_of_char = nat_of_integer \<circ> integer_of_char"
+  by (simp add: integer_of_char_def fun_eq_iff)
 
-lemma nat_of_nibble_less_16:
-  "nat_of_nibble x < 16"
-  by (cases x) auto
+lemma char_of_nat_code [code]:
+  "char_of_nat = char_of_integer \<circ> integer_of_nat"
+  by (simp add: char_of_integer_def fun_eq_iff)
 
-lemma nibble_of_nat_mod_16:
-  "nibble_of_nat (n mod 16) = nibble_of_nat n"
-  by (simp add: nibble_of_nat_def)
-
-context
+instantiation char :: equal
 begin
 
-local_setup \<open>Local_Theory.map_background_naming (Name_Space.add_path "char")\<close>
+definition equal_char
+  where "equal_char (c :: char) d \<longleftrightarrow> c = d"
 
-definition Char :: "nibble \<Rightarrow> nibble \<Rightarrow> char"
-where
-  "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)"
-  \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
+instance
+  by standard (simp add: equal_char_def)
 
 end
 
-lemma nat_of_char_Char:
-  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" (is "_ = ?rhs")
-proof -
-  have "?rhs < 256"
-    using nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
-    by arith
-  then show ?thesis by (simp add: Char_def)
-qed
-
-lemma char_of_nat_Char_nibbles:
-  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
-proof -
-  from mod_mult2_eq [of n 16 16]
-  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
-  then show ?thesis
-    by (simp add: Char_def)
-qed
-
-lemma char_of_nat_nibble_pair [simp]:
-  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
-  by (simp add: nat_of_char_Char [symmetric])
-
-free_constructors char for Char
-proof -
-  fix P c
-  assume hyp: "\<And>x y. c = Char x y \<Longrightarrow> P"
-  have "nat_of_char c \<le> 255"
-    using nat_of_char_less_256 [of c] by arith
-  then have "nat_of_char c div 16 \<le> 255 div 16"
-    by (auto intro: div_le_mono2)
-  then have "nat_of_char c div 16 < 16"
-    by auto
-  then have "nat_of_char c div 16 mod 16 = nat_of_char c div 16"
-    by simp
-  then have "c = Char (nibble_of_nat (nat_of_char c div 16))
-    (nibble_of_nat (nat_of_char c mod 16))"
-    by (simp add: Char_def)
-  then show P by (rule hyp)
-next
-  fix x y z w
-  have "Char x y = Char z w
-    \<longleftrightarrow> nat_of_char (Char x y) = nat_of_char (Char z w)"
-    by auto
-  also have "\<dots> \<longleftrightarrow> nat_of_nibble x = nat_of_nibble z \<and> nat_of_nibble y = nat_of_nibble w" (is "?P \<longleftrightarrow> ?Q \<and> ?R")
-  proof
-    assume "?Q \<and> ?R"
-    then show ?P by (simp add: nat_of_char_Char)
-  next
-    assume ?P
-    then have ?Q
-      using nat_of_nibble_less_16 [of y] nat_of_nibble_less_16 [of w]
-      by (simp add: nat_of_char_Char)
-    moreover with \<open>?P\<close> have ?R by (simp add: nat_of_char_Char)
-    ultimately show "?Q \<and> ?R" ..
-  qed
-  also have "\<dots> \<longleftrightarrow> x = z \<and> y = w"
-    by (simp add: nat_of_nibble_eq_iff)
-  finally show "Char x y = Char z w \<longleftrightarrow> x = z \<and> y = w" .
-qed
+lemma equal_char_simps [code]:
+  "HOL.equal (0::char) 0 \<longleftrightarrow> True"
+  "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
+  "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
+  "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
+  by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
 
 syntax
-  "_Char" :: "str_position => char"    ("CHR _")
+  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
+
+syntax
+  "_Char_ord" :: "num_const \<Rightarrow> char"     ("CHAR _")
 
 type_synonym string = "char list"
 
@@ -271,84 +217,74 @@
 
 ML_file "Tools/string_syntax.ML"
 
-lemma UNIV_char:
-  "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
-proof (rule UNIV_eq_I)
-  fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
-qed
-
 instantiation char :: enum
 begin
 
 definition
-  "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
-  Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
-  Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
-  Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
-  Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
-  Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
-  Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
-  Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
-  Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
-  Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
-  Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
-  Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
-  Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
-  CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
-  CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
-  CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
-  CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
-  CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
-  CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
-  CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
-  CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
-  CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
-  CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
-  CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
-  CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
-  Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
-  Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
-  Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
-  Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
-  Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
-  Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
-  Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
-  Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
-  Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
-  Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
-  Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
-  Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
-  Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
-  Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
-  Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
-  Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
-  Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
-  Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
-  Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
-  Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
-  Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
-  Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
-  Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
-  Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
-  Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
-  Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
-  Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
-  Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
-  Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
-  Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
-  Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
-  Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
-  Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
-  Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
-  Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
-  Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
-  Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
-  Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
-  Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
-  Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
-  Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
-  Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
-  Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
+  "Enum.enum = [0, CHAR 0x01, CHAR 0x02, CHAR 0x03,
+    CHAR 0x04, CHAR 0x05, CHAR 0x06, CHAR 0x07,
+    CHAR 0x08, CHAR 0x09, CHR ''\<newline>'', CHAR 0x0B,
+    CHAR 0x0C, CHAR 0x0D, CHAR 0x0E, CHAR 0x0F,
+    CHAR 0x10, CHAR 0x11, CHAR 0x12, CHAR 0x13,
+    CHAR 0x14, CHAR 0x15, CHAR 0x16, CHAR 0x17,
+    CHAR 0x18, CHAR 0x19, CHAR 0x1A, CHAR 0x1B,
+    CHAR 0x1C, CHAR 0x1D, CHAR 0x1E, CHAR 0x1F,
+    CHR '' '', CHR ''!'', CHAR 0x22, CHR ''#'',
+    CHR ''$'', CHR ''%'', CHR ''&'', CHAR 0x27,
+    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
+    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
+    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
+    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
+    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
+    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
+    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
+    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
+    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
+    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
+    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
+    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
+    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
+    CHAR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
+    CHAR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
+    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
+    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
+    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
+    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
+    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
+    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
+    CHR ''|'', CHR ''}'', CHR ''~'', CHAR 0x7F,
+    CHAR 0x80, CHAR 0x81, CHAR 0x82, CHAR 0x83,
+    CHAR 0x84, CHAR 0x85, CHAR 0x86, CHAR 0x87,
+    CHAR 0x88, CHAR 0x89, CHAR 0x8A, CHAR 0x8B,
+    CHAR 0x8C, CHAR 0x8D, CHAR 0x8E, CHAR 0x8F,
+    CHAR 0x90, CHAR 0x91, CHAR 0x92, CHAR 0x93,
+    CHAR 0x94, CHAR 0x95, CHAR 0x96, CHAR 0x97,
+    CHAR 0x98, CHAR 0x99, CHAR 0x9A, CHAR 0x9B,
+    CHAR 0x9C, CHAR 0x9D, CHAR 0x9E, CHAR 0x9F,
+    CHAR 0xA0, CHAR 0xA1, CHAR 0xA2, CHAR 0xA3,
+    CHAR 0xA4, CHAR 0xA5, CHAR 0xA6, CHAR 0xA7,
+    CHAR 0xA8, CHAR 0xA9, CHAR 0xAA, CHAR 0xAB,
+    CHAR 0xAC, CHAR 0xAD, CHAR 0xAE, CHAR 0xAF,
+    CHAR 0xB0, CHAR 0xB1, CHAR 0xB2, CHAR 0xB3,
+    CHAR 0xB4, CHAR 0xB5, CHAR 0xB6, CHAR 0xB7,
+    CHAR 0xB8, CHAR 0xB9, CHAR 0xBA, CHAR 0xBB,
+    CHAR 0xBC, CHAR 0xBD, CHAR 0xBE, CHAR 0xBF,
+    CHAR 0xC0, CHAR 0xC1, CHAR 0xC2, CHAR 0xC3,
+    CHAR 0xC4, CHAR 0xC5, CHAR 0xC6, CHAR 0xC7,
+    CHAR 0xC8, CHAR 0xC9, CHAR 0xCA, CHAR 0xCB,
+    CHAR 0xCC, CHAR 0xCD, CHAR 0xCE, CHAR 0xCF,
+    CHAR 0xD0, CHAR 0xD1, CHAR 0xD2, CHAR 0xD3,
+    CHAR 0xD4, CHAR 0xD5, CHAR 0xD6, CHAR 0xD7,
+    CHAR 0xD8, CHAR 0xD9, CHAR 0xDA, CHAR 0xDB,
+    CHAR 0xDC, CHAR 0xDD, CHAR 0xDE, CHAR 0xDF,
+    CHAR 0xE0, CHAR 0xE1, CHAR 0xE2, CHAR 0xE3,
+    CHAR 0xE4, CHAR 0xE5, CHAR 0xE6, CHAR 0xE7,
+    CHAR 0xE8, CHAR 0xE9, CHAR 0xEA, CHAR 0xEB,
+    CHAR 0xEC, CHAR 0xED, CHAR 0xEE, CHAR 0xEF,
+    CHAR 0xF0, CHAR 0xF1, CHAR 0xF2, CHAR 0xF3,
+    CHAR 0xF4, CHAR 0xF5, CHAR 0xF6, CHAR 0xF7,
+    CHAR 0xF8, CHAR 0xF9, CHAR 0xFA, CHAR 0xFB,
+    CHAR 0xFC, CHAR 0xFD, CHAR 0xFE, CHAR 0xFF]"
 
 definition
   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
@@ -356,15 +292,22 @@
 definition
   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
 
-lemma enum_char_product_enum_nibble:
-  "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
-  by (simp add: enum_char_def enum_nibble_def)
+lemma enum_char_unfold:
+  "Enum.enum = map char_of_nat [0..<256]"
+proof -
+  have *: "Suc (Suc 0) = 2" by simp
+  have "map nat_of_char Enum.enum = [0..<256]"
+    by (simp add: enum_char_def upt_conv_Cons_Cons *)
+  then have "map char_of_nat (map nat_of_char Enum.enum) =
+    map char_of_nat [0..<256]" by simp
+  then show ?thesis by (simp add: comp_def)
+qed
 
 instance proof
   show UNIV: "UNIV = set (Enum.enum :: char list)"
-    by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
+    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
   show "distinct (Enum.enum :: char list)"
-    by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
+    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
     by (simp add: UNIV enum_all_char_def list_all_iff)
   show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
@@ -373,66 +316,9 @@
 
 end
 
-lemma card_UNIV_char:
-  "card (UNIV :: char set) = 256"
-  by (simp add: card_UNIV_length_enum enum_char_def)
-
-lemma enum_char_unfold:
-  "Enum.enum = map char_of_nat [0..<256]"
-proof -
-  have *: "Suc (Suc 0) = 2" by simp
-  have "map nat_of_char Enum.enum = [0..<256]"
-    by (simp add: enum_char_def nat_of_char_Char upt_conv_Cons_Cons *)
-  then have "map char_of_nat (map nat_of_char Enum.enum) =
-    map char_of_nat [0..<256]" by simp
-  then show ?thesis by (simp add: comp_def)
-qed
-
-setup \<open>
-let
-  val nibbles = map_range (Thm.cterm_of @{context} o HOLogic.mk_nibble) 16;
-  val simpset =
-    put_simpset HOL_ss @{context}
-      addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
-  fun mk_code_eqn x y =
-    Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
-    |> simplify simpset;
-  val code_eqns = map_product mk_code_eqn nibbles nibbles;
-in
-  Global_Theory.note_thmss ""
-    [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
-  #> snd
-end
-\<close>
-
-declare nat_of_char_simps [code]
-
-lemma nibble_of_nat_of_char_div_16:
-  "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
-  by (cases c)
-    (simp add: nat_of_char_Char add.commute nat_of_nibble_less_16)
-
-lemma nibble_of_nat_nat_of_char:
-  "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
-proof (cases c)
-  case (Char x y)
-  then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
-    by (simp add: nibble_of_nat_mod_16)
-  then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
-    by (simp only: nibble_of_nat_mod_16)
-  with Char show ?thesis by (simp add: nat_of_char_Char add.commute)
-qed
-
-code_datatype Char \<comment> \<open>drop case certificate for char\<close>
-
-lemma case_char_code [code]:
-  "char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
-  by (cases c)
-    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
-
-lemma char_of_nat_enum [code]:
-  "char_of_nat n = Enum.enum ! (n mod 256)"
-  by (simp add: enum_char_unfold)
+lemma char_of_integer_code [code]:
+  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
+  by (simp add: char_of_integer_def enum_char_unfold)
 
 
 subsection \<open>Strings as dedicated type\<close>
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Tools/hologic.ML	Sat Mar 12 22:04:52 2016 +0100
@@ -108,9 +108,6 @@
   val code_integerT: typ
   val code_naturalT: typ
   val realT: typ
-  val nibbleT: typ
-  val mk_nibble: int -> term
-  val dest_nibble: term -> int
   val charT: typ
   val mk_char: int -> term
   val dest_char: term -> int
@@ -594,42 +591,27 @@
   | dest_list t = raise TERM ("dest_list", [t]);
 
 
-(* nibble *)
-
-val nibbleT = Type ("String.nibble", []);
-
-fun mk_nibble n =
-  let val s =
-    if 0 <= n andalso n <= 9 then chr (n + ord "0")
-    else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
-    else raise TERM ("mk_nibble", [])
-  in Const ("String.nibble.Nibble" ^ s, nibbleT) end;
-
-fun dest_nibble t =
-  let fun err () = raise TERM ("dest_nibble", [t]) in
-    (case try (unprefix "String.nibble.Nibble" o fst o Term.dest_Const) t of
-      NONE => err ()
-    | SOME c =>
-        if size c <> 1 then err ()
-        else if "0" <= c andalso c <= "9" then ord c - ord "0"
-        else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
-        else err ())
-  end;
-
-
 (* char *)
 
 val charT = Type ("String.char", []);
 
-fun mk_char n =
-  if 0 <= n andalso n <= 255 then
-    Const ("String.char.Char", nibbleT --> nibbleT --> charT) $
-      mk_nibble (n div 16) $ mk_nibble (n mod 16)
-  else raise TERM ("mk_char", []);
+val Char_const = Const ("String.Char", numT --> charT);
+
+fun mk_char 0 = Const ("Groups.zero_class.zero", charT)
+  | mk_char i =
+      if 1 <= i andalso i <= 255 then Char_const $ mk_numeral i
+      else raise TERM ("mk_char", []);
 
-fun dest_char (Const ("String.char.Char", _) $ t $ u) =
-      dest_nibble t * 16 + dest_nibble u
-  | dest_char t = raise TERM ("dest_char", [t]);
+fun dest_char t =
+  let
+    val (T, n) = case t of
+      Const ("Groups.zero_class.zero", T) => (T, 0)
+    | (Const ("String.Char", Type ("fun", [_, T])) $ t) => (T, dest_numeral t)
+    | _ => raise TERM ("dest_char", [t]);
+  in
+    if T = charT then n
+    else raise TERM ("dest_char", [t])
+  end;
 
 
 (* string *)
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Tools/numeral.ML	Sat Mar 12 22:04:52 2016 +0100
@@ -6,9 +6,12 @@
 
 signature NUMERAL =
 sig
-  val mk_cnumeral: int -> cterm
   val mk_cnumber: ctyp -> int -> cterm
   val mk_number_syntax: int -> term
+  val mk_cnumeral: int -> cterm
+  val mk_num_syntax: int -> term
+  val dest_num_syntax: term -> int
+  val dest_num: Code_Thingol.iterm -> int option
   val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
 end;
 
@@ -17,6 +20,18 @@
 
 (* numeral *)
 
+fun dest_num_syntax (Const (@{const_syntax Num.Bit0}, _) $ t) = 2 * dest_num_syntax t
+  | dest_num_syntax (Const (@{const_syntax Num.Bit1}, _) $ t) = 2 * dest_num_syntax t + 1
+  | dest_num_syntax (Const (@{const_syntax Num.One}, _)) = 1;
+
+fun mk_num_syntax n =
+  if n > 0 then
+    (case IntInf.quotRem (n, 2) of
+      (0, 1) => Syntax.const @{const_syntax One}
+    | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
+    | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
+  else raise Match
+
 fun mk_cbit 0 = @{cterm "Num.Bit0"}
   | mk_cbit 1 = @{cterm "Num.Bit1"}
   | mk_cbit _ = raise CTERM ("mk_cbit", []);
@@ -67,14 +82,6 @@
 
 end;
 
-fun mk_num_syntax n =
-  if n > 0 then
-    (case IntInf.quotRem (n, 2) of
-      (0, 1) => Syntax.const @{const_syntax One}
-    | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
-    | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
-  else raise Match
-
 fun mk_number_syntax n =
   if n = 0 then Syntax.const @{const_syntax Groups.zero}
   else if n = 1 then Syntax.const @{const_syntax Groups.one}
@@ -85,17 +92,25 @@
 
 local open Basic_Code_Thingol in
 
+fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1
+  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) =
+     (case dest_num t of
+        SOME n => SOME (2 * n)
+      | _ => NONE)
+  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) =
+     (case dest_num t of
+        SOME n => SOME (2 * n + 1)
+      | _ => NONE)
+  | dest_num _ = NONE;
+
 fun add_code number_of preproc print target thy =
   let
     fun pretty literals _ thm _ _ [(t, _)] =
       let
-        fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
-          | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
-          | dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit";
-        fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
-          | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
-          | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
-      in (Code_Printer.str o print literals o preproc o dest_num) t end;
+        val n = case dest_num t of
+          SOME n => n
+        | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"
+      in (Code_Printer.str o print literals o preproc) n end;
   in
     thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
       [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Tools/string_code.ML
--- a/src/HOL/Tools/string_code.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Tools/string_code.ML	Sat Mar 12 22:04:52 2016 +0100
@@ -16,34 +16,22 @@
 
 open Basic_Code_Thingol;
 
-val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
-  @{const_name Nibble2}, @{const_name Nibble3},
-  @{const_name Nibble4}, @{const_name Nibble5},
-  @{const_name Nibble6}, @{const_name Nibble7},
-  @{const_name Nibble8}, @{const_name Nibble9},
-  @{const_name NibbleA}, @{const_name NibbleB},
-  @{const_name NibbleC}, @{const_name NibbleD},
-  @{const_name NibbleE}, @{const_name NibbleF}];
+fun decode_char_nonzero t =
+  case Numeral.dest_num t of
+    SOME n => if 0 < n andalso n < 256 then SOME n else NONE
+  | _ => NONE;
 
-fun decode_char tt =
-  let
-    fun idx c = find_index (curry (op =) c) cs_nibbles;
-    fun decode ~1 _ = NONE
-      | decode _ ~1 = NONE
-      | decode n m = SOME (chr (n * 16 + m));
-  in case tt
-   of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
-    | _ => NONE
-  end;
-   
+fun decode_char (IConst { sym = Code_Symbol.Constant @{const_name Groups.zero}, ... }) =
+     SOME 0
+  | decode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t) =
+      decode_char_nonzero t
+  | decode_char _ = NONE
+
 fun implode_string literals ts =
   let
-    fun implode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t1 `$ t2) =
-          decode_char (t1, t2)
-      | implode_char _ = NONE;
-    val ts' = map_filter implode_char ts;
-  in if length ts = length ts'
-    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
+    val is = map_filter decode_char ts;
+  in if length ts = length is
+    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode o map chr) is
     else NONE
   end;
 
@@ -64,13 +52,20 @@
 
 fun add_literal_char target thy =
   let
-    fun pretty literals _ thm _ _ [(t1, _), (t2, _)] =
-      case decode_char (t1, t2)
-       of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
+    fun pr literals =
+      Code_Printer.str o Code_Printer.literal_char literals o chr;
+    fun pretty_zero literals _ _ _ _ [] =
+      pr literals 0
+    fun pretty_Char literals _ thm _ _ [(t, _)] =
+      case decode_char_nonzero t
+       of SOME i => pr literals i
         | NONE => Code_Printer.eqn_error thy thm "Illegal character expression";
   in
-    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
-      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) thy
+    thy
+    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.zero_char_inst.zero_char},
+      [(target, SOME (Code_Printer.complex_const_syntax (0, pretty_zero)))]))
+    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
+      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty_Char)))]))
   end;
 
 fun add_literal_string target thy =
@@ -82,8 +77,9 @@
               | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression")
         | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
   in
-    Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
-      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) thy
+    thy
+    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
+      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
   end;
 
 end;
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Sat Mar 12 22:04:52 2016 +0100
@@ -1,85 +1,109 @@
 (*  Title:      HOL/Tools/string_syntax.ML
     Author:     Makarius
 
-Concrete syntax for hex chars and strings.
+Concrete syntax for chars and strings.
 *)
 
 structure String_Syntax: sig end =
 struct
 
-(* nibble *)
+(* numeral *)
 
-val mk_nib =
-  Ast.Constant o Lexicon.mark_const o
-    fst o Term.dest_Const o HOLogic.mk_nibble;
+fun hex_digit n = if n = 10 then "A"
+  else if n = 11 then "B"
+  else if n = 12 then "C"
+  else if n = 13 then "D"
+  else if n = 14 then "E"
+  else if n = 15 then "F"
+  else string_of_int n;
 
-fun dest_nib (Ast.Constant s) =
-  (case try Lexicon.unmark_const s of
-    NONE => raise Match
-  | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
+fun hex_prefix ms = "0x" ^ implode (replicate (2 - length ms) "0" @ ms);
+
+fun hex n = hex_prefix (map hex_digit (radixpand (16, n)));
 
 
 (* char *)
 
-fun mk_char s =
-  let
-    val c =
-      if Symbol.is_ascii s then ord s
-      else if s = "\<newline>" then 10
-      else error ("Bad character: " ^ quote s);
-  in Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (c div 16), mk_nib (c mod 16)] end;
+fun mk_char_syntax n =
+  if n = 0 then Syntax.const @{const_name Groups.zero}
+  else Syntax.const @{const_syntax Char} $ Numeral.mk_num_syntax n;
+
+fun mk_char_syntax' c =
+  if Symbol.is_ascii c then mk_char_syntax (ord c)
+  else if c = "\<newline>" then mk_char_syntax 10
+  else error ("Bad character: " ^ quote c);
+
+fun plain_string_of str =
+  map fst (Lexicon.explode_str (str, Position.none));
+
+datatype character = Char of string | Ord of int | Unprintable;
 
 val specials = raw_explode "\\\"`'";
 
-fun dest_chr c1 c2 =
-  let val s = chr (dest_nib c1 * 16 + dest_nib c2) in
-    if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
-    then s
-    else if s = "\n" then "\<newline>"
-    else raise Match
-  end;
+fun dest_char_syntax c =
+  case try Numeral.dest_num_syntax c of
+    SOME n =>
+      if n < 256 then
+        let
+          val s = chr n
+        in
+          if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
+          then Char s
+          else if s = "\n" then Char "\<newline>"
+          else Ord n
+        end
+      else Unprintable
+  | NONE => Unprintable;
 
-fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
-  | dest_char _ = raise Match;
+fun dest_char_ast (Ast.Appl [Ast.Constant @{syntax_const "_Char"}, Ast.Constant s]) =
+      plain_string_of s
+  | dest_char_ast _ = raise Match;
 
-fun syntax_string ss =
-  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
-    Ast.Variable (Lexicon.implode_str ss)];
-
+fun char_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+      c $ char_tr [t] $ u
+  | char_tr [Free (str, _)] =
+      (case plain_string_of str of
+        [c] => mk_char_syntax' c
+      | _ => error ("Single character expected: " ^ str))
+  | char_tr ts = raise TERM ("char_tr", ts);
 
-fun char_ast_tr [Ast.Variable str] =
-      (case Lexicon.explode_str (str, Position.none) of
-        [(s, _)] => mk_char s
-      | _ => error ("Single character expected: " ^ str))
-  | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
-      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
-  | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
+fun char_ord_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+      c $ char_ord_tr [t] $ u
+  | char_ord_tr [Const (num, _)] =
+      (mk_char_syntax o #value o Lexicon.read_num) num
+  | char_ord_tr ts = raise TERM ("char_ord_tr", ts);
 
-fun char_ast_tr' [c1, c2] =
-      Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
-  | char_ast_tr' _ = raise Match;
+fun char_tr' [t] = (case dest_char_syntax t of
+        Char s => Syntax.const @{syntax_const "_Char"} $
+          Syntax.const (Lexicon.implode_str [s])
+      | Ord n => 
+          if n = 0
+          then Syntax.const @{const_syntax Groups.zero}
+          else Syntax.const @{syntax_const "_Char_ord"} $
+            Syntax.free (hex n)
+      | _ => raise Match)
+  | char_tr' _ = raise Match;
 
 
 (* string *)
 
-fun mk_string [] = Ast.Constant @{const_syntax Nil}
-  | mk_string (s :: ss) =
-      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char s, mk_string ss];
+fun mk_string_syntax [] = Syntax.const @{const_syntax Nil}
+  | mk_string_syntax (c :: cs) =
+      Syntax.const @{const_syntax Cons} $ mk_char_syntax' c $ mk_string_syntax cs;
 
-fun string_ast_tr [Ast.Variable str] =
-      (case Lexicon.explode_str (str, Position.none) of
-        [] =>
-          Ast.Appl
-            [Ast.Constant @{syntax_const "_constrain"},
-              Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
-      | ss => mk_string (map Symbol_Pos.symbol ss))
-  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
-      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
-  | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
+fun mk_string_ast ss =
+  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
+    Ast.Variable (Lexicon.implode_str ss)];
+
+fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+      c $ string_tr [t] $ u
+  | string_tr [Free (str, _)] =
+      mk_string_syntax (plain_string_of str)
+  | string_tr ts = raise TERM ("char_tr", ts);
 
 fun list_ast_tr' [args] =
       Ast.Appl [Ast.Constant @{syntax_const "_String"},
-        syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
+        (mk_string_ast o maps dest_char_ast o Ast.unfold_ast @{syntax_const "_args"}) args]
   | list_ast_tr' _ = raise Match;
 
 
@@ -87,11 +111,13 @@
 
 val _ =
   Theory.setup
-   (Sign.parse_ast_translation
-     [(@{syntax_const "_Char"}, K char_ast_tr),
-      (@{syntax_const "_String"}, K string_ast_tr)] #>
+   (Sign.parse_translation
+     [(@{syntax_const "_Char"}, K char_tr),
+      (@{syntax_const "_Char_ord"}, K char_ord_tr),
+      (@{syntax_const "_String"}, K string_tr)] #>
+    Sign.print_translation
+     [(@{const_syntax Char}, K char_tr')] #>
     Sign.print_ast_translation
-     [(@{const_syntax Char}, K char_ast_tr'),
-      (@{syntax_const "_list"}, K list_ast_tr')]);
+     [(@{syntax_const "_list"}, K list_ast_tr')]);
 
 end;
diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -53,17 +53,13 @@
 
 ML \<open>
   local
-    val mk_nib =
-      Syntax.const o Lexicon.mark_const o
-        fst o Term.dest_Const o HOLogic.mk_nibble;
-
     fun mk_char (s, pos) =
       let
         val c =
           if Symbol.is_ascii s then ord s
           else if s = "\<newline>" then 10
           else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
-      in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end;
+      in Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c end;
 
     fun mk_string [] = Const (@{const_syntax Nil}, @{typ string})
       | mk_string (s :: ss) =