src/HOL/Set.thy
 changeset 11979 0a3dace545c5 parent 11752 8941d8d15dc8 child 11982 65e2822d83dd
```     1.1 --- a/src/HOL/Set.thy	Sun Oct 28 22:58:39 2001 +0100
1.2 +++ b/src/HOL/Set.thy	Sun Oct 28 22:59:12 2001 +0100
1.3 @@ -4,70 +4,71 @@
1.4      Copyright   1993  University of Cambridge
1.5  *)
1.6
1.7 -Set = HOL +
1.8 +header {* Set theory for higher-order logic *}
1.9 +
1.10 +theory Set = HOL
1.11 +files ("subset.ML") ("equalities.ML") ("mono.ML"):
1.12 +
1.13 +text {* A set in HOL is simply a predicate. *}
1.14
1.15
1.16 -(** Core syntax **)
1.17 +subsection {* Basic syntax *}
1.18
1.19  global
1.20
1.21 -types
1.22 -  'a set
1.23 -
1.24 -arities
1.25 -  set :: (term) term
1.26 -
1.27 -instance
1.28 -  set :: (term) {ord, minus}
1.29 -
1.30 -syntax
1.31 -  "op :"        :: ['a, 'a set] => bool             ("op :")
1.32 +typedecl 'a set
1.33 +arities set :: ("term") "term"
1.34
1.35  consts
1.36 -  "{}"          :: 'a set                           ("{}")
1.37 -  UNIV          :: 'a set
1.38 -  insert        :: ['a, 'a set] => 'a set
1.39 -  Collect       :: ('a => bool) => 'a set               (*comprehension*)
1.40 -  Int           :: ['a set, 'a set] => 'a set       (infixl 70)
1.41 -  Un            :: ['a set, 'a set] => 'a set       (infixl 65)
1.42 -  UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
1.43 -  Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
1.44 -  Pow           :: 'a set => 'a set set                 (*powerset*)
1.45 -  Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
1.46 -  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "`" 90)
1.47 -  (*membership*)
1.48 -  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
1.49 +  "{}"          :: "'a set"                             ("{}")
1.50 +  UNIV          :: "'a set"
1.51 +  insert        :: "'a => 'a set => 'a set"
1.52 +  Collect       :: "('a => bool) => 'a set"              -- "comprehension"
1.53 +  Int           :: "'a set => 'a set => 'a set"          (infixl 70)
1.54 +  Un            :: "'a set => 'a set => 'a set"          (infixl 65)
1.55 +  UNION         :: "'a set => ('a => 'b set) => 'b set"  -- "general union"
1.56 +  INTER         :: "'a set => ('a => 'b set) => 'b set"  -- "general intersection"
1.57 +  Union         :: "'a set set => 'a set"                -- "union of a set"
1.58 +  Inter         :: "'a set set => 'a set"                -- "intersection of a set"
1.59 +  Pow           :: "'a set => 'a set set"                -- "powerset"
1.60 +  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
1.61 +  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
1.62 +  image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
1.63 +
1.64 +syntax
1.65 +  "op :"        :: "'a => 'a set => bool"                ("op :")
1.66 +consts
1.67 +  "op :"        :: "'a => 'a set => bool"                ("(_/ : _)" [50, 51] 50)  -- "membership"
1.68 +
1.69 +local
1.70 +
1.71 +instance set :: ("term") ord ..
1.72 +instance set :: ("term") minus ..
1.73
1.74
1.75 -(** Additional concrete syntax **)
1.76 +subsection {* Additional concrete syntax *}
1.77
1.78  syntax
1.79 -  range         :: ('a => 'b) => 'b set                 (*of function*)
1.80 -
1.81 -  (* Infix syntax for non-membership *)
1.82 +  range         :: "('a => 'b) => 'b set"             -- "of function"
1.83
1.84 -  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
1.85 -  "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
1.86 -
1.87 +  "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
1.88 +  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ ~: _)" [50, 51] 50)
1.89
1.90 -  "@Finset"     :: args => 'a set                     ("{(_)}")
1.91 -  "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
1.92 -  "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
1.93 -
1.94 -  (* Big Intersection / Union *)
1.95 +  "@Finset"     :: "args => 'a set"                       ("{(_)}")
1.96 +  "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
1.97 +  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
1.98
1.99 -  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3INT _./ _)" 10)
1.100 -  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3UN _./ _)" 10)
1.101 -  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
1.102 -  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
1.103 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" 10)
1.104 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" 10)
1.105 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" 10)
1.106 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" 10)
1.107
1.108 -  (* Bounded Quantifiers *)
1.109 -  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
1.110 -  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
1.111 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
1.112 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
1.113
1.114  syntax (HOL)
1.115 -  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
1.116 -  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
1.117 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
1.118 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
1.119
1.120  translations
1.121    "range f"     == "f`UNIV"
1.122 @@ -85,120 +86,811 @@
1.123    "EX x:A. P"   == "Bex A (%x. P)"
1.124
1.125  syntax ("" output)
1.126 -  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
1.127 -  "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
1.128 -  "_setless"    :: ['a set, 'a set] => bool           ("op <")
1.129 -  "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
1.130 +  "_setle"      :: "'a set => 'a set => bool"             ("op <=")
1.131 +  "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
1.132 +  "_setless"    :: "'a set => 'a set => bool"             ("op <")
1.133 +  "_setless"    :: "'a set => 'a set => bool"             ("(_/ < _)" [50, 51] 50)
1.134
1.135  syntax (symbols)
1.136 -  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
1.137 -  "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
1.138 -  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
1.139 -  "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
1.140 -  "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
1.141 -  "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
1.142 -  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
1.143 -  "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
1.144 -  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
1.145 -  "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
1.146 -  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Union>_./ _)" 10)
1.147 -  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Inter>_./ _)" 10)
1.148 -  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union>_\\<in>_./ _)" 10)
1.149 -  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter>_\\<in>_./ _)" 10)
1.150 -  Union         :: (('a set) set) => 'a set           ("\\<Union>_" [90] 90)
1.151 -  Inter         :: (('a set) set) => 'a set           ("\\<Inter>_" [90] 90)
1.152 -  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10)
1.153 -  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10)
1.154 +  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
1.155 +  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
1.156 +  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
1.157 +  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
1.158 +  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
1.159 +  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
1.160 +  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
1.161 +  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
1.162 +  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
1.163 +  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
1.164 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
1.165 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
1.166 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
1.167 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
1.168 +  Union         :: "'a set set => 'a set"                 ("\<Union>_" [90] 90)
1.169 +  Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
1.170 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
1.171 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
1.172
1.173  translations
1.174 -  "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
1.175 -  "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
1.176 -
1.177 +  "op \<subseteq>" => "op <= :: _ set => _ set => bool"
1.178 +  "op \<subset>" => "op <  :: _ set => _ set => bool"
1.179
1.180
1.181 -(** Rules and definitions **)
1.182 +typed_print_translation {*
1.183 +  let
1.184 +    fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
1.185 +          list_comb (Syntax.const "_setle", ts)
1.186 +      | le_tr' _ _ _ = raise Match;
1.187 +
1.188 +    fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
1.189 +          list_comb (Syntax.const "_setless", ts)
1.190 +      | less_tr' _ _ _ = raise Match;
1.191 +  in [("op <=", le_tr'), ("op <", less_tr')] end
1.192 +*}
1.193
1.194 -local
1.195 +text {*
1.196 +  \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
1.197 +  "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is
1.198 +  only translated if @{text "[0..n] subset bvs(e)"}.
1.199 +*}
1.200 +
1.201 +parse_translation {*
1.202 +  let
1.203 +    val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
1.204
1.205 -rules
1.206 +    fun nvars (Const ("_idts", _) \$ _ \$ idts) = nvars idts + 1
1.207 +      | nvars _ = 1;
1.208 +
1.209 +    fun setcompr_tr [e, idts, b] =
1.210 +      let
1.211 +        val eq = Syntax.const "op =" \$ Bound (nvars idts) \$ e;
1.212 +        val P = Syntax.const "op &" \$ eq \$ b;
1.213 +        val exP = ex_tr [idts, P];
1.214 +      in Syntax.const "Collect" \$ Abs ("", dummyT, exP) end;
1.215 +
1.216 +  in [("@SetCompr", setcompr_tr)] end;
1.217 +*}
1.218
1.219 -  (* Isomorphisms between Predicates and Sets *)
1.220 +print_translation {*
1.221 +  let
1.222 +    val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
1.223 +
1.224 +    fun setcompr_tr' [Abs (_, _, P)] =
1.225 +      let
1.226 +        fun check (Const ("Ex", _) \$ Abs (_, _, P), n) = check (P, n + 1)
1.227 +          | check (Const ("op &", _) \$ (Const ("op =", _) \$ Bound m \$ e) \$ P, n) =
1.228 +              if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
1.229 +                ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then ()
1.230 +              else raise Match;
1.231
1.232 -  mem_Collect_eq    "(a : {x. P(x)}) = P(a)"
1.233 -  Collect_mem_eq    "{x. x:A} = A"
1.234 +        fun tr' (_ \$ abs) =
1.235 +          let val _ \$ idts \$ (_ \$ (_ \$ _ \$ e) \$ Q) = ex_tr' [abs]
1.236 +          in Syntax.const "@SetCompr" \$ e \$ idts \$ Q end;
1.237 +      in check (P, 0); tr' P end;
1.238 +  in [("Collect", setcompr_tr')] end;
1.239 +*}
1.240 +
1.241 +
1.242 +subsection {* Rules and definitions *}
1.243 +
1.244 +text {* Isomorphisms between predicates and sets. *}
1.245
1.246 +axioms
1.247 +  mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
1.248 +  Collect_mem_eq [simp]: "{x. x:A} = A"
1.249 +
1.250 +defs
1.251 +  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
1.252 +  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
1.253 +
1.255 +  subset_def:   "A <= B         == ALL x:A. x:B"
1.256 +  psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B"
1.257 +  Compl_def:    "- A            == {x. ~x:A}"
1.258
1.259  defs
1.260 -  Ball_def      "Ball A P       == ! x. x:A --> P(x)"
1.261 -  Bex_def       "Bex A P        == ? x. x:A & P(x)"
1.262 -  subset_def    "A <= B         == ! x:A. x:B"
1.263 -  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
1.264 -  Compl_def     "- A            == {x. ~x:A}"
1.265 -  Un_def        "A Un B         == {x. x:A | x:B}"
1.266 -  Int_def       "A Int B        == {x. x:A & x:B}"
1.267 -  set_diff_def  "A - B          == {x. x:A & ~x:B}"
1.268 -  INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
1.269 -  UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
1.270 -  Inter_def     "Inter S        == (INT x:S. x)"
1.271 -  Union_def     "Union S        == (UN x:S. x)"
1.272 -  Pow_def       "Pow A          == {B. B <= A}"
1.273 -  empty_def     "{}             == {x. False}"
1.274 -  UNIV_def      "UNIV           == {x. True}"
1.275 -  insert_def    "insert a B     == {x. x=a} Un B"
1.276 -  image_def     "f`A           == {y. ? x:A. y=f(x)}"
1.277 +  Un_def:       "A Un B         == {x. x:A | x:B}"
1.278 +  Int_def:      "A Int B        == {x. x:A & x:B}"
1.279 +  set_diff_def: "A - B          == {x. x:A & ~x:B}"
1.280 +  INTER_def:    "INTER A B      == {y. ALL x:A. y: B(x)}"
1.281 +  UNION_def:    "UNION A B      == {y. EX x:A. y: B(x)}"
1.282 +  Inter_def:    "Inter S        == (INT x:S. x)"
1.283 +  Union_def:    "Union S        == (UN x:S. x)"
1.284 +  Pow_def:      "Pow A          == {B. B <= A}"
1.285 +  empty_def:    "{}             == {x. False}"
1.286 +  UNIV_def:     "UNIV           == {x. True}"
1.287 +  insert_def:   "insert a B     == {x. x=a} Un B"
1.288 +  image_def:    "f`A            == {y. EX x:A. y = f(x)}"
1.289 +
1.290 +
1.291 +subsection {* Lemmas and proof tool setup *}
1.292 +
1.293 +subsubsection {* Relating predicates and sets *}
1.294 +
1.295 +lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}"
1.296 +  by simp
1.297 +
1.298 +lemma CollectD: "a : {x. P(x)} ==> P(a)"
1.299 +  by simp
1.300 +
1.301 +lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B"
1.302 +proof -
1.303 +  case rule_context
1.304 +  show ?thesis
1.305 +    apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals])
1.306 +     apply (rule Collect_mem_eq)
1.307 +    apply (rule Collect_mem_eq)
1.308 +    done
1.309 +qed
1.310 +
1.311 +lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
1.312 +  by simp
1.313 +
1.314 +lemmas CollectE [elim!] = CollectD [elim_format]
1.315 +
1.316 +
1.317 +subsubsection {* Bounded quantifiers *}
1.318 +
1.319 +lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
1.320 +  by (simp add: Ball_def)
1.321 +
1.322 +lemmas strip = impI allI ballI
1.323 +
1.324 +lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
1.325 +  by (simp add: Ball_def)
1.326 +
1.327 +lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
1.328 +  by (unfold Ball_def) blast
1.329 +
1.330 +text {*
1.331 +  \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
1.332 +  @{prop "a:A"}; creates assumption @{prop "P a"}.
1.333 +*}
1.334 +
1.335 +ML {*
1.336 +  local val ballE = thm "ballE"
1.337 +  in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end;
1.338 +*}
1.339 +
1.340 +text {*
1.341 +  Gives better instantiation for bound:
1.342 +*}
1.343 +
1.344 +ML_setup {*
1.345 +  claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1);
1.346 +*}
1.347 +
1.348 +lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
1.349 +  -- {* Normally the best argument order: @{prop "P x"} constrains the
1.350 +    choice of @{prop "x:A"}. *}
1.351 +  by (unfold Bex_def) blast
1.352 +
1.353 +lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x"
1.354 +  -- {* The best argument order when there is only one @{prop "x:A"}. *}
1.355 +  by (unfold Bex_def) blast
1.356 +
1.357 +lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"
1.358 +  by (unfold Bex_def) blast
1.359 +
1.360 +lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q"
1.361 +  by (unfold Bex_def) blast
1.362 +
1.363 +lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"
1.364 +  -- {* Trival rewrite rule. *}
1.365 +  by (simp add: Ball_def)
1.366 +
1.367 +lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"
1.368 +  -- {* Dual form for existentials. *}
1.369 +  by (simp add: Bex_def)
1.370 +
1.371 +lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"
1.372 +  by blast
1.373 +
1.374 +lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
1.375 +  by blast
1.376 +
1.377 +lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
1.378 +  by blast
1.379 +
1.380 +lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)"
1.381 +  by blast
1.382 +
1.383 +lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)"
1.384 +  by blast
1.385 +
1.386 +lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
1.387 +  by blast
1.388 +
1.389 +ML_setup {*
1.390 +  let
1.391 +    val Ball_def = thm "Ball_def";
1.392 +    val Bex_def = thm "Bex_def";
1.393 +
1.394 +    val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
1.395 +      ("EX x:A. P x & Q x", HOLogic.boolT);
1.396 +
1.397 +    val prove_bex_tac =
1.398 +      rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
1.399 +    val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
1.400 +
1.401 +    val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
1.402 +      ("ALL x:A. P x --> Q x", HOLogic.boolT);
1.403 +
1.404 +    val prove_ball_tac =
1.405 +      rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
1.406 +    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
1.407 +
1.408 +    val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
1.409 +    val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
1.410 +  in
1.412 +  end;
1.413 +*}
1.414 +
1.415 +
1.416 +subsubsection {* Congruence rules *}
1.417 +
1.418 +lemma ball_cong [cong]:
1.419 +  "A = B ==> (!!x. x:B ==> P x = Q x) ==>
1.420 +    (ALL x:A. P x) = (ALL x:B. Q x)"
1.421 +  by (simp add: Ball_def)
1.422 +
1.423 +lemma bex_cong [cong]:
1.424 +  "A = B ==> (!!x. x:B ==> P x = Q x) ==>
1.425 +    (EX x:A. P x) = (EX x:B. Q x)"
1.426 +  by (simp add: Bex_def cong: conj_cong)
1.427
1.428
1.429 -end
1.430 +subsubsection {* Subsets *}
1.431 +
1.432 +lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B"
1.433 +  by (simp add: subset_def)
1.434 +
1.435 +text {*
1.436 +  \medskip Map the type @{text "'a set => anything"} to just @{typ
1.437 +  'a}; for overloading constants whose first argument has type @{typ
1.438 +  "'a set"}.
1.439 +*}
1.440 +
1.441 +ML {*
1.443 +*}
1.444 +
1.445 +ML "
1.446 +  (* While (:) is not, its type must be kept
1.448 +  Blast.overloaded (\"op :\", domain_type);
1.449 +
1.450 +  overload_1st_set \"Ball\";            (*need UNION, INTER also?*)
1.452 +
1.453 +  (*Image: retain the type of the set being expressed*)
1.455 +"
1.456 +
1.457 +lemma subsetD [elim]: "A <= B ==> c:A ==> c:B"
1.458 +  -- {* Rule in Modus Ponens style. *}
1.459 +  by (unfold subset_def) blast
1.460 +
1.461 +declare subsetD [intro?] -- FIXME
1.462 +
1.463 +lemma rev_subsetD: "c:A ==> A <= B ==> c:B"
1.464 +  -- {* The same, with reversed premises for use with @{text erule} --
1.465 +      cf @{text rev_mp}. *}
1.466 +  by (rule subsetD)
1.467 +
1.468 +declare rev_subsetD [intro?] -- FIXME
1.469 +
1.470 +text {*
1.471 +  \medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}.
1.472 +*}
1.473 +
1.474 +ML {*
1.475 +  local val rev_subsetD = thm "rev_subsetD"
1.476 +  in fun impOfSubs th = th RSN (2, rev_subsetD) end;
1.477 +*}
1.478 +
1.479 +lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P"
1.480 +  -- {* Classical elimination rule. *}
1.481 +  by (unfold subset_def) blast
1.482 +
1.483 +text {*
1.484 +  \medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and
1.485 +  creates the assumption @{prop "c:B"}.
1.486 +*}
1.487 +
1.488 +ML {*
1.489 +  local val subsetCE = thm "subsetCE"
1.490 +  in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;
1.491 +*}
1.492 +
1.493 +lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A"
1.494 +  by blast
1.495 +
1.496 +lemma subset_refl: "A <= (A::'a set)"
1.497 +  by fast
1.498 +
1.499 +lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)"
1.500 +  by blast
1.501
1.502
1.503 -ML
1.504 +subsubsection {* Equality *}
1.505 +
1.506 +lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)"
1.507 +  -- {* Anti-symmetry of the subset relation. *}
1.508 +  by (rule set_ext) (blast intro: subsetD)
1.509 +
1.510 +lemmas equalityI = subset_antisym
1.511 +
1.512 +text {*
1.513 +  \medskip Equality rules from ZF set theory -- are they appropriate
1.514 +  here?
1.515 +*}
1.516 +
1.517 +lemma equalityD1: "A = B ==> A <= (B::'a set)"
1.518 +  by (simp add: subset_refl)
1.519 +
1.520 +lemma equalityD2: "A = B ==> B <= (A::'a set)"
1.521 +  by (simp add: subset_refl)
1.522 +
1.523 +text {*
1.524 +  \medskip Be careful when adding this to the claset as @{text
1.525 +  subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
1.526 +  <= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}!
1.527 +*}
1.528 +
1.529 +lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P"
1.530 +  by (simp add: subset_refl)
1.531
1.532 -local
1.533 +lemma equalityCE [elim]:
1.534 +    "A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P"
1.535 +  by blast
1.536 +
1.537 +text {*
1.538 +  \medskip Lemma for creating induction formulae -- for "pattern
1.539 +  matching" on @{text p}.  To make the induction hypotheses usable,
1.540 +  apply @{text spec} or @{text bspec} to put universal quantifiers over the free
1.541 +  variables in @{text p}.
1.542 +*}
1.543 +
1.544 +lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R"
1.545 +  by simp
1.546
1.547 -(* Set inclusion *)
1.548 +lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
1.549 +  by simp
1.550 +
1.551 +
1.552 +subsubsection {* The universal set -- UNIV *}
1.553 +
1.554 +lemma UNIV_I [simp]: "x : UNIV"
1.555 +  by (simp add: UNIV_def)
1.556 +
1.557 +declare UNIV_I [intro]  -- {* unsafe makes it less likely to cause problems *}
1.558 +
1.559 +lemma UNIV_witness [intro?]: "EX x. x : UNIV"
1.560 +  by simp
1.561 +
1.562 +lemma subset_UNIV: "A <= UNIV"
1.563 +  by (rule subsetI) (rule UNIV_I)
1.564
1.565 -fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
1.566 -      list_comb (Syntax.const "_setle", ts)
1.567 -  | le_tr' _ (*op <=*) _ _ = raise Match;
1.568 +text {*
1.569 +  \medskip Eta-contracting these two rules (to remove @{text P})
1.570 +  causes them to be ignored because of their interaction with
1.571 +  congruence rules.
1.572 +*}
1.573 +
1.574 +lemma ball_UNIV [simp]: "Ball UNIV P = All P"
1.575 +  by (simp add: Ball_def)
1.576 +
1.577 +lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
1.578 +  by (simp add: Bex_def)
1.579 +
1.580 +
1.581 +subsubsection {* The empty set *}
1.582 +
1.583 +lemma empty_iff [simp]: "(c : {}) = False"
1.584 +  by (simp add: empty_def)
1.585 +
1.586 +lemma emptyE [elim!]: "a : {} ==> P"
1.587 +  by simp
1.588 +
1.589 +lemma empty_subsetI [iff]: "{} <= A"
1.590 +    -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
1.591 +  by blast
1.592 +
1.593 +lemma equals0I: "(!!y. y:A ==> False) ==> A = {}"
1.594 +  by blast
1.595
1.596 -fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
1.597 -      list_comb (Syntax.const "_setless", ts)
1.598 -  | less_tr' _ (*op <*) _ _ = raise Match;
1.599 +lemma equals0D: "A={} ==> a ~: A"
1.600 +    -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
1.601 +  by blast
1.602 +
1.603 +lemma ball_empty [simp]: "Ball {} P = True"
1.604 +  by (simp add: Ball_def)
1.605 +
1.606 +lemma bex_empty [simp]: "Bex {} P = False"
1.607 +  by (simp add: Bex_def)
1.608 +
1.609 +lemma UNIV_not_empty [iff]: "UNIV ~= {}"
1.610 +  by (blast elim: equalityE)
1.611 +
1.612 +
1.613 +section {* The Powerset operator -- Pow *}
1.614 +
1.615 +lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
1.616 +  by (simp add: Pow_def)
1.617 +
1.618 +lemma PowI: "A <= B ==> A : Pow B"
1.619 +  by (simp add: Pow_def)
1.620 +
1.621 +lemma PowD: "A : Pow B ==> A <= B"
1.622 +  by (simp add: Pow_def)
1.623 +
1.624 +lemma Pow_bottom: "{}: Pow B"
1.625 +  by simp
1.626 +
1.627 +lemma Pow_top: "A : Pow A"
1.628 +  by (simp add: subset_refl)
1.629
1.630
1.631 -(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
1.632 -(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
1.633 +subsubsection {* Set complement *}
1.634 +
1.635 +lemma Compl_iff [simp]: "(c : -A) = (c~:A)"
1.636 +  by (unfold Compl_def) blast
1.637 +
1.638 +lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A"
1.639 +  by (unfold Compl_def) blast
1.640 +
1.641 +text {*
1.642 +  \medskip This form, with negated conclusion, works well with the
1.643 +  Classical prover.  Negated assumptions behave like formulae on the
1.644 +  right side of the notional turnstile ... *}
1.645 +
1.646 +lemma ComplD: "c : -A ==> c~:A"
1.647 +  by (unfold Compl_def) blast
1.648 +
1.649 +lemmas ComplE [elim!] = ComplD [elim_format]
1.650 +
1.651 +
1.652 +subsubsection {* Binary union -- Un *}
1.653
1.654 -val ex_tr = snd(mk_binder_tr("EX ","Ex"));
1.655 +lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
1.656 +  by (unfold Un_def) blast
1.657 +
1.658 +lemma UnI1 [elim?]: "c:A ==> c : A Un B"
1.659 +  by simp
1.660 +
1.661 +lemma UnI2 [elim?]: "c:B ==> c : A Un B"
1.662 +  by simp
1.663
1.664 -fun nvars(Const("_idts",_) \$ _ \$ idts) = nvars(idts)+1
1.665 -  | nvars(_) = 1;
1.666 +text {*
1.667 +  \medskip Classical introduction rule: no commitment to @{prop A} vs
1.668 +  @{prop B}.
1.669 +*}
1.670 +
1.671 +lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"
1.672 +  by auto
1.673 +
1.674 +lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
1.675 +  by (unfold Un_def) blast
1.676 +
1.677 +
1.678 +section {* Binary intersection -- Int *}
1.679
1.680 -fun setcompr_tr[e,idts,b] =
1.681 -  let val eq = Syntax.const("op =") \$ Bound(nvars(idts)) \$ e
1.682 -      val P = Syntax.const("op &") \$ eq \$ b
1.683 -      val exP = ex_tr [idts,P]
1.684 -  in Syntax.const("Collect") \$ Abs("",dummyT,exP) end;
1.685 +lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
1.686 +  by (unfold Int_def) blast
1.687 +
1.688 +lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
1.689 +  by simp
1.690 +
1.691 +lemma IntD1: "c : A Int B ==> c:A"
1.692 +  by simp
1.693 +
1.694 +lemma IntD2: "c : A Int B ==> c:B"
1.695 +  by simp
1.696 +
1.697 +lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
1.698 +  by simp
1.699 +
1.700 +
1.701 +section {* Set difference *}
1.702 +
1.703 +lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
1.704 +  by (unfold set_diff_def) blast
1.705
1.706 -val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
1.707 +lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
1.708 +  by simp
1.709 +
1.710 +lemma DiffD1: "c : A - B ==> c : A"
1.711 +  by simp
1.712 +
1.713 +lemma DiffD2: "c : A - B ==> c : B ==> P"
1.714 +  by simp
1.715 +
1.716 +lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"
1.717 +  by simp
1.718 +
1.719 +
1.720 +subsubsection {* Augmenting a set -- insert *}
1.721 +
1.722 +lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
1.723 +  by (unfold insert_def) blast
1.724 +
1.725 +lemma insertI1: "a : insert a B"
1.726 +  by simp
1.727 +
1.728 +lemma insertI2: "a : B ==> a : insert b B"
1.729 +  by simp
1.730
1.731 -fun setcompr_tr'[Abs(_,_,P)] =
1.732 -  let fun ok(Const("Ex",_)\$Abs(_,_,P),n) = ok(P,n+1)
1.733 -        | ok(Const("op &",_) \$ (Const("op =",_) \$ Bound(m) \$ e) \$ P, n) =
1.734 -            if n>0 andalso m=n andalso not(loose_bvar1(P,n)) andalso
1.735 -               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
1.736 -            then () else raise Match
1.737 +lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"
1.738 +  by (unfold insert_def) blast
1.739 +
1.740 +lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
1.741 +  -- {* Classical introduction rule. *}
1.742 +  by auto
1.743 +
1.744 +lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)"
1.745 +  by auto
1.746 +
1.747 +
1.748 +subsubsection {* Singletons, using insert *}
1.749 +
1.750 +lemma singletonI [intro!]: "a : {a}"
1.751 +    -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
1.752 +  by (rule insertI1)
1.753 +
1.754 +lemma singletonD: "b : {a} ==> b = a"
1.755 +  by blast
1.756 +
1.757 +lemmas singletonE [elim!] = singletonD [elim_format]
1.758 +
1.759 +lemma singleton_iff: "(b : {a}) = (b = a)"
1.760 +  by blast
1.761 +
1.762 +lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
1.763 +  by blast
1.764 +
1.765 +lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})"
1.766 +  by blast
1.767 +
1.768 +lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})"
1.769 +  by blast
1.770 +
1.771 +lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}"
1.772 +  by fast
1.773 +
1.774 +lemma singleton_conv [simp]: "{x. x = a} = {a}"
1.775 +  by blast
1.776 +
1.777 +lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
1.778 +  by blast
1.779
1.780 -      fun tr'(_ \$ abs) =
1.781 -        let val _ \$ idts \$ (_ \$ (_ \$ _ \$ e) \$ Q) = ex_tr'[abs]
1.782 -        in Syntax.const("@SetCompr") \$ e \$ idts \$ Q end
1.783 -  in ok(P,0); tr'(P) end;
1.784 +lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B"
1.785 +  by blast
1.786 +
1.787 +
1.788 +subsubsection {* Unions of families *}
1.789 +
1.790 +text {*
1.791 +  @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
1.792 +*}
1.793 +
1.794 +lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
1.795 +  by (unfold UNION_def) blast
1.796 +
1.797 +lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"
1.798 +  -- {* The order of the premises presupposes that @{term A} is rigid;
1.799 +    @{term b} may be flexible. *}
1.800 +  by auto
1.801 +
1.802 +lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"
1.803 +  by (unfold UNION_def) blast
1.804
1.805 -in
1.806 +lemma UN_cong [cong]:
1.807 +    "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
1.808 +  by (simp add: UNION_def)
1.809 +
1.810 +
1.811 +subsubsection {* Intersections of families *}
1.812 +
1.813 +text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *}
1.814 +
1.815 +lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
1.816 +  by (unfold INTER_def) blast
1.817
1.818 -val parse_translation = [("@SetCompr", setcompr_tr)];
1.819 -val print_translation = [("Collect", setcompr_tr')];
1.820 -val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
1.821 +lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
1.822 +  by (unfold INTER_def) blast
1.823 +
1.824 +lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
1.825 +  by auto
1.826 +
1.827 +lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
1.828 +  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
1.829 +  by (unfold INTER_def) blast
1.830 +
1.831 +lemma INT_cong [cong]:
1.832 +    "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
1.833 +  by (simp add: INTER_def)
1.834
1.835
1.836 -end;
1.837 +subsubsection {* Union *}
1.838 +
1.839 +lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)"
1.840 +  by (unfold Union_def) blast
1.841 +
1.842 +lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
1.843 +  -- {* The order of the premises presupposes that @{term C} is rigid;
1.844 +    @{term A} may be flexible. *}
1.845 +  by auto
1.846 +
1.847 +lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
1.848 +  by (unfold Union_def) blast
1.849 +
1.850 +
1.851 +subsubsection {* Inter *}
1.852 +
1.853 +lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)"
1.854 +  by (unfold Inter_def) blast
1.855 +
1.856 +lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
1.857 +  by (simp add: Inter_def)
1.858 +
1.859 +text {*
1.860 +  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
1.861 +  contains @{term A} as an element, but @{prop "A:X"} can hold when
1.862 +  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
1.863 +*}
1.864 +
1.865 +lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
1.866 +  by auto
1.867 +
1.868 +lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
1.869 +  -- {* ``Classical'' elimination rule -- does not require proving
1.870 +    @{prop "X:C"}. *}
1.871 +  by (unfold Inter_def) blast
1.872 +
1.873 +text {*
1.874 +  \medskip Image of a set under a function.  Frequently @{term b} does
1.875 +  not have the syntactic form of @{term "f x"}.
1.876 +*}
1.877 +
1.878 +lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
1.879 +  by (unfold image_def) blast
1.880 +
1.881 +lemma imageI: "x : A ==> f x : f ` A"
1.882 +  by (rule image_eqI) (rule refl)
1.883 +
1.884 +lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
1.885 +  -- {* This version's more effective when we already have the
1.886 +    required @{term x}. *}
1.887 +  by (unfold image_def) blast
1.888 +
1.889 +lemma imageE [elim!]:
1.890 +  "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
1.891 +  -- {* The eta-expansion gives variable-name preservation. *}
1.892 +  by (unfold image_def) blast
1.893 +
1.894 +lemma image_Un: "f`(A Un B) = f`A Un f`B"
1.895 +  by blast
1.896 +
1.897 +lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
1.898 +  by blast
1.899 +
1.900 +lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)"
1.901 +  -- {* This rewrite rule would confuse users if made default. *}
1.902 +  by blast
1.903 +
1.904 +lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)"
1.905 +  apply safe
1.906 +   prefer 2 apply fast
1.907 +  apply (rule_tac x = "{a. a : A & f a : B}" in exI)
1.908 +  apply fast
1.909 +  done
1.910 +
1.911 +lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B"
1.912 +  -- {* Replaces the three steps @{text subsetI}, @{text imageE},
1.913 +    @{text hypsubst}, but breaks too many existing proofs. *}
1.914 +  by blast
1.915 +
1.916 +text {*
1.917 +  \medskip Range of a function -- just a translation for image!
1.918 +*}
1.919 +
1.920 +lemma range_eqI: "b = f x ==> b : range f"
1.921 +  by simp
1.922 +
1.923 +lemma rangeI: "f x : range f"
1.924 +  by simp
1.925 +
1.926 +lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P"
1.927 +  by blast
1.928 +
1.929 +
1.930 +subsubsection {* Set reasoning tools *}
1.931 +
1.932 +text {*
1.933 +  Rewrite rules for boolean case-splitting: faster than @{text
1.934 +  "split_if [split]"}.
1.935 +*}
1.936 +
1.937 +lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
1.938 +  by (rule split_if)
1.939 +
1.940 +lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
1.941 +  by (rule split_if)
1.942 +
1.943 +text {*
1.944 +  Split ifs on either side of the membership relation.  Not for @{text
1.945 +  "[simp]"} -- can cause goals to blow up!
1.946 +*}
1.947 +
1.948 +lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
1.949 +  by (rule split_if)
1.950 +
1.951 +lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
1.952 +  by (rule split_if)
1.953 +
1.954 +lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
1.955 +
1.956 +lemmas mem_simps =
1.957 +  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
1.958 +  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
1.959 +  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
1.960 +
1.961 +(*Would like to add these, but the existing code only searches for the
1.962 +  outer-level constant, which in this case is just "op :"; we instead need
1.963 +  to use term-nets to associate patterns with rules.  Also, if a rule fails to
1.964 +  apply, then the formula should be kept.
1.965 +  [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]),
1.966 +   ("op Int", [IntD1,IntD2]),
1.967 +   ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
1.968 + *)
1.969 +
1.970 +ML_setup {*
1.971 +  val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;
1.972 +  simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
1.973 +*}
1.974 +
1.975 +declare subset_UNIV [simp] subset_refl [simp]
1.976 +
1.977 +
1.978 +subsubsection {* The ``proper subset'' relation *}
1.979 +
1.980 +lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B"
1.981 +  by (unfold psubset_def) blast
1.982 +
1.983 +lemma psubset_insert_iff:
1.984 +  "(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)"
1.985 +  apply (simp add: psubset_def subset_insert_iff)
1.986 +  apply blast
1.987 +  done
1.988 +
1.989 +lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)"
1.990 +  by (simp only: psubset_def)
1.991 +
1.992 +lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B"
1.993 +  by (simp add: psubset_eq)
1.994 +
1.995 +lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C"
1.996 +  by (auto simp add: psubset_eq)
1.997 +
1.998 +lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C"
1.999 +  by (auto simp add: psubset_eq)
1.1000 +
1.1001 +lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)"
1.1002 +  by (unfold psubset_def) blast
1.1003 +
1.1004 +lemma atomize_ball:
1.1005 +    "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)"
1.1006 +  by (simp only: Ball_def atomize_all atomize_imp)
1.1007 +
1.1008 +declare atomize_ball [symmetric, rulify]
1.1009 +
1.1010 +
1.1011 +subsection {* Further set-theory lemmas *}
1.1012 +
1.1013 +use "subset.ML"
1.1014 +use "equalities.ML"
1.1015 +use "mono.ML"
1.1016 +
1.1017 +end
```