Quelle Set.thy Sprache: Isabelle

(*  Title:      HOL/Set.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
*)

section \<open>Set theory for higher-order logic\<close>

theory Set
  imports Lattices Boolean_Algebras
begin

subsection \<open>Sets as predicates\<close>

typedecl 'a set

axiomatization Collect :: "('a \ bool) \ 'a set" \ \comprehension\
  and member :: "'a \ 'a set \ bool" \ \membership\
  where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
    and Collect_mem_eq [simp, code_unfold]: "Collect (\x. member x A) = A"

notation
  member  (\<open>'(\<in>')\<close>) and
  member  (\<open>(\<open>notation=\<open>infix \<in>\<close>\<close>_/ \<in> _)\<close> [51, 51] 50)

abbreviation not_member
  where "not_member x A \ \ (x \ A)" \ \non-membership\
notation
  not_member  (\<open>'(\<notin>')\<close>) and
  not_member  (\<open>(\<open>notation=\<open>infix \<notin>\<close>\<close>_/ \<notin> _)\<close> [51, 51] 50)

open_bundle member_ASCII_syntax
begin
notation (ASCII)
  member  (\<open>'(:')\<close>) and
  member  (\<open>(\<open>notation=\<open>infix :\<close>\<close>_/ : _)\<close> [51, 51] 50) and
  not_member  (\<open>'(~:')\<close>) and
  not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
end

text \<open>Set comprehensions\<close>

syntax
  "_Coll" :: "pttrn \ bool \ 'a set" ($\indent=1 notation=\mixfix set comprehension\\{_./ _})$
syntax_consts
  "_Coll" \<rightleftharpoons> Collect
translations
  "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"

syntax (ASCII)
  "_Collect" :: "pttrn \ 'a set \ bool \ 'a set" ($\indent=1 notation=\mixfix set comprehension\\{(_/: _)./ _})$
syntax
  "_Collect" :: "pttrn \ 'a set \ bool \ 'a set" ($\indent=1 notation=\mixfix set comprehension\\{(_/ \ _)./ _})$
translations
  "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"

ML \<open>
  fun Collect_binder_tr' c [Abs (x, T, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, _, P)] =
        if x = y then
          let
            val x' = Syntax_Trans.mark_bound_body (x, T);
            val t' = subst_bound (x', t);
            val P' = subst_bound (x', P);
          in Syntax.const c $ Syntax_Trans.mark_bound_abs (x, T) $ P' $ t' end
        else raise Match
    | Collect_binder_tr' _ _ = raise Match
\<close>

lemma CollectI: "P a \ a \ {x. P x}"
  by simp

lemma CollectD: "a \ {x. P x} \ P a"
  by simp

lemma Collect_cong: "(\x. P x = Q x) \ {x. P x} = {x. Q x}"
  by simp

text \<open>
  Simproc for pulling \<open>x = t\<close> in \<open>{x. \<dots> \<and> x = t \<and> \<dots>}\<close>
  to the front (and similarly for \<open>t = x\<close>):
\<close>

simproc_setup defined_Collect ("{x. P x \ Q x}") = \
  K (Quantifier1.rearrange_Collect
    (fn ctxt =>
      resolve_tac ctxt @{thms Collect_cong} 1 THEN
      resolve_tac ctxt @{thms iffI} 1 THEN
      ALLGOALS
        (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
          DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})])))
\<close>

lemmas CollectE = CollectD [elim_format]

lemma set_eqI:
  assumes "\x. x \ A \ x \ B"
  shows "A = B"
proof -
  from assms have "{x. x \ A} = {x. x \ B}"
    by simp
  then show ?thesis by simp
qed

lemma set_eq_iff: "A = B \ (\x. x \ A \ x \ B)"
  by (auto intro:set_eqI)

lemma Collect_eqI:
  assumes "\x. P x = Q x"
  shows "Collect P = Collect Q"
  using assms by (auto intro: set_eqI)

text \<open>Lifting of predicate class instances\<close>

instantiation set :: (type) boolean_algebra
begin

definition less_eq_set
  where "A \ B \ (\x. member x A) \ (\x. member x B)"

definition less_set
  where "A < B \ (\x. member x A) < (\x. member x B)"

definition inf_set
  where "A \ B = Collect ((\x. member x A) \ (\x. member x B))"

definition sup_set
  where "A \ B = Collect ((\x. member x A) \ (\x. member x B))"

definition bot_set
  where "\ = Collect \"

definition top_set
  where "\ = Collect \"

definition uminus_set
  where "- A = Collect (- (\x. member x A))"

definition minus_set
  where "A - B = Collect ((\x. member x A) - (\x. member x B))"

instance
  by standard
    (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
      bot_set_def top_set_def uminus_set_def minus_set_def
      less_le_not_le sup_inf_distrib1 diff_eq set_eqI fun_eq_iff
      del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)

end

text \<open>Set enumerations\<close>

abbreviation empty :: "'a set" (\<open>{}\<close>)
  where "{} \ bot"

definition insert :: "'a \ 'a set \ 'a set"
  where insert_compr: "insert a B = {x. x = a \ x \ B}"

open_bundle set_enumeration_syntax
begin

syntax
  "_Finset" :: "args \ 'a set" ($\indent=1 notation=\mixfix set enumeration\\{_})$
syntax_consts
  "_Finset" \<rightleftharpoons> insert
translations
  "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
  "{x}" \<rightleftharpoons> "CONST insert x {}"

end

subsection \<open>Subsets and bounded quantifiers\<close>

abbreviation subset :: "'a set \ 'a set \ bool"
  where "subset \ less"

abbreviation subset_eq :: "'a set \ 'a set \ bool"
  where "subset_eq \ less_eq"

notation
  subset  (\<open>'(\<subset>')\<close>) and
  subset  (\<open>(\<open>notation=\<open>infix \<subset>\<close>\<close>_/ \<subset> _)\<close> [51, 51] 50) and
  subset_eq  (\<open>'(\<subseteq>')\<close>) and
  subset_eq  (\<open>(\<open>notation=\<open>infix \<subseteq>\<close>\<close>_/ \<subseteq> _)\<close> [51, 51] 50)

abbreviation (input)
  supset :: "'a set \ 'a set \ bool" where
  "supset \ greater"

abbreviation (input)
  supset_eq :: "'a set \ 'a set \ bool" where
  "supset_eq \ greater_eq"

notation
  supset  (\<open>'(\<supset>')\<close>) and
  supset  (\<open>(\<open>notation=\<open>infix \<supset>\<close>\<close>_/ \<supset> _)\<close> [51, 51] 50) and
  supset_eq  (\<open>'(\<supseteq>')\<close>) and
  supset_eq  (\<open>(\<open>notation=\<open>infix \<supseteq>\<close>\<close>_/ \<supseteq> _)\<close> [51, 51] 50)

notation (ASCII output)
  subset  (\<open>'(<')\<close>) and
  subset  (\<open>(\<open>notation=\<open>infix <\<close>\<close>_/ < _)\<close> [51, 51] 50) and
  subset_eq  (\<open>'(<=')\<close>) and
  subset_eq  (\<open>(\<open>notation=\<open>infix <=\<close>\<close>_/ <= _)\<close> [51, 51] 50)

definition Ball :: "'a set \ ('a \ bool) \ bool"
  where "Ball A P \ (\x. x \ A \ P x)" \ \bounded universal quantifiers\

definition Bex :: "'a set \ ('a \ bool) \ bool"
  where "Bex A P \ (\x. x \ A \ P x)" \ \bounded existential quantifiers\

