# HG changeset patch
# User haftmann
# Date 1350717136 -7200
# Node ID 744934b818c7d190cd4e6dad173af6d4f723712a
# Parent  29cd291bfea6974a61e039c4461a5af496857901
moved quite generic material from theory Enum to more appropriate places

diff -r 29cd291bfea6 -r 744934b818c7 NEWS
--- a/NEWS	Sat Oct 20 09:09:37 2012 +0200
+++ b/NEWS	Sat Oct 20 09:12:16 2012 +0200
@@ -70,6 +70,9 @@
 
 *** HOL ***
 
+* Moved operation product, sublists and n_lists from Enum.thy
+to List.thy.  INCOMPATIBILITY.
+
 * Simplified 'typedef' specifications: historical options for implicit
 set definition and alternative name have been discontinued.  The
 former behavior of "typedef (open) t = A" is now the default, but
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/Codegenerator_Test/RBT_Set_Test.thy
--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -5,7 +5,7 @@
 header {* Test of the code generator using an implementation of sets by RBT trees *}
 
 theory RBT_Set_Test
-imports Library "~~/src/HOL/Library/RBT_Set"
+imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set"
 begin
 
 (* 
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Enum.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -74,61 +74,11 @@
   by (simp add: enum_ex)
 
 lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
-unfolding list_ex1_iff enum_UNIV by auto
+  by (auto simp add: enum_UNIV list_ex1_iff)
 
 
 subsection {* Default instances *}
 
-primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
-  "n_lists 0 xs = [[]]"
-  | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
-
-lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
-  by (induct n) simp_all
-
-lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
-  by (induct n) (auto simp add: length_concat o_def listsum_triv)
-
-lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
-  by (induct n arbitrary: ys) auto
-
-lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
-proof (rule set_eqI)
-  fix ys :: "'a list"
-  show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
-  proof -
-    have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
-      by (induct n arbitrary: ys) auto
-    moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
-      by (induct n arbitrary: ys) auto
-    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
-      by (induct ys) auto
-    ultimately show ?thesis by auto
-  qed
-qed
-
-lemma distinct_n_lists:
-  assumes "distinct xs"
-  shows "distinct (n_lists n xs)"
-proof (rule card_distinct)
-  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
-  have "card (set (n_lists n xs)) = card (set xs) ^ n"
-  proof (induct n)
-    case 0 then show ?case by simp
-  next
-    case (Suc n)
-    moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
-      = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
-      by (rule card_UN_disjoint) auto
-    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
-      by (rule card_image) (simp add: inj_on_def)
-    ultimately show ?case by auto
-  qed
-  also have "\<dots> = length xs ^ n" by (simp add: card_length)
-  finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
-    by (simp add: length_n_lists)
-qed
-
 lemma map_of_zip_enum_is_Some:
   assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
@@ -164,7 +114,7 @@
 definition
   all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
 where
-  "all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)"
+  "all_n_lists P n = (\<forall>xs \<in> set (List.n_lists n enum). P xs)"
 
 lemma [code]:
   "all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
@@ -174,7 +124,7 @@
 definition
   ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
 where
-  "ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)"
+  "ex_n_lists P n = (\<exists>xs \<in> set (List.n_lists n enum). P xs)"
 
 lemma [code]:
   "ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
@@ -186,7 +136,7 @@
 begin
 
 definition
-  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
+  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (List.n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
 
 definition
   "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
@@ -258,7 +208,7 @@
 end
 
 lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
-  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
+  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
   by (simp add: enum_fun_def Let_def)
 
 lemma enum_all_fun_code [code]:
@@ -312,25 +262,11 @@
 
 end
 
-primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> '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 \<times> set ys"
-  by (induct xs) auto
-
-lemma distinct_product:
-  assumes "distinct xs" and "distinct ys"
-  shows "distinct (product xs ys)"
-  using assms by (induct xs)
-    (auto intro: inj_onI simp add: product_list_set distinct_map)
-
 instantiation prod :: (enum, enum) enum
 begin
 
 definition
-  "enum = product enum enum"
+  "enum = List.product enum enum"
 
 definition
   "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
@@ -404,7 +340,7 @@
 begin
 
 definition
-  "enum = map (split Char) (product enum enum)"
+  "enum = map (split Char) (List.product enum enum)"
 
 lemma enum_chars [code]:
   "enum = chars"
@@ -461,37 +397,6 @@
 qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
 end
 
-primrec sublists :: "'a list \<Rightarrow> 'a list list" where
-  "sublists [] = [[]]"
-  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
-
-lemma length_sublists:
-  "length (sublists xs) = 2 ^ length xs"
-  by (induct xs) (simp_all add: Let_def)
-
-lemma sublists_powset:
-  "set ` set (sublists xs) = Pow (set xs)"
-proof -
-  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
-    by (auto simp add: image_def)
-  have "set (map set (sublists xs)) = Pow (set xs)"
-    by (induct xs)
-      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
-  then show ?thesis by simp
-qed
-
-lemma distinct_set_sublists:
-  assumes "distinct xs"
-  shows "distinct (map set (sublists xs))"
-proof (rule card_distinct)
-  have "finite (set xs)" by rule
-  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
-  with assms distinct_card [of xs]
-    have "card (Pow (set xs)) = 2 ^ length xs" by simp
-  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
-    by (simp add: sublists_powset length_sublists)
-qed
-
 instantiation set :: (enum) enum
 begin
 
@@ -745,10 +650,11 @@
 
 hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
 
+
 subsection {* An executable THE operator on finite types *}
 
 definition
-  [code del]: "enum_the P = The P"
+  [code del]: "enum_the = The"
 
 lemma [code]:
   "The P = (case filter P enum of [x] => x | _ => enum_the P)"
@@ -782,9 +688,10 @@
 code_abort enum_the
 code_const enum_the (Eval "(fn p => raise Match)")
 
+
 subsection {* Further operations on finite types *}
 
-lemma Collect_code[code]:
+lemma Collect_code [code]:
   "Collect P = set (filter P enum)"
 by (auto simp add: enum_UNIV)
 
@@ -796,11 +703,11 @@
   "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
 by (simp add: trancl_def)
 
-lemma rtranclp_rtrancl_eq[code, no_atp]:
+lemma rtranclp_rtrancl_eq [code, no_atp]:
   "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
 unfolding rtrancl_def by auto
 
-lemma max_ext_eq[code]:
+lemma max_ext_eq [code]:
   "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
 by (auto simp add: max_ext.simps)
 
@@ -813,157 +720,26 @@
 unfolding mlex_prod_def by auto
 
 subsection {* Executable accessible part *}
-(* FIXME: should be moved somewhere else !? *)
-
-subsubsection {* Finite monotone eventually stable sequences *}
-
-lemma finite_mono_remains_stable_implies_strict_prefix:
-  fixes f :: "nat \<Rightarrow> 'a::order"
-  assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
-  shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
-  using assms
-proof -
-  have "\<exists>n. f n = f (Suc n)"
-  proof (rule ccontr)
-    assume "\<not> ?thesis"
-    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
-    then have "\<And>n. f n < f (Suc n)"
-      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
-    with lift_Suc_mono_less_iff[of f]
-    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
-    then have "inj f"
-      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
-    with `finite (range f)` have "finite (UNIV::nat set)"
-      by (rule finite_imageD)
-    then show False by simp
-  qed
-  then obtain n where n: "f n = f (Suc n)" ..
-  def N \<equiv> "LEAST n. f n = f (Suc n)"
-  have N: "f N = f (Suc N)"
-    unfolding N_def using n by (rule LeastI)
-  show ?thesis
-  proof (intro exI[of _ N] conjI allI impI)
-    fix n assume "N \<le> n"
-    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
-    proof (induct rule: dec_induct)
-      case (step n) then show ?case
-        using eq[rule_format, of "n - 1"] N
-        by (cases n) (auto simp add: le_Suc_eq)
-    qed simp
-    from this[of n] `N \<le> n` show "f N = f n" by auto
-  next
-    fix n m :: nat assume "m < n" "n \<le> N"
-    then show "f m < f n"
-    proof (induct rule: less_Suc_induct[consumes 1])
-      case (1 i)
-      then have "i < N" by simp
-      then have "f i \<noteq> f (Suc i)"
-        unfolding N_def by (rule not_less_Least)
-      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
-    qed auto
-  qed
-qed
-
-lemma finite_mono_strict_prefix_implies_finite_fixpoint:
-  fixes f :: "nat \<Rightarrow> 'a set"
-  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
-    and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
-  shows "f (card S) = (\<Union>n. f n)"
-proof -
-  from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
-
-  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
-    proof (induct i)
-      case 0 then show ?case by simp
-    next
-      case (Suc i)
-      with inj[rule_format, of "Suc i" i]
-      have "(f i) \<subset> (f (Suc i))" by auto
-      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
-      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
-      with Suc show ?case using inj by auto
-    qed
-  }
-  then have "N \<le> card (f N)" by simp
-  also have "\<dots> \<le> card S" using S by (intro card_mono)
-  finally have "f (card S) = f N" using eq by auto
-  then show ?thesis using eq inj[rule_format, of N]
-    apply auto
-    apply (case_tac "n < N")
-    apply (auto simp: not_less)
-    done
-qed
-
-subsubsection {* Bounded accessible part *}
-
-fun bacc :: "('a * 'a) set => nat => 'a set" 
-where
-  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
-| "bacc r (Suc n) = (bacc r n Un {x. \<forall> y. (y, x) : r --> y : bacc r n})"
-
-lemma bacc_subseteq_acc:
-  "bacc r n \<subseteq> acc r"
-by (induct n) (auto intro: acc.intros)
-
-lemma bacc_mono:
-  "n <= m ==> bacc r n \<subseteq> bacc r m"
-by (induct rule: dec_induct) auto
-  
-lemma bacc_upper_bound:
-  "bacc (r :: ('a * 'a) set)  (card (UNIV :: ('a :: enum) set)) = (UN n. bacc r n)"
-proof -
-  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
-  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
-  moreover have "finite (range (bacc r))" by auto
-  ultimately show ?thesis
-   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
-     (auto intro: finite_mono_remains_stable_implies_strict_prefix  simp add: enum_UNIV)
-qed
-
-lemma acc_subseteq_bacc:
-  assumes "finite r"
-  shows "acc r \<subseteq> (UN n. bacc r n)"
-proof
-  fix x
-  assume "x : acc r"
-  then have "\<exists> n. x : bacc r n"
-  proof (induct x arbitrary: rule: acc.induct)
-    case (accI x)
-    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
-    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
-    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
-    proof
-      fix y assume y: "(y, x) : r"
-      with n have "y : bacc r (n y)" by auto
-      moreover have "n y <= Max ((%(y, x). n y) ` r)"
-        using y `finite r` by (auto intro!: Max_ge)
-      note bacc_mono[OF this, of r]
-      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
-    qed
-    then show ?case
-      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
-  qed
-  then show "x : (UN n. bacc r n)" by auto
-qed
-
-lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
-by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound finite_set order_eq_iff)
 
 definition 
   [code del]: "card_UNIV = card UNIV"
 
 lemma [code]:
   "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
