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 {} = {{}}"