src/HOL/Set.thy
 author wenzelm Tue Oct 30 13:43:26 2001 +0100 (2001-10-30) changeset 11982 65e2822d83dd parent 11979 0a3dace545c5 child 12020 a24373086908 permissions -rw-r--r--
lemma Least_mono moved from Typedef.thy to Set.thy;
 clasohm@923 ` 1` ```(* Title: HOL/Set.thy ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@923 ` 3` ``` Author: Tobias Nipkow ``` clasohm@923 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@923 ` 5` ```*) ``` clasohm@923 ` 6` wenzelm@11979 ` 7` ```header {* Set theory for higher-order logic *} ``` wenzelm@11979 ` 8` wenzelm@11979 ` 9` ```theory Set = HOL ``` wenzelm@11979 ` 10` ```files ("subset.ML") ("equalities.ML") ("mono.ML"): ``` wenzelm@11979 ` 11` wenzelm@11979 ` 12` ```text {* A set in HOL is simply a predicate. *} ``` clasohm@923 ` 13` wenzelm@2261 ` 14` wenzelm@11979 ` 15` ```subsection {* Basic syntax *} ``` wenzelm@2261 ` 16` wenzelm@3947 ` 17` ```global ``` wenzelm@3947 ` 18` wenzelm@11979 ` 19` ```typedecl 'a set ``` wenzelm@11979 ` 20` ```arities set :: ("term") "term" ``` wenzelm@3820 ` 21` clasohm@923 ` 22` ```consts ``` wenzelm@11979 ` 23` ``` "{}" :: "'a set" ("{}") ``` wenzelm@11979 ` 24` ``` UNIV :: "'a set" ``` wenzelm@11979 ` 25` ``` insert :: "'a => 'a set => 'a set" ``` wenzelm@11979 ` 26` ``` Collect :: "('a => bool) => 'a set" -- "comprehension" ``` wenzelm@11979 ` 27` ``` Int :: "'a set => 'a set => 'a set" (infixl 70) ``` wenzelm@11979 ` 28` ``` Un :: "'a set => 'a set => 'a set" (infixl 65) ``` wenzelm@11979 ` 29` ``` UNION :: "'a set => ('a => 'b set) => 'b set" -- "general union" ``` wenzelm@11979 ` 30` ``` INTER :: "'a set => ('a => 'b set) => 'b set" -- "general intersection" ``` wenzelm@11979 ` 31` ``` Union :: "'a set set => 'a set" -- "union of a set" ``` wenzelm@11979 ` 32` ``` Inter :: "'a set set => 'a set" -- "intersection of a set" ``` wenzelm@11979 ` 33` ``` Pow :: "'a set => 'a set set" -- "powerset" ``` wenzelm@11979 ` 34` ``` Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers" ``` wenzelm@11979 ` 35` ``` Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers" ``` wenzelm@11979 ` 36` ``` image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) ``` wenzelm@11979 ` 37` wenzelm@11979 ` 38` ```syntax ``` wenzelm@11979 ` 39` ``` "op :" :: "'a => 'a set => bool" ("op :") ``` wenzelm@11979 ` 40` ```consts ``` wenzelm@11979 ` 41` ``` "op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50) -- "membership" ``` wenzelm@11979 ` 42` wenzelm@11979 ` 43` ```local ``` wenzelm@11979 ` 44` wenzelm@11979 ` 45` ```instance set :: ("term") ord .. ``` wenzelm@11979 ` 46` ```instance set :: ("term") minus .. ``` clasohm@923 ` 47` clasohm@923 ` 48` wenzelm@11979 ` 49` ```subsection {* Additional concrete syntax *} ``` wenzelm@2261 ` 50` clasohm@923 ` 51` ```syntax ``` wenzelm@11979 ` 52` ``` range :: "('a => 'b) => 'b set" -- "of function" ``` clasohm@923 ` 53` wenzelm@11979 ` 54` ``` "op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership" ``` wenzelm@11979 ` 55` ``` "op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50) ``` wenzelm@7238 ` 56` wenzelm@11979 ` 57` ``` "@Finset" :: "args => 'a set" ("{(_)}") ``` wenzelm@11979 ` 58` ``` "@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") ``` wenzelm@11979 ` 59` ``` "@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})") ``` clasohm@923 ` 60` wenzelm@11979 ` 61` ``` "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10) ``` wenzelm@11979 ` 62` ``` "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10) ``` wenzelm@11979 ` 63` ``` "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10) ``` wenzelm@11979 ` 64` ``` "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10) ``` clasohm@923 ` 65` wenzelm@11979 ` 66` ``` "_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) ``` wenzelm@11979 ` 67` ``` "_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10) ``` clasohm@923 ` 68` wenzelm@7238 ` 69` ```syntax (HOL) ``` wenzelm@11979 ` 70` ``` "_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10) ``` wenzelm@11979 ` 71` ``` "_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10) ``` clasohm@923 ` 72` clasohm@923 ` 73` ```translations ``` nipkow@10832 ` 74` ``` "range f" == "f`UNIV" ``` clasohm@923 ` 75` ``` "x ~: y" == "~ (x : y)" ``` clasohm@923 ` 76` ``` "{x, xs}" == "insert x {xs}" ``` clasohm@923 ` 77` ``` "{x}" == "insert x {}" ``` clasohm@923 ` 78` ``` "{x. P}" == "Collect (%x. P)" ``` paulson@4159 ` 79` ``` "UN x y. B" == "UN x. UN y. B" ``` paulson@4159 ` 80` ``` "UN x. B" == "UNION UNIV (%x. B)" ``` wenzelm@7238 ` 81` ``` "INT x y. B" == "INT x. INT y. B" ``` paulson@4159 ` 82` ``` "INT x. B" == "INTER UNIV (%x. B)" ``` paulson@4159 ` 83` ``` "UN x:A. B" == "UNION A (%x. B)" ``` clasohm@923 ` 84` ``` "INT x:A. B" == "INTER A (%x. B)" ``` wenzelm@7238 ` 85` ``` "ALL x:A. P" == "Ball A (%x. P)" ``` wenzelm@7238 ` 86` ``` "EX x:A. P" == "Bex A (%x. P)" ``` clasohm@923 ` 87` wenzelm@2388 ` 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@2261 ` 94` ```syntax (symbols) ``` 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) ``` wenzelm@11979 ` 105` ``` "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" 10) ``` wenzelm@11979 ` 106` ``` "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" 10) ``` wenzelm@11979 ` 107` ``` "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" 10) ``` wenzelm@11979 ` 108` ``` "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" 10) ``` wenzelm@11979 ` 109` ``` Union :: "'a set set => 'a set" ("\_" [90] 90) ``` wenzelm@11979 ` 110` ``` Inter :: "'a set set => 'a set" ("\_" [90] 90) ``` wenzelm@11979 ` 111` ``` "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@11979 ` 112` ``` "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@2261 ` 113` wenzelm@2412 ` 114` ```translations ``` wenzelm@11979 ` 115` ``` "op \" => "op <= :: _ set => _ set => bool" ``` wenzelm@11979 ` 116` ``` "op \" => "op < :: _ set => _ set => bool" ``` wenzelm@2261 ` 117` wenzelm@2261 ` 118` wenzelm@11979 ` 119` ```typed_print_translation {* ``` wenzelm@11979 ` 120` ``` let ``` wenzelm@11979 ` 121` ``` fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = ``` wenzelm@11979 ` 122` ``` list_comb (Syntax.const "_setle", ts) ``` wenzelm@11979 ` 123` ``` | le_tr' _ _ _ = raise Match; ``` wenzelm@11979 ` 124` wenzelm@11979 ` 125` ``` fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = ``` wenzelm@11979 ` 126` ``` list_comb (Syntax.const "_setless", ts) ``` wenzelm@11979 ` 127` ``` | less_tr' _ _ _ = raise Match; ``` wenzelm@11979 ` 128` ``` in [("op <=", le_tr'), ("op <", less_tr')] end ``` wenzelm@11979 ` 129` ```*} ``` wenzelm@2261 ` 130` wenzelm@11979 ` 131` ```text {* ``` wenzelm@11979 ` 132` ``` \medskip Translate between @{text "{e | x1...xn. P}"} and @{text ``` wenzelm@11979 ` 133` ``` "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is ``` wenzelm@11979 ` 134` ``` only translated if @{text "[0..n] subset bvs(e)"}. ``` wenzelm@11979 ` 135` ```*} ``` wenzelm@11979 ` 136` wenzelm@11979 ` 137` ```parse_translation {* ``` wenzelm@11979 ` 138` ``` let ``` wenzelm@11979 ` 139` ``` val ex_tr = snd (mk_binder_tr ("EX ", "Ex")); ``` wenzelm@3947 ` 140` wenzelm@11979 ` 141` ``` fun nvars (Const ("_idts", _) \$ _ \$ idts) = nvars idts + 1 ``` wenzelm@11979 ` 142` ``` | nvars _ = 1; ``` wenzelm@11979 ` 143` wenzelm@11979 ` 144` ``` fun setcompr_tr [e, idts, b] = ``` wenzelm@11979 ` 145` ``` let ``` wenzelm@11979 ` 146` ``` val eq = Syntax.const "op =" \$ Bound (nvars idts) \$ e; ``` wenzelm@11979 ` 147` ``` val P = Syntax.const "op &" \$ eq \$ b; ``` wenzelm@11979 ` 148` ``` val exP = ex_tr [idts, P]; ``` wenzelm@11979 ` 149` ``` in Syntax.const "Collect" \$ Abs ("", dummyT, exP) end; ``` wenzelm@11979 ` 150` wenzelm@11979 ` 151` ``` in [("@SetCompr", setcompr_tr)] end; ``` wenzelm@11979 ` 152` ```*} ``` clasohm@923 ` 153` wenzelm@11979 ` 154` ```print_translation {* ``` wenzelm@11979 ` 155` ``` let ``` wenzelm@11979 ` 156` ``` val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY")); ``` wenzelm@11979 ` 157` wenzelm@11979 ` 158` ``` fun setcompr_tr' [Abs (_, _, P)] = ``` wenzelm@11979 ` 159` ``` let ``` wenzelm@11979 ` 160` ``` fun check (Const ("Ex", _) \$ Abs (_, _, P), n) = check (P, n + 1) ``` wenzelm@11979 ` 161` ``` | check (Const ("op &", _) \$ (Const ("op =", _) \$ Bound m \$ e) \$ P, n) = ``` wenzelm@11979 ` 162` ``` if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso ``` wenzelm@11979 ` 163` ``` ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then () ``` wenzelm@11979 ` 164` ``` else raise Match; ``` clasohm@923 ` 165` wenzelm@11979 ` 166` ``` fun tr' (_ \$ abs) = ``` wenzelm@11979 ` 167` ``` let val _ \$ idts \$ (_ \$ (_ \$ _ \$ e) \$ Q) = ex_tr' [abs] ``` wenzelm@11979 ` 168` ``` in Syntax.const "@SetCompr" \$ e \$ idts \$ Q end; ``` wenzelm@11979 ` 169` ``` in check (P, 0); tr' P end; ``` wenzelm@11979 ` 170` ``` in [("Collect", setcompr_tr')] end; ``` wenzelm@11979 ` 171` ```*} ``` wenzelm@11979 ` 172` wenzelm@11979 ` 173` wenzelm@11979 ` 174` ```subsection {* Rules and definitions *} ``` wenzelm@11979 ` 175` wenzelm@11979 ` 176` ```text {* Isomorphisms between predicates and sets. *} ``` clasohm@923 ` 177` wenzelm@11979 ` 178` ```axioms ``` wenzelm@11979 ` 179` ``` mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)" ``` wenzelm@11979 ` 180` ``` Collect_mem_eq [simp]: "{x. x:A} = A" ``` wenzelm@11979 ` 181` wenzelm@11979 ` 182` ```defs ``` wenzelm@11979 ` 183` ``` Ball_def: "Ball A P == ALL x. x:A --> P(x)" ``` wenzelm@11979 ` 184` ``` Bex_def: "Bex A P == EX x. x:A & P(x)" ``` wenzelm@11979 ` 185` wenzelm@11979 ` 186` ```defs (overloaded) ``` wenzelm@11979 ` 187` ``` subset_def: "A <= B == ALL x:A. x:B" ``` wenzelm@11979 ` 188` ``` psubset_def: "A < B == (A::'a set) <= B & ~ A=B" ``` wenzelm@11979 ` 189` ``` Compl_def: "- A == {x. ~x:A}" ``` clasohm@923 ` 190` clasohm@923 ` 191` ```defs ``` wenzelm@11979 ` 192` ``` Un_def: "A Un B == {x. x:A | x:B}" ``` wenzelm@11979 ` 193` ``` Int_def: "A Int B == {x. x:A & x:B}" ``` wenzelm@11979 ` 194` ``` set_diff_def: "A - B == {x. x:A & ~x:B}" ``` wenzelm@11979 ` 195` ``` INTER_def: "INTER A B == {y. ALL x:A. y: B(x)}" ``` wenzelm@11979 ` 196` ``` UNION_def: "UNION A B == {y. EX x:A. y: B(x)}" ``` wenzelm@11979 ` 197` ``` Inter_def: "Inter S == (INT x:S. x)" ``` wenzelm@11979 ` 198` ``` Union_def: "Union S == (UN x:S. x)" ``` wenzelm@11979 ` 199` ``` Pow_def: "Pow A == {B. B <= A}" ``` wenzelm@11979 ` 200` ``` empty_def: "{} == {x. False}" ``` wenzelm@11979 ` 201` ``` UNIV_def: "UNIV == {x. True}" ``` wenzelm@11979 ` 202` ``` insert_def: "insert a B == {x. x=a} Un B" ``` wenzelm@11979 ` 203` ``` image_def: "f`A == {y. EX x:A. y = f(x)}" ``` wenzelm@11979 ` 204` wenzelm@11979 ` 205` wenzelm@11979 ` 206` ```subsection {* Lemmas and proof tool setup *} ``` wenzelm@11979 ` 207` wenzelm@11979 ` 208` ```subsubsection {* Relating predicates and sets *} ``` wenzelm@11979 ` 209` wenzelm@11979 ` 210` ```lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}" ``` wenzelm@11979 ` 211` ``` by simp ``` wenzelm@11979 ` 212` wenzelm@11979 ` 213` ```lemma CollectD: "a : {x. P(x)} ==> P(a)" ``` wenzelm@11979 ` 214` ``` by simp ``` wenzelm@11979 ` 215` wenzelm@11979 ` 216` ```lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B" ``` wenzelm@11979 ` 217` ```proof - ``` wenzelm@11979 ` 218` ``` case rule_context ``` wenzelm@11979 ` 219` ``` show ?thesis ``` wenzelm@11979 ` 220` ``` apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals]) ``` wenzelm@11979 ` 221` ``` apply (rule Collect_mem_eq) ``` wenzelm@11979 ` 222` ``` apply (rule Collect_mem_eq) ``` wenzelm@11979 ` 223` ``` done ``` wenzelm@11979 ` 224` ```qed ``` wenzelm@11979 ` 225` wenzelm@11979 ` 226` ```lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}" ``` wenzelm@11979 ` 227` ``` by simp ``` wenzelm@11979 ` 228` wenzelm@11979 ` 229` ```lemmas CollectE [elim!] = CollectD [elim_format] ``` wenzelm@11979 ` 230` wenzelm@11979 ` 231` wenzelm@11979 ` 232` ```subsubsection {* Bounded quantifiers *} ``` wenzelm@11979 ` 233` wenzelm@11979 ` 234` ```lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" ``` wenzelm@11979 ` 235` ``` by (simp add: Ball_def) ``` wenzelm@11979 ` 236` wenzelm@11979 ` 237` ```lemmas strip = impI allI ballI ``` wenzelm@11979 ` 238` wenzelm@11979 ` 239` ```lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x" ``` wenzelm@11979 ` 240` ``` by (simp add: Ball_def) ``` wenzelm@11979 ` 241` wenzelm@11979 ` 242` ```lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" ``` wenzelm@11979 ` 243` ``` by (unfold Ball_def) blast ``` wenzelm@11979 ` 244` wenzelm@11979 ` 245` ```text {* ``` wenzelm@11979 ` 246` ``` \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and ``` wenzelm@11979 ` 247` ``` @{prop "a:A"}; creates assumption @{prop "P a"}. ``` wenzelm@11979 ` 248` ```*} ``` wenzelm@11979 ` 249` wenzelm@11979 ` 250` ```ML {* ``` wenzelm@11979 ` 251` ``` local val ballE = thm "ballE" ``` wenzelm@11979 ` 252` ``` in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end; ``` wenzelm@11979 ` 253` ```*} ``` wenzelm@11979 ` 254` wenzelm@11979 ` 255` ```text {* ``` wenzelm@11979 ` 256` ``` Gives better instantiation for bound: ``` wenzelm@11979 ` 257` ```*} ``` wenzelm@11979 ` 258` wenzelm@11979 ` 259` ```ML_setup {* ``` wenzelm@11979 ` 260` ``` claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1); ``` wenzelm@11979 ` 261` ```*} ``` wenzelm@11979 ` 262` wenzelm@11979 ` 263` ```lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" ``` wenzelm@11979 ` 264` ``` -- {* Normally the best argument order: @{prop "P x"} constrains the ``` wenzelm@11979 ` 265` ``` choice of @{prop "x:A"}. *} ``` wenzelm@11979 ` 266` ``` by (unfold Bex_def) blast ``` wenzelm@11979 ` 267` wenzelm@11979 ` 268` ```lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x" ``` wenzelm@11979 ` 269` ``` -- {* The best argument order when there is only one @{prop "x:A"}. *} ``` wenzelm@11979 ` 270` ``` by (unfold Bex_def) blast ``` wenzelm@11979 ` 271` wenzelm@11979 ` 272` ```lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x" ``` wenzelm@11979 ` 273` ``` by (unfold Bex_def) blast ``` wenzelm@11979 ` 274` wenzelm@11979 ` 275` ```lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q" ``` wenzelm@11979 ` 276` ``` by (unfold Bex_def) blast ``` wenzelm@11979 ` 277` wenzelm@11979 ` 278` ```lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)" ``` wenzelm@11979 ` 279` ``` -- {* Trival rewrite rule. *} ``` wenzelm@11979 ` 280` ``` by (simp add: Ball_def) ``` wenzelm@11979 ` 281` wenzelm@11979 ` 282` ```lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)" ``` wenzelm@11979 ` 283` ``` -- {* Dual form for existentials. *} ``` wenzelm@11979 ` 284` ``` by (simp add: Bex_def) ``` wenzelm@11979 ` 285` wenzelm@11979 ` 286` ```lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)" ``` wenzelm@11979 ` 287` ``` by blast ``` wenzelm@11979 ` 288` wenzelm@11979 ` 289` ```lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)" ``` wenzelm@11979 ` 290` ``` by blast ``` wenzelm@11979 ` 291` wenzelm@11979 ` 292` ```lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)" ``` wenzelm@11979 ` 293` ``` by blast ``` wenzelm@11979 ` 294` wenzelm@11979 ` 295` ```lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)" ``` wenzelm@11979 ` 296` ``` by blast ``` wenzelm@11979 ` 297` wenzelm@11979 ` 298` ```lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)" ``` wenzelm@11979 ` 299` ``` by blast ``` wenzelm@11979 ` 300` wenzelm@11979 ` 301` ```lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)" ``` wenzelm@11979 ` 302` ``` by blast ``` wenzelm@11979 ` 303` wenzelm@11979 ` 304` ```ML_setup {* ``` wenzelm@11979 ` 305` ``` let ``` wenzelm@11979 ` 306` ``` val Ball_def = thm "Ball_def"; ``` wenzelm@11979 ` 307` ``` val Bex_def = thm "Bex_def"; ``` wenzelm@11979 ` 308` wenzelm@11979 ` 309` ``` val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` wenzelm@11979 ` 310` ``` ("EX x:A. P x & Q x", HOLogic.boolT); ``` wenzelm@11979 ` 311` wenzelm@11979 ` 312` ``` val prove_bex_tac = ``` wenzelm@11979 ` 313` ``` rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac; ``` wenzelm@11979 ` 314` ``` val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; ``` wenzelm@11979 ` 315` wenzelm@11979 ` 316` ``` val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ``` wenzelm@11979 ` 317` ``` ("ALL x:A. P x --> Q x", HOLogic.boolT); ``` wenzelm@11979 ` 318` wenzelm@11979 ` 319` ``` val prove_ball_tac = ``` wenzelm@11979 ` 320` ``` rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac; ``` wenzelm@11979 ` 321` ``` val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; ``` wenzelm@11979 ` 322` wenzelm@11979 ` 323` ``` val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; ``` wenzelm@11979 ` 324` ``` val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball; ``` wenzelm@11979 ` 325` ``` in ``` wenzelm@11979 ` 326` ``` Addsimprocs [defBALL_regroup, defBEX_regroup] ``` wenzelm@11979 ` 327` ``` end; ``` wenzelm@11979 ` 328` ```*} ``` wenzelm@11979 ` 329` wenzelm@11979 ` 330` wenzelm@11979 ` 331` ```subsubsection {* Congruence rules *} ``` wenzelm@11979 ` 332` wenzelm@11979 ` 333` ```lemma ball_cong [cong]: ``` wenzelm@11979 ` 334` ``` "A = B ==> (!!x. x:B ==> P x = Q x) ==> ``` wenzelm@11979 ` 335` ``` (ALL x:A. P x) = (ALL x:B. Q x)" ``` wenzelm@11979 ` 336` ``` by (simp add: Ball_def) ``` wenzelm@11979 ` 337` wenzelm@11979 ` 338` ```lemma bex_cong [cong]: ``` wenzelm@11979 ` 339` ``` "A = B ==> (!!x. x:B ==> P x = Q x) ==> ``` wenzelm@11979 ` 340` ``` (EX x:A. P x) = (EX x:B. Q x)" ``` wenzelm@11979 ` 341` ``` by (simp add: Bex_def cong: conj_cong) ``` regensbu@1273 ` 342` wenzelm@7238 ` 343` wenzelm@11979 ` 344` ```subsubsection {* Subsets *} ``` wenzelm@11979 ` 345` wenzelm@11979 ` 346` ```lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B" ``` wenzelm@11979 ` 347` ``` by (simp add: subset_def) ``` wenzelm@11979 ` 348` wenzelm@11979 ` 349` ```text {* ``` wenzelm@11979 ` 350` ``` \medskip Map the type @{text "'a set => anything"} to just @{typ ``` wenzelm@11979 ` 351` ``` 'a}; for overloading constants whose first argument has type @{typ ``` wenzelm@11979 ` 352` ``` "'a set"}. ``` wenzelm@11979 ` 353` ```*} ``` wenzelm@11979 ` 354` wenzelm@11979 ` 355` ```ML {* ``` wenzelm@11979 ` 356` ``` fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type); ``` wenzelm@11979 ` 357` ```*} ``` wenzelm@11979 ` 358` wenzelm@11979 ` 359` ```ML " ``` wenzelm@11979 ` 360` ``` (* While (:) is not, its type must be kept ``` wenzelm@11979 ` 361` ``` for overloading of = to work. *) ``` wenzelm@11979 ` 362` ``` Blast.overloaded (\"op :\", domain_type); ``` wenzelm@11979 ` 363` wenzelm@11979 ` 364` ``` overload_1st_set \"Ball\"; (*need UNION, INTER also?*) ``` wenzelm@11979 ` 365` ``` overload_1st_set \"Bex\"; ``` wenzelm@11979 ` 366` wenzelm@11979 ` 367` ``` (*Image: retain the type of the set being expressed*) ``` wenzelm@11979 ` 368` ``` Blast.overloaded (\"image\", domain_type); ``` wenzelm@11979 ` 369` ```" ``` wenzelm@11979 ` 370` wenzelm@11979 ` 371` ```lemma subsetD [elim]: "A <= B ==> c:A ==> c:B" ``` wenzelm@11979 ` 372` ``` -- {* Rule in Modus Ponens style. *} ``` wenzelm@11979 ` 373` ``` by (unfold subset_def) blast ``` wenzelm@11979 ` 374` wenzelm@11979 ` 375` ```declare subsetD [intro?] -- FIXME ``` wenzelm@11979 ` 376` wenzelm@11979 ` 377` ```lemma rev_subsetD: "c:A ==> A <= B ==> c:B" ``` wenzelm@11979 ` 378` ``` -- {* The same, with reversed premises for use with @{text erule} -- ``` wenzelm@11979 ` 379` ``` cf @{text rev_mp}. *} ``` wenzelm@11979 ` 380` ``` by (rule subsetD) ``` wenzelm@11979 ` 381` wenzelm@11979 ` 382` ```declare rev_subsetD [intro?] -- FIXME ``` wenzelm@11979 ` 383` wenzelm@11979 ` 384` ```text {* ``` wenzelm@11979 ` 385` ``` \medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}. ``` wenzelm@11979 ` 386` ```*} ``` wenzelm@11979 ` 387` wenzelm@11979 ` 388` ```ML {* ``` wenzelm@11979 ` 389` ``` local val rev_subsetD = thm "rev_subsetD" ``` wenzelm@11979 ` 390` ``` in fun impOfSubs th = th RSN (2, rev_subsetD) end; ``` wenzelm@11979 ` 391` ```*} ``` wenzelm@11979 ` 392` wenzelm@11979 ` 393` ```lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P" ``` wenzelm@11979 ` 394` ``` -- {* Classical elimination rule. *} ``` wenzelm@11979 ` 395` ``` by (unfold subset_def) blast ``` wenzelm@11979 ` 396` wenzelm@11979 ` 397` ```text {* ``` wenzelm@11979 ` 398` ``` \medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and ``` wenzelm@11979 ` 399` ``` creates the assumption @{prop "c:B"}. ``` wenzelm@11979 ` 400` ```*} ``` wenzelm@11979 ` 401` wenzelm@11979 ` 402` ```ML {* ``` wenzelm@11979 ` 403` ``` local val subsetCE = thm "subsetCE" ``` wenzelm@11979 ` 404` ``` in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end; ``` wenzelm@11979 ` 405` ```*} ``` wenzelm@11979 ` 406` wenzelm@11979 ` 407` ```lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A" ``` wenzelm@11979 ` 408` ``` by blast ``` wenzelm@11979 ` 409` wenzelm@11979 ` 410` ```lemma subset_refl: "A <= (A::'a set)" ``` wenzelm@11979 ` 411` ``` by fast ``` wenzelm@11979 ` 412` wenzelm@11979 ` 413` ```lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)" ``` wenzelm@11979 ` 414` ``` by blast ``` clasohm@923 ` 415` wenzelm@2261 ` 416` wenzelm@11979 ` 417` ```subsubsection {* Equality *} ``` wenzelm@11979 ` 418` wenzelm@11979 ` 419` ```lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)" ``` wenzelm@11979 ` 420` ``` -- {* Anti-symmetry of the subset relation. *} ``` wenzelm@11979 ` 421` ``` by (rule set_ext) (blast intro: subsetD) ``` wenzelm@11979 ` 422` wenzelm@11979 ` 423` ```lemmas equalityI = subset_antisym ``` wenzelm@11979 ` 424` wenzelm@11979 ` 425` ```text {* ``` wenzelm@11979 ` 426` ``` \medskip Equality rules from ZF set theory -- are they appropriate ``` wenzelm@11979 ` 427` ``` here? ``` wenzelm@11979 ` 428` ```*} ``` wenzelm@11979 ` 429` wenzelm@11979 ` 430` ```lemma equalityD1: "A = B ==> A <= (B::'a set)" ``` wenzelm@11979 ` 431` ``` by (simp add: subset_refl) ``` wenzelm@11979 ` 432` wenzelm@11979 ` 433` ```lemma equalityD2: "A = B ==> B <= (A::'a set)" ``` wenzelm@11979 ` 434` ``` by (simp add: subset_refl) ``` wenzelm@11979 ` 435` wenzelm@11979 ` 436` ```text {* ``` wenzelm@11979 ` 437` ``` \medskip Be careful when adding this to the claset as @{text ``` wenzelm@11979 ` 438` ``` subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{} ``` wenzelm@11979 ` 439` ``` <= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}! ``` wenzelm@11979 ` 440` ```*} ``` wenzelm@11979 ` 441` wenzelm@11979 ` 442` ```lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P" ``` wenzelm@11979 ` 443` ``` by (simp add: subset_refl) ``` clasohm@923 ` 444` wenzelm@11979 ` 445` ```lemma equalityCE [elim]: ``` wenzelm@11979 ` 446` ``` "A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P" ``` wenzelm@11979 ` 447` ``` by blast ``` wenzelm@11979 ` 448` wenzelm@11979 ` 449` ```text {* ``` wenzelm@11979 ` 450` ``` \medskip Lemma for creating induction formulae -- for "pattern ``` wenzelm@11979 ` 451` ``` matching" on @{text p}. To make the induction hypotheses usable, ``` wenzelm@11979 ` 452` ``` apply @{text spec} or @{text bspec} to put universal quantifiers over the free ``` wenzelm@11979 ` 453` ``` variables in @{text p}. ``` wenzelm@11979 ` 454` ```*} ``` wenzelm@11979 ` 455` wenzelm@11979 ` 456` ```lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R" ``` wenzelm@11979 ` 457` ``` by simp ``` clasohm@923 ` 458` wenzelm@11979 ` 459` ```lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)" ``` wenzelm@11979 ` 460` ``` by simp ``` wenzelm@11979 ` 461` wenzelm@11979 ` 462` wenzelm@11979 ` 463` ```subsubsection {* The universal set -- UNIV *} ``` wenzelm@11979 ` 464` wenzelm@11979 ` 465` ```lemma UNIV_I [simp]: "x : UNIV" ``` wenzelm@11979 ` 466` ``` by (simp add: UNIV_def) ``` wenzelm@11979 ` 467` wenzelm@11979 ` 468` ```declare UNIV_I [intro] -- {* unsafe makes it less likely to cause problems *} ``` wenzelm@11979 ` 469` wenzelm@11979 ` 470` ```lemma UNIV_witness [intro?]: "EX x. x : UNIV" ``` wenzelm@11979 ` 471` ``` by simp ``` wenzelm@11979 ` 472` wenzelm@11979 ` 473` ```lemma subset_UNIV: "A <= UNIV" ``` wenzelm@11979 ` 474` ``` by (rule subsetI) (rule UNIV_I) ``` wenzelm@2388 ` 475` wenzelm@11979 ` 476` ```text {* ``` wenzelm@11979 ` 477` ``` \medskip Eta-contracting these two rules (to remove @{text P}) ``` wenzelm@11979 ` 478` ``` causes them to be ignored because of their interaction with ``` wenzelm@11979 ` 479` ``` congruence rules. ``` wenzelm@11979 ` 480` ```*} ``` wenzelm@11979 ` 481` wenzelm@11979 ` 482` ```lemma ball_UNIV [simp]: "Ball UNIV P = All P" ``` wenzelm@11979 ` 483` ``` by (simp add: Ball_def) ``` wenzelm@11979 ` 484` wenzelm@11979 ` 485` ```lemma bex_UNIV [simp]: "Bex UNIV P = Ex P" ``` wenzelm@11979 ` 486` ``` by (simp add: Bex_def) ``` wenzelm@11979 ` 487` wenzelm@11979 ` 488` wenzelm@11979 ` 489` ```subsubsection {* The empty set *} ``` wenzelm@11979 ` 490` wenzelm@11979 ` 491` ```lemma empty_iff [simp]: "(c : {}) = False" ``` wenzelm@11979 ` 492` ``` by (simp add: empty_def) ``` wenzelm@11979 ` 493` wenzelm@11979 ` 494` ```lemma emptyE [elim!]: "a : {} ==> P" ``` wenzelm@11979 ` 495` ``` by simp ``` wenzelm@11979 ` 496` wenzelm@11979 ` 497` ```lemma empty_subsetI [iff]: "{} <= A" ``` wenzelm@11979 ` 498` ``` -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *} ``` wenzelm@11979 ` 499` ``` by blast ``` wenzelm@11979 ` 500` wenzelm@11979 ` 501` ```lemma equals0I: "(!!y. y:A ==> False) ==> A = {}" ``` wenzelm@11979 ` 502` ``` by blast ``` wenzelm@2388 ` 503` wenzelm@11979 ` 504` ```lemma equals0D: "A={} ==> a ~: A" ``` wenzelm@11979 ` 505` ``` -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *} ``` wenzelm@11979 ` 506` ``` by blast ``` wenzelm@11979 ` 507` wenzelm@11979 ` 508` ```lemma ball_empty [simp]: "Ball {} P = True" ``` wenzelm@11979 ` 509` ``` by (simp add: Ball_def) ``` wenzelm@11979 ` 510` wenzelm@11979 ` 511` ```lemma bex_empty [simp]: "Bex {} P = False" ``` wenzelm@11979 ` 512` ``` by (simp add: Bex_def) ``` wenzelm@11979 ` 513` wenzelm@11979 ` 514` ```lemma UNIV_not_empty [iff]: "UNIV ~= {}" ``` wenzelm@11979 ` 515` ``` by (blast elim: equalityE) ``` wenzelm@11979 ` 516` wenzelm@11979 ` 517` wenzelm@11979 ` 518` ```section {* The Powerset operator -- Pow *} ``` wenzelm@11979 ` 519` wenzelm@11979 ` 520` ```lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)" ``` wenzelm@11979 ` 521` ``` by (simp add: Pow_def) ``` wenzelm@11979 ` 522` wenzelm@11979 ` 523` ```lemma PowI: "A <= B ==> A : Pow B" ``` wenzelm@11979 ` 524` ``` by (simp add: Pow_def) ``` wenzelm@11979 ` 525` wenzelm@11979 ` 526` ```lemma PowD: "A : Pow B ==> A <= B" ``` wenzelm@11979 ` 527` ``` by (simp add: Pow_def) ``` wenzelm@11979 ` 528` wenzelm@11979 ` 529` ```lemma Pow_bottom: "{}: Pow B" ``` wenzelm@11979 ` 530` ``` by simp ``` wenzelm@11979 ` 531` wenzelm@11979 ` 532` ```lemma Pow_top: "A : Pow A" ``` wenzelm@11979 ` 533` ``` by (simp add: subset_refl) ``` wenzelm@2684 ` 534` wenzelm@2388 ` 535` wenzelm@11979 ` 536` ```subsubsection {* Set complement *} ``` wenzelm@11979 ` 537` wenzelm@11979 ` 538` ```lemma Compl_iff [simp]: "(c : -A) = (c~:A)" ``` wenzelm@11979 ` 539` ``` by (unfold Compl_def) blast ``` wenzelm@11979 ` 540` wenzelm@11979 ` 541` ```lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A" ``` wenzelm@11979 ` 542` ``` by (unfold Compl_def) blast ``` wenzelm@11979 ` 543` wenzelm@11979 ` 544` ```text {* ``` wenzelm@11979 ` 545` ``` \medskip This form, with negated conclusion, works well with the ``` wenzelm@11979 ` 546` ``` Classical prover. Negated assumptions behave like formulae on the ``` wenzelm@11979 ` 547` ``` right side of the notional turnstile ... *} ``` wenzelm@11979 ` 548` wenzelm@11979 ` 549` ```lemma ComplD: "c : -A ==> c~:A" ``` wenzelm@11979 ` 550` ``` by (unfold Compl_def) blast ``` wenzelm@11979 ` 551` wenzelm@11979 ` 552` ```lemmas ComplE [elim!] = ComplD [elim_format] ``` wenzelm@11979 ` 553` wenzelm@11979 ` 554` wenzelm@11979 ` 555` ```subsubsection {* Binary union -- Un *} ``` clasohm@923 ` 556` wenzelm@11979 ` 557` ```lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)" ``` wenzelm@11979 ` 558` ``` by (unfold Un_def) blast ``` wenzelm@11979 ` 559` wenzelm@11979 ` 560` ```lemma UnI1 [elim?]: "c:A ==> c : A Un B" ``` wenzelm@11979 ` 561` ``` by simp ``` wenzelm@11979 ` 562` wenzelm@11979 ` 563` ```lemma UnI2 [elim?]: "c:B ==> c : A Un B" ``` wenzelm@11979 ` 564` ``` by simp ``` clasohm@923 ` 565` wenzelm@11979 ` 566` ```text {* ``` wenzelm@11979 ` 567` ``` \medskip Classical introduction rule: no commitment to @{prop A} vs ``` wenzelm@11979 ` 568` ``` @{prop B}. ``` wenzelm@11979 ` 569` ```*} ``` wenzelm@11979 ` 570` wenzelm@11979 ` 571` ```lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B" ``` wenzelm@11979 ` 572` ``` by auto ``` wenzelm@11979 ` 573` wenzelm@11979 ` 574` ```lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P" ``` wenzelm@11979 ` 575` ``` by (unfold Un_def) blast ``` wenzelm@11979 ` 576` wenzelm@11979 ` 577` wenzelm@11979 ` 578` ```section {* Binary intersection -- Int *} ``` clasohm@923 ` 579` wenzelm@11979 ` 580` ```lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)" ``` wenzelm@11979 ` 581` ``` by (unfold Int_def) blast ``` wenzelm@11979 ` 582` wenzelm@11979 ` 583` ```lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B" ``` wenzelm@11979 ` 584` ``` by simp ``` wenzelm@11979 ` 585` wenzelm@11979 ` 586` ```lemma IntD1: "c : A Int B ==> c:A" ``` wenzelm@11979 ` 587` ``` by simp ``` wenzelm@11979 ` 588` wenzelm@11979 ` 589` ```lemma IntD2: "c : A Int B ==> c:B" ``` wenzelm@11979 ` 590` ``` by simp ``` wenzelm@11979 ` 591` wenzelm@11979 ` 592` ```lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P" ``` wenzelm@11979 ` 593` ``` by simp ``` wenzelm@11979 ` 594` wenzelm@11979 ` 595` wenzelm@11979 ` 596` ```section {* Set difference *} ``` wenzelm@11979 ` 597` wenzelm@11979 ` 598` ```lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)" ``` wenzelm@11979 ` 599` ``` by (unfold set_diff_def) blast ``` clasohm@923 ` 600` wenzelm@11979 ` 601` ```lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B" ``` wenzelm@11979 ` 602` ``` by simp ``` wenzelm@11979 ` 603` wenzelm@11979 ` 604` ```lemma DiffD1: "c : A - B ==> c : A" ``` wenzelm@11979 ` 605` ``` by simp ``` wenzelm@11979 ` 606` wenzelm@11979 ` 607` ```lemma DiffD2: "c : A - B ==> c : B ==> P" ``` wenzelm@11979 ` 608` ``` by simp ``` wenzelm@11979 ` 609` wenzelm@11979 ` 610` ```lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P" ``` wenzelm@11979 ` 611` ``` by simp ``` wenzelm@11979 ` 612` wenzelm@11979 ` 613` wenzelm@11979 ` 614` ```subsubsection {* Augmenting a set -- insert *} ``` wenzelm@11979 ` 615` wenzelm@11979 ` 616` ```lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)" ``` wenzelm@11979 ` 617` ``` by (unfold insert_def) blast ``` wenzelm@11979 ` 618` wenzelm@11979 ` 619` ```lemma insertI1: "a : insert a B" ``` wenzelm@11979 ` 620` ``` by simp ``` wenzelm@11979 ` 621` wenzelm@11979 ` 622` ```lemma insertI2: "a : B ==> a : insert b B" ``` wenzelm@11979 ` 623` ``` by simp ``` clasohm@923 ` 624` wenzelm@11979 ` 625` ```lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P" ``` wenzelm@11979 ` 626` ``` by (unfold insert_def) blast ``` wenzelm@11979 ` 627` wenzelm@11979 ` 628` ```lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B" ``` wenzelm@11979 ` 629` ``` -- {* Classical introduction rule. *} ``` wenzelm@11979 ` 630` ``` by auto ``` wenzelm@11979 ` 631` wenzelm@11979 ` 632` ```lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)" ``` wenzelm@11979 ` 633` ``` by auto ``` wenzelm@11979 ` 634` wenzelm@11979 ` 635` wenzelm@11979 ` 636` ```subsubsection {* Singletons, using insert *} ``` wenzelm@11979 ` 637` wenzelm@11979 ` 638` ```lemma singletonI [intro!]: "a : {a}" ``` wenzelm@11979 ` 639` ``` -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *} ``` wenzelm@11979 ` 640` ``` by (rule insertI1) ``` wenzelm@11979 ` 641` wenzelm@11979 ` 642` ```lemma singletonD: "b : {a} ==> b = a" ``` wenzelm@11979 ` 643` ``` by blast ``` wenzelm@11979 ` 644` wenzelm@11979 ` 645` ```lemmas singletonE [elim!] = singletonD [elim_format] ``` wenzelm@11979 ` 646` wenzelm@11979 ` 647` ```lemma singleton_iff: "(b : {a}) = (b = a)" ``` wenzelm@11979 ` 648` ``` by blast ``` wenzelm@11979 ` 649` wenzelm@11979 ` 650` ```lemma singleton_inject [dest!]: "{a} = {b} ==> a = b" ``` wenzelm@11979 ` 651` ``` by blast ``` wenzelm@11979 ` 652` wenzelm@11979 ` 653` ```lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})" ``` wenzelm@11979 ` 654` ``` by blast ``` wenzelm@11979 ` 655` wenzelm@11979 ` 656` ```lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})" ``` wenzelm@11979 ` 657` ``` by blast ``` wenzelm@11979 ` 658` wenzelm@11979 ` 659` ```lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}" ``` wenzelm@11979 ` 660` ``` by fast ``` wenzelm@11979 ` 661` wenzelm@11979 ` 662` ```lemma singleton_conv [simp]: "{x. x = a} = {a}" ``` wenzelm@11979 ` 663` ``` by blast ``` wenzelm@11979 ` 664` wenzelm@11979 ` 665` ```lemma singleton_conv2 [simp]: "{x. a = x} = {a}" ``` wenzelm@11979 ` 666` ``` by blast ``` clasohm@923 ` 667` wenzelm@11979 ` 668` ```lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B" ``` wenzelm@11979 ` 669` ``` by blast ``` wenzelm@11979 ` 670` wenzelm@11979 ` 671` wenzelm@11979 ` 672` ```subsubsection {* Unions of families *} ``` wenzelm@11979 ` 673` wenzelm@11979 ` 674` ```text {* ``` wenzelm@11979 ` 675` ``` @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}. ``` wenzelm@11979 ` 676` ```*} ``` wenzelm@11979 ` 677` wenzelm@11979 ` 678` ```lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)" ``` wenzelm@11979 ` 679` ``` by (unfold UNION_def) blast ``` wenzelm@11979 ` 680` wenzelm@11979 ` 681` ```lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)" ``` wenzelm@11979 ` 682` ``` -- {* The order of the premises presupposes that @{term A} is rigid; ``` wenzelm@11979 ` 683` ``` @{term b} may be flexible. *} ``` wenzelm@11979 ` 684` ``` by auto ``` wenzelm@11979 ` 685` wenzelm@11979 ` 686` ```lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R" ``` wenzelm@11979 ` 687` ``` by (unfold UNION_def) blast ``` clasohm@923 ` 688` wenzelm@11979 ` 689` ```lemma UN_cong [cong]: ``` wenzelm@11979 ` 690` ``` "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" ``` wenzelm@11979 ` 691` ``` by (simp add: UNION_def) ``` wenzelm@11979 ` 692` wenzelm@11979 ` 693` wenzelm@11979 ` 694` ```subsubsection {* Intersections of families *} ``` wenzelm@11979 ` 695` wenzelm@11979 ` 696` ```text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *} ``` wenzelm@11979 ` 697` wenzelm@11979 ` 698` ```lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" ``` wenzelm@11979 ` 699` ``` by (unfold INTER_def) blast ``` clasohm@923 ` 700` wenzelm@11979 ` 701` ```lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)" ``` wenzelm@11979 ` 702` ``` by (unfold INTER_def) blast ``` wenzelm@11979 ` 703` wenzelm@11979 ` 704` ```lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a" ``` wenzelm@11979 ` 705` ``` by auto ``` wenzelm@11979 ` 706` wenzelm@11979 ` 707` ```lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R" ``` wenzelm@11979 ` 708` ``` -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *} ``` wenzelm@11979 ` 709` ``` by (unfold INTER_def) blast ``` wenzelm@11979 ` 710` wenzelm@11979 ` 711` ```lemma INT_cong [cong]: ``` wenzelm@11979 ` 712` ``` "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)" ``` wenzelm@11979 ` 713` ``` by (simp add: INTER_def) ``` wenzelm@7238 ` 714` clasohm@923 ` 715` wenzelm@11979 ` 716` ```subsubsection {* Union *} ``` wenzelm@11979 ` 717` wenzelm@11979 ` 718` ```lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)" ``` wenzelm@11979 ` 719` ``` by (unfold Union_def) blast ``` wenzelm@11979 ` 720` wenzelm@11979 ` 721` ```lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C" ``` wenzelm@11979 ` 722` ``` -- {* The order of the premises presupposes that @{term C} is rigid; ``` wenzelm@11979 ` 723` ``` @{term A} may be flexible. *} ``` wenzelm@11979 ` 724` ``` by auto ``` wenzelm@11979 ` 725` wenzelm@11979 ` 726` ```lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R" ``` wenzelm@11979 ` 727` ``` by (unfold Union_def) blast ``` wenzelm@11979 ` 728` wenzelm@11979 ` 729` wenzelm@11979 ` 730` ```subsubsection {* Inter *} ``` wenzelm@11979 ` 731` wenzelm@11979 ` 732` ```lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)" ``` wenzelm@11979 ` 733` ``` by (unfold Inter_def) blast ``` wenzelm@11979 ` 734` wenzelm@11979 ` 735` ```lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" ``` wenzelm@11979 ` 736` ``` by (simp add: Inter_def) ``` wenzelm@11979 ` 737` wenzelm@11979 ` 738` ```text {* ``` wenzelm@11979 ` 739` ``` \medskip A ``destruct'' rule -- every @{term X} in @{term C} ``` wenzelm@11979 ` 740` ``` contains @{term A} as an element, but @{prop "A:X"} can hold when ``` wenzelm@11979 ` 741` ``` @{prop "X:C"} does not! This rule is analogous to @{text spec}. ``` wenzelm@11979 ` 742` ```*} ``` wenzelm@11979 ` 743` wenzelm@11979 ` 744` ```lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X" ``` wenzelm@11979 ` 745` ``` by auto ``` wenzelm@11979 ` 746` wenzelm@11979 ` 747` ```lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" ``` wenzelm@11979 ` 748` ``` -- {* ``Classical'' elimination rule -- does not require proving ``` wenzelm@11979 ` 749` ``` @{prop "X:C"}. *} ``` wenzelm@11979 ` 750` ``` by (unfold Inter_def) blast ``` wenzelm@11979 ` 751` wenzelm@11979 ` 752` ```text {* ``` wenzelm@11979 ` 753` ``` \medskip Image of a set under a function. Frequently @{term b} does ``` wenzelm@11979 ` 754` ``` not have the syntactic form of @{term "f x"}. ``` wenzelm@11979 ` 755` ```*} ``` wenzelm@11979 ` 756` wenzelm@11979 ` 757` ```lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A" ``` wenzelm@11979 ` 758` ``` by (unfold image_def) blast ``` wenzelm@11979 ` 759` wenzelm@11979 ` 760` ```lemma imageI: "x : A ==> f x : f ` A" ``` wenzelm@11979 ` 761` ``` by (rule image_eqI) (rule refl) ``` wenzelm@11979 ` 762` wenzelm@11979 ` 763` ```lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A" ``` wenzelm@11979 ` 764` ``` -- {* This version's more effective when we already have the ``` wenzelm@11979 ` 765` ``` required @{term x}. *} ``` wenzelm@11979 ` 766` ``` by (unfold image_def) blast ``` wenzelm@11979 ` 767` wenzelm@11979 ` 768` ```lemma imageE [elim!]: ``` wenzelm@11979 ` 769` ``` "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P" ``` wenzelm@11979 ` 770` ``` -- {* The eta-expansion gives variable-name preservation. *} ``` wenzelm@11979 ` 771` ``` by (unfold image_def) blast ``` wenzelm@11979 ` 772` wenzelm@11979 ` 773` ```lemma image_Un: "f`(A Un B) = f`A Un f`B" ``` wenzelm@11979 ` 774` ``` by blast ``` wenzelm@11979 ` 775` wenzelm@11979 ` 776` ```lemma image_iff: "(z : f`A) = (EX x:A. z = f x)" ``` wenzelm@11979 ` 777` ``` by blast ``` wenzelm@11979 ` 778` wenzelm@11979 ` 779` ```lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)" ``` wenzelm@11979 ` 780` ``` -- {* This rewrite rule would confuse users if made default. *} ``` wenzelm@11979 ` 781` ``` by blast ``` wenzelm@11979 ` 782` wenzelm@11979 ` 783` ```lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)" ``` wenzelm@11979 ` 784` ``` apply safe ``` wenzelm@11979 ` 785` ``` prefer 2 apply fast ``` wenzelm@11979 ` 786` ``` apply (rule_tac x = "{a. a : A & f a : B}" in exI) ``` wenzelm@11979 ` 787` ``` apply fast ``` wenzelm@11979 ` 788` ``` done ``` wenzelm@11979 ` 789` wenzelm@11979 ` 790` ```lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B" ``` wenzelm@11979 ` 791` ``` -- {* Replaces the three steps @{text subsetI}, @{text imageE}, ``` wenzelm@11979 ` 792` ``` @{text hypsubst}, but breaks too many existing proofs. *} ``` wenzelm@11979 ` 793` ``` by blast ``` wenzelm@11979 ` 794` wenzelm@11979 ` 795` ```text {* ``` wenzelm@11979 ` 796` ``` \medskip Range of a function -- just a translation for image! ``` wenzelm@11979 ` 797` ```*} ``` wenzelm@11979 ` 798` wenzelm@11979 ` 799` ```lemma range_eqI: "b = f x ==> b : range f" ``` wenzelm@11979 ` 800` ``` by simp ``` wenzelm@11979 ` 801` wenzelm@11979 ` 802` ```lemma rangeI: "f x : range f" ``` wenzelm@11979 ` 803` ``` by simp ``` wenzelm@11979 ` 804` wenzelm@11979 ` 805` ```lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P" ``` wenzelm@11979 ` 806` ``` by blast ``` wenzelm@11979 ` 807` wenzelm@11979 ` 808` wenzelm@11979 ` 809` ```subsubsection {* Set reasoning tools *} ``` wenzelm@11979 ` 810` wenzelm@11979 ` 811` ```text {* ``` wenzelm@11979 ` 812` ``` Rewrite rules for boolean case-splitting: faster than @{text ``` wenzelm@11979 ` 813` ``` "split_if [split]"}. ``` wenzelm@11979 ` 814` ```*} ``` wenzelm@11979 ` 815` wenzelm@11979 ` 816` ```lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))" ``` wenzelm@11979 ` 817` ``` by (rule split_if) ``` wenzelm@11979 ` 818` wenzelm@11979 ` 819` ```lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))" ``` wenzelm@11979 ` 820` ``` by (rule split_if) ``` wenzelm@11979 ` 821` wenzelm@11979 ` 822` ```text {* ``` wenzelm@11979 ` 823` ``` Split ifs on either side of the membership relation. Not for @{text ``` wenzelm@11979 ` 824` ``` "[simp]"} -- can cause goals to blow up! ``` wenzelm@11979 ` 825` ```*} ``` wenzelm@11979 ` 826` wenzelm@11979 ` 827` ```lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))" ``` wenzelm@11979 ` 828` ``` by (rule split_if) ``` wenzelm@11979 ` 829` wenzelm@11979 ` 830` ```lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))" ``` wenzelm@11979 ` 831` ``` by (rule split_if) ``` wenzelm@11979 ` 832` wenzelm@11979 ` 833` ```lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 ``` wenzelm@11979 ` 834` wenzelm@11979 ` 835` ```lemmas mem_simps = ``` wenzelm@11979 ` 836` ``` insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff ``` wenzelm@11979 ` 837` ``` mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff ``` wenzelm@11979 ` 838` ``` -- {* Each of these has ALREADY been added @{text "[simp]"} above. *} ``` wenzelm@11979 ` 839` wenzelm@11979 ` 840` ```(*Would like to add these, but the existing code only searches for the ``` wenzelm@11979 ` 841` ``` outer-level constant, which in this case is just "op :"; we instead need ``` wenzelm@11979 ` 842` ``` to use term-nets to associate patterns with rules. Also, if a rule fails to ``` wenzelm@11979 ` 843` ``` apply, then the formula should be kept. ``` wenzelm@11979 ` 844` ``` [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]), ``` wenzelm@11979 ` 845` ``` ("op Int", [IntD1,IntD2]), ``` wenzelm@11979 ` 846` ``` ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] ``` wenzelm@11979 ` 847` ``` *) ``` wenzelm@11979 ` 848` wenzelm@11979 ` 849` ```ML_setup {* ``` wenzelm@11979 ` 850` ``` val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs; ``` wenzelm@11979 ` 851` ``` simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs); ``` wenzelm@11979 ` 852` ```*} ``` wenzelm@11979 ` 853` wenzelm@11979 ` 854` ```declare subset_UNIV [simp] subset_refl [simp] ``` wenzelm@11979 ` 855` wenzelm@11979 ` 856` wenzelm@11979 ` 857` ```subsubsection {* The ``proper subset'' relation *} ``` wenzelm@11979 ` 858` wenzelm@11979 ` 859` ```lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B" ``` wenzelm@11979 ` 860` ``` by (unfold psubset_def) blast ``` wenzelm@11979 ` 861` wenzelm@11979 ` 862` ```lemma psubset_insert_iff: ``` wenzelm@11979 ` 863` ``` "(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)" ``` wenzelm@11979 ` 864` ``` apply (simp add: psubset_def subset_insert_iff) ``` wenzelm@11979 ` 865` ``` apply blast ``` wenzelm@11979 ` 866` ``` done ``` wenzelm@11979 ` 867` wenzelm@11979 ` 868` ```lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)" ``` wenzelm@11979 ` 869` ``` by (simp only: psubset_def) ``` wenzelm@11979 ` 870` wenzelm@11979 ` 871` ```lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B" ``` wenzelm@11979 ` 872` ``` by (simp add: psubset_eq) ``` wenzelm@11979 ` 873` wenzelm@11979 ` 874` ```lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C" ``` wenzelm@11979 ` 875` ``` by (auto simp add: psubset_eq) ``` wenzelm@11979 ` 876` wenzelm@11979 ` 877` ```lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C" ``` wenzelm@11979 ` 878` ``` by (auto simp add: psubset_eq) ``` wenzelm@11979 ` 879` wenzelm@11979 ` 880` ```lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)" ``` wenzelm@11979 ` 881` ``` by (unfold psubset_def) blast ``` wenzelm@11979 ` 882` wenzelm@11979 ` 883` ```lemma atomize_ball: ``` wenzelm@11979 ` 884` ``` "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)" ``` wenzelm@11979 ` 885` ``` by (simp only: Ball_def atomize_all atomize_imp) ``` wenzelm@11979 ` 886` wenzelm@11979 ` 887` ```declare atomize_ball [symmetric, rulify] ``` wenzelm@11979 ` 888` wenzelm@11979 ` 889` wenzelm@11979 ` 890` ```subsection {* Further set-theory lemmas *} ``` wenzelm@11979 ` 891` wenzelm@11979 ` 892` ```use "subset.ML" ``` wenzelm@11979 ` 893` ```use "equalities.ML" ``` wenzelm@11979 ` 894` ```use "mono.ML" ``` wenzelm@11979 ` 895` wenzelm@11982 ` 896` ```lemma Least_mono: ``` wenzelm@11982 ` 897` ``` "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y ``` wenzelm@11982 ` 898` ``` ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" ``` wenzelm@11982 ` 899` ``` -- {* Courtesy of Stephan Merz *} ``` wenzelm@11982 ` 900` ``` apply clarify ``` wenzelm@11982 ` 901` ``` apply (erule_tac P = "%x. x : S" in LeastI2) ``` wenzelm@11982 ` 902` ``` apply fast ``` wenzelm@11982 ` 903` ``` apply (rule LeastI2) ``` wenzelm@11982 ` 904` ``` apply (auto elim: monoD intro!: order_antisym) ``` wenzelm@11982 ` 905` ``` done ``` wenzelm@11982 ` 906` wenzelm@11979 ` 907` ```end ```