-unfolding card_UNIV_def enum_UNIV ..
+  unfolding card_UNIV_def enum_UNIV ..
 
-declare acc_bacc_eq[folded card_UNIV_def, code]
+lemma [code]:
+  fixes xs :: "('a::finite \<times> 'a) list"
+  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
+  by (simp add: card_UNIV_def acc_bacc_eq)
 
-lemma [code_unfold]: "accp r = (%x. x : acc {(x, y). r x y})"
-unfolding acc_def by simp
+lemma [code_unfold]: "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
+  unfolding acc_def by simp
 
 subsection {* Closing up *}
 
 hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
-hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
+hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl
 
 end
+
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -6,7 +6,7 @@
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
 theory Hilbert_Choice
-imports Nat Wellfounded Plain
+imports Nat Wellfounded Big_Operators
 keywords "specification" "ax_specification" :: thy_goal
 begin
 
@@ -643,6 +643,144 @@
   done
 
 
+subsection {* An aside: bounded accessible part *}
+
+text {* Finite monotone eventually stable sequences *}
+
+lemma finite_mono_remains_stable_implies_strict_prefix:
+  fixes f :: "nat \<Rightarrow> 'a::order"
+  assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
+  shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
+  using assms
+proof -
+  have "\<exists>n. f n = f (Suc n)"
+  proof (rule ccontr)
+    assume "\<not> ?thesis"
+    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
+    then have "\<And>n. f n < f (Suc n)"
+      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
+    with lift_Suc_mono_less_iff[of f]
+    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
+    then have "inj f"
+      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
+    with `finite (range f)` have "finite (UNIV::nat set)"
+      by (rule finite_imageD)
+    then show False by simp
+  qed
+  then obtain n where n: "f n = f (Suc n)" ..
+  def N \<equiv> "LEAST n. f n = f (Suc n)"
+  have N: "f N = f (Suc N)"
+    unfolding N_def using n by (rule LeastI)
+  show ?thesis
+  proof (intro exI[of _ N] conjI allI impI)
+    fix n assume "N \<le> n"
+    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
+    proof (induct rule: dec_induct)
+      case (step n) then show ?case
+        using eq[rule_format, of "n - 1"] N
+        by (cases n) (auto simp add: le_Suc_eq)
+    qed simp
+    from this[of n] `N \<le> n` show "f N = f n" by auto
+  next
+    fix n m :: nat assume "m < n" "n \<le> N"
+    then show "f m < f n"
+    proof (induct rule: less_Suc_induct[consumes 1])
+      case (1 i)
+      then have "i < N" by simp
+      then have "f i \<noteq> f (Suc i)"
+        unfolding N_def by (rule not_less_Least)
+      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
+    qed auto
+  qed
+qed
+
+lemma finite_mono_strict_prefix_implies_finite_fixpoint:
+  fixes f :: "nat \<Rightarrow> 'a set"
+  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
+    and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
+  shows "f (card S) = (\<Union>n. f n)"
+proof -
+  from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
+
+  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
+    proof (induct i)
+      case 0 then show ?case by simp
+    next
+      case (Suc i)
+      with inj[rule_format, of "Suc i" i]
+      have "(f i) \<subset> (f (Suc i))" by auto
+      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
+      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
+      with Suc show ?case using inj by auto
+    qed
+  }
+  then have "N \<le> card (f N)" by simp
+  also have "\<dots> \<le> card S" using S by (intro card_mono)
+  finally have "f (card S) = f N" using eq by auto
+  then show ?thesis using eq inj[rule_format, of N]
+    apply auto
+    apply (case_tac "n < N")
+    apply (auto simp: not_less)
+    done
+qed
+
+primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set" 
+where
+  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
+| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
+
+lemma bacc_subseteq_acc:
+  "bacc r n \<subseteq> acc r"
+  by (induct n) (auto intro: acc.intros)
+
+lemma bacc_mono:
+  "n \<le> m \<Longrightarrow> bacc r n \<subseteq> bacc r m"
+  by (induct rule: dec_induct) auto
+  
+lemma bacc_upper_bound:
+  "bacc (r :: ('a \<times> 'a) set)  (card (UNIV :: 'a::finite set)) = (\<Union>n. bacc r n)"
+proof -
+  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
+  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
+  moreover have "finite (range (bacc r))" by auto
+  ultimately show ?thesis
+   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
+     (auto intro: finite_mono_remains_stable_implies_strict_prefix)
+qed
+
+lemma acc_subseteq_bacc:
+  assumes "finite r"
+  shows "acc r \<subseteq> (\<Union>n. bacc r n)"
+proof
+  fix x
+  assume "x : acc r"
+  then have "\<exists> n. x : bacc r n"
+  proof (induct x arbitrary: rule: acc.induct)
+    case (accI x)
+    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
+    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
+    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
+    proof
+      fix y assume y: "(y, x) : r"
+      with n have "y : bacc r (n y)" by auto
+      moreover have "n y <= Max ((%(y, x). n y) ` r)"
+        using y `finite r` by (auto intro!: Max_ge)
+      note bacc_mono[OF this, of r]
+      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
+    qed
+    then show ?case
+      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
+  qed
+  then show "x : (UN n. bacc r n)" by auto
+qed
+
+lemma acc_bacc_eq:
+  fixes A :: "('a :: finite \<times> 'a) set"
+  assumes "finite A"
+  shows "acc A = bacc A (card (UNIV :: 'a set))"
+  using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
+
+
 subsection {* Specification package -- Hilbertized version *}
 
 lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
