systematic conversions between nat and nibble/char;
authorhaftmann
Fri Feb 15 11:47:33 2013 +0100 (2013-02-15)
changeset 51160599ff65b85e2
parent 51159 3fe7242f8346
child 51161 6ed12ae3b3e1
systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char
src/Doc/Codegen/Adaptation.thy
src/HOL/Code_Evaluation.thy
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Codegenerator_Test/Candidates_Pretty.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Code_Char_ord.thy
src/HOL/List.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/ROOT
src/HOL/String.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/string_code.ML
src/HOL/Tools/string_syntax.ML
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 15:22:16 2013 +0100
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 11:47:33 2013 +0100
     1.3 @@ -150,10 +150,6 @@
     1.4         containing both @{text "Code_Target_Nat"} and
     1.5         @{text "Code_Target_Int"}.
     1.6  
     1.7 -    \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but
     1.8 -       also offers treatment of character codes; includes @{text
     1.9 -       "Code_Char"}.
    1.10 -
    1.11      \item[@{text "Efficient_Nat"}] \label{eff_nat} implements
    1.12         natural numbers by integers, which in general will result in
    1.13         higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
     2.1 --- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 15:22:16 2013 +0100
     2.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 11:47:33 2013 +0100
     2.3 @@ -119,11 +119,10 @@
     2.4    = Code_Evaluation.term_of" ..
     2.5  
     2.6  lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
     2.7 -  "Code_Evaluation.term_of c =
     2.8 -    (let (n, m) = nibble_pair_of_char c
     2.9 -  in Code_Evaluation.App (Code_Evaluation.App
    2.10 +  "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
    2.11 +   Code_Evaluation.App (Code_Evaluation.App
    2.12      (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    2.13 -      (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
    2.14 +      (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
    2.15    by (subst term_of_anything) rule 
    2.16  
    2.17  code_type "term"
     3.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 15:22:16 2013 +0100
     3.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 11:47:33 2013 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  theory Candidates
     3.5  imports
     3.6    Complex_Main
     3.7 -  Library
     3.8 +  "~~/src/HOL/Library/Library"
     3.9    "~~/src/HOL/Library/Sublist"
    3.10    "~~/src/HOL/Number_Theory/Primes"
    3.11    "~~/src/HOL/ex/Records"
     4.1 --- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Fri Feb 15 15:22:16 2013 +0100
     4.2 +++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Fri Feb 15 11:47:33 2013 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4  header {* Generating code using pretty literals and natural number literals  *}
     4.5  
     4.6  theory Candidates_Pretty
     4.7 -imports Candidates Code_Char_ord Code_Target_Numeral
     4.8 +imports Candidates Code_Char Code_Target_Numeral
     4.9  begin
    4.10  
    4.11  end
     5.1 --- a/src/HOL/Library/Char_nat.thy	Fri Feb 15 15:22:16 2013 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,199 +0,0 @@
     5.4 -(*  Title:      HOL/Library/Char_nat.thy
     5.5 -    Author:     Norbert Voelker, Florian Haftmann
     5.6 -*)
     5.7 -
     5.8 -header {* Mapping between characters and natural numbers *}
     5.9 -
    5.10 -theory Char_nat
    5.11 -imports List Main
    5.12 -begin
    5.13 -
    5.14 -text {* Conversions between nibbles and natural numbers in [0..15]. *}
    5.15 -
    5.16 -primrec
    5.17 -  nat_of_nibble :: "nibble \<Rightarrow> nat" where
    5.18 -    "nat_of_nibble Nibble0 = 0"
    5.19 -  | "nat_of_nibble Nibble1 = 1"
    5.20 -  | "nat_of_nibble Nibble2 = 2"
    5.21 -  | "nat_of_nibble Nibble3 = 3"
    5.22 -  | "nat_of_nibble Nibble4 = 4"
    5.23 -  | "nat_of_nibble Nibble5 = 5"
    5.24 -  | "nat_of_nibble Nibble6 = 6"
    5.25 -  | "nat_of_nibble Nibble7 = 7"
    5.26 -  | "nat_of_nibble Nibble8 = 8"
    5.27 -  | "nat_of_nibble Nibble9 = 9"
    5.28 -  | "nat_of_nibble NibbleA = 10"
    5.29 -  | "nat_of_nibble NibbleB = 11"
    5.30 -  | "nat_of_nibble NibbleC = 12"
    5.31 -  | "nat_of_nibble NibbleD = 13"
    5.32 -  | "nat_of_nibble NibbleE = 14"
    5.33 -  | "nat_of_nibble NibbleF = 15"
    5.34 -
    5.35 -definition
    5.36 -  nibble_of_nat :: "nat \<Rightarrow> nibble" where
    5.37 -  "nibble_of_nat x = (let y = x mod 16 in
    5.38 -    if y = 0 then Nibble0 else
    5.39 -    if y = 1 then Nibble1 else
    5.40 -    if y = 2 then Nibble2 else
    5.41 -    if y = 3 then Nibble3 else
    5.42 -    if y = 4 then Nibble4 else
    5.43 -    if y = 5 then Nibble5 else
    5.44 -    if y = 6 then Nibble6 else
    5.45 -    if y = 7 then Nibble7 else
    5.46 -    if y = 8 then Nibble8 else
    5.47 -    if y = 9 then Nibble9 else
    5.48 -    if y = 10 then NibbleA else
    5.49 -    if y = 11 then NibbleB else
    5.50 -    if y = 12 then NibbleC else
    5.51 -    if y = 13 then NibbleD else
    5.52 -    if y = 14 then NibbleE else
    5.53 -    NibbleF)"
    5.54 -
    5.55 -lemma nibble_of_nat_norm:
    5.56 -  "nibble_of_nat (n mod 16) = nibble_of_nat n"
    5.57 -  unfolding nibble_of_nat_def mod_mod_trivial ..
    5.58 -
    5.59 -lemma nibble_of_nat_simps [simp]:
    5.60 -  "nibble_of_nat  0 = Nibble0"
    5.61 -  "nibble_of_nat  1 = Nibble1"
    5.62 -  "nibble_of_nat  2 = Nibble2"
    5.63 -  "nibble_of_nat  3 = Nibble3"
    5.64 -  "nibble_of_nat  4 = Nibble4"
    5.65 -  "nibble_of_nat  5 = Nibble5"
    5.66 -  "nibble_of_nat  6 = Nibble6"
    5.67 -  "nibble_of_nat  7 = Nibble7"
    5.68 -  "nibble_of_nat  8 = Nibble8"
    5.69 -  "nibble_of_nat  9 = Nibble9"
    5.70 -  "nibble_of_nat 10 = NibbleA"
    5.71 -  "nibble_of_nat 11 = NibbleB"
    5.72 -  "nibble_of_nat 12 = NibbleC"
    5.73 -  "nibble_of_nat 13 = NibbleD"
    5.74 -  "nibble_of_nat 14 = NibbleE"
    5.75 -  "nibble_of_nat 15 = NibbleF"
    5.76 -  unfolding nibble_of_nat_def by auto
    5.77 -
    5.78 -lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
    5.79 -  by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
    5.80 -
    5.81 -lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
    5.82 -proof -
    5.83 -  have nibble_nat_enum:
    5.84 -    "n mod 16 \<in> {15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0}"
    5.85 -  proof -
    5.86 -    have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
    5.87 -    have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
    5.88 -      (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
    5.89 -    from this [simplified set_unfold atLeastAtMost_singleton]
    5.90 -    show ?thesis by (simp add: numeral_2_eq_2 [symmetric])
    5.91 -  qed
    5.92 -  then show ?thesis unfolding nibble_of_nat_def
    5.93 -  by auto
    5.94 -qed
    5.95 -
    5.96 -lemma inj_nat_of_nibble: "inj nat_of_nibble"
    5.97 -  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
    5.98 -
    5.99 -lemma nat_of_nibble_eq: "nat_of_nibble n = nat_of_nibble m \<longleftrightarrow> n = m"
   5.100 -  by (rule inj_eq) (rule inj_nat_of_nibble)
   5.101 -
   5.102 -lemma nat_of_nibble_less_16: "nat_of_nibble n < 16"
   5.103 -  by (cases n) auto
   5.104 -
   5.105 -lemma nat_of_nibble_div_16: "nat_of_nibble n div 16 = 0"
   5.106 -  by (cases n) auto
   5.107 -
   5.108 -
   5.109 -text {* Conversion between chars and nats. *}
   5.110 -
   5.111 -definition
   5.112 -  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
   5.113 -  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
   5.114 -
   5.115 -lemma nibble_of_pair [code]:
   5.116 -  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
   5.117 -  unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
   5.118 -
   5.119 -primrec
   5.120 -  nat_of_char :: "char \<Rightarrow> nat" where
   5.121 -  "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"
   5.122 -
   5.123 -lemmas [simp del] = nat_of_char.simps
   5.124 -
   5.125 -definition
   5.126 -  char_of_nat :: "nat \<Rightarrow> char" where
   5.127 -  char_of_nat_def: "char_of_nat n = split Char (nibble_pair_of_nat n)"
   5.128 -
   5.129 -lemma Char_char_of_nat:
   5.130 -  "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
   5.131 -  unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
   5.132 -  by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
   5.133 -
   5.134 -lemma char_of_nat_of_char:
   5.135 -  "char_of_nat (nat_of_char c) = c"
   5.136 -  by (cases c) (simp add: nat_of_char.simps, simp add: Char_char_of_nat)
   5.137 -
   5.138 -lemma nat_of_char_of_nat:
   5.139 -  "nat_of_char (char_of_nat n) = n mod 256"
   5.140 -proof -
   5.141 -  from mod_div_equality [of n, symmetric, of 16]
   5.142 -  have mod_mult_self3: "\<And>m k n \<Colon> nat. (k * n + m) mod n = m mod n"
   5.143 -  proof -
   5.144 -    fix m k n :: nat
   5.145 -    show "(k * n + m) mod n = m mod n"
   5.146 -      by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
   5.147 -  qed
   5.148 -  from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
   5.149 -    and k: "k = n div 256" and l: "l = n mod 256" by blast
   5.150 -  have 16: "(0::nat) < 16" by auto
   5.151 -  have 256: "(256 :: nat) = 16 * 16" by auto
   5.152 -  have l_256: "l mod 256 = l" using l by auto
   5.153 -  have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
   5.154 -    using l by auto
   5.155 -  have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
   5.156 -    unfolding 256 mult_assoc [symmetric] mod_mult_self2_is_0 by simp
   5.157 -  have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
   5.158 -    unfolding div_add1_eq [of "k * 256" l 16] aux2 256
   5.159 -      mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
   5.160 -  have aux4: "(k * 256 + l) mod 16 = l mod 16"
   5.161 -    unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
   5.162 -  show ?thesis
   5.163 -    by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
   5.164 -      nat_of_nibble_of_nat mult_mod_left
   5.165 -      n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
   5.166 -qed
   5.167 -
   5.168 -lemma nibble_pair_of_nat_char:
   5.169 -  "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
   5.170 -proof -
   5.171 -  have nat_of_nibble_256:
   5.172 -    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 =
   5.173 -      nat_of_nibble n * 16 + nat_of_nibble m"
   5.174 -  proof -
   5.175 -    fix n m
   5.176 -    have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
   5.177 -      using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: eval_nat_numeral)
   5.178 -    have less_eq_240: "nat_of_nibble n * 16 \<le> 240"
   5.179 -      using nat_of_nibble_less_eq_15 by auto
   5.180 -    have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
   5.181 -      by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
   5.182 -    then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
   5.183 -    then show "?rhs mod 256 = ?rhs" by auto
   5.184 -  qed
   5.185 -  show ?thesis
   5.186 -    unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
   5.187 -    by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
   5.188 -qed
   5.189 -
   5.190 -
   5.191 -text {* Code generator setup *}
   5.192 -
   5.193 -code_modulename SML
   5.194 -  Char_nat String
   5.195 -
   5.196 -code_modulename OCaml
   5.197 -  Char_nat String
   5.198 -
   5.199 -code_modulename Haskell
   5.200 -  Char_nat String
   5.201 -
   5.202 -end
   5.203 \ No newline at end of file
     6.1 --- a/src/HOL/Library/Char_ord.thy	Fri Feb 15 15:22:16 2013 +0100
     6.2 +++ b/src/HOL/Library/Char_ord.thy	Fri Feb 15 11:47:33 2013 +0100
     6.3 @@ -5,43 +5,20 @@
     6.4  header {* Order on characters *}
     6.5  
     6.6  theory Char_ord
     6.7 -imports Char_nat
     6.8 +imports Main
     6.9  begin
    6.10  
    6.11  instantiation nibble :: linorder
    6.12  begin
    6.13  
    6.14  definition
    6.15 -  nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    6.16 +  "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    6.17  
    6.18  definition
    6.19 -  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    6.20 +  "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    6.21  
    6.22  instance proof
    6.23 -  fix n :: nibble
    6.24 -  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    6.25 -next
    6.26 -  fix n m q :: nibble
    6.27 -  assume "n \<le> m"
    6.28 -    and "m \<le> q"
    6.29 -  then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
    6.30 -next
    6.31 -  fix n m :: nibble
    6.32 -  assume "n \<le> m"
    6.33 -    and "m \<le> n"
    6.34 -  then show "n = m"
    6.35 -    unfolding nibble_less_eq_def nibble_less_def
    6.36 -    by (auto simp add: nat_of_nibble_eq)
    6.37 -next
    6.38 -  fix n m :: nibble
    6.39 -  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
    6.40 -    unfolding nibble_less_eq_def nibble_less_def less_le
    6.41 -    by (auto simp add: nat_of_nibble_eq)
    6.42 -next
    6.43 -  fix n m :: nibble
    6.44 -  show "n \<le> m \<or> m \<le> n"
    6.45 -    unfolding nibble_less_eq_def by auto
    6.46 -qed
    6.47 +qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
    6.48  
    6.49  end
    6.50  
    6.51 @@ -54,8 +31,8 @@
    6.52  definition
    6.53    "(sup \<Colon> nibble \<Rightarrow> _) = max"
    6.54  
    6.55 -instance by default (auto simp add:
    6.56 -    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    6.57 +instance proof
    6.58 +qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    6.59  
    6.60  end
    6.61  
    6.62 @@ -63,18 +40,46 @@
    6.63  begin
    6.64  
    6.65  definition
    6.66 -  char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    6.67 -    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
    6.68 +  "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
    6.69  
    6.70  definition
    6.71 -  char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    6.72 -    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
    6.73 +  "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    6.74  
    6.75 -instance
    6.76 -  by default (auto simp: char_less_eq_def char_less_def split: char.splits)
    6.77 +instance proof
    6.78 +qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
    6.79  
    6.80  end
    6.81  
    6.82 +lemma less_eq_char_Char:
    6.83 +  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    6.84 +proof -
    6.85 +  {
    6.86 +    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
    6.87 +      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
    6.88 +    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
    6.89 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
    6.90 +  }
    6.91 +  note * = this
    6.92 +  show ?thesis
    6.93 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    6.94 +    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.95 +qed
    6.96 +
    6.97 +lemma less_char_Char:
    6.98 +  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    6.99 +proof -
   6.100 +  {
   6.101 +    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
   6.102 +      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
   6.103 +    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
   6.104 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
   6.105 +  }
   6.106 +  note * = this
   6.107 +  show ?thesis
   6.108 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
   6.109 +    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.110 +qed
   6.111 +
   6.112  instantiation char :: distrib_lattice
   6.113  begin
   6.114  
   6.115 @@ -84,14 +89,19 @@
   6.116  definition
   6.117    "(sup \<Colon> char \<Rightarrow> _) = max"
   6.118  
   6.119 -instance   by default (auto simp add:
   6.120 -    inf_char_def sup_char_def min_max.sup_inf_distrib1)
   6.121 +instance proof
   6.122 +qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
   6.123  
   6.124  end
   6.125  
   6.126 -lemma [simp, code]:
   6.127 -  shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
   6.128 -  and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
   6.129 -  unfolding char_less_eq_def char_less_def by simp_all
   6.130 +text {* Legacy aliasses *}
   6.131 +
   6.132 +lemmas nibble_less_eq_def = less_eq_nibble_def
   6.133 +lemmas nibble_less_def = less_nibble_def
   6.134 +lemmas char_less_eq_def = less_eq_char_def
   6.135 +lemmas char_less_def = less_char_def
   6.136 +lemmas char_less_eq_simp = less_eq_char_Char
   6.137 +lemmas char_less_simp = less_char_Char
   6.138  
   6.139  end
   6.140 +
     7.1 --- a/src/HOL/Library/Code_Char.thy	Fri Feb 15 15:22:16 2013 +0100
     7.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Feb 15 11:47:33 2013 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Code generation of pretty characters (and strings) *}
     7.5  
     7.6  theory Code_Char
     7.7 -imports List Code_Evaluation Main
     7.8 +imports Main "~~/src/HOL/Library/Char_ord"
     7.9  begin
    7.10  
    7.11  code_type char
    7.12 @@ -58,4 +58,47 @@
    7.13    (Haskell "_")
    7.14    (Scala "!(_.toList)")
    7.15  
    7.16 +
    7.17 +definition integer_of_char :: "char \<Rightarrow> integer"
    7.18 +where
    7.19 +  "integer_of_char = integer_of_nat o nat_of_char"
    7.20 +
    7.21 +definition char_of_integer :: "integer \<Rightarrow> char"
    7.22 +where
    7.23 +  "char_of_integer = char_of_nat \<circ> nat_of_integer"
    7.24 +
    7.25 +lemma [code]:
    7.26 +  "nat_of_char = nat_of_integer o integer_of_char"
    7.27 +  by (simp add: integer_of_char_def fun_eq_iff)
    7.28 +
    7.29 +lemma [code]:
    7.30 +  "char_of_nat = char_of_integer o integer_of_nat"
    7.31 +  by (simp add: char_of_integer_def fun_eq_iff)
    7.32 +
    7.33 +code_const integer_of_char and char_of_integer
    7.34 +  (SML "!(IntInf.fromInt o Char.ord)"
    7.35 +    and "!(Char.chr o IntInf.toInt)")
    7.36 +  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
    7.37 +    and "Char.chr (Big'_int.int'_of'_big'_int _)")
    7.38 +  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
    7.39 +    and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
    7.40 +  (Scala "BigInt(_.toInt)"
    7.41 +    and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    7.42 +
    7.43 +
    7.44 +code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    7.45 +  (SML "!((_ : char) <= _)")
    7.46 +  (OCaml "!((_ : char) <= _)")
    7.47 +  (Haskell infix 4 "<=")
    7.48 +  (Scala infixl 4 "<=")
    7.49 +  (Eval infixl 6 "<=")
    7.50 +
    7.51 +code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    7.52 +  (SML "!((_ : char) < _)")
    7.53 +  (OCaml "!((_ : char) < _)")
    7.54 +  (Haskell infix 4 "<")
    7.55 +  (Scala infixl 4 "<")
    7.56 +  (Eval infixl 6 "<")
    7.57 +
    7.58  end
    7.59 +
     8.1 --- a/src/HOL/Library/Code_Char_chr.thy	Fri Feb 15 15:22:16 2013 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,31 +0,0 @@
     8.4 -(*  Title:      HOL/Library/Code_Char_chr.thy
     8.5 -    Author:     Florian Haftmann
     8.6 -*)
     8.7 -
     8.8 -header {* Code generation of pretty characters with character codes *}
     8.9 -
    8.10 -theory Code_Char_chr
    8.11 -imports Char_nat Code_Char Code_Target_Int Main
    8.12 -begin
    8.13 -
    8.14 -definition
    8.15 -  "int_of_char = int o nat_of_char"
    8.16 -
    8.17 -lemma [code]:
    8.18 -  "nat_of_char = nat o int_of_char"
    8.19 -  unfolding int_of_char_def by (simp add: fun_eq_iff)
    8.20 -
    8.21 -definition
    8.22 -  "char_of_int = char_of_nat o nat"
    8.23 -
    8.24 -lemma [code]:
    8.25 -  "char_of_nat = char_of_int o int"
    8.26 -  unfolding char_of_int_def by (simp add: fun_eq_iff)
    8.27 -
    8.28 -code_const int_of_char and char_of_int
    8.29 -  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
    8.30 -  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
    8.31 -  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
    8.32 -  (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    8.33 -
    8.34 -end
     9.1 --- a/src/HOL/Library/Code_Char_ord.thy	Fri Feb 15 15:22:16 2013 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,25 +0,0 @@
     9.4 -(*  Title:      HOL/Library/Code_Char_ord.thy
     9.5 -    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
     9.6 -*)
     9.7 -
     9.8 -header {* Code generation of orderings for pretty characters *}
     9.9 -
    9.10 -theory Code_Char_ord
    9.11 -imports Code_Char Char_ord
    9.12 -begin
    9.13 -  
    9.14 -code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    9.15 -  (SML "!((_ : char) <= _)")
    9.16 -  (OCaml "!((_ : char) <= _)")
    9.17 -  (Haskell infix 4 "<=")
    9.18 -  (Scala infixl 4 "<=")
    9.19 -  (Eval infixl 6 "<=")
    9.20 -
    9.21 -code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    9.22 -  (SML "!((_ : char) < _)")
    9.23 -  (OCaml "!((_ : char) < _)")
    9.24 -  (Haskell infix 4 "<")
    9.25 -  (Scala infixl 4 "<")
    9.26 -  (Eval infixl 6 "<")
    9.27 -
    9.28 -end
    9.29 \ No newline at end of file
    10.1 --- a/src/HOL/List.thy	Fri Feb 15 15:22:16 2013 +0100
    10.2 +++ b/src/HOL/List.thy	Fri Feb 15 11:47:33 2013 +0100
    10.3 @@ -1626,6 +1626,35 @@
    10.4  lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
    10.5  by(auto simp:set_conv_nth)
    10.6  
    10.7 +lemma nth_equal_first_eq:
    10.8 +  assumes "x \<notin> set xs"
    10.9 +  assumes "n \<le> length xs"
   10.10 +  shows "(x # xs) ! n = x \<longleftrightarrow> n = 0" (is "?lhs \<longleftrightarrow> ?rhs")
   10.11 +proof
   10.12 +  assume ?lhs
   10.13 +  show ?rhs
   10.14 +  proof (rule ccontr)
   10.15 +    assume "n \<noteq> 0"
   10.16 +    then have "n > 0" by simp
   10.17 +    with `?lhs` have "xs ! (n - 1) = x" by simp
   10.18 +    moreover from `n > 0` `n \<le> length xs` have "n - 1 < length xs" by simp
   10.19 +    ultimately have "\<exists>i<length xs. xs ! i = x" by auto
   10.20 +    with `x \<notin> set xs` in_set_conv_nth [of x xs] show False by simp
   10.21 +  qed
   10.22 +next
   10.23 +  assume ?rhs then show ?lhs by simp
   10.24 +qed
   10.25 +
   10.26 +lemma nth_non_equal_first_eq:
   10.27 +  assumes "x \<noteq> y"
   10.28 +  shows "(x # xs) ! n = y \<longleftrightarrow> xs ! (n - 1) = y \<and> n > 0" (is "?lhs \<longleftrightarrow> ?rhs")
   10.29 +proof
   10.30 +  assume "?lhs" with assms have "n > 0" by (cases n) simp_all
   10.31 +  with `?lhs` show ?rhs by simp
   10.32 +next
   10.33 +  assume "?rhs" then show "?lhs" by simp
   10.34 +qed
   10.35 +
   10.36  lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
   10.37  by (auto simp add: set_conv_nth)
   10.38  
   10.39 @@ -2614,6 +2643,22 @@
   10.40    "set (List.product xs ys) = set xs \<times> set ys"
   10.41    by (induct xs) auto
   10.42  
   10.43 +lemma length_product [simp]:
   10.44 +  "length (List.product xs ys) = length xs * length ys"
   10.45 +  by (induct xs) simp_all
   10.46 +
   10.47 +lemma product_nth:
   10.48 +  assumes "n < length xs * length ys"
   10.49 +  shows "List.product xs ys ! n = (xs ! (n div length ys), ys ! (n mod length ys))"
   10.50 +using assms proof (induct xs arbitrary: n)
   10.51 +  case Nil then show ?case by simp
   10.52 +next
   10.53 +  case (Cons x xs n)
   10.54 +  then have "length ys > 0" by auto
   10.55 +  with Cons show ?case
   10.56 +    by (auto simp add: nth_append not_less le_mod_geq le_div_geq)
   10.57 +qed
   10.58 +
   10.59  
   10.60  subsubsection {* @{const fold} with natural argument order *}
   10.61  
    11.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 15 15:22:16 2013 +0100
    11.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 15 11:47:33 2013 +0100
    11.3 @@ -230,8 +230,7 @@
    11.4    "nibble"]
    11.5  
    11.6  val forbidden_consts =
    11.7 - [@{const_name nibble_pair_of_char}, @{const_name "TYPE"},
    11.8 -  @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
    11.9 + [@{const_name "TYPE"}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
   11.10  
   11.11  fun is_forbidden_theorem (s, th) =
   11.12    let val consts = Term.add_const_names (prop_of th) [] in
    12.1 --- a/src/HOL/ROOT	Fri Feb 15 15:22:16 2013 +0100
    12.2 +++ b/src/HOL/ROOT	Fri Feb 15 11:47:33 2013 +0100
    12.3 @@ -24,8 +24,7 @@
    12.4      List_lexord
    12.5      Sublist_Order
    12.6      Finite_Lattice
    12.7 -    Code_Char_chr
    12.8 -    Code_Char_ord
    12.9 +    Code_Char
   12.10      Product_Lexorder
   12.11      Product_Order
   12.12      (* Code_Prolog  FIXME cf. 76965c356d2a *)
    13.1 --- a/src/HOL/String.thy	Fri Feb 15 15:22:16 2013 +0100
    13.2 +++ b/src/HOL/String.thy	Fri Feb 15 11:47:33 2013 +0100
    13.3 @@ -49,6 +49,72 @@
    13.4    "card (UNIV :: nibble set) = 16"
    13.5    by (simp add: card_UNIV_length_enum enum_nibble_def)
    13.6  
    13.7 +primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
    13.8 +where
    13.9 +  "nat_of_nibble Nibble0 = 0"
   13.10 +| "nat_of_nibble Nibble1 = 1"
   13.11 +| "nat_of_nibble Nibble2 = 2"
   13.12 +| "nat_of_nibble Nibble3 = 3"
   13.13 +| "nat_of_nibble Nibble4 = 4"
   13.14 +| "nat_of_nibble Nibble5 = 5"
   13.15 +| "nat_of_nibble Nibble6 = 6"
   13.16 +| "nat_of_nibble Nibble7 = 7"
   13.17 +| "nat_of_nibble Nibble8 = 8"
   13.18 +| "nat_of_nibble Nibble9 = 9"
   13.19 +| "nat_of_nibble NibbleA = 10"
   13.20 +| "nat_of_nibble NibbleB = 11"
   13.21 +| "nat_of_nibble NibbleC = 12"
   13.22 +| "nat_of_nibble NibbleD = 13"
   13.23 +| "nat_of_nibble NibbleE = 14"
   13.24 +| "nat_of_nibble NibbleF = 15"
   13.25 +
   13.26 +definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
   13.27 +  "nibble_of_nat n = Enum.enum ! (n mod 16)"
   13.28 +
   13.29 +lemma nibble_of_nat_simps [simp]:
   13.30 +  "nibble_of_nat  0 = Nibble0"
   13.31 +  "nibble_of_nat  1 = Nibble1"
   13.32 +  "nibble_of_nat  2 = Nibble2"
   13.33 +  "nibble_of_nat  3 = Nibble3"
   13.34 +  "nibble_of_nat  4 = Nibble4"
   13.35 +  "nibble_of_nat  5 = Nibble5"
   13.36 +  "nibble_of_nat  6 = Nibble6"
   13.37 +  "nibble_of_nat  7 = Nibble7"
   13.38 +  "nibble_of_nat  8 = Nibble8"
   13.39 +  "nibble_of_nat  9 = Nibble9"
   13.40 +  "nibble_of_nat 10 = NibbleA"
   13.41 +  "nibble_of_nat 11 = NibbleB"
   13.42 +  "nibble_of_nat 12 = NibbleC"
   13.43 +  "nibble_of_nat 13 = NibbleD"
   13.44 +  "nibble_of_nat 14 = NibbleE"
   13.45 +  "nibble_of_nat 15 = NibbleF"
   13.46 +  unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
   13.47 +
   13.48 +lemma nibble_of_nat_of_nibble [simp]:
   13.49 +  "nibble_of_nat (nat_of_nibble x) = x"
   13.50 +  by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
   13.51 +
   13.52 +lemma nat_of_nibble_of_nat [simp]:
   13.53 +  "nat_of_nibble (nibble_of_nat n) = n mod 16"
   13.54 +  by (cases "nibble_of_nat n")
   13.55 +     (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
   13.56 +
   13.57 +lemma inj_nat_of_nibble:
   13.58 +  "inj nat_of_nibble"
   13.59 +  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
   13.60 +
   13.61 +lemma nat_of_nibble_eq_iff:
   13.62 +  "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
   13.63 +  by (rule inj_eq) (rule inj_nat_of_nibble)
   13.64 +
   13.65 +lemma nat_of_nibble_less_16:
   13.66 +  "nat_of_nibble x < 16"
   13.67 +  by (cases x) auto
   13.68 +
   13.69 +lemma nibble_of_nat_mod_16:
   13.70 +  "nibble_of_nat (n mod 16) = nibble_of_nat n"
   13.71 +  by (simp add: nibble_of_nat_def)
   13.72 +
   13.73  datatype char = Char nibble nibble
   13.74    -- "Note: canonical order of character encoding coincides with standard term ordering"
   13.75  
   13.76 @@ -154,13 +220,15 @@
   13.77  definition
   13.78    "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
   13.79  
   13.80 +lemma enum_char_product_enum_nibble:
   13.81 +  "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
   13.82 +  by (simp add: enum_char_def enum_nibble_def)
   13.83 +
   13.84  instance proof
   13.85 -  have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
   13.86 -    by (simp add: enum_char_def enum_nibble_def)
   13.87    show UNIV: "UNIV = set (Enum.enum :: char list)"
   13.88 -    by (simp add: enum UNIV_char product_list_set enum_UNIV)
   13.89 +    by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
   13.90    show "distinct (Enum.enum :: char list)"
   13.91 -    by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct)
   13.92 +    by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
   13.93    show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
   13.94      by (simp add: UNIV enum_all_char_def list_all_iff)
   13.95    show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
   13.96 @@ -173,30 +241,115 @@
   13.97    "card (UNIV :: char set) = 256"
   13.98    by (simp add: card_UNIV_length_enum enum_char_def)
   13.99  
  13.100 -primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
  13.101 -  "nibble_pair_of_char (Char n m) = (n, m)"
  13.102 +definition nat_of_char :: "char \<Rightarrow> nat"
  13.103 +where
  13.104 +  "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
  13.105 +
  13.106 +lemma nat_of_char_Char:
  13.107 +  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
  13.108 +  by (simp add: nat_of_char_def)
  13.109  
  13.110  setup {*
  13.111  let
  13.112    val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
  13.113 -  val thms = map_product
  13.114 -   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
  13.115 -      nibbles nibbles;
  13.116 +  val simpset = HOL_ss addsimps
  13.117 +    @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
  13.118 +  fun mk_code_eqn x y =
  13.119 +    Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
  13.120 +    |> simplify simpset;
  13.121 +  val code_eqns = map_product mk_code_eqn nibbles nibbles;
  13.122  in
  13.123    Global_Theory.note_thmss ""
  13.124 -    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
  13.125 -  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
  13.126 +    [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
  13.127 +  #> snd
  13.128  end
  13.129  *}
  13.130  
  13.131 -lemma char_case_nibble_pair [code, code_unfold]:
  13.132 -  "char_case f = split f o nibble_pair_of_char"
  13.133 +declare nat_of_char_simps [code]
  13.134 +
  13.135 +lemma nibble_of_nat_of_char_div_16:
  13.136 +  "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
  13.137 +  by (cases c)
  13.138 +    (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
  13.139 +
  13.140 +lemma nibble_of_nat_nat_of_char:
  13.141 +  "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
  13.142 +proof (cases c)
  13.143 +  case (Char x y)
  13.144 +  then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
  13.145 +    by (simp add: nibble_of_nat_mod_16)
  13.146 +  then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
  13.147 +    by (simp only: nibble_of_nat_mod_16)
  13.148 +  with Char show ?thesis by (simp add: nat_of_char_def add_commute)
  13.149 +qed
  13.150 +
  13.151 +code_datatype Char -- {* drop case certificate for char *}
  13.152 +
  13.153 +lemma char_case_code [code]:
  13.154 +  "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
  13.155 +  by (cases c)
  13.156 +    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
  13.157 +
  13.158 +lemma [code]:
  13.159 +  "char_rec = char_case"
  13.160    by (simp add: fun_eq_iff split: char.split)
  13.161  
  13.162 -lemma char_rec_nibble_pair [code, code_unfold]:
  13.163 -  "char_rec f = split f o nibble_pair_of_char"
  13.164 -  unfolding char_case_nibble_pair [symmetric]
  13.165 -  by (simp add: fun_eq_iff split: char.split)
  13.166 +definition char_of_nat :: "nat \<Rightarrow> char" where
  13.167 +  "char_of_nat n = Enum.enum ! (n mod 256)"
  13.168 +
  13.169 +lemma char_of_nat_Char_nibbles:
  13.170 +  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
  13.171 +proof -
  13.172 +  from mod_mult2_eq [of n 16 16]
  13.173 +  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
  13.174 +  then show ?thesis
  13.175 +    by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
  13.176 +      card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
  13.177 +qed
  13.178 +
  13.179 +lemma char_of_nat_of_char [simp]:
  13.180 +  "char_of_nat (nat_of_char c) = c"
  13.181 +  by (cases c)
  13.182 +    (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
  13.183 +
  13.184 +lemma nat_of_char_of_nat [simp]:
  13.185 +  "nat_of_char (char_of_nat n) = n mod 256"
  13.186 +proof -
  13.187 +  have "n mod 256 = n mod (16 * 16)" by simp
  13.188 +  then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
  13.189 +  then show ?thesis
  13.190 +    by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
  13.191 +qed
  13.192 +
  13.193 +lemma inj_nat_of_char:
  13.194 +  "inj nat_of_char"
  13.195 +  by (rule inj_on_inverseI) (rule char_of_nat_of_char)
  13.196 +
  13.197 +lemma nat_of_char_eq_iff:
  13.198 +  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
  13.199 +  by (rule inj_eq) (rule inj_nat_of_char)
  13.200 +
  13.201 +lemma nat_of_char_less_256:
  13.202 +  "nat_of_char c < 256"
  13.203 +proof (cases c)
  13.204 +  case (Char x y)
  13.205 +  with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
  13.206 +  show ?thesis by (simp add: nat_of_char_def)
  13.207 +qed
  13.208 +
  13.209 +lemma char_of_nat_mod_256:
  13.210 +  "char_of_nat (n mod 256) = char_of_nat n"
  13.211 +proof -
  13.212 +  from nibble_of_nat_mod_16 [of "n mod 256"]
  13.213 +  have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
  13.214 +  with nibble_of_nat_mod_16 [of n]
  13.215 +  have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
  13.216 +  have "n mod 256 = n mod (16 * 16)" by simp
  13.217 +  then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
  13.218 +  show ?thesis
  13.219 +    by (simp add: char_of_nat_Char_nibbles *)
  13.220 +     (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
  13.221 +qed
  13.222  
  13.223  
  13.224  subsection {* Strings as dedicated type *}
  13.225 @@ -228,8 +381,9 @@
  13.226  
  13.227  end
  13.228  
  13.229 -lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
  13.230 -by(simp add: STR_inject)
  13.231 +lemma STR_inject' [simp]:
  13.232 +  "STR xs = STR ys \<longleftrightarrow> xs = ys"
  13.233 +  by (simp add: STR_inject)
  13.234  
  13.235  
  13.236  subsection {* Code generator *}
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Feb 15 15:22:16 2013 +0100
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Feb 15 11:47:33 2013 +0100
    14.3 @@ -155,7 +155,7 @@
    14.4  fun multi_base_blacklist ctxt ho_atp =
    14.5    ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    14.6     "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
    14.7 -   "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
    14.8 +   "weak_case_cong", "nat_of_char_simps", "nibble.simps",
    14.9     "nibble.distinct"]
   14.10    |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
   14.11          append ["induct", "inducts"]
    15.1 --- a/src/HOL/Tools/string_code.ML	Fri Feb 15 15:22:16 2013 +0100
    15.2 +++ b/src/HOL/Tools/string_code.ML	Fri Feb 15 11:47:33 2013 +0100
    15.3 @@ -27,14 +27,14 @@
    15.4      | _ => NONE
    15.5    end;
    15.6     
    15.7 -fun implode_string char' nibbles' mk_char mk_string ts =
    15.8 +fun implode_string literals char' nibbles' ts =
    15.9    let
   15.10      fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
   15.11            if c = char' then decode_char nibbles' (t1, t2) else NONE
   15.12        | implode_char _ = NONE;
   15.13      val ts' = map_filter implode_char ts;
   15.14    in if length ts = length ts'
   15.15 -    then (SOME o Code_Printer.str o mk_string o implode) ts'
   15.16 +    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
   15.17      else NONE
   15.18    end;
   15.19  
   15.20 @@ -50,10 +50,9 @@
   15.21  
   15.22  fun add_literal_list_string target =
   15.23    let
   15.24 -    fun pretty literals (nil' :: cons' :: char' :: nibbles') pr thm vars fxy [(t1, _), (t2, _)] =
   15.25 +    fun pretty literals (nil' :: cons' :: char' :: nibbles') pr _ vars fxy [(t1, _), (t2, _)] =
   15.26        case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
   15.27 -       of SOME ts => (case implode_string char' nibbles'
   15.28 -          (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
   15.29 +       of SOME ts => (case implode_string literals char' nibbles' ts
   15.30               of SOME p => p
   15.31                | NONE =>
   15.32                    Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
   15.33 @@ -77,8 +76,7 @@
   15.34    let
   15.35      fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
   15.36        case List_Code.implode_list nil' cons' t
   15.37 -       of SOME ts => (case implode_string char' nibbles'
   15.38 -          (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
   15.39 +       of SOME ts => (case implode_string literals char' nibbles' ts
   15.40               of SOME p => p
   15.41                | NONE => Code_Printer.eqn_error thm "Illegal message expression")
   15.42          | NONE => Code_Printer.eqn_error thm "Illegal message expression";
    16.1 --- a/src/HOL/Tools/string_syntax.ML	Fri Feb 15 15:22:16 2013 +0100
    16.2 +++ b/src/HOL/Tools/string_syntax.ML	Fri Feb 15 11:47:33 2013 +0100
    16.3 @@ -81,7 +81,7 @@
    16.4  fun list_ast_tr' [args] =
    16.5        Ast.Appl [Ast.Constant @{syntax_const "_String"},
    16.6          syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
    16.7 -  | list_ast_tr' ts = raise Match;
    16.8 +  | list_ast_tr' _ = raise Match;
    16.9  
   16.10  
   16.11  (* theory setup *)