# HG changeset patch # User haftmann # Date 1310924882 -7200 # Node ID 8a50dc70cbff81818387d8b20cb972bf2ab88768 # Parent db18f4d0cc7dbf2863426b457124f3b55c04714f moving UNIV = ... equations to their proper theories diff -r db18f4d0cc7d -r 8a50dc70cbff src/HOL/Complete_Lattice.thy --- 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 @@ "(\x\UNIV. f x) = \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: "(\b. A b) = A True \ A False" by (simp add: UNIV_bool INF_empty INF_insert inf_commute) diff -r db18f4d0cc7d -r 8a50dc70cbff src/HOL/Finite_Set.thy --- 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 \ 'a set)" by (rule subset_UNIV finite_UNIV finite_subset)+ -lemma finite_code [code]: "finite (A \ 'a set) = True" +lemma finite_code [code]: "finite (A \ 'a set) \ 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) diff -r db18f4d0cc7d -r 8a50dc70cbff src/HOL/Product_Type.thy --- 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 diff -r db18f4d0cc7d -r 8a50dc70cbff src/HOL/Set.thy --- 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: "(\b. P b) \ P True \ 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 {} = {{}}"