@@ -651,3 +789,4 @@
 ML_file "Tools/choice_specification.ML"
 
 end
+
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -92,7 +92,7 @@
       unfolding bs[symmetric] distinct_card[OF distb] ..
     have ca: "CARD('a) = length as"
       unfolding as[symmetric] distinct_card[OF dista] ..
-    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
+    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)"
     have "UNIV = set ?xs"
     proof(rule UNIV_eq_I)
       fix f :: "'a \<Rightarrow> 'b"
@@ -103,8 +103,8 @@
     moreover have "distinct ?xs" unfolding distinct_map
     proof(intro conjI distinct_n_lists distb inj_onI)
       fix xs ys :: "'b list"
-      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
-        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
+      assume xs: "xs \<in> set (List.n_lists (length as) bs)"
+        and ys: "ys \<in> set (List.n_lists (length as) bs)"
         and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
       from xs ys have [simp]: "length xs = length as" "length ys = length as"
         by(simp_all add: length_n_lists_elem)
@@ -472,3 +472,4 @@
 hide_const (open) card' finite' subset' eq_set
 
 end
+
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -63,6 +63,11 @@
 lemma [code, code del]:
   "Bex = Bex" ..
 
+term can_select
+
+lemma [code, code del]:
+  "can_select = can_select" ..
+
 lemma [code, code del]:
   "Set.union = Set.union" ..
 
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/List.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -160,6 +160,13 @@
   -- {*Warning: simpset does not contain this definition, but separate
        theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
 
+primrec
+  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
+    "product [] _ = []"
+  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
+
+hide_const (open) product
+
 primrec 
   upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
     upt_0: "[i..<0] = []"
@@ -228,6 +235,18 @@
   sublist :: "'a list => nat set => 'a list" where
   "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
 
+primrec
+  sublists :: "'a list \<Rightarrow> 'a list list" where
+  "sublists [] = [[]]"
+| "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
+
+primrec
+  n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+  "n_lists 0 xs = [[]]"
+| "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
+
+hide_const (open) n_lists
+
 fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "splice [] ys = ys" |
 "splice xs [] = xs" |
@@ -253,6 +272,7 @@
 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
+@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
@@ -272,6 +292,8 @@
 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
+@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
+@{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c, b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\
 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
@@ -490,6 +512,7 @@
 
 hide_const (open) coset
 
+
 subsubsection {* @{const Nil} and @{const Cons} *}
 
 lemma not_Cons_self [simp]:
@@ -527,6 +550,7 @@
 lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
   by (auto intro!: inj_onI)
 
+
 subsubsection {* @{const length} *}
 
 text {*
@@ -788,7 +812,7 @@
 *}
 
 
-subsubsection {* @{text map} *}
+subsubsection {* @{const map} *}
 
 lemma hd_map:
   "xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)"
@@ -917,9 +941,10 @@
 enriched_type map: map
 by (simp_all add: id_def)
 
-declare map.id[simp]
-
-subsubsection {* @{text rev} *}
+declare map.id [simp]
+
+
+subsubsection {* @{const rev} *}
 
 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
 by (induct xs) auto
@@ -966,7 +991,7 @@
 by(rule rev_cases[of xs]) auto
 
 
-subsubsection {* @{text set} *}
+subsubsection {* @{const set} *}
 
 declare set.simps [code_post]  --"pretty output"
 
@@ -1128,7 +1153,7 @@
   by (induct xs) auto
 
 
-subsubsection {* @{text filter} *}
+subsubsection {* @{const filter} *}
 
 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
 by (induct xs) auto
@@ -1310,7 +1335,7 @@
 declare partition.simps[simp del]
 
 
-subsubsection {* @{text concat} *}
+subsubsection {* @{const concat} *}
 
 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
 by (induct xs) auto
@@ -1346,7 +1371,7 @@
 by (simp add: concat_eq_concat_iff)
 
 
-subsubsection {* @{text nth} *}
+subsubsection {* @{const nth} *}
 
 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
 by auto
@@ -1458,7 +1483,7 @@
 qed
 
 
-subsubsection {* @{text list_update} *}
+subsubsection {* @{const list_update} *}
 
 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
 by (induct xs arbitrary: i) (auto split: nat.split)
@@ -1548,7 +1573,7 @@
   by simp_all
 
 
-subsubsection {* @{text last} and @{text butlast} *}
+subsubsection {* @{const last} and @{const butlast} *}
 
 lemma last_snoc [simp]: "last (xs @ [x]) = x"
 by (induct xs) auto
@@ -1650,7 +1675,7 @@
 by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)
 
 
-subsubsection {* @{text take} and @{text drop} *}
+subsubsection {* @{const take} and @{const drop} *}
 
 lemma take_0 [simp]: "take 0 xs = []"
 by (induct xs) auto
@@ -1904,7 +1929,7 @@
 done
 
 
-subsubsection {* @{text takeWhile} and @{text dropWhile} *}
+subsubsection {* @{const takeWhile} and @{const dropWhile} *}
 
 lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
   by (induct xs) auto
@@ -2068,7 +2093,7 @@
 by (induct k arbitrary: l, simp_all)
 
 
-subsubsection {* @{text zip} *}
+subsubsection {* @{const zip} *}
 
 lemma zip_Nil [simp]: "zip [] ys = []"
 by (induct ys) auto
@@ -2230,7 +2255,7 @@
   by (auto simp add: zip_map_fst_snd)
 
 
-subsubsection {* @{text list_all2} *}
+subsubsection {* @{const list_all2} *}
 
 lemma list_all2_lengthD [intro?]: 
   "list_all2 P xs ys ==> length xs = length ys"
@@ -2387,6 +2412,13 @@
 by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
 
 
+subsubsection {* @{const List.product} *}
+
+lemma product_list_set:
+  "set (List.product xs ys) = set xs \<times> set ys"
+  by (induct xs) auto
+
+
 subsubsection {* @{const fold} with natural argument order *}
 
 lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *}
