# HG changeset patch # User haftmann # Date 1206010870 -3600 # Node ID 0f8e23edd357ddc1ba2132ab5f809360ea4e45b3 # Parent 105f552010775255e613fa4f9c39f7c4e3ce359f added theory Library/Enum.thy diff -r 105f55201077 -r 0f8e23edd357 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Mar 20 12:01:09 2008 +0100 +++ b/src/HOL/IsaMakefile Thu Mar 20 12:01:10 2008 +0100 @@ -236,7 +236,7 @@ Library/Abstract_Rat.thy Library/Univ_Poly.thy\ Library/Numeral_Type.thy Library/Boolean_Algebra.thy Library/Countable.thy \ Library/RType.thy Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \ - Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy + Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy Library/Enum.thy @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library diff -r 105f55201077 -r 0f8e23edd357 src/HOL/Library/Enum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Enum.thy Thu Mar 20 12:01:10 2008 +0100 @@ -0,0 +1,173 @@ +(* Title: HOL/Library/Enum.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Finite types as explicit enumerations *} + +theory Enum +imports Main +begin + +subsection {* Class @{text enum} *} + +class enum = finite + -- FIXME + fixes enum :: "'a list" + assumes enum_all: "set enum = UNIV" +begin + +lemma in_enum [intro]: "x \ set enum" + unfolding enum_all by auto + +lemma enum_eq_I: + assumes "\x. x \ set xs" + shows "set enum = set xs" +proof - + from assms UNIV_eq_I have "UNIV = set xs" by auto + with enum_all show ?thesis by simp +qed + +end + + +subsection {* Equality and order on functions *} + +declare eq_fun [code func del] order_fun [code func del] + +instance "fun" :: (enum, eq) eq .. + +lemma eq_fun [code func]: + fixes f g :: "'a\enum \ 'b\eq" + shows "f = g \ (\x \ set enum. f x = g x)" + by (simp add: enum_all expand_fun_eq) + +lemma order_fun [code func]: + fixes f g :: "'a\enum \ 'b\order" + shows "f \ g \ (\x \ set enum. f x \ g x)" + and "f < g \ f \ g \ (\x \ set enum. f x \ g x)" + by (simp_all add: enum_all expand_fun_eq le_fun_def less_fun_def order_less_le) + + +subsection {* Default instances *} + +instantiation unit :: enum +begin + +definition + "enum = [()]" + +instance by default + (simp add: enum_unit_def UNIV_unit) + +end + +instantiation bool :: enum +begin + +definition + "enum = [False, True]" + +instance by default + (simp add: enum_bool_def UNIV_bool) + +end + +primrec product :: "'a list \ 'b list \ ('a \ 'b) list" where + "product [] _ = []" + | "product (x#xs) ys = map (Pair x) ys @ product xs ys" + +lemma product_list_set: + "set (product xs ys) = set xs \ set ys" + by (induct xs) auto + +instantiation * :: (enum, enum) enum +begin + +definition + "enum = product enum enum" + +instance by default + (simp add: enum_prod_def product_list_set enum_all) + +end + +instantiation "+" :: (enum, enum) enum +begin + +definition + "enum = map Inl enum @ map Inr enum" + +instance by default + (auto simp add: enum_all enum_sum_def, case_tac x, auto) + +end + +primrec sublists :: "'a list \ 'a list list" where + "sublists [] = [[]]" + | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" + +lemma sublists_powset: + "set (map set (sublists xs)) = Pow (set xs)" +proof - + have aux: "\x A. set ` Cons x ` A = insert x ` set ` A" + by (auto simp add: image_def) + show ?thesis + by (induct xs) + (simp_all add: aux Let_def Pow_insert Un_commute) +qed + +instantiation set :: (enum) enum +begin + +definition + "enum = map set (sublists enum)" + +instance by default + (simp add: enum_set_def sublists_powset enum_all del: set_map) + +end + +instantiation nibble :: enum +begin + +definition + "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, + Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]" + +instance by default + (simp add: enum_nibble_def UNIV_nibble) + +end + +instantiation char :: enum +begin + +definition + "enum = map (split Char) (product enum enum)" + +instance by default + (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]) + +end + +(*instantiation "fun" :: (enum, enum) enum +begin + + +definition + "enum + +lemma inj_graph: "inj (%f. {(x, y). y = f x})" + by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq) + +instance "fun" :: (finite, finite) finite +proof + show "finite (UNIV :: ('a => 'b) set)" + proof (rule finite_imageD) + let ?graph = "%f::'a => 'b. {(x, y). y = f x}" + show "finite (range ?graph)" by (rule finite) + show "inj ?graph" by (rule inj_graph) + qed +qed*) + +end \ No newline at end of file diff -r 105f55201077 -r 0f8e23edd357 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Thu Mar 20 12:01:09 2008 +0100 +++ b/src/HOL/Library/Library.thy Thu Mar 20 12:01:10 2008 +0100 @@ -18,6 +18,7 @@ Countable Dense_Linear_Order Efficient_Nat + Enum Eval Eval_Witness Executable_Set