model characters directly as range 0..255
authorhaftmann
Sat Mar 12 22:04:52 2016 +0100 (2016-03-12)
changeset 62597b3f2b8c906a6
parent 62596 cf79f8866bc3
child 62598 f26dc26f2161
model characters directly as range 0..255
* * *
operate on syntax terms rather than asts
NEWS
src/HOL/Code_Evaluation.thy
src/HOL/Divides.thy
src/HOL/HOLCF/Library/Char_Discrete.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Test.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Num.thy
src/HOL/Parity.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Statespace/state_fun.ML
src/HOL/String.thy
src/HOL/Tools/hologic.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/string_code.ML
src/HOL/Tools/string_syntax.ML
src/HOL/ex/Cartouche_Examples.thy
     1.1 --- a/NEWS	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/NEWS	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -53,6 +53,30 @@
     1.4  * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
     1.5  resemble the f.split naming convention, INCOMPATIBILITY.
     1.6  
     1.7 +* Characters (type char) are modelled as finite algebraic type
     1.8 +corresponding to {0..255}.
     1.9 +
    1.10 +  - Logical representation:
    1.11 +    * 0 is instantiated to the ASCII zero character.
    1.12 +    * All other characters are represented as »Char n«
    1.13 +      with n being a raw numeral expression less than 256.
    1.14 +    * Expressions of the form »Char n« with n greater than 255
    1.15 +      are non-canonical.
    1.16 +  - Printing and parsing:
    1.17 +    * Printable characters are printed and parsed as »CHR ''…''«
    1.18 +      (as before).
    1.19 +    * The ASCII zero character is printed and parsed as »0«.
    1.20 +    * All other canonical characters are printed as »CHAR 0xXX«
    1.21 +      with XX being the hexadecimal character code.  »CHAR n«
    1.22 +      is parsable for every numeral expression n.
    1.23 +    * Non-canonial characters have no special syntax and are
    1.24 +      printed as their logical representation.
    1.25 +  - Explicit conversions from and to the natural numbers are
    1.26 +    provided as char_of_nat, nat_of_char (as before).
    1.27 +  - The auxiliary nibble type has been discontinued.
    1.28 +
    1.29 +INCOMPATIBILITY.
    1.30 +
    1.31  * Multiset membership is now expressed using set_mset rather than count.
    1.32  
    1.33    - Expressions "count M a > 0" and similar simplify to membership
     2.1 --- a/src/HOL/Code_Evaluation.thy	Fri Mar 11 17:20:14 2016 +0100
     2.2 +++ b/src/HOL/Code_Evaluation.thy	Sat Mar 12 22:04:52 2016 +0100
     2.3 @@ -105,12 +105,14 @@
     2.4    "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
     2.5    "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
     2.6  
     2.7 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
     2.8 -  "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
     2.9 -   Code_Evaluation.App (Code_Evaluation.App
    2.10 -    (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    2.11 -      (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
    2.12 -  by (subst term_of_anything) rule 
    2.13 +definition case_char :: "'a \<Rightarrow> (num \<Rightarrow> 'a) \<Rightarrow> char \<Rightarrow> 'a"
    2.14 +  where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))"
    2.15 +
    2.16 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]:
    2.17 +  "term_of =
    2.18 +    case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char)))
    2.19 +    (\<lambda>k. App (Const (STR ''String.Char'') (TYPEREP(num \<Rightarrow> char))) (term_of k))"
    2.20 +  by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq])
    2.21  
    2.22  lemma term_of_string [code]:
    2.23     "term_of s = App (Const (STR ''STR'')
    2.24 @@ -133,7 +135,7 @@
    2.25     else
    2.26       App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer))
    2.27         (term_of (- i)))"
    2.28 -by(rule term_of_anything[THEN meta_eq_to_obj_eq])
    2.29 +  by (rule term_of_anything [THEN meta_eq_to_obj_eq])
    2.30  
    2.31  code_reserved Eval HOLogic
    2.32  
     3.1 --- a/src/HOL/Divides.thy	Fri Mar 11 17:20:14 2016 +0100
     3.2 +++ b/src/HOL/Divides.thy	Sat Mar 12 22:04:52 2016 +0100
     3.3 @@ -1635,6 +1635,37 @@
     3.4    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
     3.5    by (simp_all add: snd_divmod)
     3.6  
     3.7 +lemma cut_eq_simps: -- \<open>rewriting equivalence on @{text "n mod 2 ^ q"}\<close>
     3.8 +  fixes m n q :: num
     3.9 +  shows
    3.10 +    "numeral n mod numeral Num.One = (0::nat)
    3.11 +      \<longleftrightarrow> True"
    3.12 +    "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
    3.13 +      \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
    3.14 +    "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
    3.15 +      \<longleftrightarrow> False"
    3.16 +    "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
    3.17 +      \<longleftrightarrow> True"
    3.18 +    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    3.19 +      \<longleftrightarrow> True"
    3.20 +    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    3.21 +      \<longleftrightarrow> False"
    3.22 +    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    3.23 +      \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
    3.24 +    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    3.25 +      \<longleftrightarrow> False"
    3.26 +    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    3.27 +      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    3.28 +    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    3.29 +      \<longleftrightarrow> False"
    3.30 +    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    3.31 +      \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
    3.32 +    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    3.33 +      \<longleftrightarrow> False"
    3.34 +    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    3.35 +      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    3.36 +  by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
    3.37 +
    3.38  
    3.39  subsection \<open>Division on @{typ int}\<close>
    3.40  
     4.1 --- a/src/HOL/HOLCF/Library/Char_Discrete.thy	Fri Mar 11 17:20:14 2016 +0100
     4.2 +++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Sat Mar 12 22:04:52 2016 +0100
     4.3 @@ -8,52 +8,6 @@
     4.4  imports HOLCF
     4.5  begin
     4.6  
     4.7 -subsection \<open>Discrete cpo instance for @{typ nibble}.\<close>
     4.8 -
     4.9 -instantiation nibble :: discrete_cpo
    4.10 -begin
    4.11 -
    4.12 -definition below_nibble_def:
    4.13 -  "(x::nibble) \<sqsubseteq> y \<longleftrightarrow> x = y"
    4.14 -
    4.15 -instance proof
    4.16 -qed (rule below_nibble_def)
    4.17 -
    4.18 -end
    4.19 -
    4.20 -text \<open>
    4.21 -  TODO: implement a command to automate discrete predomain instances.
    4.22 -\<close>
    4.23 -
    4.24 -instantiation nibble :: predomain
    4.25 -begin
    4.26 -
    4.27 -definition
    4.28 -  "(liftemb :: nibble u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
    4.29 -
    4.30 -definition
    4.31 -  "(liftprj :: udom u \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
    4.32 -
    4.33 -definition
    4.34 -  "liftdefl \<equiv> (\<lambda>(t::nibble itself). LIFTDEFL(nibble discr))"
    4.35 -
    4.36 -instance proof
    4.37 -  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nibble u)"
    4.38 -    unfolding liftemb_nibble_def liftprj_nibble_def
    4.39 -    apply (rule ep_pair_comp)
    4.40 -    apply (rule ep_pair_u_map)
    4.41 -    apply (simp add: ep_pair.intro)
    4.42 -    apply (rule predomain_ep)
    4.43 -    done
    4.44 -  show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom u \<rightarrow> nibble u)"
    4.45 -    unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def
    4.46 -    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    4.47 -    apply (simp add: ID_def [symmetric] u_map_ID)
    4.48 -    done
    4.49 -qed
    4.50 -
    4.51 -end
    4.52 -
    4.53  subsection \<open>Discrete cpo instance for @{typ char}.\<close>
    4.54  
    4.55  instantiation char :: discrete_cpo
    4.56 @@ -100,146 +54,4 @@
    4.57  
    4.58  end
    4.59  
    4.60 -subsection \<open>Using chars with Fixrec\<close>
    4.61 -
    4.62 -definition match_Char :: "char \<rightarrow> (nibble \<rightarrow> nibble \<rightarrow> 'a match) \<rightarrow> 'a match"
    4.63 -  where "match_Char = (\<Lambda> c k. case c of Char a b \<Rightarrow> k\<cdot>a\<cdot>b)"
    4.64 -
    4.65 -lemma match_Char_simps [simp]:
    4.66 -  "match_Char\<cdot>(Char a b)\<cdot>k = k\<cdot>a\<cdot>b"
    4.67 -by (simp add: match_Char_def)
    4.68 -
    4.69 -definition match_Nibble0 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.70 -  where "match_Nibble0 = (\<Lambda> c k. if c = Nibble0 then k else Fixrec.fail)"
    4.71 -
    4.72 -definition match_Nibble1 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.73 -  where "match_Nibble1 = (\<Lambda> c k. if c = Nibble1 then k else Fixrec.fail)"
    4.74 -
    4.75 -definition match_Nibble2 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.76 -  where "match_Nibble2 = (\<Lambda> c k. if c = Nibble2 then k else Fixrec.fail)"
    4.77 -
    4.78 -definition match_Nibble3 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.79 -  where "match_Nibble3 = (\<Lambda> c k. if c = Nibble3 then k else Fixrec.fail)"
    4.80 -
    4.81 -definition match_Nibble4 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.82 -  where "match_Nibble4 = (\<Lambda> c k. if c = Nibble4 then k else Fixrec.fail)"
    4.83 -
    4.84 -definition match_Nibble5 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.85 -  where "match_Nibble5 = (\<Lambda> c k. if c = Nibble5 then k else Fixrec.fail)"
    4.86 -
    4.87 -definition match_Nibble6 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.88 -  where "match_Nibble6 = (\<Lambda> c k. if c = Nibble6 then k else Fixrec.fail)"
    4.89 -
    4.90 -definition match_Nibble7 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.91 -  where "match_Nibble7 = (\<Lambda> c k. if c = Nibble7 then k else Fixrec.fail)"
    4.92 -
    4.93 -definition match_Nibble8 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.94 -  where "match_Nibble8 = (\<Lambda> c k. if c = Nibble8 then k else Fixrec.fail)"
    4.95 -
    4.96 -definition match_Nibble9 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
    4.97 -  where "match_Nibble9 = (\<Lambda> c k. if c = Nibble9 then k else Fixrec.fail)"
    4.98 -
    4.99 -definition match_NibbleA :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   4.100 -  where "match_NibbleA = (\<Lambda> c k. if c = NibbleA then k else Fixrec.fail)"
   4.101 -
   4.102 -definition match_NibbleB :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   4.103 -  where "match_NibbleB = (\<Lambda> c k. if c = NibbleB then k else Fixrec.fail)"
   4.104 -
   4.105 -definition match_NibbleC :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   4.106 -  where "match_NibbleC = (\<Lambda> c k. if c = NibbleC then k else Fixrec.fail)"
   4.107 -
   4.108 -definition match_NibbleD :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   4.109 -  where "match_NibbleD = (\<Lambda> c k. if c = NibbleD then k else Fixrec.fail)"
   4.110 -
   4.111 -definition match_NibbleE :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   4.112 -  where "match_NibbleE = (\<Lambda> c k. if c = NibbleE then k else Fixrec.fail)"
   4.113 -
   4.114 -definition match_NibbleF :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   4.115 -  where "match_NibbleF = (\<Lambda> c k. if c = NibbleF then k else Fixrec.fail)"
   4.116 -
   4.117 -lemma match_Nibble0_simps [simp]:
   4.118 -  "match_Nibble0\<cdot>c\<cdot>k = (if c = Nibble0 then k else Fixrec.fail)"
   4.119 -by (simp add: match_Nibble0_def)
   4.120 -
   4.121 -lemma match_Nibble1_simps [simp]:
   4.122 -  "match_Nibble1\<cdot>c\<cdot>k = (if c = Nibble1 then k else Fixrec.fail)"
   4.123 -by (simp add: match_Nibble1_def)
   4.124 -
   4.125 -lemma match_Nibble2_simps [simp]:
   4.126 -  "match_Nibble2\<cdot>c\<cdot>k = (if c = Nibble2 then k else Fixrec.fail)"
   4.127 -by (simp add: match_Nibble2_def)
   4.128 -
   4.129 -lemma match_Nibble3_simps [simp]:
   4.130 -  "match_Nibble3\<cdot>c\<cdot>k = (if c = Nibble3 then k else Fixrec.fail)"
   4.131 -by (simp add: match_Nibble3_def)
   4.132 -
   4.133 -lemma match_Nibble4_simps [simp]:
   4.134 -  "match_Nibble4\<cdot>c\<cdot>k = (if c = Nibble4 then k else Fixrec.fail)"
   4.135 -by (simp add: match_Nibble4_def)
   4.136 -
   4.137 -lemma match_Nibble5_simps [simp]:
   4.138 -  "match_Nibble5\<cdot>c\<cdot>k = (if c = Nibble5 then k else Fixrec.fail)"
   4.139 -by (simp add: match_Nibble5_def)
   4.140 -
   4.141 -lemma match_Nibble6_simps [simp]:
   4.142 -  "match_Nibble6\<cdot>c\<cdot>k = (if c = Nibble6 then k else Fixrec.fail)"
   4.143 -by (simp add: match_Nibble6_def)
   4.144 -
   4.145 -lemma match_Nibble7_simps [simp]:
   4.146 -  "match_Nibble7\<cdot>c\<cdot>k = (if c = Nibble7 then k else Fixrec.fail)"
   4.147 -by (simp add: match_Nibble7_def)
   4.148 -
   4.149 -lemma match_Nibble8_simps [simp]:
   4.150 -  "match_Nibble8\<cdot>c\<cdot>k = (if c = Nibble8 then k else Fixrec.fail)"
   4.151 -by (simp add: match_Nibble8_def)
   4.152 -
   4.153 -lemma match_Nibble9_simps [simp]:
   4.154 -  "match_Nibble9\<cdot>c\<cdot>k = (if c = Nibble9 then k else Fixrec.fail)"
   4.155 -by (simp add: match_Nibble9_def)
   4.156 -
   4.157 -lemma match_NibbleA_simps [simp]:
   4.158 -  "match_NibbleA\<cdot>c\<cdot>k = (if c = NibbleA then k else Fixrec.fail)"
   4.159 -by (simp add: match_NibbleA_def)
   4.160 -
   4.161 -lemma match_NibbleB_simps [simp]:
   4.162 -  "match_NibbleB\<cdot>c\<cdot>k = (if c = NibbleB then k else Fixrec.fail)"
   4.163 -by (simp add: match_NibbleB_def)
   4.164 -
   4.165 -lemma match_NibbleC_simps [simp]:
   4.166 -  "match_NibbleC\<cdot>c\<cdot>k = (if c = NibbleC then k else Fixrec.fail)"
   4.167 -by (simp add: match_NibbleC_def)
   4.168 -
   4.169 -lemma match_NibbleD_simps [simp]:
   4.170 -  "match_NibbleD\<cdot>c\<cdot>k = (if c = NibbleD then k else Fixrec.fail)"
   4.171 -by (simp add: match_NibbleD_def)
   4.172 -
   4.173 -lemma match_NibbleE_simps [simp]:
   4.174 -  "match_NibbleE\<cdot>c\<cdot>k = (if c = NibbleE then k else Fixrec.fail)"
   4.175 -by (simp add: match_NibbleE_def)
   4.176 -
   4.177 -lemma match_NibbleF_simps [simp]:
   4.178 -  "match_NibbleF\<cdot>c\<cdot>k = (if c = NibbleF then k else Fixrec.fail)"
   4.179 -by (simp add: match_NibbleF_def)
   4.180 -
   4.181 -setup \<open>
   4.182 -  Fixrec.add_matchers
   4.183 -    [ (@{const_name Char}, @{const_name match_Char}),
   4.184 -      (@{const_name Nibble0}, @{const_name match_Nibble0}),
   4.185 -      (@{const_name Nibble1}, @{const_name match_Nibble1}),
   4.186 -      (@{const_name Nibble2}, @{const_name match_Nibble2}),
   4.187 -      (@{const_name Nibble3}, @{const_name match_Nibble3}),
   4.188 -      (@{const_name Nibble4}, @{const_name match_Nibble4}),
   4.189 -      (@{const_name Nibble5}, @{const_name match_Nibble5}),
   4.190 -      (@{const_name Nibble6}, @{const_name match_Nibble6}),
   4.191 -      (@{const_name Nibble7}, @{const_name match_Nibble7}),
   4.192 -      (@{const_name Nibble8}, @{const_name match_Nibble8}),
   4.193 -      (@{const_name Nibble9}, @{const_name match_Nibble9}),
   4.194 -      (@{const_name NibbleA}, @{const_name match_NibbleA}),
   4.195 -      (@{const_name NibbleB}, @{const_name match_NibbleB}),
   4.196 -      (@{const_name NibbleC}, @{const_name match_NibbleC}),
   4.197 -      (@{const_name NibbleD}, @{const_name match_NibbleD}),
   4.198 -      (@{const_name NibbleE}, @{const_name match_NibbleE}),
   4.199 -      (@{const_name NibbleF}, @{const_name match_NibbleF}) ]
   4.200 -\<close>
   4.201 -
   4.202  end
     5.1 --- a/src/HOL/Library/Cardinality.thy	Fri Mar 11 17:20:14 2016 +0100
     5.2 +++ b/src/HOL/Library/Cardinality.thy	Sat Mar 12 22:04:52 2016 +0100
     5.3 @@ -149,15 +149,6 @@
     5.4    finally show ?thesis .
     5.5  qed
     5.6  
     5.7 -lemma card_nibble: "CARD(nibble) = 16"
     5.8 -unfolding UNIV_nibble by simp
     5.9 -
    5.10 -lemma card_UNIV_char: "CARD(char) = 256"
    5.11 -proof -
    5.12 -  have "inj (\<lambda>(x, y). Char x y)" by(auto intro: injI)
    5.13 -  thus ?thesis unfolding UNIV_char by(simp add: card_image card_nibble)
    5.14 -qed
    5.15 -
    5.16  lemma card_literal: "CARD(String.literal) = 0"
    5.17  by(simp add: card_eq_0_iff infinite_literal)
    5.18  
    5.19 @@ -263,12 +254,6 @@
    5.20  instance by(intro_classes)(simp_all add: card_UNIV_bool_def finite_UNIV_bool_def)
    5.21  end
    5.22  
    5.23 -instantiation nibble :: card_UNIV begin
    5.24 -definition "finite_UNIV = Phantom(nibble) True"
    5.25 -definition "card_UNIV = Phantom(nibble) 16"
    5.26 -instance by(intro_classes)(simp_all add: card_UNIV_nibble_def card_nibble finite_UNIV_nibble_def)
    5.27 -end
    5.28 -
    5.29  instantiation char :: card_UNIV begin
    5.30  definition "finite_UNIV = Phantom(char) True"
    5.31  definition "card_UNIV = Phantom(char) 256"
     6.1 --- a/src/HOL/Library/Char_ord.thy	Fri Mar 11 17:20:14 2016 +0100
     6.2 +++ b/src/HOL/Library/Char_ord.thy	Sat Mar 12 22:04:52 2016 +0100
     6.3 @@ -8,28 +8,6 @@
     6.4  imports Main
     6.5  begin
     6.6  
     6.7 -instantiation nibble :: linorder
     6.8 -begin
     6.9 -
    6.10 -definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    6.11 -definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    6.12 -
    6.13 -instance
    6.14 -  by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
    6.15 -
    6.16 -end
    6.17 -
    6.18 -instantiation nibble :: distrib_lattice
    6.19 -begin
    6.20 -
    6.21 -definition "(inf :: nibble \<Rightarrow> _) = min"
    6.22 -definition "(sup :: nibble \<Rightarrow> _) = max"
    6.23 -
    6.24 -instance
    6.25 -  by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
    6.26 -
    6.27 -end
    6.28 -
    6.29  instantiation char :: linorder
    6.30  begin
    6.31  
    6.32 @@ -37,40 +15,22 @@
    6.33  definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    6.34  
    6.35  instance
    6.36 -  by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
    6.37 +  by standard (auto simp add: less_eq_char_def less_char_def)
    6.38  
    6.39  end
    6.40  
    6.41 -lemma less_eq_char_Char:
    6.42 -  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    6.43 -proof -
    6.44 -  {
    6.45 -    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
    6.46 -      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
    6.47 -    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
    6.48 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
    6.49 -  }
    6.50 -  note * = this
    6.51 -  show ?thesis
    6.52 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    6.53 -    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: *)
    6.54 -qed
    6.55 +lemma less_eq_char_simps:
    6.56 +  "(0 :: char) \<le> c"
    6.57 +  "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
    6.58 +  "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
    6.59 +  by (simp_all add: Char_def less_eq_char_def)
    6.60  
    6.61 -lemma less_char_Char:
    6.62 -  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    6.63 -proof -
    6.64 -  {
    6.65 -    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
    6.66 -      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
    6.67 -    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
    6.68 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
    6.69 -  }
    6.70 -  note * = this
    6.71 -  show ?thesis
    6.72 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    6.73 -    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: *)
    6.74 -qed
    6.75 -
    6.76 +lemma less_char_simps:
    6.77 +  "\<not> c < (0 :: char)"
    6.78 +  "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
    6.79 +  "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
    6.80 +  by (simp_all add: Char_def less_char_def)
    6.81 +  
    6.82  instantiation char :: distrib_lattice
    6.83  begin
    6.84  
    6.85 @@ -111,14 +71,4 @@
    6.86  lifting_update literal.lifting
    6.87  lifting_forget literal.lifting
    6.88  
    6.89 -text \<open>Legacy aliasses\<close>
    6.90 -
    6.91 -lemmas nibble_less_eq_def = less_eq_nibble_def
    6.92 -lemmas nibble_less_def = less_nibble_def
    6.93 -lemmas char_less_eq_def = less_eq_char_def
    6.94 -lemmas char_less_def = less_char_def
    6.95 -lemmas char_less_eq_simp = less_eq_char_Char
    6.96 -lemmas char_less_simp = less_char_Char
    6.97 -
    6.98  end
    6.99 -
     7.1 --- a/src/HOL/Library/Code_Char.thy	Fri Mar 11 17:20:14 2016 +0100
     7.2 +++ b/src/HOL/Library/Code_Char.thy	Sat Mar 12 22:04:52 2016 +0100
     7.3 @@ -21,7 +21,17 @@
     7.4  \<close>
     7.5  
     7.6  code_printing
     7.7 -  class_instance char :: equal \<rightharpoonup>
     7.8 +  constant integer_of_char \<rightharpoonup>
     7.9 +    (SML) "!(IntInf.fromInt o Char.ord)"
    7.10 +    and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
    7.11 +    and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
    7.12 +    and (Scala) "BigInt(_.toInt)"
    7.13 +| constant char_of_integer \<rightharpoonup>
    7.14 +    (SML) "!(Char.chr o IntInf.toInt)"
    7.15 +    and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
    7.16 +    and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
    7.17 +    and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))"
    7.18 +| class_instance char :: equal \<rightharpoonup>
    7.19      (Haskell) -
    7.20  | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
    7.21      (SML) "!((_ : char) = _)"
    7.22 @@ -54,45 +64,8 @@
    7.23      and (Haskell) "_"
    7.24      and (Scala) "!(_.toList)"
    7.25  
    7.26 -
    7.27 -definition integer_of_char :: "char \<Rightarrow> integer"
    7.28 -where
    7.29 -  "integer_of_char = integer_of_nat o nat_of_char"
    7.30 -
    7.31 -definition char_of_integer :: "integer \<Rightarrow> char"
    7.32 -where
    7.33 -  "char_of_integer = char_of_nat \<circ> nat_of_integer"
    7.34 -
    7.35 -lemma [code]:
    7.36 -  "nat_of_char = nat_of_integer o integer_of_char"
    7.37 -  by (simp add: integer_of_char_def fun_eq_iff)
    7.38 -
    7.39 -lemma [code]:
    7.40 -  "char_of_nat = char_of_integer o integer_of_nat"
    7.41 -  by (simp add: char_of_integer_def fun_eq_iff)
    7.42 -
    7.43 -lemmas integer_of_char_code [code] =
    7.44 -  nat_of_char_simps[
    7.45 -    THEN arg_cong[where f="integer_of_nat"],
    7.46 -    unfolded integer_of_nat_numeral integer_of_nat_1 integer_of_nat_0,
    7.47 -    folded fun_cong[OF integer_of_char_def, unfolded o_apply]]
    7.48 -
    7.49 -lemma char_of_integer_code [code]:
    7.50 -  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
    7.51 -  by (simp add: char_of_integer_def enum_char_unfold)
    7.52 -
    7.53  code_printing
    7.54 -  constant integer_of_char \<rightharpoonup>
    7.55 -    (SML) "!(IntInf.fromInt o Char.ord)"
    7.56 -    and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
    7.57 -    and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
    7.58 -    and (Scala) "BigInt(_.toInt)"
    7.59 -| constant char_of_integer \<rightharpoonup>
    7.60 -    (SML) "!(Char.chr o IntInf.toInt)"
    7.61 -    and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
    7.62 -    and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
    7.63 -    and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))"
    7.64 -| constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
    7.65 +  constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
    7.66      (SML) "!((_ : char) <= _)"
    7.67      and (OCaml) "!((_ : char) <= _)"
    7.68      and (Haskell) infix 4 "<="
     8.1 --- a/src/HOL/Library/Code_Test.thy	Fri Mar 11 17:20:14 2016 +0100
     8.2 +++ b/src/HOL/Library/Code_Test.thy	Sat Mar 12 22:04:52 2016 +0100
     8.3 @@ -83,8 +83,8 @@
     8.4  
     8.5  definition list where "list f xs = map (node \<circ> f) xs"
     8.6  
     8.7 -definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])"
     8.8 -definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])"
     8.9 +definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])"
    8.10 +definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])"
    8.11  definition XY :: yxml_of_term where "XY = yot_append X Y"
    8.12  definition XYX :: yxml_of_term where "XYX = yot_append XY X"
    8.13  
     9.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Mar 11 17:20:14 2016 +0100
     9.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sat Mar 12 22:04:52 2016 +0100
     9.3 @@ -52,6 +52,8 @@
     9.4  
     9.5  setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close>
     9.6  setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close>
     9.7 +setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Char}]\<close>
     9.8 +setup \<open>Predicate_Compile_Data.keep_functions [@{const_name Char}]\<close>
     9.9  
    9.10  setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}]\<close>
    9.11  
    10.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Mar 11 17:20:14 2016 +0100
    10.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Mar 12 22:04:52 2016 +0100
    10.3 @@ -14,6 +14,11 @@
    10.4  nitpick_params [verbose, card = 1-8, max_potential = 0,
    10.5                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    10.6  
    10.7 +datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3
    10.8 +  | Nibble4 | Nibble5 | Nibble6 | Nibble7
    10.9 +  | Nibble8 | Nibble9 | NibbleA | NibbleB
   10.10 +  | NibbleC | NibbleD | NibbleE | NibbleF
   10.11 +
   10.12  primrec rot where
   10.13  "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
   10.14  "rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
    11.1 --- a/src/HOL/Num.thy	Fri Mar 11 17:20:14 2016 +0100
    11.2 +++ b/src/HOL/Num.thy	Sat Mar 12 22:04:52 2016 +0100
    11.3 @@ -297,12 +297,9 @@
    11.4  
    11.5  typed_print_translation \<open>
    11.6    let
    11.7 -    fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
    11.8 -      | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
    11.9 -      | dest_num (Const (@{const_syntax One}, _)) = 1;
   11.10      fun num_tr' ctxt T [n] =
   11.11        let
   11.12 -        val k = dest_num n;
   11.13 +        val k = Numeral.dest_num_syntax n;
   11.14          val t' =
   11.15            Syntax.const @{syntax_const "_Numeral"} $
   11.16              Syntax.free (string_of_int k);
    12.1 --- a/src/HOL/Parity.thy	Fri Mar 11 17:20:14 2016 +0100
    12.2 +++ b/src/HOL/Parity.thy	Sat Mar 12 22:04:52 2016 +0100
    12.3 @@ -180,6 +180,21 @@
    12.4    "odd (n :: nat) \<Longrightarrow> 0 < n"
    12.5    by (auto elim: oddE)
    12.6  
    12.7 +lemma Suc_double_not_eq_double:
    12.8 +  fixes m n :: nat
    12.9 +  shows "Suc (2 * m) \<noteq> 2 * n"
   12.10 +proof
   12.11 +  assume "Suc (2 * m) = 2 * n"
   12.12 +  moreover have "odd (Suc (2 * m))" and "even (2 * n)"
   12.13 +    by simp_all
   12.14 +  ultimately show False by simp
   12.15 +qed
   12.16 +
   12.17 +lemma double_not_eq_Suc_double:
   12.18 +  fixes m n :: nat
   12.19 +  shows "2 * m \<noteq> Suc (2 * n)"
   12.20 +  using Suc_double_not_eq_double [of n m] by simp
   12.21 +
   12.22  lemma even_diff_iff [simp]:
   12.23    fixes k l :: int
   12.24    shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
    13.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 17:20:14 2016 +0100
    13.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Mar 12 22:04:52 2016 +0100
    13.3 @@ -379,42 +379,13 @@
    13.4  
    13.5  end
    13.6  
    13.7 -instantiation nibble :: check_all
    13.8 +(* FIXME instantiation char :: check_all
    13.9  begin
   13.10  
   13.11  definition
   13.12 -  "check_all f =
   13.13 -    f (Code_Evaluation.valtermify Nibble0) orelse
   13.14 -    f (Code_Evaluation.valtermify Nibble1) orelse
   13.15 -    f (Code_Evaluation.valtermify Nibble2) orelse
   13.16 -    f (Code_Evaluation.valtermify Nibble3) orelse
   13.17 -    f (Code_Evaluation.valtermify Nibble4) orelse
   13.18 -    f (Code_Evaluation.valtermify Nibble5) orelse
   13.19 -    f (Code_Evaluation.valtermify Nibble6) orelse
   13.20 -    f (Code_Evaluation.valtermify Nibble7) orelse
   13.21 -    f (Code_Evaluation.valtermify Nibble8) orelse
   13.22 -    f (Code_Evaluation.valtermify Nibble9) orelse
   13.23 -    f (Code_Evaluation.valtermify NibbleA) orelse
   13.24 -    f (Code_Evaluation.valtermify NibbleB) orelse
   13.25 -    f (Code_Evaluation.valtermify NibbleC) orelse
   13.26 -    f (Code_Evaluation.valtermify NibbleD) orelse
   13.27 -    f (Code_Evaluation.valtermify NibbleE) orelse
   13.28 -    f (Code_Evaluation.valtermify NibbleF)"
   13.29 -
   13.30 -definition enum_term_of_nibble :: "nibble itself => unit => term list"
   13.31 -where
   13.32 -  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
   13.33 -
   13.34 -instance ..
   13.35 -
   13.36 -end
   13.37 -
   13.38 -
   13.39 -instantiation char :: check_all
   13.40 -begin
   13.41 -
   13.42 -definition
   13.43 -  "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 ()))))"
   13.44 +  "check_all f = check_all (%(x, t1). check_all (%(y, t2).
   13.45 +     f (Char x y, %_. Code_Evaluation.App
   13.46 +       (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
   13.47  
   13.48  definition enum_term_of_char :: "char itself => unit => term list"
   13.49  where
   13.50 @@ -422,8 +393,7 @@
   13.51  
   13.52  instance ..
   13.53  
   13.54 -end
   13.55 -
   13.56 +end *)
   13.57  
   13.58  instantiation option :: (check_all) check_all
   13.59  begin
   13.60 @@ -624,13 +594,7 @@
   13.61  
   13.62  ML_file "Tools/Quickcheck/abstract_generators.ML"
   13.63  
   13.64 -lemma check_all_char [code]:
   13.65 -  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
   13.66 -     f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
   13.67 -       (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
   13.68 -  by (simp add: check_all_char_def)
   13.69 -
   13.70 -instantiation char :: full_exhaustive
   13.71 +(* FIXME instantiation char :: full_exhaustive
   13.72  begin
   13.73  
   13.74  definition full_exhaustive_char
   13.75 @@ -648,7 +612,7 @@
   13.76  
   13.77  instance ..
   13.78  
   13.79 -end
   13.80 +end *)
   13.81  
   13.82  hide_fact (open) orelse_def
   13.83  no_notation orelse (infixr "orelse" 55)
    14.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Mar 11 17:20:14 2016 +0100
    14.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Mar 12 22:04:52 2016 +0100
    14.3 @@ -77,7 +77,8 @@
    14.4  
    14.5  fun string_eq_simp_tac ctxt =
    14.6    simp_tac (put_simpset HOL_basic_ss ctxt
    14.7 -    addsimps (@{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms simp_thms})
    14.8 +    addsimps @{thms list.inject list.distinct Char_eq_Char_iff
    14.9 +      cut_eq_simps simp_thms}
   14.10      addsimprocs [lazy_conj_simproc]
   14.11      |> Simplifier.add_cong @{thm block_conj_cong});
   14.12  
   14.13 @@ -85,7 +86,7 @@
   14.14  
   14.15  val lookup_ss =
   14.16    simpset_of (put_simpset HOL_basic_ss @{context}
   14.17 -    addsimps (@{thms list.inject} @ @{thms char.inject}
   14.18 +    addsimps (@{thms list.inject} @ @{thms Char_eq_Char_iff}
   14.19        @ @{thms list.distinct} @ @{thms simp_thms}
   14.20        @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
   14.21          @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
   14.22 @@ -162,7 +163,7 @@
   14.23  val meta_ext = @{thm StateFun.meta_ext};
   14.24  val ss' =
   14.25    simpset_of (put_simpset HOL_ss @{context} addsimps
   14.26 -    (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
   14.27 +    (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms Char_eq_Char_iff}
   14.28        @ @{thms list.distinct})
   14.29      addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
   14.30      |> fold Simplifier.add_cong @{thms block_conj_cong});
    15.1 --- a/src/HOL/String.thy	Fri Mar 11 17:20:14 2016 +0100
    15.2 +++ b/src/HOL/String.thy	Sat Mar 12 22:04:52 2016 +0100
    15.3 @@ -56,7 +56,7 @@
    15.4    by (simp add: char_of_nat_def Abs_char_inject)
    15.5  
    15.6  lemma inj_on_char_of_nat [simp]:
    15.7 -  "inj_on char_of_nat {0..<256}"
    15.8 +  "inj_on char_of_nat {..<256}"
    15.9    by (rule inj_onI) simp
   15.10  
   15.11  lemma nat_of_char_mod_256 [simp]:
   15.12 @@ -72,197 +72,143 @@
   15.13  qed
   15.14  
   15.15  lemma UNIV_char_of_nat:
   15.16 -  "UNIV = char_of_nat ` {0..<256}"
   15.17 +  "UNIV = char_of_nat ` {..<256}"
   15.18  proof -
   15.19    { fix c
   15.20 -    have "c \<in> char_of_nat ` {0..<256}"
   15.21 +    have "c \<in> char_of_nat ` {..<256}"
   15.22        by (cases c) auto
   15.23    } then show ?thesis by auto
   15.24  qed
   15.25  
   15.26 -
   15.27 -subsubsection \<open>Traditional concrete representation of characters\<close>
   15.28 -
   15.29 -datatype (plugins del: transfer) nibble =
   15.30 -    Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
   15.31 -  | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
   15.32 +lemma card_UNIV_char:
   15.33 +  "card (UNIV :: char set) = 256"
   15.34 +  by (auto simp add: UNIV_char_of_nat card_image)
   15.35  
   15.36 -lemma UNIV_nibble:
   15.37 -  "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
   15.38 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
   15.39 -proof (rule UNIV_eq_I)
   15.40 -  fix x show "x \<in> ?A" by (cases x) simp_all
   15.41 -qed
   15.42 +lemma range_nat_of_char:
   15.43 +  "range nat_of_char = {..<256}"
   15.44 +  by (auto simp add: UNIV_char_of_nat image_image image_def)
   15.45  
   15.46 -lemma size_nibble [code, simp]:
   15.47 -  "size_nibble (x::nibble) = 0"
   15.48 -  "size (x::nibble) = 0"
   15.49 -  by (cases x, simp_all)+
   15.50  
   15.51 -instantiation nibble :: enum
   15.52 +subsubsection \<open>Character literals as variant of numerals\<close>
   15.53 +
   15.54 +instantiation char :: zero
   15.55  begin
   15.56  
   15.57 -definition
   15.58 -  "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
   15.59 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
   15.60 +definition zero_char :: char
   15.61 +  where "0 = char_of_nat 0"
   15.62  
   15.63 -definition
   15.64 -  "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
   15.65 -     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
   15.66 -
   15.67 -definition
   15.68 -  "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
   15.69 -     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
   15.70 -
   15.71 -instance proof
   15.72 -qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
   15.73 +instance ..
   15.74  
   15.75  end
   15.76  
   15.77 -lemma card_UNIV_nibble:
   15.78 -  "card (UNIV :: nibble set) = 16"
   15.79 -  by (simp add: card_UNIV_length_enum enum_nibble_def)
   15.80 +definition Char :: "num \<Rightarrow> char"
   15.81 +  where "Char k = char_of_nat (numeral k)"
   15.82 +
   15.83 +code_datatype "0 :: char" Char
   15.84 +
   15.85 +lemma nat_of_char_zero [simp]:
   15.86 +  "nat_of_char 0 = 0"
   15.87 +  by (simp add: zero_char_def)
   15.88 +
   15.89 +lemma nat_of_char_Char [simp]:
   15.90 +  "nat_of_char (Char k) = numeral k mod 256"
   15.91 +  by (simp add: Char_def)
   15.92  
   15.93 -primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
   15.94 +lemma Char_eq_Char_iff [simp]:
   15.95 +  "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
   15.96 +proof -
   15.97 +  have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
   15.98 +    by (rule sym, rule inj_eq) (fact inj_nat_of_char)
   15.99 +  also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
  15.100 +    by (simp only: Char_def nat_of_char_of_nat)
  15.101 +  finally show ?thesis .
  15.102 +qed
  15.103 +
  15.104 +lemma zero_eq_Char_iff [simp]:
  15.105 +  "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
  15.106 +  by (auto simp add: zero_char_def Char_def)
  15.107 +
  15.108 +lemma Char_eq_zero_iff [simp]:
  15.109 +  "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
  15.110 +  by (auto simp add: zero_char_def Char_def) 
  15.111 +
  15.112 +definition integer_of_char :: "char \<Rightarrow> integer"
  15.113  where
  15.114 -  "nat_of_nibble Nibble0 = 0"
  15.115 -| "nat_of_nibble Nibble1 = 1"
  15.116 -| "nat_of_nibble Nibble2 = 2"
  15.117 -| "nat_of_nibble Nibble3 = 3"
  15.118 -| "nat_of_nibble Nibble4 = 4"
  15.119 -| "nat_of_nibble Nibble5 = 5"
  15.120 -| "nat_of_nibble Nibble6 = 6"
  15.121 -| "nat_of_nibble Nibble7 = 7"
  15.122 -| "nat_of_nibble Nibble8 = 8"
  15.123 -| "nat_of_nibble Nibble9 = 9"
  15.124 -| "nat_of_nibble NibbleA = 10"
  15.125 -| "nat_of_nibble NibbleB = 11"
  15.126 -| "nat_of_nibble NibbleC = 12"
  15.127 -| "nat_of_nibble NibbleD = 13"
  15.128 -| "nat_of_nibble NibbleE = 14"
  15.129 -| "nat_of_nibble NibbleF = 15"
  15.130 +  "integer_of_char = integer_of_nat \<circ> nat_of_char"
  15.131  
  15.132 -definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
  15.133 -  "nibble_of_nat n = Enum.enum ! (n mod 16)"
  15.134 +definition char_of_integer :: "integer \<Rightarrow> char"
  15.135 +where
  15.136 +  "char_of_integer = char_of_nat \<circ> nat_of_integer"
  15.137 +
  15.138 +lemma integer_of_char_zero [simp, code]:
  15.139 +  "integer_of_char 0 = 0"
  15.140 +  by (simp add: integer_of_char_def integer_of_nat_def)
  15.141  
  15.142 -lemma nibble_of_nat_simps [simp]:
  15.143 -  "nibble_of_nat  0 = Nibble0"
  15.144 -  "nibble_of_nat  1 = Nibble1"
  15.145 -  "nibble_of_nat  2 = Nibble2"
  15.146 -  "nibble_of_nat  3 = Nibble3"
  15.147 -  "nibble_of_nat  4 = Nibble4"
  15.148 -  "nibble_of_nat  5 = Nibble5"
  15.149 -  "nibble_of_nat  6 = Nibble6"
  15.150 -  "nibble_of_nat  7 = Nibble7"
  15.151 -  "nibble_of_nat  8 = Nibble8"
  15.152 -  "nibble_of_nat  9 = Nibble9"
  15.153 -  "nibble_of_nat 10 = NibbleA"
  15.154 -  "nibble_of_nat 11 = NibbleB"
  15.155 -  "nibble_of_nat 12 = NibbleC"
  15.156 -  "nibble_of_nat 13 = NibbleD"
  15.157 -  "nibble_of_nat 14 = NibbleE"
  15.158 -  "nibble_of_nat 15 = NibbleF"
  15.159 -  unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
  15.160 +lemma integer_of_char_Char [simp]:
  15.161 +  "integer_of_char (Char k) = numeral k mod 256"
  15.162 +  by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
  15.163 +    id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
  15.164  
  15.165 -lemma nibble_of_nat_of_nibble [simp]:
  15.166 -  "nibble_of_nat (nat_of_nibble x) = x"
  15.167 -  by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
  15.168 +lemma less_256_integer_of_char_Char:
  15.169 +  assumes "numeral k < (256 :: integer)"
  15.170 +  shows "integer_of_char (Char k) = numeral k"
  15.171 +proof -
  15.172 +  have "numeral k mod 256 = (numeral k :: integer)"
  15.173 +    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
  15.174 +  then show ?thesis using integer_of_char_Char [of k]
  15.175 +    by (simp only:)
  15.176 +qed
  15.177  
  15.178 -lemma nat_of_nibble_of_nat [simp]:
  15.179 -  "nat_of_nibble (nibble_of_nat n) = n mod 16"
  15.180 -  by (cases "nibble_of_nat n")
  15.181 -     (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
  15.182 -
  15.183 -lemma inj_nat_of_nibble:
  15.184 -  "inj nat_of_nibble"
  15.185 -  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
  15.186 +setup \<open>
  15.187 +let
  15.188 +  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
  15.189 +  val simpset =
  15.190 +    put_simpset HOL_ss @{context}
  15.191 +      addsimps @{thms numeral_less_iff less_num_simps};
  15.192 +  fun mk_code_eqn ct =
  15.193 +    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
  15.194 +    |> full_simplify simpset;
  15.195 +  val code_eqns = map mk_code_eqn chars;
  15.196 +in
  15.197 +  Global_Theory.note_thmss ""
  15.198 +    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
  15.199 +  #> snd
  15.200 +end
  15.201 +\<close>
  15.202  
  15.203 -lemma nat_of_nibble_eq_iff:
  15.204 -  "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
  15.205 -  by (rule inj_eq) (rule inj_nat_of_nibble)
  15.206 +declare integer_of_char_simps [code]
  15.207 +
  15.208 +lemma nat_of_char_code [code]:
  15.209 +  "nat_of_char = nat_of_integer \<circ> integer_of_char"
  15.210 +  by (simp add: integer_of_char_def fun_eq_iff)
  15.211  
  15.212 -lemma nat_of_nibble_less_16:
  15.213 -  "nat_of_nibble x < 16"
  15.214 -  by (cases x) auto
  15.215 +lemma char_of_nat_code [code]:
  15.216 +  "char_of_nat = char_of_integer \<circ> integer_of_nat"
  15.217 +  by (simp add: char_of_integer_def fun_eq_iff)
  15.218  
  15.219 -lemma nibble_of_nat_mod_16:
  15.220 -  "nibble_of_nat (n mod 16) = nibble_of_nat n"
  15.221 -  by (simp add: nibble_of_nat_def)
  15.222 -
  15.223 -context
  15.224 +instantiation char :: equal
  15.225  begin
  15.226  
  15.227 -local_setup \<open>Local_Theory.map_background_naming (Name_Space.add_path "char")\<close>
  15.228 +definition equal_char
  15.229 +  where "equal_char (c :: char) d \<longleftrightarrow> c = d"
  15.230  
  15.231 -definition Char :: "nibble \<Rightarrow> nibble \<Rightarrow> char"
  15.232 -where
  15.233 -  "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)"
  15.234 -  \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
  15.235 +instance
  15.236 +  by standard (simp add: equal_char_def)
  15.237  
  15.238  end
  15.239  
  15.240 -lemma nat_of_char_Char:
  15.241 -  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" (is "_ = ?rhs")
  15.242 -proof -
  15.243 -  have "?rhs < 256"
  15.244 -    using nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
  15.245 -    by arith
  15.246 -  then show ?thesis by (simp add: Char_def)
  15.247 -qed
  15.248 -
  15.249 -lemma char_of_nat_Char_nibbles:
  15.250 -  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
  15.251 -proof -
  15.252 -  from mod_mult2_eq [of n 16 16]
  15.253 -  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
  15.254 -  then show ?thesis
  15.255 -    by (simp add: Char_def)
  15.256 -qed
  15.257 -
  15.258 -lemma char_of_nat_nibble_pair [simp]:
  15.259 -  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
  15.260 -  by (simp add: nat_of_char_Char [symmetric])
  15.261 -
  15.262 -free_constructors char for Char
  15.263 -proof -
  15.264 -  fix P c
  15.265 -  assume hyp: "\<And>x y. c = Char x y \<Longrightarrow> P"
  15.266 -  have "nat_of_char c \<le> 255"
  15.267 -    using nat_of_char_less_256 [of c] by arith
  15.268 -  then have "nat_of_char c div 16 \<le> 255 div 16"
  15.269 -    by (auto intro: div_le_mono2)
  15.270 -  then have "nat_of_char c div 16 < 16"
  15.271 -    by auto
  15.272 -  then have "nat_of_char c div 16 mod 16 = nat_of_char c div 16"
  15.273 -    by simp
  15.274 -  then have "c = Char (nibble_of_nat (nat_of_char c div 16))
  15.275 -    (nibble_of_nat (nat_of_char c mod 16))"
  15.276 -    by (simp add: Char_def)
  15.277 -  then show P by (rule hyp)
  15.278 -next
  15.279 -  fix x y z w
  15.280 -  have "Char x y = Char z w
  15.281 -    \<longleftrightarrow> nat_of_char (Char x y) = nat_of_char (Char z w)"
  15.282 -    by auto
  15.283 -  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")
  15.284 -  proof
  15.285 -    assume "?Q \<and> ?R"
  15.286 -    then show ?P by (simp add: nat_of_char_Char)
  15.287 -  next
  15.288 -    assume ?P
  15.289 -    then have ?Q
  15.290 -      using nat_of_nibble_less_16 [of y] nat_of_nibble_less_16 [of w]
  15.291 -      by (simp add: nat_of_char_Char)
  15.292 -    moreover with \<open>?P\<close> have ?R by (simp add: nat_of_char_Char)
  15.293 -    ultimately show "?Q \<and> ?R" ..
  15.294 -  qed
  15.295 -  also have "\<dots> \<longleftrightarrow> x = z \<and> y = w"
  15.296 -    by (simp add: nat_of_nibble_eq_iff)
  15.297 -  finally show "Char x y = Char z w \<longleftrightarrow> x = z \<and> y = w" .
  15.298 -qed
  15.299 +lemma equal_char_simps [code]:
  15.300 +  "HOL.equal (0::char) 0 \<longleftrightarrow> True"
  15.301 +  "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
  15.302 +  "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
  15.303 +  "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
  15.304 +  by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
  15.305  
  15.306  syntax
  15.307 -  "_Char" :: "str_position => char"    ("CHR _")
  15.308 +  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
  15.309 +
  15.310 +syntax
  15.311 +  "_Char_ord" :: "num_const \<Rightarrow> char"     ("CHAR _")
  15.312  
  15.313  type_synonym string = "char list"
  15.314  
  15.315 @@ -271,84 +217,74 @@
  15.316  
  15.317  ML_file "Tools/string_syntax.ML"
  15.318  
  15.319 -lemma UNIV_char:
  15.320 -  "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
  15.321 -proof (rule UNIV_eq_I)
  15.322 -  fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
  15.323 -qed
  15.324 -
  15.325  instantiation char :: enum
  15.326  begin
  15.327  
  15.328  definition
  15.329 -  "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
  15.330 -  Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
  15.331 -  Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
  15.332 -  Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
  15.333 -  Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
  15.334 -  Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
  15.335 -  Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
  15.336 -  Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
  15.337 -  Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
  15.338 -  Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
  15.339 -  Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
  15.340 -  Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
  15.341 -  Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
  15.342 -  CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
  15.343 -  CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
  15.344 -  CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
  15.345 -  CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
  15.346 -  CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
  15.347 -  CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
  15.348 -  CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
  15.349 -  CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
  15.350 -  CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
  15.351 -  CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
  15.352 -  CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
  15.353 -  CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
  15.354 -  Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
  15.355 -  Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
  15.356 -  Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
  15.357 -  Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
  15.358 -  Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
  15.359 -  Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
  15.360 -  Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
  15.361 -  Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
  15.362 -  Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
  15.363 -  Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
  15.364 -  Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
  15.365 -  Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
  15.366 -  Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
  15.367 -  Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
  15.368 -  Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
  15.369 -  Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
  15.370 -  Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
  15.371 -  Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
  15.372 -  Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
  15.373 -  Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
  15.374 -  Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
  15.375 -  Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
  15.376 -  Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
  15.377 -  Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
  15.378 -  Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
  15.379 -  Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
  15.380 -  Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
  15.381 -  Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
  15.382 -  Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
  15.383 -  Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
  15.384 -  Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
  15.385 -  Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
  15.386 -  Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
  15.387 -  Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
  15.388 -  Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
  15.389 -  Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
  15.390 -  Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
  15.391 -  Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
  15.392 -  Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
  15.393 -  Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
  15.394 -  Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
  15.395 -  Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
  15.396 -  Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
  15.397 +  "Enum.enum = [0, CHAR 0x01, CHAR 0x02, CHAR 0x03,
  15.398 +    CHAR 0x04, CHAR 0x05, CHAR 0x06, CHAR 0x07,
  15.399 +    CHAR 0x08, CHAR 0x09, CHR ''\<newline>'', CHAR 0x0B,
  15.400 +    CHAR 0x0C, CHAR 0x0D, CHAR 0x0E, CHAR 0x0F,
  15.401 +    CHAR 0x10, CHAR 0x11, CHAR 0x12, CHAR 0x13,
  15.402 +    CHAR 0x14, CHAR 0x15, CHAR 0x16, CHAR 0x17,
  15.403 +    CHAR 0x18, CHAR 0x19, CHAR 0x1A, CHAR 0x1B,
  15.404 +    CHAR 0x1C, CHAR 0x1D, CHAR 0x1E, CHAR 0x1F,
  15.405 +    CHR '' '', CHR ''!'', CHAR 0x22, CHR ''#'',
  15.406 +    CHR ''$'', CHR ''%'', CHR ''&'', CHAR 0x27,
  15.407 +    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
  15.408 +    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
  15.409 +    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
  15.410 +    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
  15.411 +    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
  15.412 +    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
  15.413 +    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
  15.414 +    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
  15.415 +    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
  15.416 +    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
  15.417 +    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
  15.418 +    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
  15.419 +    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
  15.420 +    CHAR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
  15.421 +    CHAR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
  15.422 +    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
  15.423 +    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
  15.424 +    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
  15.425 +    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
  15.426 +    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
  15.427 +    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
  15.428 +    CHR ''|'', CHR ''}'', CHR ''~'', CHAR 0x7F,
  15.429 +    CHAR 0x80, CHAR 0x81, CHAR 0x82, CHAR 0x83,
  15.430 +    CHAR 0x84, CHAR 0x85, CHAR 0x86, CHAR 0x87,
  15.431 +    CHAR 0x88, CHAR 0x89, CHAR 0x8A, CHAR 0x8B,
  15.432 +    CHAR 0x8C, CHAR 0x8D, CHAR 0x8E, CHAR 0x8F,
  15.433 +    CHAR 0x90, CHAR 0x91, CHAR 0x92, CHAR 0x93,
  15.434 +    CHAR 0x94, CHAR 0x95, CHAR 0x96, CHAR 0x97,
  15.435 +    CHAR 0x98, CHAR 0x99, CHAR 0x9A, CHAR 0x9B,
  15.436 +    CHAR 0x9C, CHAR 0x9D, CHAR 0x9E, CHAR 0x9F,
  15.437 +    CHAR 0xA0, CHAR 0xA1, CHAR 0xA2, CHAR 0xA3,
  15.438 +    CHAR 0xA4, CHAR 0xA5, CHAR 0xA6, CHAR 0xA7,
  15.439 +    CHAR 0xA8, CHAR 0xA9, CHAR 0xAA, CHAR 0xAB,
  15.440 +    CHAR 0xAC, CHAR 0xAD, CHAR 0xAE, CHAR 0xAF,
  15.441 +    CHAR 0xB0, CHAR 0xB1, CHAR 0xB2, CHAR 0xB3,
  15.442 +    CHAR 0xB4, CHAR 0xB5, CHAR 0xB6, CHAR 0xB7,
  15.443 +    CHAR 0xB8, CHAR 0xB9, CHAR 0xBA, CHAR 0xBB,
  15.444 +    CHAR 0xBC, CHAR 0xBD, CHAR 0xBE, CHAR 0xBF,
  15.445 +    CHAR 0xC0, CHAR 0xC1, CHAR 0xC2, CHAR 0xC3,
  15.446 +    CHAR 0xC4, CHAR 0xC5, CHAR 0xC6, CHAR 0xC7,
  15.447 +    CHAR 0xC8, CHAR 0xC9, CHAR 0xCA, CHAR 0xCB,
  15.448 +    CHAR 0xCC, CHAR 0xCD, CHAR 0xCE, CHAR 0xCF,
  15.449 +    CHAR 0xD0, CHAR 0xD1, CHAR 0xD2, CHAR 0xD3,
  15.450 +    CHAR 0xD4, CHAR 0xD5, CHAR 0xD6, CHAR 0xD7,
  15.451 +    CHAR 0xD8, CHAR 0xD9, CHAR 0xDA, CHAR 0xDB,
  15.452 +    CHAR 0xDC, CHAR 0xDD, CHAR 0xDE, CHAR 0xDF,
  15.453 +    CHAR 0xE0, CHAR 0xE1, CHAR 0xE2, CHAR 0xE3,
  15.454 +    CHAR 0xE4, CHAR 0xE5, CHAR 0xE6, CHAR 0xE7,
  15.455 +    CHAR 0xE8, CHAR 0xE9, CHAR 0xEA, CHAR 0xEB,
  15.456 +    CHAR 0xEC, CHAR 0xED, CHAR 0xEE, CHAR 0xEF,
  15.457 +    CHAR 0xF0, CHAR 0xF1, CHAR 0xF2, CHAR 0xF3,
  15.458 +    CHAR 0xF4, CHAR 0xF5, CHAR 0xF6, CHAR 0xF7,
  15.459 +    CHAR 0xF8, CHAR 0xF9, CHAR 0xFA, CHAR 0xFB,
  15.460 +    CHAR 0xFC, CHAR 0xFD, CHAR 0xFE, CHAR 0xFF]"
  15.461  
  15.462  definition
  15.463    "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
  15.464 @@ -356,15 +292,22 @@
  15.465  definition
  15.466    "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
  15.467  
  15.468 -lemma enum_char_product_enum_nibble:
  15.469 -  "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
  15.470 -  by (simp add: enum_char_def enum_nibble_def)
  15.471 +lemma enum_char_unfold:
  15.472 +  "Enum.enum = map char_of_nat [0..<256]"
  15.473 +proof -
  15.474 +  have *: "Suc (Suc 0) = 2" by simp
  15.475 +  have "map nat_of_char Enum.enum = [0..<256]"
  15.476 +    by (simp add: enum_char_def upt_conv_Cons_Cons *)
  15.477 +  then have "map char_of_nat (map nat_of_char Enum.enum) =
  15.478 +    map char_of_nat [0..<256]" by simp
  15.479 +  then show ?thesis by (simp add: comp_def)
  15.480 +qed
  15.481  
  15.482  instance proof
  15.483    show UNIV: "UNIV = set (Enum.enum :: char list)"
  15.484 -    by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
  15.485 +    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
  15.486    show "distinct (Enum.enum :: char list)"
  15.487 -    by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
  15.488 +    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
  15.489    show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
  15.490      by (simp add: UNIV enum_all_char_def list_all_iff)
  15.491    show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
  15.492 @@ -373,66 +316,9 @@
  15.493  
  15.494  end
  15.495  
  15.496 -lemma card_UNIV_char:
  15.497 -  "card (UNIV :: char set) = 256"
  15.498 -  by (simp add: card_UNIV_length_enum enum_char_def)
  15.499 -
  15.500 -lemma enum_char_unfold:
  15.501 -  "Enum.enum = map char_of_nat [0..<256]"
  15.502 -proof -
  15.503 -  have *: "Suc (Suc 0) = 2" by simp
  15.504 -  have "map nat_of_char Enum.enum = [0..<256]"
  15.505 -    by (simp add: enum_char_def nat_of_char_Char upt_conv_Cons_Cons *)
  15.506 -  then have "map char_of_nat (map nat_of_char Enum.enum) =
  15.507 -    map char_of_nat [0..<256]" by simp
  15.508 -  then show ?thesis by (simp add: comp_def)
  15.509 -qed
  15.510 -
  15.511 -setup \<open>
  15.512 -let
  15.513 -  val nibbles = map_range (Thm.cterm_of @{context} o HOLogic.mk_nibble) 16;
  15.514 -  val simpset =
  15.515 -    put_simpset HOL_ss @{context}
  15.516 -      addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
  15.517 -  fun mk_code_eqn x y =
  15.518 -    Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
  15.519 -    |> simplify simpset;
  15.520 -  val code_eqns = map_product mk_code_eqn nibbles nibbles;
  15.521 -in
  15.522 -  Global_Theory.note_thmss ""
  15.523 -    [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
  15.524 -  #> snd
  15.525 -end
  15.526 -\<close>
  15.527 -
  15.528 -declare nat_of_char_simps [code]
  15.529 -
  15.530 -lemma nibble_of_nat_of_char_div_16:
  15.531 -  "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
  15.532 -  by (cases c)
  15.533 -    (simp add: nat_of_char_Char add.commute nat_of_nibble_less_16)
  15.534 -
  15.535 -lemma nibble_of_nat_nat_of_char:
  15.536 -  "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
  15.537 -proof (cases c)
  15.538 -  case (Char x y)
  15.539 -  then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
  15.540 -    by (simp add: nibble_of_nat_mod_16)
  15.541 -  then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
  15.542 -    by (simp only: nibble_of_nat_mod_16)
  15.543 -  with Char show ?thesis by (simp add: nat_of_char_Char add.commute)
  15.544 -qed
  15.545 -
  15.546 -code_datatype Char \<comment> \<open>drop case certificate for char\<close>
  15.547 -
  15.548 -lemma case_char_code [code]:
  15.549 -  "char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
  15.550 -  by (cases c)
  15.551 -    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
  15.552 -
  15.553 -lemma char_of_nat_enum [code]:
  15.554 -  "char_of_nat n = Enum.enum ! (n mod 256)"
  15.555 -  by (simp add: enum_char_unfold)
  15.556 +lemma char_of_integer_code [code]:
  15.557 +  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
  15.558 +  by (simp add: char_of_integer_def enum_char_unfold)
  15.559  
  15.560  
  15.561  subsection \<open>Strings as dedicated type\<close>
    16.1 --- a/src/HOL/Tools/hologic.ML	Fri Mar 11 17:20:14 2016 +0100
    16.2 +++ b/src/HOL/Tools/hologic.ML	Sat Mar 12 22:04:52 2016 +0100
    16.3 @@ -108,9 +108,6 @@
    16.4    val code_integerT: typ
    16.5    val code_naturalT: typ
    16.6    val realT: typ
    16.7 -  val nibbleT: typ
    16.8 -  val mk_nibble: int -> term
    16.9 -  val dest_nibble: term -> int
   16.10    val charT: typ
   16.11    val mk_char: int -> term
   16.12    val dest_char: term -> int
   16.13 @@ -594,42 +591,27 @@
   16.14    | dest_list t = raise TERM ("dest_list", [t]);
   16.15  
   16.16  
   16.17 -(* nibble *)
   16.18 -
   16.19 -val nibbleT = Type ("String.nibble", []);
   16.20 -
   16.21 -fun mk_nibble n =
   16.22 -  let val s =
   16.23 -    if 0 <= n andalso n <= 9 then chr (n + ord "0")
   16.24 -    else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
   16.25 -    else raise TERM ("mk_nibble", [])
   16.26 -  in Const ("String.nibble.Nibble" ^ s, nibbleT) end;
   16.27 -
   16.28 -fun dest_nibble t =
   16.29 -  let fun err () = raise TERM ("dest_nibble", [t]) in
   16.30 -    (case try (unprefix "String.nibble.Nibble" o fst o Term.dest_Const) t of
   16.31 -      NONE => err ()
   16.32 -    | SOME c =>
   16.33 -        if size c <> 1 then err ()
   16.34 -        else if "0" <= c andalso c <= "9" then ord c - ord "0"
   16.35 -        else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
   16.36 -        else err ())
   16.37 -  end;
   16.38 -
   16.39 -
   16.40  (* char *)
   16.41  
   16.42  val charT = Type ("String.char", []);
   16.43  
   16.44 -fun mk_char n =
   16.45 -  if 0 <= n andalso n <= 255 then
   16.46 -    Const ("String.char.Char", nibbleT --> nibbleT --> charT) $
   16.47 -      mk_nibble (n div 16) $ mk_nibble (n mod 16)
   16.48 -  else raise TERM ("mk_char", []);
   16.49 +val Char_const = Const ("String.Char", numT --> charT);
   16.50 +
   16.51 +fun mk_char 0 = Const ("Groups.zero_class.zero", charT)
   16.52 +  | mk_char i =
   16.53 +      if 1 <= i andalso i <= 255 then Char_const $ mk_numeral i
   16.54 +      else raise TERM ("mk_char", []);
   16.55  
   16.56 -fun dest_char (Const ("String.char.Char", _) $ t $ u) =
   16.57 -      dest_nibble t * 16 + dest_nibble u
   16.58 -  | dest_char t = raise TERM ("dest_char", [t]);
   16.59 +fun dest_char t =
   16.60 +  let
   16.61 +    val (T, n) = case t of
   16.62 +      Const ("Groups.zero_class.zero", T) => (T, 0)
   16.63 +    | (Const ("String.Char", Type ("fun", [_, T])) $ t) => (T, dest_numeral t)
   16.64 +    | _ => raise TERM ("dest_char", [t]);
   16.65 +  in
   16.66 +    if T = charT then n
   16.67 +    else raise TERM ("dest_char", [t])
   16.68 +  end;
   16.69  
   16.70  
   16.71  (* string *)
    17.1 --- a/src/HOL/Tools/numeral.ML	Fri Mar 11 17:20:14 2016 +0100
    17.2 +++ b/src/HOL/Tools/numeral.ML	Sat Mar 12 22:04:52 2016 +0100
    17.3 @@ -6,9 +6,12 @@
    17.4  
    17.5  signature NUMERAL =
    17.6  sig
    17.7 -  val mk_cnumeral: int -> cterm
    17.8    val mk_cnumber: ctyp -> int -> cterm
    17.9    val mk_number_syntax: int -> term
   17.10 +  val mk_cnumeral: int -> cterm
   17.11 +  val mk_num_syntax: int -> term
   17.12 +  val dest_num_syntax: term -> int
   17.13 +  val dest_num: Code_Thingol.iterm -> int option
   17.14    val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
   17.15  end;
   17.16  
   17.17 @@ -17,6 +20,18 @@
   17.18  
   17.19  (* numeral *)
   17.20  
   17.21 +fun dest_num_syntax (Const (@{const_syntax Num.Bit0}, _) $ t) = 2 * dest_num_syntax t
   17.22 +  | dest_num_syntax (Const (@{const_syntax Num.Bit1}, _) $ t) = 2 * dest_num_syntax t + 1
   17.23 +  | dest_num_syntax (Const (@{const_syntax Num.One}, _)) = 1;
   17.24 +
   17.25 +fun mk_num_syntax n =
   17.26 +  if n > 0 then
   17.27 +    (case IntInf.quotRem (n, 2) of
   17.28 +      (0, 1) => Syntax.const @{const_syntax One}
   17.29 +    | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
   17.30 +    | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
   17.31 +  else raise Match
   17.32 +
   17.33  fun mk_cbit 0 = @{cterm "Num.Bit0"}
   17.34    | mk_cbit 1 = @{cterm "Num.Bit1"}
   17.35    | mk_cbit _ = raise CTERM ("mk_cbit", []);
   17.36 @@ -67,14 +82,6 @@
   17.37  
   17.38  end;
   17.39  
   17.40 -fun mk_num_syntax n =
   17.41 -  if n > 0 then
   17.42 -    (case IntInf.quotRem (n, 2) of
   17.43 -      (0, 1) => Syntax.const @{const_syntax One}
   17.44 -    | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
   17.45 -    | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
   17.46 -  else raise Match
   17.47 -
   17.48  fun mk_number_syntax n =
   17.49    if n = 0 then Syntax.const @{const_syntax Groups.zero}
   17.50    else if n = 1 then Syntax.const @{const_syntax Groups.one}
   17.51 @@ -85,17 +92,25 @@
   17.52  
   17.53  local open Basic_Code_Thingol in
   17.54  
   17.55 +fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1
   17.56 +  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) =
   17.57 +     (case dest_num t of
   17.58 +        SOME n => SOME (2 * n)
   17.59 +      | _ => NONE)
   17.60 +  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) =
   17.61 +     (case dest_num t of
   17.62 +        SOME n => SOME (2 * n + 1)
   17.63 +      | _ => NONE)
   17.64 +  | dest_num _ = NONE;
   17.65 +
   17.66  fun add_code number_of preproc print target thy =
   17.67    let
   17.68      fun pretty literals _ thm _ _ [(t, _)] =
   17.69        let
   17.70 -        fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
   17.71 -          | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
   17.72 -          | dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit";
   17.73 -        fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
   17.74 -          | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
   17.75 -          | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
   17.76 -      in (Code_Printer.str o print literals o preproc o dest_num) t end;
   17.77 +        val n = case dest_num t of
   17.78 +          SOME n => n
   17.79 +        | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"
   17.80 +      in (Code_Printer.str o print literals o preproc) n end;
   17.81    in
   17.82      thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
   17.83        [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
    18.1 --- a/src/HOL/Tools/string_code.ML	Fri Mar 11 17:20:14 2016 +0100
    18.2 +++ b/src/HOL/Tools/string_code.ML	Sat Mar 12 22:04:52 2016 +0100
    18.3 @@ -16,34 +16,22 @@
    18.4  
    18.5  open Basic_Code_Thingol;
    18.6  
    18.7 -val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    18.8 -  @{const_name Nibble2}, @{const_name Nibble3},
    18.9 -  @{const_name Nibble4}, @{const_name Nibble5},
   18.10 -  @{const_name Nibble6}, @{const_name Nibble7},
   18.11 -  @{const_name Nibble8}, @{const_name Nibble9},
   18.12 -  @{const_name NibbleA}, @{const_name NibbleB},
   18.13 -  @{const_name NibbleC}, @{const_name NibbleD},
   18.14 -  @{const_name NibbleE}, @{const_name NibbleF}];
   18.15 +fun decode_char_nonzero t =
   18.16 +  case Numeral.dest_num t of
   18.17 +    SOME n => if 0 < n andalso n < 256 then SOME n else NONE
   18.18 +  | _ => NONE;
   18.19  
   18.20 -fun decode_char tt =
   18.21 -  let
   18.22 -    fun idx c = find_index (curry (op =) c) cs_nibbles;
   18.23 -    fun decode ~1 _ = NONE
   18.24 -      | decode _ ~1 = NONE
   18.25 -      | decode n m = SOME (chr (n * 16 + m));
   18.26 -  in case tt
   18.27 -   of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
   18.28 -    | _ => NONE
   18.29 -  end;
   18.30 -   
   18.31 +fun decode_char (IConst { sym = Code_Symbol.Constant @{const_name Groups.zero}, ... }) =
   18.32 +     SOME 0
   18.33 +  | decode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t) =
   18.34 +      decode_char_nonzero t
   18.35 +  | decode_char _ = NONE
   18.36 +
   18.37  fun implode_string literals ts =
   18.38    let
   18.39 -    fun implode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t1 `$ t2) =
   18.40 -          decode_char (t1, t2)
   18.41 -      | implode_char _ = NONE;
   18.42 -    val ts' = map_filter implode_char ts;
   18.43 -  in if length ts = length ts'
   18.44 -    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
   18.45 +    val is = map_filter decode_char ts;
   18.46 +  in if length ts = length is
   18.47 +    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode o map chr) is
   18.48      else NONE
   18.49    end;
   18.50  
   18.51 @@ -64,13 +52,20 @@
   18.52  
   18.53  fun add_literal_char target thy =
   18.54    let
   18.55 -    fun pretty literals _ thm _ _ [(t1, _), (t2, _)] =
   18.56 -      case decode_char (t1, t2)
   18.57 -       of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
   18.58 +    fun pr literals =
   18.59 +      Code_Printer.str o Code_Printer.literal_char literals o chr;
   18.60 +    fun pretty_zero literals _ _ _ _ [] =
   18.61 +      pr literals 0
   18.62 +    fun pretty_Char literals _ thm _ _ [(t, _)] =
   18.63 +      case decode_char_nonzero t
   18.64 +       of SOME i => pr literals i
   18.65          | NONE => Code_Printer.eqn_error thy thm "Illegal character expression";
   18.66    in
   18.67 -    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
   18.68 -      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) thy
   18.69 +    thy
   18.70 +    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.zero_char_inst.zero_char},
   18.71 +      [(target, SOME (Code_Printer.complex_const_syntax (0, pretty_zero)))]))
   18.72 +    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
   18.73 +      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty_Char)))]))
   18.74    end;
   18.75  
   18.76  fun add_literal_string target thy =
   18.77 @@ -82,8 +77,9 @@
   18.78                | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression")
   18.79          | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
   18.80    in
   18.81 -    Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
   18.82 -      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) thy
   18.83 +    thy
   18.84 +    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
   18.85 +      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
   18.86    end;
   18.87  
   18.88  end;
    19.1 --- a/src/HOL/Tools/string_syntax.ML	Fri Mar 11 17:20:14 2016 +0100
    19.2 +++ b/src/HOL/Tools/string_syntax.ML	Sat Mar 12 22:04:52 2016 +0100
    19.3 @@ -1,85 +1,109 @@
    19.4  (*  Title:      HOL/Tools/string_syntax.ML
    19.5      Author:     Makarius
    19.6  
    19.7 -Concrete syntax for hex chars and strings.
    19.8 +Concrete syntax for chars and strings.
    19.9  *)
   19.10  
   19.11  structure String_Syntax: sig end =
   19.12  struct
   19.13  
   19.14 -(* nibble *)
   19.15 +(* numeral *)
   19.16  
   19.17 -val mk_nib =
   19.18 -  Ast.Constant o Lexicon.mark_const o
   19.19 -    fst o Term.dest_Const o HOLogic.mk_nibble;
   19.20 +fun hex_digit n = if n = 10 then "A"
   19.21 +  else if n = 11 then "B"
   19.22 +  else if n = 12 then "C"
   19.23 +  else if n = 13 then "D"
   19.24 +  else if n = 14 then "E"
   19.25 +  else if n = 15 then "F"
   19.26 +  else string_of_int n;
   19.27  
   19.28 -fun dest_nib (Ast.Constant s) =
   19.29 -  (case try Lexicon.unmark_const s of
   19.30 -    NONE => raise Match
   19.31 -  | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
   19.32 +fun hex_prefix ms = "0x" ^ implode (replicate (2 - length ms) "0" @ ms);
   19.33 +
   19.34 +fun hex n = hex_prefix (map hex_digit (radixpand (16, n)));
   19.35  
   19.36  
   19.37  (* char *)
   19.38  
   19.39 -fun mk_char s =
   19.40 -  let
   19.41 -    val c =
   19.42 -      if Symbol.is_ascii s then ord s
   19.43 -      else if s = "\<newline>" then 10
   19.44 -      else error ("Bad character: " ^ quote s);
   19.45 -  in Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (c div 16), mk_nib (c mod 16)] end;
   19.46 +fun mk_char_syntax n =
   19.47 +  if n = 0 then Syntax.const @{const_name Groups.zero}
   19.48 +  else Syntax.const @{const_syntax Char} $ Numeral.mk_num_syntax n;
   19.49 +
   19.50 +fun mk_char_syntax' c =
   19.51 +  if Symbol.is_ascii c then mk_char_syntax (ord c)
   19.52 +  else if c = "\<newline>" then mk_char_syntax 10
   19.53 +  else error ("Bad character: " ^ quote c);
   19.54 +
   19.55 +fun plain_string_of str =
   19.56 +  map fst (Lexicon.explode_str (str, Position.none));
   19.57 +
   19.58 +datatype character = Char of string | Ord of int | Unprintable;
   19.59  
   19.60  val specials = raw_explode "\\\"`'";
   19.61  
   19.62 -fun dest_chr c1 c2 =
   19.63 -  let val s = chr (dest_nib c1 * 16 + dest_nib c2) in
   19.64 -    if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
   19.65 -    then s
   19.66 -    else if s = "\n" then "\<newline>"
   19.67 -    else raise Match
   19.68 -  end;
   19.69 +fun dest_char_syntax c =
   19.70 +  case try Numeral.dest_num_syntax c of
   19.71 +    SOME n =>
   19.72 +      if n < 256 then
   19.73 +        let
   19.74 +          val s = chr n
   19.75 +        in
   19.76 +          if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
   19.77 +          then Char s
   19.78 +          else if s = "\n" then Char "\<newline>"
   19.79 +          else Ord n
   19.80 +        end
   19.81 +      else Unprintable
   19.82 +  | NONE => Unprintable;
   19.83  
   19.84 -fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
   19.85 -  | dest_char _ = raise Match;
   19.86 +fun dest_char_ast (Ast.Appl [Ast.Constant @{syntax_const "_Char"}, Ast.Constant s]) =
   19.87 +      plain_string_of s
   19.88 +  | dest_char_ast _ = raise Match;
   19.89  
   19.90 -fun syntax_string ss =
   19.91 -  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
   19.92 -    Ast.Variable (Lexicon.implode_str ss)];
   19.93 -
   19.94 +fun char_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   19.95 +      c $ char_tr [t] $ u
   19.96 +  | char_tr [Free (str, _)] =
   19.97 +      (case plain_string_of str of
   19.98 +        [c] => mk_char_syntax' c
   19.99 +      | _ => error ("Single character expected: " ^ str))
  19.100 +  | char_tr ts = raise TERM ("char_tr", ts);
  19.101  
  19.102 -fun char_ast_tr [Ast.Variable str] =
  19.103 -      (case Lexicon.explode_str (str, Position.none) of
  19.104 -        [(s, _)] => mk_char s
  19.105 -      | _ => error ("Single character expected: " ^ str))
  19.106 -  | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
  19.107 -      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
  19.108 -  | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
  19.109 +fun char_ord_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
  19.110 +      c $ char_ord_tr [t] $ u
  19.111 +  | char_ord_tr [Const (num, _)] =
  19.112 +      (mk_char_syntax o #value o Lexicon.read_num) num
  19.113 +  | char_ord_tr ts = raise TERM ("char_ord_tr", ts);
  19.114  
  19.115 -fun char_ast_tr' [c1, c2] =
  19.116 -      Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
  19.117 -  | char_ast_tr' _ = raise Match;
  19.118 +fun char_tr' [t] = (case dest_char_syntax t of
  19.119 +        Char s => Syntax.const @{syntax_const "_Char"} $
  19.120 +          Syntax.const (Lexicon.implode_str [s])
  19.121 +      | Ord n => 
  19.122 +          if n = 0
  19.123 +          then Syntax.const @{const_syntax Groups.zero}
  19.124 +          else Syntax.const @{syntax_const "_Char_ord"} $
  19.125 +            Syntax.free (hex n)
  19.126 +      | _ => raise Match)
  19.127 +  | char_tr' _ = raise Match;
  19.128  
  19.129  
  19.130  (* string *)
  19.131  
  19.132 -fun mk_string [] = Ast.Constant @{const_syntax Nil}
  19.133 -  | mk_string (s :: ss) =
  19.134 -      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char s, mk_string ss];
  19.135 +fun mk_string_syntax [] = Syntax.const @{const_syntax Nil}
  19.136 +  | mk_string_syntax (c :: cs) =
  19.137 +      Syntax.const @{const_syntax Cons} $ mk_char_syntax' c $ mk_string_syntax cs;
  19.138  
  19.139 -fun string_ast_tr [Ast.Variable str] =
  19.140 -      (case Lexicon.explode_str (str, Position.none) of
  19.141 -        [] =>
  19.142 -          Ast.Appl
  19.143 -            [Ast.Constant @{syntax_const "_constrain"},
  19.144 -              Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
  19.145 -      | ss => mk_string (map Symbol_Pos.symbol ss))
  19.146 -  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
  19.147 -      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
  19.148 -  | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
  19.149 +fun mk_string_ast ss =
  19.150 +  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
  19.151 +    Ast.Variable (Lexicon.implode_str ss)];
  19.152 +
  19.153 +fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
  19.154 +      c $ string_tr [t] $ u
  19.155 +  | string_tr [Free (str, _)] =
  19.156 +      mk_string_syntax (plain_string_of str)
  19.157 +  | string_tr ts = raise TERM ("char_tr", ts);
  19.158  
  19.159  fun list_ast_tr' [args] =
  19.160        Ast.Appl [Ast.Constant @{syntax_const "_String"},
  19.161 -        syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
  19.162 +        (mk_string_ast o maps dest_char_ast o Ast.unfold_ast @{syntax_const "_args"}) args]
  19.163    | list_ast_tr' _ = raise Match;
  19.164  
  19.165  
  19.166 @@ -87,11 +111,13 @@
  19.167  
  19.168  val _ =
  19.169    Theory.setup
  19.170 -   (Sign.parse_ast_translation
  19.171 -     [(@{syntax_const "_Char"}, K char_ast_tr),
  19.172 -      (@{syntax_const "_String"}, K string_ast_tr)] #>
  19.173 +   (Sign.parse_translation
  19.174 +     [(@{syntax_const "_Char"}, K char_tr),
  19.175 +      (@{syntax_const "_Char_ord"}, K char_ord_tr),
  19.176 +      (@{syntax_const "_String"}, K string_tr)] #>
  19.177 +    Sign.print_translation
  19.178 +     [(@{const_syntax Char}, K char_tr')] #>
  19.179      Sign.print_ast_translation
  19.180 -     [(@{const_syntax Char}, K char_ast_tr'),
  19.181 -      (@{syntax_const "_list"}, K list_ast_tr')]);
  19.182 +     [(@{syntax_const "_list"}, K list_ast_tr')]);
  19.183  
  19.184  end;
    20.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Fri Mar 11 17:20:14 2016 +0100
    20.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Mar 12 22:04:52 2016 +0100
    20.3 @@ -53,17 +53,13 @@
    20.4  
    20.5  ML \<open>
    20.6    local
    20.7 -    val mk_nib =
    20.8 -      Syntax.const o Lexicon.mark_const o
    20.9 -        fst o Term.dest_Const o HOLogic.mk_nibble;
   20.10 -
   20.11      fun mk_char (s, pos) =
   20.12        let
   20.13          val c =
   20.14            if Symbol.is_ascii s then ord s
   20.15            else if s = "\<newline>" then 10
   20.16            else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
   20.17 -      in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end;
   20.18 +      in Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c end;
   20.19  
   20.20      fun mk_string [] = Const (@{const_syntax Nil}, @{typ string})
   20.21        | mk_string (s :: ss) =