@@ -2613,6 +2645,7 @@
 
 declare SUP_set_fold [code]
 
+
 subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
 
 text {* Correspondence *}
@@ -2667,7 +2700,7 @@
   by (simp add: fold_append_concat_rev foldr_conv_fold)
 
 
-subsubsection {* @{text upt} *}
+subsubsection {* @{const upt} *}
 
 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
 -- {* simp does not terminate! *}
@@ -2830,7 +2863,7 @@
 qed
 
 
-subsubsection {* @{text "distinct"} and @{text remdups} *}
+subsubsection {* @{const distinct} and @{const remdups} *}
 
 lemma distinct_tl:
   "distinct xs \<Longrightarrow> distinct (tl xs)"
@@ -2885,7 +2918,6 @@
   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
 by (induct xs) auto
 
-
 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
 by (induct xs) auto
 
@@ -3020,6 +3052,12 @@
   qed
 qed (auto simp: dec_def)
 
+lemma distinct_product:
+  assumes "distinct xs" and "distinct ys"
+  shows "distinct (List.product xs ys)"
+  using assms by (induct xs)
+    (auto intro: inj_onI simp add: product_list_set distinct_map)
+
 lemma length_remdups_concat:
   "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
   by (simp add: distinct_card [symmetric])
@@ -3083,6 +3121,7 @@
 "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
 by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
 