syntax (ASCII)
  "_Ball"       :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder ALL :\\ALL (_/:_)./ _)\ [0, 0, 10] 10)
  "_Bex"        :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder EX :\\EX (_/:_)./ _)\ [0, 0, 10] 10)
  "_Bex1"       :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder EX! :\\EX! (_/:_)./ _)\ [0, 0, 10] 10)
  "_Bleast"     :: "id \ 'a set \ bool \ 'a" (\(\indent=3 notation=\binder LEAST :\\LEAST (_/:_)./ _)\ [0, 0, 10] 10)

syntax (input)
  "_Ball"       :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder ! :\\! (_/:_)./ _)\ [0, 0, 10] 10)
  "_Bex"        :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder ? :\\? (_/:_)./ _)\ [0, 0, 10] 10)
  "_Bex1"       :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder ?! :\\?! (_/:_)./ _)\ [0, 0, 10] 10)

syntax
  "_Ball"       :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder \\\\(_/\_)./ _)\ [0, 0, 10] 10)
  "_Bex"        :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder \\\\(_/\_)./ _)\ [0, 0, 10] 10)
  "_Bex1"       :: "pttrn \ 'a set \ bool \ bool" (\(\indent=3 notation=\binder \!\\\!(_/\_)./ _)\ [0, 0, 10] 10)
  "_Bleast"     :: "id \ 'a set \ bool \ 'a" (\(\indent=3 notation=\binder LEAST\\LEAST(_/\_)./ _)\ [0, 0, 10] 10)

syntax_consts
  "_Ball" \<rightleftharpoons> Ball and
  "_Bex" \<rightleftharpoons> Bex and
  "_Bex1" \<rightleftharpoons> Ex1 and
  "_Bleast" \<rightleftharpoons> Least

translations
  "\x\A. P" \ "CONST Ball A (\x. P)"
  "\x\A. P" \ "CONST Bex A (\x. P)"
  "\!x\A. P" \ "\!x. x \ A \ P"
  "LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"

syntax (ASCII output)
  "_setlessAll" :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder ALL\\ALL _<_./ _)\ [0, 0, 10] 10)
  "_setlessEx"  :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder EX\\EX _<_./ _)\ [0, 0, 10] 10)
  "_setleAll"   :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder ALL\\ALL _<=_./ _)\ [0, 0, 10] 10)
  "_setleEx"    :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder EX\\EX _<=_./ _)\ [0, 0, 10] 10)
  "_setleEx1"   :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder EX!\\EX! _<=_./ _)\ [0, 0, 10] 10)

syntax
  "_setlessAll" :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0, 0, 10] 10)
  "_setlessEx"  :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0, 0, 10] 10)
  "_setleAll"   :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0, 0, 10] 10)
  "_setleEx"    :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0, 0, 10] 10)
  "_setleEx1"   :: "[idt, 'a, bool] \ bool" (\(\indent=3 notation=\binder \!\\\!_\_./ _)\ [0, 0, 10] 10)

syntax_consts
  "_setlessAll" "_setleAll" \<rightleftharpoons> All and
  "_setlessEx" "_setleEx" \<rightleftharpoons> Ex and
  "_setleEx1" \<rightleftharpoons> Ex1

translations
  "\A\B. P" \ "\A. A \ B \ P"
  "\A\B. P" \ "\A. A \ B \ P"
  "\A\B. P" \ "\A. A \ B \ P"
  "\A\B. P" \ "\A. A \ B \ P"
  "\!A\B. P" \ "\!A. A \ B \ P"

print_translation \<open>
  let
    val All_binder = Mixfix.binder_name \<^const_syntax>\<open>All\<close>;
    val Ex_binder = Mixfix.binder_name \<^const_syntax>\<open>Ex\<close>;
    val impl = \<^const_syntax>\<open>HOL.implies\<close>;
    val conj = \<^const_syntax>\<open>HOL.conj\<close>;
    val sbset = \<^const_syntax>\<open>subset\<close>;
    val sbset_eq = \<^const_syntax>\<open>subset_eq\<close>;

    val trans =
     [((All_binder, impl, sbset), \<^syntax_const>\<open>_setlessAll\<close>),
      ((All_binder, impl, sbset_eq), \<^syntax_const>\<open>_setleAll\<close>),
      ((Ex_binder, conj, sbset), \<^syntax_const>\<open>_setlessEx\<close>),
      ((Ex_binder, conj, sbset_eq), \<^syntax_const>\<open>_setleEx\<close>)];

    fun mk v (v', T) c n P =
      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
      then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P
      else raise Match;

    fun tr' q = (q, fn _ =>
      (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, \<^Type>\<open>set _\<close>),
          Const (c, _) $
            (Const (d, _) $ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v', T)) $ n) $ P] =>
          (case AList.lookup (=) trans (q, c, d) of
            NONE => raise Match
          | SOME l => mk v (v', T) l n P)
        | _ => raise Match));
  in
    [tr' All_binder, tr' Ex_binder]
  end
\<close>

text \<open>
  \<^medskip>
  Translate between \<open>{e | x1\<dots>xn. P}\<close> and \<open>{u. \<exists>x1\<dots>xn. u = e \<and> P}\<close>;
  \<open>{y. \<exists>x1\<dots>xn. y = e \<and> P}\<close> is only translated if \<open>[0..n] \<subseteq> bvs e\<close>.
\<close>

syntax
  "_Setcompr" :: "'a \ idts \ bool \ 'a set"
    (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ |/_./ _})\<close>)
syntax_consts
  "_Setcompr" \<rightleftharpoons> Collect

parse_translation \<open>
  let
    val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", \<^const_syntax>\<open>Ex\<close>));

    fun nvars (Const (\<^syntax_const>\<open>_idts\<close>, _) $ _ $ idts) = nvars idts + 1
      | nvars _ = 1;

    fun setcompr_tr ctxt [e, idts, b] =
      let
        val eq = Syntax.const \<^const_syntax>\<open>HOL.eq\<close> $ Bound (nvars idts) $ e;
        val P = Syntax.const \<^const_syntax>\<open>HOL.conj\<close> $ eq $ b;
        val exP = ex_tr ctxt [idts, P];
      in Syntax.const \<^const_syntax>\<open>Collect\<close> $ absdummy dummyT exP end;

  in [(\<^syntax_const>\<open>_Setcompr\<close>, setcompr_tr)] end
\<close>

