1.1 --- a/src/HOL/Enum.thy	Sat Dec 24 15:53:08 2011 +0100
     1.2 +++ b/src/HOL/Enum.thy	Sat Dec 24 15:53:08 2011 +0100
     1.3 @@ -458,9 +458,58 @@
     1.4      unfolding enum_ex_option_def enum_ex
     1.5      by (auto, case_tac x) auto
     1.6  qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
     1.7 +end
     1.8 +
     1.9 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where
    1.10 +  "sublists [] = [[]]"
    1.11 +  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
    1.12 +
    1.13 +lemma length_sublists:
    1.14 +  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
    1.15 +  by (induct xs) (simp_all add: Let_def)
    1.16 +
    1.17 +lemma sublists_powset:
    1.18 +  "set ` set (sublists xs) = Pow (set xs)"
    1.19 +proof -
    1.20 +  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
    1.21 +    by (auto simp add: image_def)
    1.22 +  have "set (map set (sublists xs)) = Pow (set xs)"
    1.23 +    by (induct xs)
    1.24 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
    1.25 +  then show ?thesis by simp
    1.26 +qed
    1.27 +
    1.28 +lemma distinct_set_sublists:
    1.29 +  assumes "distinct xs"
    1.30 +  shows "distinct (map set (sublists xs))"
    1.31 +proof (rule card_distinct)
    1.32 +  have "finite (set xs)" by rule
    1.33 +  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
    1.34 +  with assms distinct_card [of xs]
    1.35 +    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
    1.36 +  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
    1.37 +    by (simp add: sublists_powset length_sublists)
    1.38 +qed
    1.39 +
    1.40 +instantiation set :: (enum) enum
    1.41 +begin
    1.42 +
    1.43 +definition
    1.44 +  "enum = map set (sublists enum)"
    1.45 +
    1.46 +definition
    1.47 +  "enum_all P \<longleftrightarrow> (\<forall>A\<in>set enum. P (A::'a set))"
    1.48 +
    1.49 +definition
    1.50 +  "enum_ex P \<longleftrightarrow> (\<exists>A\<in>set enum. P (A::'a set))"
    1.51 +
    1.52 +instance proof
    1.53 +qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists
    1.54 +  enum_distinct enum_UNIV)
    1.55  
    1.56  end
    1.57  
    1.58 +
    1.59  subsection {* Small finite types *}
    1.60  
    1.61  text {* We define small finite types for the use in Quickcheck *}
    1.62 @@ -728,12 +777,6 @@
    1.63  qed
    1.64  
    1.65  
    1.66 -subsection {* Transitive closure on relations over finite types *}
    1.67 -
    1.68 -lemma [code]: "trancl (R :: (('a :: enum) \<times> 'a) set) = ntrancl (length (filter R enum) - 1) R"
    1.69 -  by (simp add: finite_trancl_ntranl distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def)
    1.70 -
    1.71 -
    1.72  subsection {* Closing up *}
    1.73  
    1.74  code_abort enum_the