# HG changeset patch
# User haftmann
# Date 1360925253 -3600
# Node ID 599ff65b85e27429e07754124ea92755798c4254
# Parent  3fe7242f834625614a0701f02816bc2885a2bfc8
systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char

diff -r 3fe7242f8346 -r 599ff65b85e2 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -150,10 +150,6 @@
        containing both @{text "Code_Target_Nat"} and
        @{text "Code_Target_Int"}.
 
-    \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but
-       also offers treatment of character codes; includes @{text
-       "Code_Char"}.
-
     \item[@{text "Efficient_Nat"}] \label{eff_nat} implements
        natural numbers by integers, which in general will result in
        higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -119,11 +119,10 @@
   = Code_Evaluation.term_of" ..
 
 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
-  "Code_Evaluation.term_of c =
-    (let (n, m) = nibble_pair_of_char c
-  in Code_Evaluation.App (Code_Evaluation.App
+  "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
+   Code_Evaluation.App (Code_Evaluation.App
     (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
-      (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
+      (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
   by (subst term_of_anything) rule 
 
 code_type "term"
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -6,7 +6,7 @@
 theory Candidates
 imports
   Complex_Main
-  Library
+  "~~/src/HOL/Library/Library"
   "~~/src/HOL/Library/Sublist"
   "~~/src/HOL/Number_Theory/Primes"
   "~~/src/HOL/ex/Records"
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Codegenerator_Test/Candidates_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -4,7 +4,7 @@
 header {* Generating code using pretty literals and natural number literals  *}
 
 theory Candidates_Pretty
-imports Candidates Code_Char_ord Code_Target_Numeral
+imports Candidates Code_Char Code_Target_Numeral
 begin
 
 end
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Fri Feb 15 15:22:16 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,199 +0,0 @@
-(*  Title:      HOL/Library/Char_nat.thy
-    Author:     Norbert Voelker, Florian Haftmann
-*)
-
-header {* Mapping between characters and natural numbers *}
-
-theory Char_nat
-imports List Main
-begin
-
-text {* Conversions between nibbles and natural numbers in [0..15]. *}
-
-primrec
-  nat_of_nibble :: "nibble \<Rightarrow> nat" where
-    "nat_of_nibble Nibble0 = 0"
-  | "nat_of_nibble Nibble1 = 1"
-  | "nat_of_nibble Nibble2 = 2"
-  | "nat_of_nibble Nibble3 = 3"
-  | "nat_of_nibble Nibble4 = 4"
-  | "nat_of_nibble Nibble5 = 5"
-  | "nat_of_nibble Nibble6 = 6"
-  | "nat_of_nibble Nibble7 = 7"
-  | "nat_of_nibble Nibble8 = 8"
-  | "nat_of_nibble Nibble9 = 9"
-  | "nat_of_nibble NibbleA = 10"
-  | "nat_of_nibble NibbleB = 11"
-  | "nat_of_nibble NibbleC = 12"
-  | "nat_of_nibble NibbleD = 13"
-  | "nat_of_nibble NibbleE = 14"
-  | "nat_of_nibble NibbleF = 15"
-
-definition
-  nibble_of_nat :: "nat \<Rightarrow> nibble" where
-  "nibble_of_nat x = (let y = x mod 16 in
-    if y = 0 then Nibble0 else
-    if y = 1 then Nibble1 else
-    if y = 2 then Nibble2 else
-    if y = 3 then Nibble3 else
-    if y = 4 then Nibble4 else
-    if y = 5 then Nibble5 else
-    if y = 6 then Nibble6 else
-    if y = 7 then Nibble7 else
-    if y = 8 then Nibble8 else
-    if y = 9 then Nibble9 else
-    if y = 10 then NibbleA else
-    if y = 11 then NibbleB else
-    if y = 12 then NibbleC else
-    if y = 13 then NibbleD else
-    if y = 14 then NibbleE else
-    NibbleF)"
-
-lemma nibble_of_nat_norm:
-  "nibble_of_nat (n mod 16) = nibble_of_nat n"
-  unfolding nibble_of_nat_def mod_mod_trivial ..
-
-lemma nibble_of_nat_simps [simp]:
-  "nibble_of_nat  0 = Nibble0"
-  "nibble_of_nat  1 = Nibble1"
-  "nibble_of_nat  2 = Nibble2"
-  "nibble_of_nat  3 = Nibble3"
-  "nibble_of_nat  4 = Nibble4"
-  "nibble_of_nat  5 = Nibble5"
-  "nibble_of_nat  6 = Nibble6"
-  "nibble_of_nat  7 = Nibble7"
-  "nibble_of_nat  8 = Nibble8"
-  "nibble_of_nat  9 = Nibble9"
-  "nibble_of_nat 10 = NibbleA"
-  "nibble_of_nat 11 = NibbleB"
-  "nibble_of_nat 12 = NibbleC"
-  "nibble_of_nat 13 = NibbleD"
-  "nibble_of_nat 14 = NibbleE"
-  "nibble_of_nat 15 = NibbleF"
-  unfolding nibble_of_nat_def by auto
-
-lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
-  by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
-
-lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
-proof -
-  have nibble_nat_enum:
-    "n mod 16 \<in> {15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0}"
-  proof -
-    have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
-    have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
-      (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
-    from this [simplified set_unfold atLeastAtMost_singleton]
-    show ?thesis by (simp add: numeral_2_eq_2 [symmetric])
-  qed
-  then show ?thesis unfolding nibble_of_nat_def
-  by auto
-qed
-
-lemma inj_nat_of_nibble: "inj nat_of_nibble"
-  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
-
-lemma nat_of_nibble_eq: "nat_of_nibble n = nat_of_nibble m \<longleftrightarrow> n = m"
-  by (rule inj_eq) (rule inj_nat_of_nibble)
-
-lemma nat_of_nibble_less_16: "nat_of_nibble n < 16"
-  by (cases n) auto
-
-lemma nat_of_nibble_div_16: "nat_of_nibble n div 16 = 0"
-  by (cases n) auto
-
-
-text {* Conversion between chars and nats. *}
-
-definition
-  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
-  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
-
-lemma nibble_of_pair [code]:
-  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
-  unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
-
-primrec
-  nat_of_char :: "char \<Rightarrow> nat" where
-  "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"
-
-lemmas [simp del] = nat_of_char.simps
-
-definition
-  char_of_nat :: "nat \<Rightarrow> char" where
-  char_of_nat_def: "char_of_nat n = split Char (nibble_pair_of_nat n)"
-
-lemma Char_char_of_nat:
-  "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
-  unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
-  by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
-
-lemma char_of_nat_of_char:
-  "char_of_nat (nat_of_char c) = c"
-  by (cases c) (simp add: nat_of_char.simps, simp add: Char_char_of_nat)
-
-lemma nat_of_char_of_nat:
-  "nat_of_char (char_of_nat n) = n mod 256"
-proof -
-  from mod_div_equality [of n, symmetric, of 16]
-  have mod_mult_self3: "\<And>m k n \<Colon> nat. (k * n + m) mod n = m mod n"
-  proof -
-    fix m k n :: nat
-    show "(k * n + m) mod n = m mod n"
-      by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
-  qed
-  from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
-    and k: "k = n div 256" and l: "l = n mod 256" by blast
-  have 16: "(0::nat) < 16" by auto
-  have 256: "(256 :: nat) = 16 * 16" by auto
-  have l_256: "l mod 256 = l" using l by auto
-  have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
-    using l by auto
-  have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
-    unfolding 256 mult_assoc [symmetric] mod_mult_self2_is_0 by simp
-  have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
-    unfolding div_add1_eq [of "k * 256" l 16] aux2 256
-      mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
-  have aux4: "(k * 256 + l) mod 16 = l mod 16"
-    unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
-  show ?thesis
-    by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
-      nat_of_nibble_of_nat mult_mod_left
-      n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
-qed
-
-lemma nibble_pair_of_nat_char:
-  "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
-proof -
-  have nat_of_nibble_256:
-    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 =
-      nat_of_nibble n * 16 + nat_of_nibble m"
-  proof -
-    fix n m
-    have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
-      using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: eval_nat_numeral)
-    have less_eq_240: "nat_of_nibble n * 16 \<le> 240"
-      using nat_of_nibble_less_eq_15 by auto
-    have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
-      by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
-    then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
-    then show "?rhs mod 256 = ?rhs" by auto
-  qed
-  show ?thesis
-    unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
-    by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
-qed
-
-
-text {* Code generator setup *}
-
-code_modulename SML
-  Char_nat String
-
-code_modulename OCaml
-  Char_nat String
-
-code_modulename Haskell
-  Char_nat String
-
-end
\ No newline at end of file
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Library/Char_ord.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -5,43 +5,20 @@
 header {* Order on characters *}
 
 theory Char_ord
-imports Char_nat
+imports Main
 begin
 
 instantiation nibble :: linorder
 begin
 
 definition
-  nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+  "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
 
 definition
-  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
+  "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
 
 instance proof
-  fix n :: nibble
-  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
-next
-  fix n m q :: nibble
-  assume "n \<le> m"
-    and "m \<le> q"
-  then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
-next
-  fix n m :: nibble
-  assume "n \<le> m"
-    and "m \<le> n"
-  then show "n = m"
-    unfolding nibble_less_eq_def nibble_less_def
-    by (auto simp add: nat_of_nibble_eq)
-next
-  fix n m :: nibble
-  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
-    unfolding nibble_less_eq_def nibble_less_def less_le
-    by (auto simp add: nat_of_nibble_eq)
-next
-  fix n m :: nibble
-  show "n \<le> m \<or> m \<le> n"
-    unfolding nibble_less_eq_def by auto
-qed
+qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
 
 end
 
@@ -54,8 +31,8 @@
 definition
   "(sup \<Colon> nibble \<Rightarrow> _) = max"
 
-instance by default (auto simp add:
-    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
+instance proof
+qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
 
 end
 
@@ -63,18 +40,46 @@
 begin
 
 definition
-  char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
-    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
+  "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
 
 definition
-  char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
-    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
+  "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
 
-instance
-  by default (auto simp: char_less_eq_def char_less_def split: char.splits)
+instance proof
+qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
 
 end
 
+lemma less_eq_char_Char:
+  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
+proof -
+  {
+    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
+      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
+    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
+  }
+  note * = this
+  show ?thesis
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
+    by (auto simp add: less_eq_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
+qed
+
+lemma less_char_Char:
+  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
+proof -
+  {
+    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
+      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
+    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
+  }
+  note * = this
+  show ?thesis
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
+    by (auto simp add: less_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
+qed
+
 instantiation char :: distrib_lattice
 begin
 
@@ -84,14 +89,19 @@
 definition
   "(sup \<Colon> char \<Rightarrow> _) = max"
 
-instance   by default (auto simp add:
-    inf_char_def sup_char_def min_max.sup_inf_distrib1)
+instance proof
+qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
 
 end
 
-lemma [simp, code]:
-  shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
-  and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
-  unfolding char_less_eq_def char_less_def by simp_all
+text {* Legacy aliasses *}
+
+lemmas nibble_less_eq_def = less_eq_nibble_def
+lemmas nibble_less_def = less_nibble_def
+lemmas char_less_eq_def = less_eq_char_def
+lemmas char_less_def = less_char_def
+lemmas char_less_eq_simp = less_eq_char_Char
+lemmas char_less_simp = less_char_Char
 
 end
+
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Library/Code_Char.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -5,7 +5,7 @@
 header {* Code generation of pretty characters (and strings) *}
 
 theory Code_Char
-imports List Code_Evaluation Main
+imports Main "~~/src/HOL/Library/Char_ord"
 begin
 
 code_type char
@@ -58,4 +58,47 @@
   (Haskell "_")
   (Scala "!(_.toList)")
 
+
+definition integer_of_char :: "char \<Rightarrow> integer"
+where
+  "integer_of_char = integer_of_nat o nat_of_char"
+
+definition char_of_integer :: "integer \<Rightarrow> char"
+where
+  "char_of_integer = char_of_nat \<circ> nat_of_integer"
+
+lemma [code]:
+  "nat_of_char = nat_of_integer o integer_of_char"
+  by (simp add: integer_of_char_def fun_eq_iff)
+
+lemma [code]:
+  "char_of_nat = char_of_integer o integer_of_nat"
+  by (simp add: char_of_integer_def fun_eq_iff)
+
+code_const integer_of_char and char_of_integer
+  (SML "!(IntInf.fromInt o Char.ord)"
+    and "!(Char.chr o IntInf.toInt)")
+  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
+    and "Char.chr (Big'_int.int'_of'_big'_int _)")
+  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
+    and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
+  (Scala "BigInt(_.toInt)"
+    and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
+
+
+code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) <= _)")
+  (OCaml "!((_ : char) <= _)")
+  (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
+  (Eval infixl 6 "<=")
+
+code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) < _)")
+  (OCaml "!((_ : char) < _)")
+  (Haskell infix 4 "<")
+  (Scala infixl 4 "<")
+  (Eval infixl 6 "<")
+
 end
+
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Fri Feb 15 15:22:16 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOL/Library/Code_Char_chr.thy
-    Author:     Florian Haftmann
-*)
-
-header {* Code generation of pretty characters with character codes *}
-
-theory Code_Char_chr
-imports Char_nat Code_Char Code_Target_Int Main
-begin
-
-definition
-  "int_of_char = int o nat_of_char"
-
-lemma [code]:
-  "nat_of_char = nat o int_of_char"
-  unfolding int_of_char_def by (simp add: fun_eq_iff)
-
-definition
-  "char_of_int = char_of_nat o nat"
-
-lemma [code]:
-  "char_of_nat = char_of_int o int"
-  unfolding char_of_int_def by (simp add: fun_eq_iff)
-
-code_const int_of_char and char_of_int
-  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
-  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
-  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
-  (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
-
-end
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Library/Code_Char_ord.thy
--- a/src/HOL/Library/Code_Char_ord.thy	Fri Feb 15 15:22:16 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      HOL/Library/Code_Char_ord.thy
-    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
-*)
-
-header {* Code generation of orderings for pretty characters *}
-
-theory Code_Char_ord
-imports Code_Char Char_ord
-begin
-  
-code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
-  (SML "!((_ : char) <= _)")
-  (OCaml "!((_ : char) <= _)")
-  (Haskell infix 4 "<=")
-  (Scala infixl 4 "<=")
-  (Eval infixl 6 "<=")
-
-code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
-  (SML "!((_ : char) < _)")
-  (OCaml "!((_ : char) < _)")
-  (Haskell infix 4 "<")
-  (Scala infixl 4 "<")
-  (Eval infixl 6 "<")
-
-end
\ No newline at end of file
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/List.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -1626,6 +1626,35 @@
 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
 by(auto simp:set_conv_nth)
 
+lemma nth_equal_first_eq:
+  assumes "x \<notin> set xs"
+  assumes "n \<le> length xs"
+  shows "(x # xs) ! n = x \<longleftrightarrow> n = 0" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  show ?rhs
+  proof (rule ccontr)
+    assume "n \<noteq> 0"
+    then have "n > 0" by simp
+    with `?lhs` have "xs ! (n - 1) = x" by simp
+    moreover from `n > 0` `n \<le> length xs` have "n - 1 < length xs" by simp
+    ultimately have "\<exists>i<length xs. xs ! i = x" by auto
+    with `x \<notin> set xs` in_set_conv_nth [of x xs] show False by simp
+  qed
+next
+  assume ?rhs then show ?lhs by simp
+qed
+
+lemma nth_non_equal_first_eq:
+  assumes "x \<noteq> y"
+  shows "(x # xs) ! n = y \<longleftrightarrow> xs ! (n - 1) = y \<and> n > 0" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume "?lhs" with assms have "n > 0" by (cases n) simp_all
+  with `?lhs` show ?rhs by simp
+next
+  assume "?rhs" then show "?lhs" by simp
+qed
+
 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
 by (auto simp add: set_conv_nth)
 
@@ -2614,6 +2643,22 @@
   "set (List.product xs ys) = set xs \<times> set ys"
   by (induct xs) auto
 
+lemma length_product [simp]:
+  "length (List.product xs ys) = length xs * length ys"
+  by (induct xs) simp_all
+
+lemma product_nth:
+  assumes "n < length xs * length ys"
+  shows "List.product xs ys ! n = (xs ! (n div length ys), ys ! (n mod length ys))"
+using assms proof (induct xs arbitrary: n)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs n)
+  then have "length ys > 0" by auto
+  with Cons show ?case
+    by (auto simp add: nth_append not_less le_mod_geq le_div_geq)
+qed
+
 
 subsubsection {* @{const fold} with natural argument order *}
 
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 15 11:47:33 2013 +0100
@@ -230,8 +230,7 @@
   "nibble"]
 
 val forbidden_consts =
- [@{const_name nibble_pair_of_char}, @{const_name "TYPE"},
-  @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
+ [@{const_name "TYPE"}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
 
 fun is_forbidden_theorem (s, th) =
   let val consts = Term.add_const_names (prop_of th) [] in
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/ROOT	Fri Feb 15 11:47:33 2013 +0100
@@ -24,8 +24,7 @@
     List_lexord
     Sublist_Order
     Finite_Lattice
-    Code_Char_chr
-    Code_Char_ord
+    Code_Char
     Product_Lexorder
     Product_Order
     (* Code_Prolog  FIXME cf. 76965c356d2a *)
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/String.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -49,6 +49,72 @@
   "card (UNIV :: nibble set) = 16"
   by (simp add: card_UNIV_length_enum enum_nibble_def)
 
+primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
+where
+  "nat_of_nibble Nibble0 = 0"
+| "nat_of_nibble Nibble1 = 1"
+| "nat_of_nibble Nibble2 = 2"
+| "nat_of_nibble Nibble3 = 3"
+| "nat_of_nibble Nibble4 = 4"
+| "nat_of_nibble Nibble5 = 5"
+| "nat_of_nibble Nibble6 = 6"
+| "nat_of_nibble Nibble7 = 7"
+| "nat_of_nibble Nibble8 = 8"
+| "nat_of_nibble Nibble9 = 9"
+| "nat_of_nibble NibbleA = 10"
+| "nat_of_nibble NibbleB = 11"
+| "nat_of_nibble NibbleC = 12"
+| "nat_of_nibble NibbleD = 13"
+| "nat_of_nibble NibbleE = 14"
+| "nat_of_nibble NibbleF = 15"
+
+definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
+  "nibble_of_nat n = Enum.enum ! (n mod 16)"
+
+lemma nibble_of_nat_simps [simp]:
+  "nibble_of_nat  0 = Nibble0"
+  "nibble_of_nat  1 = Nibble1"
+  "nibble_of_nat  2 = Nibble2"
+  "nibble_of_nat  3 = Nibble3"
+  "nibble_of_nat  4 = Nibble4"
+  "nibble_of_nat  5 = Nibble5"
+  "nibble_of_nat  6 = Nibble6"
+  "nibble_of_nat  7 = Nibble7"
+  "nibble_of_nat  8 = Nibble8"
+  "nibble_of_nat  9 = Nibble9"
+  "nibble_of_nat 10 = NibbleA"
+  "nibble_of_nat 11 = NibbleB"
+  "nibble_of_nat 12 = NibbleC"
+  "nibble_of_nat 13 = NibbleD"
+  "nibble_of_nat 14 = NibbleE"
+  "nibble_of_nat 15 = NibbleF"
+  unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
+
+lemma nibble_of_nat_of_nibble [simp]:
+  "nibble_of_nat (nat_of_nibble x) = x"
+  by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
+
+lemma nat_of_nibble_of_nat [simp]:
+  "nat_of_nibble (nibble_of_nat n) = n mod 16"
+  by (cases "nibble_of_nat n")
+     (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
+
+lemma inj_nat_of_nibble:
+  "inj nat_of_nibble"
+  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
+
+lemma nat_of_nibble_eq_iff:
+  "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
+  by (rule inj_eq) (rule inj_nat_of_nibble)
+
+lemma nat_of_nibble_less_16:
+  "nat_of_nibble x < 16"
+  by (cases x) auto
+
+lemma nibble_of_nat_mod_16:
+  "nibble_of_nat (n mod 16) = nibble_of_nat n"
+  by (simp add: nibble_of_nat_def)
+
 datatype char = Char nibble nibble
   -- "Note: canonical order of character encoding coincides with standard term ordering"
 
@@ -154,13 +220,15 @@
 definition
   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
 
+lemma enum_char_product_enum_nibble:
+  "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
+  by (simp add: enum_char_def enum_nibble_def)
+
 instance proof
-  have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
-    by (simp add: enum_char_def enum_nibble_def)
   show UNIV: "UNIV = set (Enum.enum :: char list)"
-    by (simp add: enum UNIV_char product_list_set enum_UNIV)
+    by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
   show "distinct (Enum.enum :: char list)"
-    by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct)
+    by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
     by (simp add: UNIV enum_all_char_def list_all_iff)
   show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
@@ -173,30 +241,115 @@
   "card (UNIV :: char set) = 256"
   by (simp add: card_UNIV_length_enum enum_char_def)
 
-primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
-  "nibble_pair_of_char (Char n m) = (n, m)"
+definition nat_of_char :: "char \<Rightarrow> nat"
+where
+  "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
+
+lemma nat_of_char_Char:
+  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
+  by (simp add: nat_of_char_def)
 
 setup {*
 let
   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
-  val thms = map_product
-   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
-      nibbles nibbles;
+  val simpset = HOL_ss addsimps
+    @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
+  fun mk_code_eqn x y =
+    Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
+    |> simplify simpset;
+  val code_eqns = map_product mk_code_eqn nibbles nibbles;
 in
   Global_Theory.note_thmss ""
-    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
-  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
+    [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
+  #> snd
 end
 *}
 
-lemma char_case_nibble_pair [code, code_unfold]:
-  "char_case f = split f o nibble_pair_of_char"
+declare nat_of_char_simps [code]
+
+lemma nibble_of_nat_of_char_div_16:
+  "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
+  by (cases c)
+    (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
+
+lemma nibble_of_nat_nat_of_char:
+  "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
+proof (cases c)
+  case (Char x y)
+  then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
+    by (simp add: nibble_of_nat_mod_16)
+  then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
+    by (simp only: nibble_of_nat_mod_16)
+  with Char show ?thesis by (simp add: nat_of_char_def add_commute)
+qed
+
+code_datatype Char -- {* drop case certificate for char *}
+
+lemma char_case_code [code]:
+  "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
+  by (cases c)
+    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
+
+lemma [code]:
+  "char_rec = char_case"
   by (simp add: fun_eq_iff split: char.split)
 
-lemma char_rec_nibble_pair [code, code_unfold]:
-  "char_rec f = split f o nibble_pair_of_char"
-  unfolding char_case_nibble_pair [symmetric]
-  by (simp add: fun_eq_iff split: char.split)
+definition char_of_nat :: "nat \<Rightarrow> char" where
+  "char_of_nat n = Enum.enum ! (n mod 256)"
+
+lemma char_of_nat_Char_nibbles:
+  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
+proof -
+  from mod_mult2_eq [of n 16 16]
+  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
+  then show ?thesis
+    by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
+      card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
+qed
+
+lemma char_of_nat_of_char [simp]:
+  "char_of_nat (nat_of_char c) = c"
+  by (cases c)
+    (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
+
+lemma nat_of_char_of_nat [simp]:
+  "nat_of_char (char_of_nat n) = n mod 256"
+proof -
+  have "n mod 256 = n mod (16 * 16)" by simp
+  then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
+  then show ?thesis
+    by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
+qed
+
+lemma inj_nat_of_char:
+  "inj nat_of_char"
+  by (rule inj_on_inverseI) (rule char_of_nat_of_char)
+
+lemma nat_of_char_eq_iff:
+  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
+  by (rule inj_eq) (rule inj_nat_of_char)
+
+lemma nat_of_char_less_256:
+  "nat_of_char c < 256"
+proof (cases c)
+  case (Char x y)
+  with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
+  show ?thesis by (simp add: nat_of_char_def)
+qed
+
+lemma char_of_nat_mod_256:
+  "char_of_nat (n mod 256) = char_of_nat n"
+proof -
+  from nibble_of_nat_mod_16 [of "n mod 256"]
+  have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
+  with nibble_of_nat_mod_16 [of n]
+  have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
+  have "n mod 256 = n mod (16 * 16)" by simp
+  then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
+  show ?thesis
+    by (simp add: char_of_nat_Char_nibbles *)
+     (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
+qed
 
 
 subsection {* Strings as dedicated type *}
@@ -228,8 +381,9 @@
 
 end
 
-lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
-by(simp add: STR_inject)
+lemma STR_inject' [simp]:
+  "STR xs = STR ys \<longleftrightarrow> xs = ys"
+  by (simp add: STR_inject)
 
 
 subsection {* Code generator *}
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Feb 15 11:47:33 2013 +0100
@@ -155,7 +155,7 @@
 fun multi_base_blacklist ctxt ho_atp =
   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
-   "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
+   "weak_case_cong", "nat_of_char_simps", "nibble.simps",
    "nibble.distinct"]
   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
         append ["induct", "inducts"]
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Tools/string_code.ML
--- a/src/HOL/Tools/string_code.ML	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Tools/string_code.ML	Fri Feb 15 11:47:33 2013 +0100
@@ -27,14 +27,14 @@
     | _ => NONE
   end;
    
-fun implode_string char' nibbles' mk_char mk_string ts =
+fun implode_string literals char' nibbles' ts =
   let
     fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
           if c = char' then decode_char nibbles' (t1, t2) else NONE
       | implode_char _ = NONE;
     val ts' = map_filter implode_char ts;
   in if length ts = length ts'
-    then (SOME o Code_Printer.str o mk_string o implode) ts'
+    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
     else NONE
   end;
 
@@ -50,10 +50,9 @@
 
 fun add_literal_list_string target =
   let
-    fun pretty literals (nil' :: cons' :: char' :: nibbles') pr thm vars fxy [(t1, _), (t2, _)] =
+    fun pretty literals (nil' :: cons' :: char' :: nibbles') pr _ vars fxy [(t1, _), (t2, _)] =
       case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
-       of SOME ts => (case implode_string char' nibbles'
-          (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
+       of SOME ts => (case implode_string literals char' nibbles' ts
              of SOME p => p
               | NONE =>
                   Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
@@ -77,8 +76,7 @@
   let
     fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
       case List_Code.implode_list nil' cons' t
-       of SOME ts => (case implode_string char' nibbles'
-          (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
+       of SOME ts => (case implode_string literals char' nibbles' ts
              of SOME p => p
               | NONE => Code_Printer.eqn_error thm "Illegal message expression")
         | NONE => Code_Printer.eqn_error thm "Illegal message expression";
diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Fri Feb 15 11:47:33 2013 +0100
@@ -81,7 +81,7 @@
 fun list_ast_tr' [args] =
       Ast.Appl [Ast.Constant @{syntax_const "_String"},
         syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
-  | list_ast_tr' ts = raise Match;
+  | list_ast_tr' _ = raise Match;
 
 
 (* theory setup *)