typed_print_translation \<open>
[(\<^const_syntax>\<open>Ball\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Ball\<close>),
  (\<^const_syntax>\<open>Bex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Bex\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>

print_translation \<open>
let
  val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (\<^const_syntax>\<open>Ex\<close>, "DUMMY"));

  fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
    let
      fun check (Const (\<^const_syntax>\<open>Ex\<close>, _) $ Abs (_, _, P), n) = check (P, n + 1)
        | check (Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
              (Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ Bound m $ e) $ P, n) =
            n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
            subset (=) (0 upto (n - 1), add_loose_bnos (e, 0, []))
        | check _ = false;

        fun tr' (_ $ abs) =
          let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' ctxt [abs]
          in Syntax.const \<^syntax_const>\<open>_Setcompr\<close> $ e $ idts $ Q end;
    in
      if check (P, 0) then tr' P
      else
        let
          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
          val M = Syntax.const \<^syntax_const>\<open>_Coll\<close> $ x $ t;
        in
          case t of
            Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
              (Const (\<^const_syntax>\<open>Set.member\<close>, _) $
                (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P =>
            if xN = yN then Syntax.const \<^syntax_const>\<open>_Collect\<close> $ x $ A $ P else M
          | _ => M
        end
    end;
  in [(\<^const_syntax>\<open>Collect\<close>, setcompr_tr')] end
\<close>

simproc_setup defined_Bex ("\x\A. P x \ Q x") = \
  K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
\<close>

simproc_setup defined_All ("\x\A. P x \ Q x") = \
  K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
\<close>

lemma ballI [intro!]: "(\x. x \ A \ P x) \ \x\A. P x"
  by (simp add: Ball_def)

lemmas strip = impI allI ballI

lemma bspec [dest?]: "\x\A. P x \ x \ A \ P x"
  by (simp add: Ball_def)

text \<open>Gives better instantiation for bound:\<close>
setup \<open>
  map_theory_claset (fn ctxt =>
    ctxt addbefore ("bspec", fn ctxt' => dresolve_tac ctxt' @{thms bspec} THEN' assume_tac ctxt'))
\<close>

ML \<open>
structure Simpdata =
struct
  open Simpdata;
  val mksimps_pairs = [(\<^const_name>\<open>Ball\<close>, @{thms bspec})] @ mksimps_pairs;
end;

open Simpdata;
\<close>

declaration \<open>fn _ => Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))\<close>

lemma ballE [elim]: "\x\A. P x \ (P x \ Q) \ (x \ A \ Q) \ Q"
  unfolding Ball_def by blast

lemma bexI [intro]: "P x \ x \ A \ \x\A. P x"
  \<comment> \<open>Normally the best argument order: \<open>P x\<close> constrains the choice of \<open>x \<in> A\<close>.\<close>
  unfolding Bex_def by blast

lemma rev_bexI [intro?]: "x \ A \ P x \ \x\A. P x"
  \<comment> \<open>The best argument order when there is only one \<open>x \<in> A\<close>.\<close>
  unfolding Bex_def by blast

lemma bexCI: "(\x\A. \ P x \ P a) \ a \ A \ \x\A. P x"
  unfolding Bex_def by blast

lemma bexE [elim!]: "\x\A. P x \ (\x. x \ A \ P x \ Q) \ Q"
  unfolding Bex_def by blast

lemma ball_triv [simp]: "(\x\A. P) \ ((\x. x \ A) \ P)"
  \<comment> \<open>trivial rewrite rule.\<close>
  by (simp add: Ball_def)

lemma bex_triv [simp]: "(\x\A. P) \ ((\x. x \ A) \ P)"
  \<comment> \<open>Dual form for existentials.\<close>
  by (simp add: Bex_def)

lemma bex_triv_one_point1 [simp]: "(\x\A. x = a) \ a \ A"
  by blast

lemma bex_triv_one_point2 [simp]: "(\x\A. a = x) \ a \ A"
  by blast

lemma bex_one_point1 [simp]: "(\x\A. x = a \ P x) \ a \ A \ P a"
  by blast

lemma bex_one_point2 [simp]: "(\x\A. a = x \ P x) \ a \ A \ P a"
  by blast

lemma ball_one_point1 [simp]: "(\x\A. x = a \ P x) \ (a \ A \ P a)"
  by blast

lemma ball_one_point2 [simp]: "(\x\A. a = x \ P x) \ (a \ A \ P a)"
  by blast

lemma ball_conj_distrib: "(\x\A. P x \ Q x) \ (\x\A. P x) \ (\x\A. Q x)"
  by blast

lemma bex_disj_distrib: "(\x\A. P x \ Q x) \ (\x\A. P x) \ (\x\A. Q x)"
  by blast

text \<open>Congruence rules\<close>

lemma ball_cong:
  "\ A = B; \x. x \ B \ P x \ Q x \ \
    (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
by (simp add: Ball_def)

lemma ball_cong_simp [cong]:
  "\ A = B; \x. x \ B =simp=> P x \ Q x \ \
    (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
by (simp add: simp_implies_def Ball_def)

lemma bex_cong:
  "\ A = B; \x. x \ B \ P x \ Q x \ \
    (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
by (simp add: Bex_def cong: conj_cong)

lemma bex_cong_simp [cong]:
  "\ A = B; \x. x \ B =simp=> P x \ Q x \ \
    (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
by (simp add: simp_implies_def Bex_def cong: conj_cong)

lemma bex1_def: "(\!x\X. P x) \ (\x\X. P x) \ (\x\X. \y\X. P x \ P y \ x = y)"
  by auto

subsection \<open>Basic operations\<close>

subsubsection \<open>Subsets\<close>

lemma subsetI [intro!]: "(\x. x \ A \ x \ B) \ A \ B"
  by (simp add: less_eq_set_def le_fun_def)

text \<open>
  \<^medskip>
  Map the type \<open>'a set \<Rightarrow> anything\<close> to just \<open>'a\<close>; for overloading constants
  whose first argument has type \<open>'a set\<close>.
\<close>

lemma subsetD [elim, intro?]: "A \ B \ c \ A \ c \ B"
  by (simp add: less_eq_set_def le_fun_def)
  \<comment> \<open>Rule in Modus Ponens style.\<close>

lemma rev_subsetD [intro?,no_atp]: "c \ A \ A \ B \ c \ B"
  \<comment> \<open>The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.\<close>
  by (rule subsetD)

lemma subsetCE [elim,no_atp]: "A \ B \ (c \ A \ P) \ (c \ B \ P) \ P"
  \<comment> \<open>Classical elimination rule.\<close>
  by (auto simp add: less_eq_set_def le_fun_def)

lemma subset_eq: "A \ B \ (\x\A. x \ B)"
  by blast

lemma contra_subsetD [no_atp]: "A \ B \ c \ B \ c \ A"
  by blast

lemma subset_refl: "A \ A"
  by (fact order_refl) (* already [iff] *)

lemma subset_trans: "A \ B \ B \ C \ A \ C"
  by (fact order_trans)

lemma subset_not_subset_eq [code]: "A \ B \ A \ B \ \ B \ A"
  by (fact less_le_not_le)

lemma eq_mem_trans: "a = b \ b \ A \ a \ A"
  by simp

lemmas basic_trans_rules [trans] =
  order_trans_rules rev_subsetD subsetD eq_mem_trans

subsubsection \<open>Equality\<close>

lemma subset_antisym [intro!]: "A \ B \ B \ A \ A = B"
  \<comment> \<open>Anti-symmetry of the subset relation.\<close>
  by (iprover intro: set_eqI subsetD)

text \<open>\<^medskip> Equality rules from ZF set theory -- are they appropriate here?\<close>

lemma equalityD1: "A = B \ A \ B"
  by simp

lemma equalityD2: "A = B \ B \ A"
  by simp

text \<open>
  \<^medskip>
  Be careful when adding this to the claset as \<open>subset_empty\<close> is in the
  simpset: \<^prop>\<open>A = {}\<close> goes to \<^prop>\<open>{} \<subseteq> A\<close> and \<^prop>\<open>A \<subseteq> {}\<close>
  and then back to \<^prop>\<open>A = {}\<close>!
\<close>

lemma equalityE: "A = B \ (A \ B \ B \ A \ P) \ P"
  by simp

lemma equalityCE [elim]: "A = B \ (c \ A \ c \ B \ P) \ (c \ A \ c \ B \ P) \ P"
  by blast

lemma eqset_imp_iff: "A = B \ x \ A \ x \ B"
  by simp

lemma eqelem_imp_iff: "x = y \ x \ A \ y \ A"
  by simp

subsubsection \<open>The empty set\<close>

lemma empty_def: "{} = {x. False}"
  by (simp add: bot_set_def bot_fun_def)

lemma empty_iff [simp]: "c \ {} \ False"
  by (simp add: empty_def)

lemma emptyE [elim!]: "a \ {} \ P"
  by simp

lemma empty_subsetI [iff]: "{} \ A"
  \<comment> \<open>One effect is to delete the ASSUMPTION \<^prop>\<open>{} \<subseteq> A\<close>\<close>
  by blast

lemma equals0I: "(\y. y \ A \ False) \ A = {}"
  by blast

lemma equals0D: "A = {} \ a \ A"
  \<comment> \<open>Use for reasoning about disjointness: \<open>A \<inter> B = {}\<close>\<close>
  by blast

lemma ball_empty [simp]: "Ball {} P \ True"
  by (simp add: Ball_def)

lemma bex_empty [simp]: "Bex {} P \ False"
  by (simp add: Bex_def)

subsubsection \<open>The universal set -- UNIV\<close>

abbreviation UNIV :: "'a set"
  where "UNIV \ top"

lemma UNIV_def: "UNIV = {x. True}"
  by (simp add: top_set_def top_fun_def)

lemma UNIV_I [simp]: "x \ UNIV"
  by (simp add: UNIV_def)

declare UNIV_I [intro]  \<comment> \<open>unsafe makes it less likely to cause problems\<close>

lemma UNIV_witness [intro?]: "\x. x \ UNIV"
  by simp

lemma subset_UNIV: "A \ UNIV"
  by (fact top_greatest) (* already simp *)

text \<open>
  \<^medskip>
  Eta-contracting these two rules (to remove \<open>P\<close>) causes them
  to be ignored because of their interaction with congruence rules.
\<close>

lemma ball_UNIV [simp]: "Ball UNIV P \ All P"
  by (simp add: Ball_def)

lemma bex_UNIV [simp]: "Bex UNIV P \ Ex P"
  by (simp add: Bex_def)

lemma UNIV_eq_I: "(\x. x \ A) \ UNIV = A"
  by auto

lemma UNIV_not_empty [iff]: "UNIV \ {}"
  by (blast elim: equalityE)

lemma empty_not_UNIV[simp]: "{} \ UNIV"
  by blast

subsubsection \<open>The Powerset operator -- Pow\<close>

definition Pow :: "'a set \ 'a set set"
  where Pow_def: "Pow A = {B. B \ A}"

lemma Pow_iff [iff]: "A \ Pow B \ A \ B"
  by (simp add: Pow_def)

lemma PowI: "A \ B \ A \ Pow B"
  by (simp add: Pow_def)

lemma PowD: "A \ Pow B \ A \ B"
  by (simp add: Pow_def)

lemma Pow_bottom: "{} \ Pow B"
  by simp

lemma Pow_top: "A \ Pow A"
  by simp

lemma Pow_not_empty: "Pow A \ {}"
  using Pow_top by blast

subsubsection \<open>Set complement\<close>

lemma Compl_iff [simp]: "c \ - A \ c \ A"
  by (simp add: fun_Compl_def uminus_set_def)

lemma ComplI [intro!]: "(c \ A \ False) \ c \ - A"
  by (simp add: fun_Compl_def uminus_set_def) blast

text \<open>
  \<^medskip>
  This form, with negated conclusion, works well with the Classical prover.
  Negated assumptions behave like formulae on the right side of the
  notional turnstile \dots
\<close>

lemma ComplD [dest!]: "c \ - A \ c \ A"
  by simp

lemmas ComplE = ComplD [elim_format]

lemma Compl_eq: "- A = {x. \ x \ A}"
  by blast

subsubsection \<open>Binary intersection\<close>

abbreviation inter :: "'a set \ 'a set \ 'a set" (infixl \\\ 70)
  where "(\) \ inf"

notation (ASCII)
  inter  (infixl \<open>Int\<close> 70)

lemma Int_def: "A \ B = {x. x \ A \ x \ B}"
  by (simp add: inf_set_def inf_fun_def)

lemma Int_iff [simp]: "c \ A \ B \ c \ A \ c \ B"
  unfolding Int_def by blast

lemma IntI [intro!]: "c \ A \ c \ B \ c \ A \ B"
  by simp

lemma IntD1: "c \ A \ B \ c \ A"
  by simp

lemma IntD2: "c \ A \ B \ c \ B"
  by simp

lemma IntE [elim!]: "c \ A \ B \ (c \ A \ c \ B \ P) \ P"
  by simp

subsubsection \<open>Binary union\<close>

abbreviation union :: "'a set \ 'a set \ 'a set" (infixl \\\ 65)
  where "union \ sup"

notation (ASCII)
  union  (infixl \<open>Un\<close> 65)

lemma Un_def: "A \ B = {x. x \ A \ x \ B}"
  by (simp add: sup_set_def sup_fun_def)

lemma Un_iff [simp]: "c \ A \ B \ c \ A \ c \ B"
  unfolding Un_def by blast

lemma UnI1 [elim?]: "c \ A \ c \ A \ B"
  by simp

lemma UnI2 [elim?]: "c \ B \ c \ A \ B"
  by simp

text \<open>\<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs. \<open>B\<close>.\<close>
lemma UnCI [intro!]: "(c \ B \ c \ A) \ c \ A \ B"
  by auto

lemma UnE [elim!]: "c \ A \ B \ (c \ A \ P) \ (c \ B \ P) \ P"
  unfolding Un_def by blast

lemma insert_def: "insert a B = {x. x = a} \ B"
  by (simp add: insert_compr Un_def)

subsubsection \<open>Set difference\<close>

lemma Diff_iff [simp]: "c \ A - B \ c \ A \ c \ B"
  by (simp add: minus_set_def fun_diff_def)

lemma DiffI [intro!]: "c \ A \ c \ B \ c \ A - B"
  by simp

lemma DiffD1: "c \ A - B \ c \ A"
  by simp

lemma DiffD2: "c \ A - B \ c \ B \ P"
  by simp

lemma DiffE [elim!]: "c \ A - B \ (c \ A \ c \ B \ P) \ P"
  by simp

lemma set_diff_eq: "A - B = {x. x \ A \ x \ B}"
  by blast

lemma Compl_eq_Diff_UNIV: "- A = (UNIV - A)"
  by blast

abbreviation sym_diff :: "'a set \ 'a set \ 'a set" where
  "sym_diff A B \ ((A - B) \ (B-A))"

subsubsection \<open>Augmenting a set -- \<^const>\<open>insert\<close>\<close>

lemma insert_iff [simp]: "a \ insert b A \ a = b \ a \ A"
  unfolding insert_def by blast

lemma insertI1: "a \ insert a B"
  by simp

lemma insertI2: "a \ B \ a \ insert b B"
  by simp

lemma insertE [elim!]: "a \ insert b A \ (a = b \ P) \ (a \ A \ P) \ P"
  unfolding insert_def by blast

lemma insertCI [intro!]: "(a \ B \ a = b) \ a \ insert b B"
  \<comment> \<open>Classical introduction rule.\<close>
  by auto

lemma subset_insert_iff: "A \ insert x B \ (if x \ A then A - {x} \ B else A \ B)"
  by auto

lemma set_insert:
  assumes "x \ A"
  obtains B where "A = insert x B" and "x \ B"
proof
  show "A = insert x (A - {x})" using assms by blast
  show "x \ A - {x}" by blast
qed

lemma insert_ident: "x \ A \ x \ B \ insert x A = insert x B \ A = B"
  by auto

lemma insert_eq_iff:
  assumes "a \ A" "b \ B"
  shows "insert a A = insert b B \
    (if a = b then A = B else \<exists>C. A = insert b C \<and> b \<notin> C \<and> B = insert a C \<and> a \<notin> C)"
    (is "?L \ ?R")
proof
  show ?R if ?L
  proof (cases "a = b")
    case True
    with assms \<open>?L\<close> show ?R
      by (simp add: insert_ident)
  next
    case False
    let ?C = "A - {b}"
    have "A = insert b ?C \ b \ ?C \ B = insert a ?C \ a \ ?C"
      using assms \<open>?L\<close> \<open>a \<noteq> b\<close> by auto
    then show ?R using \<open>a \<noteq> b\<close> by auto
  qed
  show ?L if ?R
    using that by (auto split: if_splits)
qed

lemma insert_UNIV[simp]: "insert x UNIV = UNIV"
  by auto

subsubsection \<open>Singletons, using insert\<close>

lemma singletonI [intro!]: "a \ {a}"
  \<comment> \<open>Redundant? But unlike \<open>insertCI\<close>, it proves the subgoal immediately!\<close>
  by (rule insertI1)

lemma singletonD [dest!]: "b \ {a} \ b = a"
  by blast

lemmas singletonE = singletonD [elim_format]

lemma singleton_iff: "b \ {a} \ b = a"
  by blast

lemma singleton_inject [dest!]: "{a} = {b} \ a = b"
  by blast

lemma singleton_insert_inj_eq [iff]: "{b} = insert a A \ a = b \ A \ {b}"
  by blast

lemma singleton_insert_inj_eq' [iff]: "insert a A = {b} \ a = b \ A \ {b}"
  by blast

lemma subset_singletonD: "A \ {x} \ A = {} \ A = {x}"
  by fast

lemma subset_singleton_iff: "X \ {a} \ X = {} \ X = {a}"
  by blast

lemma subset_singleton_iff_Uniq: "(\a. A \ {a}) \ (\\<^sub>\\<^sub>1x. x \ A)"
  unfolding Uniq_def by blast

lemma singleton_conv [simp]: "{x. x = a} = {a}"
  by blast

lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
  by blast

lemma Diff_single_insert: "A - {x} \ B \ A \ insert x B"
  by blast

lemma subset_Diff_insert: "A \ B - insert x C \ A \ B - C \ x \ A"
  by blast

lemma doubleton_eq_iff: "{a, b} = {c, d} \ a = c \ b = d \ a = d \ b = c"
  by (blast elim: equalityE)

lemma Un_singleton_iff: "A \ B = {x} \ A = {} \ B = {x} \ A = {x} \ B = {} \ A = {x} \ B = {x}"
  by auto

lemma singleton_Un_iff: "{x} = A \ B \ A = {} \ B = {x} \ A = {x} \ B = {} \ A = {x} \ B = {x}"
  by auto

subsubsection \<open>Image of a set under a function\<close>

text \<open>Frequently \<open>b\<close> does not have the syntactic form of \<open>f x\<close>.\<close>

definition image :: "('a \ 'b) \ 'a set \ 'b set" (infixr \`\ 90)
  where "f ` A = {y. \x\A. y = f x}"

lemma image_eqI [simp, intro]: "b = f x \ x \ A \ b \ f ` A"
  unfolding image_def by blast

lemma imageI: "x \ A \ f x \ f ` A"
  by (rule image_eqI) (rule refl)

lemma rev_image_eqI: "x \ A \ b = f x \ b \ f ` A"
  \<comment> \<open>This version's more effective when we already have the required \<open>x\<close>.\<close>
  by (rule image_eqI)

lemma imageE [elim!]:
  assumes "b \ (\x. f x) ` A" \ \The eta-expansion gives variable-name preservation.\
  obtains x where "b = f x" and "x \ A"
  using assms unfolding image_def by blast

lemma Compr_image_eq: "{x \ f ` A. P x} = f ` {x \ A. P (f x)}"
  by auto

lemma image_Un: "f ` (A \ B) = f ` A \ f ` B"
  by blast

lemma image_iff: "z \ f ` A \ (\x\A. z = f x)"
  by blast

lemma image_subsetI: "(\x. x \ A \ f x \ B) \ f ` A \ B"
  \<comment> \<open>Replaces the three steps \<open>subsetI\<close>, \<open>imageE\<close>,
    \<open>hypsubst\<close>, but breaks too many existing proofs.\<close>
  by blast

lemma image_subset_iff: "f ` A \ B \ (\x\A. f x \ B)"
  \<comment> \<open>This rewrite rule would confuse users if made default.\<close>
  by blast

lemma subset_imageE:
  assumes "B \ f ` A"
  obtains C where "C \ A" and "B = f ` C"
proof -
  from assms have "B = f ` {a \ A. f a \ B}" by fast
  moreover have "{a \ A. f a \ B} \ A" by blast
  ultimately show thesis by (blast intro: that)
qed

lemma subset_image_iff: "B \ f ` A \ (\AA\A. B = f ` AA)"
  by (blast elim: subset_imageE)

lemma image_ident [simp]: "(\x. x) ` Y = Y"
  by blast

lemma image_empty [simp]: "f ` {} = {}"
  by blast

lemma image_insert [simp]: "f ` insert a B = insert (f a) (f ` B)"
  by blast

lemma image_constant: "x \ A \ (\x. c) ` A = {c}"
  by auto

lemma image_constant_conv: "(\x. c) ` A = (if A = {} then {} else {c})"
  by auto

lemma image_image: "f ` (g ` A) = (\x. f (g x)) ` A"
  by blast

lemma insert_image [simp]: "x \ A \ insert (f x) (f ` A) = f ` A"
  by blast

lemma image_is_empty [iff]: "f ` A = {} \ A = {}"
  by blast

lemma empty_is_image [iff]: "{} = f ` A \ A = {}"
  by blast

lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
  \<comment> \<open>NOT suitable as a default simp rule: the RHS isn't simpler than the LHS,
      with its implicit quantifier and conjunction.  Also image enjoys better
      equational properties than does the RHS.\<close>
  by blast

lemma if_image_distrib [simp]:
  "(\x. if P x then f x else g x) ` S = f ` (S \ {x. P x}) \ g ` (S \ {x. \ P x})"
  by auto

lemma image_cong:
  "f ` M = g ` N" if "M = N" "\x. x \ N \ f x = g x"
  using that by (simp add: image_def)

lemma image_cong_simp [cong]:
  "f ` M = g ` N" if "M = N" "\x. x \ N =simp=> f x = g x"
  using that image_cong [of M N f g] by (simp add: simp_implies_def)

lemma image_Int_subset: "f ` (A \ B) \ f ` A \ f ` B"
  by blast

lemma image_diff_subset: "f ` A - f ` B \ f ` (A - B)"
  by blast

lemma Setcompr_eq_image: "{f x |x. x \ A} = f ` A"
  by blast

lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}"
  by auto

lemma ball_imageD: "\x\f ` A. P x \ \x\A. P (f x)"
  by simp

lemma bex_imageD: "\x\f ` A. P x \ \x\A. P (f x)"
  by auto

lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
  by auto

theorem Cantors_theorem: "\f. f ` A = Pow A"
proof
  assume "\f. f ` A = Pow A"
  then obtain f where f: "f ` A = Pow A" ..
  let ?X = "{a \ A. a \ f a}"
  have "?X \ Pow A" by blast
  then have "?X \ f ` A" by (simp only: f)
  then obtain x where "x \ A" and "f x = ?X" by blast
  then show False by blast
qed

text \<open>\<^medskip> Range of a function -- just an abbreviation for image!\<close>

abbreviation range :: "('a \ 'b) \ 'b set" \ \of function\
  where "range f \ f ` UNIV"

lemma range_eqI: "b = f x \ b \ range f"
  by simp

lemma rangeI: "f x \ range f"
  by simp

lemma rangeE [elim?]: "b \ range (\x. f x) \ (\x. b = f x \ P) \ P"
  by (rule imageE)

lemma range_subsetD: "range f \ B \ f i \ B"
  by blast

lemma full_SetCompr_eq: "{u. \x. u = f x} = range f"
  by auto

lemma range_composition: "range (\x. f (g x)) = f ` range g"
  by auto

lemma range_constant [simp]: "range (\_. x) = {x}"
  by (simp add: image_constant)

lemma range_eq_singletonD: "range f = {a} \ f x = a"
  by auto

subsubsection \<open>Some rules with \<open>if\<close>\<close>

text \<open>Elimination of \<open>{x. \<dots> \<and> x = t \<and> \<dots>}\<close>.\<close>

lemma Collect_conv_if: "{x. x = a \ P x} = (if P a then {a} else {})"
  by auto

lemma Collect_conv_if2: "{x. a = x \ P x} = (if P a then {a} else {})"
  by auto

text \<open>
  Rewrite rules for boolean case-splitting: faster than \<open>if_split [split]\<close>.
\<close>

lemma if_split_eq1: "(if Q then x else y) = b \ (Q \ x = b) \ (\ Q \ y = b)"
  by (rule if_split)

lemma if_split_eq2: "a = (if Q then x else y) \ (Q \ a = x) \ (\ Q \ a = y)"
  by (rule if_split)

text \<open>
  Split ifs on either side of the membership relation.
  Not for \<open>[simp]\<close> -- can cause goals to blow up!
\<close>

lemma if_split_mem1: "(if Q then x else y) \ b \ (Q \ x \ b) \ (\ Q \ y \ b)"
  by (rule if_split)

lemma if_split_mem2: "(a \ (if Q then x else y)) \ (Q \ a \ x) \ (\ Q \ a \ y)"
  by (rule if_split [where P = "\S. a \ S"])

lemmas split_ifs = if_bool_eq_conj if_split_eq1 if_split_eq2 if_split_mem1 if_split_mem2

(*Would like to add these, but the existing code only searches for the
  outer-level constant, which in this case is just Set.member; we instead need
  to use term-nets to associate patterns with rules.  Also, if a rule fails to
  apply, then the formula should be kept.
  [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
   ("Int", [IntD1,IntD2]),
   ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
*)

subsection \<open>Further operations and lemmas\<close>

subsubsection \<open>The ``proper subset'' relation\<close>

lemma psubsetI [intro!]: "A \ B \ A \ B \ A \ B"
  unfolding less_le by blast

lemma psubsetE [elim!]: "A \ B \ (A \ B \ \ B \ A \ R) \ R"
  unfolding less_le by blast

lemma psubset_insert_iff:
  "A \ insert x B \ (if x \ B then A \ B else if x \ A then A - {x} \ B else A \ B)"
  by (auto simp add: less_le subset_insert_iff)

lemma psubset_eq: "A \ B \ A \ B \ A \ B"
  by (simp only: less_le)

lemma psubset_imp_subset: "A \ B \ A \ B"
  by (simp add: psubset_eq)

lemma psubset_trans: "A \ B \ B \ C \ A \ C"
  unfolding less_le by (auto dest: subset_antisym)

lemma psubsetD: "A \ B \ c \ A \ c \ B"
  unfolding less_le by (auto dest: subsetD)

lemma psubset_subset_trans: "A \ B \ B \ C \ A \ C"
  by (auto simp add: psubset_eq)

lemma subset_psubset_trans: "A \ B \ B \ C \ A \ C"
  by (auto simp add: psubset_eq)

lemma psubset_imp_ex_mem: "A \ B \ \b. b \ B - A"
  unfolding less_le by blast

lemma atomize_ball: "(\x. x \ A \ P x) \ Trueprop (\x\A. P x)"
  by (simp only: Ball_def atomize_all atomize_imp)

lemmas [symmetric, rulify] = atomize_ball
  and [symmetric, defn] = atomize_ball

lemma image_Pow_mono: "f ` A \ B \ image f ` Pow A \ Pow B"
  by blast

lemma image_Pow_surj: "f ` A = B \ image f ` Pow A = Pow B"
  by (blast elim: subset_imageE)

subsubsection \<open>Derived rules involving subsets.\<close>

text \<open>\<open>insert\<close>.\<close>

lemma subset_insertI: "B \ insert a B"
  by (rule subsetI) (erule insertI2)

lemma subset_insertI2: "A \ B \ A \ insert b B"
  by blast

lemma subset_insert: "x \ A \ A \ insert x B \ A \ B"
  by blast

text \<open>\<^medskip> Finite Union -- the least upper bound of two sets.\<close>

lemma Un_upper1: "A \ A \ B"
  by (fact sup_ge1)

lemma Un_upper2: "B \ A \ B"
  by (fact sup_ge2)

lemma Un_least: "A \ C \ B \ C \ A \ B \ C"
  by (fact sup_least)

text \<open>\<^medskip> Finite Intersection -- the greatest lower bound of two sets.\<close>

lemma Int_lower1: "A \ B \ A"
  by (fact inf_le1)

lemma Int_lower2: "A \ B \ B"
  by (fact inf_le2)

lemma Int_greatest: "C \ A \ C \ B \ C \ A \ B"
  by (fact inf_greatest)

text \<open>\<^medskip> Set difference.\<close>

lemma Diff_subset[simp]: "A - B \ A"
  by blast

lemma Diff_subset_conv: "A - B \ C \ A \ B \ C"
  by blast

subsubsection \<open>Equalities involving union, intersection, inclusion, etc.\<close>

text \<open>\<open>{}\<close>.\<close>

lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
  \<comment> \<open>supersedes \<open>Collect_False_empty\<close>\<close>
  by auto

lemma subset_empty [simp]: "A \ {} \ A = {}"
  by (fact bot_unique)

lemma not_psubset_empty [iff]: "\ (A < {})"
  by (fact not_less_bot) (*already simp *)

lemma Collect_subset [simp]: "{x\A. P x} \ A" by auto

lemma Collect_empty_eq [simp]: "Collect P = {} \ (\x. \ P x)"
  by blast

lemma empty_Collect_eq [simp]: "{} = Collect P \ (\x. \ P x)"
  by blast

lemma Collect_neg_eq: "{x. \ P x} = - {x. P x}"
  by blast

lemma Collect_disj_eq: "{x. P x \ Q x} = {x. P x} \ {x. Q x}"
  by blast

lemma Collect_imp_eq: "{x. P x \ Q x} = - {x. P x} \ {x. Q x}"
  by blast

lemma Collect_conj_eq: "{x. P x \ Q x} = {x. P x} \ {x. Q x}"
  by blast

lemma Collect_conj_eq2: "{x \ A. P x \ Q x} = {x \ A. P x} \ {x \ A. Q x}"
  by blast

lemma Collect_mono_iff: "Collect P \ Collect Q \ (\x. P x \ Q x)"
  by blast

text \<open>\<^medskip> \<open>insert\<close>.\<close>

lemma insert_is_Un: "insert a A = {a} \ A"
  \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} \<equiv> insert a {}\<close>\<close>
  by blast

lemma insert_not_empty [simp]: "insert a A \ {}"
  and empty_not_insert [simp]: "{} \ insert a A"
  by blast+

lemma insert_absorb: "a \ A \ insert a A = A"
  \<comment> \<open>\<open>[simp]\<close> causes recursive calls when there are nested inserts\<close>
  \<comment> \<open>with \<^emph>\<open>quadratic\<close> running time\<close>
  by blast

lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
  by blast

lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
  by blast

lemma insert_subset [simp]: "insert x A \ B \ x \ B \ A \ B"
  by blast

lemma mk_disjoint_insert: "a \ A \ \B. A = insert a B \ a \ B"
  \<comment> \<open>use new \<open>B\<close> rather than \<open>A - {a}\<close> to avoid infinite unfolding\<close>
  by (rule exI [where x = "A - {a}"]) blast

lemma insert_Collect: "insert a (Collect P) = {u. u \ a \ P u}"
  by auto

lemma insert_inter_insert [simp]: "insert a A \ insert a B = insert a (A \ B)"
  by blast

lemma insert_disjoint [simp]:
  "insert a A \ B = {} \ a \ B \ A \ B = {}"
  "{} = insert a A \ B \ a \ B \ {} = A \ B"
  by auto

lemma disjoint_insert [simp]:
  "B \ insert a A = {} \ a \ B \ B \ A = {}"
  "{} = A \ insert b B \ b \ A \ {} = A \ B"
  by auto

text \<open>\<^medskip> \<open>Int\<close>\<close>

lemma Int_absorb: "A \ A = A"
  by (fact inf_idem) (* already simp *)

lemma Int_left_absorb: "A \ (A \ B) = A \ B"
  by (fact inf_left_idem)

lemma Int_commute: "A \ B = B \ A"
  by (fact inf_commute)

lemma Int_left_commute: "A \ (B \ C) = B \ (A \ C)"
  by (fact inf_left_commute)

lemma Int_assoc: "(A \ B) \ C = A \ (B \ C)"
  by (fact inf_assoc)

lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
  \<comment> \<open>Intersection is an AC-operator\<close>

lemma Int_absorb1: "B \ A \ A \ B = B"
  by (fact inf_absorb2)

lemma Int_absorb2: "A \ B \ A \ B = A"
  by (fact inf_absorb1)

lemma Int_empty_left: "{} \ B = {}"
  by (fact inf_bot_left) (* already simp *)

lemma Int_empty_right: "A \ {} = {}"
  by (fact inf_bot_right) (* already simp *)

lemma disjoint_eq_subset_Compl: "A \ B = {} \ A \ - B"
  by blast

lemma disjoint_iff: "A \ B = {} \ (\x. x\A \ x \ B)"
  by blast

lemma disjoint_iff_not_equal: "A \ B = {} \ (\x\A. \y\B. x \ y)"
  by blast

lemma Int_UNIV_left: "UNIV \ B = B"
  by (fact inf_top_left) (* already simp *)

lemma Int_UNIV_right: "A \ UNIV = A"
  by (fact inf_top_right) (* already simp *)

lemma Int_Un_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)"
  by (fact inf_sup_distrib1)

lemma Int_Un_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)"
  by (fact inf_sup_distrib2)

lemma Int_UNIV: "A \ B = UNIV \ A = UNIV \ B = UNIV"
  by (fact inf_eq_top_iff) (* already simp *)

lemma Int_subset_iff: "C \ A \ B \ C \ A \ C \ B"
  by (fact le_inf_iff) (* already simp *)

lemma Int_Collect: "x \ A \ {x. P x} \ x \ A \ P x"
  by blast

text \<open>\<^medskip> \<open>Un\<close>.\<close>

lemma Un_absorb: "A \ A = A"
  by (fact sup_idem) (* already simp *)

lemma Un_left_absorb: "A \ (A \ B) = A \ B"
  by (fact sup_left_idem)

lemma Un_commute: "A \ B = B \ A"
  by (fact sup_commute)

lemma Un_left_commute: "A \ (B \ C) = B \ (A \ C)"
  by (fact sup_left_commute)

lemma Un_assoc: "(A \ B) \ C = A \ (B \ C)"
  by (fact sup_assoc)

lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
  \<comment> \<open>Union is an AC-operator\<close>

lemma Un_absorb1: "A \ B \ A \ B = B"
  by (fact sup_absorb2)

lemma Un_absorb2: "B \ A \ A \ B = A"
  by (fact sup_absorb1)

lemma Un_empty_left: "{} \ B = B"
  by (fact sup_bot_left) (* already simp *)

lemma Un_empty_right: "A \ {} = A"
  by (fact sup_bot_right) (* already simp *)

lemma Un_UNIV_left: "UNIV \ B = UNIV"
  by (fact sup_top_left) (* already simp *)

lemma Un_UNIV_right: "A \ UNIV = UNIV"
  by (fact sup_top_right) (* already simp *)

lemma Un_insert_left [simp]: "(insert a B) \ C = insert a (B \ C)"
  by blast

lemma Un_insert_right [simp]: "A \ (insert a B) = insert a (A \ B)"
  by blast

lemma Int_insert_left: "(insert a B) \ C = (if a \ C then insert a (B \ C) else B \ C)"
  by auto

lemma Int_insert_left_if0 [simp]: "a \ C \ (insert a B) \ C = B \ C"
  by auto

lemma Int_insert_left_if1 [simp]: "a \ C \ (insert a B) \ C = insert a (B \ C)"
  by auto

lemma Int_insert_right: "A \ (insert a B) = (if a \ A then insert a (A \ B) else A \ B)"
  by auto

lemma Int_insert_right_if0 [simp]: "a \ A \ A \ (insert a B) = A \ B"
  by auto

lemma Int_insert_right_if1 [simp]: "a \ A \ A \ (insert a B) = insert a (A \ B)"
  by auto

lemma Un_Int_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)"
  by (fact sup_inf_distrib1)

