src/HOL/Set.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 18413 50c0c118e96d
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 
     2 (* legacy ML bindings *)
     3 
     4 val Ball_def = thm "Ball_def";
     5 val Bex_def = thm "Bex_def";
     6 val CollectD = thm "CollectD";
     7 val CollectE = thm "CollectE";
     8 val CollectI = thm "CollectI";
     9 val Collect_all_eq = thm "Collect_all_eq";
    10 val Collect_ball_eq = thm "Collect_ball_eq";
    11 val Collect_bex_eq = thm "Collect_bex_eq";
    12 val Collect_cong = thm "Collect_cong";
    13 val Collect_conj_eq = thm "Collect_conj_eq";
    14 val Collect_const = thm "Collect_const";
    15 val Collect_disj_eq = thm "Collect_disj_eq";
    16 val Collect_empty_eq = thm "Collect_empty_eq";
    17 val Collect_ex_eq = thm "Collect_ex_eq";
    18 val Collect_mem_eq = thm "Collect_mem_eq";
    19 val Collect_mono = thm "Collect_mono";
    20 val Collect_neg_eq = thm "Collect_neg_eq";
    21 val ComplD = thm "ComplD";
    22 val ComplE = thm "ComplE";
    23 val ComplI = thm "ComplI";
    24 val Compl_Diff_eq = thm "Compl_Diff_eq";
    25 val Compl_INT = thm "Compl_INT";
    26 val Compl_Int = thm "Compl_Int";
    27 val Compl_UN = thm "Compl_UN";
    28 val Compl_UNIV_eq = thm "Compl_UNIV_eq";
    29 val Compl_Un = thm "Compl_Un";
    30 val Compl_anti_mono = thm "Compl_anti_mono";
    31 val Compl_def = thm "Compl_def";
    32 val Compl_disjoint = thm "Compl_disjoint";
    33 val Compl_disjoint2 = thm "Compl_disjoint2";
    34 val Compl_empty_eq = thm "Compl_empty_eq";
    35 val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff";
    36 val Compl_iff = thm "Compl_iff";
    37 val Compl_partition = thm "Compl_partition";
    38 val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff";
    39 val DiffD1 = thm "DiffD1";
    40 val DiffD2 = thm "DiffD2";
    41 val DiffE = thm "DiffE";
    42 val DiffI = thm "DiffI";
    43 val Diff_Compl = thm "Diff_Compl";
    44 val Diff_Int = thm "Diff_Int";
    45 val Diff_Int_distrib = thm "Diff_Int_distrib";
    46 val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
    47 val Diff_UNIV = thm "Diff_UNIV";
    48 val Diff_Un = thm "Diff_Un";
    49 val Diff_cancel = thm "Diff_cancel";
    50 val Diff_disjoint = thm "Diff_disjoint";
    51 val Diff_empty = thm "Diff_empty";
    52 val Diff_eq = thm "Diff_eq";
    53 val Diff_eq_empty_iff = thm "Diff_eq_empty_iff";
    54 val Diff_iff = thm "Diff_iff";
    55 val Diff_insert = thm "Diff_insert";
    56 val Diff_insert0 = thm "Diff_insert0";
    57 val Diff_insert2 = thm "Diff_insert2";
    58 val Diff_insert_absorb = thm "Diff_insert_absorb";
    59 val Diff_mono = thm "Diff_mono";
    60 val Diff_partition = thm "Diff_partition";
    61 val Diff_subset = thm "Diff_subset";
    62 val Diff_triv = thm "Diff_triv";
    63 val INTER_def = thm "INTER_def";
    64 val INT_D = thm "INT_D";
    65 val INT_E = thm "INT_E";
    66 val INT_I = thm "INT_I";
    67 val INT_Int_distrib = thm "INT_Int_distrib";
    68 val INT_Un = thm "INT_Un";
    69 val INT_absorb = thm "INT_absorb";
    70 val INT_anti_mono = thm "INT_anti_mono";
    71 val INT_bool_eq = thm "INT_bool_eq";
    72 val INT_cong = thm "INT_cong";
    73 val INT_constant = thm "INT_constant";
    74 val INT_empty = thm "INT_empty";
    75 val INT_eq = thm "INT_eq";
    76 val INT_greatest = thm "INT_greatest";
    77 val INT_iff = thm "INT_iff";
    78 val INT_insert = thm "INT_insert";
    79 val INT_insert_distrib = thm "INT_insert_distrib";
    80 val INT_lower = thm "INT_lower";
    81 val INT_simps = thms "INT_simps";
    82 val INT_subset_iff = thm "INT_subset_iff";
    83 val IntD1 = thm "IntD1";
    84 val IntD2 = thm "IntD2";
    85 val IntE = thm "IntE";
    86 val IntI = thm "IntI";
    87 val Int_Collect = thm "Int_Collect";
    88 val Int_Collect_mono = thm "Int_Collect_mono";
    89 val Int_Diff = thm "Int_Diff";
    90 val Int_Inter_image = thm "Int_Inter_image";
    91 val Int_UNIV = thm "Int_UNIV";
    92 val Int_UNIV_left = thm "Int_UNIV_left";
    93 val Int_UNIV_right = thm "Int_UNIV_right";
    94 val Int_UN_distrib = thm "Int_UN_distrib";
    95 val Int_UN_distrib2 = thm "Int_UN_distrib2";
    96 val Int_Un_distrib = thm "Int_Un_distrib";
    97 val Int_Un_distrib2 = thm "Int_Un_distrib2";
    98 val Int_Union = thm "Int_Union";
    99 val Int_Union2 = thm "Int_Union2";
   100 val Int_absorb = thm "Int_absorb";
   101 val Int_absorb1 = thm "Int_absorb1";
   102 val Int_absorb2 = thm "Int_absorb2";
   103 val Int_ac = thms "Int_ac";
   104 val Int_assoc = thm "Int_assoc";
   105 val Int_commute = thm "Int_commute";
   106 val Int_def = thm "Int_def";
   107 val Int_empty_left = thm "Int_empty_left";
   108 val Int_empty_right = thm "Int_empty_right";
   109 val Int_eq_Inter = thm "Int_eq_Inter";
   110 val Int_greatest = thm "Int_greatest";
   111 val Int_iff = thm "Int_iff";
   112 val Int_insert_left = thm "Int_insert_left";
   113 val Int_insert_right = thm "Int_insert_right";
   114 val Int_left_absorb = thm "Int_left_absorb";
   115 val Int_left_commute = thm "Int_left_commute";
   116 val Int_lower1 = thm "Int_lower1";
   117 val Int_lower2 = thm "Int_lower2";
   118 val Int_mono = thm "Int_mono";
   119 val Int_subset_iff = thm "Int_subset_iff";
   120 val InterD = thm "InterD";
   121 val InterE = thm "InterE";
   122 val InterI = thm "InterI";
   123 val Inter_UNIV = thm "Inter_UNIV";
   124 val Inter_Un_distrib = thm "Inter_Un_distrib";
   125 val Inter_Un_subset = thm "Inter_Un_subset";
   126 val Inter_anti_mono = thm "Inter_anti_mono";
   127 val Inter_def = thm "Inter_def";
   128 val Inter_empty = thm "Inter_empty";
   129 val Inter_greatest = thm "Inter_greatest";
   130 val Inter_iff = thm "Inter_iff";
   131 val Inter_image_eq = thm "Inter_image_eq";
   132 val Inter_insert = thm "Inter_insert";
   133 val Inter_lower = thm "Inter_lower";
   134 val PowD = thm "PowD";
   135 val PowI = thm "PowI";
   136 val Pow_Compl = thm "Pow_Compl";
   137 val Pow_INT_eq = thm "Pow_INT_eq";
   138 val Pow_Int_eq = thm "Pow_Int_eq";
   139 val Pow_UNIV = thm "Pow_UNIV";
   140 val Pow_bottom = thm "Pow_bottom";
   141 val Pow_def = thm "Pow_def";
   142 val Pow_empty = thm "Pow_empty";
   143 val Pow_iff = thm "Pow_iff";
   144 val Pow_insert = thm "Pow_insert";
   145 val Pow_mono = thm "Pow_mono";
   146 val Pow_top = thm "Pow_top";
   147 val UNION_def = thm "UNION_def";
   148 val UNIV_I = thm "UNIV_I";
   149 val UNIV_def = thm "UNIV_def";
   150 val UNIV_not_empty = thm "UNIV_not_empty";
   151 val UNIV_witness = thm "UNIV_witness";
   152 val UN_E = thm "UN_E";
   153 val UN_I = thm "UN_I";
   154 val UN_Pow_subset = thm "UN_Pow_subset";
   155 val UN_UN_flatten = thm "UN_UN_flatten";
   156 val UN_Un = thm "UN_Un";
   157 val UN_Un_distrib = thm "UN_Un_distrib";
   158 val UN_absorb = thm "UN_absorb";
   159 val UN_bool_eq = thm "UN_bool_eq";
   160 val UN_cong = thm "UN_cong";
   161 val UN_constant = thm "UN_constant";
   162 val UN_empty = thm "UN_empty";
   163 val UN_empty2 = thm "UN_empty2";
   164 val UN_eq = thm "UN_eq";
   165 val UN_iff = thm "UN_iff";
   166 val UN_insert = thm "UN_insert";
   167 val UN_insert_distrib = thm "UN_insert_distrib";
   168 val UN_least = thm "UN_least";
   169 val UN_mono = thm "UN_mono";
   170 val UN_simps = thms "UN_simps";
   171 val UN_singleton = thm "UN_singleton";
   172 val UN_subset_iff = thm "UN_subset_iff";
   173 val UN_upper = thm "UN_upper";
   174 val UnCI = thm "UnCI";
   175 val UnE = thm "UnE";
   176 val UnI1 = thm "UnI1";
   177 val UnI2 = thm "UnI2";
   178 val Un_Diff = thm "Un_Diff";
   179 val Un_Diff_Int = thm "Un_Diff_Int";
   180 val Un_Diff_cancel = thm "Un_Diff_cancel";
   181 val Un_Diff_cancel2 = thm "Un_Diff_cancel2";
   182 val Un_INT_distrib = thm "Un_INT_distrib";
   183 val Un_INT_distrib2 = thm "Un_INT_distrib2";
   184 val Un_Int_assoc_eq = thm "Un_Int_assoc_eq";
   185 val Un_Int_crazy = thm "Un_Int_crazy";
   186 val Un_Int_distrib = thm "Un_Int_distrib";
   187 val Un_Int_distrib2 = thm "Un_Int_distrib2";
   188 val Un_Inter = thm "Un_Inter";
   189 val Un_Pow_subset = thm "Un_Pow_subset";
   190 val Un_UNIV_left = thm "Un_UNIV_left";
   191 val Un_UNIV_right = thm "Un_UNIV_right";
   192 val Un_Union_image = thm "Un_Union_image";
   193 val Un_absorb = thm "Un_absorb";
   194 val Un_absorb1 = thm "Un_absorb1";
   195 val Un_absorb2 = thm "Un_absorb2";
   196 val Un_ac = thms "Un_ac";
   197 val Un_assoc = thm "Un_assoc";
   198 val Un_commute = thm "Un_commute";
   199 val Un_def = thm "Un_def";
   200 val Un_empty = thm "Un_empty";
   201 val Un_empty_left = thm "Un_empty_left";
   202 val Un_empty_right = thm "Un_empty_right";
   203 val Un_eq_UN = thm "Un_eq_UN";
   204 val Un_eq_Union = thm "Un_eq_Union";
   205 val Un_iff = thm "Un_iff";
   206 val Un_insert_left = thm "Un_insert_left";
   207 val Un_insert_right = thm "Un_insert_right";
   208 val Un_least = thm "Un_least";
   209 val Un_left_absorb = thm "Un_left_absorb";
   210 val Un_left_commute = thm "Un_left_commute";
   211 val Un_mono = thm "Un_mono";
   212 val Un_subset_iff = thm "Un_subset_iff";
   213 val Un_upper1 = thm "Un_upper1";
   214 val Un_upper2 = thm "Un_upper2";
   215 val UnionE = thm "UnionE";
   216 val UnionI = thm "UnionI";
   217 val Union_Int_subset = thm "Union_Int_subset";
   218 val Union_Pow_eq = thm "Union_Pow_eq";
   219 val Union_UNIV = thm "Union_UNIV";
   220 val Union_Un_distrib = thm "Union_Un_distrib";
   221 val Union_def = thm "Union_def";
   222 val Union_disjoint = thm "Union_disjoint";
   223 val Union_empty = thm "Union_empty";
   224 val Union_empty_conv = thm "Union_empty_conv";
   225 val Union_iff = thm "Union_iff";
   226 val Union_image_eq = thm "Union_image_eq";
   227 val Union_insert = thm "Union_insert";
   228 val Union_least = thm "Union_least";
   229 val Union_mono = thm "Union_mono";
   230 val Union_upper = thm "Union_upper";
   231 val all_bool_eq = thm "all_bool_eq";
   232 val all_mono = thm "all_mono";
   233 val all_not_in_conv = thm "all_not_in_conv";
   234 val atomize_ball = thm "atomize_ball";
   235 val ballE = thm "ballE";
   236 val ballI = thm "ballI";
   237 val ball_UN = thm "ball_UN";
   238 val ball_UNIV = thm "ball_UNIV";
   239 val ball_Un = thm "ball_Un";
   240 val ball_cong = thm "ball_cong";
   241 val ball_conj_distrib = thm "ball_conj_distrib";
   242 val ball_empty = thm "ball_empty";
   243 val ball_one_point1 = thm "ball_one_point1";
   244 val ball_one_point2 = thm "ball_one_point2";
   245 val ball_simps = thms "ball_simps";
   246 val ball_triv = thm "ball_triv";
   247 val basic_monos = thms "basic_monos";
   248 val bexCI = thm "bexCI";
   249 val bexE = thm "bexE";
   250 val bexI = thm "bexI";
   251 val bex_UN = thm "bex_UN";
   252 val bex_UNIV = thm "bex_UNIV";
   253 val bex_Un = thm "bex_Un";
   254 val bex_cong = thm "bex_cong";
   255 val bex_disj_distrib = thm "bex_disj_distrib";
   256 val bex_empty = thm "bex_empty";
   257 val bex_one_point1 = thm "bex_one_point1";
   258 val bex_one_point2 = thm "bex_one_point2";
   259 val bex_simps = thms "bex_simps";
   260 val bex_triv = thm "bex_triv";
   261 val bex_triv_one_point1 = thm "bex_triv_one_point1";
   262 val bex_triv_one_point2 = thm "bex_triv_one_point2";
   263 val bool_induct = thm "bool_induct";
   264 val bspec = thm "bspec";
   265 val conj_mono = thm "conj_mono";
   266 val contra_subsetD = thm "contra_subsetD";
   267 val diff_single_insert = thm "diff_single_insert";
   268 val disj_mono = thm "disj_mono";
   269 val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl";
   270 val disjoint_iff_not_equal = thm "disjoint_iff_not_equal";
   271 val distinct_lemma = thm "distinct_lemma";
   272 val double_complement = thm "double_complement";
   273 val double_diff = thm "double_diff";
   274 val emptyE = thm "emptyE";
   275 val empty_Diff = thm "empty_Diff";
   276 val empty_def = thm "empty_def";
   277 val empty_iff = thm "empty_iff";
   278 val empty_subsetI = thm "empty_subsetI";
   279 val eq_to_mono = thm "eq_to_mono";
   280 val eq_to_mono2 = thm "eq_to_mono2";
   281 val eqset_imp_iff = thm "eqset_imp_iff";
   282 val equalityCE = thm "equalityCE";
   283 val equalityD1 = thm "equalityD1";
   284 val equalityD2 = thm "equalityD2";
   285 val equalityE = thm "equalityE";
   286 val equalityI = thm "equalityI";
   287 val equals0D = thm "equals0D";
   288 val equals0I = thm "equals0I";
   289 val ex_bool_eq = thm "ex_bool_eq";
   290 val ex_mono = thm "ex_mono";
   291 val full_SetCompr_eq = thm "full_SetCompr_eq";
   292 val if_image_distrib = thm "if_image_distrib";
   293 val imageE = thm "imageE";
   294 val imageI = thm "imageI";
   295 val image_Collect = thm "image_Collect";
   296 val image_Un = thm "image_Un";
   297 val image_Union = thm "image_Union";
   298 val image_cong = thm "image_cong";
   299 val image_constant = thm "image_constant";
   300 val image_def = thm "image_def";
   301 val image_empty = thm "image_empty";
   302 val image_eqI = thm "image_eqI";
   303 val image_iff = thm "image_iff";
   304 val image_image = thm "image_image";
   305 val image_insert = thm "image_insert";
   306 val image_is_empty = thm "image_is_empty";
   307 val image_mono = thm "image_mono";
   308 val image_subsetI = thm "image_subsetI";
   309 val image_subset_iff = thm "image_subset_iff";
   310 val imp_mono = thm "imp_mono";
   311 val imp_refl = thm "imp_refl";
   312 val in_mono = thm "in_mono";
   313 val insertCI = thm "insertCI";
   314 val insertE = thm "insertE";
   315 val insertI1 = thm "insertI1";
   316 val insertI2 = thm "insertI2";
   317 val insert_Collect = thm "insert_Collect";
   318 val insert_Diff = thm "insert_Diff";
   319 val insert_Diff1 = thm "insert_Diff1";
   320 val insert_Diff_if = thm "insert_Diff_if";
   321 val insert_absorb = thm "insert_absorb";
   322 val insert_absorb2 = thm "insert_absorb2";
   323 val insert_commute = thm "insert_commute";
   324 val insert_def = thm "insert_def";
   325 val insert_iff = thm "insert_iff";
   326 val insert_image = thm "insert_image";
   327 val insert_is_Un = thm "insert_is_Un";
   328 val insert_mono = thm "insert_mono";
   329 val insert_not_empty = thm "insert_not_empty";
   330 val insert_subset = thm "insert_subset";
   331 val mem_Collect_eq = thm "mem_Collect_eq";
   332 val mem_simps = thms "mem_simps";
   333 val mk_disjoint_insert = thm "mk_disjoint_insert";
   334 val mono_Int = thm "mono_Int";
   335 val mono_Un = thm "mono_Un";
   336 val not_psubset_empty = thm "not_psubset_empty";
   337 val psubsetI = thm "psubsetI";
   338 val psubset_def = thm "psubset_def";
   339 val psubset_eq = thm "psubset_eq";
   340 val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
   341 val psubset_imp_subset = thm "psubset_imp_subset";
   342 val psubset_insert_iff = thm "psubset_insert_iff";
   343 val psubset_subset_trans = thm "psubset_subset_trans";
   344 val rangeE = thm "rangeE";
   345 val rangeI = thm "rangeI";
   346 val range_composition = thm "range_composition";
   347 val range_eqI = thm "range_eqI";
   348 val rev_bexI = thm "rev_bexI";
   349 val rev_image_eqI = thm "rev_image_eqI";
   350 val rev_subsetD = thm "rev_subsetD";
   351 val set_diff_def = thm "set_diff_def";
   352 val set_eq_subset = thm "set_eq_subset";
   353 val set_ext = thm "set_ext";
   354 val singletonD = thm "singletonD";
   355 val singletonE = thm "singletonE";
   356 val singletonI = thm "singletonI";
   357 val singleton_conv = thm "singleton_conv";
   358 val singleton_conv2 = thm "singleton_conv2";
   359 val singleton_iff = thm "singleton_iff";
   360 val singleton_inject = thm "singleton_inject";
   361 val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
   362 val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
   363 val split_if_eq1 = thm "split_if_eq1";
   364 val split_if_eq2 = thm "split_if_eq2";
   365 val split_if_mem1 = thm "split_if_mem1";
   366 val split_if_mem2 = thm "split_if_mem2";
   367 val split_ifs = thms "split_ifs";
   368 val strip = thms "strip";
   369 val subsetCE = thm "subsetCE";
   370 val subsetD = thm "subsetD";
   371 val subsetI = thm "subsetI";
   372 val subset_Compl_self_eq = thm "subset_Compl_self_eq";
   373 val subset_Pow_Union = thm "subset_Pow_Union";
   374 val subset_UNIV = thm "subset_UNIV";
   375 val subset_Un_eq = thm "subset_Un_eq";
   376 val subset_antisym = thm "subset_antisym";
   377 val subset_def = thm "subset_def";
   378 val subset_empty = thm "subset_empty";
   379 val subset_iff = thm "subset_iff";
   380 val subset_iff_psubset_eq = thm "subset_iff_psubset_eq";
   381 val subset_image_iff = thm "subset_image_iff";
   382 val subset_insert = thm "subset_insert";
   383 val subset_insertI = thm "subset_insertI";
   384 val subset_insert_iff = thm "subset_insert_iff";
   385 val subset_psubset_trans = thm "subset_psubset_trans";
   386 val subset_refl = thm "subset_refl";
   387 val subset_singletonD = thm "subset_singletonD";
   388 val subset_trans = thm "subset_trans";
   389 val vimageD = thm "vimageD";
   390 val vimageE = thm "vimageE";
   391 val vimageI = thm "vimageI";
   392 val vimageI2 = thm "vimageI2";
   393 val vimage_Collect = thm "vimage_Collect";
   394 val vimage_Collect_eq = thm "vimage_Collect_eq";
   395 val vimage_Compl = thm "vimage_Compl";
   396 val vimage_Diff = thm "vimage_Diff";
   397 val vimage_INT = thm "vimage_INT";
   398 val vimage_Int = thm "vimage_Int";
   399 val vimage_UN = thm "vimage_UN";
   400 val vimage_UNIV = thm "vimage_UNIV";
   401 val vimage_Un = thm "vimage_Un";
   402 val vimage_Union = thm "vimage_Union";
   403 val vimage_def = thm "vimage_def";
   404 val vimage_empty = thm "vimage_empty";
   405 val vimage_eq = thm "vimage_eq";
   406 val vimage_eq_UN = thm "vimage_eq_UN";
   407 val vimage_insert = thm "vimage_insert";
   408 val vimage_mono = thm "vimage_mono";
   409 val vimage_singleton_eq = thm "vimage_singleton_eq";
   410 
   411 structure Set =
   412 struct
   413   val thy = the_context ();
   414   val Ball_def = Ball_def;
   415   val Bex_def = Bex_def;
   416   val Collect_mem_eq = Collect_mem_eq;
   417   val Compl_def = Compl_def;
   418   val INTER_def = INTER_def;
   419   val Int_def = Int_def;
   420   val Inter_def = Inter_def;
   421   val Pow_def = Pow_def;
   422   val UNION_def = UNION_def;
   423   val UNIV_def = UNIV_def;
   424   val Un_def = Un_def;
   425   val Union_def = Union_def;
   426   val empty_def = empty_def;
   427   val image_def = image_def;
   428   val insert_def = insert_def;
   429   val mem_Collect_eq = mem_Collect_eq;
   430   val psubset_def = psubset_def;
   431   val set_diff_def = set_diff_def;
   432   val subset_def = subset_def;
   433 end;