incorporated constant chars into instantiation proof for enum;
authorhaftmann
Mon Oct 22 22:24:34 2012 +0200 (2012-10-22)
changeset 49972f11f8905d9fd
parent 49971 8b50286c36d3
child 49973 e84baadd4963
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
NEWS
src/HOL/Enum.thy
src/HOL/IMP/Vars.thy
src/HOL/Quickcheck.thy
src/HOL/String.thy
     1.1 --- a/NEWS	Mon Oct 22 19:02:36 2012 +0200
     1.2 +++ b/NEWS	Mon Oct 22 22:24:34 2012 +0200
     1.3 @@ -99,6 +99,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Removed constant "chars".  Prefer "Enum.enum" on type "char"
     1.8 +directly.  INCOMPATIBILITY.
     1.9 +
    1.10  * Moved operation product, sublists and n_lists from Enum.thy
    1.11  to List.thy.  INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/HOL/Enum.thy	Mon Oct 22 19:02:36 2012 +0200
     2.2 +++ b/src/HOL/Enum.thy	Mon Oct 22 22:24:34 2012 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  header {* Finite types as explicit enumerations *}
     2.5  
     2.6  theory Enum
     2.7 -imports Map String
     2.8 +imports Map
     2.9  begin
    2.10  
    2.11  subsection {* Class @{text enum} *}
    2.12 @@ -37,6 +37,10 @@
    2.13    with enum_UNIV show ?thesis by simp
    2.14  qed
    2.15  
    2.16 +lemma card_UNIV_length_enum:
    2.17 +  "card (UNIV :: 'a set) = length enum"
    2.18 +  by (simp add: UNIV_enum distinct_card enum_distinct)
    2.19 +
    2.20  lemma enum_all [simp]:
    2.21    "enum_all = HOL.All"
    2.22    by (simp add: fun_eq_iff enum_all_UNIV)
    2.23 @@ -405,44 +409,6 @@
    2.24  
    2.25  end
    2.26  
    2.27 -instantiation nibble :: enum
    2.28 -begin
    2.29 -
    2.30 -definition
    2.31 -  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    2.32 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
    2.33 -
    2.34 -definition
    2.35 -  "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
    2.36 -     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
    2.37 -
    2.38 -definition
    2.39 -  "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
    2.40 -     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
    2.41 -
    2.42 -instance proof
    2.43 -qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
    2.44 -
    2.45 -end
    2.46 -
    2.47 -instantiation char :: enum
    2.48 -begin
    2.49 -
    2.50 -definition
    2.51 -  "enum = chars"
    2.52 -
    2.53 -definition
    2.54 -  "enum_all P \<longleftrightarrow> list_all P chars"
    2.55 -
    2.56 -definition
    2.57 -  "enum_ex P \<longleftrightarrow> list_ex P chars"
    2.58 -
    2.59 -instance proof
    2.60 -qed (simp_all only: enum_char_def enum_all_char_def enum_ex_char_def UNIV_set_chars distinct_chars,
    2.61 -  simp_all add: list_all_iff list_ex_iff)
    2.62 -
    2.63 -end
    2.64 -
    2.65  instantiation option :: (enum) enum
    2.66  begin
    2.67  
     3.1 --- a/src/HOL/IMP/Vars.thy	Mon Oct 22 19:02:36 2012 +0200
     3.2 +++ b/src/HOL/IMP/Vars.thy	Mon Oct 22 22:24:34 2012 +0200
     3.3 @@ -16,7 +16,7 @@
     3.4  *}
     3.5  definition 
     3.6    letters :: "string list" where
     3.7 -  "letters = map (\<lambda>c. [c]) chars"
     3.8 +  "letters = map (\<lambda>c. [c]) Enum.enum"
     3.9  
    3.10  definition 
    3.11    "show" :: "string set \<Rightarrow> string list" where
    3.12 @@ -91,3 +91,4 @@
    3.13  qed simp_all
    3.14  
    3.15  end
    3.16 +
     4.1 --- a/src/HOL/Quickcheck.thy	Mon Oct 22 19:02:36 2012 +0200
     4.2 +++ b/src/HOL/Quickcheck.thy	Mon Oct 22 22:24:34 2012 +0200
     4.3 @@ -52,7 +52,7 @@
     4.4  begin
     4.5  
     4.6  definition
     4.7 -  "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
     4.8 +  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
     4.9  
    4.10  instance ..
    4.11  
    4.12 @@ -281,3 +281,4 @@
    4.13    iterate_upto not_randompred Random map
    4.14  
    4.15  end
    4.16 +
     5.1 --- a/src/HOL/String.thy	Mon Oct 22 19:02:36 2012 +0200
     5.2 +++ b/src/HOL/String.thy	Mon Oct 22 22:24:34 2012 +0200
     5.3 @@ -3,10 +3,10 @@
     5.4  header {* Character and string types *}
     5.5  
     5.6  theory String
     5.7 -imports List
     5.8 +imports List Enum
     5.9  begin
    5.10  
    5.11 -subsection {* Characters *}
    5.12 +subsection {* Characters and strings *}
    5.13  
    5.14  datatype nibble =
    5.15      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    5.16 @@ -19,58 +19,42 @@
    5.17    fix x show "x \<in> ?A" by (cases x) simp_all
    5.18  qed
    5.19  
    5.20 -instance nibble :: finite
    5.21 -  by default (simp add: UNIV_nibble)
    5.22 +lemma size_nibble [code, simp]:
    5.23 +  "size (x::nibble) = 0" by (cases x) simp_all
    5.24 +
    5.25 +lemma nibble_size [code, simp]:
    5.26 +  "nibble_size (x::nibble) = 0" by (cases x) simp_all
    5.27 +
    5.28 +instantiation nibble :: enum
    5.29 +begin
    5.30 +
    5.31 +definition
    5.32 +  "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    5.33 +    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
    5.34 +
    5.35 +definition
    5.36 +  "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
    5.37 +     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
    5.38 +
    5.39 +definition
    5.40 +  "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
    5.41 +     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
    5.42 +
    5.43 +instance proof
    5.44 +qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
    5.45 +
    5.46 +end
    5.47 +
    5.48 +lemma card_UNIV_nibble:
    5.49 +  "card (UNIV :: nibble set) = 16"
    5.50 +  by (simp add: card_UNIV_length_enum enum_nibble_def)
    5.51  
    5.52  datatype char = Char nibble nibble
    5.53    -- "Note: canonical order of character encoding coincides with standard term ordering"
    5.54  
    5.55 -lemma UNIV_char:
    5.56 -  "UNIV = image (split Char) (UNIV \<times> UNIV)"
    5.57 -proof (rule UNIV_eq_I)
    5.58 -  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    5.59 -qed
    5.60 -
    5.61 -instance char :: finite
    5.62 -  by default (simp add: UNIV_char)
    5.63 -
    5.64 -lemma size_char [code, simp]:
    5.65 -  "size (c::char) = 0" by (cases c) simp
    5.66 -
    5.67 -lemma char_size [code, simp]:
    5.68 -  "char_size (c::char) = 0" by (cases c) simp
    5.69 -
    5.70 -primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
    5.71 -  "nibble_pair_of_char (Char n m) = (n, m)"
    5.72 -
    5.73 -setup {*
    5.74 -let
    5.75 -  val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
    5.76 -  val thms = map_product
    5.77 -   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    5.78 -      nibbles nibbles;
    5.79 -in
    5.80 -  Global_Theory.note_thmss ""
    5.81 -    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    5.82 -  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    5.83 -end
    5.84 -*}
    5.85 -
    5.86 -lemma char_case_nibble_pair [code, code_unfold]:
    5.87 -  "char_case f = split f o nibble_pair_of_char"
    5.88 -  by (simp add: fun_eq_iff split: char.split)
    5.89 -
    5.90 -lemma char_rec_nibble_pair [code, code_unfold]:
    5.91 -  "char_rec f = split f o nibble_pair_of_char"
    5.92 -  unfolding char_case_nibble_pair [symmetric]
    5.93 -  by (simp add: fun_eq_iff split: char.split)
    5.94 -
    5.95  syntax
    5.96    "_Char" :: "str_position => char"    ("CHR _")
    5.97  
    5.98 -
    5.99 -subsection {* Strings *}
   5.100 -
   5.101  type_synonym string = "char list"
   5.102  
   5.103  syntax
   5.104 @@ -79,8 +63,23 @@
   5.105  ML_file "Tools/string_syntax.ML"
   5.106  setup String_Syntax.setup
   5.107  
   5.108 -definition chars :: string where
   5.109 -  "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   5.110 +lemma UNIV_char:
   5.111 +  "UNIV = image (split Char) (UNIV \<times> UNIV)"
   5.112 +proof (rule UNIV_eq_I)
   5.113 +  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
   5.114 +qed
   5.115 +
   5.116 +lemma size_char [code, simp]:
   5.117 +  "size (c::char) = 0" by (cases c) simp
   5.118 +
   5.119 +lemma char_size [code, simp]:
   5.120 +  "char_size (c::char) = 0" by (cases c) simp
   5.121 +
   5.122 +instantiation char :: enum
   5.123 +begin
   5.124 +
   5.125 +definition
   5.126 +  "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   5.127    Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   5.128    Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
   5.129    Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
   5.130 @@ -149,13 +148,55 @@
   5.131    Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   5.132    Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   5.133  
   5.134 -lemma UNIV_set_chars:
   5.135 -  "UNIV = set chars"
   5.136 -  by (simp only: UNIV_char UNIV_nibble) code_simp
   5.137 +definition
   5.138 +  "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
   5.139 +
   5.140 +definition
   5.141 +  "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
   5.142 +
   5.143 +instance proof
   5.144 +  have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
   5.145 +    by (simp add: enum_char_def enum_nibble_def)
   5.146 +  show UNIV: "UNIV = set (Enum.enum :: char list)"
   5.147 +    by (simp add: enum UNIV_char product_list_set enum_UNIV)
   5.148 +  show "distinct (Enum.enum :: char list)"
   5.149 +    by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct)
   5.150 +  show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
   5.151 +    by (simp add: UNIV enum_all_char_def list_all_iff)
   5.152 +  show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
   5.153 +    by (simp add: UNIV enum_ex_char_def list_ex_iff)
   5.154 +qed
   5.155 +
   5.156 +end
   5.157 +
   5.158 +lemma card_UNIV_char:
   5.159 +  "card (UNIV :: char set) = 256"
   5.160 +  by (simp add: card_UNIV_length_enum enum_char_def)
   5.161  
   5.162 -lemma distinct_chars:
   5.163 -  "distinct chars"
   5.164 -  by code_simp
   5.165 +primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
   5.166 +  "nibble_pair_of_char (Char n m) = (n, m)"
   5.167 +
   5.168 +setup {*
   5.169 +let
   5.170 +  val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
   5.171 +  val thms = map_product
   5.172 +   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
   5.173 +      nibbles nibbles;
   5.174 +in
   5.175 +  Global_Theory.note_thmss ""
   5.176 +    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
   5.177 +  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
   5.178 +end
   5.179 +*}
   5.180 +
   5.181 +lemma char_case_nibble_pair [code, code_unfold]:
   5.182 +  "char_case f = split f o nibble_pair_of_char"
   5.183 +  by (simp add: fun_eq_iff split: char.split)
   5.184 +
   5.185 +lemma char_rec_nibble_pair [code, code_unfold]:
   5.186 +  "char_rec f = split f o nibble_pair_of_char"
   5.187 +  unfolding char_case_nibble_pair [symmetric]
   5.188 +  by (simp add: fun_eq_iff split: char.split)
   5.189  
   5.190  
   5.191  subsection {* Strings as dedicated type *}