lemma Un_Int_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)"
  by (fact sup_inf_distrib2)

lemma Un_Int_crazy: "(A \ B) \ (B \ C) \ (C \ A) = (A \ B) \ (B \ C) \ (C \ A)"
  by blast

lemma subset_Un_eq: "A \ B \ A \ B = B"
  by (fact le_iff_sup)

lemma Un_empty [iff]: "A \ B = {} \ A = {} \ B = {}"
  by (fact sup_eq_bot_iff) (* FIXME: already simp *)

lemma Un_subset_iff: "A \ B \ C \ A \ C \ B \ C"
  by (fact le_sup_iff) (* already simp *)

lemma Un_Diff_Int: "(A - B) \ (A \ B) = A"
  by blast

lemma Diff_Int2: "A \ C - B \ C = A \ C - B"
  by blast

lemma subset_UnE:
  assumes "C \ A \ B"
  obtains A' B' where "A' \ A" "B' \ B" "C = A' \ B'"
proof
  show "C \ A \ A" "C \ B \ B" "C = (C \ A) \ (C \ B)"
    using assms by blast+
qed

lemma Un_Int_eq [simp]: "(S \ T) \ S = S" "(S \ T) \ T = T" "S \ (S \ T) = S" "T \ (S \ T) = T"
  by auto

