src/HOL/Set.thy
author wenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114 a8e860c86252
parent 12023 d982f98e0f0d
child 12257 e3f7d6fb55d7
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
     1 (*  Title:      HOL/Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Set theory for higher-order logic *}
     8 
     9 theory Set = HOL
    10 files ("subset.ML") ("equalities.ML") ("mono.ML"):
    11 
    12 text {* A set in HOL is simply a predicate. *}
    13 
    14 
    15 subsection {* Basic syntax *}
    16 
    17 global
    18 
    19 typedecl 'a set
    20 arities set :: ("term") "term"
    21 
    22 consts
    23   "{}"          :: "'a set"                             ("{}")
    24   UNIV          :: "'a set"
    25   insert        :: "'a => 'a set => 'a set"
    26   Collect       :: "('a => bool) => 'a set"              -- "comprehension"
    27   Int           :: "'a set => 'a set => 'a set"          (infixl 70)
    28   Un            :: "'a set => 'a set => 'a set"          (infixl 65)
    29   UNION         :: "'a set => ('a => 'b set) => 'b set"  -- "general union"
    30   INTER         :: "'a set => ('a => 'b set) => 'b set"  -- "general intersection"
    31   Union         :: "'a set set => 'a set"                -- "union of a set"
    32   Inter         :: "'a set set => 'a set"                -- "intersection of a set"
    33   Pow           :: "'a set => 'a set set"                -- "powerset"
    34   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    35   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    36   image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
    37 
    38 syntax
    39   "op :"        :: "'a => 'a set => bool"                ("op :")
    40 consts
    41   "op :"        :: "'a => 'a set => bool"                ("(_/ : _)" [50, 51] 50)  -- "membership"
    42 
    43 local
    44 
    45 instance set :: ("term") ord ..
    46 instance set :: ("term") minus ..
    47 
    48 
    49 subsection {* Additional concrete syntax *}
    50 
    51 syntax
    52   range         :: "('a => 'b) => 'b set"             -- "of function"
    53 
    54   "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
    55   "op ~:"       :: "'a => 'a set => bool"                 ("(_/ ~: _)" [50, 51] 50)
    56 
    57   "@Finset"     :: "args => 'a set"                       ("{(_)}")
    58   "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
    59   "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
    60 
    61   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" 10)
    62   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" 10)
    63   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" 10)
    64   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" 10)
    65 
    66   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    67   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
    68 
    69 syntax (HOL)
    70   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
    71   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
    72 
    73 translations
    74   "range f"     == "f`UNIV"
    75   "x ~: y"      == "~ (x : y)"
    76   "{x, xs}"     == "insert x {xs}"
    77   "{x}"         == "insert x {}"
    78   "{x. P}"      == "Collect (%x. P)"
    79   "UN x y. B"   == "UN x. UN y. B"
    80   "UN x. B"     == "UNION UNIV (%x. B)"
    81   "INT x y. B"  == "INT x. INT y. B"
    82   "INT x. B"    == "INTER UNIV (%x. B)"
    83   "UN x:A. B"   == "UNION A (%x. B)"
    84   "INT x:A. B"  == "INTER A (%x. B)"
    85   "ALL x:A. P"  == "Ball A (%x. P)"
    86   "EX x:A. P"   == "Bex A (%x. P)"
    87 
    88 syntax ("" output)
    89   "_setle"      :: "'a set => 'a set => bool"             ("op <=")
    90   "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
    91   "_setless"    :: "'a set => 'a set => bool"             ("op <")
    92   "_setless"    :: "'a set => 'a set => bool"             ("(_/ < _)" [50, 51] 50)
    93 
    94 syntax (xsymbols)
    95   "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
    96   "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
    97   "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
    98   "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
    99   "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
   100   "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
   101   "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
   102   "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
   103   "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
   104   "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
   105   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
   106   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
   107   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
   108   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
   109   Union         :: "'a set set => 'a set"                 ("\<Union>_" [90] 90)
   110   Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
   111   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   112   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   113 
   114 translations
   115   "op \<subseteq>" => "op <= :: _ set => _ set => bool"
   116   "op \<subset>" => "op <  :: _ set => _ set => bool"
   117 
   118 
   119 typed_print_translation {*
   120   let
   121     fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
   122           list_comb (Syntax.const "_setle", ts)
   123       | le_tr' _ _ _ = raise Match;
   124 
   125     fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
   126           list_comb (Syntax.const "_setless", ts)
   127       | less_tr' _ _ _ = raise Match;
   128   in [("op <=", le_tr'), ("op <", less_tr')] end
   129 *}
   130 
   131 text {*
   132   \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
   133   "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is
   134   only translated if @{text "[0..n] subset bvs(e)"}.
   135 *}
   136 
   137 parse_translation {*
   138   let
   139     val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
   140 
   141     fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1
   142       | nvars _ = 1;
   143 
   144     fun setcompr_tr [e, idts, b] =
   145       let
   146         val eq = Syntax.const "op =" $ Bound (nvars idts) $ e;
   147         val P = Syntax.const "op &" $ eq $ b;
   148         val exP = ex_tr [idts, P];
   149       in Syntax.const "Collect" $ Abs ("", dummyT, exP) end;
   150 
   151   in [("@SetCompr", setcompr_tr)] end;
   152 *}
   153 
   154 print_translation {*
   155   let
   156     val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
   157 
   158     fun setcompr_tr' [Abs (_, _, P)] =
   159       let
   160         fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
   161           | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
   162               if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
   163                 ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then ()
   164               else raise Match;
   165 
   166         fun tr' (_ $ abs) =
   167           let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
   168           in Syntax.const "@SetCompr" $ e $ idts $ Q end;
   169       in check (P, 0); tr' P end;
   170   in [("Collect", setcompr_tr')] end;
   171 *}
   172 
   173 
   174 subsection {* Rules and definitions *}
   175 
   176 text {* Isomorphisms between predicates and sets. *}
   177 
   178 axioms
   179   mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
   180   Collect_mem_eq [simp]: "{x. x:A} = A"
   181 
   182 defs
   183   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   184   Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   185 
   186 defs (overloaded)
   187   subset_def:   "A <= B         == ALL x:A. x:B"
   188   psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B"
   189   Compl_def:    "- A            == {x. ~x:A}"
   190 
   191 defs
   192   Un_def:       "A Un B         == {x. x:A | x:B}"
   193   Int_def:      "A Int B        == {x. x:A & x:B}"
   194   set_diff_def: "A - B          == {x. x:A & ~x:B}"
   195   INTER_def:    "INTER A B      == {y. ALL x:A. y: B(x)}"
   196   UNION_def:    "UNION A B      == {y. EX x:A. y: B(x)}"
   197   Inter_def:    "Inter S        == (INT x:S. x)"
   198   Union_def:    "Union S        == (UN x:S. x)"
   199   Pow_def:      "Pow A          == {B. B <= A}"
   200   empty_def:    "{}             == {x. False}"
   201   UNIV_def:     "UNIV           == {x. True}"
   202   insert_def:   "insert a B     == {x. x=a} Un B"
   203   image_def:    "f`A            == {y. EX x:A. y = f(x)}"
   204 
   205 
   206 subsection {* Lemmas and proof tool setup *}
   207 
   208 subsubsection {* Relating predicates and sets *}
   209 
   210 lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}"
   211   by simp
   212 
   213 lemma CollectD: "a : {x. P(x)} ==> P(a)"
   214   by simp
   215 
   216 lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B"
   217 proof -
   218   case rule_context
   219   show ?thesis
   220     apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals])
   221      apply (rule Collect_mem_eq)
   222     apply (rule Collect_mem_eq)
   223     done
   224 qed
   225 
   226 lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
   227   by simp
   228 
   229 lemmas CollectE [elim!] = CollectD [elim_format]
   230 
   231 
   232 subsubsection {* Bounded quantifiers *}
   233 
   234 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
   235   by (simp add: Ball_def)
   236 
   237 lemmas strip = impI allI ballI
   238 
   239 lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
   240   by (simp add: Ball_def)
   241 
   242 lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
   243   by (unfold Ball_def) blast
   244 
   245 text {*
   246   \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
   247   @{prop "a:A"}; creates assumption @{prop "P a"}.
   248 *}
   249 
   250 ML {*
   251   local val ballE = thm "ballE"
   252   in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end;
   253 *}
   254 
   255 text {*
   256   Gives better instantiation for bound:
   257 *}
   258 
   259 ML_setup {*
   260   claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1);
   261 *}
   262 
   263 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   264   -- {* Normally the best argument order: @{prop "P x"} constrains the
   265     choice of @{prop "x:A"}. *}
   266   by (unfold Bex_def) blast
   267 
   268 lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x"
   269   -- {* The best argument order when there is only one @{prop "x:A"}. *}
   270   by (unfold Bex_def) blast
   271 
   272 lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"
   273   by (unfold Bex_def) blast
   274 
   275 lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q"
   276   by (unfold Bex_def) blast
   277 
   278 lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"
   279   -- {* Trival rewrite rule. *}
   280   by (simp add: Ball_def)
   281 
   282 lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"
   283   -- {* Dual form for existentials. *}
   284   by (simp add: Bex_def)
   285 
   286 lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"
   287   by blast
   288 
   289 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
   290   by blast
   291 
   292 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
   293   by blast
   294 
   295 lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)"
   296   by blast
   297 
   298 lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)"
   299   by blast
   300 
   301 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   302   by blast
   303 
   304 ML_setup {*
   305   let
   306     val Ball_def = thm "Ball_def";
   307     val Bex_def = thm "Bex_def";
   308 
   309     val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   310       ("EX x:A. P x & Q x", HOLogic.boolT);
   311 
   312     val prove_bex_tac =
   313       rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
   314     val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   315 
   316     val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   317       ("ALL x:A. P x --> Q x", HOLogic.boolT);
   318 
   319     val prove_ball_tac =
   320       rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
   321     val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   322 
   323     val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
   324     val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
   325   in
   326     Addsimprocs [defBALL_regroup, defBEX_regroup]
   327   end;
   328 *}
   329 
   330 
   331 subsubsection {* Congruence rules *}
   332 
   333 lemma ball_cong [cong]:
   334   "A = B ==> (!!x. x:B ==> P x = Q x) ==>
   335     (ALL x:A. P x) = (ALL x:B. Q x)"
   336   by (simp add: Ball_def)
   337 
   338 lemma bex_cong [cong]:
   339   "A = B ==> (!!x. x:B ==> P x = Q x) ==>
   340     (EX x:A. P x) = (EX x:B. Q x)"
   341   by (simp add: Bex_def cong: conj_cong)
   342 
   343 
   344 subsubsection {* Subsets *}
   345 
   346 lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B"
   347   by (simp add: subset_def)
   348 
   349 text {*
   350   \medskip Map the type @{text "'a set => anything"} to just @{typ
   351   'a}; for overloading constants whose first argument has type @{typ
   352   "'a set"}.
   353 *}
   354 
   355 ML {*
   356   fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
   357 *}
   358 
   359 ML "
   360   (* While (:) is not, its type must be kept
   361     for overloading of = to work. *)
   362   Blast.overloaded (\"op :\", domain_type);
   363 
   364   overload_1st_set \"Ball\";            (*need UNION, INTER also?*)
   365   overload_1st_set \"Bex\";
   366 
   367   (*Image: retain the type of the set being expressed*)
   368   Blast.overloaded (\"image\", domain_type);
   369 "
   370 
   371 lemma subsetD [elim]: "A <= B ==> c:A ==> c:B"
   372   -- {* Rule in Modus Ponens style. *}
   373   by (unfold subset_def) blast
   374 
   375 declare subsetD [intro?] -- FIXME
   376 
   377 lemma rev_subsetD: "c:A ==> A <= B ==> c:B"
   378   -- {* The same, with reversed premises for use with @{text erule} --
   379       cf @{text rev_mp}. *}
   380   by (rule subsetD)
   381 
   382 declare rev_subsetD [intro?] -- FIXME
   383 
   384 text {*
   385   \medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}.
   386 *}
   387 
   388 ML {*
   389   local val rev_subsetD = thm "rev_subsetD"
   390   in fun impOfSubs th = th RSN (2, rev_subsetD) end;
   391 *}
   392 
   393 lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P"
   394   -- {* Classical elimination rule. *}
   395   by (unfold subset_def) blast
   396 
   397 text {*
   398   \medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and
   399   creates the assumption @{prop "c:B"}.
   400 *}
   401 
   402 ML {*
   403   local val subsetCE = thm "subsetCE"
   404   in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;
   405 *}
   406 
   407 lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A"
   408   by blast
   409 
   410 lemma subset_refl: "A <= (A::'a set)"
   411   by fast
   412 
   413 lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)"
   414   by blast
   415 
   416 
   417 subsubsection {* Equality *}
   418 
   419 lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)"
   420   -- {* Anti-symmetry of the subset relation. *}
   421   by (rule set_ext) (blast intro: subsetD)
   422 
   423 lemmas equalityI = subset_antisym
   424 
   425 text {*
   426   \medskip Equality rules from ZF set theory -- are they appropriate
   427   here?
   428 *}
   429 
   430 lemma equalityD1: "A = B ==> A <= (B::'a set)"
   431   by (simp add: subset_refl)
   432 
   433 lemma equalityD2: "A = B ==> B <= (A::'a set)"
   434   by (simp add: subset_refl)
   435 
   436 text {*
   437   \medskip Be careful when adding this to the claset as @{text
   438   subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
   439   <= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}!
   440 *}
   441 
   442 lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P"
   443   by (simp add: subset_refl)
   444 
   445 lemma equalityCE [elim]:
   446     "A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P"
   447   by blast
   448 
   449 text {*
   450   \medskip Lemma for creating induction formulae -- for "pattern
   451   matching" on @{text p}.  To make the induction hypotheses usable,
   452   apply @{text spec} or @{text bspec} to put universal quantifiers over the free
   453   variables in @{text p}.
   454 *}
   455 
   456 lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R"
   457   by simp
   458 
   459 lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
   460   by simp
   461 
   462 
   463 subsubsection {* The universal set -- UNIV *}
   464 
   465 lemma UNIV_I [simp]: "x : UNIV"
   466   by (simp add: UNIV_def)
   467 
   468 declare UNIV_I [intro]  -- {* unsafe makes it less likely to cause problems *}
   469 
   470 lemma UNIV_witness [intro?]: "EX x. x : UNIV"
   471   by simp
   472 
   473 lemma subset_UNIV: "A <= UNIV"
   474   by (rule subsetI) (rule UNIV_I)
   475 
   476 text {*
   477   \medskip Eta-contracting these two rules (to remove @{text P})
   478   causes them to be ignored because of their interaction with
   479   congruence rules.
   480 *}
   481 
   482 lemma ball_UNIV [simp]: "Ball UNIV P = All P"
   483   by (simp add: Ball_def)
   484 
   485 lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
   486   by (simp add: Bex_def)
   487 
   488 
   489 subsubsection {* The empty set *}
   490 
   491 lemma empty_iff [simp]: "(c : {}) = False"
   492   by (simp add: empty_def)
   493 
   494 lemma emptyE [elim!]: "a : {} ==> P"
   495   by simp
   496 
   497 lemma empty_subsetI [iff]: "{} <= A"
   498     -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
   499   by blast
   500 
   501 lemma equals0I: "(!!y. y:A ==> False) ==> A = {}"
   502   by blast
   503 
   504 lemma equals0D: "A={} ==> a ~: A"
   505     -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
   506   by blast
   507 
   508 lemma ball_empty [simp]: "Ball {} P = True"
   509   by (simp add: Ball_def)
   510 
   511 lemma bex_empty [simp]: "Bex {} P = False"
   512   by (simp add: Bex_def)
   513 
   514 lemma UNIV_not_empty [iff]: "UNIV ~= {}"
   515   by (blast elim: equalityE)
   516 
   517 
   518 subsubsection {* The Powerset operator -- Pow *}
   519 
   520 lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
   521   by (simp add: Pow_def)
   522 
   523 lemma PowI: "A <= B ==> A : Pow B"
   524   by (simp add: Pow_def)
   525 
   526 lemma PowD: "A : Pow B ==> A <= B"
   527   by (simp add: Pow_def)
   528 
   529 lemma Pow_bottom: "{}: Pow B"
   530   by simp
   531 
   532 lemma Pow_top: "A : Pow A"
   533   by (simp add: subset_refl)
   534 
   535 
   536 subsubsection {* Set complement *}
   537 
   538 lemma Compl_iff [simp]: "(c : -A) = (c~:A)"
   539   by (unfold Compl_def) blast
   540 
   541 lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A"
   542   by (unfold Compl_def) blast
   543 
   544 text {*
   545   \medskip This form, with negated conclusion, works well with the
   546   Classical prover.  Negated assumptions behave like formulae on the
   547   right side of the notional turnstile ... *}
   548 
   549 lemma ComplD: "c : -A ==> c~:A"
   550   by (unfold Compl_def) blast
   551 
   552 lemmas ComplE [elim!] = ComplD [elim_format]
   553 
   554 
   555 subsubsection {* Binary union -- Un *}
   556 
   557 lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   558   by (unfold Un_def) blast
   559 
   560 lemma UnI1 [elim?]: "c:A ==> c : A Un B"
   561   by simp
   562 
   563 lemma UnI2 [elim?]: "c:B ==> c : A Un B"
   564   by simp
   565 
   566 text {*
   567   \medskip Classical introduction rule: no commitment to @{prop A} vs
   568   @{prop B}.
   569 *}
   570 
   571 lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"
   572   by auto
   573 
   574 lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
   575   by (unfold Un_def) blast
   576 
   577 
   578 subsubsection {* Binary intersection -- Int *}
   579 
   580 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   581   by (unfold Int_def) blast
   582 
   583 lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
   584   by simp
   585 
   586 lemma IntD1: "c : A Int B ==> c:A"
   587   by simp
   588 
   589 lemma IntD2: "c : A Int B ==> c:B"
   590   by simp
   591 
   592 lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
   593   by simp
   594 
   595 
   596 subsubsection {* Set difference *}
   597 
   598 lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
   599   by (unfold set_diff_def) blast
   600 
   601 lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
   602   by simp
   603 
   604 lemma DiffD1: "c : A - B ==> c : A"
   605   by simp
   606 
   607 lemma DiffD2: "c : A - B ==> c : B ==> P"
   608   by simp
   609 
   610 lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"
   611   by simp
   612 
   613 
   614 subsubsection {* Augmenting a set -- insert *}
   615 
   616 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
   617   by (unfold insert_def) blast
   618 
   619 lemma insertI1: "a : insert a B"
   620   by simp
   621 
   622 lemma insertI2: "a : B ==> a : insert b B"
   623   by simp
   624 
   625 lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"
   626   by (unfold insert_def) blast
   627 
   628 lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
   629   -- {* Classical introduction rule. *}
   630   by auto
   631 
   632 lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)"
   633   by auto
   634 
   635 
   636 subsubsection {* Singletons, using insert *}
   637 
   638 lemma singletonI [intro!]: "a : {a}"
   639     -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   640   by (rule insertI1)
   641 
   642 lemma singletonD: "b : {a} ==> b = a"
   643   by blast
   644 
   645 lemmas singletonE [elim!] = singletonD [elim_format]
   646 
   647 lemma singleton_iff: "(b : {a}) = (b = a)"
   648   by blast
   649 
   650 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   651   by blast
   652 
   653 lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})"
   654   by blast
   655 
   656 lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})"
   657   by blast
   658 
   659 lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}"
   660   by fast
   661 
   662 lemma singleton_conv [simp]: "{x. x = a} = {a}"
   663   by blast
   664 
   665 lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
   666   by blast
   667 
   668 lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B"
   669   by blast
   670 
   671 
   672 subsubsection {* Unions of families *}
   673 
   674 text {*
   675   @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
   676 *}
   677 
   678 lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
   679   by (unfold UNION_def) blast
   680 
   681 lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"
   682   -- {* The order of the premises presupposes that @{term A} is rigid;
   683     @{term b} may be flexible. *}
   684   by auto
   685 
   686 lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"
   687   by (unfold UNION_def) blast
   688 
   689 lemma UN_cong [cong]:
   690     "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
   691   by (simp add: UNION_def)
   692 
   693 
   694 subsubsection {* Intersections of families *}
   695 
   696 text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *}
   697 
   698 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
   699   by (unfold INTER_def) blast
   700 
   701 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
   702   by (unfold INTER_def) blast
   703 
   704 lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
   705   by auto
   706 
   707 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
   708   -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
   709   by (unfold INTER_def) blast
   710 
   711 lemma INT_cong [cong]:
   712     "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
   713   by (simp add: INTER_def)
   714 
   715 
   716 subsubsection {* Union *}
   717 
   718 lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)"
   719   by (unfold Union_def) blast
   720 
   721 lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
   722   -- {* The order of the premises presupposes that @{term C} is rigid;
   723     @{term A} may be flexible. *}
   724   by auto
   725 
   726 lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
   727   by (unfold Union_def) blast
   728 
   729 
   730 subsubsection {* Inter *}
   731 
   732 lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)"
   733   by (unfold Inter_def) blast
   734 
   735 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
   736   by (simp add: Inter_def)
   737 
   738 text {*
   739   \medskip A ``destruct'' rule -- every @{term X} in @{term C}
   740   contains @{term A} as an element, but @{prop "A:X"} can hold when
   741   @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
   742 *}
   743 
   744 lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
   745   by auto
   746 
   747 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
   748   -- {* ``Classical'' elimination rule -- does not require proving
   749     @{prop "X:C"}. *}
   750   by (unfold Inter_def) blast
   751 
   752 text {*
   753   \medskip Image of a set under a function.  Frequently @{term b} does
   754   not have the syntactic form of @{term "f x"}.
   755 *}
   756 
   757 lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
   758   by (unfold image_def) blast
   759 
   760 lemma imageI: "x : A ==> f x : f ` A"
   761   by (rule image_eqI) (rule refl)
   762 
   763 lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
   764   -- {* This version's more effective when we already have the
   765     required @{term x}. *}
   766   by (unfold image_def) blast
   767 
   768 lemma imageE [elim!]:
   769   "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
   770   -- {* The eta-expansion gives variable-name preservation. *}
   771   by (unfold image_def) blast
   772 
   773 lemma image_Un: "f`(A Un B) = f`A Un f`B"
   774   by blast
   775 
   776 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   777   by blast
   778 
   779 lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)"
   780   -- {* This rewrite rule would confuse users if made default. *}
   781   by blast
   782 
   783 lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)"
   784   apply safe
   785    prefer 2 apply fast
   786   apply (rule_tac x = "{a. a : A & f a : B}" in exI)
   787   apply fast
   788   done
   789 
   790 lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B"
   791   -- {* Replaces the three steps @{text subsetI}, @{text imageE},
   792     @{text hypsubst}, but breaks too many existing proofs. *}
   793   by blast
   794 
   795 text {*
   796   \medskip Range of a function -- just a translation for image!
   797 *}
   798 
   799 lemma range_eqI: "b = f x ==> b : range f"
   800   by simp
   801 
   802 lemma rangeI: "f x : range f"
   803   by simp
   804 
   805 lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P"
   806   by blast
   807 
   808 
   809 subsubsection {* Set reasoning tools *}
   810 
   811 text {*
   812   Rewrite rules for boolean case-splitting: faster than @{text
   813   "split_if [split]"}.
   814 *}
   815 
   816 lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
   817   by (rule split_if)
   818 
   819 lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
   820   by (rule split_if)
   821 
   822 text {*
   823   Split ifs on either side of the membership relation.  Not for @{text
   824   "[simp]"} -- can cause goals to blow up!
   825 *}
   826 
   827 lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
   828   by (rule split_if)
   829 
   830 lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
   831   by (rule split_if)
   832 
   833 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
   834 
   835 lemmas mem_simps =
   836   insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
   837   mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
   838   -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
   839 
   840 (*Would like to add these, but the existing code only searches for the
   841   outer-level constant, which in this case is just "op :"; we instead need
   842   to use term-nets to associate patterns with rules.  Also, if a rule fails to
   843   apply, then the formula should be kept.
   844   [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]),
   845    ("op Int", [IntD1,IntD2]),
   846    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
   847  *)
   848 
   849 ML_setup {*
   850   val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;
   851   simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
   852 *}
   853 
   854 declare subset_UNIV [simp] subset_refl [simp]
   855 
   856 
   857 subsubsection {* The ``proper subset'' relation *}
   858 
   859 lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B"
   860   by (unfold psubset_def) blast
   861 
   862 lemma psubset_insert_iff:
   863   "(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)"
   864   apply (simp add: psubset_def subset_insert_iff)
   865   apply blast
   866   done
   867 
   868 lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)"
   869   by (simp only: psubset_def)
   870 
   871 lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B"
   872   by (simp add: psubset_eq)
   873 
   874 lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C"
   875   by (auto simp add: psubset_eq)
   876 
   877 lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C"
   878   by (auto simp add: psubset_eq)
   879 
   880 lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)"
   881   by (unfold psubset_def) blast
   882 
   883 lemma atomize_ball:
   884     "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)"
   885   by (simp only: Ball_def atomize_all atomize_imp)
   886 
   887 declare atomize_ball [symmetric, rulify]
   888 
   889 
   890 subsection {* Further set-theory lemmas *}
   891 
   892 use "subset.ML"
   893 use "equalities.ML"
   894 use "mono.ML"
   895 
   896 lemma Least_mono:
   897   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
   898     ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
   899     -- {* Courtesy of Stephan Merz *}
   900   apply clarify
   901   apply (erule_tac P = "%x. x : S" in LeastI2)
   902    apply fast
   903   apply (rule LeastI2)
   904   apply (auto elim: monoD intro!: order_antisym)
   905   done
   906 
   907 
   908 subsection {* Transitivity rules for calculational reasoning *}
   909 
   910 lemma forw_subst: "a = b ==> P b ==> P a"
   911   by (rule ssubst)
   912 
   913 lemma back_subst: "P a ==> a = b ==> P b"
   914   by (rule subst)
   915 
   916 lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
   917   by (rule subsetD)
   918 
   919 lemma set_mp: "A <= B ==> x:A ==> x:B"
   920   by (rule subsetD)
   921 
   922 lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
   923   by (simp add: order_less_le)
   924 
   925 lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
   926   by (simp add: order_less_le)
   927 
   928 lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
   929   by (rule order_less_asym)
   930 
   931 lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
   932   by (rule subst)
   933 
   934 lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
   935   by (rule ssubst)
   936 
   937 lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
   938   by (rule subst)
   939 
   940 lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
   941   by (rule ssubst)
   942 
   943 lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
   944   (!!x y. x < y ==> f x < f y) ==> f a < c"
   945 proof -
   946   assume r: "!!x y. x < y ==> f x < f y"
   947   assume "a < b" hence "f a < f b" by (rule r)
   948   also assume "f b < c"
   949   finally (order_less_trans) show ?thesis .
   950 qed
   951 
   952 lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
   953   (!!x y. x < y ==> f x < f y) ==> a < f c"
   954 proof -
   955   assume r: "!!x y. x < y ==> f x < f y"
   956   assume "a < f b"
   957   also assume "b < c" hence "f b < f c" by (rule r)
   958   finally (order_less_trans) show ?thesis .
   959 qed
   960 
   961 lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
   962   (!!x y. x <= y ==> f x <= f y) ==> f a < c"
   963 proof -
   964   assume r: "!!x y. x <= y ==> f x <= f y"
   965   assume "a <= b" hence "f a <= f b" by (rule r)
   966   also assume "f b < c"
   967   finally (order_le_less_trans) show ?thesis .
   968 qed
   969 
   970 lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
   971   (!!x y. x < y ==> f x < f y) ==> a < f c"
   972 proof -
   973   assume r: "!!x y. x < y ==> f x < f y"
   974   assume "a <= f b"
   975   also assume "b < c" hence "f b < f c" by (rule r)
   976   finally (order_le_less_trans) show ?thesis .
   977 qed
   978 
   979 lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
   980   (!!x y. x < y ==> f x < f y) ==> f a < c"
   981 proof -
   982   assume r: "!!x y. x < y ==> f x < f y"
   983   assume "a < b" hence "f a < f b" by (rule r)
   984   also assume "f b <= c"
   985   finally (order_less_le_trans) show ?thesis .
   986 qed
   987 
   988 lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
   989   (!!x y. x <= y ==> f x <= f y) ==> a < f c"
   990 proof -
   991   assume r: "!!x y. x <= y ==> f x <= f y"
   992   assume "a < f b"
   993   also assume "b <= c" hence "f b <= f c" by (rule r)
   994   finally (order_less_le_trans) show ?thesis .
   995 qed
   996 
   997 lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
   998   (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
   999 proof -
  1000   assume r: "!!x y. x <= y ==> f x <= f y"
  1001   assume "a <= f b"
  1002   also assume "b <= c" hence "f b <= f c" by (rule r)
  1003   finally (order_trans) show ?thesis .
  1004 qed
  1005 
  1006 lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
  1007   (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
  1008 proof -
  1009   assume r: "!!x y. x <= y ==> f x <= f y"
  1010   assume "a <= b" hence "f a <= f b" by (rule r)
  1011   also assume "f b <= c"
  1012   finally (order_trans) show ?thesis .
  1013 qed
  1014 
  1015 lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
  1016   (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
  1017 proof -
  1018   assume r: "!!x y. x <= y ==> f x <= f y"
  1019   assume "a <= b" hence "f a <= f b" by (rule r)
  1020   also assume "f b = c"
  1021   finally (ord_le_eq_trans) show ?thesis .
  1022 qed
  1023 
  1024 lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
  1025   (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
  1026 proof -
  1027   assume r: "!!x y. x <= y ==> f x <= f y"
  1028   assume "a = f b"
  1029   also assume "b <= c" hence "f b <= f c" by (rule r)
  1030   finally (ord_eq_le_trans) show ?thesis .
  1031 qed
  1032 
  1033 lemma ord_less_eq_subst: "a < b ==> f b = c ==>
  1034   (!!x y. x < y ==> f x < f y) ==> f a < c"
  1035 proof -
  1036   assume r: "!!x y. x < y ==> f x < f y"
  1037   assume "a < b" hence "f a < f b" by (rule r)
  1038   also assume "f b = c"
  1039   finally (ord_less_eq_trans) show ?thesis .
  1040 qed
  1041 
  1042 lemma ord_eq_less_subst: "a = f b ==> b < c ==>
  1043   (!!x y. x < y ==> f x < f y) ==> a < f c"
  1044 proof -
  1045   assume r: "!!x y. x < y ==> f x < f y"
  1046   assume "a = f b"
  1047   also assume "b < c" hence "f b < f c" by (rule r)
  1048   finally (ord_eq_less_trans) show ?thesis .
  1049 qed
  1050 
  1051 text {*
  1052   Note that this list of rules is in reverse order of priorities.
  1053 *}
  1054 
  1055 lemmas basic_trans_rules [trans] =
  1056   order_less_subst2
  1057   order_less_subst1
  1058   order_le_less_subst2
  1059   order_le_less_subst1
  1060   order_less_le_subst2
  1061   order_less_le_subst1
  1062   order_subst2
  1063   order_subst1
  1064   ord_le_eq_subst
  1065   ord_eq_le_subst
  1066   ord_less_eq_subst
  1067   ord_eq_less_subst
  1068   forw_subst
  1069   back_subst
  1070   rev_mp
  1071   mp
  1072   set_rev_mp
  1073   set_mp
  1074   order_neq_le_trans
  1075   order_le_neq_trans
  1076   order_less_trans
  1077   order_less_asym'
  1078   order_le_less_trans
  1079   order_less_le_trans
  1080   order_trans
  1081   order_antisym
  1082   ord_le_eq_trans
  1083   ord_eq_le_trans
  1084   ord_less_eq_trans
  1085   ord_eq_less_trans
  1086   trans
  1087 
  1088 end