converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
authorwenzelm
Sat Feb 16 20:59:34 2002 +0100 (2002-02-16)
changeset 12897f4d10ad0ea7b
parent 12896 4518acda6d93
child 12898 c78872ea3320
converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
src/HOL/IsaMakefile
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/equalities.ML
src/HOL/mono.ML
src/HOL/subset.ML
     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,32 +851,30 @@
   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 -  apply blast
   3.272 -  done
   3.273 -
   3.274 -lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)"
   3.275 +  "(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.276 +  by (auto simp add: psubset_def subset_insert_iff)
   3.277 +
   3.278 +lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
   3.279    by (simp only: psubset_def)
   3.280  
   3.281 -lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B"
   3.282 +lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
   3.283    by (simp add: psubset_eq)
   3.284  
   3.285 -lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C"
   3.286 +lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
   3.287    by (auto simp add: psubset_eq)
   3.288  
   3.289 -lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C"
   3.290 +lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
   3.291    by (auto simp add: psubset_eq)
   3.292  
   3.293 -lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)"
   3.294 +lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
   3.295    by (unfold psubset_def) blast
   3.296  
   3.297  lemma atomize_ball:
   3.298 -    "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)"
   3.299 +    "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
   3.300    by (simp only: Ball_def atomize_all atomize_imp)
   3.301  
   3.302  declare atomize_ball [symmetric, rulify]
   3.303 @@ -885,9 +882,898 @@
   3.304  
   3.305  subsection {* Further set-theory lemmas *}
   3.306  
   3.307 -use "subset.ML"
   3.308 -use "equalities.ML"
   3.309 -use "mono.ML"
   3.310 +subsubsection {* Derived rules involving subsets. *}
   3.311 +
   3.312 +text {* @{text insert}. *}
   3.313 +
   3.314 +lemma subset_insertI: "B \<subseteq> insert a B"
   3.315 +  apply (rule subsetI)
   3.316 +  apply (erule insertI2)
   3.317 +  done
   3.318 +
   3.319 +lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
   3.320 +  by blast
   3.321 +
   3.322 +
   3.323 +text {* \medskip Big Union -- least upper bound of a set. *}
   3.324 +
   3.325 +lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
   3.326 +  by (rules intro: subsetI UnionI)
   3.327 +
   3.328 +lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
   3.329 +  by (rules intro: subsetI elim: UnionE dest: subsetD)
   3.330 +
   3.331 +
   3.332 +text {* \medskip General union. *}
   3.333 +
   3.334 +lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
   3.335 +  by blast
   3.336 +
   3.337 +lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
   3.338 +  by (rules intro: subsetI elim: UN_E dest: subsetD)
   3.339 +
   3.340 +
   3.341 +text {* \medskip Big Intersection -- greatest lower bound of a set. *}
   3.342 +
   3.343 +lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
   3.344 +  by blast
   3.345 +
   3.346 +lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
   3.347 +  by (rules intro: InterI subsetI dest: subsetD)
   3.348 +
   3.349 +lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
   3.350 +  by blast
   3.351 +
   3.352 +lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
   3.353 +  by (rules intro: INT_I subsetI dest: subsetD)
   3.354 +
   3.355 +
   3.356 +text {* \medskip Finite Union -- the least upper bound of two sets. *}
   3.357 +
   3.358 +lemma Un_upper1: "A \<subseteq> A \<union> B"
   3.359 +  by blast
   3.360 +
   3.361 +lemma Un_upper2: "B \<subseteq> A \<union> B"
   3.362 +  by blast
   3.363 +
   3.364 +lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
   3.365 +  by blast
   3.366 +
   3.367 +
   3.368 +text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
   3.369 +
   3.370 +lemma Int_lower1: "A \<inter> B \<subseteq> A"
   3.371 +  by blast
   3.372 +
   3.373 +lemma Int_lower2: "A \<inter> B \<subseteq> B"
   3.374 +  by blast
   3.375 +
   3.376 +lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
   3.377 +  by blast
   3.378 +
   3.379 +
   3.380 +text {* \medskip Set difference. *}
   3.381 +
   3.382 +lemma Diff_subset: "A - B \<subseteq> A"
   3.383 +  by blast
   3.384 +
   3.385 +
   3.386 +text {* \medskip Monotonicity. *}
   3.387 +
   3.388 +lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
   3.389 +  apply (rule Un_least)
   3.390 +   apply (erule Un_upper1 [THEN [2] monoD])
   3.391 +  apply (erule Un_upper2 [THEN [2] monoD])
   3.392 +  done
   3.393 +
   3.394 +lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   3.395 +  apply (rule Int_greatest)
   3.396 +   apply (erule Int_lower1 [THEN [2] monoD])
   3.397 +  apply (erule Int_lower2 [THEN [2] monoD])
   3.398 +  done
   3.399 +
   3.400 +
   3.401 +subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
   3.402 +
   3.403 +text {* @{text "{}"}. *}
   3.404 +
   3.405 +lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
   3.406 +  -- {* supersedes @{text "Collect_False_empty"} *}
   3.407 +  by auto
   3.408 +
   3.409 +lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
   3.410 +  by blast
   3.411 +
   3.412 +lemma not_psubset_empty [iff]: "\<not> (A < {})"
   3.413 +  by (unfold psubset_def) blast
   3.414 +
   3.415 +lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
   3.416 +  by auto
   3.417 +
   3.418 +lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
   3.419 +  by blast
   3.420 +
   3.421 +lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
   3.422 +  by blast
   3.423 +
   3.424 +lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
   3.425 +  by blast
   3.426 +
   3.427 +lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
   3.428 +  by blast
   3.429 +
   3.430 +lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
   3.431 +  by blast
   3.432 +
   3.433 +lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   3.434 +  by blast
   3.435 +
   3.436 +lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   3.437 +  by blast
   3.438 +
   3.439 +
   3.440 +text {* \medskip @{text insert}. *}
   3.441 +
   3.442 +lemma insert_is_Un: "insert a A = {a} Un A"
   3.443 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
   3.444 +  by blast
   3.445 +
   3.446 +lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
   3.447 +  by blast
   3.448 +
   3.449 +lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard]
   3.450 +
   3.451 +lemma insert_absorb: "a \<in> A ==> insert a A = A"
   3.452 +  -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
   3.453 +  -- {* with \emph{quadratic} running time *}
   3.454 +  by blast
   3.455 +
   3.456 +lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
   3.457 +  by blast
   3.458 +
   3.459 +lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
   3.460 +  by blast
   3.461 +
   3.462 +lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
   3.463 +  by blast
   3.464 +
   3.465 +lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
   3.466 +  -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
   3.467 +  apply (rule_tac x = "A - {a}" in exI)
   3.468 +  apply blast
   3.469 +  done
   3.470 +
   3.471 +lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
   3.472 +  by auto
   3.473 +
   3.474 +lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   3.475 +  by blast
   3.476 +
   3.477 +
   3.478 +text {* \medskip @{text image}. *}
   3.479 +
   3.480 +lemma image_empty [simp]: "f`{} = {}"
   3.481 +  by blast
   3.482 +
   3.483 +lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
   3.484 +  by blast
   3.485 +
   3.486 +lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
   3.487 +  by blast
   3.488 +
   3.489 +lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   3.490 +  by blast
   3.491 +
   3.492 +lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
   3.493 +  by blast
   3.494 +
   3.495 +lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
   3.496 +  by blast
   3.497 +
   3.498 +lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
   3.499 +  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *}
   3.500 +  -- {* with its implicit quantifier and conjunction.  Also image enjoys better *}
   3.501 +  -- {* equational properties than does the RHS. *}
   3.502 +  by blast
   3.503 +
   3.504 +lemma if_image_distrib [simp]:
   3.505 +  "(\<lambda>x. if P x then f x else g x) ` S
   3.506 +    = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
   3.507 +  by (auto simp add: image_def)
   3.508 +
   3.509 +lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
   3.510 +  by (simp add: image_def)
   3.511 +
   3.512 +
   3.513 +text {* \medskip @{text range}. *}
   3.514 +
   3.515 +lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
   3.516 +  by auto
   3.517 +
   3.518 +lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
   3.519 +  apply (subst image_image)
   3.520 +  apply simp
   3.521 +  done
   3.522 +
   3.523 +
   3.524 +text {* \medskip @{text Int} *}
   3.525 +
   3.526 +lemma Int_absorb [simp]: "A \<inter> A = A"
   3.527 +  by blast
   3.528 +
   3.529 +lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
   3.530 +  by blast
   3.531 +
   3.532 +lemma Int_commute: "A \<inter> B = B \<inter> A"
   3.533 +  by blast
   3.534 +
   3.535 +lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
   3.536 +  by blast
   3.537 +
   3.538 +lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
   3.539 +  by blast
   3.540 +
   3.541 +lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
   3.542 +  -- {* Intersection is an AC-operator *}
   3.543 +
   3.544 +lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
   3.545 +  by blast
   3.546 +
   3.547 +lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
   3.548 +  by blast
   3.549 +
   3.550 +lemma Int_empty_left [simp]: "{} \<inter> B = {}"
   3.551 +  by blast
   3.552 +
   3.553 +lemma Int_empty_right [simp]: "A \<inter> {} = {}"
   3.554 +  by blast
   3.555 +
   3.556 +lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
   3.557 +  by blast
   3.558 +
   3.559 +lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
   3.560 +  by blast
   3.561 +
   3.562 +lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
   3.563 +  by blast
   3.564 +
   3.565 +lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
   3.566 +  by blast
   3.567 +
   3.568 +lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   3.569 +  by blast
   3.570 +
   3.571 +lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
   3.572 +  by blast
   3.573 +
   3.574 +lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   3.575 +  by blast
   3.576 +
   3.577 +lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   3.578 +  by blast
   3.579 +
   3.580 +lemma Int_subset_iff: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
   3.581 +  by blast
   3.582 +
   3.583 +lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
   3.584 +  by blast
   3.585 +
   3.586 +
   3.587 +text {* \medskip @{text Un}. *}
   3.588 +
   3.589 +lemma Un_absorb [simp]: "A \<union> A = A"
   3.590 +  by blast
   3.591 +
   3.592 +lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
   3.593 +  by blast
   3.594 +
   3.595 +lemma Un_commute: "A \<union> B = B \<union> A"
   3.596 +  by blast
   3.597 +
   3.598 +lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
   3.599 +  by blast
   3.600 +
   3.601 +lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
   3.602 +  by blast
   3.603 +
   3.604 +lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
   3.605 +  -- {* Union is an AC-operator *}
   3.606 +
   3.607 +lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
   3.608 +  by blast
   3.609 +
   3.610 +lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
   3.611 +  by blast
   3.612 +
   3.613 +lemma Un_empty_left [simp]: "{} \<union> B = B"
   3.614 +  by blast
   3.615 +
   3.616 +lemma Un_empty_right [simp]: "A \<union> {} = A"
   3.617 +  by blast
   3.618 +
   3.619 +lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
   3.620 +  by blast
   3.621 +
   3.622 +lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
   3.623 +  by blast
   3.624 +
   3.625 +lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
   3.626 +  by blast
   3.627 +
   3.628 +lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
   3.629 +  by blast
   3.630 +
   3.631 +lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
   3.632 +  by blast
   3.633 +
   3.634 +lemma Int_insert_left:
   3.635 +    "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
   3.636 +  by auto
   3.637 +
   3.638 +lemma Int_insert_right:
   3.639 +    "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
   3.640 +  by auto
   3.641 +
   3.642 +lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
   3.643 +  by blast
   3.644 +
   3.645 +lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
   3.646 +  by blast
   3.647 +
   3.648 +lemma Un_Int_crazy:
   3.649 +    "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
   3.650 +  by blast
   3.651 +
   3.652 +lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
   3.653 +  by blast
   3.654 +
   3.655 +lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   3.656 +  by blast
   3.657 +
   3.658 +lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   3.659 +  by blast
   3.660 +
   3.661 +lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
   3.662 +  by blast
   3.663 +
   3.664 +
   3.665 +text {* \medskip Set complement *}
   3.666 +
   3.667 +lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
   3.668 +  by blast
   3.669 +
   3.670 +lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
   3.671 +  by blast
   3.672 +
   3.673 +lemma Compl_partition: "A \<union> (-A) = UNIV"
   3.674 +  by blast
   3.675 +
   3.676 +lemma double_complement [simp]: "- (-A) = (A::'a set)"
   3.677 +  by blast
   3.678 +
   3.679 +lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
   3.680 +  by blast
   3.681 +
   3.682 +lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
   3.683 +  by blast
   3.684 +
   3.685 +lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
   3.686 +  by blast
   3.687 +
   3.688 +lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   3.689 +  by blast
   3.690 +
   3.691 +lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
   3.692 +  by blast
   3.693 +
   3.694 +lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
   3.695 +  -- {* Halmos, Naive Set Theory, page 16. *}
   3.696 +  by blast
   3.697 +
   3.698 +lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
   3.699 +  by blast
   3.700 +
   3.701 +lemma Compl_empty_eq [simp]: "-{} = UNIV"
   3.702 +  by blast
   3.703 +
   3.704 +lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
   3.705 +  by blast
   3.706 +
   3.707 +lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
   3.708 +  by blast
   3.709 +
   3.710 +
   3.711 +text {* \medskip @{text Union}. *}
   3.712 +
   3.713 +lemma Union_empty [simp]: "Union({}) = {}"
   3.714 +  by blast
   3.715 +
   3.716 +lemma Union_UNIV [simp]: "Union UNIV = UNIV"
   3.717 +  by blast
   3.718 +
   3.719 +lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
   3.720 +  by blast
   3.721 +
   3.722 +lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
   3.723 +  by blast
   3.724 +
   3.725 +lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   3.726 +  by blast
   3.727 +
   3.728 +lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
   3.729 +  by auto
   3.730 +
   3.731 +lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
   3.732 +  by blast
   3.733 +
   3.734 +
   3.735 +text {* \medskip @{text Inter}. *}
   3.736 +
   3.737 +lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
   3.738 +  by blast
   3.739 +
   3.740 +lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
   3.741 +  by blast
   3.742 +
   3.743 +lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
   3.744 +  by blast
   3.745 +
   3.746 +lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
   3.747 +  by blast
   3.748 +
   3.749 +lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   3.750 +  by blast
   3.751 +
   3.752 +
   3.753 +text {*
   3.754 +  \medskip @{text UN} and @{text INT}.
   3.755 +
   3.756 +  Basic identities: *}
   3.757 +
   3.758 +lemma UN_empty [simp]: "(\<Union>x\<in>{}. B x) = {}"
   3.759 +  by blast
   3.760 +
   3.761 +lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
   3.762 +  by blast
   3.763 +
   3.764 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
   3.765 +  by blast
   3.766 +
   3.767 +lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
   3.768 +  by blast
   3.769 +
   3.770 +lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
   3.771 +  by blast
   3.772 +
   3.773 +lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   3.774 +  by blast
   3.775 +
   3.776 +lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
   3.777 +  by blast
   3.778 +
   3.779 +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.780 +  by blast
   3.781 +
   3.782 +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.783 +  by blast
   3.784 +
   3.785 +lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
   3.786 +  by blast
   3.787 +
   3.788 +lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
   3.789 +  by blast
   3.790 +
   3.791 +lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
   3.792 +  by blast
   3.793 +
   3.794 +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.795 +  by blast
   3.796 +
   3.797 +lemma INT_insert_distrib:
   3.798 +    "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   3.799 +  by blast
   3.800 +
   3.801 +lemma Union_image_eq [simp]: "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
   3.802 +  by blast
   3.803 +
   3.804 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   3.805 +  by blast
   3.806 +
   3.807 +lemma Inter_image_eq [simp]: "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   3.808 +  by blast
   3.809 +
   3.810 +lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
   3.811 +  by auto
   3.812 +
   3.813 +lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
   3.814 +  by auto
   3.815 +
   3.816 +lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
   3.817 +  by blast
   3.818 +
   3.819 +lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
   3.820 +  -- {* Look: it has an \emph{existential} quantifier *}
   3.821 +  by blast
   3.822 +
   3.823 +lemma UN_empty3 [iff]: "(UNION A B = {}) = (\<forall>x\<in>A. B x = {})"
   3.824 +  by auto
   3.825 +
   3.826 +
   3.827 +text {* \medskip Distributive laws: *}
   3.828 +
   3.829 +lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
   3.830 +  by blast
   3.831 +
   3.832 +lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
   3.833 +  by blast
   3.834 +
   3.835 +lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A`C) \<union> \<Union>(B`C)"
   3.836 +  -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
   3.837 +  -- {* Union of a family of unions *}
   3.838 +  by blast
   3.839 +
   3.840 +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.841 +  -- {* Equivalent version *}
   3.842 +  by blast
   3.843 +
   3.844 +lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
   3.845 +  by blast
   3.846 +
   3.847 +lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A`C) \<inter> \<Inter>(B`C)"
   3.848 +  by blast
   3.849 +
   3.850 +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.851 +  -- {* Equivalent version *}
   3.852 +  by blast
   3.853 +
   3.854 +lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
   3.855 +  -- {* Halmos, Naive Set Theory, page 35. *}
   3.856 +  by blast
   3.857 +
   3.858 +lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
   3.859 +  by blast
   3.860 +
   3.861 +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.862 +  by blast
   3.863 +
   3.864 +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.865 +  by blast
   3.866 +
   3.867 +
   3.868 +text {* \medskip Bounded quantifiers.
   3.869 +
   3.870 +  The following are not added to the default simpset because
   3.871 +  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
   3.872 +
   3.873 +lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
   3.874 +  by blast
   3.875 +
   3.876 +lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"
   3.877 +  by blast
   3.878 +
   3.879 +lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
   3.880 +  by blast
   3.881 +
   3.882 +lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
   3.883 +  by blast
   3.884 +
   3.885 +
   3.886 +text {* \medskip Set difference. *}
   3.887 +
   3.888 +lemma Diff_eq: "A - B = A \<inter> (-B)"
   3.889 +  by blast
   3.890 +
   3.891 +lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
   3.892 +  by blast
   3.893 +
   3.894 +lemma Diff_cancel [simp]: "A - A = {}"
   3.895 +  by blast
   3.896 +
   3.897 +lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
   3.898 +  by (blast elim: equalityE)
   3.899 +
   3.900 +lemma empty_Diff [simp]: "{} - A = {}"
   3.901 +  by blast
   3.902 +
   3.903 +lemma Diff_empty [simp]: "A - {} = A"
   3.904 +  by blast
   3.905 +
   3.906 +lemma Diff_UNIV [simp]: "A - UNIV = {}"
   3.907 +  by blast
   3.908 +
   3.909 +lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
   3.910 +  by blast
   3.911 +
   3.912 +lemma Diff_insert: "A - insert a B = A - B - {a}"
   3.913 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
   3.914 +  by blast
   3.915 +
   3.916 +lemma Diff_insert2: "A - insert a B = A - {a} - B"
   3.917 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
   3.918 +  by blast
   3.919 +
   3.920 +lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
   3.921 +  by auto
   3.922 +
   3.923 +lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
   3.924 +  by blast
   3.925 +
   3.926 +lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
   3.927 +  by blast
   3.928 +
   3.929 +lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"
   3.930 +  by auto
   3.931 +
   3.932 +lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
   3.933 +  by blast
   3.934 +
   3.935 +lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"
   3.936 +  by blast
   3.937 +
   3.938 +lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"
   3.939 +  by blast
   3.940 +
   3.941 +lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
   3.942 +  by blast
   3.943 +
   3.944 +lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
   3.945 +  by blast
   3.946 +
   3.947 +lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
   3.948 +  by blast
   3.949 +
   3.950 +lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
   3.951 +  by blast
   3.952 +
   3.953 +lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
   3.954 +  by blast
   3.955 +
   3.956 +lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
   3.957 +  by blast
   3.958 +
   3.959 +lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
   3.960 +  by blast
   3.961 +
   3.962 +lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
   3.963 +  by blast
   3.964 +
   3.965 +lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
   3.966 +  by auto
   3.967 +
   3.968 +lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
   3.969 +  by blast
   3.970 +
   3.971 +
   3.972 +text {* \medskip Quantification over type @{typ bool}. *}
   3.973 +
   3.974 +lemma all_bool_eq: "(\<forall>b::bool. P b) = (P True & P False)"
   3.975 +  apply auto
   3.976 +  apply (tactic {* case_tac "b" 1 *})
   3.977 +   apply auto
   3.978 +  done
   3.979 +
   3.980 +lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
   3.981 +  by (rule conjI [THEN all_bool_eq [THEN iffD2], THEN spec])
   3.982 +
   3.983 +lemma ex_bool_eq: "(\<exists>b::bool. P b) = (P True | P False)"
   3.984 +  apply auto
   3.985 +  apply (tactic {* case_tac "b" 1 *})
   3.986 +   apply auto
   3.987 +  done
   3.988 +
   3.989 +lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
   3.990 +  by (auto simp add: split_if_mem2)
   3.991 +
   3.992 +lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
   3.993 +  apply auto
   3.994 +  apply (tactic {* case_tac "b" 1 *})
   3.995 +   apply auto
   3.996 +  done
   3.997 +
   3.998 +lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
   3.999 +  apply auto
  3.1000 +  apply (tactic {* case_tac "b" 1 *})
  3.1001 +  apply auto
  3.1002 +  done
  3.1003 +
  3.1004 +
  3.1005 +text {* \medskip @{text Pow} *}
  3.1006 +
  3.1007 +lemma Pow_empty [simp]: "Pow {} = {{}}"
  3.1008 +  by (auto simp add: Pow_def)
  3.1009 +
  3.1010 +lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
  3.1011 +  by (blast intro: image_eqI [where ?x = "u - {a}", standard])
  3.1012 +
  3.1013 +lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
  3.1014 +  by (blast intro: exI [where ?x = "- u", standard])
  3.1015 +
  3.1016 +lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
  3.1017 +  by blast
  3.1018 +
  3.1019 +lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
  3.1020 +  by blast
  3.1021 +
  3.1022 +lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
  3.1023 +  by blast
  3.1024 +
  3.1025 +lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
  3.1026 +  by blast
  3.1027 +
  3.1028 +lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
  3.1029 +  by blast
  3.1030 +
  3.1031 +lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
  3.1032 +  by blast
  3.1033 +
  3.1034 +lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
  3.1035 +  by blast
  3.1036 +
  3.1037 +
  3.1038 +text {* \medskip Miscellany. *}
  3.1039 +
  3.1040 +lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
  3.1041 +  by blast
  3.1042 +
  3.1043 +lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
  3.1044 +  by blast
  3.1045 +
  3.1046 +lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
  3.1047 +  by (unfold psubset_def) blast
  3.1048 +
  3.1049 +lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
  3.1050 +  by blast
  3.1051 +
  3.1052 +lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
  3.1053 +  by rules
  3.1054 +
  3.1055 +
  3.1056 +text {* \medskip Miniscoping: pushing in big Unions and Intersections. *}
  3.1057 +
  3.1058 +lemma UN_simps [simp]:
  3.1059 +  "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"
  3.1060 +  "!!A B C. (UN x:C. A x Un B)   = ((if C={} then {} else (UN x:C. A x) Un B))"
  3.1061 +  "!!A B C. (UN x:C. A Un B x)   = ((if C={} then {} else A Un (UN x:C. B x)))"
  3.1062 +  "!!A B C. (UN x:C. A x Int B)  = ((UN x:C. A x) Int B)"
  3.1063 +  "!!A B C. (UN x:C. A Int B x)  = (A Int (UN x:C. B x))"
  3.1064 +  "!!A B C. (UN x:C. A x - B)    = ((UN x:C. A x) - B)"
  3.1065 +  "!!A B C. (UN x:C. A - B x)    = (A - (INT x:C. B x))"
  3.1066 +  "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"
  3.1067 +  "!!A B C. (UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)"
  3.1068 +  "!!A B f. (UN x:f`A. B x)     = (UN a:A. B (f a))"
  3.1069 +  by auto
  3.1070 +
  3.1071 +lemma INT_simps [simp]:
  3.1072 +  "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"
  3.1073 +  "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"
  3.1074 +  "!!A B C. (INT x:C. A x - B)   = (if C={} then UNIV else (INT x:C. A x) - B)"
  3.1075 +  "!!A B C. (INT x:C. A - B x)   = (if C={} then UNIV else A - (UN x:C. B x))"
  3.1076 +  "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"
  3.1077 +  "!!A B C. (INT x:C. A x Un B)  = ((INT x:C. A x) Un B)"
  3.1078 +  "!!A B C. (INT x:C. A Un B x)  = (A Un (INT x:C. B x))"
  3.1079 +  "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"
  3.1080 +  "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"
  3.1081 +  "!!A B f. (INT x:f`A. B x)    = (INT a:A. B (f a))"
  3.1082 +  by auto
  3.1083 +
  3.1084 +lemma ball_simps [simp]:
  3.1085 +  "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
  3.1086 +  "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
  3.1087 +  "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
  3.1088 +  "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"
  3.1089 +  "!!P. (ALL x:{}. P x) = True"
  3.1090 +  "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"
  3.1091 +  "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"
  3.1092 +  "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"
  3.1093 +  "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"
  3.1094 +  "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"
  3.1095 +  "!!A P f. (ALL x:f`A. P x) = (ALL x:A. P (f x))"
  3.1096 +  "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
  3.1097 +  by auto
  3.1098 +
  3.1099 +lemma bex_simps [simp]:
  3.1100 +  "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
  3.1101 +  "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
  3.1102 +  "!!P. (EX x:{}. P x) = False"
  3.1103 +  "!!P. (EX x:UNIV. P x) = (EX x. P x)"
  3.1104 +  "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"
  3.1105 +  "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"
  3.1106 +  "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"
  3.1107 +  "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"
  3.1108 +  "!!A P f. (EX x:f`A. P x) = (EX x:A. P (f x))"
  3.1109 +  "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"
  3.1110 +  by auto
  3.1111 +
  3.1112 +lemma ball_conj_distrib:
  3.1113 +  "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"
  3.1114 +  by blast
  3.1115 +
  3.1116 +lemma bex_disj_distrib:
  3.1117 +  "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"
  3.1118 +  by blast
  3.1119 +
  3.1120 +
  3.1121 +subsubsection {* Monotonicity of various operations *}
  3.1122 +
  3.1123 +lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
  3.1124 +  by blast
  3.1125 +
  3.1126 +lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"
  3.1127 +  by blast
  3.1128 +
  3.1129 +lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
  3.1130 +  by blast
  3.1131 +
  3.1132 +lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
  3.1133 +  by blast
  3.1134 +
  3.1135 +lemma UN_mono:
  3.1136 +  "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  3.1137 +    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
  3.1138 +  by (blast dest: subsetD)
  3.1139 +
  3.1140 +lemma INT_anti_mono:
  3.1141 +  "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  3.1142 +    (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
  3.1143 +  -- {* The last inclusion is POSITIVE! *}
  3.1144 +  by (blast dest: subsetD)
  3.1145 +
  3.1146 +lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"
  3.1147 +  by blast
  3.1148 +
  3.1149 +lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
  3.1150 +  by blast
  3.1151 +
  3.1152 +lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
  3.1153 +  by blast
  3.1154 +
  3.1155 +lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
  3.1156 +  by blast
  3.1157 +
  3.1158 +lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
  3.1159 +  by blast
  3.1160 +
  3.1161 +text {* \medskip Monotonicity of implications. *}
  3.1162 +
  3.1163 +lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
  3.1164 +  apply (rule impI)
  3.1165 +  apply (erule subsetD)
  3.1166 +  apply assumption
  3.1167 +  done
  3.1168 +
  3.1169 +lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
  3.1170 +  by rules
  3.1171 +
  3.1172 +lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
  3.1173 +  by rules
  3.1174 +
  3.1175 +lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
  3.1176 +  by rules
  3.1177 +
  3.1178 +lemma imp_refl: "P --> P" ..
  3.1179 +
  3.1180 +lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
  3.1181 +  by rules
  3.1182 +
  3.1183 +lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
  3.1184 +  by rules
  3.1185 +
  3.1186 +lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
  3.1187 +  by blast
  3.1188 +
  3.1189 +lemma Int_Collect_mono:
  3.1190 +    "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
  3.1191 +  by blast
  3.1192 +
  3.1193 +lemmas basic_monos =
  3.1194 +  subset_refl imp_refl disj_mono conj_mono
  3.1195 +  ex_mono Collect_mono in_mono
  3.1196 +
  3.1197 +lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
  3.1198 +  by rules
  3.1199 +
  3.1200 +lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
  3.1201 +  by rules
  3.1202  
  3.1203  lemma Least_mono:
  3.1204    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
  3.1205 @@ -972,7 +1858,7 @@
  3.1206    -- {* NOT suitable for rewriting *}
  3.1207    by blast
  3.1208  
  3.1209 -lemma vimage_mono: "A <= B ==> f -` A <= f -` B"
  3.1210 +lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
  3.1211    -- {* monotonicity *}
  3.1212    by blast
  3.1213  
  3.1214 @@ -985,10 +1871,10 @@
  3.1215  lemma back_subst: "P a ==> a = b ==> P b"
  3.1216    by (rule subst)
  3.1217  
  3.1218 -lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
  3.1219 +lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
  3.1220    by (rule subsetD)
  3.1221  
  3.1222 -lemma set_mp: "A <= B ==> x:A ==> x:B"
  3.1223 +lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
  3.1224    by (rule subsetD)
  3.1225  
  3.1226  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";