src/HOL/Set.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 50580 fbb973a53106 child 51173 3cbb4e95a565 permissions -rw-r--r--
introduce order topology
     1 (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel *)

     2

     3 header {* Set theory for higher-order logic *}

     4

     5 theory Set

     6 imports Lattices

     7 begin

     8

     9 subsection {* Sets as predicates *}

    10

    11 typedecl 'a set

    12

    13 axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" -- "comprehension"

    14   and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" -- "membership"

    15 where

    16   mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"

    17   and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"

    18

    19 notation

    20   member  ("op :") and

    21   member  ("(_/ : _)" [51, 51] 50)

    22

    23 abbreviation not_member where

    24   "not_member x A \<equiv> ~ (x : A)" -- "non-membership"

    25

    26 notation

    27   not_member  ("op ~:") and

    28   not_member  ("(_/ ~: _)" [51, 51] 50)

    29

    30 notation (xsymbols)

    31   member      ("op \<in>") and

    32   member      ("(_/ \<in> _)" [51, 51] 50) and

    33   not_member  ("op \<notin>") and

    34   not_member  ("(_/ \<notin> _)" [51, 51] 50)

    35

    36 notation (HTML output)

    37   member      ("op \<in>") and

    38   member      ("(_/ \<in> _)" [51, 51] 50) and

    39   not_member  ("op \<notin>") and

    40   not_member  ("(_/ \<notin> _)" [51, 51] 50)

    41

    42

    43 text {* Set comprehensions *}

    44

    45 syntax

    46   "_Coll" :: "pttrn => bool => 'a set"    ("(1{_./ _})")

    47 translations

    48   "{x. P}" == "CONST Collect (%x. P)"

    49

    50 syntax

    51   "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")

    52 syntax (xsymbols)

    53   "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")

    54 translations

    55   "{x:A. P}" => "{x. x:A & P}"

    56

    57 lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"

    58   by simp

    59

    60 lemma CollectD: "a \<in> {x. P x} \<Longrightarrow> P a"

    61   by simp

    62

    63 lemma Collect_cong: "(\<And>x. P x = Q x) ==> {x. P x} = {x. Q x}"

    64   by simp

    65

    66 text {*

    67 Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}

    68 to the front (and similarly for @{text "t=x"}):

    69 *}

    70

    71 simproc_setup defined_Collect ("{x. P x & Q x}") = {*

    72   fn _ =>

    73     Quantifier1.rearrange_Collect

    74      (rtac @{thm Collect_cong} 1 THEN

    75       rtac @{thm iffI} 1 THEN

    76       ALLGOALS

    77         (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))

    78 *}

    79

    80 lemmas CollectE = CollectD [elim_format]

    81

    82 lemma set_eqI:

    83   assumes "\<And>x. x \<in> A \<longleftrightarrow> x \<in> B"

    84   shows "A = B"

    85 proof -

    86   from assms have "{x. x \<in> A} = {x. x \<in> B}" by simp

    87   then show ?thesis by simp

    88 qed

    89

    90 lemma set_eq_iff [no_atp]:

    91   "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"

    92   by (auto intro:set_eqI)

    93

    94 text {* Lifting of predicate class instances *}

    95

    96 instantiation set :: (type) boolean_algebra

    97 begin

    98

    99 definition less_eq_set where

   100   "A \<le> B \<longleftrightarrow> (\<lambda>x. member x A) \<le> (\<lambda>x. member x B)"

   101

   102 definition less_set where

   103   "A < B \<longleftrightarrow> (\<lambda>x. member x A) < (\<lambda>x. member x B)"

   104

   105 definition inf_set where

   106   "A \<sqinter> B = Collect ((\<lambda>x. member x A) \<sqinter> (\<lambda>x. member x B))"

   107

   108 definition sup_set where

   109   "A \<squnion> B = Collect ((\<lambda>x. member x A) \<squnion> (\<lambda>x. member x B))"

   110

   111 definition bot_set where

   112   "\<bottom> = Collect \<bottom>"

   113

   114 definition top_set where

   115   "\<top> = Collect \<top>"

   116

   117 definition uminus_set where

   118   "- A = Collect (- (\<lambda>x. member x A))"

   119

   120 definition minus_set where

   121   "A - B = Collect ((\<lambda>x. member x A) - (\<lambda>x. member x B))"

   122

   123 instance proof

   124 qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def

   125   bot_set_def top_set_def uminus_set_def minus_set_def

   126   less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq

   127   set_eqI fun_eq_iff

   128   del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)

   129

   130 end

   131

   132 text {* Set enumerations *}

   133

   134 abbreviation empty :: "'a set" ("{}") where

   135   "{} \<equiv> bot"

   136

   137 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where

   138   insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"

   139

   140 syntax

   141   "_Finset" :: "args => 'a set"    ("{(_)}")

   142 translations

   143   "{x, xs}" == "CONST insert x {xs}"

   144   "{x}" == "CONST insert x {}"

   145

   146

   147 subsection {* Subsets and bounded quantifiers *}

   148

   149 abbreviation

   150   subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where

   151   "subset \<equiv> less"

   152

   153 abbreviation

   154   subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where

   155   "subset_eq \<equiv> less_eq"

   156

   157 notation (output)

   158   subset  ("op <") and

   159   subset  ("(_/ < _)" [51, 51] 50) and

   160   subset_eq  ("op <=") and

   161   subset_eq  ("(_/ <= _)" [51, 51] 50)

   162

   163 notation (xsymbols)

   164   subset  ("op \<subset>") and

   165   subset  ("(_/ \<subset> _)" [51, 51] 50) and

   166   subset_eq  ("op \<subseteq>") and

   167   subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)

   168

   169 notation (HTML output)

   170   subset  ("op \<subset>") and

   171   subset  ("(_/ \<subset> _)" [51, 51] 50) and

   172   subset_eq  ("op \<subseteq>") and

   173   subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)

   174

   175 abbreviation (input)

   176   supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where

   177   "supset \<equiv> greater"

   178

   179 abbreviation (input)

   180   supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where

   181   "supset_eq \<equiv> greater_eq"

   182

   183 notation (xsymbols)

   184   supset  ("op \<supset>") and

   185   supset  ("(_/ \<supset> _)" [51, 51] 50) and

   186   supset_eq  ("op \<supseteq>") and

   187   supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)

   188

   189 definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where

   190   "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"

   191

   192 definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where

   193   "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   -- "bounded existential quantifiers"

   194

   195 syntax

   196   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)

   197   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)

   198   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)

   199   "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST _:_./ _)" [0, 0, 10] 10)

   200

   201 syntax (HOL)

   202   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)

   203   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)

   204   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)

   205

   206 syntax (xsymbols)

   207   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)

   208   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)

   209   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)

   210   "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)

   211

   212 syntax (HTML output)

   213   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)

   214   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)

   215   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)

   216

   217 translations

   218   "ALL x:A. P" == "CONST Ball A (%x. P)"

   219   "EX x:A. P" == "CONST Bex A (%x. P)"

   220   "EX! x:A. P" => "EX! x. x:A & P"

   221   "LEAST x:A. P" => "LEAST x. x:A & P"

   222

   223 syntax (output)

   224   "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)

   225   "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)

   226   "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)

   227   "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)

   228   "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)

   229

   230 syntax (xsymbols)

   231   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)

   232   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)

   233   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)

   234   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)

   235   "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)

   236

   237 syntax (HOL output)

   238   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)

   239   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)

   240   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)

   241   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)

   242   "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)

   243

   244 syntax (HTML output)

   245   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)

   246   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)

   247   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)

   248   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)

   249   "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)

   250

   251 translations

   252  "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"

   253  "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"

   254  "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"

   255  "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"

   256  "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"

   257

   258 print_translation {*

   259 let

   260   val All_binder = Mixfix.binder_name @{const_syntax All};

   261   val Ex_binder = Mixfix.binder_name @{const_syntax Ex};

   262   val impl = @{const_syntax HOL.implies};

   263   val conj = @{const_syntax HOL.conj};

   264   val sbset = @{const_syntax subset};

   265   val sbset_eq = @{const_syntax subset_eq};

   266

   267   val trans =

   268    [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),

   269     ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),

   270     ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),

   271     ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];

   272

   273   fun mk v (v', T) c n P =

   274     if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)

   275     then Syntax.const c $Syntax_Trans.mark_bound_body (v', T)$ n $P else raise Match;   276   277 fun tr' q = (q,   278 fn [Const (@{syntax_const "_bound"}, _)$ Free (v, Type (@{type_name set}, _)),

   279             Const (c, _) $  280 (Const (d, _)$ (Const (@{syntax_const "_bound"}, _) $Free (v', T))$ n) $P] =>   281 (case AList.lookup (op =) trans (q, c, d) of   282 NONE => raise Match   283 | SOME l => mk v (v', T) l n P)   284 | _ => raise Match);   285 in   286 [tr' All_binder, tr' Ex_binder]   287 end   288 *}   289   290   291 text {*   292 \medskip Translate between @{text "{e | x1...xn. P}"} and @{text   293 "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is   294 only translated if @{text "[0..n] subset bvs(e)"}.   295 *}   296   297 syntax   298 "_Setcompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")   299   300 parse_translation {*   301 let   302 val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex}));   303   304 fun nvars (Const (@{syntax_const "_idts"}, _)$ _ $idts) = nvars idts + 1   305 | nvars _ = 1;   306   307 fun setcompr_tr [e, idts, b] =   308 let   309 val eq = Syntax.const @{const_syntax HOL.eq}$ Bound (nvars idts) $e;   310 val P = Syntax.const @{const_syntax HOL.conj}$ eq $b;   311 val exP = ex_tr [idts, P];   312 in Syntax.const @{const_syntax Collect}$ absdummy dummyT exP end;

   313

   314   in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;

   315 *}

   316

   317 print_translation {*

   318  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},

   319   Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]

   320 *} -- {* to avoid eta-contraction of body *}

   321

   322 print_translation {*

   323 let

   324   val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));

   325

   326   fun setcompr_tr' [Abs (abs as (_, _, P))] =

   327     let

   328       fun check (Const (@{const_syntax Ex}, _) $Abs (_, _, P), n) = check (P, n + 1)   329 | check (Const (@{const_syntax HOL.conj}, _)$

   330               (Const (@{const_syntax HOL.eq}, _) $Bound m$ e) $P, n) =   331 n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso   332 subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))   333 | check _ = false;   334   335 fun tr' (_$ abs) =

   336           let val _ $idts$ (_ $(_$ _ $e)$ Q) = ex_tr' [abs]

   337           in Syntax.const @{syntax_const "_Setcompr"} $e$ idts $Q end;   338 in   339 if check (P, 0) then tr' P   340 else   341 let   342 val (x as _$ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;

   343           val M = Syntax.const @{syntax_const "_Coll"} $x$ t;

   344         in

   345           case t of

   346             Const (@{const_syntax HOL.conj}, _) $  347 (Const (@{const_syntax Set.member}, _)$

   348                 (Const (@{syntax_const "_bound"}, _) $Free (yN, _))$ A) $P =>   349 if xN = yN then Syntax.const @{syntax_const "_Collect"}$ x $A$ P else M

   350           | _ => M

   351         end

   352     end;

   353   in [(@{const_syntax Collect}, setcompr_tr')] end;

   354 *}

   355

   356 simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*

   357   let

   358     val unfold_bex_tac = unfold_tac @{thms Bex_def};

   359     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;

   360   in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end

   361 *}

   362

   363 simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*

   364   let

   365     val unfold_ball_tac = unfold_tac @{thms Ball_def};

   366     fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;

   367   in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end

   368 *}

   369

   370 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"

   371   by (simp add: Ball_def)

   372

   373 lemmas strip = impI allI ballI

   374

   375 lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"

   376   by (simp add: Ball_def)

   377

   378 text {*

   379   Gives better instantiation for bound:

   380 *}

   381

   382 declaration {* fn _ =>

   383   Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))

   384 *}

   385

   386 ML {*

   387 structure Simpdata =

   388 struct

   389

   390 open Simpdata;

   391

   392 val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;

   393

   394 end;

   395

   396 open Simpdata;

   397 *}

   398

   399 declaration {* fn _ =>

   400   Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))

   401 *}

   402

   403 lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"

   404   by (unfold Ball_def) blast

   405

   406 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"

   407   -- {* Normally the best argument order: @{prop "P x"} constrains the

   408     choice of @{prop "x:A"}. *}

   409   by (unfold Bex_def) blast

   410

   411 lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x"

   412   -- {* The best argument order when there is only one @{prop "x:A"}. *}

   413   by (unfold Bex_def) blast

   414

   415 lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"

   416   by (unfold Bex_def) blast

   417

   418 lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q"

   419   by (unfold Bex_def) blast

   420

   421 lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"

   422   -- {* Trival rewrite rule. *}

   423   by (simp add: Ball_def)

   424

   425 lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"

   426   -- {* Dual form for existentials. *}

   427   by (simp add: Bex_def)

   428

   429 lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"

   430   by blast

   431

   432 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"

   433   by blast

   434

   435 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"

   436   by blast

   437

   438 lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)"

   439   by blast

   440

   441 lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)"

   442   by blast

   443

   444 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"

   445   by blast

   446

   447 lemma ball_conj_distrib:

   448   "(\<forall>x\<in>A. P x \<and> Q x) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>A. Q x))"

   449   by blast

   450

   451 lemma bex_disj_distrib:

   452   "(\<exists>x\<in>A. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>A. Q x))"

   453   by blast

   454

   455

   456 text {* Congruence rules *}

   457

   458 lemma ball_cong:

   459   "A = B ==> (!!x. x:B ==> P x = Q x) ==>

   460     (ALL x:A. P x) = (ALL x:B. Q x)"

   461   by (simp add: Ball_def)

   462

   463 lemma strong_ball_cong [cong]:

   464   "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>

   465     (ALL x:A. P x) = (ALL x:B. Q x)"

   466   by (simp add: simp_implies_def Ball_def)

   467

   468 lemma bex_cong:

   469   "A = B ==> (!!x. x:B ==> P x = Q x) ==>

   470     (EX x:A. P x) = (EX x:B. Q x)"

   471   by (simp add: Bex_def cong: conj_cong)

   472

   473 lemma strong_bex_cong [cong]:

   474   "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>

   475     (EX x:A. P x) = (EX x:B. Q x)"

   476   by (simp add: simp_implies_def Bex_def cong: conj_cong)

   477

   478

   479 subsection {* Basic operations *}

   480

   481 subsubsection {* Subsets *}

   482

   483 lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"

   484   by (simp add: less_eq_set_def le_fun_def)

   485

   486 text {*

   487   \medskip Map the type @{text "'a set => anything"} to just @{typ

   488   'a}; for overloading constants whose first argument has type @{typ

   489   "'a set"}.

   490 *}

   491

   492 lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"

   493   by (simp add: less_eq_set_def le_fun_def)

   494   -- {* Rule in Modus Ponens style. *}

   495

   496 lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"

   497   -- {* The same, with reversed premises for use with @{text erule} --

   498       cf @{text rev_mp}. *}

   499   by (rule subsetD)

   500

   501 text {*

   502   \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.

   503 *}

   504

   505 lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"

   506   -- {* Classical elimination rule. *}

   507   by (auto simp add: less_eq_set_def le_fun_def)

   508

   509 lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast

   510

   511 lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"

   512   by blast

   513

   514 lemma subset_refl: "A \<subseteq> A"

   515   by (fact order_refl) (* already [iff] *)

   516

   517 lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"

   518   by (fact order_trans)

   519

   520 lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"

   521   by (rule subsetD)

   522

   523 lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"

   524   by (rule subsetD)

   525

   526 lemma subset_not_subset_eq [code]:

   527   "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"

   528   by (fact less_le_not_le)

   529

   530 lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"

   531   by simp

   532

   533 lemmas basic_trans_rules [trans] =

   534   order_trans_rules set_rev_mp set_mp eq_mem_trans

   535

   536

   537 subsubsection {* Equality *}

   538

   539 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"

   540   -- {* Anti-symmetry of the subset relation. *}

   541   by (iprover intro: set_eqI subsetD)

   542

   543 text {*

   544   \medskip Equality rules from ZF set theory -- are they appropriate

   545   here?

   546 *}

   547

   548 lemma equalityD1: "A = B ==> A \<subseteq> B"

   549   by simp

   550

   551 lemma equalityD2: "A = B ==> B \<subseteq> A"

   552   by simp

   553

   554 text {*

   555   \medskip Be careful when adding this to the claset as @{text

   556   subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}

   557   \<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!

   558 *}

   559

   560 lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"

   561   by simp

   562

   563 lemma equalityCE [elim]:

   564     "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"

   565   by blast

   566

   567 lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"

   568   by simp

   569

   570 lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"

   571   by simp

   572

   573

   574 subsubsection {* The empty set *}

   575

   576 lemma empty_def:

   577   "{} = {x. False}"

   578   by (simp add: bot_set_def bot_fun_def)

   579

   580 lemma empty_iff [simp]: "(c : {}) = False"

   581   by (simp add: empty_def)

   582

   583 lemma emptyE [elim!]: "a : {} ==> P"

   584   by simp

   585

   586 lemma empty_subsetI [iff]: "{} \<subseteq> A"

   587     -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}

   588   by blast

   589

   590 lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"

   591   by blast

   592

   593 lemma equals0D: "A = {} ==> a \<notin> A"

   594     -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}

   595   by blast

   596

   597 lemma ball_empty [simp]: "Ball {} P = True"

   598   by (simp add: Ball_def)

   599

   600 lemma bex_empty [simp]: "Bex {} P = False"

   601   by (simp add: Bex_def)

   602

   603

   604 subsubsection {* The universal set -- UNIV *}

   605

   606 abbreviation UNIV :: "'a set" where

   607   "UNIV \<equiv> top"

   608

   609 lemma UNIV_def:

   610   "UNIV = {x. True}"

   611   by (simp add: top_set_def top_fun_def)

   612

   613 lemma UNIV_I [simp]: "x : UNIV"

   614   by (simp add: UNIV_def)

   615

   616 declare UNIV_I [intro]  -- {* unsafe makes it less likely to cause problems *}

   617

   618 lemma UNIV_witness [intro?]: "EX x. x : UNIV"

   619   by simp

   620

   621 lemma subset_UNIV: "A \<subseteq> UNIV"

   622   by (fact top_greatest) (* already simp *)

   623

   624 text {*

   625   \medskip Eta-contracting these two rules (to remove @{text P})

   626   causes them to be ignored because of their interaction with

   627   congruence rules.

   628 *}

   629

   630 lemma ball_UNIV [simp]: "Ball UNIV P = All P"

   631   by (simp add: Ball_def)

   632

   633 lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"

   634   by (simp add: Bex_def)

   635

   636 lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"

   637   by auto

   638

   639 lemma UNIV_not_empty [iff]: "UNIV ~= {}"

   640   by (blast elim: equalityE)

   641

   642

   643 subsubsection {* The Powerset operator -- Pow *}

   644

   645 definition Pow :: "'a set => 'a set set" where

   646   Pow_def: "Pow A = {B. B \<le> A}"

   647

   648 lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)"

   649   by (simp add: Pow_def)

   650

   651 lemma PowI: "A \<subseteq> B ==> A \<in> Pow B"

   652   by (simp add: Pow_def)

   653

   654 lemma PowD: "A \<in> Pow B ==> A \<subseteq> B"

   655   by (simp add: Pow_def)

   656

   657 lemma Pow_bottom: "{} \<in> Pow B"

   658   by simp

   659

   660 lemma Pow_top: "A \<in> Pow A"

   661   by simp

   662

   663 lemma Pow_not_empty: "Pow A \<noteq> {}"

   664   using Pow_top by blast

   665

   666

   667 subsubsection {* Set complement *}

   668

   669 lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"

   670   by (simp add: fun_Compl_def uminus_set_def)

   671

   672 lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"

   673   by (simp add: fun_Compl_def uminus_set_def) blast

   674

   675 text {*

   676   \medskip This form, with negated conclusion, works well with the

   677   Classical prover.  Negated assumptions behave like formulae on the

   678   right side of the notional turnstile ... *}

   679

   680 lemma ComplD [dest!]: "c : -A ==> c~:A"

   681   by simp

   682

   683 lemmas ComplE = ComplD [elim_format]

   684

   685 lemma Compl_eq: "- A = {x. ~ x : A}"

   686   by blast

   687

   688

   689 subsubsection {* Binary intersection *}

   690

   691 abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where

   692   "op Int \<equiv> inf"

   693

   694 notation (xsymbols)

   695   inter  (infixl "\<inter>" 70)

   696

   697 notation (HTML output)

   698   inter  (infixl "\<inter>" 70)

   699

   700 lemma Int_def:

   701   "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"

   702   by (simp add: inf_set_def inf_fun_def)

   703

   704 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"

   705   by (unfold Int_def) blast

   706

   707 lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"

   708   by simp

   709

   710 lemma IntD1: "c : A Int B ==> c:A"

   711   by simp

   712

   713 lemma IntD2: "c : A Int B ==> c:B"

   714   by simp

   715

   716 lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"

   717   by simp

   718

   719 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"

   720   by (fact mono_inf)

   721

   722

   723 subsubsection {* Binary union *}

   724

   725 abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where

   726   "union \<equiv> sup"

   727

   728 notation (xsymbols)

   729   union  (infixl "\<union>" 65)

   730

   731 notation (HTML output)

   732   union  (infixl "\<union>" 65)

   733

   734 lemma Un_def:

   735   "A \<union> B = {x. x \<in> A \<or> x \<in> B}"

   736   by (simp add: sup_set_def sup_fun_def)

   737

   738 lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"

   739   by (unfold Un_def) blast

   740

   741 lemma UnI1 [elim?]: "c:A ==> c : A Un B"

   742   by simp

   743

   744 lemma UnI2 [elim?]: "c:B ==> c : A Un B"

   745   by simp

   746

   747 text {*

   748   \medskip Classical introduction rule: no commitment to @{prop A} vs

   749   @{prop B}.

   750 *}

   751

   752 lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"

   753   by auto

   754

   755 lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"

   756   by (unfold Un_def) blast

   757

   758 lemma insert_def: "insert a B = {x. x = a} \<union> B"

   759   by (simp add: insert_compr Un_def)

   760

   761 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"

   762   by (fact mono_sup)

   763

   764

   765 subsubsection {* Set difference *}

   766

   767 lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"

   768   by (simp add: minus_set_def fun_diff_def)

   769

   770 lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"

   771   by simp

   772

   773 lemma DiffD1: "c : A - B ==> c : A"

   774   by simp

   775

   776 lemma DiffD2: "c : A - B ==> c : B ==> P"

   777   by simp

   778

   779 lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"

   780   by simp

   781

   782 lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast

   783

   784 lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"

   785 by blast

   786

   787

   788 subsubsection {* Augmenting a set -- @{const insert} *}

   789

   790 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"

   791   by (unfold insert_def) blast

   792

   793 lemma insertI1: "a : insert a B"

   794   by simp

   795

   796 lemma insertI2: "a : B ==> a : insert b B"

   797   by simp

   798

   799 lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"

   800   by (unfold insert_def) blast

   801

   802 lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"

   803   -- {* Classical introduction rule. *}

   804   by auto

   805

   806 lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"

   807   by auto

   808

   809 lemma set_insert:

   810   assumes "x \<in> A"

   811   obtains B where "A = insert x B" and "x \<notin> B"

   812 proof

   813   from assms show "A = insert x (A - {x})" by blast

   814 next

   815   show "x \<notin> A - {x}" by blast

   816 qed

   817

   818 lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"

   819 by auto

   820

   821 lemma insert_eq_iff: assumes "a \<notin> A" "b \<notin> B"

   822 shows "insert a A = insert b B \<longleftrightarrow>

   823   (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)"

   824   (is "?L \<longleftrightarrow> ?R")

   825 proof

   826   assume ?L

   827   show ?R

   828   proof cases

   829     assume "a=b" with assms ?L show ?R by (simp add: insert_ident)

   830   next

   831     assume "a\<noteq>b"

   832     let ?C = "A - {b}"

   833     have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"

   834       using assms ?L a\<noteq>b by auto

   835     thus ?R using a\<noteq>b by auto

   836   qed

   837 next

   838   assume ?R thus ?L by (auto split: if_splits)

   839 qed

   840

   841 subsubsection {* Singletons, using insert *}

   842

   843 lemma singletonI [intro!,no_atp]: "a : {a}"

   844     -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}

   845   by (rule insertI1)

   846

   847 lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"

   848   by blast

   849

   850 lemmas singletonE = singletonD [elim_format]

   851

   852 lemma singleton_iff: "(b : {a}) = (b = a)"

   853   by blast

   854

   855 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"

   856   by blast

   857

   858 lemma singleton_insert_inj_eq [iff,no_atp]:

   859      "({b} = insert a A) = (a = b & A \<subseteq> {b})"

   860   by blast

   861

   862 lemma singleton_insert_inj_eq' [iff,no_atp]:

   863      "(insert a A = {b}) = (a = b & A \<subseteq> {b})"

   864   by blast

   865

   866 lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"

   867   by fast

   868

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

   870   by blast

   871

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

   873   by blast

   874

   875 lemma diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"

   876   by blast

   877

   878 lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"

   879   by (blast elim: equalityE)

   880

   881

   882 subsubsection {* Image of a set under a function *}

   883

   884 text {*

   885   Frequently @{term b} does not have the syntactic form of @{term "f x"}.

   886 *}

   887

   888 definition image :: "('a => 'b) => 'a set => 'b set" (infixr "" 90) where

   889   image_def [no_atp]: "f  A = {y. EX x:A. y = f(x)}"

   890

   891 abbreviation

   892   range :: "('a => 'b) => 'b set" where -- "of function"

   893   "range f == f  UNIV"

   894

   895 lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : fA"

   896   by (unfold image_def) blast

   897

   898 lemma imageI: "x : A ==> f x : f  A"

   899   by (rule image_eqI) (rule refl)

   900

   901 lemma rev_image_eqI: "x:A ==> b = f x ==> b : fA"

   902   -- {* This version's more effective when we already have the

   903     required @{term x}. *}

   904   by (unfold image_def) blast

   905

   906 lemma imageE [elim!]:

   907   "b : (%x. f x)A ==> (!!x. b = f x ==> x:A ==> P) ==> P"

   908   -- {* The eta-expansion gives variable-name preservation. *}

   909   by (unfold image_def) blast

   910

   911 lemma image_Un: "f(A Un B) = fA Un fB"

   912   by blast

   913

   914 lemma image_iff: "(z : fA) = (EX x:A. z = f x)"

   915   by blast

   916

   917 lemma image_subset_iff [no_atp]: "(fA \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"

   918   -- {* This rewrite rule would confuse users if made default. *}

   919   by blast

   920

   921 lemma subset_image_iff: "(B \<subseteq> fA) = (EX AA. AA \<subseteq> A & B = fAA)"

   922   apply safe

   923    prefer 2 apply fast

   924   apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)

   925   done

   926

   927 lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> fA \<subseteq> B"

   928   -- {* Replaces the three steps @{text subsetI}, @{text imageE},

   929     @{text hypsubst}, but breaks too many existing proofs. *}

   930   by blast

   931

   932 text {*

   933   \medskip Range of a function -- just a translation for image!

   934 *}

   935

   936 lemma image_ident [simp]: "(%x. x)  Y = Y"

   937   by blast

   938

   939 lemma range_eqI: "b = f x ==> b \<in> range f"

   940   by simp

   941

   942 lemma rangeI: "f x \<in> range f"

   943   by simp

   944

   945 lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"

   946   by blast

   947

   948 subsubsection {* Some rules with @{text "if"} *}

   949

   950 text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}

   951

   952 lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"

   953   by auto

   954

   955 lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"

   956   by auto

   957

   958 text {*

   959   Rewrite rules for boolean case-splitting: faster than @{text

   960   "split_if [split]"}.

   961 *}

   962

   963 lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"

   964   by (rule split_if)

   965

   966 lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"

   967   by (rule split_if)

   968

   969 text {*

   970   Split ifs on either side of the membership relation.  Not for @{text

   971   "[simp]"} -- can cause goals to blow up!

   972 *}

   973

   974 lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"

   975   by (rule split_if)

   976

   977 lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"

   978   by (rule split_if [where P="%S. a : S"])

   979

   980 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2

   981

   982 (*Would like to add these, but the existing code only searches for the

   983   outer-level constant, which in this case is just Set.member; we instead need

   984   to use term-nets to associate patterns with rules.  Also, if a rule fails to

   985   apply, then the formula should be kept.

   986   [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),

   987    ("Int", [IntD1,IntD2]),

   988    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]

   989  *)

   990

   991

   992 subsection {* Further operations and lemmas *}

   993

   994 subsubsection {* The proper subset'' relation *}

   995

   996 lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"

   997   by (unfold less_le) blast

   998

   999 lemma psubsetE [elim!,no_atp]:

  1000     "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"

  1001   by (unfold less_le) blast

  1002

  1003 lemma psubset_insert_iff:

  1004   "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"

  1005   by (auto simp add: less_le subset_insert_iff)

  1006

  1007 lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"

  1008   by (simp only: less_le)

  1009

  1010 lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"

  1011   by (simp add: psubset_eq)

  1012

  1013 lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"

  1014 apply (unfold less_le)

  1015 apply (auto dest: subset_antisym)

  1016 done

  1017

  1018 lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"

  1019 apply (unfold less_le)

  1020 apply (auto dest: subsetD)

  1021 done

  1022

  1023 lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"

  1024   by (auto simp add: psubset_eq)

  1025

  1026 lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"

  1027   by (auto simp add: psubset_eq)

  1028

  1029 lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"

  1030   by (unfold less_le) blast

  1031

  1032 lemma atomize_ball:

  1033     "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"

  1034   by (simp only: Ball_def atomize_all atomize_imp)

  1035

  1036 lemmas [symmetric, rulify] = atomize_ball

  1037   and [symmetric, defn] = atomize_ball

  1038

  1039 lemma image_Pow_mono:

  1040   assumes "f  A \<le> B"

  1041   shows "(image f)  (Pow A) \<le> Pow B"

  1042 using assms by blast

  1043

  1044 lemma image_Pow_surj:

  1045   assumes "f  A = B"

  1046   shows "(image f)  (Pow A) = Pow B"

  1047 using assms unfolding Pow_def proof(auto)

  1048   fix Y assume *: "Y \<le> f  A"

  1049   obtain X where X_def: "X = {x \<in> A. f x \<in> Y}" by blast

  1050   have "f  X = Y \<and> X \<le> A" unfolding X_def using * by auto

  1051   thus "Y \<in> (image f)  {X. X \<le> A}" by blast

  1052 qed

  1053

  1054 subsubsection {* Derived rules involving subsets. *}

  1055

  1056 text {* @{text insert}. *}

  1057

  1058 lemma subset_insertI: "B \<subseteq> insert a B"

  1059   by (rule subsetI) (erule insertI2)

  1060

  1061 lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"

  1062   by blast

  1063

  1064 lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"

  1065   by blast

  1066

  1067

  1068 text {* \medskip Finite Union -- the least upper bound of two sets. *}

  1069

  1070 lemma Un_upper1: "A \<subseteq> A \<union> B"

  1071   by (fact sup_ge1)

  1072

  1073 lemma Un_upper2: "B \<subseteq> A \<union> B"

  1074   by (fact sup_ge2)

  1075

  1076 lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"

  1077   by (fact sup_least)

  1078

  1079

  1080 text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}

  1081

  1082 lemma Int_lower1: "A \<inter> B \<subseteq> A"

  1083   by (fact inf_le1)

  1084

  1085 lemma Int_lower2: "A \<inter> B \<subseteq> B"

  1086   by (fact inf_le2)

  1087

  1088 lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"

  1089   by (fact inf_greatest)

  1090

  1091

  1092 text {* \medskip Set difference. *}

  1093

  1094 lemma Diff_subset: "A - B \<subseteq> A"

  1095   by blast

  1096

  1097 lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"

  1098 by blast

  1099

  1100

  1101 subsubsection {* Equalities involving union, intersection, inclusion, etc. *}

  1102

  1103 text {* @{text "{}"}. *}

  1104

  1105 lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"

  1106   -- {* supersedes @{text "Collect_False_empty"} *}

  1107   by auto

  1108

  1109 lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"

  1110   by (fact bot_unique)

  1111

  1112 lemma not_psubset_empty [iff]: "\<not> (A < {})"

  1113   by (fact not_less_bot) (* FIXME: already simp *)

  1114

  1115 lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"

  1116 by blast

  1117

  1118 lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"

  1119 by blast

  1120

  1121 lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"

  1122   by blast

  1123

  1124 lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"

  1125   by blast

  1126

  1127 lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}"

  1128   by blast

  1129

  1130 lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"

  1131   by blast

  1132

  1133

  1134 text {* \medskip @{text insert}. *}

  1135

  1136 lemma insert_is_Un: "insert a A = {a} Un A"

  1137   -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}

  1138   by blast

  1139

  1140 lemma insert_not_empty [simp]: "insert a A \<noteq> {}"

  1141   by blast

  1142

  1143 lemmas empty_not_insert = insert_not_empty [symmetric]

  1144 declare empty_not_insert [simp]

  1145

  1146 lemma insert_absorb: "a \<in> A ==> insert a A = A"

  1147   -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}

  1148   -- {* with \emph{quadratic} running time *}

  1149   by blast

  1150

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

  1152   by blast

  1153

  1154 lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"

  1155   by blast

  1156

  1157 lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"

  1158   by blast

  1159

  1160 lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"

  1161   -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}

  1162   apply (rule_tac x = "A - {a}" in exI, blast)

  1163   done

  1164

  1165 lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"

  1166   by auto

  1167

  1168 lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"

  1169   by blast

  1170

  1171 lemma insert_disjoint [simp,no_atp]:

  1172  "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"

  1173  "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"

  1174   by auto

  1175

  1176 lemma disjoint_insert [simp,no_atp]:

  1177  "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"

  1178  "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"

  1179   by auto

  1180

  1181 text {* \medskip @{text image}. *}

  1182

  1183 lemma image_empty [simp]: "f{} = {}"

  1184   by blast

  1185

  1186 lemma image_insert [simp]: "f  insert a B = insert (f a) (fB)"

  1187   by blast

  1188

  1189 lemma image_constant: "x \<in> A ==> (\<lambda>x. c)  A = {c}"

  1190   by auto

  1191

  1192 lemma image_constant_conv: "(%x. c)  A = (if A = {} then {} else {c})"

  1193 by auto

  1194

  1195 lemma image_image: "f  (g  A) = (\<lambda>x. f (g x))  A"

  1196 by blast

  1197

  1198 lemma insert_image [simp]: "x \<in> A ==> insert (f x) (fA) = fA"

  1199 by blast

  1200

  1201 lemma image_is_empty [iff]: "(fA = {}) = (A = {})"

  1202 by blast

  1203

  1204 lemma empty_is_image[iff]: "({} = f  A) = (A = {})"

  1205 by blast

  1206

  1207

  1208 lemma image_Collect [no_atp]: "f  {x. P x} = {f x | x. P x}"

  1209   -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,

  1210       with its implicit quantifier and conjunction.  Also image enjoys better

  1211       equational properties than does the RHS. *}

  1212   by blast

  1213

  1214 lemma if_image_distrib [simp]:

  1215   "(\<lambda>x. if P x then f x else g x)  S

  1216     = (f  (S \<inter> {x. P x})) \<union> (g  (S \<inter> {x. \<not> P x}))"

  1217   by (auto simp add: image_def)

  1218

  1219 lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> fM = gN"

  1220   by (simp add: image_def)

  1221

  1222 lemma image_Int_subset: "f(A Int B) <= fA Int fB"

  1223 by blast

  1224

  1225 lemma image_diff_subset: "fA - fB <= f(A - B)"

  1226 by blast

  1227

  1228

  1229 text {* \medskip @{text range}. *}

  1230

  1231 lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"

  1232   by auto

  1233

  1234 lemma range_composition: "range (\<lambda>x. f (g x)) = frange g"

  1235 by (subst image_image, simp)

  1236

  1237

  1238 text {* \medskip @{text Int} *}

  1239

  1240 lemma Int_absorb: "A \<inter> A = A"

  1241   by (fact inf_idem) (* already simp *)

  1242

  1243 lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"

  1244   by (fact inf_left_idem)

  1245

  1246 lemma Int_commute: "A \<inter> B = B \<inter> A"

  1247   by (fact inf_commute)

  1248

  1249 lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"

  1250   by (fact inf_left_commute)

  1251

  1252 lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"

  1253   by (fact inf_assoc)

  1254

  1255 lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute

  1256   -- {* Intersection is an AC-operator *}

  1257

  1258 lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"

  1259   by (fact inf_absorb2)

  1260

  1261 lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"

  1262   by (fact inf_absorb1)

  1263

  1264 lemma Int_empty_left: "{} \<inter> B = {}"

  1265   by (fact inf_bot_left) (* already simp *)

  1266

  1267 lemma Int_empty_right: "A \<inter> {} = {}"

  1268   by (fact inf_bot_right) (* already simp *)

  1269

  1270 lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"

  1271   by blast

  1272

  1273 lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"

  1274   by blast

  1275

  1276 lemma Int_UNIV_left: "UNIV \<inter> B = B"

  1277   by (fact inf_top_left) (* already simp *)

  1278

  1279 lemma Int_UNIV_right: "A \<inter> UNIV = A"

  1280   by (fact inf_top_right) (* already simp *)

  1281

  1282 lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"

  1283   by (fact inf_sup_distrib1)

  1284

  1285 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"

  1286   by (fact inf_sup_distrib2)

  1287

  1288 lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"

  1289   by (fact inf_eq_top_iff) (* already simp *)

  1290

  1291 lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"

  1292   by (fact le_inf_iff)

  1293

  1294 lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"

  1295   by blast

  1296

  1297

  1298 text {* \medskip @{text Un}. *}

  1299

  1300 lemma Un_absorb: "A \<union> A = A"

  1301   by (fact sup_idem) (* already simp *)

  1302

  1303 lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"

  1304   by (fact sup_left_idem)

  1305

  1306 lemma Un_commute: "A \<union> B = B \<union> A"

  1307   by (fact sup_commute)

  1308

  1309 lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"

  1310   by (fact sup_left_commute)

  1311

  1312 lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"

  1313   by (fact sup_assoc)

  1314

  1315 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute

  1316   -- {* Union is an AC-operator *}

  1317

  1318 lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"

  1319   by (fact sup_absorb2)

  1320

  1321 lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"

  1322   by (fact sup_absorb1)

  1323

  1324 lemma Un_empty_left: "{} \<union> B = B"

  1325   by (fact sup_bot_left) (* already simp *)

  1326

  1327 lemma Un_empty_right: "A \<union> {} = A"

  1328   by (fact sup_bot_right) (* already simp *)

  1329

  1330 lemma Un_UNIV_left: "UNIV \<union> B = UNIV"

  1331   by (fact sup_top_left) (* already simp *)

  1332

  1333 lemma Un_UNIV_right: "A \<union> UNIV = UNIV"

  1334   by (fact sup_top_right) (* already simp *)

  1335

  1336 lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"

  1337   by blast

  1338

  1339 lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"

  1340   by blast

  1341

  1342 lemma Int_insert_left:

  1343     "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"

  1344   by auto

  1345

  1346 lemma Int_insert_left_if0[simp]:

  1347     "a \<notin> C \<Longrightarrow> (insert a B) Int C = B \<inter> C"

  1348   by auto

  1349

  1350 lemma Int_insert_left_if1[simp]:

  1351     "a \<in> C \<Longrightarrow> (insert a B) Int C = insert a (B Int C)"

  1352   by auto

  1353

  1354 lemma Int_insert_right:

  1355     "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"

  1356   by auto

  1357

  1358 lemma Int_insert_right_if0[simp]:

  1359     "a \<notin> A \<Longrightarrow> A Int (insert a B) = A Int B"

  1360   by auto

  1361

  1362 lemma Int_insert_right_if1[simp]:

  1363     "a \<in> A \<Longrightarrow> A Int (insert a B) = insert a (A Int B)"

  1364   by auto

  1365

  1366 lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"

  1367   by (fact sup_inf_distrib1)

  1368

  1369 lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"

  1370   by (fact sup_inf_distrib2)

  1371

  1372 lemma Un_Int_crazy:

  1373     "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"

  1374   by blast

  1375

  1376 lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"

  1377   by (fact le_iff_sup)

  1378

  1379 lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"

  1380   by (fact sup_eq_bot_iff) (* FIXME: already simp *)

  1381

  1382 lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"

  1383   by (fact le_sup_iff)

  1384

  1385 lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"

  1386   by blast

  1387

  1388 lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"

  1389   by blast

  1390

  1391

  1392 text {* \medskip Set complement *}

  1393

  1394 lemma Compl_disjoint [simp]: "A \<inter> -A = {}"

  1395   by (fact inf_compl_bot)

  1396

  1397 lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"

  1398   by (fact compl_inf_bot)

  1399

  1400 lemma Compl_partition: "A \<union> -A = UNIV"

  1401   by (fact sup_compl_top)

  1402

  1403 lemma Compl_partition2: "-A \<union> A = UNIV"

  1404   by (fact compl_sup_top)

  1405

  1406 lemma double_complement: "- (-A) = (A::'a set)"

  1407   by (fact double_compl) (* already simp *)

  1408

  1409 lemma Compl_Un: "-(A \<union> B) = (-A) \<inter> (-B)"

  1410   by (fact compl_sup) (* already simp *)

  1411

  1412 lemma Compl_Int: "-(A \<inter> B) = (-A) \<union> (-B)"

  1413   by (fact compl_inf) (* already simp *)

  1414

  1415 lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"

  1416   by blast

  1417

  1418 lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"

  1419   -- {* Halmos, Naive Set Theory, page 16. *}

  1420   by blast

  1421

  1422 lemma Compl_UNIV_eq: "-UNIV = {}"

  1423   by (fact compl_top_eq) (* already simp *)

  1424

  1425 lemma Compl_empty_eq: "-{} = UNIV"

  1426   by (fact compl_bot_eq) (* already simp *)

  1427

  1428 lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"

  1429   by (fact compl_le_compl_iff) (* FIXME: already simp *)

  1430

  1431 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"

  1432   by (fact compl_eq_compl_iff) (* FIXME: already simp *)

  1433

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

  1435   by blast

  1436

  1437 text {* \medskip Bounded quantifiers.

  1438

  1439   The following are not added to the default simpset because

  1440   (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}

  1441

  1442 lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"

  1443   by blast

  1444

  1445 lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"

  1446   by blast

  1447

  1448

  1449 text {* \medskip Set difference. *}

  1450

  1451 lemma Diff_eq: "A - B = A \<inter> (-B)"

  1452   by blast

  1453

  1454 lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"

  1455   by blast

  1456

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

  1458   by blast

  1459

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

  1461 by blast

  1462

  1463 lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"

  1464   by (blast elim: equalityE)

  1465

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

  1467   by blast

  1468

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

  1470   by blast

  1471

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

  1473   by blast

  1474

  1475 lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"

  1476   by blast

  1477

  1478 lemma Diff_insert: "A - insert a B = A - B - {a}"

  1479   -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}

  1480   by blast

  1481

  1482 lemma Diff_insert2: "A - insert a B = A - {a} - B"

  1483   -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}

  1484   by blast

  1485

  1486 lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"

  1487   by auto

  1488

  1489 lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"

  1490   by blast

  1491

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

  1493 by blast

  1494

  1495 lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"

  1496   by blast

  1497

  1498 lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"

  1499   by auto

  1500

  1501 lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"

  1502   by blast

  1503

  1504 lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"

  1505   by blast

  1506

  1507 lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"

  1508   by blast

  1509

  1510 lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"

  1511   by blast

  1512

  1513 lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"

  1514   by blast

  1515

  1516 lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"

  1517   by blast

  1518

  1519 lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"

  1520   by blast

  1521

  1522 lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"

  1523   by blast

  1524

  1525 lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"

  1526   by blast

  1527

  1528 lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"

  1529   by blast

  1530

  1531 lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"

  1532   by blast

  1533

  1534 lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"

  1535   by auto

  1536

  1537 lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"

  1538   by blast

  1539

  1540

  1541 text {* \medskip Quantification over type @{typ bool}. *}

  1542

  1543 lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"

  1544   by (cases x) auto

  1545

  1546 lemma all_bool_eq: "(\<forall>b. P b) \<longleftrightarrow> P True \<and> P False"

  1547   by (auto intro: bool_induct)

  1548

  1549 lemma bool_contrapos: "P x \<Longrightarrow> \<not> P False \<Longrightarrow> P True"

  1550   by (cases x) auto

  1551

  1552 lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"

  1553   by (auto intro: bool_contrapos)

  1554

  1555 lemma UNIV_bool [no_atp]: "UNIV = {False, True}"

  1556   by (auto intro: bool_induct)

  1557

  1558 text {* \medskip @{text Pow} *}

  1559

  1560 lemma Pow_empty [simp]: "Pow {} = {{}}"

  1561   by (auto simp add: Pow_def)

  1562

  1563 lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a  Pow A)"

  1564   by (blast intro: image_eqI [where ?x = "u - {a}", standard])

  1565

  1566 lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"

  1567   by (blast intro: exI [where ?x = "- u", standard])

  1568

  1569 lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"

  1570   by blast

  1571

  1572 lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"

  1573   by blast

  1574

  1575 lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"

  1576   by blast

  1577

  1578

  1579 text {* \medskip Miscellany. *}

  1580

  1581 lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"

  1582   by blast

  1583

  1584 lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"

  1585   by blast

  1586

  1587 lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"

  1588   by (unfold less_le) blast

  1589

  1590 lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"

  1591   by blast

  1592

  1593 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"

  1594   by blast

  1595

  1596 lemma ball_simps [simp, no_atp]:

  1597   "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"

  1598   "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"

  1599   "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"

  1600   "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"

  1601   "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"

  1602   "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"

  1603   "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"

  1604   "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"

  1605   "\<And>A P f. (\<forall>x\<in>fA. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"

  1606   "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"

  1607   by auto

  1608

  1609 lemma bex_simps [simp, no_atp]:

  1610   "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"

  1611   "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"

  1612   "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"

  1613   "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"

  1614   "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"

  1615   "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"

  1616   "\<And>A P f. (\<exists>x\<in>fA. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"

  1617   "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"

  1618   by auto

  1619

  1620

  1621 subsubsection {* Monotonicity of various operations *}

  1622

  1623 lemma image_mono: "A \<subseteq> B ==> fA \<subseteq> fB"

  1624   by blast

  1625

  1626 lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"

  1627   by blast

  1628

  1629 lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"

  1630   by blast

  1631

  1632 lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"

  1633   by (fact sup_mono)

  1634

  1635 lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"

  1636   by (fact inf_mono)

  1637

  1638 lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"

  1639   by blast

  1640

  1641 lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"

  1642   by (fact compl_mono)

  1643

  1644 text {* \medskip Monotonicity of implications. *}

  1645

  1646 lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"

  1647   apply (rule impI)

  1648   apply (erule subsetD, assumption)

  1649   done

  1650

  1651 lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"

  1652   by iprover

  1653

  1654 lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"

  1655   by iprover

  1656

  1657 lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"

  1658   by iprover

  1659

  1660 lemma imp_refl: "P --> P" ..

  1661

  1662 lemma not_mono: "Q --> P ==> ~ P --> ~ Q"

  1663   by iprover

  1664

  1665 lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"

  1666   by iprover

  1667

  1668 lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"

  1669   by iprover

  1670

  1671 lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"

  1672   by blast

  1673

  1674 lemma Int_Collect_mono:

  1675     "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"

  1676   by blast

  1677

  1678 lemmas basic_monos =

  1679   subset_refl imp_refl disj_mono conj_mono

  1680   ex_mono Collect_mono in_mono

  1681

  1682 lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"

  1683   by iprover

  1684

  1685

  1686 subsubsection {* Inverse image of a function *}

  1687

  1688 definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-" 90) where

  1689   "f - B == {x. f x : B}"

  1690

  1691 lemma vimage_eq [simp]: "(a : f - B) = (f a : B)"

  1692   by (unfold vimage_def) blast

  1693

  1694 lemma vimage_singleton_eq: "(a : f - {b}) = (f a = b)"

  1695   by simp

  1696

  1697 lemma vimageI [intro]: "f a = b ==> b:B ==> a : f - B"

  1698   by (unfold vimage_def) blast

  1699

  1700 lemma vimageI2: "f a : A ==> a : f - A"

  1701   by (unfold vimage_def) fast

  1702

  1703 lemma vimageE [elim!]: "a: f - B ==> (!!x. f a = x ==> x:B ==> P) ==> P"

  1704   by (unfold vimage_def) blast

  1705

  1706 lemma vimageD: "a : f - A ==> f a : A"

  1707   by (unfold vimage_def) fast

  1708

  1709 lemma vimage_empty [simp]: "f - {} = {}"

  1710   by blast

  1711

  1712 lemma vimage_Compl: "f - (-A) = -(f - A)"

  1713   by blast

  1714

  1715 lemma vimage_Un [simp]: "f - (A Un B) = (f - A) Un (f - B)"

  1716   by blast

  1717

  1718 lemma vimage_Int [simp]: "f - (A Int B) = (f - A) Int (f - B)"

  1719   by fast

  1720

  1721 lemma vimage_Collect_eq [simp]: "f - Collect P = {y. P (f y)}"

  1722   by blast

  1723

  1724 lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f - (Collect P) = Collect Q"

  1725   by blast

  1726

  1727 lemma vimage_insert: "f-(insert a B) = (f-{a}) Un (f-B)"

  1728   -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}

  1729   by blast

  1730

  1731 lemma vimage_Diff: "f - (A - B) = (f - A) - (f - B)"

  1732   by blast

  1733

  1734 lemma vimage_UNIV [simp]: "f - UNIV = UNIV"

  1735   by blast

  1736

  1737 lemma vimage_mono: "A \<subseteq> B ==> f - A \<subseteq> f - B"

  1738   -- {* monotonicity *}

  1739   by blast

  1740

  1741 lemma vimage_image_eq [no_atp]: "f - (f  A) = {y. EX x:A. f x = f y}"

  1742 by (blast intro: sym)

  1743

  1744 lemma image_vimage_subset: "f  (f - A) <= A"

  1745 by blast

  1746

  1747 lemma image_vimage_eq [simp]: "f  (f - A) = A Int range f"

  1748 by blast

  1749

  1750 lemma vimage_const [simp]: "((\<lambda>x. c) - A) = (if c \<in> A then UNIV else {})"

  1751   by auto

  1752

  1753 lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) - A) =

  1754    (if c \<in> A then (if d \<in> A then UNIV else B)

  1755     else if d \<in> A then -B else {})"

  1756   by (auto simp add: vimage_def)

  1757

  1758 lemma vimage_inter_cong:

  1759   "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f - y \<inter> S = g - y \<inter> S"

  1760   by auto

  1761

  1762 lemma vimage_ident [simp]: "(%x. x) - Y = Y"

  1763   by blast

  1764

  1765

  1766 subsubsection {* Getting the Contents of a Singleton Set *}

  1767

  1768 definition the_elem :: "'a set \<Rightarrow> 'a" where

  1769   "the_elem X = (THE x. X = {x})"

  1770

  1771 lemma the_elem_eq [simp]: "the_elem {x} = x"

  1772   by (simp add: the_elem_def)

  1773

  1774

  1775 subsubsection {* Least value operator *}

  1776

  1777 lemma Least_mono:

  1778   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y

  1779     ==> (LEAST y. y : f  S) = f (LEAST x. x : S)"

  1780     -- {* Courtesy of Stephan Merz *}

  1781   apply clarify

  1782   apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)

  1783   apply (rule LeastI2_order)

  1784   apply (auto elim: monoD intro!: order_antisym)

  1785   done

  1786

  1787

  1788 subsubsection {* Monad operation *}

  1789

  1790 definition bind :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where

  1791   "bind A f = {x. \<exists>B \<in> fA. x \<in> B}"

  1792

  1793 hide_const (open) bind

  1794

  1795 lemma bind_bind:

  1796   fixes A :: "'a set"

  1797   shows "Set.bind (Set.bind A B) C = Set.bind A (\<lambda>x. Set.bind (B x) C)"

  1798   by (auto simp add: bind_def)

  1799

  1800 lemma empty_bind [simp]:

  1801   "Set.bind {} f = {}"

  1802   by (simp add: bind_def)

  1803

  1804 lemma nonempty_bind_const:

  1805   "A \<noteq> {} \<Longrightarrow> Set.bind A (\<lambda>_. B) = B"

  1806   by (auto simp add: bind_def)

  1807

  1808 lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"

  1809   by (auto simp add: bind_def)

  1810

  1811

  1812 subsubsection {* Operations for execution *}

  1813

  1814 definition is_empty :: "'a set \<Rightarrow> bool" where

  1815   [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"

  1816

  1817 hide_const (open) is_empty

  1818

  1819 definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where

  1820   [code_abbrev]: "remove x A = A - {x}"

  1821

  1822 hide_const (open) remove

  1823

  1824 lemma member_remove [simp]:

  1825   "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"

  1826   by (simp add: remove_def)

  1827

  1828 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where

  1829   [code_abbrev]: "filter P A = {a \<in> A. P a}"

  1830

  1831 hide_const (open) filter

  1832

  1833 lemma member_filter [simp]:

  1834   "x \<in> Set.filter P A \<longleftrightarrow> x \<in> A \<and> P x"

  1835   by (simp add: filter_def)

  1836

  1837 instantiation set :: (equal) equal

  1838 begin

  1839

  1840 definition

  1841   "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"

  1842

  1843 instance proof

  1844 qed (auto simp add: equal_set_def)

  1845

  1846 end

  1847

  1848

  1849 text {* Misc *}

  1850

  1851 hide_const (open) member not_member

  1852

  1853 lemmas equalityI = subset_antisym

  1854

  1855 ML {*

  1856 val Ball_def = @{thm Ball_def}

  1857 val Bex_def = @{thm Bex_def}

  1858 val CollectD = @{thm CollectD}

  1859 val CollectE = @{thm CollectE}

  1860 val CollectI = @{thm CollectI}

  1861 val Collect_conj_eq = @{thm Collect_conj_eq}

  1862 val Collect_mem_eq = @{thm Collect_mem_eq}

  1863 val IntD1 = @{thm IntD1}

  1864 val IntD2 = @{thm IntD2}

  1865 val IntE = @{thm IntE}

  1866 val IntI = @{thm IntI}

  1867 val Int_Collect = @{thm Int_Collect}

  1868 val UNIV_I = @{thm UNIV_I}

  1869 val UNIV_witness = @{thm UNIV_witness}

  1870 val UnE = @{thm UnE}

  1871 val UnI1 = @{thm UnI1}

  1872 val UnI2 = @{thm UnI2}

  1873 val ballE = @{thm ballE}

  1874 val ballI = @{thm ballI}

  1875 val bexCI = @{thm bexCI}

  1876 val bexE = @{thm bexE}

  1877 val bexI = @{thm bexI}

  1878 val bex_triv = @{thm bex_triv}

  1879 val bspec = @{thm bspec}

  1880 val contra_subsetD = @{thm contra_subsetD}

  1881 val equalityCE = @{thm equalityCE}

  1882 val equalityD1 = @{thm equalityD1}

  1883 val equalityD2 = @{thm equalityD2}

  1884 val equalityE = @{thm equalityE}

  1885 val equalityI = @{thm equalityI}

  1886 val imageE = @{thm imageE}

  1887 val imageI = @{thm imageI}

  1888 val image_Un = @{thm image_Un}

  1889 val image_insert = @{thm image_insert}

  1890 val insert_commute = @{thm insert_commute}

  1891 val insert_iff = @{thm insert_iff}

  1892 val mem_Collect_eq = @{thm mem_Collect_eq}

  1893 val rangeE = @{thm rangeE}

  1894 val rangeI = @{thm rangeI}

  1895 val range_eqI = @{thm range_eqI}

  1896 val subsetCE = @{thm subsetCE}

  1897 val subsetD = @{thm subsetD}

  1898 val subsetI = @{thm subsetI}

  1899 val subset_refl = @{thm subset_refl}

  1900 val subset_trans = @{thm subset_trans}

  1901 val vimageD = @{thm vimageD}

  1902 val vimageE = @{thm vimageE}

  1903 val vimageI = @{thm vimageI}

  1904 val vimageI2 = @{thm vimageI2}

  1905 val vimage_Collect = @{thm vimage_Collect}

  1906 val vimage_Int = @{thm vimage_Int}

  1907 val vimage_Un = @{thm vimage_Un}

  1908 *}

  1909

  1910 end

  1911