lemma Int_Un_eq [simp]: "(S \ T) \ S = S" "(S \ T) \ T = T" "S \ (S \ T) = S" "T \ (S \ T) = T"
  by auto

text \<open>\<^medskip> Set complement\<close>

lemma Compl_disjoint [simp]: "A \ - A = {}"
  by (fact inf_compl_bot)

lemma Compl_disjoint2 [simp]: "- A \ A = {}"
  by (fact compl_inf_bot)

lemma Compl_partition: "A \ - A = UNIV"
  by (fact sup_compl_top)

lemma Compl_partition2: "- A \ A = UNIV"
  by (fact compl_sup_top)

lemma double_complement: "- (-A) = A" for A :: "'a set"
  by (fact double_compl) (* already simp *)

lemma Compl_Un: "- (A \ B) = (- A) \ (- B)"
  by (fact compl_sup) (* already simp *)

lemma Compl_Int: "- (A \ B) = (- A) \ (- B)"
  by (fact compl_inf) (* already simp *)

lemma subset_Compl_self_eq: "A \ - A \ A = {}"
  by blast

lemma Un_Int_assoc_eq: "(A \ B) \ C = A \ (B \ C) \ C \ A"
  \<comment> \<open>Halmos, Naive Set Theory, page 16.\<close>
  by blast

