incorporated constant chars into instantiation proof for enum;
tuned proofs for properties on enum of chars;
swapped theory dependency of Enum.thy and String.thy

--- a/NEWS	Mon Oct 22 19:02:36 2012 +0200
+++ b/NEWS	Mon Oct 22 22:24:34 2012 +0200
@@ -99,6 +99,9 @@
 
 *** HOL ***
 
+* Removed constant "chars".  Prefer "Enum.enum" on type "char"
+directly.  INCOMPATIBILITY.
+
 * Moved operation product, sublists and n_lists from Enum.thy
 to List.thy.  INCOMPATIBILITY.
 

--- a/src/HOL/Enum.thy	Mon Oct 22 19:02:36 2012 +0200
+++ b/src/HOL/Enum.thy	Mon Oct 22 22:24:34 2012 +0200
@@ -3,7 +3,7 @@
 header {* Finite types as explicit enumerations *}
 
 theory Enum
-imports Map String
+imports Map
 begin
 
 subsection {* Class @{text enum} *}
@@ -37,6 +37,10 @@
   with enum_UNIV show ?thesis by simp
 qed
 
+lemma card_UNIV_length_enum:
+  "card (UNIV :: 'a set) = length enum"
+  by (simp add: UNIV_enum distinct_card enum_distinct)
+
 lemma enum_all [simp]:
   "enum_all = HOL.All"
   by (simp add: fun_eq_iff enum_all_UNIV)
@@ -405,44 +409,6 @@
 
 end
 
-instantiation nibble :: enum
-begin
-
-definition
-  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
-    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
-
-definition
-  "enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
-     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
-
-definition
-  "enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
-     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
-
-instance proof
-qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
-
-end
-
-instantiation char :: enum
-begin
-
-definition
-  "enum = chars"
-
-definition
-  "enum_all P \<longleftrightarrow> list_all P chars"
-
-definition
-  "enum_ex P \<longleftrightarrow> list_ex P chars"
-
-instance proof
-qed (simp_all only: enum_char_def enum_all_char_def enum_ex_char_def UNIV_set_chars distinct_chars,
-  simp_all add: list_all_iff list_ex_iff)
-
-end
-
 instantiation option :: (enum) enum
 begin
 

--- a/src/HOL/IMP/Vars.thy	Mon Oct 22 19:02:36 2012 +0200
+++ b/src/HOL/IMP/Vars.thy	Mon Oct 22 22:24:34 2012 +0200
@@ -16,7 +16,7 @@
 *}
 definition 
   letters :: "string list" where
-  "letters = map (\<lambda>c. [c]) chars"
+  "letters = map (\<lambda>c. [c]) Enum.enum"
 
 definition 
   "show" :: "string set \<Rightarrow> string list" where
@@ -91,3 +91,4 @@
 qed simp_all
 
 end
+

--- a/src/HOL/Quickcheck.thy	Mon Oct 22 19:02:36 2012 +0200
+++ b/src/HOL/Quickcheck.thy	Mon Oct 22 22:24:34 2012 +0200
@@ -52,7 +52,7 @@
 begin
 
 definition
-  "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
+  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
 
 instance ..
 
@@ -281,3 +281,4 @@
   iterate_upto not_randompred Random map
 
 end
+

--- a/src/HOL/String.thy	Mon Oct 22 19:02:36 2012 +0200
+++ b/src/HOL/String.thy	Mon Oct 22 22:24:34 2012 +0200
@@ -3,10 +3,10 @@
 header {* Character and string types *}
 
 theory String
-imports List
+imports List Enum
 begin
 
-subsection {* Characters *}
+subsection {* Characters and strings *}
 
 datatype nibble =
     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
@@ -19,58 +19,42 @@
   fix x show "x \<in> ?A" by (cases x) simp_all
 qed
 
-instance nibble :: finite
-  by default (simp add: UNIV_nibble)
+lemma size_nibble [code, simp]:
+  "size (x::nibble) = 0" by (cases x) simp_all
+
+lemma nibble_size [code, simp]:
+  "nibble_size (x::nibble) = 0" by (cases x) simp_all
+
+instantiation nibble :: enum
+begin
+
+definition
+  "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
+    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
+
+definition
+  "Enum.enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
+     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
+
+definition
+  "Enum.enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
+     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
+
+instance proof
+qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
+
+end
+
+lemma card_UNIV_nibble:
+  "card (UNIV :: nibble set) = 16"
+  by (simp add: card_UNIV_length_enum enum_nibble_def)
 
 datatype char = Char nibble nibble
   -- "Note: canonical order of character encoding coincides with standard term ordering"
 
-lemma UNIV_char:
-  "UNIV = image (split Char) (UNIV \<times> UNIV)"
-proof (rule UNIV_eq_I)
-  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
-qed
-
-instance char :: finite
-  by default (simp add: UNIV_char)
-
-lemma size_char [code, simp]:
-  "size (c::char) = 0" by (cases c) simp
-
-lemma char_size [code, simp]:
-  "char_size (c::char) = 0" by (cases c) simp
-
-primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
-  "nibble_pair_of_char (Char n m) = (n, m)"
-
-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;
-in
-  Global_Theory.note_thmss ""
-    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
-  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
-end
-*}
-
-lemma char_case_nibble_pair [code, code_unfold]:
-  "char_case f = split f o nibble_pair_of_char"
-  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)
-
 syntax
   "_Char" :: "str_position => char"    ("CHR _")
 
-
-subsection {* Strings *}
-
 type_synonym string = "char list"
 
 syntax
@@ -79,8 +63,23 @@
 ML_file "Tools/string_syntax.ML"
 setup String_Syntax.setup
 
-definition chars :: string where
-  "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
+lemma UNIV_char:
+  "UNIV = image (split Char) (UNIV \<times> UNIV)"
+proof (rule UNIV_eq_I)
+  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
+qed
+
+lemma size_char [code, simp]:
+  "size (c::char) = 0" by (cases c) simp
+
+lemma char_size [code, simp]:
+  "char_size (c::char) = 0" by (cases c) simp
+
+instantiation char :: enum
+begin
+
+definition
+  "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
@@ -149,13 +148,55 @@
   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
 
-lemma UNIV_set_chars:
-  "UNIV = set chars"
-  by (simp only: UNIV_char UNIV_nibble) code_simp
+definition
+  "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
+
+definition
+  "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
+
+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)
+  show "distinct (Enum.enum :: char list)"
+    by (auto intro: inj_onI simp add: enum 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"
+    by (simp add: UNIV enum_ex_char_def list_ex_iff)
+qed
+
+end
+
+lemma card_UNIV_char:
+  "card (UNIV :: char set) = 256"
+  by (simp add: card_UNIV_length_enum enum_char_def)
 
-lemma distinct_chars:
-  "distinct chars"
-  by code_simp
+primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
+  "nibble_pair_of_char (Char n m) = (n, m)"
+
+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;
+in
+  Global_Theory.note_thmss ""
+    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
+  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
+end
+*}
+
+lemma char_case_nibble_pair [code, code_unfold]:
+  "char_case f = split f o nibble_pair_of_char"
+  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)
 
 
 subsection {* Strings as dedicated type *}