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