lemma Compl_UNIV_eq: "- UNIV = {}"
  by (fact compl_top_eq) (* already simp *)

lemma Compl_empty_eq: "- {} = UNIV"
  by (fact compl_bot_eq) (* already simp *)

lemma Compl_subset_Compl_iff [iff]: "- A \ - B \ B \ A"
  by (fact compl_le_compl_iff) (* FIXME: already simp *)

lemma Compl_eq_Compl_iff [iff]: "- A = - B \ A = B"
  for A B :: "'a set"
  by (fact compl_eq_compl_iff) (* FIXME: already simp *)

lemma Compl_insert: "- insert x A = (- A) - {x}"
  by blast

text \<open>\<^medskip> Bounded quantifiers.

  The following are not added to the default simpset because
  (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.
\<close>

lemma ball_Un: "(\x \ A \ B. P x) \ (\x\A. P x) \ (\x\B. P x)"
  by blast

lemma bex_Un: "(\x \ A \ B. P x) \ (\x\A. P x) \ (\x\B. P x)"
  by blast

text \<open>\<^medskip> Set difference.\<close>

lemma Diff_eq: "A - B = A \ (- B)"
  by(rule boolean_algebra_class.diff_eq)

lemma Diff_eq_empty_iff: "A - B = {} \ A \ B"
  by(rule boolean_algebra_class.diff_shunt_var) (* already simp *)

lemma Diff_cancel [simp]: "A - A = {}"
  by blast

lemma Diff_idemp [simp]: "(A - B) - B = A - B"
  for A B :: "'a set"
  by blast

lemma Diff_triv: "A \ B = {} \ A - B = A"
  by (blast elim: equalityE)

lemma empty_Diff [simp]: "{} - A = {}"
  by blast

lemma Diff_empty [simp]: "A - {} = A"
  by blast

lemma Diff_UNIV [simp]: "A - UNIV = {}"
  by blast

lemma Diff_insert0 [simp]: "x \ A \ A - insert x B = A - B"
  by blast

lemma Diff_insert: "A - insert a B = A - B - {a}"
  \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} \<equiv> insert a 0\<close>\<close>
  by blast