+
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
 lemma (in monoid_add) listsum_simps [simp]:
@@ -3342,7 +3381,7 @@
   using assms by (induct xs) simp_all
 
 
-subsubsection {* @{text removeAll} *}
+subsubsection {* @{const removeAll} *}
 
 lemma removeAll_filter_not_eq:
   "removeAll x = filter (\<lambda>y. x \<noteq> y)"
@@ -3388,7 +3427,7 @@
 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
 
 
-subsubsection {* @{text replicate} *}
+subsubsection {* @{const replicate} *}
 
 lemma length_replicate [simp]: "length (replicate n x) = n"
 by (induct n) auto
@@ -3578,7 +3617,7 @@
 qed
 
 
-subsubsection{*@{text rotate1} and @{text rotate}*}
+subsubsection {* @{const rotate1} and @{const rotate} *}
 
 lemma rotate0[simp]: "rotate 0 = id"
 by(simp add:rotate_def)
@@ -3672,7 +3711,7 @@
 using mod_less_divisor[of "length xs" n] by arith
 
 
-subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
+subsubsection {* @{const sublist} --- a generalization of @{const nth} to sets *}
 
 lemma sublist_empty [simp]: "sublist xs {} = []"
 by (auto simp add: sublist_def)
@@ -3755,6 +3794,82 @@
 qed
 
 
