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