lemma Diff_insert2: "A - insert a B = A - {a} - B"
  \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} \<equiv> insert a 0\<close>\<close>
  by blast

lemma insert_Diff_if: "insert x A - B = (if x \ B then A - B else insert x (A - B))"
  by auto

lemma insert_Diff1 [simp]: "x \ B \ insert x A - B = A - B"
  by blast

lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
  by blast

lemma insert_Diff: "a \ A \ insert a (A - {a}) = A"
  by blast

lemma Diff_insert_absorb: "x \ A \ (insert x A) - {x} = A"
  by auto

lemma Diff_disjoint [simp]: "A \ (B - A) = {}"
  by blast

lemma Diff_partition: "A \ B \ A \ (B - A) = B"
  by blast

lemma double_diff: "A \ B \ B \ C \ B - (C - A) = A"
  by blast

lemma Un_Diff_cancel [simp]: "A \ (B - A) = A \ B"
  by blast

lemma Un_Diff_cancel2 [simp]: "(B - A) \ A = B \ A"
  by blast

lemma Diff_Un: "A - (B \ C) = (A - B) \ (A - C)"
  by blast

lemma Diff_Int: "A - (B \ C) = (A - B) \ (A - C)"
  by blast

lemma Diff_Diff_Int: "A - (A - B) = A \ B"
  by blast

