1.1 --- a/src/HOL/IsaMakefile	Thu Mar 20 12:01:09 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 20 12:01:10 2008 +0100
     1.3 @@ -236,7 +236,7 @@
     1.4    Library/Abstract_Rat.thy Library/Univ_Poly.thy\
     1.5    Library/Numeral_Type.thy Library/Boolean_Algebra.thy Library/Countable.thy \
     1.6    Library/RType.thy Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \
     1.7 -  Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy
     1.8 +  Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy Library/Enum.thy
     1.9  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    1.10  
    1.11  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Enum.thy	Thu Mar 20 12:01:10 2008 +0100
     2.3 @@ -0,0 +1,173 @@
     2.4 +(*  Title:      HOL/Library/Enum.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Florian Haftmann, TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header {* Finite types as explicit enumerations *}
    2.10 +
    2.11 +theory Enum
    2.12 +imports Main
    2.13 +begin
    2.14 +
    2.15 +subsection {* Class @{text enum} *}
    2.16 +
    2.17 +class enum = finite + -- FIXME
    2.18 +  fixes enum :: "'a list"
    2.19 +  assumes enum_all: "set enum = UNIV"
    2.20 +begin
    2.21 +
    2.22 +lemma in_enum [intro]: "x \<in> set enum"
    2.23 +  unfolding enum_all by auto
    2.24 +
    2.25 +lemma enum_eq_I:
    2.26 +  assumes "\<And>x. x \<in> set xs"
    2.27 +  shows "set enum = set xs"
    2.28 +proof -
    2.29 +  from assms UNIV_eq_I have "UNIV = set xs" by auto
    2.30 +  with enum_all show ?thesis by simp
    2.31 +qed
    2.32 +
    2.33 +end
    2.34 +
    2.35 +
    2.36 +subsection {* Equality and order on functions *}
    2.37 +
    2.38 +declare eq_fun [code func del] order_fun [code func del]
    2.39 +
    2.40 +instance "fun" :: (enum, eq) eq ..
    2.41 +
    2.42 +lemma eq_fun [code func]:
    2.43 +  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>eq"
    2.44 +  shows "f = g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
    2.45 +  by (simp add: enum_all expand_fun_eq)
    2.46 +
    2.47 +lemma order_fun [code func]:
    2.48 +  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    2.49 +  shows "f \<le> g \<longleftrightarrow> (\<forall>x \<in> set enum. f x \<le> g x)"
    2.50 +    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x \<in> set enum. f x \<noteq> g x)"
    2.51 +  by (simp_all add: enum_all expand_fun_eq le_fun_def less_fun_def order_less_le)
    2.52 +
    2.53 +
    2.54 +subsection {* Default instances *}
    2.55 +
    2.56 +instantiation unit :: enum
    2.57 +begin
    2.58 +
    2.59 +definition
    2.60 +  "enum = [()]"
    2.61 +
    2.62 +instance by default
    2.63 +  (simp add: enum_unit_def UNIV_unit)
    2.64 +
    2.65 +end
    2.66 +
    2.67 +instantiation bool :: enum
    2.68 +begin
    2.69 +
    2.70 +definition
    2.71 +  "enum = [False, True]"
    2.72 +
    2.73 +instance by default
    2.74 +  (simp add: enum_bool_def UNIV_bool)
    2.75 +
    2.76 +end
    2.77 +
    2.78 +primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
    2.79 +  "product [] _ = []"
    2.80 +  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
    2.81 +
    2.82 +lemma product_list_set:
    2.83 +  "set (product xs ys) = set xs \<times> set ys"
    2.84 +  by (induct xs) auto
    2.85 +
    2.86 +instantiation * :: (enum, enum) enum
    2.87 +begin
    2.88 +
    2.89 +definition
    2.90 +  "enum = product enum enum"
    2.91 +
    2.92 +instance by default
    2.93 +  (simp add: enum_prod_def product_list_set enum_all)
    2.94 +
    2.95 +end
    2.96 +
    2.97 +instantiation "+" :: (enum, enum) enum
    2.98 +begin
    2.99 +
   2.100 +definition
   2.101 +  "enum = map Inl enum @ map Inr enum"
   2.102 +
   2.103 +instance by default
   2.104 +  (auto simp add: enum_all enum_sum_def, case_tac x, auto)
   2.105 +
   2.106 +end
   2.107 +
   2.108 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   2.109 +  "sublists [] = [[]]"
   2.110 +  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   2.111 +
   2.112 +lemma sublists_powset:
   2.113 +  "set (map set (sublists xs)) = Pow (set xs)"
   2.114 +proof -
   2.115 +  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   2.116 +    by (auto simp add: image_def)
   2.117 +  show ?thesis
   2.118 +    by (induct xs)
   2.119 +     (simp_all add: aux Let_def Pow_insert Un_commute)
   2.120 +qed
   2.121 +
   2.122 +instantiation set :: (enum) enum
   2.123 +begin
   2.124 +
   2.125 +definition
   2.126 +  "enum = map set (sublists enum)"
   2.127 +
   2.128 +instance by default
   2.129 +  (simp add: enum_set_def sublists_powset enum_all del: set_map)
   2.130 +
   2.131 +end
   2.132 +
   2.133 +instantiation nibble :: enum
   2.134 +begin
   2.135 +
   2.136 +definition
   2.137 +  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
   2.138 +    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
   2.139 +
   2.140 +instance by default
   2.141 +  (simp add: enum_nibble_def UNIV_nibble)
   2.142 +
   2.143 +end
   2.144 +
   2.145 +instantiation char :: enum
   2.146 +begin
   2.147 +
   2.148 +definition
   2.149 +  "enum = map (split Char) (product enum enum)"
   2.150 +
   2.151 +instance by default
   2.152 +  (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric])
   2.153 +
   2.154 +end
   2.155 +
   2.156 +(*instantiation "fun" :: (enum, enum) enum
   2.157 +begin
   2.158 +
   2.159 +
   2.160 +definition
   2.161 +  "enum 
   2.162 +
   2.163 +lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   2.164 +  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   2.165 +
   2.166 +instance "fun" :: (finite, finite) finite
   2.167 +proof
   2.168 +  show "finite (UNIV :: ('a => 'b) set)"
   2.169 +  proof (rule finite_imageD)
   2.170 +    let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
   2.171 +    show "finite (range ?graph)" by (rule finite)
   2.172 +    show "inj ?graph" by (rule inj_graph)
   2.173 +  qed
   2.174 +qed*)
   2.175 +
   2.176 +end
   2.177 \ No newline at end of file

     3.1 --- a/src/HOL/Library/Library.thy	Thu Mar 20 12:01:09 2008 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Thu Mar 20 12:01:10 2008 +0100
     3.3 @@ -18,6 +18,7 @@
     3.4    Countable
     3.5    Dense_Linear_Order
     3.6    Efficient_Nat
     3.7 +  Enum
     3.8    Eval
     3.9    Eval_Witness
    3.10    Executable_Set