src/HOL/Set.thy
changeset 36009 9cdbc5ffc15c
parent 35828 46cfc4b8112e
child 37387 3581483cca6c
     1.1 --- a/src/HOL/Set.thy	Sun Mar 28 12:49:14 2010 -0700
     1.2 +++ b/src/HOL/Set.thy	Sun Mar 28 12:50:38 2010 -0700
     1.3 @@ -507,7 +507,6 @@
     1.4    apply (rule Collect_mem_eq)
     1.5    done
     1.6  
     1.7 -(* Due to Brian Huffman *)
     1.8  lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
     1.9  by(auto intro:set_ext)
    1.10  
    1.11 @@ -1002,25 +1001,25 @@
    1.12  text {* \medskip Finite Union -- the least upper bound of two sets. *}
    1.13  
    1.14  lemma Un_upper1: "A \<subseteq> A \<union> B"
    1.15 -  by blast
    1.16 +  by (fact sup_ge1)
    1.17  
    1.18  lemma Un_upper2: "B \<subseteq> A \<union> B"
    1.19 -  by blast
    1.20 +  by (fact sup_ge2)
    1.21  
    1.22  lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
    1.23 -  by blast
    1.24 +  by (fact sup_least)
    1.25  
    1.26  
    1.27  text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
    1.28  
    1.29  lemma Int_lower1: "A \<inter> B \<subseteq> A"
    1.30 -  by blast
    1.31 +  by (fact inf_le1)
    1.32  
    1.33  lemma Int_lower2: "A \<inter> B \<subseteq> B"
    1.34 -  by blast
    1.35 +  by (fact inf_le2)
    1.36  
    1.37  lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
    1.38 -  by blast
    1.39 +  by (fact inf_greatest)
    1.40  
    1.41  
    1.42  text {* \medskip Set difference. *}
    1.43 @@ -1166,34 +1165,34 @@
    1.44  text {* \medskip @{text Int} *}
    1.45  
    1.46  lemma Int_absorb [simp]: "A \<inter> A = A"
    1.47 -  by blast
    1.48 +  by (fact inf_idem)
    1.49  
    1.50  lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
    1.51 -  by blast
    1.52 +  by (fact inf_left_idem)
    1.53  
    1.54  lemma Int_commute: "A \<inter> B = B \<inter> A"
    1.55 -  by blast
    1.56 +  by (fact inf_commute)
    1.57  
    1.58  lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
    1.59 -  by blast
    1.60 +  by (fact inf_left_commute)
    1.61  
    1.62  lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
    1.63 -  by blast
    1.64 +  by (fact inf_assoc)
    1.65  
    1.66  lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
    1.67    -- {* Intersection is an AC-operator *}
    1.68  
    1.69  lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
    1.70 -  by blast
    1.71 +  by (fact inf_absorb2)
    1.72  
    1.73  lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
    1.74 -  by blast
    1.75 +  by (fact inf_absorb1)
    1.76  
    1.77  lemma Int_empty_left [simp]: "{} \<inter> B = {}"
    1.78 -  by blast
    1.79 +  by (fact inf_bot_left)
    1.80  
    1.81  lemma Int_empty_right [simp]: "A \<inter> {} = {}"
    1.82 -  by blast
    1.83 +  by (fact inf_bot_right)
    1.84  
    1.85  lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
    1.86    by blast
    1.87 @@ -1202,22 +1201,22 @@
    1.88    by blast
    1.89  
    1.90  lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
    1.91 -  by blast
    1.92 +  by (fact inf_top_left)
    1.93  
    1.94  lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
    1.95 -  by blast
    1.96 +  by (fact inf_top_right)
    1.97  
    1.98  lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
    1.99 -  by blast
   1.100 +  by (fact inf_sup_distrib1)
   1.101  
   1.102  lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   1.103 -  by blast
   1.104 +  by (fact inf_sup_distrib2)
   1.105  
   1.106  lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   1.107 -  by blast
   1.108 +  by (fact inf_eq_top_iff)
   1.109  
   1.110  lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
   1.111 -  by blast
   1.112 +  by (fact le_inf_iff)
   1.113  
   1.114  lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
   1.115    by blast
   1.116 @@ -1226,40 +1225,40 @@
   1.117  text {* \medskip @{text Un}. *}
   1.118  
   1.119  lemma Un_absorb [simp]: "A \<union> A = A"
   1.120 -  by blast
   1.121 +  by (fact sup_idem)
   1.122  
   1.123  lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
   1.124 -  by blast
   1.125 +  by (fact sup_left_idem)
   1.126  
   1.127  lemma Un_commute: "A \<union> B = B \<union> A"
   1.128 -  by blast
   1.129 +  by (fact sup_commute)
   1.130  
   1.131  lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
   1.132 -  by blast
   1.133 +  by (fact sup_left_commute)
   1.134  
   1.135  lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
   1.136 -  by blast
   1.137 +  by (fact sup_assoc)
   1.138  
   1.139  lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
   1.140    -- {* Union is an AC-operator *}
   1.141  
   1.142  lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
   1.143 -  by blast
   1.144 +  by (fact sup_absorb2)
   1.145  
   1.146  lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
   1.147 -  by blast
   1.148 +  by (fact sup_absorb1)
   1.149  
   1.150  lemma Un_empty_left [simp]: "{} \<union> B = B"
   1.151 -  by blast
   1.152 +  by (fact sup_bot_left)
   1.153  
   1.154  lemma Un_empty_right [simp]: "A \<union> {} = A"
   1.155 -  by blast
   1.156 +  by (fact sup_bot_right)
   1.157  
   1.158  lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
   1.159 -  by blast
   1.160 +  by (fact sup_top_left)
   1.161  
   1.162  lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
   1.163 -  by blast
   1.164 +  by (fact sup_top_right)
   1.165  
   1.166  lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
   1.167    by blast
   1.168 @@ -1292,23 +1291,23 @@
   1.169    by auto
   1.170  
   1.171  lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
   1.172 -  by blast
   1.173 +  by (fact sup_inf_distrib1)
   1.174  
   1.175  lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
   1.176 -  by blast
   1.177 +  by (fact sup_inf_distrib2)
   1.178  
   1.179  lemma Un_Int_crazy:
   1.180      "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
   1.181    by blast
   1.182  
   1.183  lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
   1.184 -  by blast
   1.185 +  by (fact le_iff_sup)
   1.186  
   1.187  lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   1.188 -  by blast
   1.189 +  by (fact sup_eq_bot_iff)
   1.190  
   1.191  lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   1.192 -  by blast
   1.193 +  by (fact le_sup_iff)
   1.194  
   1.195  lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
   1.196    by blast
   1.197 @@ -1320,25 +1319,25 @@
   1.198  text {* \medskip Set complement *}
   1.199  
   1.200  lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
   1.201 -  by blast
   1.202 +  by (fact inf_compl_bot)
   1.203  
   1.204  lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
   1.205 -  by blast
   1.206 +  by (fact compl_inf_bot)
   1.207  
   1.208  lemma Compl_partition: "A \<union> -A = UNIV"
   1.209 -  by blast
   1.210 +  by (fact sup_compl_top)
   1.211  
   1.212  lemma Compl_partition2: "-A \<union> A = UNIV"
   1.213 -  by blast
   1.214 +  by (fact compl_sup_top)
   1.215  
   1.216  lemma double_complement [simp]: "- (-A) = (A::'a set)"
   1.217 -  by blast
   1.218 +  by (fact double_compl)
   1.219  
   1.220  lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
   1.221 -  by blast
   1.222 +  by (fact compl_sup)
   1.223  
   1.224  lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
   1.225 -  by blast
   1.226 +  by (fact compl_inf)
   1.227  
   1.228  lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
   1.229    by blast
   1.230 @@ -1348,16 +1347,16 @@
   1.231    by blast
   1.232  
   1.233  lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
   1.234 -  by blast
   1.235 +  by (fact compl_top_eq)
   1.236  
   1.237  lemma Compl_empty_eq [simp]: "-{} = UNIV"
   1.238 -  by blast
   1.239 +  by (fact compl_bot_eq)
   1.240  
   1.241  lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
   1.242 -  by blast
   1.243 +  by (fact compl_le_compl_iff)
   1.244  
   1.245  lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
   1.246 -  by blast
   1.247 +  by (fact compl_eq_compl_iff)
   1.248  
   1.249  text {* \medskip Bounded quantifiers.
   1.250  
   1.251 @@ -1531,16 +1530,16 @@
   1.252    by blast
   1.253  
   1.254  lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
   1.255 -  by blast
   1.256 +  by (fact sup_mono)
   1.257  
   1.258  lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
   1.259 -  by blast
   1.260 +  by (fact inf_mono)
   1.261  
   1.262  lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
   1.263    by blast
   1.264  
   1.265  lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
   1.266 -  by blast
   1.267 +  by (fact compl_mono)
   1.268  
   1.269  text {* \medskip Monotonicity of implications. *}
   1.270