1.1 --- a/src/HOL/IsaMakefile Fri Feb 15 20:43:44 2002 +0100
1.2 +++ b/src/HOL/IsaMakefile Sat Feb 16 20:59:34 2002 +0100
1.3 @@ -102,8 +102,7 @@
1.4 Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
1.5 Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
1.6 Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
1.7 - document/root.tex equalities.ML hologic.ML meson_lemmas.ML mono.ML \
1.8 - simpdata.ML subset.ML thy_syntax.ML
1.9 + document/root.tex hologic.ML meson_lemmas.ML simpdata.ML thy_syntax.ML
1.10 @$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL
1.11
1.12
2.1 --- a/src/HOL/Set.ML Fri Feb 15 20:43:44 2002 +0100
2.2 +++ b/src/HOL/Set.ML Sat Feb 16 20:59:34 2002 +0100
2.3 @@ -1,6 +1,415 @@
2.4
2.5 (* legacy ML bindings *)
2.6
2.7 +val Ball_def = thm "Ball_def";
2.8 +val Bex_def = thm "Bex_def";
2.9 +val CollectD = thm "CollectD";
2.10 +val CollectE = thm "CollectE";
2.11 +val CollectI = thm "CollectI";
2.12 +val Collect_all_eq = thm "Collect_all_eq";
2.13 +val Collect_ball_eq = thm "Collect_ball_eq";
2.14 +val Collect_bex_eq = thm "Collect_bex_eq";
2.15 +val Collect_cong = thm "Collect_cong";
2.16 +val Collect_conj_eq = thm "Collect_conj_eq";
2.17 +val Collect_const = thm "Collect_const";
2.18 +val Collect_disj_eq = thm "Collect_disj_eq";
2.19 +val Collect_empty_eq = thm "Collect_empty_eq";
2.20 +val Collect_ex_eq = thm "Collect_ex_eq";
2.21 +val Collect_mem_eq = thm "Collect_mem_eq";
2.22 +val Collect_mono = thm "Collect_mono";
2.23 +val Collect_neg_eq = thm "Collect_neg_eq";
2.24 +val ComplD = thm "ComplD";
2.25 +val ComplE = thm "ComplE";
2.26 +val ComplI = thm "ComplI";
2.27 +val Compl_Diff_eq = thm "Compl_Diff_eq";
2.28 +val Compl_INT = thm "Compl_INT";
2.29 +val Compl_Int = thm "Compl_Int";
2.30 +val Compl_UN = thm "Compl_UN";
2.31 +val Compl_UNIV_eq = thm "Compl_UNIV_eq";
2.32 +val Compl_Un = thm "Compl_Un";
2.33 +val Compl_anti_mono = thm "Compl_anti_mono";
2.34 +val Compl_def = thm "Compl_def";
2.35 +val Compl_disjoint = thm "Compl_disjoint";
2.36 +val Compl_disjoint2 = thm "Compl_disjoint2";
2.37 +val Compl_empty_eq = thm "Compl_empty_eq";
2.38 +val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff";
2.39 +val Compl_iff = thm "Compl_iff";
2.40 +val Compl_partition = thm "Compl_partition";
2.41 +val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff";
2.42 +val DiffD1 = thm "DiffD1";
2.43 +val DiffD2 = thm "DiffD2";
2.44 +val DiffE = thm "DiffE";
2.45 +val DiffI = thm "DiffI";
2.46 +val Diff_Compl = thm "Diff_Compl";
2.47 +val Diff_Int = thm "Diff_Int";
2.48 +val Diff_Int_distrib = thm "Diff_Int_distrib";
2.49 +val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
2.50 +val Diff_UNIV = thm "Diff_UNIV";
2.51 +val Diff_Un = thm "Diff_Un";
2.52 +val Diff_cancel = thm "Diff_cancel";
2.53 +val Diff_disjoint = thm "Diff_disjoint";
2.54 +val Diff_empty = thm "Diff_empty";
2.55 +val Diff_eq = thm "Diff_eq";
2.56 +val Diff_eq_empty_iff = thm "Diff_eq_empty_iff";
2.57 +val Diff_iff = thm "Diff_iff";
2.58 +val Diff_insert = thm "Diff_insert";
2.59 +val Diff_insert0 = thm "Diff_insert0";
2.60 +val Diff_insert2 = thm "Diff_insert2";
2.61 +val Diff_insert_absorb = thm "Diff_insert_absorb";
2.62 +val Diff_mono = thm "Diff_mono";
2.63 +val Diff_partition = thm "Diff_partition";
2.64 +val Diff_subset = thm "Diff_subset";
2.65 +val Diff_triv = thm "Diff_triv";
2.66 +val INTER_def = thm "INTER_def";
2.67 +val INT_D = thm "INT_D";
2.68 +val INT_E = thm "INT_E";
2.69 +val INT_I = thm "INT_I";
2.70 +val INT_Int_distrib = thm "INT_Int_distrib";
2.71 +val INT_Un = thm "INT_Un";
2.72 +val INT_absorb = thm "INT_absorb";
2.73 +val INT_anti_mono = thm "INT_anti_mono";
2.74 +val INT_bool_eq = thm "INT_bool_eq";
2.75 +val INT_cong = thm "INT_cong";
2.76 +val INT_constant = thm "INT_constant";
2.77 +val INT_empty = thm "INT_empty";
2.78 +val INT_eq = thm "INT_eq";
2.79 +val INT_greatest = thm "INT_greatest";
2.80 +val INT_iff = thm "INT_iff";
2.81 +val INT_insert = thm "INT_insert";
2.82 +val INT_insert_distrib = thm "INT_insert_distrib";
2.83 +val INT_lower = thm "INT_lower";
2.84 +val INT_simps = thms "INT_simps";
2.85 +val INT_subset_iff = thm "INT_subset_iff";
2.86 +val IntD1 = thm "IntD1";
2.87 +val IntD2 = thm "IntD2";
2.88 +val IntE = thm "IntE";
2.89 +val IntI = thm "IntI";
2.90 +val Int_Collect = thm "Int_Collect";
2.91 +val Int_Collect_mono = thm "Int_Collect_mono";
2.92 +val Int_Diff = thm "Int_Diff";
2.93 +val Int_Inter_image = thm "Int_Inter_image";
2.94 +val Int_UNIV = thm "Int_UNIV";
2.95 +val Int_UNIV_left = thm "Int_UNIV_left";
2.96 +val Int_UNIV_right = thm "Int_UNIV_right";
2.97 +val Int_UN_distrib = thm "Int_UN_distrib";
2.98 +val Int_UN_distrib2 = thm "Int_UN_distrib2";
2.99 +val Int_Un_distrib = thm "Int_Un_distrib";
2.100 +val Int_Un_distrib2 = thm "Int_Un_distrib2";
2.101 +val Int_Union = thm "Int_Union";
2.102 +val Int_Union2 = thm "Int_Union2";
2.103 +val Int_absorb = thm "Int_absorb";
2.104 +val Int_absorb1 = thm "Int_absorb1";
2.105 +val Int_absorb2 = thm "Int_absorb2";
2.106 +val Int_ac = thms "Int_ac";
2.107 +val Int_assoc = thm "Int_assoc";
2.108 +val Int_commute = thm "Int_commute";
2.109 +val Int_def = thm "Int_def";
2.110 +val Int_empty_left = thm "Int_empty_left";
2.111 +val Int_empty_right = thm "Int_empty_right";
2.112 +val Int_eq_Inter = thm "Int_eq_Inter";
2.113 +val Int_greatest = thm "Int_greatest";
2.114 +val Int_iff = thm "Int_iff";
2.115 +val Int_insert_left = thm "Int_insert_left";
2.116 +val Int_insert_right = thm "Int_insert_right";
2.117 +val Int_left_absorb = thm "Int_left_absorb";
2.118 +val Int_left_commute = thm "Int_left_commute";
2.119 +val Int_lower1 = thm "Int_lower1";
2.120 +val Int_lower2 = thm "Int_lower2";
2.121 +val Int_mono = thm "Int_mono";
2.122 +val Int_subset_iff = thm "Int_subset_iff";
2.123 +val InterD = thm "InterD";
2.124 +val InterE = thm "InterE";
2.125 +val InterI = thm "InterI";
2.126 +val Inter_UNIV = thm "Inter_UNIV";
2.127 +val Inter_Un_distrib = thm "Inter_Un_distrib";
2.128 +val Inter_Un_subset = thm "Inter_Un_subset";
2.129 +val Inter_anti_mono = thm "Inter_anti_mono";
2.130 +val Inter_def = thm "Inter_def";
2.131 +val Inter_empty = thm "Inter_empty";
2.132 +val Inter_greatest = thm "Inter_greatest";
2.133 +val Inter_iff = thm "Inter_iff";
2.134 +val Inter_image_eq = thm "Inter_image_eq";
2.135 +val Inter_insert = thm "Inter_insert";
2.136 +val Inter_lower = thm "Inter_lower";
2.137 +val PowD = thm "PowD";
2.138 +val PowI = thm "PowI";
2.139 +val Pow_Compl = thm "Pow_Compl";
2.140 +val Pow_INT_eq = thm "Pow_INT_eq";
2.141 +val Pow_Int_eq = thm "Pow_Int_eq";
2.142 +val Pow_UNIV = thm "Pow_UNIV";
2.143 +val Pow_bottom = thm "Pow_bottom";
2.144 +val Pow_def = thm "Pow_def";
2.145 +val Pow_empty = thm "Pow_empty";
2.146 +val Pow_iff = thm "Pow_iff";
2.147 +val Pow_insert = thm "Pow_insert";
2.148 +val Pow_mono = thm "Pow_mono";
2.149 +val Pow_top = thm "Pow_top";
2.150 +val UNION_def = thm "UNION_def";
2.151 +val UNIV_I = thm "UNIV_I";
2.152 +val UNIV_def = thm "UNIV_def";
2.153 +val UNIV_not_empty = thm "UNIV_not_empty";
2.154 +val UNIV_witness = thm "UNIV_witness";
2.155 +val UN_E = thm "UN_E";
2.156 +val UN_I = thm "UN_I";
2.157 +val UN_Pow_subset = thm "UN_Pow_subset";
2.158 +val UN_UN_flatten = thm "UN_UN_flatten";
2.159 +val UN_Un = thm "UN_Un";
2.160 +val UN_Un_distrib = thm "UN_Un_distrib";
2.161 +val UN_absorb = thm "UN_absorb";
2.162 +val UN_bool_eq = thm "UN_bool_eq";
2.163 +val UN_cong = thm "UN_cong";
2.164 +val UN_constant = thm "UN_constant";
2.165 +val UN_empty = thm "UN_empty";
2.166 +val UN_empty2 = thm "UN_empty2";
2.167 +val UN_empty3 = thm "UN_empty3";
2.168 +val UN_eq = thm "UN_eq";
2.169 +val UN_iff = thm "UN_iff";
2.170 +val UN_insert = thm "UN_insert";
2.171 +val UN_insert_distrib = thm "UN_insert_distrib";
2.172 +val UN_least = thm "UN_least";
2.173 +val UN_mono = thm "UN_mono";
2.174 +val UN_simps = thms "UN_simps";
2.175 +val UN_singleton = thm "UN_singleton";
2.176 +val UN_subset_iff = thm "UN_subset_iff";
2.177 +val UN_upper = thm "UN_upper";
2.178 +val UnCI = thm "UnCI";
2.179 +val UnE = thm "UnE";
2.180 +val UnI1 = thm "UnI1";
2.181 +val UnI2 = thm "UnI2";
2.182 +val Un_Diff = thm "Un_Diff";
2.183 +val Un_Diff_Int = thm "Un_Diff_Int";
2.184 +val Un_Diff_cancel = thm "Un_Diff_cancel";
2.185 +val Un_Diff_cancel2 = thm "Un_Diff_cancel2";
2.186 +val Un_INT_distrib = thm "Un_INT_distrib";
2.187 +val Un_INT_distrib2 = thm "Un_INT_distrib2";
2.188 +val Un_Int_assoc_eq = thm "Un_Int_assoc_eq";
2.189 +val Un_Int_crazy = thm "Un_Int_crazy";
2.190 +val Un_Int_distrib = thm "Un_Int_distrib";
2.191 +val Un_Int_distrib2 = thm "Un_Int_distrib2";
2.192 +val Un_Inter = thm "Un_Inter";
2.193 +val Un_Pow_subset = thm "Un_Pow_subset";
2.194 +val Un_UNIV_left = thm "Un_UNIV_left";
2.195 +val Un_UNIV_right = thm "Un_UNIV_right";
2.196 +val Un_Union_image = thm "Un_Union_image";
2.197 +val Un_absorb = thm "Un_absorb";
2.198 +val Un_absorb1 = thm "Un_absorb1";
2.199 +val Un_absorb2 = thm "Un_absorb2";
2.200 +val Un_ac = thms "Un_ac";
2.201 +val Un_assoc = thm "Un_assoc";
2.202 +val Un_commute = thm "Un_commute";
2.203 +val Un_def = thm "Un_def";
2.204 +val Un_empty = thm "Un_empty";
2.205 +val Un_empty_left = thm "Un_empty_left";
2.206 +val Un_empty_right = thm "Un_empty_right";
2.207 +val Un_eq_UN = thm "Un_eq_UN";
2.208 +val Un_eq_Union = thm "Un_eq_Union";
2.209 +val Un_iff = thm "Un_iff";
2.210 +val Un_insert_left = thm "Un_insert_left";
2.211 +val Un_insert_right = thm "Un_insert_right";
2.212 +val Un_least = thm "Un_least";
2.213 +val Un_left_absorb = thm "Un_left_absorb";
2.214 +val Un_left_commute = thm "Un_left_commute";
2.215 +val Un_mono = thm "Un_mono";
2.216 +val Un_subset_iff = thm "Un_subset_iff";
2.217 +val Un_upper1 = thm "Un_upper1";
2.218 +val Un_upper2 = thm "Un_upper2";
2.219 +val UnionE = thm "UnionE";
2.220 +val UnionI = thm "UnionI";
2.221 +val Union_Int_subset = thm "Union_Int_subset";
2.222 +val Union_Pow_eq = thm "Union_Pow_eq";
2.223 +val Union_UNIV = thm "Union_UNIV";
2.224 +val Union_Un_distrib = thm "Union_Un_distrib";
2.225 +val Union_def = thm "Union_def";
2.226 +val Union_disjoint = thm "Union_disjoint";
2.227 +val Union_empty = thm "Union_empty";
2.228 +val Union_empty_conv = thm "Union_empty_conv";
2.229 +val Union_iff = thm "Union_iff";
2.230 +val Union_image_eq = thm "Union_image_eq";
2.231 +val Union_insert = thm "Union_insert";
2.232 +val Union_least = thm "Union_least";
2.233 +val Union_mono = thm "Union_mono";
2.234 +val Union_upper = thm "Union_upper";
2.235 +val all_bool_eq = thm "all_bool_eq";
2.236 +val all_mono = thm "all_mono";
2.237 +val all_not_in_conv = thm "all_not_in_conv";
2.238 +val atomize_ball = thm "atomize_ball";
2.239 +val ballE = thm "ballE";
2.240 +val ballI = thm "ballI";
2.241 +val ball_UN = thm "ball_UN";
2.242 +val ball_UNIV = thm "ball_UNIV";
2.243 +val ball_Un = thm "ball_Un";
2.244 +val ball_cong = thm "ball_cong";
2.245 +val ball_conj_distrib = thm "ball_conj_distrib";
2.246 +val ball_empty = thm "ball_empty";
2.247 +val ball_one_point1 = thm "ball_one_point1";
2.248 +val ball_one_point2 = thm "ball_one_point2";
2.249 +val ball_simps = thms "ball_simps";
2.250 +val ball_triv = thm "ball_triv";
2.251 +val basic_monos = thms "basic_monos";
2.252 +val bexCI = thm "bexCI";
2.253 +val bexE = thm "bexE";
2.254 +val bexI = thm "bexI";
2.255 +val bex_UN = thm "bex_UN";
2.256 +val bex_UNIV = thm "bex_UNIV";
2.257 +val bex_Un = thm "bex_Un";
2.258 +val bex_cong = thm "bex_cong";
2.259 +val bex_disj_distrib = thm "bex_disj_distrib";
2.260 +val bex_empty = thm "bex_empty";
2.261 +val bex_one_point1 = thm "bex_one_point1";
2.262 +val bex_one_point2 = thm "bex_one_point2";
2.263 +val bex_simps = thms "bex_simps";
2.264 +val bex_triv = thm "bex_triv";
2.265 +val bex_triv_one_point1 = thm "bex_triv_one_point1";
2.266 +val bex_triv_one_point2 = thm "bex_triv_one_point2";
2.267 +val bool_induct = thm "bool_induct";
2.268 +val bspec = thm "bspec";
2.269 +val conj_mono = thm "conj_mono";
2.270 +val contra_subsetD = thm "contra_subsetD";
2.271 +val diff_single_insert = thm "diff_single_insert";
2.272 +val disj_mono = thm "disj_mono";
2.273 +val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl";
2.274 +val disjoint_iff_not_equal = thm "disjoint_iff_not_equal";
2.275 +val distinct_lemma = thm "distinct_lemma";
2.276 +val double_complement = thm "double_complement";
2.277 +val double_diff = thm "double_diff";
2.278 +val emptyE = thm "emptyE";
2.279 +val empty_Diff = thm "empty_Diff";
2.280 +val empty_def = thm "empty_def";
2.281 +val empty_iff = thm "empty_iff";
2.282 +val empty_subsetI = thm "empty_subsetI";
2.283 +val eq_to_mono = thm "eq_to_mono";
2.284 +val eq_to_mono2 = thm "eq_to_mono2";
2.285 +val eqset_imp_iff = thm "eqset_imp_iff";
2.286 +val equalityCE = thm "equalityCE";
2.287 +val equalityD1 = thm "equalityD1";
2.288 +val equalityD2 = thm "equalityD2";
2.289 +val equalityE = thm "equalityE";
2.290 +val equalityI = thm "equalityI";
2.291 +val equals0D = thm "equals0D";
2.292 +val equals0I = thm "equals0I";
2.293 +val ex_bool_eq = thm "ex_bool_eq";
2.294 +val ex_mono = thm "ex_mono";
2.295 +val full_SetCompr_eq = thm "full_SetCompr_eq";
2.296 +val if_image_distrib = thm "if_image_distrib";
2.297 +val imageE = thm "imageE";
2.298 +val imageI = thm "imageI";
2.299 +val image_Collect = thm "image_Collect";
2.300 +val image_Un = thm "image_Un";
2.301 +val image_Union = thm "image_Union";
2.302 +val image_cong = thm "image_cong";
2.303 +val image_constant = thm "image_constant";
2.304 +val image_def = thm "image_def";
2.305 +val image_empty = thm "image_empty";
2.306 +val image_eqI = thm "image_eqI";
2.307 +val image_iff = thm "image_iff";
2.308 +val image_image = thm "image_image";
2.309 +val image_insert = thm "image_insert";
2.310 +val image_is_empty = thm "image_is_empty";
2.311 +val image_mono = thm "image_mono";
2.312 +val image_subsetI = thm "image_subsetI";
2.313 +val image_subset_iff = thm "image_subset_iff";
2.314 +val imp_mono = thm "imp_mono";
2.315 +val imp_refl = thm "imp_refl";
2.316 +val in_mono = thm "in_mono";
2.317 +val insertCI = thm "insertCI";
2.318 +val insertE = thm "insertE";
2.319 +val insertI1 = thm "insertI1";
2.320 +val insertI2 = thm "insertI2";
2.321 +val insert_Collect = thm "insert_Collect";
2.322 +val insert_Diff = thm "insert_Diff";
2.323 +val insert_Diff1 = thm "insert_Diff1";
2.324 +val insert_Diff_if = thm "insert_Diff_if";
2.325 +val insert_absorb = thm "insert_absorb";
2.326 +val insert_absorb2 = thm "insert_absorb2";
2.327 +val insert_commute = thm "insert_commute";
2.328 +val insert_def = thm "insert_def";
2.329 +val insert_iff = thm "insert_iff";
2.330 +val insert_image = thm "insert_image";
2.331 +val insert_is_Un = thm "insert_is_Un";
2.332 +val insert_mono = thm "insert_mono";
2.333 +val insert_not_empty = thm "insert_not_empty";
2.334 +val insert_subset = thm "insert_subset";
2.335 +val mem_Collect_eq = thm "mem_Collect_eq";
2.336 +val mem_simps = thms "mem_simps";
2.337 +val mk_disjoint_insert = thm "mk_disjoint_insert";
2.338 +val mono_Int = thm "mono_Int";
2.339 +val mono_Un = thm "mono_Un";
2.340 +val not_psubset_empty = thm "not_psubset_empty";
2.341 +val psubsetI = thm "psubsetI";
2.342 +val psubset_def = thm "psubset_def";
2.343 +val psubset_eq = thm "psubset_eq";
2.344 +val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
2.345 +val psubset_imp_subset = thm "psubset_imp_subset";
2.346 +val psubset_insert_iff = thm "psubset_insert_iff";
2.347 +val psubset_subset_trans = thm "psubset_subset_trans";
2.348 +val rangeE = thm "rangeE";
2.349 +val rangeI = thm "rangeI";
2.350 +val range_composition = thm "range_composition";
2.351 +val range_eqI = thm "range_eqI";
2.352 +val rev_bexI = thm "rev_bexI";
2.353 +val rev_image_eqI = thm "rev_image_eqI";
2.354 +val rev_subsetD = thm "rev_subsetD";
2.355 +val set_diff_def = thm "set_diff_def";
2.356 +val set_eq_subset = thm "set_eq_subset";
2.357 +val set_ext = thm "set_ext";
2.358 +val setup_induction = thm "setup_induction";
2.359 +val singletonD = thm "singletonD";
2.360 +val singletonE = thm "singletonE";
2.361 +val singletonI = thm "singletonI";
2.362 +val singleton_conv = thm "singleton_conv";
2.363 +val singleton_conv2 = thm "singleton_conv2";
2.364 +val singleton_iff = thm "singleton_iff";
2.365 +val singleton_inject = thm "singleton_inject";
2.366 +val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
2.367 +val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
2.368 +val split_if_eq1 = thm "split_if_eq1";
2.369 +val split_if_eq2 = thm "split_if_eq2";
2.370 +val split_if_mem1 = thm "split_if_mem1";
2.371 +val split_if_mem2 = thm "split_if_mem2";
2.372 +val split_ifs = thms "split_ifs";
2.373 +val strip = thms "strip";
2.374 +val subsetCE = thm "subsetCE";
2.375 +val subsetD = thm "subsetD";
2.376 +val subsetI = thm "subsetI";
2.377 +val subset_Compl_self_eq = thm "subset_Compl_self_eq";
2.378 +val subset_Pow_Union = thm "subset_Pow_Union";
2.379 +val subset_UNIV = thm "subset_UNIV";
2.380 +val subset_Un_eq = thm "subset_Un_eq";
2.381 +val subset_antisym = thm "subset_antisym";
2.382 +val subset_def = thm "subset_def";
2.383 +val subset_empty = thm "subset_empty";
2.384 +val subset_iff = thm "subset_iff";
2.385 +val subset_iff_psubset_eq = thm "subset_iff_psubset_eq";
2.386 +val subset_image_iff = thm "subset_image_iff";
2.387 +val subset_insert = thm "subset_insert";
2.388 +val subset_insertI = thm "subset_insertI";
2.389 +val subset_insert_iff = thm "subset_insert_iff";
2.390 +val subset_psubset_trans = thm "subset_psubset_trans";
2.391 +val subset_refl = thm "subset_refl";
2.392 +val subset_singletonD = thm "subset_singletonD";
2.393 +val subset_trans = thm "subset_trans";
2.394 +val vimageD = thm "vimageD";
2.395 +val vimageE = thm "vimageE";
2.396 +val vimageI = thm "vimageI";
2.397 +val vimageI2 = thm "vimageI2";
2.398 +val vimage_Collect = thm "vimage_Collect";
2.399 +val vimage_Collect_eq = thm "vimage_Collect_eq";
2.400 +val vimage_Compl = thm "vimage_Compl";
2.401 +val vimage_Diff = thm "vimage_Diff";
2.402 +val vimage_INT = thm "vimage_INT";
2.403 +val vimage_Int = thm "vimage_Int";
2.404 +val vimage_UN = thm "vimage_UN";
2.405 +val vimage_UNIV = thm "vimage_UNIV";
2.406 +val vimage_Un = thm "vimage_Un";
2.407 +val vimage_Union = thm "vimage_Union";
2.408 +val vimage_def = thm "vimage_def";
2.409 +val vimage_empty = thm "vimage_empty";
2.410 +val vimage_eq = thm "vimage_eq";
2.411 +val vimage_eq_UN = thm "vimage_eq_UN";
2.412 +val vimage_insert = thm "vimage_insert";
2.413 +val vimage_mono = thm "vimage_mono";
2.414 +val vimage_singleton_eq = thm "vimage_singleton_eq";
2.415 +
2.416 structure Set =
2.417 struct
2.418 val thy = the_context ();
2.419 @@ -24,25 +433,3 @@
2.420 val set_diff_def = set_diff_def;
2.421 val subset_def = subset_def;
2.422 end;
2.423 -
2.424 -val vimageD = thm "vimageD";
2.425 -val vimageE = thm "vimageE";
2.426 -val vimageI = thm "vimageI";
2.427 -val vimageI2 = thm "vimageI2";
2.428 -val vimage_Collect = thm "vimage_Collect";
2.429 -val vimage_Collect_eq = thm "vimage_Collect_eq";
2.430 -val vimage_Compl = thm "vimage_Compl";
2.431 -val vimage_Diff = thm "vimage_Diff";
2.432 -val vimage_INT = thm "vimage_INT";
2.433 -val vimage_Int = thm "vimage_Int";
2.434 -val vimage_UN = thm "vimage_UN";
2.435 -val vimage_UNIV = thm "vimage_UNIV";
2.436 -val vimage_Un = thm "vimage_Un";
2.437 -val vimage_Union = thm "vimage_Union";
2.438 -val vimage_def = thm "vimage_def";
2.439 -val vimage_empty = thm "vimage_empty";
2.440 -val vimage_eq = thm "vimage_eq";
2.441 -val vimage_eq_UN = thm "vimage_eq_UN";
2.442 -val vimage_insert = thm "vimage_insert";
2.443 -val vimage_mono = thm "vimage_mono";
2.444 -val vimage_singleton_eq = thm "vimage_singleton_eq";
3.1 --- a/src/HOL/Set.thy Fri Feb 15 20:43:44 2002 +0100
3.2 +++ b/src/HOL/Set.thy Sat Feb 16 20:59:34 2002 +0100
3.3 @@ -6,8 +6,7 @@
3.4
3.5 header {* Set theory for higher-order logic *}
3.6
3.7 -theory Set = HOL
3.8 -files ("subset.ML") ("equalities.ML") ("mono.ML"):
3.9 +theory Set = HOL:
3.10
3.11 text {* A set in HOL is simply a predicate. *}
3.12
3.13 @@ -339,7 +338,7 @@
3.14
3.15 subsubsection {* Subsets *}
3.16
3.17 -lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B"
3.18 +lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
3.19 by (simp add: subset_def)
3.20
3.21 text {*
3.22 @@ -364,13 +363,13 @@
3.23 Blast.overloaded (\"image\", domain_type);
3.24 "
3.25
3.26 -lemma subsetD [elim]: "A <= B ==> c:A ==> c:B"
3.27 +lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
3.28 -- {* Rule in Modus Ponens style. *}
3.29 by (unfold subset_def) blast
3.30
3.31 declare subsetD [intro?] -- FIXME
3.32
3.33 -lemma rev_subsetD: "c:A ==> A <= B ==> c:B"
3.34 +lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
3.35 -- {* The same, with reversed premises for use with @{text erule} --
3.36 cf @{text rev_mp}. *}
3.37 by (rule subsetD)
3.38 @@ -378,7 +377,7 @@
3.39 declare rev_subsetD [intro?] -- FIXME
3.40
3.41 text {*
3.42 - \medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}.
3.43 + \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
3.44 *}
3.45
3.46 ML {*
3.47 @@ -386,13 +385,13 @@
3.48 in fun impOfSubs th = th RSN (2, rev_subsetD) end;
3.49 *}
3.50
3.51 -lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P"
3.52 +lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
3.53 -- {* Classical elimination rule. *}
3.54 by (unfold subset_def) blast
3.55
3.56 text {*
3.57 - \medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and
3.58 - creates the assumption @{prop "c:B"}.
3.59 + \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
3.60 + creates the assumption @{prop "c \<in> B"}.
3.61 *}
3.62
3.63 ML {*
3.64 @@ -400,46 +399,46 @@
3.65 in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;
3.66 *}
3.67
3.68 -lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A"
3.69 +lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
3.70 by blast
3.71
3.72 -lemma subset_refl: "A <= (A::'a set)"
3.73 +lemma subset_refl: "A \<subseteq> A"
3.74 by fast
3.75
3.76 -lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)"
3.77 +lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
3.78 by blast
3.79
3.80
3.81 subsubsection {* Equality *}
3.82
3.83 -lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)"
3.84 +lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
3.85 -- {* Anti-symmetry of the subset relation. *}
3.86 - by (rule set_ext) (blast intro: subsetD)
3.87 -
3.88 -lemmas equalityI = subset_antisym
3.89 + by (rules intro: set_ext subsetD)
3.90 +
3.91 +lemmas equalityI [intro!] = subset_antisym
3.92
3.93 text {*
3.94 \medskip Equality rules from ZF set theory -- are they appropriate
3.95 here?
3.96 *}
3.97
3.98 -lemma equalityD1: "A = B ==> A <= (B::'a set)"
3.99 +lemma equalityD1: "A = B ==> A \<subseteq> B"
3.100 by (simp add: subset_refl)
3.101
3.102 -lemma equalityD2: "A = B ==> B <= (A::'a set)"
3.103 +lemma equalityD2: "A = B ==> B \<subseteq> A"
3.104 by (simp add: subset_refl)
3.105
3.106 text {*
3.107 \medskip Be careful when adding this to the claset as @{text
3.108 subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
3.109 - <= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}!
3.110 + \<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!
3.111 *}
3.112
3.113 -lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P"
3.114 +lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
3.115 by (simp add: subset_refl)
3.116
3.117 lemma equalityCE [elim]:
3.118 - "A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P"
3.119 + "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
3.120 by blast
3.121
3.122 text {*
3.123 @@ -466,7 +465,7 @@
3.124 lemma UNIV_witness [intro?]: "EX x. x : UNIV"
3.125 by simp
3.126
3.127 -lemma subset_UNIV: "A <= UNIV"
3.128 +lemma subset_UNIV: "A \<subseteq> UNIV"
3.129 by (rule subsetI) (rule UNIV_I)
3.130
3.131 text {*
3.132 @@ -490,14 +489,14 @@
3.133 lemma emptyE [elim!]: "a : {} ==> P"
3.134 by simp
3.135
3.136 -lemma empty_subsetI [iff]: "{} <= A"
3.137 +lemma empty_subsetI [iff]: "{} \<subseteq> A"
3.138 -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
3.139 by blast
3.140
3.141 -lemma equals0I: "(!!y. y:A ==> False) ==> A = {}"
3.142 +lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
3.143 by blast
3.144
3.145 -lemma equals0D: "A={} ==> a ~: A"
3.146 +lemma equals0D: "A = {} ==> a \<notin> A"
3.147 -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
3.148 by blast
3.149
3.150 @@ -513,28 +512,28 @@
3.151
3.152 subsubsection {* The Powerset operator -- Pow *}
3.153
3.154 -lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
3.155 +lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)"
3.156 by (simp add: Pow_def)
3.157
3.158 -lemma PowI: "A <= B ==> A : Pow B"
3.159 +lemma PowI: "A \<subseteq> B ==> A \<in> Pow B"
3.160 by (simp add: Pow_def)
3.161
3.162 -lemma PowD: "A : Pow B ==> A <= B"
3.163 +lemma PowD: "A \<in> Pow B ==> A \<subseteq> B"
3.164 by (simp add: Pow_def)
3.165
3.166 -lemma Pow_bottom: "{}: Pow B"
3.167 +lemma Pow_bottom: "{} \<in> Pow B"
3.168 by simp
3.169
3.170 -lemma Pow_top: "A : Pow A"
3.171 +lemma Pow_top: "A \<in> Pow A"
3.172 by (simp add: subset_refl)
3.173
3.174
3.175 subsubsection {* Set complement *}
3.176
3.177 -lemma Compl_iff [simp]: "(c : -A) = (c~:A)"
3.178 +lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
3.179 by (unfold Compl_def) blast
3.180
3.181 -lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A"
3.182 +lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
3.183 by (unfold Compl_def) blast
3.184
3.185 text {*
3.186 @@ -625,7 +624,7 @@
3.187 -- {* Classical introduction rule. *}
3.188 by auto
3.189
3.190 -lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)"
3.191 +lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
3.192 by auto
3.193
3.194
3.195 @@ -646,13 +645,13 @@
3.196 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
3.197 by blast
3.198
3.199 -lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})"
3.200 +lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A \<subseteq> {b})"
3.201 by blast
3.202
3.203 -lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})"
3.204 +lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
3.205 by blast
3.206
3.207 -lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}"
3.208 +lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
3.209 by fast
3.210
3.211 lemma singleton_conv [simp]: "{x. x = a} = {a}"
3.212 @@ -661,7 +660,7 @@
3.213 lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
3.214 by blast
3.215
3.216 -lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B"
3.217 +lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B"
3.218 by blast
3.219
3.220
3.221 @@ -772,18 +771,18 @@
3.222 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
3.223 by blast
3.224
3.225 -lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)"
3.226 +lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
3.227 -- {* This rewrite rule would confuse users if made default. *}
3.228 by blast
3.229
3.230 -lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)"
3.231 +lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
3.232 apply safe
3.233 prefer 2 apply fast
3.234 apply (rule_tac x = "{a. a : A & f a : B}" in exI)
3.235 apply fast
3.236 done
3.237
3.238 -lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B"
3.239 +lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
3.240 -- {* Replaces the three steps @{text subsetI}, @{text imageE},
3.241 @{text hypsubst}, but breaks too many existing proofs. *}
3.242 by blast
3.243 @@ -792,13 +791,13 @@
3.244 \medskip Range of a function -- just a translation for image!
3.245 *}
3.246
3.247 -lemma range_eqI: "b = f x ==> b : range f"
3.248 +lemma range_eqI: "b = f x ==> b \<in> range f"
3.249 by simp
3.250
3.251 -lemma rangeI: "f x : range f"
3.252 +lemma rangeI: "f x \<in> range f"
3.253 by simp
3.254
3.255 -lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P"
3.256 +lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
3.257 by blast
3.258
3.259
3.260 @@ -852,42 +851,929 @@
3.261
3.262 subsubsection {* The ``proper subset'' relation *}
3.263
3.264 -lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B"
3.265 +lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
3.266 by (unfold psubset_def) blast
3.267
3.268 lemma psubset_insert_iff:
3.269 - "(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)"
3.270 - apply (simp add: psubset_def subset_insert_iff)
3.271 + "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
3.272 + by (auto simp add: psubset_def subset_insert_iff)
3.273 +
3.274 +lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
3.275 + by (simp only: psubset_def)
3.276 +
3.277 +lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
3.278 + by (simp add: psubset_eq)
3.279 +
3.280 +lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
3.281 + by (auto simp add: psubset_eq)
3.282 +
3.283 +lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
3.284 + by (auto simp add: psubset_eq)
3.285 +
3.286 +lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
3.287 + by (unfold psubset_def) blast
3.288 +
3.289 +lemma atomize_ball:
3.290 + "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
3.291 + by (simp only: Ball_def atomize_all atomize_imp)
3.292 +
3.293 +declare atomize_ball [symmetric, rulify]
3.294 +
3.295 +
3.296 +subsection {* Further set-theory lemmas *}
3.297 +
3.298 +subsubsection {* Derived rules involving subsets. *}
3.299 +
3.300 +text {* @{text insert}. *}
3.301 +
3.302 +lemma subset_insertI: "B \<subseteq> insert a B"
3.303 + apply (rule subsetI)
3.304 + apply (erule insertI2)
3.305 + done
3.306 +
3.307 +lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
3.308 + by blast
3.309 +
3.310 +
3.311 +text {* \medskip Big Union -- least upper bound of a set. *}
3.312 +
3.313 +lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
3.314 + by (rules intro: subsetI UnionI)
3.315 +
3.316 +lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
3.317 + by (rules intro: subsetI elim: UnionE dest: subsetD)
3.318 +
3.319 +
3.320 +text {* \medskip General union. *}
3.321 +
3.322 +lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
3.323 + by blast
3.324 +
3.325 +lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
3.326 + by (rules intro: subsetI elim: UN_E dest: subsetD)
3.327 +
3.328 +
3.329 +text {* \medskip Big Intersection -- greatest lower bound of a set. *}
3.330 +
3.331 +lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
3.332 + by blast
3.333 +
3.334 +lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
3.335 + by (rules intro: InterI subsetI dest: subsetD)
3.336 +
3.337 +lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
3.338 + by blast
3.339 +
3.340 +lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
3.341 + by (rules intro: INT_I subsetI dest: subsetD)
3.342 +
3.343 +
3.344 +text {* \medskip Finite Union -- the least upper bound of two sets. *}
3.345 +
3.346 +lemma Un_upper1: "A \<subseteq> A \<union> B"
3.347 + by blast
3.348 +
3.349 +lemma Un_upper2: "B \<subseteq> A \<union> B"
3.350 + by blast
3.351 +
3.352 +lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
3.353 + by blast
3.354 +
3.355 +
3.356 +text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
3.357 +
3.358 +lemma Int_lower1: "A \<inter> B \<subseteq> A"
3.359 + by blast
3.360 +
3.361 +lemma Int_lower2: "A \<inter> B \<subseteq> B"
3.362 + by blast
3.363 +
3.364 +lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
3.365 + by blast
3.366 +
3.367 +
3.368 +text {* \medskip Set difference. *}
3.369 +
3.370 +lemma Diff_subset: "A - B \<subseteq> A"
3.371 + by blast
3.372 +
3.373 +
3.374 +text {* \medskip Monotonicity. *}
3.375 +
3.376 +lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
3.377 + apply (rule Un_least)
3.378 + apply (erule Un_upper1 [THEN [2] monoD])
3.379 + apply (erule Un_upper2 [THEN [2] monoD])
3.380 + done
3.381 +
3.382 +lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
3.383 + apply (rule Int_greatest)
3.384 + apply (erule Int_lower1 [THEN [2] monoD])
3.385 + apply (erule Int_lower2 [THEN [2] monoD])
3.386 + done
3.387 +
3.388 +
3.389 +subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
3.390 +
3.391 +text {* @{text "{}"}. *}
3.392 +
3.393 +lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
3.394 + -- {* supersedes @{text "Collect_False_empty"} *}
3.395 + by auto
3.396 +
3.397 +lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
3.398 + by blast
3.399 +
3.400 +lemma not_psubset_empty [iff]: "\<not> (A < {})"
3.401 + by (unfold psubset_def) blast
3.402 +
3.403 +lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
3.404 + by auto
3.405 +
3.406 +lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
3.407 + by blast
3.408 +
3.409 +lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
3.410 + by blast
3.411 +
3.412 +lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
3.413 + by blast
3.414 +
3.415 +lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
3.416 + by blast
3.417 +
3.418 +lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
3.419 + by blast
3.420 +
3.421 +lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
3.422 + by blast
3.423 +
3.424 +lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
3.425 + by blast
3.426 +
3.427 +
3.428 +text {* \medskip @{text insert}. *}
3.429 +
3.430 +lemma insert_is_Un: "insert a A = {a} Un A"
3.431 + -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
3.432 + by blast
3.433 +
3.434 +lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
3.435 + by blast
3.436 +
3.437 +lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard]
3.438 +
3.439 +lemma insert_absorb: "a \<in> A ==> insert a A = A"
3.440 + -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
3.441 + -- {* with \emph{quadratic} running time *}
3.442 + by blast
3.443 +
3.444 +lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
3.445 + by blast
3.446 +
3.447 +lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
3.448 + by blast
3.449 +
3.450 +lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
3.451 + by blast
3.452 +
3.453 +lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
3.454 + -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
3.455 + apply (rule_tac x = "A - {a}" in exI)
3.456 apply blast
3.457 done
3.458
3.459 -lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)"
3.460 - by (simp only: psubset_def)
3.461 -
3.462 -lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B"
3.463 - by (simp add: psubset_eq)
3.464 -
3.465 -lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C"
3.466 - by (auto simp add: psubset_eq)
3.467 -
3.468 -lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C"
3.469 - by (auto simp add: psubset_eq)
3.470 -
3.471 -lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)"
3.472 +lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
3.473 + by auto
3.474 +
3.475 +lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
3.476 + by blast
3.477 +
3.478 +
3.479 +text {* \medskip @{text image}. *}
3.480 +
3.481 +lemma image_empty [simp]: "f`{} = {}"
3.482 + by blast
3.483 +
3.484 +lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
3.485 + by blast
3.486 +
3.487 +lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
3.488 + by blast
3.489 +
3.490 +lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
3.491 + by blast
3.492 +
3.493 +lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
3.494 + by blast
3.495 +
3.496 +lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
3.497 + by blast
3.498 +
3.499 +lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
3.500 + -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *}
3.501 + -- {* with its implicit quantifier and conjunction. Also image enjoys better *}
3.502 + -- {* equational properties than does the RHS. *}
3.503 + by blast
3.504 +
3.505 +lemma if_image_distrib [simp]:
3.506 + "(\<lambda>x. if P x then f x else g x) ` S
3.507 + = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
3.508 + by (auto simp add: image_def)
3.509 +
3.510 +lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
3.511 + by (simp add: image_def)
3.512 +
3.513 +
3.514 +text {* \medskip @{text range}. *}
3.515 +
3.516 +lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
3.517 + by auto
3.518 +
3.519 +lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
3.520 + apply (subst image_image)
3.521 + apply simp
3.522 + done
3.523 +
3.524 +
3.525 +text {* \medskip @{text Int} *}
3.526 +
3.527 +lemma Int_absorb [simp]: "A \<inter> A = A"
3.528 + by blast
3.529 +
3.530 +lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
3.531 + by blast
3.532 +
3.533 +lemma Int_commute: "A \<inter> B = B \<inter> A"
3.534 + by blast
3.535 +
3.536 +lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
3.537 + by blast
3.538 +
3.539 +lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
3.540 + by blast
3.541 +
3.542 +lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
3.543 + -- {* Intersection is an AC-operator *}
3.544 +
3.545 +lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
3.546 + by blast
3.547 +
3.548 +lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
3.549 + by blast
3.550 +
3.551 +lemma Int_empty_left [simp]: "{} \<inter> B = {}"
3.552 + by blast
3.553 +
3.554 +lemma Int_empty_right [simp]: "A \<inter> {} = {}"
3.555 + by blast
3.556 +
3.557 +lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
3.558 + by blast
3.559 +
3.560 +lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
3.561 + by blast
3.562 +
3.563 +lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
3.564 + by blast
3.565 +
3.566 +lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
3.567 + by blast
3.568 +
3.569 +lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
3.570 + by blast
3.571 +
3.572 +lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
3.573 + by blast
3.574 +
3.575 +lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
3.576 + by blast
3.577 +
3.578 +lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
3.579 + by blast
3.580 +
3.581 +lemma Int_subset_iff: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
3.582 + by blast
3.583 +
3.584 +lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
3.585 + by blast
3.586 +
3.587 +
3.588 +text {* \medskip @{text Un}. *}
3.589 +
3.590 +lemma Un_absorb [simp]: "A \<union> A = A"
3.591 + by blast
3.592 +
3.593 +lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
3.594 + by blast
3.595 +
3.596 +lemma Un_commute: "A \<union> B = B \<union> A"
3.597 + by blast
3.598 +
3.599 +lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
3.600 + by blast
3.601 +
3.602 +lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
3.603 + by blast
3.604 +
3.605 +lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
3.606 + -- {* Union is an AC-operator *}
3.607 +
3.608 +lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
3.609 + by blast
3.610 +
3.611 +lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
3.612 + by blast
3.613 +
3.614 +lemma Un_empty_left [simp]: "{} \<union> B = B"
3.615 + by blast
3.616 +
3.617 +lemma Un_empty_right [simp]: "A \<union> {} = A"
3.618 + by blast
3.619 +
3.620 +lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
3.621 + by blast
3.622 +
3.623 +lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
3.624 + by blast
3.625 +
3.626 +lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
3.627 + by blast
3.628 +
3.629 +lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
3.630 + by blast
3.631 +
3.632 +lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
3.633 + by blast
3.634 +
3.635 +lemma Int_insert_left:
3.636 + "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
3.637 + by auto
3.638 +
3.639 +lemma Int_insert_right:
3.640 + "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
3.641 + by auto
3.642 +
3.643 +lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
3.644 + by blast
3.645 +
3.646 +lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
3.647 + by blast
3.648 +
3.649 +lemma Un_Int_crazy:
3.650 + "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
3.651 + by blast
3.652 +
3.653 +lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
3.654 + by blast
3.655 +
3.656 +lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
3.657 + by blast
3.658 +
3.659 +lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
3.660 + by blast
3.661 +
3.662 +lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
3.663 + by blast
3.664 +
3.665 +
3.666 +text {* \medskip Set complement *}
3.667 +
3.668 +lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
3.669 + by blast
3.670 +
3.671 +lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
3.672 + by blast
3.673 +
3.674 +lemma Compl_partition: "A \<union> (-A) = UNIV"
3.675 + by blast
3.676 +
3.677 +lemma double_complement [simp]: "- (-A) = (A::'a set)"
3.678 + by blast
3.679 +
3.680 +lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
3.681 + by blast
3.682 +
3.683 +lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
3.684 + by blast
3.685 +
3.686 +lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
3.687 + by blast
3.688 +
3.689 +lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
3.690 + by blast
3.691 +
3.692 +lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
3.693 + by blast
3.694 +
3.695 +lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
3.696 + -- {* Halmos, Naive Set Theory, page 16. *}
3.697 + by blast
3.698 +
3.699 +lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
3.700 + by blast
3.701 +
3.702 +lemma Compl_empty_eq [simp]: "-{} = UNIV"
3.703 + by blast
3.704 +
3.705 +lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
3.706 + by blast
3.707 +
3.708 +lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
3.709 + by blast
3.710 +
3.711 +
3.712 +text {* \medskip @{text Union}. *}
3.713 +
3.714 +lemma Union_empty [simp]: "Union({}) = {}"
3.715 + by blast
3.716 +
3.717 +lemma Union_UNIV [simp]: "Union UNIV = UNIV"
3.718 + by blast
3.719 +
3.720 +lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
3.721 + by blast
3.722 +
3.723 +lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
3.724 + by blast
3.725 +
3.726 +lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
3.727 + by blast
3.728 +
3.729 +lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
3.730 + by auto
3.731 +
3.732 +lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
3.733 + by blast
3.734 +
3.735 +
3.736 +text {* \medskip @{text Inter}. *}
3.737 +
3.738 +lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
3.739 + by blast
3.740 +
3.741 +lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
3.742 + by blast
3.743 +
3.744 +lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
3.745 + by blast
3.746 +
3.747 +lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
3.748 + by blast
3.749 +
3.750 +lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
3.751 + by blast
3.752 +
3.753 +
3.754 +text {*
3.755 + \medskip @{text UN} and @{text INT}.
3.756 +
3.757 + Basic identities: *}
3.758 +
3.759 +lemma UN_empty [simp]: "(\<Union>x\<in>{}. B x) = {}"
3.760 + by blast
3.761 +
3.762 +lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
3.763 + by blast
3.764 +
3.765 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
3.766 + by blast
3.767 +
3.768 +lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
3.769 + by blast
3.770 +
3.771 +lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
3.772 + by blast
3.773 +
3.774 +lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
3.775 + by blast
3.776 +
3.777 +lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
3.778 + by blast
3.779 +
3.780 +lemma UN_Un: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
3.781 + by blast
3.782 +
3.783 +lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
3.784 + by blast
3.785 +
3.786 +lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
3.787 + by blast
3.788 +
3.789 +lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
3.790 + by blast
3.791 +
3.792 +lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
3.793 + by blast
3.794 +
3.795 +lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
3.796 + by blast
3.797 +
3.798 +lemma INT_insert_distrib:
3.799 + "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
3.800 + by blast
3.801 +
3.802 +lemma Union_image_eq [simp]: "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
3.803 + by blast
3.804 +
3.805 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
3.806 + by blast
3.807 +
3.808 +lemma Inter_image_eq [simp]: "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
3.809 + by blast
3.810 +
3.811 +lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
3.812 + by auto
3.813 +
3.814 +lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
3.815 + by auto
3.816 +
3.817 +lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
3.818 + by blast
3.819 +
3.820 +lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
3.821 + -- {* Look: it has an \emph{existential} quantifier *}
3.822 + by blast
3.823 +
3.824 +lemma UN_empty3 [iff]: "(UNION A B = {}) = (\<forall>x\<in>A. B x = {})"
3.825 + by auto
3.826 +
3.827 +
3.828 +text {* \medskip Distributive laws: *}
3.829 +
3.830 +lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
3.831 + by blast
3.832 +
3.833 +lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
3.834 + by blast
3.835 +
3.836 +lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A`C) \<union> \<Union>(B`C)"
3.837 + -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
3.838 + -- {* Union of a family of unions *}
3.839 + by blast
3.840 +
3.841 +lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
3.842 + -- {* Equivalent version *}
3.843 + by blast
3.844 +
3.845 +lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
3.846 + by blast
3.847 +
3.848 +lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A`C) \<inter> \<Inter>(B`C)"
3.849 + by blast
3.850 +
3.851 +lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
3.852 + -- {* Equivalent version *}
3.853 + by blast
3.854 +
3.855 +lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
3.856 + -- {* Halmos, Naive Set Theory, page 35. *}
3.857 + by blast
3.858 +
3.859 +lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
3.860 + by blast
3.861 +
3.862 +lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"
3.863 + by blast
3.864 +
3.865 +lemma Un_INT_distrib2: "(\<Inter>i\<in>I. A i) \<union> (\<Inter>j\<in>J. B j) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A i \<union> B j)"
3.866 + by blast
3.867 +
3.868 +
3.869 +text {* \medskip Bounded quantifiers.
3.870 +
3.871 + The following are not added to the default simpset because
3.872 + (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
3.873 +
3.874 +lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
3.875 + by blast
3.876 +
3.877 +lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"
3.878 + by blast
3.879 +
3.880 +lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
3.881 + by blast
3.882 +
3.883 +lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
3.884 + by blast
3.885 +
3.886 +
3.887 +text {* \medskip Set difference. *}
3.888 +
3.889 +lemma Diff_eq: "A - B = A \<inter> (-B)"
3.890 + by blast
3.891 +
3.892 +lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
3.893 + by blast
3.894 +
3.895 +lemma Diff_cancel [simp]: "A - A = {}"
3.896 + by blast
3.897 +
3.898 +lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
3.899 + by (blast elim: equalityE)
3.900 +
3.901 +lemma empty_Diff [simp]: "{} - A = {}"
3.902 + by blast
3.903 +
3.904 +lemma Diff_empty [simp]: "A - {} = A"
3.905 + by blast
3.906 +
3.907 +lemma Diff_UNIV [simp]: "A - UNIV = {}"
3.908 + by blast
3.909 +
3.910 +lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
3.911 + by blast
3.912 +
3.913 +lemma Diff_insert: "A - insert a B = A - B - {a}"
3.914 + -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
3.915 + by blast
3.916 +
3.917 +lemma Diff_insert2: "A - insert a B = A - {a} - B"
3.918 + -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
3.919 + by blast
3.920 +
3.921 +lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
3.922 + by auto
3.923 +
3.924 +lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
3.925 + by blast
3.926 +
3.927 +lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
3.928 + by blast
3.929 +
3.930 +lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"
3.931 + by auto
3.932 +
3.933 +lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
3.934 + by blast
3.935 +
3.936 +lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"
3.937 + by blast
3.938 +
3.939 +lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"
3.940 + by blast
3.941 +
3.942 +lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
3.943 + by blast
3.944 +
3.945 +lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
3.946 + by blast
3.947 +
3.948 +lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
3.949 + by blast
3.950 +
3.951 +lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
3.952 + by blast
3.953 +
3.954 +lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
3.955 + by blast
3.956 +
3.957 +lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
3.958 + by blast
3.959 +
3.960 +lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
3.961 + by blast
3.962 +
3.963 +lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
3.964 + by blast
3.965 +
3.966 +lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
3.967 + by auto
3.968 +
3.969 +lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
3.970 + by blast
3.971 +
3.972 +
3.973 +text {* \medskip Quantification over type @{typ bool}. *}
3.974 +
3.975 +lemma all_bool_eq: "(\<forall>b::bool. P b) = (P True & P False)"
3.976 + apply auto
3.977 + apply (tactic {* case_tac "b" 1 *})
3.978 + apply auto
3.979 + done
3.980 +
3.981 +lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
3.982 + by (rule conjI [THEN all_bool_eq [THEN iffD2], THEN spec])
3.983 +
3.984 +lemma ex_bool_eq: "(\<exists>b::bool. P b) = (P True | P False)"
3.985 + apply auto
3.986 + apply (tactic {* case_tac "b" 1 *})
3.987 + apply auto
3.988 + done
3.989 +
3.990 +lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
3.991 + by (auto simp add: split_if_mem2)
3.992 +
3.993 +lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
3.994 + apply auto
3.995 + apply (tactic {* case_tac "b" 1 *})
3.996 + apply auto
3.997 + done
3.998 +
3.999 +lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
3.1000 + apply auto
3.1001 + apply (tactic {* case_tac "b" 1 *})
3.1002 + apply auto
3.1003 + done
3.1004 +
3.1005 +
3.1006 +text {* \medskip @{text Pow} *}
3.1007 +
3.1008 +lemma Pow_empty [simp]: "Pow {} = {{}}"
3.1009 + by (auto simp add: Pow_def)
3.1010 +
3.1011 +lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
3.1012 + by (blast intro: image_eqI [where ?x = "u - {a}", standard])
3.1013 +
3.1014 +lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
3.1015 + by (blast intro: exI [where ?x = "- u", standard])
3.1016 +
3.1017 +lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
3.1018 + by blast
3.1019 +
3.1020 +lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
3.1021 + by blast
3.1022 +
3.1023 +lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
3.1024 + by blast
3.1025 +
3.1026 +lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
3.1027 + by blast
3.1028 +
3.1029 +lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
3.1030 + by blast
3.1031 +
3.1032 +lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
3.1033 + by blast
3.1034 +
3.1035 +lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
3.1036 + by blast
3.1037 +
3.1038 +
3.1039 +text {* \medskip Miscellany. *}
3.1040 +
3.1041 +lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
3.1042 + by blast
3.1043 +
3.1044 +lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
3.1045 + by blast
3.1046 +
3.1047 +lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
3.1048 by (unfold psubset_def) blast
3.1049
3.1050 -lemma atomize_ball:
3.1051 - "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)"
3.1052 - by (simp only: Ball_def atomize_all atomize_imp)
3.1053 -
3.1054 -declare atomize_ball [symmetric, rulify]
3.1055 -
3.1056 -
3.1057 -subsection {* Further set-theory lemmas *}
3.1058 -
3.1059 -use "subset.ML"
3.1060 -use "equalities.ML"
3.1061 -use "mono.ML"
3.1062 +lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
3.1063 + by blast
3.1064 +
3.1065 +lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
3.1066 + by rules
3.1067 +
3.1068 +
3.1069 +text {* \medskip Miniscoping: pushing in big Unions and Intersections. *}
3.1070 +
3.1071 +lemma UN_simps [simp]:
3.1072 + "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"
3.1073 + "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))"
3.1074 + "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))"
3.1075 + "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)"
3.1076 + "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))"
3.1077 + "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)"
3.1078 + "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))"
3.1079 + "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"
3.1080 + "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)"
3.1081 + "!!A B f. (UN x:f`A. B x) = (UN a:A. B (f a))"
3.1082 + by auto
3.1083 +
3.1084 +lemma INT_simps [simp]:
3.1085 + "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"
3.1086 + "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"
3.1087 + "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)"
3.1088 + "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))"
3.1089 + "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"
3.1090 + "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)"
3.1091 + "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))"
3.1092 + "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"
3.1093 + "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"
3.1094 + "!!A B f. (INT x:f`A. B x) = (INT a:A. B (f a))"
3.1095 + by auto
3.1096 +
3.1097 +lemma ball_simps [simp]:
3.1098 + "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
3.1099 + "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
3.1100 + "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
3.1101 + "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"
3.1102 + "!!P. (ALL x:{}. P x) = True"
3.1103 + "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"
3.1104 + "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"
3.1105 + "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"
3.1106 + "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"
3.1107 + "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"
3.1108 + "!!A P f. (ALL x:f`A. P x) = (ALL x:A. P (f x))"
3.1109 + "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
3.1110 + by auto
3.1111 +
3.1112 +lemma bex_simps [simp]:
3.1113 + "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
3.1114 + "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
3.1115 + "!!P. (EX x:{}. P x) = False"
3.1116 + "!!P. (EX x:UNIV. P x) = (EX x. P x)"
3.1117 + "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"
3.1118 + "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"
3.1119 + "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"
3.1120 + "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"
3.1121 + "!!A P f. (EX x:f`A. P x) = (EX x:A. P (f x))"
3.1122 + "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"
3.1123 + by auto
3.1124 +
3.1125 +lemma ball_conj_distrib:
3.1126 + "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"
3.1127 + by blast
3.1128 +
3.1129 +lemma bex_disj_distrib:
3.1130 + "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"
3.1131 + by blast
3.1132 +
3.1133 +
3.1134 +subsubsection {* Monotonicity of various operations *}
3.1135 +
3.1136 +lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
3.1137 + by blast
3.1138 +
3.1139 +lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"
3.1140 + by blast
3.1141 +
3.1142 +lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
3.1143 + by blast
3.1144 +
3.1145 +lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
3.1146 + by blast
3.1147 +
3.1148 +lemma UN_mono:
3.1149 + "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
3.1150 + (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
3.1151 + by (blast dest: subsetD)
3.1152 +
3.1153 +lemma INT_anti_mono:
3.1154 + "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
3.1155 + (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
3.1156 + -- {* The last inclusion is POSITIVE! *}
3.1157 + by (blast dest: subsetD)
3.1158 +
3.1159 +lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"
3.1160 + by blast
3.1161 +
3.1162 +lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
3.1163 + by blast
3.1164 +
3.1165 +lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
3.1166 + by blast
3.1167 +
3.1168 +lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
3.1169 + by blast
3.1170 +
3.1171 +lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
3.1172 + by blast
3.1173 +
3.1174 +text {* \medskip Monotonicity of implications. *}
3.1175 +
3.1176 +lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
3.1177 + apply (rule impI)
3.1178 + apply (erule subsetD)
3.1179 + apply assumption
3.1180 + done
3.1181 +
3.1182 +lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
3.1183 + by rules
3.1184 +
3.1185 +lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
3.1186 + by rules
3.1187 +
3.1188 +lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
3.1189 + by rules
3.1190 +
3.1191 +lemma imp_refl: "P --> P" ..
3.1192 +
3.1193 +lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
3.1194 + by rules
3.1195 +
3.1196 +lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
3.1197 + by rules
3.1198 +
3.1199 +lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
3.1200 + by blast
3.1201 +
3.1202 +lemma Int_Collect_mono:
3.1203 + "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
3.1204 + by blast
3.1205 +
3.1206 +lemmas basic_monos =
3.1207 + subset_refl imp_refl disj_mono conj_mono
3.1208 + ex_mono Collect_mono in_mono
3.1209 +
3.1210 +lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
3.1211 + by rules
3.1212 +
3.1213 +lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
3.1214 + by rules
3.1215
3.1216 lemma Least_mono:
3.1217 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
3.1218 @@ -972,7 +1858,7 @@
3.1219 -- {* NOT suitable for rewriting *}
3.1220 by blast
3.1221
3.1222 -lemma vimage_mono: "A <= B ==> f -` A <= f -` B"
3.1223 +lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
3.1224 -- {* monotonicity *}
3.1225 by blast
3.1226
3.1227 @@ -985,10 +1871,10 @@
3.1228 lemma back_subst: "P a ==> a = b ==> P b"
3.1229 by (rule subst)
3.1230
3.1231 -lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
3.1232 +lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
3.1233 by (rule subsetD)
3.1234
3.1235 -lemma set_mp: "A <= B ==> x:A ==> x:B"
3.1236 +lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
3.1237 by (rule subsetD)
3.1238
3.1239 lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
4.1 --- a/src/HOL/equalities.ML Fri Feb 15 20:43:44 2002 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,982 +0,0 @@
4.4 -(* Title: HOL/equalities.ML
4.5 - ID: $Id$
4.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4.7 - Copyright 1994 University of Cambridge
4.8 -
4.9 -Equalities involving union, intersection, inclusion, etc.
4.10 -*)
4.11 -
4.12 -AddSIs [equalityI];
4.13 -
4.14 -section "{}";
4.15 -
4.16 -(*supersedes Collect_False_empty*)
4.17 -Goal "{s. P} = (if P then UNIV else {})";
4.18 -by (Force_tac 1);
4.19 -qed "Collect_const";
4.20 -Addsimps [Collect_const];
4.21 -
4.22 -Goal "(A <= {}) = (A = {})";
4.23 -by (Blast_tac 1);
4.24 -qed "subset_empty";
4.25 -Addsimps[subset_empty];
4.26 -
4.27 -Goalw [psubset_def] "~ (A < {})";
4.28 -by (Blast_tac 1);
4.29 -qed "not_psubset_empty";
4.30 -AddIffs [not_psubset_empty];
4.31 -
4.32 -Goal "(Collect P = {}) = (ALL x. ~ P x)";
4.33 -by Auto_tac;
4.34 -qed "Collect_empty_eq";
4.35 -Addsimps[Collect_empty_eq];
4.36 -
4.37 -Goal "{x. ~ (P x)} = - {x. P x}";
4.38 -by (Blast_tac 1);
4.39 -qed "Collect_neg_eq";
4.40 -
4.41 -Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";
4.42 -by (Blast_tac 1);
4.43 -qed "Collect_disj_eq";
4.44 -
4.45 -Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}";
4.46 -by (Blast_tac 1);
4.47 -qed "Collect_conj_eq";
4.48 -
4.49 -Goal "{x. ALL y. P x y} = (INT y. {x. P x y})";
4.50 -by (Blast_tac 1);
4.51 -qed "Collect_all_eq";
4.52 -
4.53 -Goal "{x. ALL y: A. P x y} = (INT y: A. {x. P x y})";
4.54 -by (Blast_tac 1);
4.55 -qed "Collect_ball_eq";
4.56 -
4.57 -Goal "{x. EX y. P x y} = (UN y. {x. P x y})";
4.58 -by (Blast_tac 1);
4.59 -qed "Collect_ex_eq";
4.60 -
4.61 -Goal "{x. EX y: A. P x y} = (UN y: A. {x. P x y})";
4.62 -by (Blast_tac 1);
4.63 -qed "Collect_bex_eq";
4.64 -
4.65 -
4.66 -section "insert";
4.67 -
4.68 -(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
4.69 -Goal "insert a A = {a} Un A";
4.70 -by (Blast_tac 1);
4.71 -qed "insert_is_Un";
4.72 -
4.73 -Goal "insert a A ~= {}";
4.74 -by (Blast_tac 1);
4.75 -qed"insert_not_empty";
4.76 -Addsimps[insert_not_empty];
4.77 -
4.78 -bind_thm("empty_not_insert",insert_not_empty RS not_sym);
4.79 -Addsimps[empty_not_insert];
4.80 -
4.81 -Goal "a:A ==> insert a A = A";
4.82 -by (Blast_tac 1);
4.83 -qed "insert_absorb";
4.84 -(* Addsimps [insert_absorb] causes recursive calls
4.85 - when there are nested inserts, with QUADRATIC running time
4.86 -*)
4.87 -
4.88 -Goal "insert x (insert x A) = insert x A";
4.89 -by (Blast_tac 1);
4.90 -qed "insert_absorb2";
4.91 -Addsimps [insert_absorb2];
4.92 -
4.93 -Goal "insert x (insert y A) = insert y (insert x A)";
4.94 -by (Blast_tac 1);
4.95 -qed "insert_commute";
4.96 -
4.97 -Goal "(insert x A <= B) = (x:B & A <= B)";
4.98 -by (Blast_tac 1);
4.99 -qed "insert_subset";
4.100 -Addsimps[insert_subset];
4.101 -
4.102 -(* use new B rather than (A-{a}) to avoid infinite unfolding *)
4.103 -Goal "a:A ==> EX B. A = insert a B & a ~: B";
4.104 -by (res_inst_tac [("x","A-{a}")] exI 1);
4.105 -by (Blast_tac 1);
4.106 -qed "mk_disjoint_insert";
4.107 -
4.108 -Goal "insert a (Collect P) = {u. u ~= a --> P u}";
4.109 -by Auto_tac;
4.110 -qed "insert_Collect";
4.111 -
4.112 -Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
4.113 -by (Blast_tac 1);
4.114 -qed "UN_insert_distrib";
4.115 -
4.116 -section "`";
4.117 -
4.118 -Goal "f`{} = {}";
4.119 -by (Blast_tac 1);
4.120 -qed "image_empty";
4.121 -Addsimps[image_empty];
4.122 -
4.123 -Goal "f`insert a B = insert (f a) (f`B)";
4.124 -by (Blast_tac 1);
4.125 -qed "image_insert";
4.126 -Addsimps[image_insert];
4.127 -
4.128 -Goal "x:A ==> (%x. c) ` A = {c}";
4.129 -by (Blast_tac 1);
4.130 -qed "image_constant";
4.131 -
4.132 -Goal "f`(g`A) = (%x. f (g x)) ` A";
4.133 -by (Blast_tac 1);
4.134 -qed "image_image";
4.135 -
4.136 -Goal "x:A ==> insert (f x) (f`A) = f`A";
4.137 -by (Blast_tac 1);
4.138 -qed "insert_image";
4.139 -Addsimps [insert_image];
4.140 -
4.141 -Goal "(f`A = {}) = (A = {})";
4.142 -by (Blast_tac 1);
4.143 -qed "image_is_empty";
4.144 -AddIffs [image_is_empty];
4.145 -
4.146 -(*NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
4.147 - with its implicit quantifier and conjunction. Also image enjoys better
4.148 - equational properties than does the RHS.*)
4.149 -Goal "f ` {x. P x} = {f x | x. P x}";
4.150 -by (Blast_tac 1);
4.151 -qed "image_Collect";
4.152 -
4.153 -Goalw [image_def] "(%x. if P x then f x else g x) ` S \
4.154 -\ = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";
4.155 -by (Simp_tac 1);
4.156 -by (Blast_tac 1);
4.157 -qed "if_image_distrib";
4.158 -Addsimps[if_image_distrib];
4.159 -
4.160 -val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f`M = g`N";
4.161 -by (simp_tac (simpset() addsimps image_def::prems) 1);
4.162 -qed "image_cong";
4.163 -
4.164 -
4.165 -section "range";
4.166 -
4.167 -Goal "{u. EX x. u = f x} = range f";
4.168 -by Auto_tac;
4.169 -qed "full_SetCompr_eq";
4.170 -
4.171 -Goal "range (%x. f (g x)) = f`range g";
4.172 -by (stac image_image 1);
4.173 -by (Simp_tac 1);
4.174 -qed "range_composition";
4.175 -Addsimps[range_composition];
4.176 -
4.177 -section "Int";
4.178 -
4.179 -Goal "A Int A = A";
4.180 -by (Blast_tac 1);
4.181 -qed "Int_absorb";
4.182 -Addsimps[Int_absorb];
4.183 -
4.184 -Goal "A Int (A Int B) = A Int B";
4.185 -by (Blast_tac 1);
4.186 -qed "Int_left_absorb";
4.187 -
4.188 -Goal "A Int B = B Int A";
4.189 -by (Blast_tac 1);
4.190 -qed "Int_commute";
4.191 -
4.192 -Goal "A Int (B Int C) = B Int (A Int C)";
4.193 -by (Blast_tac 1);
4.194 -qed "Int_left_commute";
4.195 -
4.196 -Goal "(A Int B) Int C = A Int (B Int C)";
4.197 -by (Blast_tac 1);
4.198 -qed "Int_assoc";
4.199 -
4.200 -(*Intersection is an AC-operator*)
4.201 -bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]);
4.202 -
4.203 -Goal "B<=A ==> A Int B = B";
4.204 -by (Blast_tac 1);
4.205 -qed "Int_absorb1";
4.206 -
4.207 -Goal "A<=B ==> A Int B = A";
4.208 -by (Blast_tac 1);
4.209 -qed "Int_absorb2";
4.210 -
4.211 -Goal "{} Int B = {}";
4.212 -by (Blast_tac 1);
4.213 -qed "Int_empty_left";
4.214 -Addsimps[Int_empty_left];
4.215 -
4.216 -Goal "A Int {} = {}";
4.217 -by (Blast_tac 1);
4.218 -qed "Int_empty_right";
4.219 -Addsimps[Int_empty_right];
4.220 -
4.221 -Goal "(A Int B = {}) = (A <= -B)";
4.222 -by (Blast_tac 1);
4.223 -qed "disjoint_eq_subset_Compl";
4.224 -
4.225 -Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
4.226 -by (Blast_tac 1);
4.227 -qed "disjoint_iff_not_equal";
4.228 -
4.229 -Goal "UNIV Int B = B";
4.230 -by (Blast_tac 1);
4.231 -qed "Int_UNIV_left";
4.232 -Addsimps[Int_UNIV_left];
4.233 -
4.234 -Goal "A Int UNIV = A";
4.235 -by (Blast_tac 1);
4.236 -qed "Int_UNIV_right";
4.237 -Addsimps[Int_UNIV_right];
4.238 -
4.239 -Goal "A Int B = Inter{A,B}";
4.240 -by (Blast_tac 1);
4.241 -qed "Int_eq_Inter";
4.242 -
4.243 -Goal "A Int (B Un C) = (A Int B) Un (A Int C)";
4.244 -by (Blast_tac 1);
4.245 -qed "Int_Un_distrib";
4.246 -
4.247 -Goal "(B Un C) Int A = (B Int A) Un (C Int A)";
4.248 -by (Blast_tac 1);
4.249 -qed "Int_Un_distrib2";
4.250 -
4.251 -Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
4.252 -by (Blast_tac 1);
4.253 -qed "Int_UNIV";
4.254 -Addsimps[Int_UNIV];
4.255 -
4.256 -Goal "(C <= A Int B) = (C <= A & C <= B)";
4.257 -by (Blast_tac 1);
4.258 -qed "Int_subset_iff";
4.259 -
4.260 -Goal "(x : A Int {x. P x}) = (x : A & P x)";
4.261 -by (Blast_tac 1);
4.262 -qed "Int_Collect";
4.263 -
4.264 -section "Un";
4.265 -
4.266 -Goal "A Un A = A";
4.267 -by (Blast_tac 1);
4.268 -qed "Un_absorb";
4.269 -Addsimps[Un_absorb];
4.270 -
4.271 -Goal "A Un (A Un B) = A Un B";
4.272 -by (Blast_tac 1);
4.273 -qed "Un_left_absorb";
4.274 -
4.275 -Goal "A Un B = B Un A";
4.276 -by (Blast_tac 1);
4.277 -qed "Un_commute";
4.278 -
4.279 -Goal "A Un (B Un C) = B Un (A Un C)";
4.280 -by (Blast_tac 1);
4.281 -qed "Un_left_commute";
4.282 -
4.283 -Goal "(A Un B) Un C = A Un (B Un C)";
4.284 -by (Blast_tac 1);
4.285 -qed "Un_assoc";
4.286 -
4.287 -(*Union is an AC-operator*)
4.288 -bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]);
4.289 -
4.290 -Goal "A<=B ==> A Un B = B";
4.291 -by (Blast_tac 1);
4.292 -qed "Un_absorb1";
4.293 -
4.294 -Goal "B<=A ==> A Un B = A";
4.295 -by (Blast_tac 1);
4.296 -qed "Un_absorb2";
4.297 -
4.298 -Goal "{} Un B = B";
4.299 -by (Blast_tac 1);
4.300 -qed "Un_empty_left";
4.301 -Addsimps[Un_empty_left];
4.302 -
4.303 -Goal "A Un {} = A";
4.304 -by (Blast_tac 1);
4.305 -qed "Un_empty_right";
4.306 -Addsimps[Un_empty_right];
4.307 -
4.308 -Goal "UNIV Un B = UNIV";
4.309 -by (Blast_tac 1);
4.310 -qed "Un_UNIV_left";
4.311 -Addsimps[Un_UNIV_left];
4.312 -
4.313 -Goal "A Un UNIV = UNIV";
4.314 -by (Blast_tac 1);
4.315 -qed "Un_UNIV_right";
4.316 -Addsimps[Un_UNIV_right];
4.317 -
4.318 -Goal "A Un B = Union{A,B}";
4.319 -by (Blast_tac 1);
4.320 -qed "Un_eq_Union";
4.321 -
4.322 -Goal "(insert a B) Un C = insert a (B Un C)";
4.323 -by (Blast_tac 1);
4.324 -qed "Un_insert_left";
4.325 -Addsimps[Un_insert_left];
4.326 -
4.327 -Goal "A Un (insert a B) = insert a (A Un B)";
4.328 -by (Blast_tac 1);
4.329 -qed "Un_insert_right";
4.330 -Addsimps[Un_insert_right];
4.331 -
4.332 -Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \
4.333 -\ else B Int C)";
4.334 -by (Simp_tac 1);
4.335 -by (Blast_tac 1);
4.336 -qed "Int_insert_left";
4.337 -
4.338 -Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \
4.339 -\ else A Int B)";
4.340 -by (Simp_tac 1);
4.341 -by (Blast_tac 1);
4.342 -qed "Int_insert_right";
4.343 -
4.344 -Goal "A Un (B Int C) = (A Un B) Int (A Un C)";
4.345 -by (Blast_tac 1);
4.346 -qed "Un_Int_distrib";
4.347 -
4.348 -Goal "(B Int C) Un A = (B Un A) Int (C Un A)";
4.349 -by (Blast_tac 1);
4.350 -qed "Un_Int_distrib2";
4.351 -
4.352 -Goal "(A Int B) Un (B Int C) Un (C Int A) = \
4.353 -\ (A Un B) Int (B Un C) Int (C Un A)";
4.354 -by (Blast_tac 1);
4.355 -qed "Un_Int_crazy";
4.356 -
4.357 -Goal "(A<=B) = (A Un B = B)";
4.358 -by (Blast_tac 1);
4.359 -qed "subset_Un_eq";
4.360 -
4.361 -Goal "(A Un B = {}) = (A = {} & B = {})";
4.362 -by (Blast_tac 1);
4.363 -qed "Un_empty";
4.364 -AddIffs[Un_empty];
4.365 -
4.366 -Goal "(A Un B <= C) = (A <= C & B <= C)";
4.367 -by (Blast_tac 1);
4.368 -qed "Un_subset_iff";
4.369 -
4.370 -Goal "(A - B) Un (A Int B) = A";
4.371 -by (Blast_tac 1);
4.372 -qed "Un_Diff_Int";
4.373 -
4.374 -
4.375 -section "Set complement";
4.376 -
4.377 -Goal "A Int -A = {}";
4.378 -by (Blast_tac 1);
4.379 -qed "Compl_disjoint";
4.380 -
4.381 -Goal "-A Int A = {}";
4.382 -by (Blast_tac 1);
4.383 -qed "Compl_disjoint2";
4.384 -Addsimps[Compl_disjoint, Compl_disjoint2];
4.385 -
4.386 -Goal "A Un (-A) = UNIV";
4.387 -by (Blast_tac 1);
4.388 -qed "Compl_partition";
4.389 -
4.390 -Goal "- (-A) = (A:: 'a set)";
4.391 -by (Blast_tac 1);
4.392 -qed "double_complement";
4.393 -Addsimps[double_complement];
4.394 -
4.395 -Goal "-(A Un B) = (-A) Int (-B)";
4.396 -by (Blast_tac 1);
4.397 -qed "Compl_Un";
4.398 -
4.399 -Goal "-(A Int B) = (-A) Un (-B)";
4.400 -by (Blast_tac 1);
4.401 -qed "Compl_Int";
4.402 -
4.403 -Goal "-(UN x:A. B(x)) = (INT x:A. -B(x))";
4.404 -by (Blast_tac 1);
4.405 -qed "Compl_UN";
4.406 -
4.407 -Goal "-(INT x:A. B(x)) = (UN x:A. -B(x))";
4.408 -by (Blast_tac 1);
4.409 -qed "Compl_INT";
4.410 -
4.411 -Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
4.412 -
4.413 -Goal "(A <= -A) = (A = {})";
4.414 -by (Blast_tac 1);
4.415 -qed "subset_Compl_self_eq";
4.416 -
4.417 -(*Halmos, Naive Set Theory, page 16.*)
4.418 -Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
4.419 -by (Blast_tac 1);
4.420 -qed "Un_Int_assoc_eq";
4.421 -
4.422 -Goal "-UNIV = {}";
4.423 -by (Blast_tac 1);
4.424 -qed "Compl_UNIV_eq";
4.425 -
4.426 -Goal "-{} = UNIV";
4.427 -by (Blast_tac 1);
4.428 -qed "Compl_empty_eq";
4.429 -
4.430 -Addsimps [Compl_UNIV_eq, Compl_empty_eq];
4.431 -
4.432 -Goal "(-A <= -B) = (B <= (A::'a set))";
4.433 -by (Blast_tac 1);
4.434 -qed "Compl_subset_Compl_iff";
4.435 -AddIffs [Compl_subset_Compl_iff];
4.436 -
4.437 -Goal "(-A = -B) = (A = (B::'a set))";
4.438 -by (Blast_tac 1);
4.439 -qed "Compl_eq_Compl_iff";
4.440 -AddIffs [Compl_eq_Compl_iff];
4.441 -
4.442 -
4.443 -section "Union";
4.444 -
4.445 -Goal "Union({}) = {}";
4.446 -by (Blast_tac 1);
4.447 -qed "Union_empty";
4.448 -Addsimps[Union_empty];
4.449 -
4.450 -Goal "Union(UNIV) = UNIV";
4.451 -by (Blast_tac 1);
4.452 -qed "Union_UNIV";
4.453 -Addsimps[Union_UNIV];
4.454 -
4.455 -Goal "Union(insert a B) = a Un Union(B)";
4.456 -by (Blast_tac 1);
4.457 -qed "Union_insert";
4.458 -Addsimps[Union_insert];
4.459 -
4.460 -Goal "Union(A Un B) = Union(A) Un Union(B)";
4.461 -by (Blast_tac 1);
4.462 -qed "Union_Un_distrib";
4.463 -Addsimps[Union_Un_distrib];
4.464 -
4.465 -Goal "Union(A Int B) <= Union(A) Int Union(B)";
4.466 -by (Blast_tac 1);
4.467 -qed "Union_Int_subset";
4.468 -
4.469 -Goal "(Union A = {}) = (ALL x:A. x={})";
4.470 -by Auto_tac;
4.471 -qed "Union_empty_conv";
4.472 -AddIffs [Union_empty_conv];
4.473 -
4.474 -Goal "(Union(C) Int A = {}) = (ALL B:C. B Int A = {})";
4.475 -by (Blast_tac 1);
4.476 -qed "Union_disjoint";
4.477 -
4.478 -section "Inter";
4.479 -
4.480 -Goal "Inter({}) = UNIV";
4.481 -by (Blast_tac 1);
4.482 -qed "Inter_empty";
4.483 -Addsimps[Inter_empty];
4.484 -
4.485 -Goal "Inter(UNIV) = {}";
4.486 -by (Blast_tac 1);
4.487 -qed "Inter_UNIV";
4.488 -Addsimps[Inter_UNIV];
4.489 -
4.490 -Goal "Inter(insert a B) = a Int Inter(B)";
4.491 -by (Blast_tac 1);
4.492 -qed "Inter_insert";
4.493 -Addsimps[Inter_insert];
4.494 -
4.495 -Goal "Inter(A) Un Inter(B) <= Inter(A Int B)";
4.496 -by (Blast_tac 1);
4.497 -qed "Inter_Un_subset";
4.498 -
4.499 -Goal "Inter(A Un B) = Inter(A) Int Inter(B)";
4.500 -by (Blast_tac 1);
4.501 -qed "Inter_Un_distrib";
4.502 -
4.503 -section "UN and INT";
4.504 -
4.505 -(*Basic identities*)
4.506 -
4.507 -Goal "(UN x:{}. B x) = {}";
4.508 -by (Blast_tac 1);
4.509 -qed "UN_empty";
4.510 -Addsimps[UN_empty];
4.511 -
4.512 -Goal "(UN x:A. {}) = {}";
4.513 -by (Blast_tac 1);
4.514 -qed "UN_empty2";
4.515 -Addsimps[UN_empty2];
4.516 -
4.517 -Goal "(UN x:A. {x}) = A";
4.518 -by (Blast_tac 1);
4.519 -qed "UN_singleton";
4.520 -Addsimps [UN_singleton];
4.521 -
4.522 -Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
4.523 -by (Blast_tac 1);
4.524 -qed "UN_absorb";
4.525 -
4.526 -Goal "(INT x:{}. B x) = UNIV";
4.527 -by (Blast_tac 1);
4.528 -qed "INT_empty";
4.529 -Addsimps[INT_empty];
4.530 -
4.531 -Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
4.532 -by (Blast_tac 1);
4.533 -qed "INT_absorb";
4.534 -
4.535 -Goal "(UN x:insert a A. B x) = B a Un UNION A B";
4.536 -by (Blast_tac 1);
4.537 -qed "UN_insert";
4.538 -Addsimps[UN_insert];
4.539 -
4.540 -Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)";
4.541 -by (Blast_tac 1);
4.542 -qed "UN_Un";
4.543 -
4.544 -Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)";
4.545 -by (Blast_tac 1);
4.546 -qed "UN_UN_flatten";
4.547 -
4.548 -Goal "((UN i:I. A i) <= B) = (ALL i:I. A i <= B)";
4.549 -by (Blast_tac 1);
4.550 -qed "UN_subset_iff";
4.551 -
4.552 -Goal "(B <= (INT i:I. A i)) = (ALL i:I. B <= A i)";
4.553 -by (Blast_tac 1);
4.554 -qed "INT_subset_iff";
4.555 -
4.556 -Goal "(INT x:insert a A. B x) = B a Int INTER A B";
4.557 -by (Blast_tac 1);
4.558 -qed "INT_insert";
4.559 -Addsimps[INT_insert];
4.560 -
4.561 -Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)";
4.562 -by (Blast_tac 1);
4.563 -qed "INT_Un";
4.564 -
4.565 -Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
4.566 -by (Blast_tac 1);
4.567 -qed "INT_insert_distrib";
4.568 -
4.569 -Goal "Union(B`A) = (UN x:A. B(x))";
4.570 -by (Blast_tac 1);
4.571 -qed "Union_image_eq";
4.572 -Addsimps [Union_image_eq];
4.573 -
4.574 -Goal "f ` Union S = (UN x:S. f ` x)";
4.575 -by (Blast_tac 1);
4.576 -qed "image_Union";
4.577 -
4.578 -Goal "Inter(B`A) = (INT x:A. B(x))";
4.579 -by (Blast_tac 1);
4.580 -qed "Inter_image_eq";
4.581 -Addsimps [Inter_image_eq];
4.582 -
4.583 -Goal "(UN y:A. c) = (if A={} then {} else c)";
4.584 -by Auto_tac;
4.585 -qed "UN_constant";
4.586 -Addsimps[UN_constant];
4.587 -
4.588 -Goal "(INT y:A. c) = (if A={} then UNIV else c)";
4.589 -by Auto_tac;
4.590 -qed "INT_constant";
4.591 -Addsimps[INT_constant];
4.592 -
4.593 -Goal "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})";
4.594 -by (Blast_tac 1);
4.595 -qed "UN_eq";
4.596 -
4.597 -(*Look: it has an EXISTENTIAL quantifier*)
4.598 -Goal "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})";
4.599 -by (Blast_tac 1);
4.600 -qed "INT_eq";
4.601 -
4.602 -Goal "(UNION A B = {}) = (ALL x:A. B x = {})";
4.603 -by Auto_tac;
4.604 -qed "UN_empty3";
4.605 -AddIffs [UN_empty3];
4.606 -
4.607 -
4.608 -(*Distributive laws...*)
4.609 -
4.610 -Goal "A Int Union(B) = (UN C:B. A Int C)";
4.611 -by (Blast_tac 1);
4.612 -qed "Int_Union";
4.613 -
4.614 -Goal "Union(B) Int A = (UN C:B. C Int A)";
4.615 -by (Blast_tac 1);
4.616 -qed "Int_Union2";
4.617 -
4.618 -(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
4.619 - Union of a family of unions **)
4.620 -Goal "(UN x:C. A(x) Un B(x)) = Union(A`C) Un Union(B`C)";
4.621 -by (Blast_tac 1);
4.622 -qed "Un_Union_image";
4.623 -
4.624 -(*Equivalent version*)
4.625 -Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
4.626 -by (Blast_tac 1);
4.627 -qed "UN_Un_distrib";
4.628 -
4.629 -Goal "A Un Inter(B) = (INT C:B. A Un C)";
4.630 -by (Blast_tac 1);
4.631 -qed "Un_Inter";
4.632 -
4.633 -Goal "(INT x:C. A(x) Int B(x)) = Inter(A`C) Int Inter(B`C)";
4.634 -by (Blast_tac 1);
4.635 -qed "Int_Inter_image";
4.636 -
4.637 -(*Equivalent version*)
4.638 -Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
4.639 -by (Blast_tac 1);
4.640 -qed "INT_Int_distrib";
4.641 -
4.642 -(*Halmos, Naive Set Theory, page 35.*)
4.643 -Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
4.644 -by (Blast_tac 1);
4.645 -qed "Int_UN_distrib";
4.646 -
4.647 -Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
4.648 -by (Blast_tac 1);
4.649 -qed "Un_INT_distrib";
4.650 -
4.651 -Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
4.652 -by (Blast_tac 1);
4.653 -qed "Int_UN_distrib2";
4.654 -
4.655 -Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
4.656 -by (Blast_tac 1);
4.657 -qed "Un_INT_distrib2";
4.658 -
4.659 -
4.660 -section"Bounded quantifiers";
4.661 -
4.662 -(** The following are not added to the default simpset because
4.663 - (a) they duplicate the body and (b) there are no similar rules for Int. **)
4.664 -
4.665 -Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
4.666 -by (Blast_tac 1);
4.667 -qed "ball_Un";
4.668 -
4.669 -Goal "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
4.670 -by (Blast_tac 1);
4.671 -qed "bex_Un";
4.672 -
4.673 -Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)";
4.674 -by (Blast_tac 1);
4.675 -qed "ball_UN";
4.676 -
4.677 -Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)";
4.678 -by (Blast_tac 1);
4.679 -qed "bex_UN";
4.680 -
4.681 -
4.682 -section "-";
4.683 -
4.684 -Goal "A-B = A Int (-B)";
4.685 -by (Blast_tac 1);
4.686 -qed "Diff_eq";
4.687 -
4.688 -Goal "(A-B = {}) = (A<=B)";
4.689 -by (Blast_tac 1);
4.690 -qed "Diff_eq_empty_iff";
4.691 -Addsimps[Diff_eq_empty_iff];
4.692 -
4.693 -Goal "A-A = {}";
4.694 -by (Blast_tac 1);
4.695 -qed "Diff_cancel";
4.696 -Addsimps[Diff_cancel];
4.697 -
4.698 -Goal "A Int B = {} ==> A-B = A";
4.699 -by (blast_tac (claset() addEs [equalityE]) 1);
4.700 -qed "Diff_triv";
4.701 -
4.702 -Goal "{}-A = {}";
4.703 -by (Blast_tac 1);
4.704 -qed "empty_Diff";
4.705 -Addsimps[empty_Diff];
4.706 -
4.707 -Goal "A-{} = A";
4.708 -by (Blast_tac 1);
4.709 -qed "Diff_empty";
4.710 -Addsimps[Diff_empty];
4.711 -
4.712 -Goal "A-UNIV = {}";
4.713 -by (Blast_tac 1);
4.714 -qed "Diff_UNIV";
4.715 -Addsimps[Diff_UNIV];
4.716 -
4.717 -Goal "x~:A ==> A - insert x B = A-B";
4.718 -by (Blast_tac 1);
4.719 -qed "Diff_insert0";
4.720 -Addsimps [Diff_insert0];
4.721 -
4.722 -(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
4.723 -Goal "A - insert a B = A - B - {a}";
4.724 -by (Blast_tac 1);
4.725 -qed "Diff_insert";
4.726 -
4.727 -(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
4.728 -Goal "A - insert a B = A - {a} - B";
4.729 -by (Blast_tac 1);
4.730 -qed "Diff_insert2";
4.731 -
4.732 -Goal "insert x A - B = (if x:B then A-B else insert x (A-B))";
4.733 -by (Simp_tac 1);
4.734 -by (Blast_tac 1);
4.735 -qed "insert_Diff_if";
4.736 -
4.737 -Goal "x:B ==> insert x A - B = A-B";
4.738 -by (Blast_tac 1);
4.739 -qed "insert_Diff1";
4.740 -Addsimps [insert_Diff1];
4.741 -
4.742 -Goal "a:A ==> insert a (A-{a}) = A";
4.743 -by (Blast_tac 1);
4.744 -qed "insert_Diff";
4.745 -
4.746 -Goal "x ~: A ==> (insert x A) - {x} = A";
4.747 -by Auto_tac;
4.748 -qed "Diff_insert_absorb";
4.749 -
4.750 -Goal "A Int (B-A) = {}";
4.751 -by (Blast_tac 1);
4.752 -qed "Diff_disjoint";
4.753 -Addsimps[Diff_disjoint];
4.754 -
4.755 -Goal "A<=B ==> A Un (B-A) = B";
4.756 -by (Blast_tac 1);
4.757 -qed "Diff_partition";
4.758 -
4.759 -Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
4.760 -by (Blast_tac 1);
4.761 -qed "double_diff";
4.762 -
4.763 -Goal "A Un (B-A) = A Un B";
4.764 -by (Blast_tac 1);
4.765 -qed "Un_Diff_cancel";
4.766 -
4.767 -Goal "(B-A) Un A = B Un A";
4.768 -by (Blast_tac 1);
4.769 -qed "Un_Diff_cancel2";
4.770 -
4.771 -Addsimps [Un_Diff_cancel, Un_Diff_cancel2];
4.772 -
4.773 -Goal "A - (B Un C) = (A-B) Int (A-C)";
4.774 -by (Blast_tac 1);
4.775 -qed "Diff_Un";
4.776 -
4.777 -Goal "A - (B Int C) = (A-B) Un (A-C)";
4.778 -by (Blast_tac 1);
4.779 -qed "Diff_Int";
4.780 -
4.781 -Goal "(A Un B) - C = (A - C) Un (B - C)";
4.782 -by (Blast_tac 1);
4.783 -qed "Un_Diff";
4.784 -
4.785 -Goal "(A Int B) - C = A Int (B - C)";
4.786 -by (Blast_tac 1);
4.787 -qed "Int_Diff";
4.788 -
4.789 -Goal "C Int (A-B) = (C Int A) - (C Int B)";
4.790 -by (Blast_tac 1);
4.791 -qed "Diff_Int_distrib";
4.792 -
4.793 -Goal "(A-B) Int C = (A Int C) - (B Int C)";
4.794 -by (Blast_tac 1);
4.795 -qed "Diff_Int_distrib2";
4.796 -
4.797 -Goal "A - (- B) = A Int B";
4.798 -by Auto_tac;
4.799 -qed "Diff_Compl";
4.800 -Addsimps [Diff_Compl];
4.801 -
4.802 -Goal "- (A-B) = -A Un B";
4.803 -by (blast_tac (claset() addIs []) 1);
4.804 -qed "Compl_Diff_eq";
4.805 -Addsimps [Compl_Diff_eq];
4.806 -
4.807 -
4.808 -section "Quantification over type \"bool\"";
4.809 -
4.810 -Goal "(ALL b::bool. P b) = (P True & P False)";
4.811 -by Auto_tac;
4.812 -by (case_tac "b" 1);
4.813 -by Auto_tac;
4.814 -qed "all_bool_eq";
4.815 -
4.816 -bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec);
4.817 -
4.818 -Goal "(EX b::bool. P b) = (P True | P False)";
4.819 -by Auto_tac;
4.820 -by (case_tac "b" 1);
4.821 -by Auto_tac;
4.822 -qed "ex_bool_eq";
4.823 -
4.824 -Goal "A Un B = (UN b. if b then A else B)";
4.825 -by (auto_tac(claset(), simpset() addsimps [split_if_mem2]));
4.826 -qed "Un_eq_UN";
4.827 -
4.828 -Goal "(UN b::bool. A b) = (A True Un A False)";
4.829 -by Auto_tac;
4.830 -by (case_tac "b" 1);
4.831 -by Auto_tac;
4.832 -qed "UN_bool_eq";
4.833 -
4.834 -Goal "(INT b::bool. A b) = (A True Int A False)";
4.835 -by Auto_tac;
4.836 -by (case_tac "b" 1);
4.837 -by Auto_tac;
4.838 -qed "INT_bool_eq";
4.839 -
4.840 -
4.841 -section "Pow";
4.842 -
4.843 -Goalw [Pow_def] "Pow {} = {{}}";
4.844 -by Auto_tac;
4.845 -qed "Pow_empty";
4.846 -Addsimps [Pow_empty];
4.847 -
4.848 -Goal "Pow (insert a A) = Pow A Un (insert a ` Pow A)";
4.849 -by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
4.850 -qed "Pow_insert";
4.851 -
4.852 -Goal "Pow (- A) = {-B |B. A: Pow B}";
4.853 -by (blast_tac (claset() addIs [inst "x" "- ?u" exI]) 1);
4.854 -qed "Pow_Compl";
4.855 -
4.856 -Goal "Pow UNIV = UNIV";
4.857 -by (Blast_tac 1);
4.858 -qed "Pow_UNIV";
4.859 -Addsimps [Pow_UNIV];
4.860 -
4.861 -Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
4.862 -by (Blast_tac 1);
4.863 -qed "Un_Pow_subset";
4.864 -
4.865 -Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
4.866 -by (Blast_tac 1);
4.867 -qed "UN_Pow_subset";
4.868 -
4.869 -Goal "A <= Pow(Union(A))";
4.870 -by (Blast_tac 1);
4.871 -qed "subset_Pow_Union";
4.872 -
4.873 -Goal "Union(Pow(A)) = A";
4.874 -by (Blast_tac 1);
4.875 -qed "Union_Pow_eq";
4.876 -
4.877 -Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
4.878 -by (Blast_tac 1);
4.879 -qed "Pow_Int_eq";
4.880 -
4.881 -Goal "Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))";
4.882 -by (Blast_tac 1);
4.883 -qed "Pow_INT_eq";
4.884 -
4.885 -Addsimps [Union_Pow_eq, Pow_Int_eq];
4.886 -
4.887 -
4.888 -section "Miscellany";
4.889 -
4.890 -Goal "(A = B) = ((A <= (B::'a set)) & (B<=A))";
4.891 -by (Blast_tac 1);
4.892 -qed "set_eq_subset";
4.893 -
4.894 -Goal "(A <= B) = (ALL t. t:A --> t:B)";
4.895 -by (Blast_tac 1);
4.896 -qed "subset_iff";
4.897 -
4.898 -Goalw [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
4.899 -by (Blast_tac 1);
4.900 -qed "subset_iff_psubset_eq";
4.901 -
4.902 -Goal "(ALL x. x ~: A) = (A={})";
4.903 -by (Blast_tac 1);
4.904 -qed "all_not_in_conv";
4.905 -AddIffs [all_not_in_conv];
4.906 -
4.907 -
4.908 -(** for datatypes **)
4.909 -Goal "f x ~= f y ==> x ~= y";
4.910 -by (Fast_tac 1);
4.911 -qed "distinct_lemma";
4.912 -
4.913 -
4.914 -(** Miniscoping: pushing in big Unions and Intersections **)
4.915 -local
4.916 - fun prover s = prove_goal (the_context ()) s
4.917 - (fn _ => [Simp_tac 1, ALLGOALS Blast_tac])
4.918 -in
4.919 -val UN_simps = map prover
4.920 - ["(UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))",
4.921 - "(UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))",
4.922 - "(UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))",
4.923 - "(UN x:C. A x Int B) = ((UN x:C. A x) Int B)",
4.924 - "(UN x:C. A Int B x) = (A Int (UN x:C. B x))",
4.925 - "(UN x:C. A x - B) = ((UN x:C. A x) - B)",
4.926 - "(UN x:C. A - B x) = (A - (INT x:C. B x))",
4.927 - "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",
4.928 - "(UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)",
4.929 - "(UN x:f`A. B x) = (UN a:A. B(f a))"];
4.930 -
4.931 -val INT_simps = map prover
4.932 - ["(INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)",
4.933 - "(INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))",
4.934 - "(INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)",
4.935 - "(INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))",
4.936 - "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
4.937 - "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)",
4.938 - "(INT x:C. A Un B x) = (A Un (INT x:C. B x))",
4.939 - "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",
4.940 - "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",
4.941 - "(INT x:f`A. B x) = (INT a:A. B(f a))"];
4.942 -
4.943 -
4.944 -val ball_simps = map prover
4.945 - ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
4.946 - "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
4.947 - "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
4.948 - "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
4.949 - "(ALL x:{}. P x) = True",
4.950 - "(ALL x:UNIV. P x) = (ALL x. P x)",
4.951 - "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
4.952 - "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
4.953 - "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
4.954 - "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
4.955 - "(ALL x:f`A. P x) = (ALL x:A. P(f x))",
4.956 - "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
4.957 -
4.958 -val ball_conj_distrib =
4.959 - prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
4.960 -
4.961 -val bex_simps = map prover
4.962 - ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
4.963 - "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
4.964 - "(EX x:{}. P x) = False",
4.965 - "(EX x:UNIV. P x) = (EX x. P x)",
4.966 - "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
4.967 - "(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)",
4.968 - "(EX x: UNION A B. P x) = (EX a:A. EX x: B a. P x)",
4.969 - "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
4.970 - "(EX x:f`A. P x) = (EX x:A. P(f x))",
4.971 - "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
4.972 -
4.973 -val bex_disj_distrib =
4.974 - prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
4.975 -
4.976 -end;
4.977 -
4.978 -bind_thms ("UN_simps", UN_simps);
4.979 -bind_thms ("INT_simps", INT_simps);
4.980 -bind_thms ("ball_simps", ball_simps);
4.981 -bind_thms ("bex_simps", bex_simps);
4.982 -bind_thm ("ball_conj_distrib", ball_conj_distrib);
4.983 -bind_thm ("bex_disj_distrib", bex_disj_distrib);
4.984 -
4.985 -Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);
5.1 --- a/src/HOL/mono.ML Fri Feb 15 20:43:44 2002 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,113 +0,0 @@
5.4 -(* Title: HOL/mono.ML
5.5 - ID: $Id$
5.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5.7 - Copyright 1991 University of Cambridge
5.8 -
5.9 -Monotonicity of various operations
5.10 -*)
5.11 -
5.12 -Goal "A<=B ==> f`A <= f`B";
5.13 -by (Blast_tac 1);
5.14 -qed "image_mono";
5.15 -
5.16 -Goal "A<=B ==> Pow(A) <= Pow(B)";
5.17 -by (Blast_tac 1);
5.18 -qed "Pow_mono";
5.19 -
5.20 -Goal "A<=B ==> Union(A) <= Union(B)";
5.21 -by (Blast_tac 1);
5.22 -qed "Union_mono";
5.23 -
5.24 -Goal "B<=A ==> Inter(A) <= Inter(B)";
5.25 -by (Blast_tac 1);
5.26 -qed "Inter_anti_mono";
5.27 -
5.28 -val prems = Goal
5.29 - "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \
5.30 -\ (UN x:A. f(x)) <= (UN x:B. g(x))";
5.31 -by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
5.32 -qed "UN_mono";
5.33 -
5.34 -(*The last inclusion is POSITIVE! *)
5.35 -val prems = Goal
5.36 - "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
5.37 -\ (INT x:A. f(x)) <= (INT x:A. g(x))";
5.38 -by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
5.39 -qed "INT_anti_mono";
5.40 -
5.41 -Goal "C<=D ==> insert a C <= insert a D";
5.42 -by (Blast_tac 1);
5.43 -qed "insert_mono";
5.44 -
5.45 -Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D";
5.46 -by (Blast_tac 1);
5.47 -qed "Un_mono";
5.48 -
5.49 -Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D";
5.50 -by (Blast_tac 1);
5.51 -qed "Int_mono";
5.52 -
5.53 -Goal "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D";
5.54 -by (Blast_tac 1);
5.55 -qed "Diff_mono";
5.56 -
5.57 -Goal "!!A::'a set. A <= B ==> -B <= -A";
5.58 -by (Blast_tac 1);
5.59 -qed "Compl_anti_mono";
5.60 -
5.61 -(** Monotonicity of implications. For inductive definitions **)
5.62 -
5.63 -Goal "A<=B ==> x:A --> x:B";
5.64 -by (rtac impI 1);
5.65 -by (etac subsetD 1);
5.66 -by (assume_tac 1);
5.67 -qed "in_mono";
5.68 -
5.69 -Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
5.70 -by (Blast_tac 1);
5.71 -qed "conj_mono";
5.72 -
5.73 -Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
5.74 -by (Blast_tac 1);
5.75 -qed "disj_mono";
5.76 -
5.77 -Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
5.78 -by (Blast_tac 1);
5.79 -qed "imp_mono";
5.80 -
5.81 -Goal "P-->P";
5.82 -by (rtac impI 1);
5.83 -by (assume_tac 1);
5.84 -qed "imp_refl";
5.85 -
5.86 -val [PQimp] = Goal
5.87 - "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
5.88 -by (blast_tac (claset() addIs [PQimp RS mp]) 1);
5.89 -qed "ex_mono";
5.90 -
5.91 -val [PQimp] = Goal
5.92 - "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
5.93 -by (blast_tac (claset() addIs [PQimp RS mp]) 1);
5.94 -qed "all_mono";
5.95 -
5.96 -val [PQimp] = Goal
5.97 - "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
5.98 -by (blast_tac (claset() addIs [PQimp RS mp]) 1);
5.99 -qed "Collect_mono";
5.100 -
5.101 -val [subs,PQimp] = Goal
5.102 - "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \
5.103 -\ |] ==> A Int Collect(P) <= B Int Collect(Q)";
5.104 -by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
5.105 -qed "Int_Collect_mono";
5.106 -
5.107 -val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
5.108 - ex_mono, Collect_mono, in_mono];
5.109 -
5.110 -Goal "[| a = b; c = d; b --> d |] ==> a --> c";
5.111 -by (Fast_tac 1);
5.112 -qed "eq_to_mono";
5.113 -
5.114 -Goal "[| a = b; c = d; ~ b --> ~ d |] ==> ~ a --> ~ c";
5.115 -by (Fast_tac 1);
5.116 -qed "eq_to_mono2";
6.1 --- a/src/HOL/subset.ML Fri Feb 15 20:43:44 2002 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,267 +0,0 @@
6.4 -(* Title: HOL/subset.ML
6.5 - ID: $Id$
6.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
6.7 - Copyright 1991 University of Cambridge
6.8 -
6.9 -Derived rules involving subsets. Union and Intersection as lattice
6.10 -operations.
6.11 -*)
6.12 -
6.13 -(* legacy ML bindings *)
6.14 -
6.15 -val Ball_def = thm "Ball_def";
6.16 -val Bex_def = thm "Bex_def";
6.17 -val Collect_mem_eq = thm "Collect_mem_eq";
6.18 -val Compl_def = thm "Compl_def";
6.19 -val INTER_def = thm "INTER_def";
6.20 -val Int_def = thm "Int_def";
6.21 -val Inter_def = thm "Inter_def";
6.22 -val Pow_def = thm "Pow_def";
6.23 -val UNION_def = thm "UNION_def";
6.24 -val UNIV_def = thm "UNIV_def";
6.25 -val Un_def = thm "Un_def";
6.26 -val Union_def = thm "Union_def";
6.27 -val empty_def = thm "empty_def";
6.28 -val image_def = thm "image_def";
6.29 -val insert_def = thm "insert_def";
6.30 -val mem_Collect_eq = thm "mem_Collect_eq";
6.31 -val psubset_def = thm "psubset_def";
6.32 -val set_diff_def = thm "set_diff_def";
6.33 -val subset_def = thm "subset_def";
6.34 -val CollectI = thm "CollectI";
6.35 -val CollectD = thm "CollectD";
6.36 -val set_ext = thm "set_ext";
6.37 -val Collect_cong = thm "Collect_cong";
6.38 -val CollectE = thm "CollectE";
6.39 -val ballI = thm "ballI";
6.40 -val strip = thms "strip";
6.41 -val bspec = thm "bspec";
6.42 -val ballE = thm "ballE";
6.43 -val bexI = thm "bexI";
6.44 -val rev_bexI = thm "rev_bexI";
6.45 -val bexCI = thm "bexCI";
6.46 -val bexE = thm "bexE";
6.47 -val ball_triv = thm "ball_triv";
6.48 -val bex_triv = thm "bex_triv";
6.49 -val bex_triv_one_point1 = thm "bex_triv_one_point1";
6.50 -val bex_triv_one_point2 = thm "bex_triv_one_point2";
6.51 -val bex_one_point1 = thm "bex_one_point1";
6.52 -val bex_one_point2 = thm "bex_one_point2";
6.53 -val ball_one_point1 = thm "ball_one_point1";
6.54 -val ball_one_point2 = thm "ball_one_point2";
6.55 -val ball_cong = thm "ball_cong";
6.56 -val bex_cong = thm "bex_cong";
6.57 -val subsetI = thm "subsetI";
6.58 -val subsetD = thm "subsetD";
6.59 -val rev_subsetD = thm "rev_subsetD";
6.60 -val subsetCE = thm "subsetCE";
6.61 -val contra_subsetD = thm "contra_subsetD";
6.62 -val subset_refl = thm "subset_refl";
6.63 -val subset_trans = thm "subset_trans";
6.64 -val subset_antisym = thm "subset_antisym";
6.65 -val equalityI = thm "equalityI";
6.66 -val equalityD1 = thm "equalityD1";
6.67 -val equalityD2 = thm "equalityD2";
6.68 -val equalityE = thm "equalityE";
6.69 -val equalityCE = thm "equalityCE";
6.70 -val setup_induction = thm "setup_induction";
6.71 -val eqset_imp_iff = thm "eqset_imp_iff";
6.72 -val UNIV_I = thm "UNIV_I";
6.73 -val UNIV_witness = thm "UNIV_witness";
6.74 -val subset_UNIV = thm "subset_UNIV";
6.75 -val ball_UNIV = thm "ball_UNIV";
6.76 -val bex_UNIV = thm "bex_UNIV";
6.77 -val empty_iff = thm "empty_iff";
6.78 -val emptyE = thm "emptyE";
6.79 -val empty_subsetI = thm "empty_subsetI";
6.80 -val equals0I = thm "equals0I";
6.81 -val equals0D = thm "equals0D";
6.82 -val ball_empty = thm "ball_empty";
6.83 -val bex_empty = thm "bex_empty";
6.84 -val UNIV_not_empty = thm "UNIV_not_empty";
6.85 -val Pow_iff = thm "Pow_iff";
6.86 -val PowI = thm "PowI";
6.87 -val PowD = thm "PowD";
6.88 -val Pow_bottom = thm "Pow_bottom";
6.89 -val Pow_top = thm "Pow_top";
6.90 -val Compl_iff = thm "Compl_iff";
6.91 -val ComplI = thm "ComplI";
6.92 -val ComplD = thm "ComplD";
6.93 -val ComplE = thm "ComplE";
6.94 -val Un_iff = thm "Un_iff";
6.95 -val UnI1 = thm "UnI1";
6.96 -val UnI2 = thm "UnI2";
6.97 -val UnCI = thm "UnCI";
6.98 -val UnE = thm "UnE";
6.99 -val Int_iff = thm "Int_iff";
6.100 -val IntI = thm "IntI";
6.101 -val IntD1 = thm "IntD1";
6.102 -val IntD2 = thm "IntD2";
6.103 -val IntE = thm "IntE";
6.104 -val Diff_iff = thm "Diff_iff";
6.105 -val DiffI = thm "DiffI";
6.106 -val DiffD1 = thm "DiffD1";
6.107 -val DiffD2 = thm "DiffD2";
6.108 -val DiffE = thm "DiffE";
6.109 -val insert_iff = thm "insert_iff";
6.110 -val insertI1 = thm "insertI1";
6.111 -val insertI2 = thm "insertI2";
6.112 -val insertE = thm "insertE";
6.113 -val insertCI = thm "insertCI";
6.114 -val subset_insert_iff = thm "subset_insert_iff";
6.115 -val singletonI = thm "singletonI";
6.116 -val singletonD = thm "singletonD";
6.117 -val singletonE = thm "singletonE";
6.118 -val singleton_iff = thm "singleton_iff";
6.119 -val singleton_inject = thm "singleton_inject";
6.120 -val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
6.121 -val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
6.122 -val subset_singletonD = thm "subset_singletonD";
6.123 -val singleton_conv = thm "singleton_conv";
6.124 -val singleton_conv2 = thm "singleton_conv2";
6.125 -val diff_single_insert = thm "diff_single_insert";
6.126 -val UN_iff = thm "UN_iff";
6.127 -val UN_I = thm "UN_I";
6.128 -val UN_E = thm "UN_E";
6.129 -val UN_cong = thm "UN_cong";
6.130 -val INT_iff = thm "INT_iff";
6.131 -val INT_I = thm "INT_I";
6.132 -val INT_D = thm "INT_D";
6.133 -val INT_E = thm "INT_E";
6.134 -val INT_cong = thm "INT_cong";
6.135 -val Union_iff = thm "Union_iff";
6.136 -val UnionI = thm "UnionI";
6.137 -val UnionE = thm "UnionE";
6.138 -val Inter_iff = thm "Inter_iff";
6.139 -val InterI = thm "InterI";
6.140 -val InterD = thm "InterD";
6.141 -val InterE = thm "InterE";
6.142 -val image_eqI = thm "image_eqI";
6.143 -val imageI = thm "imageI";
6.144 -val rev_image_eqI = thm "rev_image_eqI";
6.145 -val imageE = thm "imageE";
6.146 -val image_Un = thm "image_Un";
6.147 -val image_iff = thm "image_iff";
6.148 -val image_subset_iff = thm "image_subset_iff";
6.149 -val subset_image_iff = thm "subset_image_iff";
6.150 -val image_subsetI = thm "image_subsetI";
6.151 -val range_eqI = thm "range_eqI";
6.152 -val rangeI = thm "rangeI";
6.153 -val rangeE = thm "rangeE";
6.154 -val split_if_eq1 = thm "split_if_eq1";
6.155 -val split_if_eq2 = thm "split_if_eq2";
6.156 -val split_if_mem1 = thm "split_if_mem1";
6.157 -val split_if_mem2 = thm "split_if_mem2";
6.158 -val split_ifs = thms "split_ifs";
6.159 -val mem_simps = thms "mem_simps";
6.160 -val psubsetI = thm "psubsetI";
6.161 -val psubset_insert_iff = thm "psubset_insert_iff";
6.162 -val psubset_eq = thm "psubset_eq";
6.163 -val psubset_imp_subset = thm "psubset_imp_subset";
6.164 -val psubset_subset_trans = thm "psubset_subset_trans";
6.165 -val subset_psubset_trans = thm "subset_psubset_trans";
6.166 -val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
6.167 -val atomize_ball = thm "atomize_ball";
6.168 -
6.169 -
6.170 -(*** insert ***)
6.171 -
6.172 -Goal "B <= insert a B";
6.173 -by (rtac subsetI 1);
6.174 -by (etac insertI2 1) ;
6.175 -qed "subset_insertI";
6.176 -
6.177 -Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
6.178 -by (Blast_tac 1);
6.179 -qed "subset_insert";
6.180 -
6.181 -(*** Big Union -- least upper bound of a set ***)
6.182 -
6.183 -Goal "B:A ==> B <= Union(A)";
6.184 -by (REPEAT (ares_tac [subsetI,UnionI] 1));
6.185 -qed "Union_upper";
6.186 -
6.187 -val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
6.188 -by (rtac subsetI 1);
6.189 -by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));
6.190 -qed "Union_least";
6.191 -
6.192 -(** General union **)
6.193 -
6.194 -Goal "a:A ==> B(a) <= (UN x:A. B(x))";
6.195 -by (Blast_tac 1);
6.196 -qed "UN_upper";
6.197 -
6.198 -val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
6.199 -by (rtac subsetI 1);
6.200 -by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
6.201 -qed "UN_least";
6.202 -
6.203 -
6.204 -(*** Big Intersection -- greatest lower bound of a set ***)
6.205 -
6.206 -Goal "B:A ==> Inter(A) <= B";
6.207 -by (Blast_tac 1);
6.208 -qed "Inter_lower";
6.209 -
6.210 -val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
6.211 -by (rtac (InterI RS subsetI) 1);
6.212 -by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
6.213 -qed "Inter_greatest";
6.214 -
6.215 -Goal "a:A ==> (INT x:A. B(x)) <= B(a)";
6.216 -by (Blast_tac 1);
6.217 -qed "INT_lower";
6.218 -
6.219 -val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
6.220 -by (rtac (INT_I RS subsetI) 1);
6.221 -by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
6.222 -qed "INT_greatest";
6.223 -
6.224 -(*** Finite Union -- the least upper bound of 2 sets ***)
6.225 -
6.226 -Goal "A <= A Un B";
6.227 -by (Blast_tac 1);
6.228 -qed "Un_upper1";
6.229 -
6.230 -Goal "B <= A Un B";
6.231 -by (Blast_tac 1);
6.232 -qed "Un_upper2";
6.233 -
6.234 -Goal "[| A<=C; B<=C |] ==> A Un B <= C";
6.235 -by (Blast_tac 1);
6.236 -qed "Un_least";
6.237 -
6.238 -(*** Finite Intersection -- the greatest lower bound of 2 sets *)
6.239 -
6.240 -Goal "A Int B <= A";
6.241 -by (Blast_tac 1);
6.242 -qed "Int_lower1";
6.243 -
6.244 -Goal "A Int B <= B";
6.245 -by (Blast_tac 1);
6.246 -qed "Int_lower2";
6.247 -
6.248 -Goal "[| C<=A; C<=B |] ==> C <= A Int B";
6.249 -by (Blast_tac 1);
6.250 -qed "Int_greatest";
6.251 -
6.252 -(*** Set difference ***)
6.253 -
6.254 -Goal "A-B <= (A::'a set)";
6.255 -by (Blast_tac 1) ;
6.256 -qed "Diff_subset";
6.257 -
6.258 -(*** Monotonicity ***)
6.259 -
6.260 -Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
6.261 -by (rtac Un_least 1);
6.262 -by (etac (Un_upper1 RSN (2,monoD)) 1);
6.263 -by (etac (Un_upper2 RSN (2,monoD)) 1);
6.264 -qed "mono_Un";
6.265 -
6.266 -Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
6.267 -by (rtac Int_greatest 1);
6.268 -by (etac (Int_lower1 RSN (2,monoD)) 1);
6.269 -by (etac (Int_lower2 RSN (2,monoD)) 1);
6.270 -qed "mono_Int";