src/HOL/Enum.thy
changeset 49972 f11f8905d9fd
parent 49950 cd882d53ba6b
child 50567 768a3fbe4149
     1.1 --- a/src/HOL/Enum.thy	Mon Oct 22 19:02:36 2012 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Oct 22 22:24:34 2012 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Finite types as explicit enumerations *}
     1.5  
     1.6  theory Enum
     1.7 -imports Map String
     1.8 +imports Map
     1.9  begin
    1.10  
    1.11  subsection {* Class @{text enum} *}
    1.12 @@ -37,6 +37,10 @@
    1.13    with enum_UNIV show ?thesis by simp
    1.14  qed
    1.15  
    1.16 +lemma card_UNIV_length_enum:
    1.17 +  "card (UNIV :: 'a set) = length enum"
    1.18 +  by (simp add: UNIV_enum distinct_card enum_distinct)
    1.19 +
    1.20  lemma enum_all [simp]:
    1.21    "enum_all = HOL.All"
    1.22    by (simp add: fun_eq_iff enum_all_UNIV)
    1.23 @@ -405,44 +409,6 @@
    1.24  
    1.25  end
    1.26  
    1.27 -instantiation nibble :: enum
    1.28 -begin
    1.29 -
    1.30 -definition
    1.31 -  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    1.32 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
    1.33 -
    1.34 -definition
    1.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
    1.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"
    1.37 -
    1.38 -definition
    1.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
    1.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"
    1.41 -
    1.42 -instance proof
    1.43 -qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
    1.44 -
    1.45 -end
    1.46 -
    1.47 -instantiation char :: enum
    1.48 -begin
    1.49 -
    1.50 -definition
    1.51 -  "enum = chars"
    1.52 -
    1.53 -definition
    1.54 -  "enum_all P \<longleftrightarrow> list_all P chars"
    1.55 -
    1.56 -definition
    1.57 -  "enum_ex P \<longleftrightarrow> list_ex P chars"
    1.58 -
    1.59 -instance proof
    1.60 -qed (simp_all only: enum_char_def enum_all_char_def enum_ex_char_def UNIV_set_chars distinct_chars,
    1.61 -  simp_all add: list_all_iff list_ex_iff)
    1.62 -
    1.63 -end
    1.64 -
    1.65  instantiation option :: (enum) enum
    1.66  begin
    1.67