author huffman Sun Mar 28 12:50:38 2010 -0700 (2010-03-28) changeset 36009 9cdbc5ffc15c parent 36008 23dfa8678c7c child 36010 a5e7574d8214
use lattice theorems to prove set theorems
 src/HOL/Set.thy file | annotate | diff | revisions
```     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
```