src/HOL/Set.thy
 author hoelzl Wed Jan 06 12:18:53 2016 +0100 (2016-01-06) changeset 62083 7582b39f51ed parent 61955 e96292f32c3c child 62087 44841d07ef1d permissions -rw-r--r--
add the proof of the central limit theorem
 haftmann@32139  1 (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel *)  clasohm@923  2 wenzelm@60758  3 section \Set theory for higher-order logic\  wenzelm@11979  4 nipkow@15131  5 theory Set  haftmann@30304  6 imports Lattices  nipkow@15131  7 begin  wenzelm@11979  8 wenzelm@60758  9 subsection \Sets as predicates\  haftmann@30531  10 haftmann@45959  11 typedecl 'a set  wenzelm@3820  12 wenzelm@61799  13 axiomatization Collect :: "('a \ bool) \ 'a set" \ "comprehension"  wenzelm@61799  14  and member :: "'a \ 'a set \ bool" \ "membership"  wenzelm@61955  15 where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"  haftmann@45959  16  and Collect_mem_eq [simp]: "Collect (\x. member x A) = A"  wenzelm@19656  17 wenzelm@21210  18 notation  wenzelm@61955  19  member ("op \") and  wenzelm@61955  20  member ("(_/ \ _)" [51, 51] 50)  wenzelm@61955  21 wenzelm@61955  22 abbreviation not_member  wenzelm@61955  23  where "not_member x A \ \ (x \ A)" \ "non-membership"  wenzelm@61955  24 notation  wenzelm@61955  25  not_member ("op \") and  wenzelm@61955  26  not_member ("(_/ \ _)" [51, 51] 50)  wenzelm@61955  27 wenzelm@61955  28 notation (ASCII)  haftmann@37677  29  member ("op :") and  wenzelm@61955  30  member ("(_/ : _)" [51, 51] 50) and  haftmann@37677  31  not_member ("op ~:") and  nipkow@50580  32  not_member ("(_/ ~: _)" [51, 51] 50)  wenzelm@19656  33 haftmann@41107  34 wenzelm@60758  35 text \Set comprehensions\  haftmann@32081  36 haftmann@30531  37 syntax  wenzelm@35115  38  "_Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")  haftmann@30531  39 translations  wenzelm@61955  40  "{x. P}" \ "CONST Collect (\x. P)"  wenzelm@61955  41 wenzelm@61955  42 syntax (ASCII)  wenzelm@61955  43  "_Collect" :: "pttrn \ 'a set \ bool \ 'a set" ("(1{_ :/ _./ _})")  haftmann@32081  44 syntax  wenzelm@61955  45  "_Collect" :: "pttrn \ 'a set \ bool \ 'a set" ("(1{_ \/ _./ _})")  haftmann@32081  46 translations  wenzelm@61955  47  "{p:A. P}" \ "CONST Collect (\p. p \ A \ P)"  haftmann@32081  48 haftmann@41107  49 lemma CollectI: "P a \ a \ {x. P x}"  haftmann@32081  50  by simp  haftmann@32081  51 haftmann@41107  52 lemma CollectD: "a \ {x. P x} \ P a"  haftmann@32081  53  by simp  haftmann@32081  54 haftmann@41107  55 lemma Collect_cong: "(\x. P x = Q x) ==> {x. P x} = {x. Q x}"  haftmann@32081  56  by simp  haftmann@32081  57 wenzelm@60758  58 text \  wenzelm@61799  59 Simproc for pulling \x=t\ in \{x. \ & x=t & \}\  wenzelm@61799  60 to the front (and similarly for \t=x\):  wenzelm@60758  61 \  wenzelm@60758  62 wenzelm@60758  63 simproc_setup defined_Collect ("{x. P x & Q x}") = \  wenzelm@54998  64  fn _ => Quantifier1.rearrange_Collect  wenzelm@59498  65  (fn ctxt =>  wenzelm@59498  66  resolve_tac ctxt @{thms Collect_cong} 1 THEN  wenzelm@59498  67  resolve_tac ctxt @{thms iffI} 1 THEN  wenzelm@42459  68  ALLGOALS  wenzelm@59498  69  (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},  wenzelm@59499  70  DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))  wenzelm@60758  71 \  haftmann@32117  72 haftmann@32081  73 lemmas CollectE = CollectD [elim_format]  haftmann@32081  74 haftmann@41107  75 lemma set_eqI:  haftmann@41107  76  assumes "\x. x \ A \ x \ B"  haftmann@41107  77  shows "A = B"  haftmann@41107  78 proof -  haftmann@41107  79  from assms have "{x. x \ A} = {x. x \ B}" by simp  haftmann@41107  80  then show ?thesis by simp  haftmann@41107  81 qed  haftmann@41107  82 blanchet@54147  83 lemma set_eq_iff:  haftmann@41107  84  "A = B \ (\x. x \ A \ x \ B)"  haftmann@41107  85  by (auto intro:set_eqI)  haftmann@41107  86 wenzelm@60758  87 text \Lifting of predicate class instances\  haftmann@45959  88 haftmann@45959  89 instantiation set :: (type) boolean_algebra  haftmann@45959  90 begin  haftmann@45959  91 haftmann@45959  92 definition less_eq_set where  haftmann@46853  93  "A \ B \ (\x. member x A) \ (\x. member x B)"  haftmann@45959  94 haftmann@45959  95 definition less_set where  haftmann@46853  96  "A < B \ (\x. member x A) < (\x. member x B)"  haftmann@45959  97 haftmann@45959  98 definition inf_set where  haftmann@46853  99  "A \ B = Collect ((\x. member x A) \ (\x. member x B))"  haftmann@45959  100 haftmann@45959  101 definition sup_set where  haftmann@46853  102  "A \ B = Collect ((\x. member x A) \ (\x. member x B))"  haftmann@45959  103 haftmann@45959  104 definition bot_set where  haftmann@46853  105  "\ = Collect \"  haftmann@45959  106 haftmann@45959  107 definition top_set where  haftmann@46853  108  "\ = Collect \"  haftmann@45959  109 haftmann@45959  110 definition uminus_set where  haftmann@46853  111  "- A = Collect (- (\x. member x A))"  haftmann@45959  112 haftmann@45959  113 definition minus_set where  haftmann@46853  114  "A - B = Collect ((\x. member x A) - (\x. member x B))"  haftmann@45959  115 haftmann@45959  116 instance proof  haftmann@45959  117 qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def  haftmann@45959  118  bot_set_def top_set_def uminus_set_def minus_set_def  haftmann@45959  119  less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq  noschinl@46882  120  set_eqI fun_eq_iff  noschinl@46882  121  del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)  haftmann@45959  122 haftmann@45959  123 end  haftmann@45959  124 wenzelm@60758  125 text \Set enumerations\  haftmann@30531  126 haftmann@32264  127 abbreviation empty :: "'a set" ("{}") where  haftmann@32264  128  "{} \ bot"  haftmann@31456  129 haftmann@31456  130 definition insert :: "'a \ 'a set \ 'a set" where  haftmann@32081  131  insert_compr: "insert a B = {x. x = a \ x \ B}"  haftmann@31456  132 haftmann@31456  133 syntax  wenzelm@35115  134  "_Finset" :: "args => 'a set" ("{(_)}")  haftmann@31456  135 translations  wenzelm@35115  136  "{x, xs}" == "CONST insert x {xs}"  wenzelm@35115  137  "{x}" == "CONST insert x {}"  haftmann@31456  138 haftmann@32081  139 wenzelm@60758  140 subsection \Subsets and bounded quantifiers\  haftmann@32081  141 wenzelm@61955  142 abbreviation subset :: "'a set \ 'a set \ bool"  wenzelm@61955  143  where "subset \ less"  wenzelm@61955  144 wenzelm@61955  145 abbreviation subset_eq :: "'a set \ 'a set \ bool"  wenzelm@61955  146  where "subset_eq \ less_eq"  wenzelm@61955  147 wenzelm@61955  148 notation  haftmann@32081  149  subset ("op \") and  nipkow@50580  150  subset ("(_/ \ _)" [51, 51] 50) and  haftmann@32081  151  subset_eq ("op \") and  nipkow@50580  152  subset_eq ("(_/ \ _)" [51, 51] 50)  haftmann@32081  153 haftmann@32081  154 abbreviation (input)  haftmann@32081  155  supset :: "'a set \ 'a set \ bool" where  haftmann@32081  156  "supset \ greater"  haftmann@32081  157 haftmann@32081  158 abbreviation (input)  haftmann@32081  159  supset_eq :: "'a set \ 'a set \ bool" where  haftmann@32081  160  "supset_eq \ greater_eq"  haftmann@32081  161 wenzelm@61955  162 notation  haftmann@32081  163  supset ("op \") and  nipkow@50580  164  supset ("(_/ \ _)" [51, 51] 50) and  haftmann@32081  165  supset_eq ("op \") and  nipkow@50580  166  supset_eq ("(_/ \ _)" [51, 51] 50)  haftmann@32081  167 wenzelm@61955  168 notation (ASCII output)  wenzelm@61955  169  subset ("op <") and  wenzelm@61955  170  subset ("(_/ < _)" [51, 51] 50) and  wenzelm@61955  171  subset_eq ("op <=") and  wenzelm@61955  172  subset_eq ("(_/ <= _)" [51, 51] 50)  wenzelm@61955  173 haftmann@37387  174 definition Ball :: "'a set \ ('a \ bool) \ bool" where  wenzelm@61799  175  "Ball A P \ (\x. x \ A \ P x)" \ "bounded universal quantifiers"  haftmann@32077  176 haftmann@37387  177 definition Bex :: "'a set \ ('a \ bool) \ bool" where  wenzelm@61799  178  "Bex A P \ (\x. x \ A \ P x)" \ "bounded existential quantifiers"  haftmann@32077  179 wenzelm@61955  180 syntax (ASCII)  haftmann@30531  181  "_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)  haftmann@30531  182  "_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)  haftmann@30531  183  "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3EX! _:_./ _)" [0, 0, 10] 10)  haftmann@30531  184  "_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST _:_./ _)" [0, 0, 10] 10)  haftmann@30531  185 haftmann@30531  186 syntax (HOL)  haftmann@30531  187  "_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10)  haftmann@30531  188  "_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10)  haftmann@30531  189  "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3?! _:_./ _)" [0, 0, 10] 10)  haftmann@30531  190 wenzelm@61955  191 syntax  haftmann@30531  192  "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@30531  193  "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@30531  194  "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\!_\_./ _)" [0, 0, 10] 10)  haftmann@30531  195  "_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\_./ _)" [0, 0, 10] 10)  haftmann@30531  196 haftmann@30531  197 translations  wenzelm@61955  198  "\x\A. P" \ "CONST Ball A (\x. P)"  wenzelm@61955  199  "\x\A. P" \ "CONST Bex A (\x. P)"  wenzelm@61955  200  "\!x\A. P" \ "\!x. x \ A \ P"  wenzelm@61955  201  "LEAST x:A. P" \ "LEAST x. x \ A \ P"  wenzelm@61955  202 wenzelm@61955  203 syntax (ASCII output)  nipkow@14804  204  "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)  nipkow@14804  205  "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)  nipkow@14804  206  "_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)  nipkow@14804  207  "_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)  webertj@20217  208  "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3EX! _<=_./ _)" [0, 0, 10] 10)  nipkow@14804  209 wenzelm@19656  210 syntax (HOL output)  nipkow@14804  211  "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)  nipkow@14804  212  "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)  nipkow@14804  213  "_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)  nipkow@14804  214  "_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)  webertj@20217  215  "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3?! _<=_./ _)" [0, 0, 10] 10)  nipkow@14804  216 wenzelm@61955  217 syntax  wenzelm@61955  218  "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  wenzelm@61955  219  "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  wenzelm@61955  220  "_setleAll" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  wenzelm@61955  221  "_setleEx" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  wenzelm@61955  222  "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\!_\_./ _)" [0, 0, 10] 10)  wenzelm@61955  223 nipkow@14804  224 translations  wenzelm@61955  225  "\A\B. P" \ "\A. A \ B \ P"  wenzelm@61955  226  "\A\B. P" \ "\A. A \ B \ P"  wenzelm@61955  227  "\A\B. P" \ "\A. A \ B \ P"  wenzelm@61955  228  "\A\B. P" \ "\A. A \ B \ P"  wenzelm@61955  229  "\!A\B. P" \ "\!A. A \ B \ P"  nipkow@14804  230 wenzelm@60758  231 print_translation \  wenzelm@52143  232  let  wenzelm@52143  233  val All_binder = Mixfix.binder_name @{const_syntax All};  wenzelm@52143  234  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};  wenzelm@52143  235  val impl = @{const_syntax HOL.implies};  wenzelm@52143  236  val conj = @{const_syntax HOL.conj};  wenzelm@52143  237  val sbset = @{const_syntax subset};  wenzelm@52143  238  val sbset_eq = @{const_syntax subset_eq};  wenzelm@52143  239 wenzelm@52143  240  val trans =  wenzelm@52143  241  [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),  wenzelm@52143  242  ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),  wenzelm@52143  243  ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),  wenzelm@52143  244  ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];  wenzelm@52143  245 wenzelm@52143  246  fun mk v (v', T) c n P =  wenzelm@52143  247  if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)  wenzelm@52143  248  then Syntax.const c $Syntax_Trans.mark_bound_body (v', T)$ n $P  wenzelm@52143  249  else raise Match;  wenzelm@52143  250 wenzelm@52143  251  fun tr' q = (q, fn _ =>  wenzelm@52143  252  (fn [Const (@{syntax_const "_bound"}, _)$ Free (v, Type (@{type_name set}, _)),  wenzelm@52143  253  Const (c, _) $ wenzelm@52143  254  (Const (d, _)$ (Const (@{syntax_const "_bound"}, _) $Free (v', T))$ n) $P] =>  wenzelm@52143  255  (case AList.lookup (op =) trans (q, c, d) of  wenzelm@52143  256  NONE => raise Match  wenzelm@52143  257  | SOME l => mk v (v', T) l n P)  wenzelm@52143  258  | _ => raise Match));  wenzelm@52143  259  in  wenzelm@52143  260  [tr' All_binder, tr' Ex_binder]  wenzelm@52143  261  end  wenzelm@60758  262 \  wenzelm@60758  263 wenzelm@60758  264 wenzelm@60758  265 text \  wenzelm@61799  266  \medskip Translate between \{e | x1...xn. P}\ and \{u. EX x1..xn. u = e & P}\; \{y. EX x1..xn. y = e & P}\ is  wenzelm@61799  267  only translated if \[0..n] subset bvs(e)\.  wenzelm@60758  268 \  wenzelm@11979  269 wenzelm@35115  270 syntax  wenzelm@35115  271  "_Setcompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")  wenzelm@35115  272 wenzelm@60758  273 parse_translation \  wenzelm@11979  274  let  wenzelm@42284  275  val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex}));  wenzelm@3947  276 wenzelm@35115  277  fun nvars (Const (@{syntax_const "_idts"}, _)$ _ $idts) = nvars idts + 1  wenzelm@11979  278  | nvars _ = 1;  wenzelm@11979  279 wenzelm@52143  280  fun setcompr_tr ctxt [e, idts, b] =  wenzelm@11979  281  let  haftmann@38864  282  val eq = Syntax.const @{const_syntax HOL.eq}$ Bound (nvars idts) $e;  haftmann@38795  283  val P = Syntax.const @{const_syntax HOL.conj}$ eq $b;  wenzelm@52143  284  val exP = ex_tr ctxt [idts, P];  wenzelm@44241  285  in Syntax.const @{const_syntax Collect}$ absdummy dummyT exP end;  wenzelm@11979  286 wenzelm@35115  287  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;  wenzelm@60758  288 \  wenzelm@60758  289 wenzelm@60758  290 print_translation \  wenzelm@42284  291  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},  wenzelm@42284  292  Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]  wenzelm@61799  293 \ \ \to avoid eta-contraction of body\  wenzelm@60758  294 wenzelm@60758  295 print_translation \  nipkow@13763  296 let  wenzelm@42284  297  val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));  nipkow@13763  298 wenzelm@52143  299  fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =  nipkow@13763  300  let  wenzelm@35115  301  fun check (Const (@{const_syntax Ex}, _) $Abs (_, _, P), n) = check (P, n + 1)  haftmann@38795  302  | check (Const (@{const_syntax HOL.conj}, _)$  haftmann@38864  303  (Const (@{const_syntax HOL.eq}, _) $Bound m$ e) $P, n) =  nipkow@13763  304  n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso  haftmann@33038  305  subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))  wenzelm@35115  306  | check _ = false;  clasohm@923  307 wenzelm@11979  308  fun tr' (_$ abs) =  wenzelm@52143  309  let val _ $idts$ (_ $(_$ _ $e)$ Q) = ex_tr' ctxt [abs]  wenzelm@35115  310  in Syntax.const @{syntax_const "_Setcompr"} $e$ idts $Q end;  wenzelm@35115  311  in  wenzelm@35115  312  if check (P, 0) then tr' P  wenzelm@35115  313  else  wenzelm@35115  314  let  wenzelm@42284  315  val (x as _$ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;  wenzelm@35115  316  val M = Syntax.const @{syntax_const "_Coll"} $x$ t;  wenzelm@35115  317  in  wenzelm@35115  318  case t of  haftmann@38795  319  Const (@{const_syntax HOL.conj}, _) $ haftmann@37677  320  (Const (@{const_syntax Set.member}, _)$  wenzelm@35115  321  (Const (@{syntax_const "_bound"}, _) $Free (yN, _))$ A) $P =>  wenzelm@35115  322  if xN = yN then Syntax.const @{syntax_const "_Collect"}$ x $A$ P else M  wenzelm@35115  323  | _ => M  wenzelm@35115  324  end  nipkow@13763  325  end;  wenzelm@35115  326  in [(@{const_syntax Collect}, setcompr_tr')] end;  wenzelm@60758  327 \  wenzelm@60758  328 wenzelm@60758  329 simproc_setup defined_Bex ("EX x:A. P x & Q x") = \  wenzelm@54998  330  fn _ => Quantifier1.rearrange_bex  wenzelm@54998  331  (fn ctxt =>  wenzelm@54998  332  unfold_tac ctxt @{thms Bex_def} THEN  wenzelm@59498  333  Quantifier1.prove_one_point_ex_tac ctxt)  wenzelm@60758  334 \  wenzelm@60758  335 wenzelm@60758  336 simproc_setup defined_All ("ALL x:A. P x --> Q x") = \  wenzelm@54998  337  fn _ => Quantifier1.rearrange_ball  wenzelm@54998  338  (fn ctxt =>  wenzelm@54998  339  unfold_tac ctxt @{thms Ball_def} THEN  wenzelm@59498  340  Quantifier1.prove_one_point_all_tac ctxt)  wenzelm@60758  341 \  haftmann@32117  342 wenzelm@11979  343 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"  wenzelm@11979  344  by (simp add: Ball_def)  wenzelm@11979  345 wenzelm@11979  346 lemmas strip = impI allI ballI  wenzelm@11979  347 wenzelm@11979  348 lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"  wenzelm@11979  349  by (simp add: Ball_def)  wenzelm@11979  350 wenzelm@60758  351 text \  wenzelm@11979  352  Gives better instantiation for bound:  wenzelm@60758  353 \  wenzelm@60758  354 wenzelm@60758  355 setup \  wenzelm@51717  356  map_theory_claset (fn ctxt =>  wenzelm@59498  357  ctxt addbefore ("bspec", fn ctxt' => dresolve_tac ctxt' @{thms bspec} THEN' assume_tac ctxt'))  wenzelm@60758  358 \  wenzelm@60758  359 wenzelm@60758  360 ML \  haftmann@32117  361 structure Simpdata =  haftmann@32117  362 struct  haftmann@32117  363 haftmann@32117  364 open Simpdata;  haftmann@32117  365 haftmann@32117  366 val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;  haftmann@32117  367 haftmann@32117  368 end;  haftmann@32117  369 haftmann@32117  370 open Simpdata;  wenzelm@60758  371 \  wenzelm@60758  372 wenzelm@60758  373 declaration \fn _ =>  wenzelm@45625  374  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))  wenzelm@60758  375 \  haftmann@32117  376 haftmann@32117  377 lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"  haftmann@32117  378  by (unfold Ball_def) blast  haftmann@32117  379 wenzelm@11979  380 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"  wenzelm@61799  381  \ \Normally the best argument order: @{prop "P x"} constrains the  wenzelm@60758  382  choice of @{prop "x:A"}.\  wenzelm@11979  383  by (unfold Bex_def) blast  wenzelm@11979  384 wenzelm@13113  385 lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x"  wenzelm@61799  386  \ \The best argument order when there is only one @{prop "x:A"}.\  wenzelm@11979  387  by (unfold Bex_def) blast  wenzelm@11979  388 wenzelm@11979  389 lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"  wenzelm@11979  390  by (unfold Bex_def) blast  wenzelm@11979  391 wenzelm@11979  392 lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q"  wenzelm@11979  393  by (unfold Bex_def) blast  wenzelm@11979  394 wenzelm@11979  395 lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"  wenzelm@61799  396  \ \Trival rewrite rule.\  wenzelm@11979  397  by (simp add: Ball_def)  wenzelm@11979  398 wenzelm@11979  399 lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"  wenzelm@61799  400  \ \Dual form for existentials.\  wenzelm@11979  401  by (simp add: Bex_def)  wenzelm@11979  402 wenzelm@11979  403 lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"  wenzelm@11979  404  by blast  wenzelm@11979  405 wenzelm@11979  406 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"  wenzelm@11979  407  by blast  wenzelm@11979  408 wenzelm@11979  409 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"  wenzelm@11979  410  by blast  wenzelm@11979  411 wenzelm@11979  412 lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)"  wenzelm@11979  413  by blast  wenzelm@11979  414 wenzelm@11979  415 lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)"  wenzelm@11979  416  by blast  wenzelm@11979  417 wenzelm@11979  418 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"  wenzelm@11979  419  by blast  wenzelm@11979  420 haftmann@43818  421 lemma ball_conj_distrib:  haftmann@43818  422  "(\x\A. P x \ Q x) \ ((\x\A. P x) \ (\x\A. Q x))"  haftmann@43818  423  by blast  haftmann@43818  424 haftmann@43818  425 lemma bex_disj_distrib:  haftmann@43818  426  "(\x\A. P x \ Q x) \ ((\x\A. P x) \ (\x\A. Q x))"  haftmann@43818  427  by blast  haftmann@43818  428 wenzelm@11979  429 wenzelm@60758  430 text \Congruence rules\  wenzelm@11979  431 berghofe@16636  432 lemma ball_cong:  wenzelm@11979  433  "A = B ==> (!!x. x:B ==> P x = Q x) ==>  wenzelm@11979  434  (ALL x:A. P x) = (ALL x:B. Q x)"  wenzelm@11979  435  by (simp add: Ball_def)  wenzelm@11979  436 berghofe@16636  437 lemma strong_ball_cong [cong]:  berghofe@16636  438  "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>  berghofe@16636  439  (ALL x:A. P x) = (ALL x:B. Q x)"  berghofe@16636  440  by (simp add: simp_implies_def Ball_def)  berghofe@16636  441 berghofe@16636  442 lemma bex_cong:  wenzelm@11979  443  "A = B ==> (!!x. x:B ==> P x = Q x) ==>  wenzelm@11979  444  (EX x:A. P x) = (EX x:B. Q x)"  wenzelm@11979  445  by (simp add: Bex_def cong: conj_cong)  regensbu@1273  446 berghofe@16636  447 lemma strong_bex_cong [cong]:  berghofe@16636  448  "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>  berghofe@16636  449  (EX x:A. P x) = (EX x:B. Q x)"  berghofe@16636  450  by (simp add: simp_implies_def Bex_def cong: conj_cong)  berghofe@16636  451 hoelzl@59000  452 lemma bex1_def: "(\!x\X. P x) \ (\x\X. P x) \ (\x\X. \y\X. P x \ P y \ x = y)"  hoelzl@59000  453  by auto  haftmann@30531  454 wenzelm@60758  455 subsection \Basic operations\  wenzelm@60758  456 wenzelm@60758  457 subsubsection \Subsets\  haftmann@30531  458 paulson@33022  459 lemma subsetI [intro!]: "(\x. x \ A \ x \ B) \ A \ B"  haftmann@45959  460  by (simp add: less_eq_set_def le_fun_def)  haftmann@30352  461 wenzelm@60758  462 text \  wenzelm@61799  463  \medskip Map the type \'a set => anything\ to just @{typ  haftmann@30531  464  'a}; for overloading constants whose first argument has type @{typ  haftmann@30531  465  "'a set"}.  wenzelm@60758  466 \  wenzelm@11979  467 haftmann@30596  468 lemma subsetD [elim, intro?]: "A \ B ==> c \ A ==> c \ B"  haftmann@45959  469  by (simp add: less_eq_set_def le_fun_def)  wenzelm@61799  470  \ \Rule in Modus Ponens style.\  haftmann@30531  471 blanchet@54147  472 lemma rev_subsetD [intro?]: "c \ A ==> A \ B ==> c \ B"  wenzelm@61799  473  \ \The same, with reversed premises for use with \erule\ --  wenzelm@61799  474  cf \rev_mp\.\  haftmann@30531  475  by (rule subsetD)  haftmann@30531  476 wenzelm@60758  477 text \  haftmann@30531  478  \medskip Converts @{prop "A \ B"} to @{prop "x \ A ==> x \ B"}.  wenzelm@60758  479 \  haftmann@30531  480 blanchet@54147  481 lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P"  wenzelm@61799  482  \ \Classical elimination rule.\  haftmann@45959  483  by (auto simp add: less_eq_set_def le_fun_def)  haftmann@30531  484 blanchet@54147  485 lemma subset_eq: "A \ B = (\x\A. x \ B)" by blast  blanchet@54147  486 blanchet@54147  487 lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A"  haftmann@30531  488  by blast  haftmann@30531  489 huffman@45121  490 lemma subset_refl: "A \ A"  huffman@45121  491  by (fact order_refl) (* already [iff] *)  haftmann@30531  492 haftmann@30531  493 lemma subset_trans: "A \ B ==> B \ C ==> A \ C"  haftmann@32081  494  by (fact order_trans)  haftmann@32081  495 haftmann@32081  496 lemma set_rev_mp: "x:A ==> A \ B ==> x:B"  haftmann@32081  497  by (rule subsetD)  haftmann@32081  498 haftmann@32081  499 lemma set_mp: "A \ B ==> x:A ==> x:B"  haftmann@32081  500  by (rule subsetD)  haftmann@32081  501 haftmann@46146  502 lemma subset_not_subset_eq [code]:  haftmann@46146  503  "A \ B \ A \ B \ \ B \ A"  haftmann@46146  504  by (fact less_le_not_le)  haftmann@46146  505 paulson@33044  506 lemma eq_mem_trans: "a=b ==> b \ A ==> a \ A"  paulson@33044  507  by simp  paulson@33044  508 haftmann@32081  509 lemmas basic_trans_rules [trans] =  paulson@33044  510  order_trans_rules set_rev_mp set_mp eq_mem_trans  haftmann@30531  511 haftmann@30531  512 wenzelm@60758  513 subsubsection \Equality\  haftmann@30531  514 haftmann@30531  515 lemma subset_antisym [intro!]: "A \ B ==> B \ A ==> A = B"  wenzelm@61799  516  \ \Anti-symmetry of the subset relation.\  nipkow@39302  517  by (iprover intro: set_eqI subsetD)  haftmann@30531  518 wenzelm@60758  519 text \  haftmann@30531  520  \medskip Equality rules from ZF set theory -- are they appropriate  haftmann@30531  521  here?  wenzelm@60758  522 \  haftmann@30531  523 haftmann@30531  524 lemma equalityD1: "A = B ==> A \ B"  krauss@34209  525  by simp  haftmann@30531  526 haftmann@30531  527 lemma equalityD2: "A = B ==> B \ A"  krauss@34209  528  by simp  haftmann@30531  529 wenzelm@60758  530 text \  wenzelm@61799  531  \medskip Be careful when adding this to the claset as \subset_empty\ is in the simpset: @{prop "A = {}"} goes to @{prop "{}  haftmann@30531  532  \ A"} and @{prop "A \ {}"} and then back to @{prop "A = {}"}!  wenzelm@60758  533 \  haftmann@30352  534 haftmann@30531  535 lemma equalityE: "A = B ==> (A \ B ==> B \ A ==> P) ==> P"  krauss@34209  536  by simp  haftmann@30531  537 haftmann@30531  538 lemma equalityCE [elim]:  haftmann@30531  539  "A = B ==> (c \ A ==> c \ B ==> P) ==> (c \ A ==> c \ B ==> P) ==> P"  haftmann@30531  540  by blast  haftmann@30531  541 haftmann@30531  542 lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"  haftmann@30531  543  by simp  haftmann@30531  544 haftmann@30531  545 lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"  haftmann@30531  546  by simp  haftmann@30531  547 haftmann@30531  548 wenzelm@60758  549 subsubsection \The empty set\  haftmann@41082  550 haftmann@41082  551 lemma empty_def:  haftmann@41082  552  "{} = {x. False}"  haftmann@45959  553  by (simp add: bot_set_def bot_fun_def)  haftmann@41082  554 haftmann@41082  555 lemma empty_iff [simp]: "(c : {}) = False"  haftmann@41082  556  by (simp add: empty_def)  haftmann@41082  557 haftmann@41082  558 lemma emptyE [elim!]: "a : {} ==> P"  haftmann@41082  559  by simp  haftmann@41082  560 haftmann@41082  561 lemma empty_subsetI [iff]: "{} \ A"  wenzelm@61799  562  \ \One effect is to delete the ASSUMPTION @{prop "{} <= A"}\  haftmann@41082  563  by blast  haftmann@41082  564 haftmann@41082  565 lemma equals0I: "(!!y. y \ A ==> False) ==> A = {}"  haftmann@41082  566  by blast  haftmann@41082  567 haftmann@41082  568 lemma equals0D: "A = {} ==> a \ A"  wenzelm@61799  569  \ \Use for reasoning about disjointness: \A Int B = {}\\  haftmann@41082  570  by blast  haftmann@41082  571 haftmann@41082  572 lemma ball_empty [simp]: "Ball {} P = True"  haftmann@41082  573  by (simp add: Ball_def)  haftmann@41082  574 haftmann@41082  575 lemma bex_empty [simp]: "Bex {} P = False"  haftmann@41082  576  by (simp add: Bex_def)  haftmann@41082  577 haftmann@41082  578 wenzelm@60758  579 subsubsection \The universal set -- UNIV\  haftmann@30531  580 haftmann@32264  581 abbreviation UNIV :: "'a set" where  haftmann@32264  582  "UNIV \ top"  haftmann@32135  583 haftmann@32135  584 lemma UNIV_def:  haftmann@32117  585  "UNIV = {x. True}"  haftmann@45959  586  by (simp add: top_set_def top_fun_def)  haftmann@32081  587 haftmann@30531  588 lemma UNIV_I [simp]: "x : UNIV"  haftmann@30531  589  by (simp add: UNIV_def)  haftmann@30531  590 wenzelm@61799  591 declare UNIV_I [intro] \ \unsafe makes it less likely to cause problems\  haftmann@30531  592 haftmann@30531  593 lemma UNIV_witness [intro?]: "EX x. x : UNIV"  haftmann@30531  594  by simp  haftmann@30531  595 huffman@45121  596 lemma subset_UNIV: "A \ UNIV"  huffman@45121  597  by (fact top_greatest) (* already simp *)  haftmann@30531  598 wenzelm@60758  599 text \  wenzelm@61799  600  \medskip Eta-contracting these two rules (to remove \P\)  haftmann@30531  601  causes them to be ignored because of their interaction with  haftmann@30531  602  congruence rules.  wenzelm@60758  603 \  haftmann@30531  604 haftmann@30531  605 lemma ball_UNIV [simp]: "Ball UNIV P = All P"  haftmann@30531  606  by (simp add: Ball_def)  haftmann@30531  607 haftmann@30531  608 lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"  haftmann@30531  609  by (simp add: Bex_def)  haftmann@30531  610 haftmann@30531  611 lemma UNIV_eq_I: "(\x. x \ A) \ UNIV = A"  haftmann@30531  612  by auto  haftmann@30531  613 haftmann@30531  614 lemma UNIV_not_empty [iff]: "UNIV ~= {}"  haftmann@30531  615  by (blast elim: equalityE)  haftmann@30531  616 nipkow@51334  617 lemma empty_not_UNIV[simp]: "{} \ UNIV"  nipkow@51334  618 by blast  nipkow@51334  619 wenzelm@60758  620 subsubsection \The Powerset operator -- Pow\  haftmann@30531  621 haftmann@32077  622 definition Pow :: "'a set => 'a set set" where  haftmann@32077  623  Pow_def: "Pow A = {B. B \ A}"  haftmann@32077  624 haftmann@30531  625 lemma Pow_iff [iff]: "(A \ Pow B) = (A \ B)"  haftmann@30531  626  by (simp add: Pow_def)  haftmann@30531  627 haftmann@30531  628 lemma PowI: "A \ B ==> A \ Pow B"  haftmann@30531  629  by (simp add: Pow_def)  haftmann@30531  630 haftmann@30531  631 lemma PowD: "A \ Pow B ==> A \ B"  haftmann@30531  632  by (simp add: Pow_def)  haftmann@30531  633 haftmann@30531  634 lemma Pow_bottom: "{} \ Pow B"  haftmann@30531  635  by simp  haftmann@30531  636 haftmann@30531  637 lemma Pow_top: "A \ Pow A"  krauss@34209  638  by simp  haftmann@30531  639 hoelzl@40703  640 lemma Pow_not_empty: "Pow A \ {}"  hoelzl@40703  641  using Pow_top by blast  haftmann@30531  642 haftmann@41076  643 wenzelm@60758  644 subsubsection \Set complement\  haftmann@30531  645 haftmann@30531  646 lemma Compl_iff [simp]: "(c \ -A) = (c \ A)"  haftmann@45959  647  by (simp add: fun_Compl_def uminus_set_def)  haftmann@30531  648 haftmann@30531  649 lemma ComplI [intro!]: "(c \ A ==> False) ==> c \ -A"  haftmann@45959  650  by (simp add: fun_Compl_def uminus_set_def) blast  clasohm@923  651 wenzelm@60758  652 text \  haftmann@30531  653  \medskip This form, with negated conclusion, works well with the  haftmann@30531  654  Classical prover. Negated assumptions behave like formulae on the  wenzelm@60758  655  right side of the notional turnstile ...\  haftmann@30531  656 haftmann@30531  657 lemma ComplD [dest!]: "c : -A ==> c~:A"  haftmann@45959  658  by simp  haftmann@30531  659 haftmann@30531  660 lemmas ComplE = ComplD [elim_format]  haftmann@30531  661 haftmann@45959  662 lemma Compl_eq: "- A = {x. ~ x : A}"  haftmann@45959  663  by blast  haftmann@30531  664 haftmann@30531  665 wenzelm@60758  666 subsubsection \Binary intersection\  haftmann@41082  667 wenzelm@61955  668 abbreviation inter :: "'a set \ 'a set \ 'a set" (infixl "\" 70)  wenzelm@61955  669  where "op \ \ inf"  wenzelm@61955  670 wenzelm@61955  671 notation (ASCII)  wenzelm@61955  672  inter (infixl "Int" 70)  haftmann@41082  673 haftmann@41082  674 lemma Int_def:  haftmann@41082  675  "A \ B = {x. x \ A \ x \ B}"  haftmann@45959  676  by (simp add: inf_set_def inf_fun_def)  haftmann@41082  677 haftmann@41082  678 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"  haftmann@41082  679  by (unfold Int_def) blast  haftmann@41082  680 haftmann@41082  681 lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"  haftmann@41082  682  by simp  haftmann@41082  683 haftmann@41082  684 lemma IntD1: "c : A Int B ==> c:A"  haftmann@41082  685  by simp  haftmann@41082  686 haftmann@41082  687 lemma IntD2: "c : A Int B ==> c:B"  haftmann@41082  688  by simp  haftmann@41082  689 haftmann@41082  690 lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"  haftmann@41082  691  by simp  haftmann@41082  692 haftmann@41082  693 lemma mono_Int: "mono f \ f (A \ B) \ f A \ f B"  haftmann@41082  694  by (fact mono_inf)  haftmann@41082  695 haftmann@41082  696 wenzelm@60758  697 subsubsection \Binary union\  haftmann@30531  698 wenzelm@61955  699 abbreviation union :: "'a set \ 'a set \ 'a set" (infixl "\" 65)  wenzelm@61955  700  where "union \ sup"  wenzelm@61955  701 wenzelm@61955  702 notation (ASCII)  wenzelm@61955  703  union (infixl "Un" 65)  haftmann@32081  704 haftmann@32135  705 lemma Un_def:  haftmann@32135  706  "A \ B = {x. x \ A \ x \ B}"  haftmann@45959  707  by (simp add: sup_set_def sup_fun_def)  haftmann@32081  708 haftmann@30531  709 lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"  haftmann@30531  710  by (unfold Un_def) blast  haftmann@30531  711 haftmann@30531  712 lemma UnI1 [elim?]: "c:A ==> c : A Un B"  haftmann@30531  713  by simp  haftmann@30531  714 haftmann@30531  715 lemma UnI2 [elim?]: "c:B ==> c : A Un B"  haftmann@30531  716  by simp  haftmann@30531  717 wenzelm@60758  718 text \  haftmann@30531  719  \medskip Classical introduction rule: no commitment to @{prop A} vs  haftmann@30531  720  @{prop B}.  wenzelm@60758  721 \  wenzelm@11979  722 haftmann@30531  723 lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"  haftmann@30531  724  by auto  haftmann@30531  725 haftmann@30531  726 lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"  haftmann@30531  727  by (unfold Un_def) blast  haftmann@30531  728 haftmann@32117  729 lemma insert_def: "insert a B = {x. x = a} \ B"  haftmann@45959  730  by (simp add: insert_compr Un_def)  haftmann@32081  731 haftmann@32081  732 lemma mono_Un: "mono f \ f A \ f B \ f (A \ B)"  haftmann@32683  733  by (fact mono_sup)  haftmann@32081  734 haftmann@30531  735 wenzelm@60758  736 subsubsection \Set difference\  haftmann@30531  737 haftmann@30531  738 lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"  haftmann@45959  739  by (simp add: minus_set_def fun_diff_def)  haftmann@30531  740 haftmann@30531  741 lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"  haftmann@30531  742  by simp  haftmann@30531  743 haftmann@30531  744 lemma DiffD1: "c : A - B ==> c : A"  haftmann@30531  745  by simp  haftmann@30531  746 haftmann@30531  747 lemma DiffD2: "c : A - B ==> c : B ==> P"  haftmann@30531  748  by simp  haftmann@30531  749 haftmann@30531  750 lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"  haftmann@30531  751  by simp  haftmann@30531  752 haftmann@30531  753 lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast  haftmann@30531  754 haftmann@30531  755 lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"  haftmann@30531  756 by blast  haftmann@30531  757 haftmann@30531  758 wenzelm@60758  759 subsubsection \Augmenting a set -- @{const insert}\  haftmann@30531  760 haftmann@30531  761 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"  haftmann@30531  762  by (unfold insert_def) blast  haftmann@30531  763 haftmann@30531  764 lemma insertI1: "a : insert a B"  haftmann@30531  765  by simp  haftmann@30531  766 haftmann@30531  767 lemma insertI2: "a : B ==> a : insert b B"  haftmann@30531  768  by simp  haftmann@30531  769 haftmann@30531  770 lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"  haftmann@30531  771  by (unfold insert_def) blast  haftmann@30531  772 haftmann@30531  773 lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"  wenzelm@61799  774  \ \Classical introduction rule.\  haftmann@30531  775  by auto  haftmann@30531  776 haftmann@30531  777 lemma subset_insert_iff: "(A \ insert x B) = (if x:A then A - {x} \ B else A \ B)"  haftmann@30531  778  by auto  haftmann@30531  779 haftmann@30531  780 lemma set_insert:  haftmann@30531  781  assumes "x \ A"  haftmann@30531  782  obtains B where "A = insert x B" and "x \ B"  haftmann@30531  783 proof  haftmann@30531  784  from assms show "A = insert x (A - {x})" by blast  haftmann@30531  785 next  haftmann@30531  786  show "x \ A - {x}" by blast  haftmann@30531  787 qed  haftmann@30531  788 haftmann@30531  789 lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"  haftmann@30531  790 by auto  haftmann@30531  791 nipkow@44744  792 lemma insert_eq_iff: assumes "a \ A" "b \ B"  nipkow@44744  793 shows "insert a A = insert b B \  nipkow@44744  794  (if a=b then A=B else \C. A = insert b C \ b \ C \ B = insert a C \ a \ C)"  nipkow@44744  795  (is "?L \ ?R")  nipkow@44744  796 proof  nipkow@44744  797  assume ?L  nipkow@44744  798  show ?R  nipkow@44744  799  proof cases  wenzelm@60758  800  assume "a=b" with assms \?L\ show ?R by (simp add: insert_ident)  nipkow@44744  801  next  nipkow@44744  802  assume "a\b"  nipkow@44744  803  let ?C = "A - {b}"  nipkow@44744  804  have "A = insert b ?C \ b \ ?C \ B = insert a ?C \ a \ ?C"  wenzelm@60758  805  using assms \?L\ \a\b\ by auto  wenzelm@60758  806  thus ?R using \a\b\ by auto  nipkow@44744  807  qed  nipkow@44744  808 next  haftmann@46128  809  assume ?R thus ?L by (auto split: if_splits)  nipkow@44744  810 qed  nipkow@44744  811 Andreas@60057  812 lemma insert_UNIV: "insert x UNIV = UNIV"  Andreas@60057  813 by auto  Andreas@60057  814 wenzelm@60758  815 subsubsection \Singletons, using insert\  haftmann@30531  816 blanchet@54147  817 lemma singletonI [intro!]: "a : {a}"  wenzelm@61799  818  \ \Redundant? But unlike \insertCI\, it proves the subgoal immediately!\  haftmann@30531  819  by (rule insertI1)  haftmann@30531  820 blanchet@54147  821 lemma singletonD [dest!]: "b : {a} ==> b = a"  haftmann@30531  822  by blast  haftmann@30531  823 haftmann@30531  824 lemmas singletonE = singletonD [elim_format]  haftmann@30531  825 haftmann@30531  826 lemma singleton_iff: "(b : {a}) = (b = a)"  haftmann@30531  827  by blast  haftmann@30531  828 haftmann@30531  829 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"  haftmann@30531  830  by blast  haftmann@30531  831 blanchet@54147  832 lemma singleton_insert_inj_eq [iff]:  haftmann@30531  833  "({b} = insert a A) = (a = b & A \ {b})"  haftmann@30531  834  by blast  haftmann@30531  835 blanchet@54147  836 lemma singleton_insert_inj_eq' [iff]:  haftmann@30531  837  "(insert a A = {b}) = (a = b & A \ {b})"  haftmann@30531  838  by blast  haftmann@30531  839 haftmann@30531  840 lemma subset_singletonD: "A \ {x} ==> A = {} | A = {x}"  haftmann@30531  841  by fast  haftmann@30531  842 haftmann@30531  843 lemma singleton_conv [simp]: "{x. x = a} = {a}"  haftmann@30531  844  by blast  haftmann@30531  845 haftmann@30531  846 lemma singleton_conv2 [simp]: "{x. a = x} = {a}"  haftmann@30531  847  by blast  haftmann@30531  848 bulwahn@46504  849 lemma diff_single_insert: "A - {x} \ B ==> A \ insert x B"  haftmann@30531  850  by blast  haftmann@30531  851 haftmann@30531  852 lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"  haftmann@30531  853  by (blast elim: equalityE)  haftmann@30531  854 nipkow@53364  855 lemma Un_singleton_iff:  nipkow@53364  856  "(A \ B = {x}) = (A = {} \ B = {x} \ A = {x} \ B = {} \ A = {x} \ B = {x})"  nipkow@53364  857 by auto  nipkow@53364  858 nipkow@53364  859 lemma singleton_Un_iff:  nipkow@53364  860  "({x} = A \ B) = (A = {} \ B = {x} \ A = {x} \ B = {} \ A = {x} \ B = {x})"  nipkow@53364  861 by auto  wenzelm@11979  862 haftmann@56014  863 wenzelm@60758  864 subsubsection \Image of a set under a function\  wenzelm@60758  865 wenzelm@60758  866 text \  haftmann@32077  867  Frequently @{term b} does not have the syntactic form of @{term "f x"}.  wenzelm@60758  868 \  haftmann@32077  869 haftmann@56014  870 definition image :: "('a \ 'b) \ 'a set \ 'b set" (infixr "" 90)  haftmann@56014  871 where  haftmann@56014  872  "f  A = {y. \x\A. y = f x}"  haftmann@56014  873 haftmann@56014  874 lemma image_eqI [simp, intro]:  haftmann@56014  875  "b = f x \ x \ A \ b \ f  A"  haftmann@32077  876  by (unfold image_def) blast  haftmann@32077  877 haftmann@56014  878 lemma imageI:  haftmann@56014  879  "x \ A \ f x \ f  A"  haftmann@32077  880  by (rule image_eqI) (rule refl)  haftmann@32077  881 haftmann@56014  882 lemma rev_image_eqI:  haftmann@56014  883  "x \ A \ b = f x \ b \ f  A"  wenzelm@61799  884  \ \This version's more effective when we already have the  wenzelm@60758  885  required @{term x}.\  haftmann@56014  886  by (rule image_eqI)  haftmann@32077  887 haftmann@32077  888 lemma imageE [elim!]:  wenzelm@61799  889  assumes "b \ (\x. f x)  A" \ \The eta-expansion gives variable-name preservation.\  haftmann@56014  890  obtains x where "b = f x" and "x \ A"  haftmann@56014  891  using assms by (unfold image_def) blast  haftmann@32077  892 haftmann@51173  893 lemma Compr_image_eq:  haftmann@51173  894  "{x \ f  A. P x} = f  {x \ A. P (f x)}"  haftmann@51173  895  by auto  haftmann@51173  896 haftmann@56014  897 lemma image_Un:  haftmann@56014  898  "f  (A \ B) = f  A \ f  B"  haftmann@32077  899  by blast  haftmann@32077  900 haftmann@56014  901 lemma image_iff:  haftmann@56014  902  "z \ f  A \ (\x\A. z = f x)"  haftmann@56014  903  by blast  haftmann@56014  904 haftmann@56014  905 lemma image_subsetI:  haftmann@56014  906  "(\x. x \ A \ f x \ B) \ f  A \ B"  wenzelm@61799  907  \ \Replaces the three steps \subsetI\, \imageE\,  wenzelm@61799  908  \hypsubst\, but breaks too many existing proofs.\  haftmann@32077  909  by blast  wenzelm@11979  910 haftmann@56014  911 lemma image_subset_iff:  haftmann@56014  912  "f  A \ B \ (\x\A. f x \ B)"  wenzelm@61799  913  \ \This rewrite rule would confuse users if made default.\  haftmann@56014  914  by blast  haftmann@56014  915 haftmann@56014  916 lemma subset_imageE:  haftmann@56014  917  assumes "B \ f  A"  haftmann@56014  918  obtains C where "C \ A" and "B = f  C"  haftmann@56014  919 proof -  haftmann@56014  920  from assms have "B = f  {a \ A. f a \ B}" by fast  haftmann@56014  921  moreover have "{a \ A. f a \ B} \ A" by blast  haftmann@56014  922  ultimately show thesis by (blast intro: that)  haftmann@56014  923 qed  haftmann@56014  924 haftmann@56014  925 lemma subset_image_iff:  haftmann@56014  926  "B \ f  A \ (\AA\A. B = f  AA)"  haftmann@56014  927  by (blast elim: subset_imageE)  haftmann@56014  928 haftmann@56014  929 lemma image_ident [simp]:  haftmann@56014  930  "(\x. x)  Y = Y"  haftmann@56014  931  by blast  haftmann@56014  932 haftmann@56014  933 lemma image_empty [simp]:  haftmann@56014  934  "f  {} = {}"  haftmann@56014  935  by blast  haftmann@56014  936 haftmann@56014  937 lemma image_insert [simp]:  haftmann@56014  938  "f  insert a B = insert (f a) (f  B)"  haftmann@56014  939  by blast  haftmann@56014  940 haftmann@56014  941 lemma image_constant:  haftmann@56014  942  "x \ A \ (\x. c)  A = {c}"  haftmann@56014  943  by auto  haftmann@56014  944 haftmann@56014  945 lemma image_constant_conv:  haftmann@56014  946  "(\x. c)  A = (if A = {} then {} else {c})"  haftmann@56014  947  by auto  haftmann@56014  948 haftmann@56014  949 lemma image_image:  haftmann@56014  950  "f  (g  A) = (\x. f (g x))  A"  haftmann@56014  951  by blast  haftmann@56014  952 haftmann@56014  953 lemma insert_image [simp]:  haftmann@56014  954  "x \ A ==> insert (f x) (f  A) = f  A"  haftmann@56014  955  by blast  haftmann@56014  956 haftmann@56014  957 lemma image_is_empty [iff]:  haftmann@56014  958  "f  A = {} \ A = {}"  haftmann@56014  959  by blast  haftmann@56014  960 haftmann@56014  961 lemma empty_is_image [iff]:  haftmann@56014  962  "{} = f  A \ A = {}"  haftmann@56014  963  by blast  haftmann@56014  964 haftmann@56014  965 lemma image_Collect:  haftmann@56014  966  "f  {x. P x} = {f x | x. P x}"  wenzelm@61799  967  \ \NOT suitable as a default simprule: the RHS isn't simpler than the LHS,  haftmann@56014  968  with its implicit quantifier and conjunction. Also image enjoys better  wenzelm@60758  969  equational properties than does the RHS.\  haftmann@56014  970  by blast  haftmann@56014  971 haftmann@56014  972 lemma if_image_distrib [simp]:  haftmann@56014  973  "(\x. if P x then f x else g x)  S  haftmann@56014  974  = (f  (S \ {x. P x})) \ (g  (S \ {x. \ P x}))"  haftmann@56077  975  by auto  haftmann@56014  976 haftmann@56014  977 lemma image_cong:  haftmann@56014  978  "M = N \ (\x. x \ N \ f x = g x) \ f  M = g  N"  haftmann@56014  979  by (simp add: image_def)  haftmann@56014  980 haftmann@56014  981 lemma image_Int_subset:  haftmann@56014  982  "f  (A \ B) \ f  A \ f  B"  haftmann@56014  983  by blast  haftmann@56014  984 haftmann@56014  985 lemma image_diff_subset:  haftmann@56014  986  "f  A - f  B \ f  (A - B)"  haftmann@56014  987  by blast  haftmann@56014  988 lp15@59504  989 lemma Setcompr_eq_image: "{f x | x. x \ A} = f  A"  lp15@59504  990  by blast  lp15@59504  991 hoelzl@62083  992 lemma setcompr_eq_image: "{f x |x. P x} = f  {x. P x}"  hoelzl@62083  993  by auto  hoelzl@62083  994 haftmann@56014  995 lemma ball_imageD:  haftmann@56014  996  assumes "\x\f  A. P x"  haftmann@56014  997  shows "\x\A. P (f x)"  haftmann@56014  998  using assms by simp  haftmann@56014  999 haftmann@56014  1000 lemma bex_imageD:  haftmann@56014  1001  assumes "\x\f  A. P x"  haftmann@56014  1002  shows "\x\A. P (f x)"  haftmann@56014  1003  using assms by auto  haftmann@56014  1004 haftmann@56014  1005 wenzelm@60758  1006 text \  haftmann@32077  1007  \medskip Range of a function -- just a translation for image!  wenzelm@60758  1008 \  haftmann@32077  1009 haftmann@56014  1010 abbreviation range :: "('a \ 'b) \ 'b set"  wenzelm@61799  1011 where \ "of function"  haftmann@56014  1012  "range f \ f  UNIV"  haftmann@56014  1013 haftmann@56014  1014 lemma range_eqI:  haftmann@56014  1015  "b = f x \ b \ range f"  haftmann@56014  1016  by simp  haftmann@56014  1017 haftmann@56014  1018 lemma rangeI:  haftmann@56014  1019  "f x \ range f"  haftmann@32077  1020  by simp  haftmann@32077  1021 haftmann@56014  1022 lemma rangeE [elim?]:  haftmann@56014  1023  "b \ range (\x. f x) \ (\x. b = f x \ P) \ P"  haftmann@56014  1024  by (rule imageE)  haftmann@56014  1025 haftmann@56014  1026 lemma full_SetCompr_eq:  haftmann@56014  1027  "{u. \x. u = f x} = range f"  haftmann@56014  1028  by auto  haftmann@56014  1029 lp15@59506  1030 lemma range_composition:  haftmann@56014  1031  "range (\x. f (g x)) = f  range g"  haftmann@56077  1032  by auto  haftmann@56014  1033 haftmann@32077  1034 wenzelm@61799  1035 subsubsection \Some rules with \if\\  wenzelm@61799  1036 wenzelm@61799  1037 text\Elimination of \{x. \ & x=t & \}\.\  haftmann@32081  1038 haftmann@32081  1039 lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"  haftmann@32117  1040  by auto  haftmann@32081  1041 haftmann@32081  1042 lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"  haftmann@32117  1043  by auto  haftmann@32081  1044 wenzelm@60758  1045 text \  wenzelm@61799  1046  Rewrite rules for boolean case-splitting: faster than \split_if [split]\.  wenzelm@60758  1047 \  haftmann@32081  1048 haftmann@32081  1049 lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"  haftmann@32081  1050  by (rule split_if)  haftmann@32081  1051 haftmann@32081  1052 lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"  haftmann@32081  1053  by (rule split_if)  haftmann@32081  1054 wenzelm@60758  1055 text \  wenzelm@61799  1056  Split ifs on either side of the membership relation. Not for \[simp]\ -- can cause goals to blow up!  wenzelm@60758  1057 \  haftmann@32081  1058 haftmann@32081  1059 lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"  haftmann@32081  1060  by (rule split_if)  haftmann@32081  1061 haftmann@32081  1062 lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"  haftmann@32081  1063  by (rule split_if [where P="%S. a : S"])  haftmann@32081  1064 haftmann@32081  1065 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2  haftmann@32081  1066 haftmann@32081  1067 (*Would like to add these, but the existing code only searches for the  haftmann@37677  1068  outer-level constant, which in this case is just Set.member; we instead need  haftmann@32081  1069  to use term-nets to associate patterns with rules. Also, if a rule fails to  haftmann@32081  1070  apply, then the formula should be kept.  haftmann@34974  1071  [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),  haftmann@32081  1072  ("Int", [IntD1,IntD2]),  haftmann@32081  1073  ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]  haftmann@32081  1074  *)  haftmann@32081  1075 haftmann@32081  1076 wenzelm@60758  1077 subsection \Further operations and lemmas\  wenzelm@60758  1078 wenzelm@60758  1079 subsubsection \The proper subset'' relation\  haftmann@32135  1080 blanchet@54147  1081 lemma psubsetI [intro!]: "A \ B ==> A \ B ==> A \ B"  haftmann@32135  1082  by (unfold less_le) blast  haftmann@32135  1083 blanchet@54147  1084 lemma psubsetE [elim!]:  haftmann@32135  1085  "[|A \ B; [|A \ B; ~ (B\A)|] ==> R|] ==> R"  haftmann@32135  1086  by (unfold less_le) blast  haftmann@32135  1087 haftmann@32135  1088 lemma psubset_insert_iff:  haftmann@32135  1089  "(A \ insert x B) = (if x \ B then A \ B else if x \ A then A - {x} \ B else A \ B)"  haftmann@32135  1090  by (auto simp add: less_le subset_insert_iff)  haftmann@32135  1091 haftmann@32135  1092 lemma psubset_eq: "(A \ B) = (A \ B & A \ B)"  haftmann@32135  1093  by (simp only: less_le)  haftmann@32135  1094 haftmann@32135  1095 lemma psubset_imp_subset: "A \ B ==> A \ B"  haftmann@32135  1096  by (simp add: psubset_eq)  haftmann@32135  1097 haftmann@32135  1098 lemma psubset_trans: "[| A \ B; B \ C |] ==> A \ C"  haftmann@32135  1099 apply (unfold less_le)  haftmann@32135  1100 apply (auto dest: subset_antisym)  haftmann@32135  1101 done  haftmann@32135  1102 haftmann@32135  1103 lemma psubsetD: "[| A \ B; c \ A |] ==> c \ B"  haftmann@32135  1104 apply (unfold less_le)  haftmann@32135  1105 apply (auto dest: subsetD)  haftmann@32135  1106 done  haftmann@32135  1107 haftmann@32135  1108 lemma psubset_subset_trans: "A \ B ==> B \ C ==> A \ C"  haftmann@32135  1109  by (auto simp add: psubset_eq)  haftmann@32135  1110 haftmann@32135  1111 lemma subset_psubset_trans: "A \ B ==> B \ C ==> A \ C"  haftmann@32135  1112  by (auto simp add: psubset_eq)  haftmann@32135  1113 haftmann@32135  1114 lemma psubset_imp_ex_mem: "A \ B ==> \b. b \ (B - A)"  haftmann@32135  1115  by (unfold less_le) blast  haftmann@32135  1116 haftmann@32135  1117 lemma atomize_ball:  haftmann@32135  1118  "(!!x. x \ A ==> P x) == Trueprop (\x\A. P x)"  haftmann@32135  1119  by (simp only: Ball_def atomize_all atomize_imp)  haftmann@32135  1120 haftmann@32135  1121 lemmas [symmetric, rulify] = atomize_ball  haftmann@32135  1122  and [symmetric, defn] = atomize_ball  haftmann@32135  1123 hoelzl@40703  1124 lemma image_Pow_mono:  haftmann@56014  1125  assumes "f  A \ B"  haftmann@56014  1126  shows "image f  Pow A \ Pow B"  haftmann@56014  1127  using assms by blast  hoelzl@40703  1128 hoelzl@40703  1129 lemma image_Pow_surj:  hoelzl@40703  1130  assumes "f  A = B"  haftmann@56014  1131  shows "image f  Pow A = Pow B"  haftmann@56014  1132  using assms by (blast elim: subset_imageE)  haftmann@56014  1133 hoelzl@40703  1134 wenzelm@60758  1135 subsubsection \Derived rules involving subsets.\  wenzelm@60758  1136 wenzelm@61799  1137 text \\insert\.\  haftmann@32135  1138 haftmann@32135  1139 lemma subset_insertI: "B \ insert a B"  haftmann@32135  1140  by (rule subsetI) (erule insertI2)  haftmann@32135  1141 haftmann@32135  1142 lemma subset_insertI2: "A \ B \ A \ insert b B"  haftmann@32135  1143  by blast  haftmann@32135  1144 haftmann@32135  1145 lemma subset_insert: "x \ A ==> (A \ insert x B) = (A \ B)"  haftmann@32135  1146  by blast  haftmann@32135  1147 haftmann@32135  1148 wenzelm@60758  1149 text \\medskip Finite Union -- the least upper bound of two sets.\  haftmann@32135  1150 haftmann@32135  1151 lemma Un_upper1: "A \ A \ B"  huffman@36009  1152  by (fact sup_ge1)  haftmann@32135  1153 haftmann@32135  1154 lemma Un_upper2: "B \ A \ B"  huffman@36009  1155  by (fact sup_ge2)  haftmann@32135  1156 haftmann@32135  1157 lemma Un_least: "A \ C ==> B \ C ==> A \ B \ C"  huffman@36009  1158  by (fact sup_least)  haftmann@32135  1159 haftmann@32135  1160 wenzelm@60758  1161 text \\medskip Finite Intersection -- the greatest lower bound of two sets.\  haftmann@32135  1162 haftmann@32135  1163 lemma Int_lower1: "A \ B \ A"  huffman@36009  1164  by (fact inf_le1)  haftmann@32135  1165 haftmann@32135  1166 lemma Int_lower2: "A \ B \ B"  huffman@36009  1167  by (fact inf_le2)  haftmann@32135  1168 haftmann@32135  1169 lemma Int_greatest: "C \ A ==> C \ B ==> C \ A \ B"  huffman@36009  1170  by (fact inf_greatest)  haftmann@32135  1171 haftmann@32135  1172 wenzelm@60758  1173 text \\medskip Set difference.\  haftmann@32135  1174 haftmann@32135  1175 lemma Diff_subset: "A - B \ A"  haftmann@32135  1176  by blast  haftmann@32135  1177 haftmann@32135  1178 lemma Diff_subset_conv: "(A - B \ C) = (A \ B \ C)"  haftmann@32135  1179 by blast  haftmann@32135  1180 haftmann@32135  1181 wenzelm@60758  1182 subsubsection \Equalities involving union, intersection, inclusion, etc.\  wenzelm@60758  1183 wenzelm@61799  1184 text \\{}\.\  haftmann@32135  1185 haftmann@32135  1186 lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"  wenzelm@61799  1187  \ \supersedes \Collect_False_empty\\  haftmann@32135  1188  by auto  haftmann@32135  1189 haftmann@32135  1190 lemma subset_empty [simp]: "(A \ {}) = (A = {})"  huffman@45121  1191  by (fact bot_unique)  haftmann@32135  1192 haftmann@32135  1193 lemma not_psubset_empty [iff]: "\ (A < {})"  huffman@45121  1194  by (fact not_less_bot) (* FIXME: already simp *)  haftmann@32135  1195 haftmann@32135  1196 lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\x. \ P x)"  haftmann@32135  1197 by blast  haftmann@32135  1198 haftmann@32135  1199 lemma empty_Collect_eq [simp]: "({} = Collect P) = (\x. \ P x)"  haftmann@32135  1200 by blast  haftmann@32135  1201 haftmann@32135  1202 lemma Collect_neg_eq: "{x. \ P x} = - {x. P x}"  haftmann@32135  1203  by blast  haftmann@32135  1204 haftmann@32135  1205 lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \ {x. Q x}"  haftmann@32135  1206  by blast  haftmann@32135  1207 haftmann@32135  1208 lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \ {x. Q x}"  haftmann@32135  1209  by blast  haftmann@32135  1210 haftmann@32135  1211 lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \ {x. Q x}"  haftmann@32135  1212  by blast  haftmann@32135  1213 lp15@59506  1214 lemma Collect_mono_iff: "Collect P \ Collect Q \ (\x. P x \ Q x)"  lp15@59504  1215  by blast  lp15@59504  1216 haftmann@32135  1217 wenzelm@61799  1218 text \\medskip \insert\.\  haftmann@32135  1219 haftmann@32135  1220 lemma insert_is_Un: "insert a A = {a} Un A"  wenzelm@61799  1221  \ \NOT SUITABLE FOR REWRITING since \{a} == insert a {}\\  haftmann@32135  1222  by blast  haftmann@32135  1223 haftmann@32135  1224 lemma insert_not_empty [simp]: "insert a A \ {}"  haftmann@32135  1225  by blast  haftmann@32135  1226 wenzelm@45607  1227 lemmas empty_not_insert = insert_not_empty [symmetric]  haftmann@32135  1228 declare empty_not_insert [simp]  haftmann@32135  1229 haftmann@32135  1230 lemma insert_absorb: "a \ A ==> insert a A = A"  wenzelm@61799  1231  \ \\[simp]\ causes recursive calls when there are nested inserts\  wenzelm@61799  1232  \ \with \emph{quadratic} running time\  haftmann@32135  1233  by blast  haftmann@32135  1234 haftmann@32135  1235 lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"  haftmann@32135  1236  by blast  haftmann@32135  1237 haftmann@32135  1238 lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"  haftmann@32135  1239  by blast  haftmann@32135  1240 haftmann@32135  1241 lemma insert_subset [simp]: "(insert x A \ B) = (x \ B & A \ B)"  haftmann@32135  1242  by blast  haftmann@32135  1243 haftmann@32135  1244 lemma mk_disjoint_insert: "a \ A ==> \B. A = insert a B & a \ B"  wenzelm@61799  1245  \ \use new \B\ rather than \A - {a}\ to avoid infinite unfolding\  haftmann@32135  1246  apply (rule_tac x = "A - {a}" in exI, blast)  haftmann@32135  1247  done  haftmann@32135  1248 haftmann@32135  1249 lemma insert_Collect: "insert a (Collect P) = {u. u \ a --> P u}"  haftmann@32135  1250  by auto  haftmann@32135  1251 haftmann@32135  1252 lemma insert_inter_insert[simp]: "insert a A \ insert a B = insert a (A \ B)"  haftmann@32135  1253  by blast  haftmann@32135  1254 blanchet@54147  1255 lemma insert_disjoint [simp]:  haftmann@32135  1256  "(insert a A \ B = {}) = (a \ B \ A \ B = {})"  haftmann@32135  1257  "({} = insert a A \ B) = (a \ B \ {} = A \ B)"  haftmann@32135  1258  by auto  haftmann@32135  1259 blanchet@54147  1260 lemma disjoint_insert [simp]:  haftmann@32135  1261  "(B \ insert a A = {}) = (a \ B \ B \ A = {})"  haftmann@32135  1262  "({} = A \ insert b B) = (b \ A \ {} = A \ B)"  haftmann@32135  1263  by auto  haftmann@32135  1264 haftmann@32135  1265 wenzelm@61799  1266 text \\medskip \Int\\  haftmann@32135  1267 huffman@45121  1268 lemma Int_absorb: "A \ A = A"  huffman@45121  1269  by (fact inf_idem) (* already simp *)  haftmann@32135  1270 haftmann@32135  1271 lemma Int_left_absorb: "A \ (A \ B) = A \ B"  huffman@36009  1272  by (fact inf_left_idem)  haftmann@32135  1273 haftmann@32135  1274 lemma Int_commute: "A \ B = B \ A"  huffman@36009  1275  by (fact inf_commute)  haftmann@32135  1276 haftmann@32135  1277 lemma Int_left_commute: "A \ (B \ C) = B \ (A \ C)"  huffman@36009  1278  by (fact inf_left_commute)  haftmann@32135  1279 haftmann@32135  1280 lemma Int_assoc: "(A \ B) \ C = A \ (B \ C)"  huffman@36009  1281  by (fact inf_assoc)  haftmann@32135  1282 haftmann@32135  1283 lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute  wenzelm@61799  1284  \ \Intersection is an AC-operator\  haftmann@32135  1285 haftmann@32135  1286 lemma Int_absorb1: "B \ A ==> A \ B = B"  huffman@36009  1287  by (fact inf_absorb2)  haftmann@32135  1288 haftmann@32135  1289 lemma Int_absorb2: "A \ B ==> A \ B = A"  huffman@36009  1290  by (fact inf_absorb1)  haftmann@32135  1291 huffman@45121  1292 lemma Int_empty_left: "{} \ B = {}"  huffman@45121  1293  by (fact inf_bot_left) (* already simp *)  haftmann@32135  1294 huffman@45121  1295 lemma Int_empty_right: "A \ {} = {}"  huffman@45121  1296  by (fact inf_bot_right) (* already simp *)  haftmann@32135  1297 haftmann@32135  1298 lemma disjoint_eq_subset_Compl: "(A \ B = {}) = (A \ -B)"  haftmann@32135  1299  by blast  haftmann@32135  1300 haftmann@32135  1301 lemma disjoint_iff_not_equal: "(A \ B = {}) = (\x\A. \y\B. x \ y)"  haftmann@32135  1302  by blast  haftmann@32135  1303 huffman@45121  1304 lemma Int_UNIV_left: "UNIV \ B = B"  huffman@45121  1305  by (fact inf_top_left) (* already simp *)  haftmann@32135  1306 huffman@45121  1307 lemma Int_UNIV_right: "A \ UNIV = A"  huffman@45121  1308  by (fact inf_top_right) (* already simp *)  haftmann@32135  1309 haftmann@32135  1310 lemma Int_Un_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)"  huffman@36009  1311  by (fact inf_sup_distrib1)  haftmann@32135  1312 haftmann@32135  1313 lemma Int_Un_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)"  huffman@36009  1314  by (fact inf_sup_distrib2)  haftmann@32135  1315 blanchet@54147  1316 lemma Int_UNIV [simp]: "(A \ B = UNIV) = (A = UNIV & B = UNIV)"  huffman@45121  1317  by (fact inf_eq_top_iff) (* already simp *)  haftmann@32135  1318 blanchet@54147  1319 lemma Int_subset_iff [simp]: "(C \ A \ B) = (C \ A & C \ B)"  huffman@36009  1320  by (fact le_inf_iff)  haftmann@32135  1321 haftmann@32135  1322 lemma Int_Collect: "(x \ A \ {x. P x}) = (x \ A & P x)"  haftmann@32135  1323  by blast  haftmann@32135  1324 haftmann@32135  1325 wenzelm@61799  1326 text \\medskip \Un\.\  haftmann@32135  1327 huffman@45121  1328 lemma Un_absorb: "A \ A = A"  huffman@45121  1329  by (fact sup_idem) (* already simp *)  haftmann@32135  1330 haftmann@32135  1331 lemma Un_left_absorb: "A \ (A \ B) = A \ B"  huffman@36009  1332  by (fact sup_left_idem)  haftmann@32135  1333 haftmann@32135  1334 lemma Un_commute: "A \ B = B \ A"  huffman@36009  1335  by (fact sup_commute)  haftmann@32135  1336 haftmann@32135  1337 lemma Un_left_commute: "A \ (B \ C) = B \ (A \ C)"  huffman@36009  1338  by (fact sup_left_commute)  haftmann@32135  1339 haftmann@32135  1340 lemma Un_assoc: "(A \ B) \ C = A \ (B \ C)"  huffman@36009  1341  by (fact sup_assoc)  haftmann@32135  1342 haftmann@32135  1343 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute  wenzelm@61799  1344  \ \Union is an AC-operator\  haftmann@32135  1345 haftmann@32135  1346 lemma Un_absorb1: "A \ B ==> A \ B = B"  huffman@36009  1347  by (fact sup_absorb2)  haftmann@32135  1348 haftmann@32135  1349 lemma Un_absorb2: "B \ A ==> A \ B = A"  huffman@36009  1350  by (fact sup_absorb1)  haftmann@32135  1351 huffman@45121  1352 lemma Un_empty_left: "{} \ B = B"  huffman@45121  1353  by (fact sup_bot_left) (* already simp *)  haftmann@32135  1354 huffman@45121  1355 lemma Un_empty_right: "A \ {} = A"  huffman@45121  1356  by (fact sup_bot_right) (* already simp *)  haftmann@32135  1357 huffman@45121  1358 lemma Un_UNIV_left: "UNIV \ B = UNIV"  huffman@45121  1359  by (fact sup_top_left) (* already simp *)  haftmann@32135  1360 huffman@45121  1361 lemma Un_UNIV_right: "A \ UNIV = UNIV"  huffman@45121  1362  by (fact sup_top_right) (* already simp *)  haftmann@32135  1363 haftmann@32135  1364 lemma Un_insert_left [simp]: "(insert a B) \ C = insert a (B \ C)"  haftmann@32135  1365  by blast  haftmann@32135  1366 haftmann@32135  1367 lemma Un_insert_right [simp]: "A \ (insert a B) = insert a (A \ B)"  haftmann@32135  1368  by blast  haftmann@32135  1369 haftmann@32135  1370 lemma Int_insert_left:  haftmann@32135  1371  "(insert a B) Int C = (if a \ C then insert a (B \ C) else B \ C)"  haftmann@32135  1372  by auto  haftmann@32135  1373 nipkow@32456  1374 lemma Int_insert_left_if0[simp]:  nipkow@32456  1375  "a \ C \ (insert a B) Int C = B \ C"  nipkow@32456  1376  by auto  nipkow@32456  1377 nipkow@32456  1378 lemma Int_insert_left_if1[simp]:  nipkow@32456  1379  "a \ C \ (insert a B) Int C = insert a (B Int C)"  nipkow@32456  1380  by auto  nipkow@32456  1381 haftmann@32135  1382 lemma Int_insert_right:  haftmann@32135  1383  "A \ (insert a B) = (if a \ A then insert a (A \ B) else A \ B)"  haftmann@32135  1384  by auto  haftmann@32135  1385 nipkow@32456  1386 lemma Int_insert_right_if0[simp]:  nipkow@32456  1387  "a \ A \ A Int (insert a B) = A Int B"  nipkow@32456  1388  by auto  nipkow@32456  1389 nipkow@32456  1390 lemma Int_insert_right_if1[simp]:  nipkow@32456  1391  "a \ A \ A Int (insert a B) = insert a (A Int B)"  nipkow@32456  1392  by auto  nipkow@32456  1393 haftmann@32135  1394 lemma Un_Int_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)"  huffman@36009  1395  by (fact sup_inf_distrib1)  haftmann@32135  1396 haftmann@32135  1397 lemma Un_Int_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)"  huffman@36009  1398  by (fact sup_inf_distrib2)  haftmann@32135  1399 haftmann@32135  1400 lemma Un_Int_crazy:  haftmann@32135  1401  "(A \ B) \ (B \ C) \ (C \ A) = (A \ B) \ (B \ C) \ (C \ A)"  haftmann@32135  1402  by blast  haftmann@32135  1403 haftmann@32135  1404 lemma subset_Un_eq: "(A \ B) = (A \ B = B)"  huffman@36009  1405  by (fact le_iff_sup)  haftmann@32135  1406 haftmann@32135  1407 lemma Un_empty [iff]: "(A \ B = {}) = (A = {} & B = {})"  huffman@45121  1408  by (fact sup_eq_bot_iff) (* FIXME: already simp *)  haftmann@32135  1409 blanchet@54147  1410 lemma Un_subset_iff [simp]: "(A \ B \ C) = (A \ C & B \ C)"  huffman@36009  1411  by (fact le_sup_iff)  haftmann@32135  1412 haftmann@32135  1413 lemma Un_Diff_Int: "(A - B) \ (A \ B) = A"  haftmann@32135  1414  by blast  haftmann@32135  1415 haftmann@32135  1416 lemma Diff_Int2: "A \ C - B \ C = A \ C - B"  haftmann@32135  1417  by blast  haftmann@32135  1418 haftmann@32135  1419 wenzelm@60758  1420 text \\medskip Set complement\  haftmann@32135  1421 haftmann@32135  1422 lemma Compl_disjoint [simp]: "A \ -A = {}"  huffman@36009  1423  by (fact inf_compl_bot)  haftmann@32135  1424 haftmann@32135  1425 lemma Compl_disjoint2 [simp]: "-A \ A = {}"  huffman@36009  1426  by (fact compl_inf_bot)  haftmann@32135  1427 haftmann@32135  1428 lemma Compl_partition: "A \ -A = UNIV"  huffman@36009  1429  by (fact sup_compl_top)  haftmann@32135  1430 haftmann@32135  1431 lemma Compl_partition2: "-A \ A = UNIV"  huffman@36009  1432  by (fact compl_sup_top)  haftmann@32135  1433 huffman@45121  1434 lemma double_complement: "- (-A) = (A::'a set)"  huffman@45121  1435  by (fact double_compl) (* already simp *)  haftmann@32135  1436 huffman@45121  1437 lemma Compl_Un: "-(A \ B) = (-A) \ (-B)"  huffman@45121  1438  by (fact compl_sup) (* already simp *)  haftmann@32135  1439 huffman@45121  1440 lemma Compl_Int: "-(A \ B) = (-A) \ (-B)"  huffman@45121  1441  by (fact compl_inf) (* already simp *)  haftmann@32135  1442 haftmann@32135  1443 lemma subset_Compl_self_eq: "(A \ -A) = (A = {})"  haftmann@32135  1444  by blast  haftmann@32135  1445 haftmann@32135  1446 lemma Un_Int_assoc_eq: "((A \ B) \ C = A \ (B \ C)) = (C \ A)"  wenzelm@61799  1447  \ \Halmos, Naive Set Theory, page 16.\  haftmann@32135  1448  by blast  haftmann@32135  1449 huffman@45121  1450 lemma Compl_UNIV_eq: "-UNIV = {}"  huffman@45121  1451  by (fact compl_top_eq) (* already simp *)  haftmann@32135  1452 huffman@45121  1453 lemma Compl_empty_eq: "-{} = UNIV"  huffman@45121  1454  by (fact compl_bot_eq) (* already simp *)  haftmann@32135  1455 haftmann@32135  1456 lemma Compl_subset_Compl_iff [iff]: "(-A \ -B) = (B \ A)"  huffman@45121  1457  by (fact compl_le_compl_iff) (* FIXME: already simp *)  haftmann@32135  1458 haftmann@32135  1459 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"  huffman@45121  1460  by (fact compl_eq_compl_iff) (* FIXME: already simp *)  haftmann@32135  1461 krauss@44490  1462 lemma Compl_insert: "- insert x A = (-A) - {x}"  krauss@44490  1463  by blast  krauss@44490  1464 wenzelm@60758  1465 text \\medskip Bounded quantifiers.  haftmann@32135  1466 haftmann@32135  1467  The following are not added to the default simpset because  wenzelm@61799  1468  (a) they duplicate the body and (b) there are no similar rules for \Int\.\  haftmann@32135  1469 haftmann@32135  1470 lemma ball_Un: "(\x \ A \ B. P x) = ((\x\A. P x) & (\x\B. P x))"  haftmann@32135  1471  by blast  haftmann@32135  1472 haftmann@32135  1473 lemma bex_Un: "(\x \ A \ B. P x) = ((\x\A. P x) | (\x\B. P x))"  haftmann@32135  1474  by blast  haftmann@32135  1475 haftmann@32135  1476 wenzelm@60758  1477 text \\medskip Set difference.\  haftmann@32135  1478 haftmann@32135  1479 lemma Diff_eq: "A - B = A \ (-B)"  haftmann@32135  1480  by blast  haftmann@32135  1481 blanchet@54147  1482 lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \ B)"  haftmann@32135  1483  by blast  haftmann@32135  1484 haftmann@32135  1485 lemma Diff_cancel [simp]: "A - A = {}"  haftmann@32135  1486  by blast  haftmann@32135  1487 haftmann@32135  1488 lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"  haftmann@32135  1489 by blast  haftmann@32135  1490 haftmann@32135  1491 lemma Diff_triv: "A \ B = {} ==> A - B = A"  haftmann@32135  1492  by (blast elim: equalityE)  haftmann@32135  1493 haftmann@32135  1494 lemma empty_Diff [simp]: "{} - A = {}"  haftmann@32135  1495  by blast  haftmann@32135  1496 haftmann@32135  1497 lemma Diff_empty [simp]: "A - {} = A"  haftmann@32135  1498  by blast  haftmann@32135  1499 haftmann@32135  1500 lemma Diff_UNIV [simp]: "A - UNIV = {}"  haftmann@32135  1501  by blast  haftmann@32135  1502 blanchet@54147  1503 lemma Diff_insert0 [simp]: "x \ A ==> A - insert x B = A - B"  haftmann@32135  1504  by blast  haftmann@32135  1505 haftmann@32135  1506 lemma Diff_insert: "A - insert a B = A - B - {a}"  wenzelm@61799  1507  \ \NOT SUITABLE FOR REWRITING since \{a} == insert a 0\\  haftmann@32135  1508  by blast  haftmann@32135  1509 haftmann@32135  1510 lemma Diff_insert2: "A - insert a B = A - {a} - B"  wenzelm@61799  1511  \ \NOT SUITABLE FOR REWRITING since \{a} == insert a 0\\  haftmann@32135  1512  by blast  haftmann@32135  1513 haftmann@32135  1514 lemma insert_Diff_if: "insert x A - B = (if x \ B then A - B else insert x (A - B))"  haftmann@32135  1515  by auto  haftmann@32135  1516 haftmann@32135  1517 lemma insert_Diff1 [simp]: "x \ B ==> insert x A - B = A - B"  haftmann@32135  1518  by blast  haftmann@32135  1519 haftmann@32135  1520 lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"  haftmann@32135  1521 by blast  haftmann@32135  1522 haftmann@32135  1523 lemma insert_Diff: "a \ A ==> insert a (A - {a}) = A"  haftmann@32135  1524  by blast  haftmann@32135  1525 haftmann@32135  1526 lemma Diff_insert_absorb: "x \ A ==> (insert x A) - {x} = A"  haftmann@32135  1527  by auto  haftmann@32135  1528 haftmann@32135  1529 lemma Diff_disjoint [simp]: "A \ (B - A) = {}"  haftmann@32135  1530  by blast  haftmann@32135  1531 haftmann@32135  1532 lemma Diff_partition: "A \ B ==> A \ (B - A) = B"  haftmann@32135  1533  by blast  haftmann@32135  1534 haftmann@32135  1535 lemma double_diff: "A \ B ==> B \ C ==> B - (C - A) = A"  haftmann@32135  1536  by blast  haftmann@32135  1537 haftmann@32135  1538 lemma Un_Diff_cancel [simp]: "A \ (B - A) = A \ B"  haftmann@32135  1539  by blast  haftmann@32135  1540 haftmann@32135  1541 lemma Un_Diff_cancel2 [simp]: "(B - A) \ A = B \ A"  haftmann@32135  1542  by blast  haftmann@32135  1543 haftmann@32135  1544 lemma Diff_Un: "A - (B \ C) = (A - B) \ (A - C)"  haftmann@32135  1545  by blast  haftmann@32135  1546 haftmann@32135  1547 lemma Diff_Int: "A - (B \ C) = (A - B) \ (A - C)"  haftmann@32135  1548  by blast  haftmann@32135  1549 paulson@61518  1550 lemma Diff_Diff_Int: "A - (A - B) = A \ B"  paulson@61518  1551  by blast  paulson@61518  1552 haftmann@32135  1553 lemma Un_Diff: "(A \ B) - C = (A - C) \ (B - C)"  haftmann@32135  1554  by blast  haftmann@32135  1555 haftmann@32135  1556 lemma Int_Diff: "(A \ B) - C = A \ (B - C)"  haftmann@32135  1557  by blast  haftmann@32135  1558 haftmann@32135  1559 lemma Diff_Int_distrib: "C \ (A - B) = (C \ A) - (C \ B)"  haftmann@32135  1560  by blast  haftmann@32135  1561 haftmann@32135  1562 lemma Diff_Int_distrib2: "(A - B) \ C = (A \ C) - (B \ C)"  haftmann@32135  1563  by blast  haftmann@32135  1564 haftmann@32135  1565 lemma Diff_Compl [simp]: "A - (- B) = A \ B"  haftmann@32135  1566  by auto  haftmann@32135  1567 haftmann@32135  1568 lemma Compl_Diff_eq [simp]: "- (A - B) = -A \ B"  haftmann@32135  1569  by blast  haftmann@32135  1570 haftmann@32135  1571 wenzelm@60758  1572 text \\medskip Quantification over type @{typ bool}.\  haftmann@32135  1573 haftmann@32135  1574 lemma bool_induct: "P True \ P False \ P x"  haftmann@32135  1575  by (cases x) auto  haftmann@32135  1576 haftmann@32135  1577 lemma all_bool_eq: "(\b. P b) \ P True \ P False"  haftmann@32135  1578  by (auto intro: bool_induct)  haftmann@32135  1579 haftmann@32135  1580 lemma bool_contrapos: "P x \ \ P False \ P True"  haftmann@32135  1581  by (cases x) auto  haftmann@32135  1582 haftmann@32135  1583 lemma ex_bool_eq: "(\b. P b) \ P True \ P False"  haftmann@32135  1584  by (auto intro: bool_contrapos)  haftmann@32135  1585 blanchet@54147  1586 lemma UNIV_bool: "UNIV = {False, True}"  haftmann@43866  1587  by (auto intro: bool_induct)  haftmann@43866  1588 wenzelm@61799  1589 text \\medskip \Pow\\  haftmann@32135  1590 haftmann@32135  1591 lemma Pow_empty [simp]: "Pow {} = {{}}"  haftmann@32135  1592  by (auto simp add: Pow_def)  haftmann@32135  1593 nipkow@60161  1594 lemma Pow_singleton_iff [simp]: "Pow X = {Y} \ X = {} \ Y = {}"  nipkow@60161  1595 by blast  nipkow@60161  1596 haftmann@32135  1597 lemma Pow_insert: "Pow (insert a A) = Pow A \ (insert a  Pow A)"  wenzelm@55143  1598  by (blast intro: image_eqI [where ?x = "u - {a}" for u])  haftmann@32135  1599 haftmann@32135  1600 lemma Pow_Compl: "Pow (- A) = {-B | B. A \ Pow B}"  wenzelm@55143  1601  by (blast intro: exI [where ?x = "- u" for u])  haftmann@32135  1602 haftmann@32135  1603 lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"  haftmann@32135  1604  by blast  haftmann@32135  1605 haftmann@32135  1606 lemma Un_Pow_subset: "Pow A \ Pow B \ Pow (A \ B)"  haftmann@32135  1607  by blast  haftmann@32135  1608 haftmann@32135  1609 lemma Pow_Int_eq [simp]: "Pow (A \ B) = Pow A \ Pow B"  haftmann@32135  1610  by blast  haftmann@32135  1611 haftmann@32135  1612 wenzelm@60758  1613 text \\medskip Miscellany.\  haftmann@32135  1614 haftmann@32135  1615 lemma set_eq_subset: "(A = B) = (A \ B & B \ A)"  haftmann@32135  1616  by blast  haftmann@32135  1617 blanchet@54147  1618 lemma subset_iff: "(A \ B) = (\t. t \ A --> t \ B)"  haftmann@32135  1619  by blast  haftmann@32135  1620 haftmann@32135  1621 lemma subset_iff_psubset_eq: "(A \ B) = ((A \ B) | (A = B))"  haftmann@32135  1622  by (unfold less_le) blast  haftmann@32135  1623 haftmann@32135  1624 lemma all_not_in_conv [simp]: "(\x. x \ A) = (A = {})"  haftmann@32135  1625  by blast  haftmann@32135  1626 haftmann@32135  1627 lemma ex_in_conv: "(\x. x \ A) = (A \ {})"  haftmann@32135  1628  by blast  haftmann@32135  1629 haftmann@43967  1630 lemma ball_simps [simp, no_atp]:  haftmann@43967  1631  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"  haftmann@43967  1632  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"  haftmann@43967  1633  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"  haftmann@43967  1634  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"  haftmann@43967  1635  "\P. (\x\{}. P x) \ True"  haftmann@43967  1636  "\P. (\x\UNIV. P x) \ (\x. P x)"  haftmann@43967  1637  "\a B P. (\x\insert a B. P x) \ (P a \ (\x\B. P x))"  haftmann@43967  1638  "\P Q. (\x\Collect Q. P x) \ (\x. Q x \ P x)"  haftmann@43967  1639  "\A P f. (\x\fA. P x) \ (\x\A. P (f x))"  haftmann@43967  1640  "\A P. (\ (\x\A. P x)) \ (\x\A. \ P x)"  haftmann@43967  1641  by auto  haftmann@43967  1642 haftmann@43967  1643 lemma bex_simps [simp, no_atp]:  haftmann@43967  1644  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"  haftmann@43967  1645  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"  haftmann@43967  1646  "\P. (\x\{}. P x) \ False"  haftmann@43967  1647  "\P. (\x\UNIV. P x) \ (\x. P x)"  haftmann@43967  1648  "\a B P. (\x\insert a B. P x) \ (P a | (\x\B. P x))"  haftmann@43967  1649  "\P Q. (\x\Collect Q. P x) \ (\x. Q x \ P x)"  haftmann@43967  1650  "\A P f. (\x\fA. P x) \ (\x\A. P (f x))"  haftmann@43967  1651  "\A P. (\(\x\A. P x)) \ (\x\A. \ P x)"  haftmann@43967  1652  by auto  haftmann@43967  1653 haftmann@32135  1654 wenzelm@60758  1655 subsubsection \Monotonicity of various operations\  haftmann@32135  1656 haftmann@32135  1657 lemma image_mono: "A \ B ==> fA \ fB"  haftmann@32135  1658  by blast  haftmann@32135  1659 haftmann@32135  1660 lemma Pow_mono: "A \ B ==> Pow A \ Pow B"  haftmann@32135  1661  by blast  haftmann@32135  1662 haftmann@32135  1663 lemma insert_mono: "C \ D ==> insert a C \ insert a D"  haftmann@32135  1664  by blast  haftmann@32135  1665 haftmann@32135  1666 lemma Un_mono: "A \ C ==> B \ D ==> A \ B \ C \ D"  huffman@36009  1667  by (fact sup_mono)  haftmann@32135  1668 haftmann@32135  1669 lemma Int_mono: "A \ C ==> B \ D ==> A \ B \ C \ D"  huffman@36009  1670  by (fact inf_mono)  haftmann@32135  1671 haftmann@32135  1672 lemma Diff_mono: "A \ C ==> D \ B ==> A - B \ C - D"  haftmann@32135  1673  by blast  haftmann@32135  1674 haftmann@32135  1675 lemma Compl_anti_mono: "A \ B ==> -B \ -A"  huffman@36009  1676  by (fact compl_mono)  haftmann@32135  1677 wenzelm@60758  1678 text \\medskip Monotonicity of implications.\  haftmann@32135  1679 haftmann@32135  1680 lemma in_mono: "A \ B ==> x \ A --> x \ B"  haftmann@32135  1681  apply (rule impI)  haftmann@32135  1682  apply (erule subsetD, assumption)  haftmann@32135  1683  done  haftmann@32135  1684 haftmann@32135  1685 lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"  haftmann@32135  1686  by iprover  haftmann@32135  1687 haftmann@32135  1688 lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"  haftmann@32135  1689  by iprover  haftmann@32135  1690 haftmann@32135  1691 lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"  haftmann@32135  1692  by iprover  haftmann@32135  1693 haftmann@32135  1694 lemma imp_refl: "P --> P" ..  haftmann@32135  1695 berghofe@33935  1696 lemma not_mono: "Q --> P ==> ~ P --> ~ Q"  berghofe@33935  1697  by iprover  berghofe@33935  1698 haftmann@32135  1699 lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"  haftmann@32135  1700  by iprover  haftmann@32135  1701 haftmann@32135  1702 lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"  haftmann@32135  1703  by iprover  haftmann@32135  1704 haftmann@32135  1705 lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \ Collect Q"  haftmann@32135  1706  by blast  haftmann@32135  1707 haftmann@32135  1708 lemma Int_Collect_mono:  haftmann@32135  1709  "A \ B ==> (!!x. x \ A ==> P x --> Q x) ==> A \ Collect P \ B \ Collect Q"  haftmann@32135  1710  by blast  haftmann@32135  1711 haftmann@32135  1712 lemmas basic_monos =  haftmann@32135  1713  subset_refl imp_refl disj_mono conj_mono  haftmann@32135  1714  ex_mono Collect_mono in_mono  haftmann@32135  1715 haftmann@32135  1716 lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"  haftmann@32135  1717  by iprover  haftmann@32135  1718 haftmann@32135  1719 wenzelm@60758  1720 subsubsection \Inverse image of a function\  haftmann@32135  1721 haftmann@35416  1722 definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-" 90) where  haftmann@37767  1723  "f - B == {x. f x : B}"  haftmann@32135  1724 haftmann@32135  1725 lemma vimage_eq [simp]: "(a : f - B) = (f a : B)"  haftmann@32135  1726  by (unfold vimage_def) blast  haftmann@32135  1727 haftmann@32135  1728 lemma vimage_singleton_eq: "(a : f - {b}) = (f a = b)"  haftmann@32135  1729  by simp  haftmann@32135  1730 haftmann@32135  1731 lemma vimageI [intro]: "f a = b ==> b:B ==> a : f - B"  haftmann@32135  1732  by (unfold vimage_def) blast  haftmann@32135  1733 haftmann@32135  1734 lemma vimageI2: "f a : A ==> a : f - A"  haftmann@32135  1735  by (unfold vimage_def) fast  haftmann@32135  1736 haftmann@32135  1737 lemma vimageE [elim!]: "a: f - B ==> (!!x. f a = x ==> x:B ==> P) ==> P"  haftmann@32135  1738  by (unfold vimage_def) blast  haftmann@32135  1739 haftmann@32135  1740 lemma vimageD: "a : f - A ==> f a : A"  haftmann@32135  1741  by (unfold vimage_def) fast  haftmann@32135  1742 haftmann@32135  1743 lemma vimage_empty [simp]: "f - {} = {}"  haftmann@32135  1744  by blast  haftmann@32135  1745 haftmann@32135  1746 lemma vimage_Compl: "f - (-A) = -(f - A)"  haftmann@32135  1747  by blast  haftmann@32135  1748 haftmann@32135  1749 lemma vimage_Un [simp]: "f - (A Un B) = (f - A) Un (f - B)"  haftmann@32135  1750  by blast  haftmann@32135  1751 haftmann@32135  1752 lemma vimage_Int [simp]: "f - (A Int B) = (f - A) Int (f - B)"  haftmann@32135  1753  by fast  haftmann@32135  1754 haftmann@32135  1755 lemma vimage_Collect_eq [simp]: "f - Collect P = {y. P (f y)}"  haftmann@32135  1756  by blast  haftmann@32135  1757 haftmann@32135  1758 lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f - (Collect P) = Collect Q"  haftmann@32135  1759  by blast  haftmann@32135  1760 haftmann@32135  1761 lemma vimage_insert: "f-(insert a B) = (f-{a}) Un (f-B)"  wenzelm@61799  1762  \ \NOT suitable for rewriting because of the recurrence of @{term "{a}"}.\  haftmann@32135  1763  by blast  haftmann@32135  1764 haftmann@32135  1765 lemma vimage_Diff: "f - (A - B) = (f - A) - (f - B)"  haftmann@32135  1766  by blast  haftmann@32135  1767 haftmann@32135  1768 lemma vimage_UNIV [simp]: "f - UNIV = UNIV"  haftmann@32135  1769  by blast  haftmann@32135  1770 haftmann@32135  1771 lemma vimage_mono: "A \ B ==> f - A \ f - B"  wenzelm@61799  1772  \ \monotonicity\  haftmann@32135  1773  by blast  haftmann@32135  1774 blanchet@54147  1775 lemma vimage_image_eq: "f - (f  A) = {y. EX x:A. f x = f y}"  haftmann@32135  1776 by (blast intro: sym)  haftmann@32135  1777 haftmann@32135  1778 lemma image_vimage_subset: "f  (f - A) <= A"  haftmann@32135  1779 by blast  haftmann@32135  1780 haftmann@32135  1781 lemma image_vimage_eq [simp]: "f  (f - A) = A Int range f"  haftmann@32135  1782 by blast  haftmann@32135  1783 lp15@55775  1784 lemma image_subset_iff_subset_vimage: "f  A \ B \ A \ f - B"  lp15@59506  1785  by blast  lp15@55775  1786 paulson@33533  1787 lemma vimage_const [simp]: "((\x. c) - A) = (if c \ A then UNIV else {})"  paulson@33533  1788  by auto  paulson@33533  1789 wenzelm@52143  1790 lemma vimage_if [simp]: "((\x. if x \ B then c else d) - A) =  paulson@33533  1791  (if c \ A then (if d \ A then UNIV else B)  wenzelm@52143  1792  else if d \ A then -B else {})"  wenzelm@52143  1793  by (auto simp add: vimage_def)  paulson@33533  1794 hoelzl@35576  1795 lemma vimage_inter_cong:  hoelzl@35576  1796  "(\ w. w \ S \ f w = g w) \ f - y \ S = g - y \ S"  hoelzl@35576  1797  by auto  hoelzl@35576  1798 haftmann@43898  1799 lemma vimage_ident [simp]: "(%x. x) - Y = Y"  haftmann@43898  1800  by blast  haftmann@32135  1801 haftmann@32135  1802 wenzelm@60758  1803 subsubsection \Getting the Contents of a Singleton Set\  haftmann@32135  1804 haftmann@39910  1805 definition the_elem :: "'a set \ 'a" where  haftmann@39910  1806  "the_elem X = (THE x. X = {x})"  haftmann@32135  1807 haftmann@39910  1808 lemma the_elem_eq [simp]: "the_elem {x} = x"  haftmann@39910  1809  by (simp add: the_elem_def)  haftmann@32135  1810 haftmann@56740  1811 lemma the_elem_image_unique:  haftmann@56740  1812  assumes "A \ {}"  haftmann@56740  1813  assumes *: "\y. y \ A \ f y = f x"  haftmann@56740  1814  shows "the_elem (f  A) = f x"  haftmann@56740  1815 unfolding the_elem_def proof (rule the1_equality)  wenzelm@60758  1816  from \A \ {}\ obtain y where "y \ A" by auto  haftmann@56740  1817  with * have "f x = f y" by simp  wenzelm@60758  1818  with \y \ A\ have "f x \ f  A" by blast  haftmann@56740  1819  with * show "f  A = {f x}" by auto  haftmann@56740  1820  then show "\!x. f  A = {x}" by auto  haftmann@56740  1821 qed  haftmann@56740  1822 haftmann@32135  1823 wenzelm@60758  1824 subsubsection \Least value operator\  haftmann@32135  1825 haftmann@32135  1826 lemma Least_mono:  haftmann@32135  1827  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y  haftmann@32135  1828  ==> (LEAST y. y : f  S) = f (LEAST x. x : S)"  wenzelm@61799  1829  \ \Courtesy of Stephan Merz\  haftmann@32135  1830  apply clarify  haftmann@32135  1831  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)  haftmann@32135  1832  apply (rule LeastI2_order)  haftmann@32135  1833  apply (auto elim: monoD intro!: order_antisym)  haftmann@32135  1834  done  haftmann@32135  1835 haftmann@32135  1836 wenzelm@60758  1837 subsubsection \Monad operation\  haftmann@32135  1838 haftmann@45959  1839 definition bind :: "'a set \ ('a \ 'b set) \ 'b set" where  haftmann@45959  1840  "bind A f = {x. \B \ fA. x \ B}"  haftmann@32135  1841 haftmann@45959  1842 hide_const (open) bind  haftmann@45959  1843 haftmann@46036  1844 lemma bind_bind:  haftmann@46036  1845  fixes A :: "'a set"  haftmann@46036  1846  shows "Set.bind (Set.bind A B) C = Set.bind A (\x. Set.bind (B x) C)"  haftmann@46036  1847  by (auto simp add: bind_def)  haftmann@46036  1848 haftmann@46036  1849 lemma empty_bind [simp]:  haftmann@46128  1850  "Set.bind {} f = {}"  haftmann@46036  1851  by (simp add: bind_def)  haftmann@46036  1852 haftmann@46036  1853 lemma nonempty_bind_const:  haftmann@46036  1854  "A \ {} \ Set.bind A (\_. B) = B"  haftmann@46036  1855  by (auto simp add: bind_def)  haftmann@46036  1856 haftmann@46036  1857 lemma bind_const: "Set.bind A (\_. B) = (if A = {} then {} else B)"  haftmann@46036  1858  by (auto simp add: bind_def)  haftmann@46036  1859 Andreas@60057  1860 lemma bind_singleton_conv_image: "Set.bind A (\x. {f x}) = f  A"  Andreas@60057  1861  by(auto simp add: bind_def)  haftmann@45959  1862 wenzelm@60758  1863 subsubsection \Operations for execution\  haftmann@45986  1864 haftmann@45986  1865 definition is_empty :: "'a set \ bool" where  haftmann@46127  1866  [code_abbrev]: "is_empty A \ A = {}"  haftmann@45986  1867 haftmann@45986  1868 hide_const (open) is_empty  haftmann@45986  1869 haftmann@45986  1870 definition remove :: "'a \ 'a set \ 'a set" where  haftmann@46127  1871  [code_abbrev]: "remove x A = A - {x}"  haftmann@45986  1872 haftmann@45986  1873 hide_const (open) remove  haftmann@45986  1874 haftmann@46128  1875 lemma member_remove [simp]:  haftmann@46128  1876  "x \ Set.remove y A \ x \ A \ x \ y"  haftmann@46128  1877  by (simp add: remove_def)  haftmann@46128  1878 kuncar@49757  1879 definition filter :: "('a \ bool) \ 'a set \ 'a set" where  kuncar@49757  1880  [code_abbrev]: "filter P A = {a \ A. P a}"  kuncar@49757  1881 kuncar@49757  1882 hide_const (open) filter  kuncar@49757  1883 kuncar@49757  1884 lemma member_filter [simp]:  kuncar@49757  1885  "x \ Set.filter P A \ x \ A \ P x"  kuncar@49757  1886  by (simp add: filter_def)  haftmann@46128  1887 haftmann@45986  1888 instantiation set :: (equal) equal  haftmann@45986  1889 begin  haftmann@45986  1890 haftmann@45986  1891 definition  haftmann@45986  1892  "HOL.equal A B \ A \ B \ B \ A"  haftmann@45986  1893 haftmann@45986  1894 instance proof  haftmann@45986  1895 qed (auto simp add: equal_set_def)  haftmann@45986  1896 haftmann@45986  1897 end  haftmann@45986  1898 haftmann@46127  1899 wenzelm@60758  1900 text \Misc\  haftmann@32135  1901 lp15@61306  1902 definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)"  lp15@61306  1903 haftmann@45152  1904 hide_const (open) member not_member  haftmann@32135  1905 haftmann@32135  1906 lemmas equalityI = subset_antisym  haftmann@32135  1907 wenzelm@60758  1908 ML \  haftmann@32135  1909 val Ball_def = @{thm Ball_def}  haftmann@32135  1910 val Bex_def = @{thm Bex_def}  haftmann@32135  1911 val CollectD = @{thm CollectD}  haftmann@32135  1912 val CollectE = @{thm CollectE}  haftmann@32135  1913 val CollectI = @{thm CollectI}  haftmann@32135  1914 val Collect_conj_eq = @{thm Collect_conj_eq}  haftmann@32135  1915 val Collect_mem_eq = @{thm Collect_mem_eq}  haftmann@32135  1916 val IntD1 = @{thm IntD1}  haftmann@32135  1917 val IntD2 = @{thm IntD2}  haftmann@32135  1918 val IntE = @{thm IntE}  haftmann@32135  1919 val IntI = @{thm IntI}  haftmann@32135  1920 val Int_Collect = @{thm Int_Collect}  haftmann@32135  1921 val UNIV_I = @{thm UNIV_I}  haftmann@32135  1922 val UNIV_witness = @{thm UNIV_witness}  haftmann@32135  1923 val UnE = @{thm UnE}  haftmann@32135  1924 val UnI1 = @{thm UnI1}  haftmann@32135  1925 val UnI2 = @{thm UnI2}  haftmann@32135  1926 val ballE = @{thm ballE}  haftmann@32135  1927 val ballI = @{thm ballI}  haftmann@32135  1928 val bexCI = @{thm bexCI}  haftmann@32135  1929 val bexE = @{thm bexE}  haftmann@32135  1930 val bexI = @{thm bexI}  haftmann@32135  1931 val bex_triv = @{thm bex_triv}  haftmann@32135  1932 val bspec = @{thm bspec}  haftmann@32135  1933 val contra_subsetD = @{thm contra_subsetD}  haftmann@32135  1934 val equalityCE = @{thm equalityCE}  haftmann@32135  1935 val equalityD1 = @{thm equalityD1}  haftmann@32135  1936 val equalityD2 = @{thm equalityD2}  haftmann@32135  1937 val equalityE = @{thm equalityE}  haftmann@32135  1938 val equalityI = @{thm equalityI}  haftmann@32135  1939 val imageE = @{thm imageE}  haftmann@32135  1940 val imageI = @{thm imageI}  haftmann@32135  1941 val image_Un = @{thm image_Un}  haftmann@32135  1942 val image_insert = @{thm image_insert}  haftmann@32135  1943 val insert_commute = @{thm insert_commute}  haftmann@32135  1944 val insert_iff = @{thm insert_iff}  haftmann@32135  1945 val mem_Collect_eq = @{thm mem_Collect_eq}  haftmann@32135  1946 val rangeE = @{thm rangeE}  haftmann@32135  1947 val rangeI = @{thm rangeI}  haftmann@32135  1948 val range_eqI = @{thm range_eqI}  haftmann@32135  1949 val subsetCE = @{thm subsetCE}  haftmann@32135  1950 val subsetD = @{thm subsetD}  haftmann@32135  1951 val subsetI = @{thm subsetI}  haftmann@32135  1952 val subset_refl = @{thm subset_refl}  haftmann@32135  1953 val subset_trans = @{thm subset_trans}  haftmann@32135  1954 val vimageD = @{thm vimageD}  haftmann@32135  1955 val vimageE = @{thm vimageE}  haftmann@32135  1956 val vimageI = @{thm vimageI}  haftmann@32135  1957 val vimageI2 = @{thm vimageI2}  haftmann@32135  1958 val vimage_Collect = @{thm vimage_Collect}  haftmann@32135  1959 val vimage_Int = @{thm vimage_Int}  haftmann@32135  1960 val vimage_Un = @{thm vimage_Un}  wenzelm@60758  1961 \  haftmann@32135  1962 haftmann@32077  1963 end  haftmann@46853  1964`