+subsubsection {* @{const sublists} and @{const List.n_lists} *}
+
+lemma length_sublists:
+  "length (sublists xs) = 2 ^ length xs"
+  by (induct xs) (simp_all add: Let_def)
+
+lemma sublists_powset:
+  "set ` set (sublists xs) = Pow (set xs)"
+proof -
+  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
+    by (auto simp add: image_def)
+  have "set (map set (sublists xs)) = Pow (set xs)"
+    by (induct xs)
+      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
+  then show ?thesis by simp
+qed
+
+lemma distinct_set_sublists:
+  assumes "distinct xs"
+  shows "distinct (map set (sublists xs))"
+proof (rule card_distinct)
+  have "finite (set xs)" by rule
+  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
+  with assms distinct_card [of xs]
+    have "card (Pow (set xs)) = 2 ^ length xs" by simp
+  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
+    by (simp add: sublists_powset length_sublists)
+qed
+
+lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
+  by (induct n) simp_all
+
+lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
+  by (induct n) (auto simp add: length_concat o_def listsum_triv)
+
+lemma length_n_lists_elem: "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
+  by (induct n arbitrary: ys) auto
+
+lemma set_n_lists: "set (List.n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+proof (rule set_eqI)
+  fix ys :: "'a list"
+  show "ys \<in> set (List.n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+  proof -
+    have "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
+      by (induct n arbitrary: ys) auto
+    moreover have "\<And>x. ys \<in> set (List.n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
+      by (induct n arbitrary: ys) auto
+    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (List.n_lists (length ys) xs)"
+      by (induct ys) auto
+    ultimately show ?thesis by auto
+  qed
+qed
+
+lemma distinct_n_lists:
+  assumes "distinct xs"
+  shows "distinct (List.n_lists n xs)"
+proof (rule card_distinct)
+  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
+  have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
+  proof (induct n)
+    case 0 then show ?case by simp
+  next
+    case (Suc n)
+    moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
+      = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
+      by (rule card_UN_disjoint) auto
+    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
+      by (rule card_image) (simp add: inj_on_def)
+    ultimately show ?case by auto
+  qed
+  also have "\<dots> = length xs ^ n" by (simp add: card_length)
+  finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
+    by (simp add: length_n_lists)
+qed
+
+
 subsubsection {* @{const splice} *}
 
 lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
