moving UNIV = ... equations to their proper theories

--- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 15:15:58 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 19:48:02 2011 +0200
@@ -564,10 +564,6 @@
   "(\<Sqinter>x\<in>UNIV. f x) = \<Sqinter>range f"
   by (simp add: INFI_def)
 
-lemma UNIV_bool [no_atp]: -- "FIXME move"
-  "UNIV = {False, True}"
-  by auto
-
 lemma (in complete_lattice) INF_bool_eq:
   "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   by (simp add: UNIV_bool INF_empty INF_insert inf_commute)

--- a/src/HOL/Finite_Set.thy	Sun Jul 17 15:15:58 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Jul 17 19:48:02 2011 +0200
@@ -477,20 +477,14 @@
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
-lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
+lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
   by simp
 
 end
 
-lemma UNIV_unit [no_atp]:
-  "UNIV = {()}" by auto
-
 instance unit :: finite proof
 qed (simp add: UNIV_unit)
 
-lemma UNIV_bool [no_atp]:
-  "UNIV = {False, True}" by auto
-
 instance bool :: finite proof
 qed (simp add: UNIV_bool)
 

--- a/src/HOL/Product_Type.thy	Sun Jul 17 15:15:58 2011 +0200
+++ b/src/HOL/Product_Type.thy	Sun Jul 17 19:48:02 2011 +0200
@@ -84,9 +84,12 @@
   f} rather than by @{term [source] "%u. f ()"}.
 *}
 
-lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
+lemma UNIV_unit [no_atp]:
+  "UNIV = {()}" by auto
+
 instantiation unit :: default
 begin
 

--- a/src/HOL/Set.thy	Sun Jul 17 15:15:58 2011 +0200
+++ b/src/HOL/Set.thy	Sun Jul 17 19:48:02 2011 +0200
@@ -1487,6 +1487,9 @@
 lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
   by (auto intro: bool_contrapos)
 
+lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
+  by (auto intro: bool_induct)
+
 text {* \medskip @{text Pow} *}
 
 lemma Pow_empty [simp]: "Pow {} = {{}}"