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