1.1 --- a/src/HOL/Set.thy	Mon Oct 03 22:21:19 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Sun Oct 09 08:30:48 2011 +0200
     1.3 @@ -483,8 +483,8 @@
     1.4  lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
     1.5    by blast
     1.6  
     1.7 -lemma subset_refl [simp]: "A \<subseteq> A"
     1.8 -  by (fact order_refl)
     1.9 +lemma subset_refl: "A \<subseteq> A"
    1.10 +  by (fact order_refl) (* already [iff] *)
    1.11  
    1.12  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
    1.13    by (fact order_trans)
    1.14 @@ -586,8 +586,8 @@
    1.15  lemma UNIV_witness [intro?]: "EX x. x : UNIV"
    1.16    by simp
    1.17  
    1.18 -lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
    1.19 -  by (rule subsetI) (rule UNIV_I)
    1.20 +lemma subset_UNIV: "A \<subseteq> UNIV"
    1.21 +  by (fact top_greatest) (* already simp *)
    1.22  
    1.23  text {*
    1.24    \medskip Eta-contracting these two rules (to remove @{text P})
    1.25 @@ -1074,10 +1074,10 @@
    1.26    by auto
    1.27  
    1.28  lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
    1.29 -  by blast
    1.30 +  by (fact bot_unique)
    1.31  
    1.32  lemma not_psubset_empty [iff]: "\<not> (A < {})"
    1.33 -  by (unfold less_le) blast
    1.34 +  by (fact not_less_bot) (* FIXME: already simp *)
    1.35  
    1.36  lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
    1.37  by blast
    1.38 @@ -1204,8 +1204,8 @@
    1.39  
    1.40  text {* \medskip @{text Int} *}
    1.41  
    1.42 -lemma Int_absorb [simp]: "A \<inter> A = A"
    1.43 -  by (fact inf_idem)
    1.44 +lemma Int_absorb: "A \<inter> A = A"
    1.45 +  by (fact inf_idem) (* already simp *)
    1.46  
    1.47  lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
    1.48    by (fact inf_left_idem)
    1.49 @@ -1228,11 +1228,11 @@
    1.50  lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
    1.51    by (fact inf_absorb1)
    1.52  
    1.53 -lemma Int_empty_left [simp]: "{} \<inter> B = {}"
    1.54 -  by (fact inf_bot_left)
    1.55 +lemma Int_empty_left: "{} \<inter> B = {}"
    1.56 +  by (fact inf_bot_left) (* already simp *)
    1.57  
    1.58 -lemma Int_empty_right [simp]: "A \<inter> {} = {}"
    1.59 -  by (fact inf_bot_right)
    1.60 +lemma Int_empty_right: "A \<inter> {} = {}"
    1.61 +  by (fact inf_bot_right) (* already simp *)
    1.62  
    1.63  lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
    1.64    by blast
    1.65 @@ -1240,11 +1240,11 @@
    1.66  lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
    1.67    by blast
    1.68  
    1.69 -lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
    1.70 -  by (fact inf_top_left)
    1.71 +lemma Int_UNIV_left: "UNIV \<inter> B = B"
    1.72 +  by (fact inf_top_left) (* already simp *)
    1.73  
    1.74 -lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
    1.75 -  by (fact inf_top_right)
    1.76 +lemma Int_UNIV_right: "A \<inter> UNIV = A"
    1.77 +  by (fact inf_top_right) (* already simp *)
    1.78  
    1.79  lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
    1.80    by (fact inf_sup_distrib1)
    1.81 @@ -1253,7 +1253,7 @@
    1.82    by (fact inf_sup_distrib2)
    1.83  
    1.84  lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
    1.85 -  by (fact inf_eq_top_iff)
    1.86 +  by (fact inf_eq_top_iff) (* already simp *)
    1.87  
    1.88  lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
    1.89    by (fact le_inf_iff)
    1.90 @@ -1264,8 +1264,8 @@
    1.91  
    1.92  text {* \medskip @{text Un}. *}
    1.93  
    1.94 -lemma Un_absorb [simp]: "A \<union> A = A"
    1.95 -  by (fact sup_idem)
    1.96 +lemma Un_absorb: "A \<union> A = A"
    1.97 +  by (fact sup_idem) (* already simp *)
    1.98  
    1.99  lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
   1.100    by (fact sup_left_idem)
   1.101 @@ -1288,17 +1288,17 @@
   1.102  lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
   1.103    by (fact sup_absorb1)
   1.104  
   1.105 -lemma Un_empty_left [simp]: "{} \<union> B = B"
   1.106 -  by (fact sup_bot_left)
   1.107 +lemma Un_empty_left: "{} \<union> B = B"
   1.108 +  by (fact sup_bot_left) (* already simp *)
   1.109  
   1.110 -lemma Un_empty_right [simp]: "A \<union> {} = A"
   1.111 -  by (fact sup_bot_right)
   1.112 +lemma Un_empty_right: "A \<union> {} = A"
   1.113 +  by (fact sup_bot_right) (* already simp *)
   1.114  
   1.115 -lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
   1.116 -  by (fact sup_top_left)
   1.117 +lemma Un_UNIV_left: "UNIV \<union> B = UNIV"
   1.118 +  by (fact sup_top_left) (* already simp *)
   1.119  
   1.120 -lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
   1.121 -  by (fact sup_top_right)
   1.122 +lemma Un_UNIV_right: "A \<union> UNIV = UNIV"
   1.123 +  by (fact sup_top_right) (* already simp *)
   1.124  
   1.125  lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
   1.126    by blast
   1.127 @@ -1344,7 +1344,7 @@
   1.128    by (fact le_iff_sup)
   1.129  
   1.130  lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   1.131 -  by (fact sup_eq_bot_iff)
   1.132 +  by (fact sup_eq_bot_iff) (* FIXME: already simp *)
   1.133  
   1.134  lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   1.135    by (fact le_sup_iff)
   1.136 @@ -1370,14 +1370,14 @@
   1.137  lemma Compl_partition2: "-A \<union> A = UNIV"
   1.138    by (fact compl_sup_top)
   1.139  
   1.140 -lemma double_complement [simp]: "- (-A) = (A::'a set)"
   1.141 -  by (fact double_compl)
   1.142 +lemma double_complement: "- (-A) = (A::'a set)"
   1.143 +  by (fact double_compl) (* already simp *)
   1.144  
   1.145 -lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
   1.146 -  by (fact compl_sup)
   1.147 +lemma Compl_Un: "-(A \<union> B) = (-A) \<inter> (-B)"
   1.148 +  by (fact compl_sup) (* already simp *)
   1.149  
   1.150 -lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
   1.151 -  by (fact compl_inf)
   1.152 +lemma Compl_Int: "-(A \<inter> B) = (-A) \<union> (-B)"
   1.153 +  by (fact compl_inf) (* already simp *)
   1.154  
   1.155  lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
   1.156    by blast
   1.157 @@ -1386,17 +1386,17 @@
   1.158    -- {* Halmos, Naive Set Theory, page 16. *}
   1.159    by blast
   1.160  
   1.161 -lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
   1.162 -  by (fact compl_top_eq)
   1.163 +lemma Compl_UNIV_eq: "-UNIV = {}"
   1.164 +  by (fact compl_top_eq) (* already simp *)
   1.165  
   1.166 -lemma Compl_empty_eq [simp]: "-{} = UNIV"
   1.167 -  by (fact compl_bot_eq)
   1.168 +lemma Compl_empty_eq: "-{} = UNIV"
   1.169 +  by (fact compl_bot_eq) (* already simp *)
   1.170  
   1.171  lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
   1.172 -  by (fact compl_le_compl_iff)
   1.173 +  by (fact compl_le_compl_iff) (* FIXME: already simp *)
   1.174  
   1.175  lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
   1.176 -  by (fact compl_eq_compl_iff)
   1.177 +  by (fact compl_eq_compl_iff) (* FIXME: already simp *)
   1.178  
   1.179  lemma Compl_insert: "- insert x A = (-A) - {x}"
   1.180    by blast