lemma Un_Diff: "(A \ B) - C = (A - C) \ (B - C)"
  by blast

lemma Int_Diff: "(A \ B) - C = A \ (B - C)"
  by blast

lemma Diff_Int_distrib: "C \ (A - B) = (C \ A) - (C \ B)"
  by blast

lemma Diff_Int_distrib2: "(A - B) \ C = (A \ C) - (B \ C)"
  by blast

lemma Diff_Compl [simp]: "A - (- B) = A \ B"
  by auto

lemma Compl_Diff_eq [simp]: "- (A - B) = - A \ B"
  by blast

lemma subset_Compl_singleton [simp]: "A \ - {b} \ b \ A"
  by blast

text \<open>\<^medskip> Quantification over type \<^typ>\<open>bool\<close>.\<close>

lemma bool_induct: "P True \ P False \ P x"
  by (cases x) auto

lemma all_bool_eq: "(\b. P b) \ P True \ P False"
  by (auto intro: bool_induct)

lemma bool_contrapos: "P x \ \ P False \ P True"
  by (cases x) auto

lemma ex_bool_eq: "(\b. P b) \ P True \ P False"
  by (auto intro: bool_contrapos)

lemma UNIV_bool: "UNIV = {False, True}"
  by (auto intro: bool_induct)

text \<open>\<^medskip> \<open>Pow\<close>\<close>

lemma Pow_empty [simp]: "Pow {} = {{}}"
  by (auto simp add: Pow_def)

lemma Pow_singleton_iff [simp]: "Pow X = {Y} \ X = {} \ Y = {}"
  by blast  (* somewhat slow *)

lemma Pow_insert: "Pow (insert a A) = Pow A \ (insert a ` Pow A)"
  by (blast intro: image_eqI [where ?x = "u - {a}" for u])

lemma Pow_Compl: "Pow (- A) = {- B | B. A \ Pow B}"
  by (blast intro: exI [where ?x = "- u" for u])

lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
  by blast

lemma Un_Pow_subset: "Pow A \ Pow B \ Pow (A \ B)"
  by blast

lemma Pow_Int_eq [simp]: "Pow (A \ B) = Pow A \ Pow B"
  by blast

text \<open>\<^medskip> Miscellany.\<close>

lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}"
  by blast

lemma Int_Diff_Un: "A \ B \ (A - B) = A"
  by blast

lemma set_eq_subset: "A = B \ A \ B \ B \ A"
  by blast

lemma subset_iff: "A \ B \ (\t. t \ A \ t \ B)"
  by blast

lemma subset_iff_psubset_eq: "A \ B \ A \ B \ A = B"
  unfolding less_le by blast

lemma all_not_in_conv [simp]: "(\x. x \ A) \ A = {}"
  by blast

lemma ex_in_conv: "(\x. x \ A) \ A \ {}"
  by blast

lemma ball_simps [simp, no_atp]:
  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"
  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"
  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"
  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"
  "\P. (\x\{}. P x) \ True"
  "\P. (\x\UNIV. P x) \ (\x. P x)"
  "\a B P. (\x\insert a B. P x) \ (P a \ (\x\B. P x))"
  "\P Q. (\x\Collect Q. P x) \ (\x. Q x \ P x)"
  "\A P f. (\x\f`A. P x) \ (\x\A. P (f x))"
  "\A P. (\ (\x\A. P x)) \ (\x\A. \ P x)"
  by auto

lemma bex_simps [simp, no_atp]:
  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"
  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"
  "\P. (\x\{}. P x) \ False"
  "\P. (\x\UNIV. P x) \ (\x. P x)"
  "\a B P. (\x\insert a B. P x) \ (P a \ (\x\B. P x))"
  "\P Q. (\x\Collect Q. P x) \ (\x. Q x \ P x)"
  "\A P f. (\x\f`A. P x) \ (\x\A. P (f x))"
  "\A P. (\(\x\A. P x)) \ (\x\A. \ P x)"
  by auto

lemma ex_image_cong_iff [simp, no_atp]:
  "(\x. x\f`A) \ A \ {}" "(\x. x\f`A \ P x) \ (\x\A. P (f x))"
  by auto

subsubsection \<open>Monotonicity of various operations\<close>

lemma image_mono: "A \ B \ f ` A \ f ` B"
  by blast

lemma Pow_mono: "A \ B \ Pow A \ Pow B"
  by blast

lemma insert_mono: "C \ D \ insert a C \ insert a D"
  by blast

lemma Un_mono: "A \ C \ B \ D \ A \ B \ C \ D"
  by (fact sup_mono)

lemma Int_mono: "A \ C \ B \ D \ A \ B \ C \ D"
  by (fact inf_mono)

lemma Diff_mono: "A \ C \ D \ B \ A - B \ C - D"
  by blast

lemma Compl_anti_mono: "A \ B \ - B \ - A"
  by (fact compl_mono)

text \<open>\<^medskip> Monotonicity of implications.\<close>

lemma in_mono: "A \ B \ x \ A \ x \ B"
  by (rule impI) (erule subsetD)

lemma conj_mono: "P1 \ Q1 \ P2 \ Q2 \ (P1 \ P2) \ (Q1 \ Q2)"
  by iprover

lemma disj_mono: "P1 \ Q1 \ P2 \ Q2 \ (P1 \ P2) \ (Q1 \ Q2)"
  by iprover

--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.