@@ -5319,6 +5434,15 @@
   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
 by (simp add: list_ex_iff)
 
+definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+where
+  [code_abbrev]: "can_select P A = (\<exists>!x\<in>A. P x)"
+
+lemma can_select_set_list_ex1 [code]:
+  "can_select P (set A) = list_ex1 P A"
+  by (simp add: list_ex1_iff can_select_def)
+
+
 text {* Executable checks for relations on sets *}
 
 definition listrel1p :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
@@ -5531,6 +5655,7 @@
 
 hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length
 
+
 subsubsection {* Pretty lists *}
 
 ML_file "Tools/list_code.ML"
@@ -5698,6 +5823,7 @@
 
 hide_const (open) map_project
 
+
 text {* Operations on relations *}
 
 lemma product_code [code]:
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -234,7 +234,7 @@
   "enum_term_of_fun = (%_ _. let
     enum_term_of_a = enum_term_of (TYPE('a));
     mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
-  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
+  in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
  
 instance ..
 
@@ -308,7 +308,7 @@
 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
 where
   "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
-     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
+     (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
 
 instance ..
 
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/String.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -149,6 +149,14 @@
   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
 
+lemma UNIV_set_chars:
+  "UNIV = set chars"
+  by (simp only: UNIV_char UNIV_nibble) code_simp
+
+lemma distinct_chars:
+  "distinct chars"
+  by code_simp
+
 
 subsection {* Strings as dedicated type *}
 
@@ -213,3 +221,4 @@
 hide_type (open) literal
 
 end
+
diff -r 29cd291bfea6 -r 744934b818c7 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Sum_Type.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -209,8 +209,19 @@
   show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
 qed
 
+lemma UNIV_sum:
+  "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
+proof -
+  { fix x :: "'a + 'b"
+    assume "x \<notin> range Inr"
+    then have "x \<in> range Inl"
+    by (cases x) simp_all
+  } then show ?thesis by auto
+qed
+
 hide_const (open) Suml Sumr Projl Projr
 
 hide_const (open) sum
 
 end
+