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.254 +defs (overloaded)
   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.411 +    Addsimprocs [defBALL_regroup, defBEX_regroup]
   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.442 +  fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
   1.443 +*}
   1.444 +
   1.445 +ML "
   1.446 +  (* While (:) is not, its type must be kept
   1.447 +    for overloading of = to work. *)
   1.448 +  Blast.overloaded (\"op :\", domain_type);
   1.449 +
   1.450 +  overload_1st_set \"Ball\";            (*need UNION, INTER also?*)
   1.451 +  overload_1st_set \"Bex\";
   1.452 +
   1.453 +  (*Image: retain the type of the set being expressed*)
   1.454 +  Blast.overloaded (\"image\", domain_type);
   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