src/HOL/Set.thy
 author mehta Thu May 13 16:02:29 2004 +0200 (2004-05-13) changeset 14742 dde816115d6a parent 14692 b8d6c395c9e2 child 14752 3fc3c7b7e99d permissions -rw-r--r--
 clasohm@923  1 (* Title: HOL/Set.thy  clasohm@923  2  ID: $Id$  wenzelm@12257  3  Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel  wenzelm@12020  4  License: GPL (GNU GENERAL PUBLIC LICENSE)  clasohm@923  5 *)  clasohm@923  6 wenzelm@11979  7 header {* Set theory for higher-order logic *}  wenzelm@11979  8 wenzelm@12897  9 theory Set = HOL:  wenzelm@11979  10 wenzelm@11979  11 text {* A set in HOL is simply a predicate. *}  clasohm@923  12 wenzelm@2261  13 wenzelm@11979  14 subsection {* Basic syntax *}  wenzelm@2261  15 wenzelm@3947  16 global  wenzelm@3947  17 wenzelm@11979  18 typedecl 'a set  wenzelm@12338  19 arities set :: (type) type  wenzelm@3820  20 clasohm@923  21 consts  wenzelm@11979  22  "{}" :: "'a set" ("{}")  wenzelm@11979  23  UNIV :: "'a set"  wenzelm@11979  24  insert :: "'a => 'a set => 'a set"  wenzelm@11979  25  Collect :: "('a => bool) => 'a set" -- "comprehension"  wenzelm@11979  26  Int :: "'a set => 'a set => 'a set" (infixl 70)  wenzelm@11979  27  Un :: "'a set => 'a set => 'a set" (infixl 65)  wenzelm@11979  28  UNION :: "'a set => ('a => 'b set) => 'b set" -- "general union"  wenzelm@11979  29  INTER :: "'a set => ('a => 'b set) => 'b set" -- "general intersection"  wenzelm@11979  30  Union :: "'a set set => 'a set" -- "union of a set"  wenzelm@11979  31  Inter :: "'a set set => 'a set" -- "intersection of a set"  wenzelm@11979  32  Pow :: "'a set => 'a set set" -- "powerset"  wenzelm@11979  33  Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"  wenzelm@11979  34  Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"  wenzelm@11979  35  image :: "('a => 'b) => 'a set => 'b set" (infixr "" 90)  wenzelm@11979  36 wenzelm@11979  37 syntax  wenzelm@11979  38  "op :" :: "'a => 'a set => bool" ("op :")  wenzelm@11979  39 consts  wenzelm@11979  40  "op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50) -- "membership"  wenzelm@11979  41 wenzelm@11979  42 local  wenzelm@11979  43 wenzelm@14692  44 instance set :: (type) "{ord, minus}" ..  clasohm@923  45 clasohm@923  46 wenzelm@11979  47 subsection {* Additional concrete syntax *}  wenzelm@2261  48 clasohm@923  49 syntax  wenzelm@11979  50  range :: "('a => 'b) => 'b set" -- "of function"  clasohm@923  51 wenzelm@11979  52  "op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership"  wenzelm@11979  53  "op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50)  wenzelm@7238  54 wenzelm@11979  55  "@Finset" :: "args => 'a set" ("{(_)}")  wenzelm@11979  56  "@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")  wenzelm@11979  57  "@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")  clasohm@923  58 wenzelm@11979  59  "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10)  wenzelm@11979  60  "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10)  wenzelm@11979  61  "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10)  wenzelm@11979  62  "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10)  clasohm@923  63 wenzelm@11979  64  "_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)  wenzelm@11979  65  "_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)  clasohm@923  66 wenzelm@7238  67 syntax (HOL)  wenzelm@11979  68  "_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10)  wenzelm@11979  69  "_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10)  clasohm@923  70 clasohm@923  71 translations  nipkow@10832  72  "range f" == "fUNIV"  clasohm@923  73  "x ~: y" == "~ (x : y)"  clasohm@923  74  "{x, xs}" == "insert x {xs}"  clasohm@923  75  "{x}" == "insert x {}"  nipkow@13764  76  "{x. P}" == "Collect (%x. P)"  paulson@4159  77  "UN x y. B" == "UN x. UN y. B"  paulson@4159  78  "UN x. B" == "UNION UNIV (%x. B)"  nipkow@13858  79  "UN x. B" == "UN x:UNIV. B"  wenzelm@7238  80  "INT x y. B" == "INT x. INT y. B"  paulson@4159  81  "INT x. B" == "INTER UNIV (%x. B)"  nipkow@13858  82  "INT x. B" == "INT x:UNIV. B"  nipkow@13764  83  "UN x:A. B" == "UNION A (%x. B)"  nipkow@13764  84  "INT x:A. B" == "INTER A (%x. B)"  nipkow@13764  85  "ALL x:A. P" == "Ball A (%x. P)"  nipkow@13764  86  "EX x:A. P" == "Bex A (%x. P)"  clasohm@923  87 wenzelm@12633  88 syntax (output)  wenzelm@11979  89  "_setle" :: "'a set => 'a set => bool" ("op <=")  wenzelm@11979  90  "_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50)  wenzelm@11979  91  "_setless" :: "'a set => 'a set => bool" ("op <")  wenzelm@11979  92  "_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50)  clasohm@923  93 wenzelm@12114  94 syntax (xsymbols)  wenzelm@11979  95  "_setle" :: "'a set => 'a set => bool" ("op \")  wenzelm@11979  96  "_setle" :: "'a set => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  wenzelm@11979  97  "_setless" :: "'a set => 'a set => bool" ("op \")  wenzelm@11979  98  "_setless" :: "'a set => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  wenzelm@11979  99  "op Int" :: "'a set => 'a set => 'a set" (infixl "\" 70)  wenzelm@11979  100  "op Un" :: "'a set => 'a set => 'a set" (infixl "\" 65)  wenzelm@11979  101  "op :" :: "'a => 'a set => bool" ("op \")  wenzelm@11979  102  "op :" :: "'a => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  wenzelm@11979  103  "op ~:" :: "'a => 'a set => bool" ("op \")  wenzelm@11979  104  "op ~:" :: "'a => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  nipkow@14381  105  Union :: "'a set set => 'a set" ("\_" [90] 90)  nipkow@14381  106  Inter :: "'a set set => 'a set" ("\_" [90] 90)  nipkow@14381  107  "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  nipkow@14381  108  "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  nipkow@14381  109 kleing@14565  110 syntax (HTML output)  kleing@14565  111  "_setle" :: "'a set => 'a set => bool" ("op \")  kleing@14565  112  "_setle" :: "'a set => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  kleing@14565  113  "_setless" :: "'a set => 'a set => bool" ("op \")  kleing@14565  114  "_setless" :: "'a set => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  kleing@14565  115  "op Int" :: "'a set => 'a set => 'a set" (infixl "\" 70)  kleing@14565  116  "op Un" :: "'a set => 'a set => 'a set" (infixl "\" 65)  kleing@14565  117  "op :" :: "'a => 'a set => bool" ("op \")  kleing@14565  118  "op :" :: "'a => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  kleing@14565  119  "op ~:" :: "'a => 'a set => bool" ("op \")  kleing@14565  120  "op ~:" :: "'a => 'a set => bool" ("(_/ \ _)" [50, 51] 50)  kleing@14565  121  "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  kleing@14565  122  "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10)  kleing@14565  123 nipkow@14381  124 syntax (input)  wenzelm@11979  125  "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" 10)  wenzelm@11979  126  "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" 10)  wenzelm@11979  127  "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" 10)  wenzelm@11979  128  "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" 10)  nipkow@14381  129 nipkow@14381  130 syntax (xsymbols)  wenzelm@14692  131  "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\()\<^bsub>_\<^esub>/ _)" 10)  wenzelm@14692  132  "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\()\<^bsub>_\<^esub>/ _)" 10)  wenzelm@14692  133  "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\()\<^bsub>_\_\<^esub>/ _)" 10)  wenzelm@14692  134  "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\()\<^bsub>_\_\<^esub>/ _)" 10)  wenzelm@2261  135 kleing@14565  136 wenzelm@2412  137 translations  wenzelm@11979  138  "op \" => "op <= :: _ set => _ set => bool"  wenzelm@11979  139  "op \" => "op < :: _ set => _ set => bool"  wenzelm@2261  140 wenzelm@2261  141 wenzelm@11979  142 typed_print_translation {*  wenzelm@11979  143  let  wenzelm@11979  144  fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =  wenzelm@11979  145  list_comb (Syntax.const "_setle", ts)  wenzelm@11979  146  | le_tr' _ _ _ = raise Match;  wenzelm@11979  147 wenzelm@11979  148  fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =  wenzelm@11979  149  list_comb (Syntax.const "_setless", ts)  wenzelm@11979  150  | less_tr' _ _ _ = raise Match;  wenzelm@11979  151  in [("op <=", le_tr'), ("op <", less_tr')] end  wenzelm@11979  152 *}  wenzelm@2261  153 wenzelm@11979  154 text {*  wenzelm@11979  155  \medskip Translate between @{text "{e | x1...xn. P}"} and @{text  wenzelm@11979  156  "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is  wenzelm@11979  157  only translated if @{text "[0..n] subset bvs(e)"}.  wenzelm@11979  158 *}  wenzelm@11979  159 wenzelm@11979  160 parse_translation {*  wenzelm@11979  161  let  wenzelm@11979  162  val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));  wenzelm@3947  163 wenzelm@11979  164  fun nvars (Const ("_idts", _) $_$ idts) = nvars idts + 1  wenzelm@11979  165  | nvars _ = 1;  wenzelm@11979  166 wenzelm@11979  167  fun setcompr_tr [e, idts, b] =  wenzelm@11979  168  let  wenzelm@11979  169  val eq = Syntax.const "op =" $Bound (nvars idts)$ e;  wenzelm@11979  170  val P = Syntax.const "op &" $eq$ b;  wenzelm@11979  171  val exP = ex_tr [idts, P];  wenzelm@11979  172  in Syntax.const "Collect" $Abs ("", dummyT, exP) end;  wenzelm@11979  173 wenzelm@11979  174  in [("@SetCompr", setcompr_tr)] end;  wenzelm@11979  175 *}  clasohm@923  176 nipkow@13763  177 (* To avoid eta-contraction of body: *)  wenzelm@11979  178 print_translation {*  nipkow@13763  179 let  nipkow@13763  180  fun btr' syn [A,Abs abs] =  nipkow@13763  181  let val (x,t) = atomic_abs_tr' abs  nipkow@13763  182  in Syntax.const syn$ x $A$ t end  nipkow@13763  183 in  nipkow@13858  184 [("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),  nipkow@13858  185  ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]  nipkow@13763  186 end  nipkow@13763  187 *}  nipkow@13763  188 nipkow@13763  189 print_translation {*  nipkow@13763  190 let  nipkow@13763  191  val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));  nipkow@13763  192 nipkow@13763  193  fun setcompr_tr' [Abs (abs as (_, _, P))] =  nipkow@13763  194  let  nipkow@13763  195  fun check (Const ("Ex", _) $Abs (_, _, P), n) = check (P, n + 1)  nipkow@13763  196  | check (Const ("op &", _)$ (Const ("op =", _) $Bound m$ e) $P, n) =  nipkow@13763  197  n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso  nipkow@13763  198  ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))  nipkow@13764  199  | check _ = false  clasohm@923  200 wenzelm@11979  201  fun tr' (_$ abs) =  wenzelm@11979  202  let val _ $idts$ (_ $(_$ _ $e)$ Q) = ex_tr' [abs]  wenzelm@11979  203  in Syntax.const "@SetCompr" $e$ idts $Q end;  nipkow@13763  204  in if check (P, 0) then tr' P  nipkow@13763  205  else let val (x,t) = atomic_abs_tr' abs  nipkow@13763  206  in Syntax.const "@Coll"$ x \$ t end  nipkow@13763  207  end;  wenzelm@11979  208  in [("Collect", setcompr_tr')] end;  wenzelm@11979  209 *}  wenzelm@11979  210 wenzelm@11979  211 wenzelm@11979  212 subsection {* Rules and definitions *}  wenzelm@11979  213 wenzelm@11979  214 text {* Isomorphisms between predicates and sets. *}  clasohm@923  215 wenzelm@11979  216 axioms  wenzelm@11979  217  mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"  wenzelm@11979  218  Collect_mem_eq [simp]: "{x. x:A} = A"  wenzelm@11979  219 wenzelm@11979  220 defs  wenzelm@11979  221  Ball_def: "Ball A P == ALL x. x:A --> P(x)"  wenzelm@11979  222  Bex_def: "Bex A P == EX x. x:A & P(x)"  wenzelm@11979  223 wenzelm@11979  224 defs (overloaded)  wenzelm@11979  225  subset_def: "A <= B == ALL x:A. x:B"  wenzelm@11979  226  psubset_def: "A < B == (A::'a set) <= B & ~ A=B"  wenzelm@11979  227  Compl_def: "- A == {x. ~x:A}"  wenzelm@12257  228  set_diff_def: "A - B == {x. x:A & ~x:B}"  clasohm@923  229 clasohm@923  230 defs  wenzelm@11979  231  Un_def: "A Un B == {x. x:A | x:B}"  wenzelm@11979  232  Int_def: "A Int B == {x. x:A & x:B}"  wenzelm@11979  233  INTER_def: "INTER A B == {y. ALL x:A. y: B(x)}"  wenzelm@11979  234  UNION_def: "UNION A B == {y. EX x:A. y: B(x)}"  wenzelm@11979  235  Inter_def: "Inter S == (INT x:S. x)"  wenzelm@11979  236  Union_def: "Union S == (UN x:S. x)"  wenzelm@11979  237  Pow_def: "Pow A == {B. B <= A}"  wenzelm@11979  238  empty_def: "{} == {x. False}"  wenzelm@11979  239  UNIV_def: "UNIV == {x. True}"  wenzelm@11979  240  insert_def: "insert a B == {x. x=a} Un B"  wenzelm@11979  241  image_def: "fA == {y. EX x:A. y = f(x)}"  wenzelm@11979  242 wenzelm@11979  243 wenzelm@11979  244 subsection {* Lemmas and proof tool setup *}  wenzelm@11979  245 wenzelm@11979  246 subsubsection {* Relating predicates and sets *}  wenzelm@11979  247 wenzelm@12257  248 lemma CollectI: "P(a) ==> a : {x. P(x)}"  wenzelm@11979  249  by simp  wenzelm@11979  250 wenzelm@11979  251 lemma CollectD: "a : {x. P(x)} ==> P(a)"  wenzelm@11979  252  by simp  wenzelm@11979  253 wenzelm@11979  254 lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"  wenzelm@11979  255  by simp  wenzelm@11979  256 wenzelm@12257  257 lemmas CollectE = CollectD [elim_format]  wenzelm@11979  258 wenzelm@11979  259 wenzelm@11979  260 subsubsection {* Bounded quantifiers *}  wenzelm@11979  261 wenzelm@11979  262 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"  wenzelm@11979  263  by (simp add: Ball_def)  wenzelm@11979  264 wenzelm@11979  265 lemmas strip = impI allI ballI  wenzelm@11979  266 wenzelm@11979  267 lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"  wenzelm@11979  268  by (simp add: Ball_def)  wenzelm@11979  269 wenzelm@11979  270 lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"  wenzelm@11979  271  by (unfold Ball_def) blast  oheimb@14098  272 ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *}  wenzelm@11979  273 wenzelm@11979  274 text {*  wenzelm@11979  275  \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and  wenzelm@11979  276  @{prop "a:A"}; creates assumption @{prop "P a"}.  wenzelm@11979  277 *}  wenzelm@11979  278 wenzelm@11979  279 ML {*  wenzelm@11979  280  local val ballE = thm "ballE"  wenzelm@11979  281  in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end;  wenzelm@11979  282 *}  wenzelm@11979  283 wenzelm@11979  284 text {*  wenzelm@11979  285  Gives better instantiation for bound:  wenzelm@11979  286 *}  wenzelm@11979  287 wenzelm@11979  288 ML_setup {*  wenzelm@11979  289  claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1);  wenzelm@11979  290 *}  wenzelm@11979  291 wenzelm@11979  292 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"  wenzelm@11979  293  -- {* Normally the best argument order: @{prop "P x"} constrains the  wenzelm@11979  294  choice of @{prop "x:A"}. *}  wenzelm@11979  295  by (unfold Bex_def) blast  wenzelm@11979  296 wenzelm@13113  297 lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x"  wenzelm@11979  298  -- {* The best argument order when there is only one @{prop "x:A"}. *}  wenzelm@11979  299  by (unfold Bex_def) blast  wenzelm@11979  300 wenzelm@11979  301 lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"  wenzelm@11979  302  by (unfold Bex_def) blast  wenzelm@11979  303 wenzelm@11979  304 lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q"  wenzelm@11979  305  by (unfold Bex_def) blast  wenzelm@11979  306 wenzelm@11979  307 lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"  wenzelm@11979  308  -- {* Trival rewrite rule. *}  wenzelm@11979  309  by (simp add: Ball_def)  wenzelm@11979  310 wenzelm@11979  311 lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"  wenzelm@11979  312  -- {* Dual form for existentials. *}  wenzelm@11979  313  by (simp add: Bex_def)  wenzelm@11979  314 wenzelm@11979  315 lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"  wenzelm@11979  316  by blast  wenzelm@11979  317 wenzelm@11979  318 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"  wenzelm@11979  319  by blast  wenzelm@11979  320 wenzelm@11979  321 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"  wenzelm@11979  322  by blast  wenzelm@11979  323 wenzelm@11979  324 lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)"  wenzelm@11979  325  by blast  wenzelm@11979  326 wenzelm@11979  327 lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)"  wenzelm@11979  328  by blast  wenzelm@11979  329 wenzelm@11979  330 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"  wenzelm@11979  331  by blast  wenzelm@11979  332 wenzelm@11979  333 ML_setup {*  wenzelm@13462  334  local  wenzelm@11979  335  val Ball_def = thm "Ball_def";  wenzelm@11979  336  val Bex_def = thm "Bex_def";  wenzelm@11979  337 wenzelm@11979  338  val prove_bex_tac =  wenzelm@11979  339  rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;  wenzelm@11979  340  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;  wenzelm@11979  341 wenzelm@11979  342  val prove_ball_tac =  wenzelm@11979  343  rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;  wenzelm@11979  344  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;  wenzelm@11979  345  in  wenzelm@13462  346  val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))  wenzelm@13462  347  "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;  wenzelm@13462  348  val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))  wenzelm@13462  349  "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;  wenzelm@11979  350  end;  wenzelm@13462  351 wenzelm@13462  352  Addsimprocs [defBALL_regroup, defBEX_regroup];  wenzelm@11979  353 *}  wenzelm@11979  354 wenzelm@11979  355 wenzelm@11979  356 subsubsection {* Congruence rules *}  wenzelm@11979  357 wenzelm@11979  358 lemma ball_cong [cong]:  wenzelm@11979  359  "A = B ==> (!!x. x:B ==> P x = Q x) ==>  wenzelm@11979  360  (ALL x:A. P x) = (ALL x:B. Q x)"  wenzelm@11979  361  by (simp add: Ball_def)  wenzelm@11979  362 wenzelm@11979  363 lemma bex_cong [cong]:  wenzelm@11979  364  "A = B ==> (!!x. x:B ==> P x = Q x) ==>  wenzelm@11979  365  (EX x:A. P x) = (EX x:B. Q x)"  wenzelm@11979  366  by (simp add: Bex_def cong: conj_cong)  regensbu@1273  367 wenzelm@7238  368 wenzelm@11979  369 subsubsection {* Subsets *}  wenzelm@11979  370 wenzelm@12897  371 lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A \ B"  wenzelm@11979  372  by (simp add: subset_def)  wenzelm@11979  373 wenzelm@11979  374 text {*  wenzelm@11979  375  \medskip Map the type @{text "'a set => anything"} to just @{typ  wenzelm@11979  376  'a}; for overloading constants whose first argument has type @{typ  wenzelm@11979  377  "'a set"}.  wenzelm@11979  378 *}  wenzelm@11979  379 wenzelm@12897  380 lemma subsetD [elim]: "A \ B ==> c \ A ==> c \ B"  wenzelm@11979  381  -- {* Rule in Modus Ponens style. *}  wenzelm@11979  382  by (unfold subset_def) blast  wenzelm@11979  383 wenzelm@11979  384 declare subsetD [intro?] -- FIXME  wenzelm@11979  385 wenzelm@12897  386 lemma rev_subsetD: "c \ A ==> A \ B ==> c \ B"  wenzelm@11979  387  -- {* The same, with reversed premises for use with @{text erule} --  wenzelm@11979  388  cf @{text rev_mp}. *}  wenzelm@11979  389  by (rule subsetD)  wenzelm@11979  390 wenzelm@11979  391 declare rev_subsetD [intro?] -- FIXME  wenzelm@11979  392 wenzelm@11979  393 text {*  wenzelm@12897  394  \medskip Converts @{prop "A \ B"} to @{prop "x \ A ==> x \ B"}.  wenzelm@11979  395 *}  wenzelm@11979  396 wenzelm@11979  397 ML {*  wenzelm@11979  398  local val rev_subsetD = thm "rev_subsetD"  wenzelm@11979  399  in fun impOfSubs th = th RSN (2, rev_subsetD) end;  wenzelm@11979  400 *}  wenzelm@11979  401 wenzelm@12897  402 lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P"  wenzelm@11979  403  -- {* Classical elimination rule. *}  wenzelm@11979  404  by (unfold subset_def) blast  wenzelm@11979  405 wenzelm@11979  406 text {*  wenzelm@12897  407  \medskip Takes assumptions @{prop "A \ B"}; @{prop "c \ A"} and  wenzelm@12897  408  creates the assumption @{prop "c \ B"}.  wenzelm@11979  409 *}  wenzelm@11979  410 wenzelm@11979  411 ML {*  wenzelm@11979  412  local val subsetCE = thm "subsetCE"  wenzelm@11979  413  in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;  wenzelm@11979  414 *}  wenzelm@11979  415 wenzelm@12897  416 lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A"  wenzelm@11979  417  by blast  wenzelm@11979  418 wenzelm@12897  419 lemma subset_refl: "A \ A"  wenzelm@11979  420  by fast  wenzelm@11979  421 wenzelm@12897  422 lemma subset_trans: "A \ B ==> B \ C ==> A \ C"  wenzelm@11979  423  by blast  clasohm@923  424 wenzelm@2261  425 wenzelm@11979  426 subsubsection {* Equality *}  wenzelm@11979  427 paulson@13865  428 lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"  paulson@13865  429  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])  paulson@13865  430  apply (rule Collect_mem_eq)  paulson@13865  431  apply (rule Collect_mem_eq)  paulson@13865  432  done  paulson@13865  433 wenzelm@12897  434 lemma subset_antisym [intro!]: "A \ B ==> B \ A ==> A = B"  wenzelm@11979  435  -- {* Anti-symmetry of the subset relation. *}  wenzelm@12897  436  by (rules intro: set_ext subsetD)  wenzelm@12897  437 wenzelm@12897  438 lemmas equalityI [intro!] = subset_antisym  wenzelm@11979  439 wenzelm@11979  440 text {*  wenzelm@11979  441  \medskip Equality rules from ZF set theory -- are they appropriate  wenzelm@11979  442  here?  wenzelm@11979  443 *}  wenzelm@11979  444 wenzelm@12897  445 lemma equalityD1: "A = B ==> A \ B"  wenzelm@11979  446  by (simp add: subset_refl)  wenzelm@11979  447 wenzelm@12897  448 lemma equalityD2: "A = B ==> B \ A"  wenzelm@11979  449  by (simp add: subset_refl)  wenzelm@11979  450 wenzelm@11979  451 text {*  wenzelm@11979  452  \medskip Be careful when adding this to the claset as @{text  wenzelm@11979  453  subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}  wenzelm@12897  454  \ A"} and @{prop "A \ {}"} and then back to @{prop "A = {}"}!  wenzelm@11979  455 *}  wenzelm@11979  456 wenzelm@12897  457 lemma equalityE: "A = B ==> (A \ B ==> B \ A ==> P) ==> P"  wenzelm@11979  458  by (simp add: subset_refl)  clasohm@923  459 wenzelm@11979  460 lemma equalityCE [elim]:  wenzelm@12897  461  "A = B ==> (c \ A ==> c \ B ==> P) ==> (c \ A ==> c \ B ==> P) ==> P"  wenzelm@11979  462  by blast  wenzelm@11979  463 wenzelm@11979  464 text {*  wenzelm@11979  465  \medskip Lemma for creating induction formulae -- for "pattern  wenzelm@11979  466  matching" on @{text p}. To make the induction hypotheses usable,  wenzelm@11979  467  apply @{text spec} or @{text bspec} to put universal quantifiers over the free  wenzelm@11979  468  variables in @{text p}.  wenzelm@11979  469 *}  wenzelm@11979  470 wenzelm@11979  471 lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R"  wenzelm@11979  472  by simp  clasohm@923  473 wenzelm@11979  474 lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"  wenzelm@11979  475  by simp  wenzelm@11979  476 paulson@13865  477 lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"  paulson@13865  478  by simp  paulson@13865  479 wenzelm@11979  480 wenzelm@11979  481 subsubsection {* The universal set -- UNIV *}  wenzelm@11979  482 wenzelm@11979  483 lemma UNIV_I [simp]: "x : UNIV"  wenzelm@11979  484  by (simp add: UNIV_def)  wenzelm@11979  485 wenzelm@11979  486 declare UNIV_I [intro] -- {* unsafe makes it less likely to cause problems *}  wenzelm@11979  487 wenzelm@11979  488 lemma UNIV_witness [intro?]: "EX x. x : UNIV"  wenzelm@11979  489  by simp  wenzelm@11979  490 wenzelm@12897  491 lemma subset_UNIV: "A \ UNIV"  wenzelm@11979  492  by (rule subsetI) (rule UNIV_I)  wenzelm@2388  493 wenzelm@11979  494 text {*  wenzelm@11979  495  \medskip Eta-contracting these two rules (to remove @{text P})  wenzelm@11979  496  causes them to be ignored because of their interaction with  wenzelm@11979  497  congruence rules.  wenzelm@11979  498 *}  wenzelm@11979  499 wenzelm@11979  500 lemma ball_UNIV [simp]: "Ball UNIV P = All P"  wenzelm@11979  501  by (simp add: Ball_def)  wenzelm@11979  502 wenzelm@11979  503 lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"  wenzelm@11979  504  by (simp add: Bex_def)  wenzelm@11979  505 wenzelm@11979  506 wenzelm@11979  507 subsubsection {* The empty set *}  wenzelm@11979  508 wenzelm@11979  509 lemma empty_iff [simp]: "(c : {}) = False"  wenzelm@11979  510  by (simp add: empty_def)  wenzelm@11979  511 wenzelm@11979  512 lemma emptyE [elim!]: "a : {} ==> P"  wenzelm@11979  513  by simp  wenzelm@11979  514 wenzelm@12897  515 lemma empty_subsetI [iff]: "{} \ A"  wenzelm@11979  516  -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}  wenzelm@11979  517  by blast  wenzelm@11979  518 wenzelm@12897  519 lemma equals0I: "(!!y. y \ A ==> False) ==> A = {}"  wenzelm@11979  520  by blast  wenzelm@2388  521 wenzelm@12897  522 lemma equals0D: "A = {} ==> a \ A"  wenzelm@11979  523  -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}  wenzelm@11979  524  by blast  wenzelm@11979  525 wenzelm@11979  526 lemma ball_empty [simp]: "Ball {} P = True"  wenzelm@11979  527  by (simp add: Ball_def)  wenzelm@11979  528 wenzelm@11979  529 lemma bex_empty [simp]: "Bex {} P = False"  wenzelm@11979  530  by (simp add: Bex_def)  wenzelm@11979  531 wenzelm@11979  532 lemma UNIV_not_empty [iff]: "UNIV ~= {}"  wenzelm@11979  533  by (blast elim: equalityE)  wenzelm@11979  534 wenzelm@11979  535 wenzelm@12023  536 subsubsection {* The Powerset operator -- Pow *}  wenzelm@11979  537 wenzelm@12897  538 lemma Pow_iff [iff]: "(A \ Pow B) = (A \ B)"  wenzelm@11979  539  by (simp add: Pow_def)  wenzelm@11979  540 wenzelm@12897  541 lemma PowI: "A \ B ==> A \ Pow B"  wenzelm@11979  542  by (simp add: Pow_def)  wenzelm@11979  543 wenzelm@12897  544 lemma PowD: "A \ Pow B ==> A \ B"  wenzelm@11979  545  by (simp add: Pow_def)  wenzelm@11979  546 wenzelm@12897  547 lemma Pow_bottom: "{} \ Pow B"  wenzelm@11979  548  by simp  wenzelm@11979  549 wenzelm@12897  550 lemma Pow_top: "A \ Pow A"  wenzelm@11979  551  by (simp add: subset_refl)  wenzelm@2684  552 wenzelm@2388  553 wenzelm@11979  554 subsubsection {* Set complement *}  wenzelm@11979  555 wenzelm@12897  556 lemma Compl_iff [simp]: "(c \ -A) = (c \ A)"  wenzelm@11979  557  by (unfold Compl_def) blast  wenzelm@11979  558 wenzelm@12897  559 lemma ComplI [intro!]: "(c \ A ==> False) ==> c \ -A"  wenzelm@11979  560  by (unfold Compl_def) blast  wenzelm@11979  561 wenzelm@11979  562 text {*  wenzelm@11979  563  \medskip This form, with negated conclusion, works well with the  wenzelm@11979  564  Classical prover. Negated assumptions behave like formulae on the  wenzelm@11979  565  right side of the notional turnstile ... *}  wenzelm@11979  566 wenzelm@11979  567 lemma ComplD: "c : -A ==> c~:A"  wenzelm@11979  568  by (unfold Compl_def) blast  wenzelm@11979  569 wenzelm@11979  570 lemmas ComplE [elim!] = ComplD [elim_format]  wenzelm@11979  571 wenzelm@11979  572 wenzelm@11979  573 subsubsection {* Binary union -- Un *}  clasohm@923  574 wenzelm@11979  575 lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"  wenzelm@11979  576  by (unfold Un_def) blast  wenzelm@11979  577 wenzelm@11979  578 lemma UnI1 [elim?]: "c:A ==> c : A Un B"  wenzelm@11979  579  by simp  wenzelm@11979  580 wenzelm@11979  581 lemma UnI2 [elim?]: "c:B ==> c : A Un B"  wenzelm@11979  582  by simp  clasohm@923  583 wenzelm@11979  584 text {*  wenzelm@11979  585  \medskip Classical introduction rule: no commitment to @{prop A} vs  wenzelm@11979  586  @{prop B}.  wenzelm@11979  587 *}  wenzelm@11979  588 wenzelm@11979  589 lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"  wenzelm@11979  590  by auto  wenzelm@11979  591 wenzelm@11979  592 lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"  wenzelm@11979  593  by (unfold Un_def) blast  wenzelm@11979  594 wenzelm@11979  595 wenzelm@12023  596 subsubsection {* Binary intersection -- Int *}  clasohm@923  597 wenzelm@11979  598 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"  wenzelm@11979  599  by (unfold Int_def) blast  wenzelm@11979  600 wenzelm@11979  601 lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"  wenzelm@11979  602  by simp  wenzelm@11979  603 wenzelm@11979  604 lemma IntD1: "c : A Int B ==> c:A"  wenzelm@11979  605  by simp  wenzelm@11979  606 wenzelm@11979  607 lemma IntD2: "c : A Int B ==> c:B"  wenzelm@11979  608  by simp  wenzelm@11979  609 wenzelm@11979  610 lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"  wenzelm@11979  611  by simp  wenzelm@11979  612 wenzelm@11979  613 wenzelm@12023  614 subsubsection {* Set difference *}  wenzelm@11979  615 wenzelm@11979  616 lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"  wenzelm@11979  617  by (unfold set_diff_def) blast  clasohm@923  618 wenzelm@11979  619 lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"  wenzelm@11979  620  by simp  wenzelm@11979  621 wenzelm@11979  622 lemma DiffD1: "c : A - B ==> c : A"  wenzelm@11979  623  by simp  wenzelm@11979  624 wenzelm@11979  625 lemma DiffD2: "c : A - B ==> c : B ==> P"  wenzelm@11979  626  by simp  wenzelm@11979  627 wenzelm@11979  628 lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"  wenzelm@11979  629  by simp  wenzelm@11979  630 wenzelm@11979  631 wenzelm@11979  632 subsubsection {* Augmenting a set -- insert *}  wenzelm@11979  633 wenzelm@11979  634 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"  wenzelm@11979  635  by (unfold insert_def) blast  wenzelm@11979  636 wenzelm@11979  637 lemma insertI1: "a : insert a B"  wenzelm@11979  638  by simp  wenzelm@11979  639 wenzelm@11979  640 lemma insertI2: "a : B ==> a : insert b B"  wenzelm@11979  641  by simp  clasohm@923  642 wenzelm@11979  643 lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"  wenzelm@11979  644  by (unfold insert_def) blast  wenzelm@11979  645 wenzelm@11979  646 lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"  wenzelm@11979  647  -- {* Classical introduction rule. *}  wenzelm@11979  648  by auto  wenzelm@11979  649 wenzelm@12897  650 lemma subset_insert_iff: "(A \ insert x B) = (if x:A then A - {x} \ B else A \ B)"  wenzelm@11979  651  by auto  wenzelm@11979  652 wenzelm@11979  653 wenzelm@11979  654 subsubsection {* Singletons, using insert *}  wenzelm@11979  655 wenzelm@11979  656 lemma singletonI [intro!]: "a : {a}"  wenzelm@11979  657  -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}  wenzelm@11979  658  by (rule insertI1)  wenzelm@11979  659 wenzelm@11979  660 lemma singletonD: "b : {a} ==> b = a"  wenzelm@11979  661  by blast  wenzelm@11979  662 wenzelm@11979  663 lemmas singletonE [elim!] = singletonD [elim_format]  wenzelm@11979  664 wenzelm@11979  665 lemma singleton_iff: "(b : {a}) = (b = a)"  wenzelm@11979  666  by blast  wenzelm@11979  667 wenzelm@11979  668 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"  wenzelm@11979  669  by blast  wenzelm@11979  670 wenzelm@12897  671 lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A \ {b})"  wenzelm@11979  672  by blast  wenzelm@11979  673 wenzelm@12897  674 lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A \ {b})"  wenzelm@11979  675  by blast  wenzelm@11979  676 wenzelm@12897  677 lemma subset_singletonD: "A \ {x} ==> A = {} | A = {x}"  wenzelm@11979  678  by fast  wenzelm@11979  679 wenzelm@11979  680 lemma singleton_conv [simp]: "{x. x = a} = {a}"  wenzelm@11979  681  by blast  wenzelm@11979  682 wenzelm@11979  683 lemma singleton_conv2 [simp]: "{x. a = x} = {a}"  wenzelm@11979  684  by blast  clasohm@923  685 wenzelm@12897  686 lemma diff_single_insert: "A - {x} \ B ==> x \ A ==> A \ insert x B"  wenzelm@11979  687  by blast  wenzelm@11979  688 wenzelm@11979  689 wenzelm@11979  690 subsubsection {* Unions of families *}  wenzelm@11979  691 wenzelm@11979  692 text {*  wenzelm@11979  693  @{term [source] "UN x:A. B x"} is @{term "Union (BA)"}.  wenzelm@11979  694 *}  wenzelm@11979  695 wenzelm@11979  696 lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"  wenzelm@11979  697  by (unfold UNION_def) blast  wenzelm@11979  698 wenzelm@11979  699 lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"  wenzelm@11979  700  -- {* The order of the premises presupposes that @{term A} is rigid;  wenzelm@11979  701  @{term b} may be flexible. *}  wenzelm@11979  702  by auto  wenzelm@11979  703 wenzelm@11979  704 lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"  wenzelm@11979  705  by (unfold UNION_def) blast  clasohm@923  706 wenzelm@11979  707 lemma UN_cong [cong]:  wenzelm@11979  708  "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"  wenzelm@11979  709  by (simp add: UNION_def)  wenzelm@11979  710 wenzelm@11979  711 wenzelm@11979  712 subsubsection {* Intersections of families *}  wenzelm@11979  713 wenzelm@11979  714 text {* @{term [source] "INT x:A. B x"} is @{term "Inter (BA)"}. *}  wenzelm@11979  715 wenzelm@11979  716 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"  wenzelm@11979  717  by (unfold INTER_def) blast  clasohm@923  718 wenzelm@11979  719 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"  wenzelm@11979  720  by (unfold INTER_def) blast  wenzelm@11979  721 wenzelm@11979  722 lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"  wenzelm@11979  723  by auto  wenzelm@11979  724 wenzelm@11979  725 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"  wenzelm@11979  726  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}  wenzelm@11979  727  by (unfold INTER_def) blast  wenzelm@11979  728 wenzelm@11979  729 lemma INT_cong [cong]:  wenzelm@11979  730  "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"  wenzelm@11979  731  by (simp add: INTER_def)  wenzelm@7238  732 clasohm@923  733 wenzelm@11979  734 subsubsection {* Union *}  wenzelm@11979  735 wenzelm@11979  736 lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)"  wenzelm@11979  737  by (unfold Union_def) blast  wenzelm@11979  738 wenzelm@11979  739 lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"  wenzelm@11979  740  -- {* The order of the premises presupposes that @{term C} is rigid;  wenzelm@11979  741  @{term A} may be flexible. *}  wenzelm@11979  742  by auto  wenzelm@11979  743 wenzelm@11979  744 lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"  wenzelm@11979  745  by (unfold Union_def) blast  wenzelm@11979  746 wenzelm@11979  747 wenzelm@11979  748 subsubsection {* Inter *}  wenzelm@11979  749 wenzelm@11979  750 lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)"  wenzelm@11979  751  by (unfold Inter_def) blast  wenzelm@11979  752 wenzelm@11979  753 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"  wenzelm@11979  754  by (simp add: Inter_def)  wenzelm@11979  755 wenzelm@11979  756 text {*  wenzelm@11979  757  \medskip A destruct'' rule -- every @{term X} in @{term C}  wenzelm@11979  758  contains @{term A} as an element, but @{prop "A:X"} can hold when  wenzelm@11979  759  @{prop "X:C"} does not! This rule is analogous to @{text spec}.  wenzelm@11979  760 *}  wenzelm@11979  761 wenzelm@11979  762 lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"  wenzelm@11979  763  by auto  wenzelm@11979  764 wenzelm@11979  765 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"  wenzelm@11979  766  -- {* Classical'' elimination rule -- does not require proving  wenzelm@11979  767  @{prop "X:C"}. *}  wenzelm@11979  768  by (unfold Inter_def) blast  wenzelm@11979  769 wenzelm@11979  770 text {*  wenzelm@11979  771  \medskip Image of a set under a function. Frequently @{term b} does  wenzelm@11979  772  not have the syntactic form of @{term "f x"}.  wenzelm@11979  773 *}  wenzelm@11979  774 wenzelm@11979  775 lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : fA"  wenzelm@11979  776  by (unfold image_def) blast  wenzelm@11979  777 wenzelm@11979  778 lemma imageI: "x : A ==> f x : f  A"  wenzelm@11979  779  by (rule image_eqI) (rule refl)  wenzelm@11979  780 wenzelm@11979  781 lemma rev_image_eqI: "x:A ==> b = f x ==> b : fA"  wenzelm@11979  782  -- {* This version's more effective when we already have the  wenzelm@11979  783  required @{term x}. *}  wenzelm@11979  784  by (unfold image_def) blast  wenzelm@11979  785 wenzelm@11979  786 lemma imageE [elim!]:  wenzelm@11979  787  "b : (%x. f x)A ==> (!!x. b = f x ==> x:A ==> P) ==> P"  wenzelm@11979  788  -- {* The eta-expansion gives variable-name preservation. *}  wenzelm@11979  789  by (unfold image_def) blast  wenzelm@11979  790 wenzelm@11979  791 lemma image_Un: "f(A Un B) = fA Un fB"  wenzelm@11979  792  by blast  wenzelm@11979  793 wenzelm@11979  794 lemma image_iff: "(z : fA) = (EX x:A. z = f x)"  wenzelm@11979  795  by blast  wenzelm@11979  796 wenzelm@12897  797 lemma image_subset_iff: "(fA \ B) = (\x\A. f x \ B)"  wenzelm@11979  798  -- {* This rewrite rule would confuse users if made default. *}  wenzelm@11979  799  by blast  wenzelm@11979  800 wenzelm@12897  801 lemma subset_image_iff: "(B \ fA) = (EX AA. AA \ A & B = fAA)"  wenzelm@11979  802  apply safe  wenzelm@11979  803  prefer 2 apply fast  paulson@14208  804  apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)  wenzelm@11979  805  done  wenzelm@11979  806 wenzelm@12897  807 lemma image_subsetI: "(!!x. x \ A ==> f x \ B) ==> fA \ B"  wenzelm@11979  808  -- {* Replaces the three steps @{text subsetI}, @{text imageE},  wenzelm@11979  809  @{text hypsubst}, but breaks too many existing proofs. *}  wenzelm@11979  810  by blast  wenzelm@11979  811 wenzelm@11979  812 text {*  wenzelm@11979  813  \medskip Range of a function -- just a translation for image!  wenzelm@11979  814 *}  wenzelm@11979  815 wenzelm@12897  816 lemma range_eqI: "b = f x ==> b \ range f"  wenzelm@11979  817  by simp  wenzelm@11979  818 wenzelm@12897  819 lemma rangeI: "f x \ range f"  wenzelm@11979  820  by simp  wenzelm@11979  821 wenzelm@12897  822 lemma rangeE [elim?]: "b \ range (\x. f x) ==> (!!x. b = f x ==> P) ==> P"  wenzelm@11979  823  by blast  wenzelm@11979  824 wenzelm@11979  825 wenzelm@11979  826 subsubsection {* Set reasoning tools *}  wenzelm@11979  827 wenzelm@11979  828 text {*  wenzelm@11979  829  Rewrite rules for boolean case-splitting: faster than @{text  wenzelm@11979  830  "split_if [split]"}.  wenzelm@11979  831 *}  wenzelm@11979  832 wenzelm@11979  833 lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"  wenzelm@11979  834  by (rule split_if)  wenzelm@11979  835 wenzelm@11979  836 lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"  wenzelm@11979  837  by (rule split_if)  wenzelm@11979  838 wenzelm@11979  839 text {*  wenzelm@11979  840  Split ifs on either side of the membership relation. Not for @{text  wenzelm@11979  841  "[simp]"} -- can cause goals to blow up!  wenzelm@11979  842 *}  wenzelm@11979  843 wenzelm@11979  844 lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"  wenzelm@11979  845  by (rule split_if)  wenzelm@11979  846 wenzelm@11979  847 lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"  wenzelm@11979  848  by (rule split_if)  wenzelm@11979  849 wenzelm@11979  850 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2  wenzelm@11979  851 wenzelm@11979  852 lemmas mem_simps =  wenzelm@11979  853  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff  wenzelm@11979  854  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff  wenzelm@11979  855  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}  wenzelm@11979  856 wenzelm@11979  857 (*Would like to add these, but the existing code only searches for the  wenzelm@11979  858  outer-level constant, which in this case is just "op :"; we instead need  wenzelm@11979  859  to use term-nets to associate patterns with rules. Also, if a rule fails to  wenzelm@11979  860  apply, then the formula should be kept.  wenzelm@11979  861  [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]),  wenzelm@11979  862  ("op Int", [IntD1,IntD2]),  wenzelm@11979  863  ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]  wenzelm@11979  864  *)  wenzelm@11979  865 wenzelm@11979  866 ML_setup {*  wenzelm@11979  867  val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;  wenzelm@11979  868  simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);  wenzelm@11979  869 *}  wenzelm@11979  870 wenzelm@11979  871 declare subset_UNIV [simp] subset_refl [simp]  wenzelm@11979  872 wenzelm@11979  873 wenzelm@11979  874 subsubsection {* The proper subset'' relation *}  wenzelm@11979  875 wenzelm@12897  876 lemma psubsetI [intro!]: "A \ B ==> A \ B ==> A \ B"  wenzelm@11979  877  by (unfold psubset_def) blast  wenzelm@11979  878 paulson@13624  879 lemma psubsetE [elim!]:  paulson@13624  880  "[|A \ B; [|A \ B; ~ (B\A)|] ==> R|] ==> R"  paulson@13624  881  by (unfold psubset_def) blast  paulson@13624  882 wenzelm@11979  883 lemma psubset_insert_iff:  wenzelm@12897  884  "(A \ insert x B) = (if x \ B then A \ B else if x \ A then A - {x} \ B else A \ B)"  wenzelm@12897  885  by (auto simp add: psubset_def subset_insert_iff)  wenzelm@12897  886 wenzelm@12897  887 lemma psubset_eq: "(A \ B) = (A \ B & A \ B)"  wenzelm@11979  888  by (simp only: psubset_def)  wenzelm@11979  889 wenzelm@12897  890 lemma psubset_imp_subset: "A \ B ==> A \ B"  wenzelm@11979  891  by (simp add: psubset_eq)  wenzelm@11979  892 paulson@14335  893 lemma psubset_trans: "[| A \ B; B \ C |] ==> A \ C"  paulson@14335  894 apply (unfold psubset_def)  paulson@14335  895 apply (auto dest: subset_antisym)  paulson@14335  896 done  paulson@14335  897 paulson@14335  898 lemma psubsetD: "[| A \ B; c \ A |] ==> c \ B"  paulson@14335  899 apply (unfold psubset_def)  paulson@14335  900 apply (auto dest: subsetD)  paulson@14335  901 done  paulson@14335  902 wenzelm@12897  903 lemma psubset_subset_trans: "A \ B ==> B \ C ==> A \ C"  wenzelm@11979  904  by (auto simp add: psubset_eq)  wenzelm@11979  905 wenzelm@12897  906 lemma subset_psubset_trans: "A \ B ==> B \ C ==> A \ C"  wenzelm@11979  907  by (auto simp add: psubset_eq)  wenzelm@11979  908 wenzelm@12897  909 lemma psubset_imp_ex_mem: "A \ B ==> \b. b \ (B - A)"  wenzelm@11979  910  by (unfold psubset_def) blast  wenzelm@11979  911 wenzelm@11979  912 lemma atomize_ball:  wenzelm@12897  913  "(!!x. x \ A ==> P x) == Trueprop (\x\A. P x)"  wenzelm@11979  914  by (simp only: Ball_def atomize_all atomize_imp)  wenzelm@11979  915 wenzelm@11979  916 declare atomize_ball [symmetric, rulify]  wenzelm@11979  917 wenzelm@11979  918 wenzelm@11979  919 subsection {* Further set-theory lemmas *}  wenzelm@11979  920 wenzelm@12897  921 subsubsection {* Derived rules involving subsets. *}  wenzelm@12897  922 wenzelm@12897  923 text {* @{text insert}. *}  wenzelm@12897  924 wenzelm@12897  925 lemma subset_insertI: "B \ insert a B"  wenzelm@12897  926  apply (rule subsetI)  wenzelm@12897  927  apply (erule insertI2)  wenzelm@12897  928  done  wenzelm@12897  929 nipkow@14302  930 lemma subset_insertI2: "A \ B \ A \ insert b B"  nipkow@14302  931 by blast  nipkow@14302  932 wenzelm@12897  933 lemma subset_insert: "x \ A ==> (A \ insert x B) = (A \ B)"  wenzelm@12897  934  by blast  wenzelm@12897  935 wenzelm@12897  936 wenzelm@12897  937 text {* \medskip Big Union -- least upper bound of a set. *}  wenzelm@12897  938 wenzelm@12897  939 lemma Union_upper: "B \ A ==> B \ Union A"  wenzelm@12897  940  by (rules intro: subsetI UnionI)  wenzelm@12897  941 wenzelm@12897  942 lemma Union_least: "(!!X. X \ A ==> X \ C) ==> Union A \ C"  wenzelm@12897  943  by (rules intro: subsetI elim: UnionE dest: subsetD)  wenzelm@12897  944 wenzelm@12897  945 wenzelm@12897  946 text {* \medskip General union. *}  wenzelm@12897  947 wenzelm@12897  948 lemma UN_upper: "a \ A ==> B a \ (\x\A. B x)"  wenzelm@12897  949  by blast  wenzelm@12897  950 wenzelm@12897  951 lemma UN_least: "(!!x. x \ A ==> B x \ C) ==> (\x\A. B x) \ C"  wenzelm@12897  952  by (rules intro: subsetI elim: UN_E dest: subsetD)  wenzelm@12897  953 wenzelm@12897  954 wenzelm@12897  955 text {* \medskip Big Intersection -- greatest lower bound of a set. *}  wenzelm@12897  956 wenzelm@12897  957 lemma Inter_lower: "B \ A ==> Inter A \ B"  wenzelm@12897  958  by blast  wenzelm@12897  959 ballarin@14551  960 lemma Inter_subset:  ballarin@14551  961  "[| !!X. X \ A ==> X \ B; A ~= {} |] ==> \A \ B"  ballarin@14551  962  by blast  ballarin@14551  963 wenzelm@12897  964 lemma Inter_greatest: "(!!X. X \ A ==> C \ X) ==> C \ Inter A"  wenzelm@12897  965  by (rules intro: InterI subsetI dest: subsetD)  wenzelm@12897  966 wenzelm@12897  967 lemma INT_lower: "a \ A ==> (\x\A. B x) \ B a"  wenzelm@12897  968  by blast  wenzelm@12897  969 wenzelm@12897  970 lemma INT_greatest: "(!!x. x \ A ==> C \ B x) ==> C \ (\x\A. B x)"  wenzelm@12897  971  by (rules intro: INT_I subsetI dest: subsetD)  wenzelm@12897  972 wenzelm@12897  973 wenzelm@12897  974 text {* \medskip Finite Union -- the least upper bound of two sets. *}  wenzelm@12897  975 wenzelm@12897  976 lemma Un_upper1: "A \ A \ B"  wenzelm@12897  977  by blast  wenzelm@12897  978 wenzelm@12897  979 lemma Un_upper2: "B \ A \ B"  wenzelm@12897  980  by blast  wenzelm@12897  981 wenzelm@12897  982 lemma Un_least: "A \ C ==> B \ C ==> A \ B \ C"  wenzelm@12897  983  by blast  wenzelm@12897  984 wenzelm@12897  985 wenzelm@12897  986 text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}  wenzelm@12897  987 wenzelm@12897  988 lemma Int_lower1: "A \ B \ A"  wenzelm@12897  989  by blast  wenzelm@12897  990 wenzelm@12897  991 lemma Int_lower2: "A \ B \ B"  wenzelm@12897  992  by blast  wenzelm@12897  993 wenzelm@12897  994 lemma Int_greatest: "C \ A ==> C \ B ==> C \ A \ B"  wenzelm@12897  995  by blast  wenzelm@12897  996 wenzelm@12897  997 wenzelm@12897  998 text {* \medskip Set difference. *}  wenzelm@12897  999 wenzelm@12897  1000 lemma Diff_subset: "A - B \ A"  wenzelm@12897  1001  by blast  wenzelm@12897  1002 nipkow@14302  1003 lemma Diff_subset_conv: "(A - B \ C) = (A \ B \ C)"  nipkow@14302  1004 by blast  nipkow@14302  1005 wenzelm@12897  1006 wenzelm@12897  1007 text {* \medskip Monotonicity. *}  wenzelm@12897  1008 wenzelm@13421  1009 lemma mono_Un: includes mono shows "f A \ f B \ f (A \ B)"  wenzelm@12897  1010  apply (rule Un_least)  wenzelm@13421  1011  apply (rule Un_upper1 [THEN mono])  wenzelm@13421  1012  apply (rule Un_upper2 [THEN mono])  wenzelm@12897  1013  done  wenzelm@12897  1014 wenzelm@13421  1015 lemma mono_Int: includes mono shows "f (A \ B) \ f A \ f B"  wenzelm@12897  1016  apply (rule Int_greatest)  wenzelm@13421  1017  apply (rule Int_lower1 [THEN mono])  wenzelm@13421  1018  apply (rule Int_lower2 [THEN mono])  wenzelm@12897  1019  done  wenzelm@12897  1020 wenzelm@12897  1021 wenzelm@12897  1022 subsubsection {* Equalities involving union, intersection, inclusion, etc. *}  wenzelm@12897  1023 wenzelm@12897  1024 text {* @{text "{}"}. *}  wenzelm@12897  1025 wenzelm@12897  1026 lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"  wenzelm@12897  1027  -- {* supersedes @{text "Collect_False_empty"} *}  wenzelm@12897  1028  by auto  wenzelm@12897  1029 wenzelm@12897  1030 lemma subset_empty [simp]: "(A \ {}) = (A = {})"  wenzelm@12897  1031  by blast  wenzelm@12897  1032 wenzelm@12897  1033 lemma not_psubset_empty [iff]: "\ (A < {})"  wenzelm@12897  1034  by (unfold psubset_def) blast  wenzelm@12897  1035 wenzelm@12897  1036 lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\x. \ P x)"  wenzelm@12897  1037  by auto  wenzelm@12897  1038 wenzelm@12897  1039 lemma Collect_neg_eq: "{x. \ P x} = - {x. P x}"  wenzelm@12897  1040  by blast  wenzelm@12897  1041 wenzelm@12897  1042 lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \ {x. Q x}"  wenzelm@12897  1043  by blast  wenzelm@12897  1044 wenzelm@12897  1045 lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \ {x. Q x}"  wenzelm@12897  1046  by blast  wenzelm@12897  1047 wenzelm@12897  1048 lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})"  wenzelm@12897  1049  by blast  wenzelm@12897  1050 wenzelm@12897  1051 lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  wenzelm@12897  1052  by blast  wenzelm@12897  1053 wenzelm@12897  1054 lemma Collect_ex_eq: "{x. \y. P x y} = (\y. {x. P x y})"  wenzelm@12897  1055  by blast  wenzelm@12897  1056 wenzelm@12897  1057 lemma Collect_bex_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  wenzelm@12897  1058  by blast  wenzelm@12897  1059 wenzelm@12897  1060 wenzelm@12897  1061 text {* \medskip @{text insert}. *}  wenzelm@12897  1062 wenzelm@12897  1063 lemma insert_is_Un: "insert a A = {a} Un A"  wenzelm@12897  1064  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}  wenzelm@12897  1065  by blast  wenzelm@12897  1066 wenzelm@12897  1067 lemma insert_not_empty [simp]: "insert a A \ {}"  wenzelm@12897  1068  by blast  wenzelm@12897  1069 wenzelm@12897  1070 lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard]  wenzelm@12897  1071 wenzelm@12897  1072 lemma insert_absorb: "a \ A ==> insert a A = A"  wenzelm@12897  1073  -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}  wenzelm@12897  1074  -- {* with \emph{quadratic} running time *}  wenzelm@12897  1075  by blast  wenzelm@12897  1076 wenzelm@12897  1077 lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"  wenzelm@12897  1078  by blast  wenzelm@12897  1079 wenzelm@12897  1080 lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"  wenzelm@12897  1081  by blast  wenzelm@12897  1082 wenzelm@12897  1083 lemma insert_subset [simp]: "(insert x A \ B) = (x \ B & A \ B)"  wenzelm@12897  1084  by blast  wenzelm@12897  1085 wenzelm@12897  1086 lemma mk_disjoint_insert: "a \ A ==> \B. A = insert a B & a \ B"  wenzelm@12897  1087  -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}  paulson@14208  1088  apply (rule_tac x = "A - {a}" in exI, blast)  wenzelm@12897  1089  done  wenzelm@12897  1090 wenzelm@12897  1091 lemma insert_Collect: "insert a (Collect P) = {u. u \ a --> P u}"  wenzelm@12897  1092  by auto  wenzelm@12897  1093 wenzelm@12897  1094 lemma UN_insert_distrib: "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)"  wenzelm@12897  1095  by blast  wenzelm@12897  1096 nipkow@14302  1097 lemma insert_inter_insert[simp]: "insert a A \ insert a B = insert a (A \ B)"  mehta@14742  1098  by blast  nipkow@14302  1099 nipkow@13103  1100 lemma insert_disjoint[simp]:  nipkow@13103  1101  "(insert a A \ B = {}) = (a \ B \ A \ B = {})"  mehta@14742  1102  "({} = insert a A \ B) = (a \ B \ {} = A \ B)"  mehta@14742  1103 by auto  nipkow@13103  1104 nipkow@13103  1105 lemma disjoint_insert[simp]:  nipkow@13103  1106  "(B \ insert a A = {}) = (a \ B \ B \ A = {})"  mehta@14742  1107  "({} = A \ insert b B) = (b \ A \ {} = A \ B)"  mehta@14742  1108 by auto  mehta@14742  1109 mehta@14742  1110 lemma disjoint_int_union[simp]:  mehta@14742  1111  "({} = A \ (B \ C)) = ({} = A \ B \ {} = A \ C)"  nipkow@13103  1112 by blast  wenzelm@12897  1113 wenzelm@12897  1114 text {* \medskip @{text image}. *}  wenzelm@12897  1115 wenzelm@12897  1116 lemma image_empty [simp]: "f{} = {}"  wenzelm@12897  1117  by blast  wenzelm@12897  1118 wenzelm@12897  1119 lemma image_insert [simp]: "f  insert a B = insert (f a) (fB)"  wenzelm@12897  1120  by blast  wenzelm@12897  1121 wenzelm@12897  1122 lemma image_constant: "x \ A ==> (\x. c)  A = {c}"  wenzelm@12897  1123  by blast  wenzelm@12897  1124 wenzelm@12897  1125 lemma image_image: "f  (g  A) = (\x. f (g x))  A"  wenzelm@12897  1126  by blast  wenzelm@12897  1127 wenzelm@12897  1128 lemma insert_image [simp]: "x \ A ==> insert (f x) (fA) = fA"  wenzelm@12897  1129  by blast  wenzelm@12897  1130 wenzelm@12897  1131 lemma image_is_empty [iff]: "(fA = {}) = (A = {})"  wenzelm@12897  1132  by blast  wenzelm@12897  1133 wenzelm@12897  1134 lemma image_Collect: "f  {x. P x} = {f x | x. P x}"  wenzelm@12897  1135  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *}  wenzelm@12897  1136  -- {* with its implicit quantifier and conjunction. Also image enjoys better *}  wenzelm@12897  1137  -- {* equational properties than does the RHS. *}  wenzelm@12897  1138  by blast  wenzelm@12897  1139 wenzelm@12897  1140 lemma if_image_distrib [simp]:  wenzelm@12897  1141  "(\x. if P x then f x else g x)  S  wenzelm@12897  1142  = (f  (S \ {x. P x})) \ (g  (S \ {x. \ P x}))"  wenzelm@12897  1143  by (auto simp add: image_def)  wenzelm@12897  1144 wenzelm@12897  1145 lemma image_cong: "M = N ==> (!!x. x \ N ==> f x = g x) ==> fM = gN"  wenzelm@12897  1146  by (simp add: image_def)  wenzelm@12897  1147 wenzelm@12897  1148 wenzelm@12897  1149 text {* \medskip @{text range}. *}  wenzelm@12897  1150 wenzelm@12897  1151 lemma full_SetCompr_eq: "{u. \x. u = f x} = range f"  wenzelm@12897  1152  by auto  wenzelm@12897  1153 wenzelm@12897  1154 lemma range_composition [simp]: "range (\x. f (g x)) = frange g"  paulson@14208  1155 by (subst image_image, simp)  wenzelm@12897  1156 wenzelm@12897  1157 wenzelm@12897  1158 text {* \medskip @{text Int} *}  wenzelm@12897  1159 wenzelm@12897  1160 lemma Int_absorb [simp]: "A \ A = A"  wenzelm@12897  1161  by blast  wenzelm@12897  1162 wenzelm@12897  1163 lemma Int_left_absorb: "A \ (A \ B) = A \ B"  wenzelm@12897  1164  by blast  wenzelm@12897  1165 wenzelm@12897  1166 lemma Int_commute: "A \ B = B \ A"  wenzelm@12897  1167  by blast  wenzelm@12897  1168 wenzelm@12897  1169 lemma Int_left_commute: "A \ (B \ C) = B \ (A \ C)"  wenzelm@12897  1170  by blast  wenzelm@12897  1171 wenzelm@12897  1172 lemma Int_assoc: "(A \ B) \ C = A \ (B \ C)"  wenzelm@12897  1173  by blast  wenzelm@12897  1174 wenzelm@12897  1175 lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute  wenzelm@12897  1176  -- {* Intersection is an AC-operator *}  wenzelm@12897  1177 wenzelm@12897  1178 lemma Int_absorb1: "B \ A ==> A \ B = B"  wenzelm@12897  1179  by blast  wenzelm@12897  1180 wenzelm@12897  1181 lemma Int_absorb2: "A \ B ==> A \ B = A"  wenzelm@12897  1182  by blast  wenzelm@12897  1183 wenzelm@12897  1184 lemma Int_empty_left [simp]: "{} \ B = {}"  wenzelm@12897  1185  by blast  wenzelm@12897  1186 wenzelm@12897  1187 lemma Int_empty_right [simp]: "A \ {} = {}"  wenzelm@12897  1188  by blast  wenzelm@12897  1189 wenzelm@12897  1190 lemma disjoint_eq_subset_Compl: "(A \ B = {}) = (A \ -B)"  wenzelm@12897  1191  by blast  wenzelm@12897  1192 wenzelm@12897  1193 lemma disjoint_iff_not_equal: "(A \ B = {}) = (\x\A. \y\B. x \ y)"  wenzelm@12897  1194  by blast  wenzelm@12897  1195 wenzelm@12897  1196 lemma Int_UNIV_left [simp]: "UNIV \ B = B"  wenzelm@12897  1197  by blast  wenzelm@12897  1198 wenzelm@12897  1199 lemma Int_UNIV_right [simp]: "A \ UNIV = A"  wenzelm@12897  1200  by blast  wenzelm@12897  1201 wenzelm@12897  1202 lemma Int_eq_Inter: "A \ B = \{A, B}"  wenzelm@12897  1203  by blast  wenzelm@12897  1204 wenzelm@12897  1205 lemma Int_Un_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)"  wenzelm@12897  1206  by blast  wenzelm@12897  1207 wenzelm@12897  1208 lemma Int_Un_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)"  wenzelm@12897  1209  by blast  wenzelm@12897  1210 wenzelm@12897  1211 lemma Int_UNIV [simp]: "(A \ B = UNIV) = (A = UNIV & B = UNIV)"  wenzelm@12897  1212  by blast  wenzelm@12897  1213 wenzelm@12897  1214 lemma Int_subset_iff: "(C \ A \ B) = (C \ A & C \ B)"  wenzelm@12897  1215  by blast  wenzelm@12897  1216 wenzelm@12897  1217 lemma Int_Collect: "(x \ A \ {x. P x}) = (x \ A & P x)"  wenzelm@12897  1218  by blast  wenzelm@12897  1219 wenzelm@12897  1220 wenzelm@12897  1221 text {* \medskip @{text Un}. *}  wenzelm@12897  1222 wenzelm@12897  1223 lemma Un_absorb [simp]: "A \ A = A"  wenzelm@12897  1224  by blast  wenzelm@12897  1225 wenzelm@12897  1226 lemma Un_left_absorb: "A \ (A \ B) = A \ B"  wenzelm@12897  1227  by blast  wenzelm@12897  1228 wenzelm@12897  1229 lemma Un_commute: "A \ B = B \ A"  wenzelm@12897  1230  by blast  wenzelm@12897  1231 wenzelm@12897  1232 lemma Un_left_commute: "A \ (B \ C) = B \ (A \ C)"  wenzelm@12897  1233  by blast  wenzelm@12897  1234 wenzelm@12897  1235 lemma Un_assoc: "(A \ B) \ C = A \ (B \ C)"  wenzelm@12897  1236  by blast  wenzelm@12897  1237 wenzelm@12897  1238 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute  wenzelm@12897  1239  -- {* Union is an AC-operator *}  wenzelm@12897  1240 wenzelm@12897  1241 lemma Un_absorb1: "A \ B ==> A \ B = B"  wenzelm@12897  1242  by blast  wenzelm@12897  1243 wenzelm@12897  1244 lemma Un_absorb2: "B \ A ==> A \ B = A"  wenzelm@12897  1245  by blast  wenzelm@12897  1246 wenzelm@12897  1247 lemma Un_empty_left [simp]: "{} \ B = B"  wenzelm@12897  1248  by blast  wenzelm@12897  1249 wenzelm@12897  1250 lemma Un_empty_right [simp]: "A \ {} = A"  wenzelm@12897  1251  by blast  wenzelm@12897  1252 wenzelm@12897  1253 lemma Un_UNIV_left [simp]: "UNIV \ B = UNIV"  wenzelm@12897  1254  by blast  wenzelm@12897  1255 wenzelm@12897  1256 lemma Un_UNIV_right [simp]: "A \ UNIV = UNIV"  wenzelm@12897  1257  by blast  wenzelm@12897  1258 wenzelm@12897  1259 lemma Un_eq_Union: "A \ B = \{A, B}"  wenzelm@12897  1260  by blast  wenzelm@12897  1261 wenzelm@12897  1262 lemma Un_insert_left [simp]: "(insert a B) \ C = insert a (B \ C)"  wenzelm@12897  1263  by blast  wenzelm@12897  1264 wenzelm@12897  1265 lemma Un_insert_right [simp]: "A \ (insert a B) = insert a (A \ B)"  wenzelm@12897  1266  by blast  wenzelm@12897  1267 wenzelm@12897  1268 lemma Int_insert_left:  wenzelm@12897  1269  "(insert a B) Int C = (if a \ C then insert a (B \ C) else B \ C)"  wenzelm@12897  1270  by auto  wenzelm@12897  1271 wenzelm@12897  1272 lemma Int_insert_right:  wenzelm@12897  1273  "A \ (insert a B) = (if a \ A then insert a (A \ B) else A \ B)"  wenzelm@12897  1274  by auto  wenzelm@12897  1275 wenzelm@12897  1276 lemma Un_Int_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)"  wenzelm@12897  1277  by blast  wenzelm@12897  1278 wenzelm@12897  1279 lemma Un_Int_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)"  wenzelm@12897  1280  by blast  wenzelm@12897  1281 wenzelm@12897  1282 lemma Un_Int_crazy:  wenzelm@12897  1283  "(A \ B) \ (B \ C) \ (C \ A) = (A \ B) \ (B \ C) \ (C \ A)"  wenzelm@12897  1284  by blast  wenzelm@12897  1285 wenzelm@12897  1286 lemma subset_Un_eq: "(A \ B) = (A \ B = B)"  wenzelm@12897  1287  by blast  wenzelm@12897  1288 wenzelm@12897  1289 lemma Un_empty [iff]: "(A \ B = {}) = (A = {} & B = {})"  wenzelm@12897  1290  by blast  wenzelm@12897  1291 wenzelm@12897  1292 lemma Un_subset_iff: "(A \ B \ C) = (A \ C & B \ C)"  wenzelm@12897  1293  by blast  wenzelm@12897  1294 wenzelm@12897  1295 lemma Un_Diff_Int: "(A - B) \ (A \ B) = A"  wenzelm@12897  1296  by blast  wenzelm@12897  1297 wenzelm@12897  1298 wenzelm@12897  1299 text {* \medskip Set complement *}  wenzelm@12897  1300 wenzelm@12897  1301 lemma Compl_disjoint [simp]: "A \ -A = {}"  wenzelm@12897  1302  by blast  wenzelm@12897  1303 wenzelm@12897  1304 lemma Compl_disjoint2 [simp]: "-A \ A = {}"  wenzelm@12897  1305  by blast  wenzelm@12897  1306 paulson@13818  1307 lemma Compl_partition: "A \ -A = UNIV"  paulson@13818  1308  by blast  paulson@13818  1309 paulson@13818  1310 lemma Compl_partition2: "-A \ A = UNIV"  wenzelm@12897  1311  by blast  wenzelm@12897  1312 wenzelm@12897  1313 lemma double_complement [simp]: "- (-A) = (A::'a set)"  wenzelm@12897  1314  by blast  wenzelm@12897  1315 wenzelm@12897  1316 lemma Compl_Un [simp]: "-(A \ B) = (-A) \ (-B)"  wenzelm@12897  1317  by blast  wenzelm@12897  1318 wenzelm@12897  1319 lemma Compl_Int [simp]: "-(A \ B) = (-A) \ (-B)"  wenzelm@12897  1320  by blast  wenzelm@12897  1321 wenzelm@12897  1322 lemma Compl_UN [simp]: "-(\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  1323  by blast  wenzelm@12897  1324 wenzelm@12897  1325 lemma Compl_INT [simp]: "-(\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  1326  by blast  wenzelm@12897  1327 wenzelm@12897  1328 lemma subset_Compl_self_eq: "(A \ -A) = (A = {})"  wenzelm@12897  1329  by blast  wenzelm@12897  1330 wenzelm@12897  1331 lemma Un_Int_assoc_eq: "((A \ B) \ C = A \ (B \ C)) = (C \ A)"  wenzelm@12897  1332  -- {* Halmos, Naive Set Theory, page 16. *}  wenzelm@12897  1333  by blast  wenzelm@12897  1334 wenzelm@12897  1335 lemma Compl_UNIV_eq [simp]: "-UNIV = {}"  wenzelm@12897  1336  by blast  wenzelm@12897  1337 wenzelm@12897  1338 lemma Compl_empty_eq [simp]: "-{} = UNIV"  wenzelm@12897  1339  by blast  wenzelm@12897  1340 wenzelm@12897  1341 lemma Compl_subset_Compl_iff [iff]: "(-A \ -B) = (B \ A)"  wenzelm@12897  1342  by blast  wenzelm@12897  1343 wenzelm@12897  1344 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"  wenzelm@12897  1345  by blast  wenzelm@12897  1346 wenzelm@12897  1347 wenzelm@12897  1348 text {* \medskip @{text Union}. *}  wenzelm@12897  1349 wenzelm@12897  1350 lemma Union_empty [simp]: "Union({}) = {}"  wenzelm@12897  1351  by blast  wenzelm@12897  1352 wenzelm@12897  1353 lemma Union_UNIV [simp]: "Union UNIV = UNIV"  wenzelm@12897  1354  by blast  wenzelm@12897  1355 wenzelm@12897  1356 lemma Union_insert [simp]: "Union (insert a B) = a \ \B"  wenzelm@12897  1357  by blast  wenzelm@12897  1358 wenzelm@12897  1359 lemma Union_Un_distrib [simp]: "\(A Un B) = \A \ \B"  wenzelm@12897  1360  by blast  wenzelm@12897  1361 wenzelm@12897  1362 lemma Union_Int_subset: "\(A \ B) \ \A \ \B"  wenzelm@12897  1363  by blast  wenzelm@12897  1364 wenzelm@12897  1365 lemma Union_empty_conv [iff]: "(\A = {}) = (\x\A. x = {})"  nipkow@13653  1366  by blast  nipkow@13653  1367 nipkow@13653  1368 lemma empty_Union_conv [iff]: "({} = \A) = (\x\A. x = {})"  nipkow@13653  1369  by blast  wenzelm@12897  1370 wenzelm@12897  1371 lemma Union_disjoint: "(\C \ A = {}) = (\B\C. B \ A = {})"  wenzelm@12897  1372  by blast  wenzelm@12897  1373 wenzelm@12897  1374 wenzelm@12897  1375 text {* \medskip @{text Inter}. *}  wenzelm@12897  1376 wenzelm@12897  1377 lemma Inter_empty [simp]: "\{} = UNIV"  wenzelm@12897  1378  by blast  wenzelm@12897  1379 wenzelm@12897  1380 lemma Inter_UNIV [simp]: "\UNIV = {}"  wenzelm@12897  1381  by blast  wenzelm@12897  1382 wenzelm@12897  1383 lemma Inter_insert [simp]: "\(insert a B) = a \ \B"  wenzelm@12897  1384  by blast  wenzelm@12897  1385 wenzelm@12897  1386 lemma Inter_Un_subset: "\A \ \B \ \(A \ B)"  wenzelm@12897  1387  by blast  wenzelm@12897  1388 wenzelm@12897  1389 lemma Inter_Un_distrib: "\(A \ B) = \A \ \B"  wenzelm@12897  1390  by blast  wenzelm@12897  1391 nipkow@13653  1392 lemma Inter_UNIV_conv [iff]:  nipkow@13653  1393  "(\A = UNIV) = (\x\A. x = UNIV)"  nipkow@13653  1394  "(UNIV = \A) = (\x\A. x = UNIV)"  paulson@14208  1395  by blast+  nipkow@13653  1396 wenzelm@12897  1397 wenzelm@12897  1398 text {*  wenzelm@12897  1399  \medskip @{text UN} and @{text INT}.  wenzelm@12897  1400 wenzelm@12897  1401  Basic identities: *}  wenzelm@12897  1402 wenzelm@12897  1403 lemma UN_empty [simp]: "(\x\{}. B x) = {}"  wenzelm@12897  1404  by blast  wenzelm@12897  1405 wenzelm@12897  1406 lemma UN_empty2 [simp]: "(\x\A. {}) = {}"  wenzelm@12897  1407  by blast  wenzelm@12897  1408 wenzelm@12897  1409 lemma UN_singleton [simp]: "(\x\A. {x}) = A"  wenzelm@12897  1410  by blast  wenzelm@12897  1411 wenzelm@12897  1412 lemma UN_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)"  wenzelm@12897  1413  by blast  wenzelm@12897  1414 wenzelm@12897  1415 lemma INT_empty [simp]: "(\x\{}. B x) = UNIV"  wenzelm@12897  1416  by blast  wenzelm@12897  1417 wenzelm@12897  1418 lemma INT_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)"  wenzelm@12897  1419  by blast  wenzelm@12897  1420 wenzelm@12897  1421 lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ UNION A B"  wenzelm@12897  1422  by blast  wenzelm@12897  1423 wenzelm@12897  1424 lemma UN_Un: "(\i \ A \ B. M i) = (\i\A. M i) \ (\i\B. M i)"  wenzelm@12897  1425  by blast  wenzelm@12897  1426 wenzelm@12897  1427 lemma UN_UN_flatten: "(\x \ (\y\A. B y). C x) = (\y\A. \x\B y. C x)"  wenzelm@12897  1428  by blast  wenzelm@12897  1429 wenzelm@12897  1430 lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)"  wenzelm@12897  1431  by blast  wenzelm@12897  1432 wenzelm@12897  1433 lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)"  wenzelm@12897  1434  by blast  wenzelm@12897  1435 wenzelm@12897  1436 lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B"  wenzelm@12897  1437  by blast  wenzelm@12897  1438 wenzelm@12897  1439 lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"  wenzelm@12897  1440  by blast  wenzelm@12897  1441 wenzelm@12897  1442 lemma INT_insert_distrib:  wenzelm@12897  1443  "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)"  wenzelm@12897  1444  by blast  wenzelm@12897  1445 wenzelm@12897  1446 lemma Union_image_eq [simp]: "\(BA) = (\x\A. B x)"  wenzelm@12897  1447  by blast  wenzelm@12897  1448 wenzelm@12897  1449 lemma image_Union: "f  \S = (\x\S. f  x)"  wenzelm@12897  1450  by blast  wenzelm@12897  1451 wenzelm@12897  1452 lemma Inter_image_eq [simp]: "\(BA) = (\x\A. B x)"  wenzelm@12897  1453  by blast  wenzelm@12897  1454 wenzelm@12897  1455 lemma UN_constant [simp]: "(\y\A. c) = (if A = {} then {} else c)"  wenzelm@12897  1456  by auto  wenzelm@12897  1457 wenzelm@12897  1458 lemma INT_constant [simp]: "(\y\A. c) = (if A = {} then UNIV else c)"  wenzelm@12897  1459  by auto  wenzelm@12897  1460 wenzelm@12897  1461 lemma UN_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  wenzelm@12897  1462  by blast  wenzelm@12897  1463 wenzelm@12897  1464 lemma INT_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  wenzelm@12897  1465  -- {* Look: it has an \emph{existential} quantifier *}  wenzelm@12897  1466  by blast  wenzelm@12897  1467 nipkow@13653  1468 lemma UNION_empty_conv[iff]:  nipkow@13653  1469  "({} = (UN x:A. B x)) = (\x\A. B x = {})"  nipkow@13653  1470  "((UN x:A. B x) = {}) = (\x\A. B x = {})"  nipkow@13653  1471 by blast+  nipkow@13653  1472 nipkow@13653  1473 lemma INTER_UNIV_conv[iff]:  nipkow@13653  1474  "(UNIV = (INT x:A. B x)) = (\x\A. B x = UNIV)"  nipkow@13653  1475  "((INT x:A. B x) = UNIV) = (\x\A. B x = UNIV)"  nipkow@13653  1476 by blast+  wenzelm@12897  1477 wenzelm@12897  1478 wenzelm@12897  1479 text {* \medskip Distributive laws: *}  wenzelm@12897  1480 wenzelm@12897  1481 lemma Int_Union: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  1482  by blast  wenzelm@12897  1483 wenzelm@12897  1484 lemma Int_Union2: "\B \ A = (\C\B. C \ A)"  wenzelm@12897  1485  by blast  wenzelm@12897  1486 wenzelm@12897  1487 lemma Un_Union_image: "(\x\C. A x \ B x) = \(AC) \ \(BC)"  wenzelm@12897  1488  -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}  wenzelm@12897  1489  -- {* Union of a family of unions *}  wenzelm@12897  1490  by blast  wenzelm@12897  1491 wenzelm@12897  1492 lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  1493  -- {* Equivalent version *}  wenzelm@12897  1494  by blast  wenzelm@12897  1495 wenzelm@12897  1496 lemma Un_Inter: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  1497  by blast  wenzelm@12897  1498 wenzelm@12897  1499 lemma Int_Inter_image: "(\x\C. A x \ B x) = \(AC) \ \(BC)"  wenzelm@12897  1500  by blast  wenzelm@12897  1501 wenzelm@12897  1502 lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  1503  -- {* Equivalent version *}  wenzelm@12897  1504  by blast  wenzelm@12897  1505 wenzelm@12897  1506 lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  1507  -- {* Halmos, Naive Set Theory, page 35. *}  wenzelm@12897  1508  by blast  wenzelm@12897  1509 wenzelm@12897  1510 lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  1511  by blast  wenzelm@12897  1512 wenzelm@12897  1513 lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  1514  by blast  wenzelm@12897  1515 wenzelm@12897  1516 lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  1517  by blast  wenzelm@12897  1518 wenzelm@12897  1519 wenzelm@12897  1520 text {* \medskip Bounded quantifiers.  wenzelm@12897  1521 wenzelm@12897  1522  The following are not added to the default simpset because  wenzelm@12897  1523  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}  wenzelm@12897  1524 wenzelm@12897  1525 lemma ball_Un: "(\x \ A \ B. P x) = ((\x\A. P x) & (\x\B. P x))"  wenzelm@12897  1526  by blast  wenzelm@12897  1527 wenzelm@12897  1528 lemma bex_Un: "(\x \ A \ B. P x) = ((\x\A. P x) | (\x\B. P x))"  wenzelm@12897  1529  by blast  wenzelm@12897  1530 wenzelm@12897  1531 lemma ball_UN: "(\z \ UNION A B. P z) = (\x\A. \z \ B x. P z)"  wenzelm@12897  1532  by blast  wenzelm@12897  1533 wenzelm@12897  1534 lemma bex_UN: "(\z \ UNION A B. P z) = (\x\A. \z\B x. P z)"  wenzelm@12897  1535  by blast  wenzelm@12897  1536 wenzelm@12897  1537 wenzelm@12897  1538 text {* \medskip Set difference. *}  wenzelm@12897  1539 wenzelm@12897  1540 lemma Diff_eq: "A - B = A \ (-B)"  wenzelm@12897  1541  by blast  wenzelm@12897  1542 wenzelm@12897  1543 lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \ B)"  wenzelm@12897  1544  by blast  wenzelm@12897  1545 wenzelm@12897  1546 lemma Diff_cancel [simp]: "A - A = {}"  wenzelm@12897  1547  by blast  wenzelm@12897  1548 nipkow@14302  1549 lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"  nipkow@14302  1550 by blast  nipkow@14302  1551 wenzelm@12897  1552 lemma Diff_triv: "A \ B = {} ==> A - B = A"  wenzelm@12897  1553  by (blast elim: equalityE)  wenzelm@12897  1554 wenzelm@12897  1555 lemma empty_Diff [simp]: "{} - A = {}"  wenzelm@12897  1556  by blast  wenzelm@12897  1557 wenzelm@12897  1558 lemma Diff_empty [simp]: "A - {} = A"  wenzelm@12897  1559  by blast  wenzelm@12897  1560 wenzelm@12897  1561 lemma Diff_UNIV [simp]: "A - UNIV = {}"  wenzelm@12897  1562  by blast  wenzelm@12897  1563 wenzelm@12897  1564 lemma Diff_insert0 [simp]: "x \ A ==> A - insert x B = A - B"  wenzelm@12897  1565  by blast  wenzelm@12897  1566 wenzelm@12897  1567 lemma Diff_insert: "A - insert a B = A - B - {a}"  wenzelm@12897  1568  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}  wenzelm@12897  1569  by blast  wenzelm@12897  1570 wenzelm@12897  1571 lemma Diff_insert2: "A - insert a B = A - {a} - B"  wenzelm@12897  1572  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}  wenzelm@12897  1573  by blast  wenzelm@12897  1574 wenzelm@12897  1575 lemma insert_Diff_if: "insert x A - B = (if x \ B then A - B else insert x (A - B))"  wenzelm@12897  1576  by auto  wenzelm@12897  1577 wenzelm@12897  1578 lemma insert_Diff1 [simp]: "x \ B ==> insert x A - B = A - B"  wenzelm@12897  1579  by blast  wenzelm@12897  1580 nipkow@14302  1581 lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"  nipkow@14302  1582 by blast  nipkow@14302  1583 wenzelm@12897  1584 lemma insert_Diff: "a \ A ==> insert a (A - {a}) = A"  wenzelm@12897  1585  by blast  wenzelm@12897  1586 wenzelm@12897  1587 lemma Diff_insert_absorb: "x \ A ==> (insert x A) - {x} = A"  wenzelm@12897  1588  by auto  wenzelm@12897  1589 wenzelm@12897  1590 lemma Diff_disjoint [simp]: "A \ (B - A) = {}"  wenzelm@12897  1591  by blast  wenzelm@12897  1592 wenzelm@12897  1593 lemma Diff_partition: "A \ B ==> A \ (B - A) = B"  wenzelm@12897  1594  by blast  wenzelm@12897  1595 wenzelm@12897  1596 lemma double_diff: "A \ B ==> B \ C ==> B - (C - A) = A"  wenzelm@12897  1597  by blast  wenzelm@12897  1598 wenzelm@12897  1599 lemma Un_Diff_cancel [simp]: "A \ (B - A) = A \ B"  wenzelm@12897  1600  by blast  wenzelm@12897  1601 wenzelm@12897  1602 lemma Un_Diff_cancel2 [simp]: "(B - A) \ A = B \ A"  wenzelm@12897  1603  by blast  wenzelm@12897  1604 wenzelm@12897  1605 lemma Diff_Un: "A - (B \ C) = (A - B) \ (A - C)"  wenzelm@12897  1606  by blast  wenzelm@12897  1607 wenzelm@12897  1608 lemma Diff_Int: "A - (B \ C) = (A - B) \ (A - C)"  wenzelm@12897  1609  by blast  wenzelm@12897  1610 wenzelm@12897  1611 lemma Un_Diff: "(A \ B) - C = (A - C) \ (B - C)"  wenzelm@12897  1612  by blast  wenzelm@12897  1613 wenzelm@12897  1614 lemma Int_Diff: "(A \ B) - C = A \ (B - C)"  wenzelm@12897  1615  by blast  wenzelm@12897  1616 wenzelm@12897  1617 lemma Diff_Int_distrib: "C \ (A - B) = (C \ A) - (C \ B)"  wenzelm@12897  1618  by blast  wenzelm@12897  1619 wenzelm@12897  1620 lemma Diff_Int_distrib2: "(A - B) \ C = (A \ C) - (B \ C)"  wenzelm@12897  1621  by blast  wenzelm@12897  1622 wenzelm@12897  1623 lemma Diff_Compl [simp]: "A - (- B) = A \ B"  wenzelm@12897  1624  by auto  wenzelm@12897  1625 wenzelm@12897  1626 lemma Compl_Diff_eq [simp]: "- (A - B) = -A \ B"  wenzelm@12897  1627  by blast  wenzelm@12897  1628 wenzelm@12897  1629 wenzelm@12897  1630 text {* \medskip Quantification over type @{typ bool}. *}  wenzelm@12897  1631 wenzelm@12897  1632 lemma all_bool_eq: "(\b::bool. P b) = (P True & P False)"  wenzelm@12897  1633  apply auto  paulson@14208  1634  apply (tactic {* case_tac "b" 1 *}, auto)  wenzelm@12897  1635  done  wenzelm@12897  1636 wenzelm@12897  1637 lemma bool_induct: "P True \ P False \ P x"  wenzelm@12897  1638  by (rule conjI [THEN all_bool_eq [THEN iffD2], THEN spec])  wenzelm@12897  1639 wenzelm@12897  1640 lemma ex_bool_eq: "(\b::bool. P b) = (P True | P False)"  wenzelm@12897  1641  apply auto  paulson@14208  1642  apply (tactic {* case_tac "b" 1 *}, auto)  wenzelm@12897  1643  done  wenzelm@12897  1644 wenzelm@12897  1645 lemma Un_eq_UN: "A \ B = (\b. if b then A else B)"  wenzelm@12897  1646  by (auto simp add: split_if_mem2)  wenzelm@12897  1647 wenzelm@12897  1648 lemma UN_bool_eq: "(\b::bool. A b) = (A True \ A False)"  wenzelm@12897  1649  apply auto  paulson@14208  1650  apply (tactic {* case_tac "b" 1 *}, auto)  wenzelm@12897  1651  done  wenzelm@12897  1652 wenzelm@12897  1653 lemma INT_bool_eq: "(\b::bool. A b) = (A True \ A False)"  wenzelm@12897  1654  apply auto  paulson@14208  1655  apply (tactic {* case_tac "b" 1 *}, auto)  wenzelm@12897  1656  done  wenzelm@12897  1657 wenzelm@12897  1658 wenzelm@12897  1659 text {* \medskip @{text Pow} *}  wenzelm@12897  1660 wenzelm@12897  1661 lemma Pow_empty [simp]: "Pow {} = {{}}"  wenzelm@12897  1662  by (auto simp add: Pow_def)  wenzelm@12897  1663 wenzelm@12897  1664 lemma Pow_insert: "Pow (insert a A) = Pow A \ (insert a  Pow A)"  wenzelm@12897  1665  by (blast intro: image_eqI [where ?x = "u - {a}", standard])  wenzelm@12897  1666 wenzelm@12897  1667 lemma Pow_Compl: "Pow (- A) = {-B | B. A \ Pow B}"  wenzelm@12897  1668  by (blast intro: exI [where ?x = "- u", standard])  wenzelm@12897  1669 wenzelm@12897  1670 lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"  wenzelm@12897  1671  by blast  wenzelm@12897  1672 wenzelm@12897  1673 lemma Un_Pow_subset: "Pow A \ Pow B \ Pow (A \ B)"  wenzelm@12897  1674  by blast  wenzelm@12897  1675 wenzelm@12897  1676 lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)"  wenzelm@12897  1677  by blast  wenzelm@12897  1678 wenzelm@12897  1679 lemma subset_Pow_Union: "A \ Pow (\A)"  wenzelm@12897  1680  by blast  wenzelm@12897  1681 wenzelm@12897  1682 lemma Union_Pow_eq [simp]: "\(Pow A) = A"  wenzelm@12897  1683  by blast  wenzelm@12897  1684 wenzelm@12897  1685 lemma Pow_Int_eq [simp]: "Pow (A \ B) = Pow A \ Pow B"  wenzelm@12897  1686  by blast  wenzelm@12897  1687 wenzelm@12897  1688 lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))"  wenzelm@12897  1689  by blast  wenzelm@12897  1690 wenzelm@12897  1691 wenzelm@12897  1692 text {* \medskip Miscellany. *}  wenzelm@12897  1693 wenzelm@12897  1694 lemma set_eq_subset: "(A = B) = (A \ B & B \ A)"  wenzelm@12897  1695  by blast  wenzelm@12897  1696 wenzelm@12897  1697 lemma subset_iff: "(A \ B) = (\t. t \ A --> t \ B)"  wenzelm@12897  1698  by blast  wenzelm@12897  1699 wenzelm@12897  1700 lemma subset_iff_psubset_eq: "(A \ B) = ((A \ B) | (A = B))"  wenzelm@12897  1701  by (unfold psubset_def) blast  wenzelm@12897  1702 wenzelm@12897  1703 lemma all_not_in_conv [iff]: "(\x. x \ A) = (A = {})"  wenzelm@12897  1704  by blast  wenzelm@12897  1705 paulson@13831  1706 lemma ex_in_conv: "(\x. x \ A) = (A \ {})"  paulson@13831  1707  by blast  paulson@13831  1708 wenzelm@12897  1709 lemma distinct_lemma: "f x \ f y ==> x \ y"  wenzelm@12897  1710  by rules  wenzelm@12897  1711 wenzelm@12897  1712 paulson@13860  1713 text {* \medskip Miniscoping: pushing in quantifiers and big Unions  paulson@13860  1714  and Intersections. *}  wenzelm@12897  1715 wenzelm@12897  1716 lemma UN_simps [simp]:  wenzelm@12897  1717  "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"  wenzelm@12897  1718  "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))"  wenzelm@12897  1719  "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))"  wenzelm@12897  1720  "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)"  wenzelm@12897  1721  "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))"  wenzelm@12897  1722  "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)"  wenzelm@12897  1723  "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))"  wenzelm@12897  1724  "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"  wenzelm@12897  1725  "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)"  wenzelm@12897  1726  "!!A B f. (UN x:fA. B x) = (UN a:A. B (f a))"  wenzelm@12897  1727  by auto  wenzelm@12897  1728 wenzelm@12897  1729 lemma INT_simps [simp]:  wenzelm@12897  1730  "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"  wenzelm@12897  1731  "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"  wenzelm@12897  1732  "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)"  wenzelm@12897  1733  "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))"  wenzelm@12897  1734  "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"  wenzelm@12897  1735  "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)"  wenzelm@12897  1736  "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))"  wenzelm@12897  1737  "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"  wenzelm@12897  1738  "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"  wenzelm@12897  1739  "!!A B f. (INT x:fA. B x) = (INT a:A. B (f a))"  wenzelm@12897  1740  by auto  wenzelm@12897  1741 wenzelm@12897  1742 lemma ball_simps [simp]:  wenzelm@12897  1743  "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"  wenzelm@12897  1744  "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"  wenzelm@12897  1745  "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"  wenzelm@12897  1746  "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"  wenzelm@12897  1747  "!!P. (ALL x:{}. P x) = True"  wenzelm@12897  1748  "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"  wenzelm@12897  1749  "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"  wenzelm@12897  1750  "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"  wenzelm@12897  1751  "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"  wenzelm@12897  1752  "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"  wenzelm@12897  1753  "!!A P f. (ALL x:fA. P x) = (ALL x:A. P (f x))"  wenzelm@12897  1754  "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"  wenzelm@12897  1755  by auto  wenzelm@12897  1756 wenzelm@12897  1757 lemma bex_simps [simp]:  wenzelm@12897  1758  "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"  wenzelm@12897  1759  "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"  wenzelm@12897  1760  "!!P. (EX x:{}. P x) = False"  wenzelm@12897  1761  "!!P. (EX x:UNIV. P x) = (EX x. P x)"  wenzelm@12897  1762  "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"  wenzelm@12897  1763  "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"  wenzelm@12897  1764  "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"  wenzelm@12897  1765  "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"  wenzelm@12897  1766  "!!A P f. (EX x:fA. P x) = (EX x:A. P (f x))"  wenzelm@12897  1767  "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"  wenzelm@12897  1768  by auto  wenzelm@12897  1769 wenzelm@12897  1770 lemma ball_conj_distrib:  wenzelm@12897  1771  "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"  wenzelm@12897  1772  by blast  wenzelm@12897  1773 wenzelm@12897  1774 lemma bex_disj_distrib:  wenzelm@12897  1775  "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"  wenzelm@12897  1776  by blast  wenzelm@12897  1777 wenzelm@12897  1778 paulson@13860  1779 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}  paulson@13860  1780 paulson@13860  1781 lemma UN_extend_simps:  paulson@13860  1782  "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))"  paulson@13860  1783  "!!A B C. (UN x:C. A x) Un B = (if C={} then B else (UN x:C. A x Un B))"  paulson@13860  1784  "!!A B C. A Un (UN x:C. B x) = (if C={} then A else (UN x:C. A Un B x))"  paulson@13860  1785  "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)"  paulson@13860  1786  "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)"  paulson@13860  1787  "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)"  paulson@13860  1788  "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)"  paulson@13860  1789  "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)"  paulson@13860  1790  "!!A B C. (UN x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"  paulson@13860  1791  "!!A B f. (UN a:A. B (f a)) = (UN x:fA. B x)"  paulson@13860  1792  by auto  paulson@13860  1793 paulson@13860  1794 lemma INT_extend_simps:  paulson@13860  1795  "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))"  paulson@13860  1796  "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))"  paulson@13860  1797  "!!A B C. (INT x:C. A x) - B = (if C={} then UNIV-B else (INT x:C. A x - B))"  paulson@13860  1798  "!!A B C. A - (UN x:C. B x) = (if C={} then A else (INT x:C. A - B x))"  paulson@13860  1799  "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))"  paulson@13860  1800  "!!A B C. ((INT x:C. A x) Un B) = (INT x:C. A x Un B)"  paulson@13860  1801  "!!A B C. A Un (INT x:C. B x) = (INT x:C. A Un B x)"  paulson@13860  1802  "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)"  paulson@13860  1803  "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)"  paulson@13860  1804  "!!A B f. (INT a:A. B (f a)) = (INT x:fA. B x)"  paulson@13860  1805  by auto  paulson@13860  1806 paulson@13860  1807 wenzelm@12897  1808 subsubsection {* Monotonicity of various operations *}  wenzelm@12897  1809 wenzelm@12897  1810 lemma image_mono: "A \ B ==> fA \ fB"  wenzelm@12897  1811  by blast  wenzelm@12897  1812 wenzelm@12897  1813 lemma Pow_mono: "A \ B ==> Pow A \ Pow B"  wenzelm@12897  1814  by blast  wenzelm@12897  1815 wenzelm@12897  1816 lemma Union_mono: "A \ B ==> \A \ \B"  wenzelm@12897  1817  by blast  wenzelm@12897  1818 wenzelm@12897  1819 lemma Inter_anti_mono: "B \ A ==> \A \ \B"  wenzelm@12897  1820  by blast  wenzelm@12897  1821 wenzelm@12897  1822 lemma UN_mono:  wenzelm@12897  1823  "A \ B ==> (!!x. x \ A ==> f x \ g x) ==>  wenzelm@12897  1824  (\x\A. f x) \ (\x\B. g x)"  wenzelm@12897  1825  by (blast dest: subsetD)  wenzelm@12897  1826 wenzelm@12897  1827 lemma INT_anti_mono:  wenzelm@12897  1828  "B \ A ==> (!!x. x \ A ==> f x \ g x) ==>  wenzelm@12897  1829  (\x\A. f x) \ (\x\A. g x)"  wenzelm@12897  1830  -- {* The last inclusion is POSITIVE! *}  wenzelm@12897  1831  by (blast dest: subsetD)  wenzelm@12897  1832 wenzelm@12897  1833 lemma insert_mono: "C \ D ==> insert a C \ insert a D"  wenzelm@12897  1834  by blast  wenzelm@12897  1835 wenzelm@12897  1836 lemma Un_mono: "A \ C ==> B \ D ==> A \ B \ C \ D"  wenzelm@12897  1837  by blast  wenzelm@12897  1838 wenzelm@12897  1839 lemma Int_mono: "A \ C ==> B \ D ==> A \ B \ C \ D"  wenzelm@12897  1840  by blast  wenzelm@12897  1841 wenzelm@12897  1842 lemma Diff_mono: "A \ C ==> D \ B ==> A - B \ C - D"  wenzelm@12897  1843  by blast  wenzelm@12897  1844 wenzelm@12897  1845 lemma Compl_anti_mono: "A \ B ==> -B \ -A"  wenzelm@12897  1846  by blast  wenzelm@12897  1847 wenzelm@12897  1848 text {* \medskip Monotonicity of implications. *}  wenzelm@12897  1849 wenzelm@12897  1850 lemma in_mono: "A \ B ==> x \ A --> x \ B"  wenzelm@12897  1851  apply (rule impI)  paulson@14208  1852  apply (erule subsetD, assumption)  wenzelm@12897  1853  done  wenzelm@12897  1854 wenzelm@12897  1855 lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"  wenzelm@12897  1856  by rules  wenzelm@12897  1857 wenzelm@12897  1858 lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"  wenzelm@12897  1859  by rules  wenzelm@12897  1860 wenzelm@12897  1861 lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"  wenzelm@12897  1862  by rules  wenzelm@12897  1863 wenzelm@12897  1864 lemma imp_refl: "P --> P" ..  wenzelm@12897  1865 wenzelm@12897  1866 lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"  wenzelm@12897  1867  by rules  wenzelm@12897  1868 wenzelm@12897  1869 lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"  wenzelm@12897  1870  by rules  wenzelm@12897  1871 wenzelm@12897  1872 lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \ Collect Q"  wenzelm@12897  1873  by blast  wenzelm@12897  1874 wenzelm@12897  1875 lemma Int_Collect_mono:  wenzelm@12897  1876  "A \ B ==> (!!x. x \ A ==> P x --> Q x) ==> A \ Collect P \ B \ Collect Q"  wenzelm@12897  1877  by blast  wenzelm@12897  1878 wenzelm@12897  1879 lemmas basic_monos =  wenzelm@12897  1880  subset_refl imp_refl disj_mono conj_mono  wenzelm@12897  1881  ex_mono Collect_mono in_mono  wenzelm@12897  1882 wenzelm@12897  1883 lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"  wenzelm@12897  1884  by rules  wenzelm@12897  1885 wenzelm@12897  1886 lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"  wenzelm@12897  1887  by rules  wenzelm@11979  1888 wenzelm@11982  1889 lemma Least_mono:  wenzelm@11982  1890  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y  wenzelm@11982  1891  ==> (LEAST y. y : f  S) = f (LEAST x. x : S)"  wenzelm@11982  1892  -- {* Courtesy of Stephan Merz *}  wenzelm@11982  1893  apply clarify  paulson@14208  1894  apply (erule_tac P = "%x. x : S" in LeastI2, fast)  wenzelm@11982  1895  apply (rule LeastI2)  wenzelm@11982  1896  apply (auto elim: monoD intro!: order_antisym)  wenzelm@11982  1897  done  wenzelm@11982  1898 wenzelm@12020  1899 wenzelm@12257  1900 subsection {* Inverse image of a function *}  wenzelm@12257  1901 wenzelm@12257  1902 constdefs  wenzelm@12257  1903  vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-" 90)  wenzelm@12257  1904  "f - B == {x. f x : B}"  wenzelm@12257  1905 wenzelm@12257  1906 wenzelm@12257  1907 subsubsection {* Basic rules *}  wenzelm@12257  1908 wenzelm@12257  1909 lemma vimage_eq [simp]: "(a : f - B) = (f a : B)"  wenzelm@12257  1910  by (unfold vimage_def) blast  wenzelm@12257  1911 wenzelm@12257  1912 lemma vimage_singleton_eq: "(a : f - {b}) = (f a = b)"  wenzelm@12257  1913  by simp  wenzelm@12257  1914 wenzelm@12257  1915 lemma vimageI [intro]: "f a = b ==> b:B ==> a : f - B"  wenzelm@12257  1916  by (unfold vimage_def) blast  wenzelm@12257  1917 wenzelm@12257  1918 lemma vimageI2: "f a : A ==> a : f - A"  wenzelm@12257  1919  by (unfold vimage_def) fast  wenzelm@12257  1920 wenzelm@12257  1921 lemma vimageE [elim!]: "a: f - B ==> (!!x. f a = x ==> x:B ==> P) ==> P"  wenzelm@12257  1922  by (unfold vimage_def) blast  wenzelm@12257  1923 wenzelm@12257  1924 lemma vimageD: "a : f - A ==> f a : A"  wenzelm@12257  1925  by (unfold vimage_def) fast  wenzelm@12257  1926 wenzelm@12257  1927 wenzelm@12257  1928 subsubsection {* Equations *}  wenzelm@12257  1929 wenzelm@12257  1930 lemma vimage_empty [simp]: "f - {} = {}"  wenzelm@12257  1931  by blast  wenzelm@12257  1932 wenzelm@12257  1933 lemma vimage_Compl: "f - (-A) = -(f - A)"  wenzelm@12257  1934  by blast  wenzelm@12257  1935 wenzelm@12257  1936 lemma vimage_Un [simp]: "f - (A Un B) = (f - A) Un (f - B)"  wenzelm@12257  1937  by blast  wenzelm@12257  1938 wenzelm@12257  1939 lemma vimage_Int [simp]: "f - (A Int B) = (f - A) Int (f - B)"  wenzelm@12257  1940  by fast  wenzelm@12257  1941 wenzelm@12257  1942 lemma vimage_Union: "f - (Union A) = (UN X:A. f - X)"  wenzelm@12257  1943  by blast  wenzelm@12257  1944 wenzelm@12257  1945 lemma vimage_UN: "f-(UN x:A. B x) = (UN x:A. f - B x)"  wenzelm@12257  1946  by blast  wenzelm@12257  1947 wenzelm@12257  1948 lemma vimage_INT: "f-(INT x:A. B x) = (INT x:A. f - B x)"  wenzelm@12257  1949  by blast  wenzelm@12257  1950 wenzelm@12257  1951 lemma vimage_Collect_eq [simp]: "f - Collect P = {y. P (f y)}"  wenzelm@12257  1952  by blast  wenzelm@12257  1953 wenzelm@12257  1954 lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f - (Collect P) = Collect Q"  wenzelm@12257  1955  by blast  wenzelm@12257  1956 wenzelm@12257  1957 lemma vimage_insert: "f-(insert a B) = (f-{a}) Un (f-B)"  wenzelm@12257  1958  -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}  wenzelm@12257  1959  by blast  wenzelm@12257  1960 wenzelm@12257  1961 lemma vimage_Diff: "f - (A - B) = (f - A) - (f - B)"  wenzelm@12257  1962  by blast  wenzelm@12257  1963 wenzelm@12257  1964 lemma vimage_UNIV [simp]: "f - UNIV = UNIV"  wenzelm@12257  1965  by blast  wenzelm@12257  1966 wenzelm@12257  1967 lemma vimage_eq_UN: "f-B = (UN y: B. f-{y})"  wenzelm@12257  1968  -- {* NOT suitable for rewriting *}  wenzelm@12257  1969  by blast  wenzelm@12257  1970 wenzelm@12897  1971 lemma vimage_mono: "A \ B ==> f - A \ f - B"  wenzelm@12257  1972  -- {* monotonicity *}  wenzelm@12257  1973  by blast  wenzelm@12257  1974 wenzelm@12257  1975 paulson@14479  1976 subsection {* Getting the Contents of a Singleton Set *}  paulson@14479  1977 paulson@14479  1978 constdefs  paulson@14479  1979  contents :: "'a set => 'a"  paulson@14479  1980  "contents X == THE x. X = {x}"  paulson@14479  1981 paulson@14479  1982 lemma contents_eq [simp]: "contents {x} = x"  paulson@14479  1983 by (simp add: contents_def)  paulson@14479  1984 paulson@14479  1985 wenzelm@12023  1986 subsection {* Transitivity rules for calculational reasoning *}  wenzelm@12020  1987 wenzelm@12020  1988 lemma forw_subst: "a = b ==> P b ==> P a"  wenzelm@12020  1989  by (rule ssubst)  wenzelm@12020  1990 wenzelm@12020  1991 lemma back_subst: "P a ==> a = b ==> P b"  wenzelm@12020  1992  by (rule subst)  wenzelm@12020  1993 wenzelm@12897  1994 lemma set_rev_mp: "x:A ==> A \ B ==> x:B"  wenzelm@12020  1995  by (rule subsetD)  wenzelm@12020  1996 wenzelm@12897  1997 lemma set_mp: "A \ B ==> x:A ==> x:B"  wenzelm@12020  1998  by (rule subsetD)  wenzelm@12020  1999 wenzelm@12020  2000 lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"  wenzelm@12020  2001  by (rule subst)  wenzelm@12020  2002 wenzelm@12020  2003 lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"  wenzelm@12020  2004  by (rule ssubst)  wenzelm@12020  2005 wenzelm@12020  2006 lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"  wenzelm@12020  2007  by (rule subst)  wenzelm@12020  2008 wenzelm@12020  2009 lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"  wenzelm@12020  2010  by (rule ssubst)  wenzelm@12020  2011 wenzelm@12020  2012 lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>  wenzelm@12020  2013  (!!x y. x < y ==> f x < f y) ==> f a < c"  wenzelm@12020  2014 proof -  wenzelm@12020  2015  assume r: "!!x y. x < y ==> f x < f y"  wenzelm@12020  2016  assume "a < b" hence "f a < f b" by (rule r)  wenzelm@12020  2017  also assume "f b < c"  wenzelm@12020  2018  finally (order_less_trans) show ?thesis .  wenzelm@12020  2019 qed  wenzelm@12020  2020 wenzelm@12020  2021 lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>  wenzelm@12020  2022  (!!x y. x < y ==> f x < f y) ==> a < f c"  wenzelm@12020  2023 proof -  wenzelm@12020  2024  assume r: "!!x y. x < y ==> f x < f y"  wenzelm@12020  2025  assume "a < f b"  wenzelm@12020  2026  also assume "b < c" hence "f b < f c" by (rule r)  wenzelm@12020  2027  finally (order_less_trans) show ?thesis .  wenzelm@12020  2028 qed  wenzelm@12020  2029 wenzelm@12020  2030 lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>  wenzelm@12020  2031  (!!x y. x <= y ==> f x <= f y) ==> f a < c"  wenzelm@12020  2032 proof -  wenzelm@12020  2033  assume r: "!!x y. x <= y ==> f x <= f y"  wenzelm@12020  2034  assume "a <= b" hence "f a <= f b" by (rule r)  wenzelm@12020  2035  also assume "f b < c"  wenzelm@12020  2036  finally (order_le_less_trans) show ?thesis .  wenzelm@12020  2037 qed  wenzelm@12020  2038 wenzelm@12020  2039 lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>  wenzelm@12020  2040  (!!x y. x < y ==> f x < f y) ==> a < f c"  wenzelm@12020  2041 proof -  wenzelm@12020  2042  assume r: "!!x y. x < y ==> f x < f y"  wenzelm@12020  2043  assume "a <= f b"  wenzelm@12020  2044  also assume "b < c" hence "f b < f c" by (rule r)  wenzelm@12020  2045  finally (order_le_less_trans) show ?thesis .  wenzelm@12020  2046 qed  wenzelm@12020  2047 wenzelm@12020  2048 lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>  wenzelm@12020  2049  (!!x y. x < y ==> f x < f y) ==> f a < c"  wenzelm@12020  2050 proof -  wenzelm@12020  2051  assume r: "!!x y. x < y ==> f x < f y"  wenzelm@12020  2052  assume "a < b" hence "f a < f b" by (rule r)  wenzelm@12020  2053  also assume "f b <= c"  wenzelm@12020  2054  finally (order_less_le_trans) show ?thesis .  wenzelm@12020  2055 qed  wenzelm@12020  2056 wenzelm@12020  2057 lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>  wenzelm@12020  2058  (!!x y. x <= y ==> f x <= f y) ==> a < f c"  wenzelm@12020  2059 proof -  wenzelm@12020  2060  assume r: "!!x y. x <= y ==> f x <= f y"  wenzelm@12020  2061  assume "a < f b"  wenzelm@12020  2062  also assume "b <= c" hence "f b <= f c" by (rule r)  wenzelm@12020  2063  finally (order_less_le_trans) show ?thesis .  wenzelm@12020  2064 qed  wenzelm@12020  2065 wenzelm@12020  2066 lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>  wenzelm@12020  2067  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"  wenzelm@12020  2068 proof -  wenzelm@12020  2069  assume r: "!!x y. x <= y ==> f x <= f y"  wenzelm@12020  2070  assume "a <= f b"  wenzelm@12020  2071  also assume "b <= c" hence "f b <= f c" by (rule r)  wenzelm@12020  2072  finally (order_trans) show ?thesis .  wenzelm@12020  2073 qed  wenzelm@12020  2074 wenzelm@12020  2075 lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>  wenzelm@12020  2076  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"  wenzelm@12020  2077 proof -  wenzelm@12020  2078  assume r: "!!x y. x <= y ==> f x <= f y"  wenzelm@12020  2079  assume "a <= b" hence "f a <= f b" by (rule r)  wenzelm@12020  2080  also assume "f b <= c"  wenzelm@12020  2081  finally (order_trans) show ?thesis .  wenzelm@12020  2082 qed  wenzelm@12020  2083 wenzelm@12020  2084 lemma ord_le_eq_subst: "a <= b ==> f b = c ==>  wenzelm@12020  2085  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"  wenzelm@12020  2086 proof -  wenzelm@12020  2087  assume r: "!!x y. x <= y ==> f x <= f y"  wenzelm@12020  2088  assume "a <= b" hence "f a <= f b" by (rule r)  wenzelm@12020  2089  also assume "f b = c"  wenzelm@12020  2090  finally (ord_le_eq_trans) show ?thesis .  wenzelm@12020  2091 qed  wenzelm@12020  2092 wenzelm@12020  2093 lemma ord_eq_le_subst: "a = f b ==> b <= c ==>  wenzelm@12020  2094  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"  wenzelm@12020  2095 proof -  wenzelm@12020  2096  assume r: "!!x y. x <= y ==> f x <= f y"  wenzelm@12020  2097  assume "a = f b"  wenzelm@12020  2098  also assume "b <= c" hence "f b <= f c" by (rule r)  wenzelm@12020  2099  finally (ord_eq_le_trans) show ?thesis .  wenzelm@12020  2100 qed  wenzelm@12020  2101 wenzelm@12020  2102 lemma ord_less_eq_subst: "a < b ==> f b = c ==>  wenzelm@12020  2103  (!!x y. x < y ==> f x < f y) ==> f a < c"  wenzelm@12020  2104 proof -  wenzelm@12020  2105  assume r: "!!x y. x < y ==> f x < f y"  wenzelm@12020  2106  assume "a < b" hence "f a < f b" by (rule r)  wenzelm@12020  2107  also assume "f b = c"  wenzelm@12020  2108  finally (ord_less_eq_trans) show ?thesis .  wenzelm@12020  2109 qed  wenzelm@12020  2110 wenzelm@12020  2111 lemma ord_eq_less_subst: "a = f b ==> b < c ==>  wenzelm@12020  2112  (!!x y. x < y ==> f x < f y) ==> a < f c"  wenzelm@12020  2113 proof -  wenzelm@12020  2114  assume r: "!!x y. x < y ==> f x < f y"  wenzelm@12020  2115  assume "a = f b"  wenzelm@12020  2116  also assume "b < c" hence "f b < f c" by (rule r)  wenzelm@12020  2117  finally (ord_eq_less_trans) show ?thesis .  wenzelm@12020  2118 qed  wenzelm@12020  2119 wenzelm@12020  2120 text {*  wenzelm@12020  2121  Note that this list of rules is in reverse order of priorities.  wenzelm@12020  2122 *}  wenzelm@12020  2123 wenzelm@12020  2124 lemmas basic_trans_rules [trans] =  wenzelm@12020  2125  order_less_subst2  wenzelm@12020  2126  order_less_subst1  wenzelm@12020  2127  order_le_less_subst2  wenzelm@12020  2128  order_le_less_subst1  wenzelm@12020  2129  order_less_le_subst2  wenzelm@12020  2130  order_less_le_subst1  wenzelm@12020  2131  order_subst2  wenzelm@12020  2132  order_subst1  wenzelm@12020  2133  ord_le_eq_subst  wenzelm@12020  2134  ord_eq_le_subst  wenzelm@12020  2135  ord_less_eq_subst  wenzelm@12020  2136  ord_eq_less_subst  wenzelm@12020  2137  forw_subst  wenzelm@12020  2138  back_subst  wenzelm@12020  2139  rev_mp  wenzelm@12020  2140  mp  wenzelm@12020  2141  set_rev_mp  wenzelm@12020  2142  set_mp  wenzelm@12020  2143  order_neq_le_trans  wenzelm@12020  2144  order_le_neq_trans  wenzelm@12020  2145  order_less_trans  wenzelm@12020  2146  order_less_asym'  wenzelm@12020  2147  order_le_less_trans  wenzelm@12020  2148  order_less_le_trans  wenzelm@12020  2149  order_trans  wenzelm@12020  2150  order_antisym  wenzelm@12020  2151  ord_le_eq_trans  wenzelm@12020  2152  ord_eq_le_trans  wenzelm@12020  2153  ord_less_eq_trans  wenzelm@12020  2154  ord_eq_less_trans  wenzelm@12020  2155  trans  wenzelm@12020  2156 wenzelm@11979  2157 end