src/CCL/Set.thy
changeset 20140 98acc6d0fab6
parent 17456 bcf7544875b2
child 24825 c4f13ab78f9d
     1.1 --- a/src/CCL/Set.thy	Mon Jul 17 18:42:38 2006 +0200
     1.2 +++ b/src/CCL/Set.thy	Tue Jul 18 02:22:38 2006 +0200
     1.3 @@ -72,7 +72,439 @@
     1.4    Inter_def:     "Inter(S)    == (INT x:S. x)"
     1.5    Union_def:     "Union(S)    == (UN x:S. x)"
     1.6  
     1.7 -ML {* use_legacy_bindings (the_context ()) *}
     1.8 +
     1.9 +lemma CollectI: "[| P(a) |] ==> a : {x. P(x)}"
    1.10 +  apply (rule mem_Collect_iff [THEN iffD2])
    1.11 +  apply assumption
    1.12 +  done
    1.13 +
    1.14 +lemma CollectD: "[| a : {x. P(x)} |] ==> P(a)"
    1.15 +  apply (erule mem_Collect_iff [THEN iffD1])
    1.16 +  done
    1.17 +
    1.18 +lemmas CollectE = CollectD [elim_format]
    1.19 +
    1.20 +lemma set_ext: "[| !!x. x:A <-> x:B |] ==> A = B"
    1.21 +  apply (rule set_extension [THEN iffD2])
    1.22 +  apply simp
    1.23 +  done
    1.24 +
    1.25 +
    1.26 +subsection {* Bounded quantifiers *}
    1.27 +
    1.28 +lemma ballI: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
    1.29 +  by (simp add: Ball_def)
    1.30 +
    1.31 +lemma bspec: "[| ALL x:A. P(x);  x:A |] ==> P(x)"
    1.32 +  by (simp add: Ball_def)
    1.33 +
    1.34 +lemma ballE: "[| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q"
    1.35 +  unfolding Ball_def by blast
    1.36 +
    1.37 +lemma bexI: "[| P(x);  x:A |] ==> EX x:A. P(x)"
    1.38 +  unfolding Bex_def by blast
    1.39 +
    1.40 +lemma bexCI: "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A. P(x)"
    1.41 +  unfolding Bex_def by blast
    1.42 +
    1.43 +lemma bexE: "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q"
    1.44 +  unfolding Bex_def by blast
    1.45 +
    1.46 +(*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
    1.47 +lemma ball_rew: "(ALL x:A. True) <-> True"
    1.48 +  by (blast intro: ballI)
    1.49 +
    1.50 +
    1.51 +subsection {* Congruence rules *}
    1.52 +
    1.53 +lemma ball_cong:
    1.54 +  "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
    1.55 +    (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
    1.56 +  by (blast intro: ballI elim: ballE)
    1.57 +
    1.58 +lemma bex_cong:
    1.59 +  "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
    1.60 +    (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
    1.61 +  by (blast intro: bexI elim: bexE)
    1.62 +
    1.63 +
    1.64 +subsection {* Rules for subsets *}
    1.65 +
    1.66 +lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B"
    1.67 +  unfolding subset_def by (blast intro: ballI)
    1.68 +
    1.69 +(*Rule in Modus Ponens style*)
    1.70 +lemma subsetD: "[| A <= B;  c:A |] ==> c:B"
    1.71 +  unfolding subset_def by (blast elim: ballE)
    1.72 +
    1.73 +(*Classical elimination rule*)
    1.74 +lemma subsetCE: "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P"
    1.75 +  by (blast dest: subsetD)
    1.76 +
    1.77 +lemma subset_refl: "A <= A"
    1.78 +  by (blast intro: subsetI)
    1.79 +
    1.80 +lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
    1.81 +  by (blast intro: subsetI dest: subsetD)
    1.82 +
    1.83 +
    1.84 +subsection {* Rules for equality *}
    1.85 +
    1.86 +(*Anti-symmetry of the subset relation*)
    1.87 +lemma subset_antisym: "[| A <= B;  B <= A |] ==> A = B"
    1.88 +  by (blast intro: set_ext dest: subsetD)
    1.89 +
    1.90 +lemmas equalityI = subset_antisym
    1.91 +
    1.92 +(* Equality rules from ZF set theory -- are they appropriate here? *)
    1.93 +lemma equalityD1: "A = B ==> A<=B"
    1.94 +  and equalityD2: "A = B ==> B<=A"
    1.95 +  by (simp_all add: subset_refl)
    1.96 +
    1.97 +lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
    1.98 +  by (simp add: subset_refl)
    1.99 +
   1.100 +lemma equalityCE:
   1.101 +    "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P"
   1.102 +  by (blast elim: equalityE subsetCE)
   1.103 +
   1.104 +lemma trivial_set: "{x. x:A} = A"
   1.105 +  by (blast intro: equalityI subsetI CollectI dest: CollectD)
   1.106 +
   1.107 +
   1.108 +subsection {* Rules for binary union *}
   1.109 +
   1.110 +lemma UnI1: "c:A ==> c : A Un B"
   1.111 +  and UnI2: "c:B ==> c : A Un B"
   1.112 +  unfolding Un_def by (blast intro: CollectI)+
   1.113 +
   1.114 +(*Classical introduction rule: no commitment to A vs B*)
   1.115 +lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B"
   1.116 +  by (blast intro: UnI1 UnI2)
   1.117 +
   1.118 +lemma UnE: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
   1.119 +  unfolding Un_def by (blast dest: CollectD)
   1.120 +
   1.121 +
   1.122 +subsection {* Rules for small intersection *}
   1.123 +
   1.124 +lemma IntI: "[| c:A;  c:B |] ==> c : A Int B"
   1.125 +  unfolding Int_def by (blast intro: CollectI)
   1.126 +
   1.127 +lemma IntD1: "c : A Int B ==> c:A"
   1.128 +  and IntD2: "c : A Int B ==> c:B"
   1.129 +  unfolding Int_def by (blast dest: CollectD)+
   1.130 +
   1.131 +lemma IntE: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
   1.132 +  by (blast dest: IntD1 IntD2)
   1.133 +
   1.134 +
   1.135 +subsection {* Rules for set complement *}
   1.136 +
   1.137 +lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)"
   1.138 +  unfolding Compl_def by (blast intro: CollectI)
   1.139 +
   1.140 +(*This form, with negated conclusion, works well with the Classical prover.
   1.141 +  Negated assumptions behave like formulae on the right side of the notional
   1.142 +  turnstile...*)
   1.143 +lemma ComplD: "[| c : Compl(A) |] ==> ~c:A"
   1.144 +  unfolding Compl_def by (blast dest: CollectD)
   1.145 +
   1.146 +lemmas ComplE = ComplD [elim_format]
   1.147 +
   1.148 +
   1.149 +subsection {* Empty sets *}
   1.150 +
   1.151 +lemma empty_eq: "{x. False} = {}"
   1.152 +  by (simp add: empty_def)
   1.153 +
   1.154 +lemma emptyD: "a : {} ==> P"
   1.155 +  unfolding empty_def by (blast dest: CollectD)
   1.156 +
   1.157 +lemmas emptyE = emptyD [elim_format]
   1.158 +
   1.159 +lemma not_emptyD:
   1.160 +  assumes "~ A={}"
   1.161 +  shows "EX x. x:A"
   1.162 +proof -
   1.163 +  have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"
   1.164 +    by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
   1.165 +  with prems show ?thesis by blast
   1.166 +qed
   1.167 +
   1.168 +
   1.169 +subsection {* Singleton sets *}
   1.170 +
   1.171 +lemma singletonI: "a : {a}"
   1.172 +  unfolding singleton_def by (blast intro: CollectI)
   1.173 +
   1.174 +lemma singletonD: "b : {a} ==> b=a"
   1.175 +  unfolding singleton_def by (blast dest: CollectD)
   1.176 +
   1.177 +lemmas singletonE = singletonD [elim_format]
   1.178 +
   1.179 +
   1.180 +subsection {* Unions of families *}
   1.181 +
   1.182 +(*The order of the premises presupposes that A is rigid; b may be flexible*)
   1.183 +lemma UN_I: "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))"
   1.184 +  unfolding UNION_def by (blast intro: bexI CollectI)
   1.185 +
   1.186 +lemma UN_E: "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R"
   1.187 +  unfolding UNION_def by (blast dest: CollectD elim: bexE)
   1.188 +
   1.189 +lemma UN_cong:
   1.190 +  "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
   1.191 +    (UN x:A. C(x)) = (UN x:B. D(x))"
   1.192 +  by (simp add: UNION_def cong: bex_cong)
   1.193 +
   1.194 +
   1.195 +subsection {* Intersections of families *}
   1.196 +
   1.197 +lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"
   1.198 +  unfolding INTER_def by (blast intro: CollectI ballI)
   1.199 +
   1.200 +lemma INT_D: "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)"
   1.201 +  unfolding INTER_def by (blast dest: CollectD bspec)
   1.202 +
   1.203 +(*"Classical" elimination rule -- does not require proving X:C *)
   1.204 +lemma INT_E: "[| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R"
   1.205 +  unfolding INTER_def by (blast dest: CollectD bspec)
   1.206 +
   1.207 +lemma INT_cong:
   1.208 +  "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
   1.209 +    (INT x:A. C(x)) = (INT x:B. D(x))"
   1.210 +  by (simp add: INTER_def cong: ball_cong)
   1.211 +
   1.212 +
   1.213 +subsection {* Rules for Unions *}
   1.214 +
   1.215 +(*The order of the premises presupposes that C is rigid; A may be flexible*)
   1.216 +lemma UnionI: "[| X:C;  A:X |] ==> A : Union(C)"
   1.217 +  unfolding Union_def by (blast intro: UN_I)
   1.218 +
   1.219 +lemma UnionE: "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R"
   1.220 +  unfolding Union_def by (blast elim: UN_E)
   1.221 +
   1.222 +
   1.223 +subsection {* Rules for Inter *}
   1.224 +
   1.225 +lemma InterI: "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"
   1.226 +  unfolding Inter_def by (blast intro: INT_I)
   1.227 +
   1.228 +(*A "destruct" rule -- every X in C contains A as an element, but
   1.229 +  A:X can hold when X:C does not!  This rule is analogous to "spec". *)
   1.230 +lemma InterD: "[| A : Inter(C);  X:C |] ==> A:X"
   1.231 +  unfolding Inter_def by (blast dest: INT_D)
   1.232 +
   1.233 +(*"Classical" elimination rule -- does not require proving X:C *)
   1.234 +lemma InterE: "[| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R"
   1.235 +  unfolding Inter_def by (blast elim: INT_E)
   1.236 +
   1.237 +
   1.238 +section {* Derived rules involving subsets; Union and Intersection as lattice operations *}
   1.239 +
   1.240 +subsection {* Big Union -- least upper bound of a set *}
   1.241 +
   1.242 +lemma Union_upper: "B:A ==> B <= Union(A)"
   1.243 +  by (blast intro: subsetI UnionI)
   1.244 +
   1.245 +lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"
   1.246 +  by (blast intro: subsetI dest: subsetD elim: UnionE)
   1.247 +
   1.248 +
   1.249 +subsection {* Big Intersection -- greatest lower bound of a set *}
   1.250 +
   1.251 +lemma Inter_lower: "B:A ==> Inter(A) <= B"
   1.252 +  by (blast intro: subsetI dest: InterD)
   1.253 +
   1.254 +lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"
   1.255 +  by (blast intro: subsetI InterI dest: subsetD)
   1.256 +
   1.257 +
   1.258 +subsection {* Finite Union -- the least upper bound of 2 sets *}
   1.259 +
   1.260 +lemma Un_upper1: "A <= A Un B"
   1.261 +  by (blast intro: subsetI UnI1)
   1.262 +
   1.263 +lemma Un_upper2: "B <= A Un B"
   1.264 +  by (blast intro: subsetI UnI2)
   1.265 +
   1.266 +lemma Un_least: "[| A<=C;  B<=C |] ==> A Un B <= C"
   1.267 +  by (blast intro: subsetI elim: UnE dest: subsetD)
   1.268 +
   1.269 +
   1.270 +subsection {* Finite Intersection -- the greatest lower bound of 2 sets *}
   1.271 +
   1.272 +lemma Int_lower1: "A Int B <= A"
   1.273 +  by (blast intro: subsetI elim: IntE)
   1.274 +
   1.275 +lemma Int_lower2: "A Int B <= B"
   1.276 +  by (blast intro: subsetI elim: IntE)
   1.277 +
   1.278 +lemma Int_greatest: "[| C<=A;  C<=B |] ==> C <= A Int B"
   1.279 +  by (blast intro: subsetI IntI dest: subsetD)
   1.280 +
   1.281 +
   1.282 +subsection {* Monotonicity *}
   1.283 +
   1.284 +lemma monoI: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"
   1.285 +  unfolding mono_def by blast
   1.286 +
   1.287 +lemma monoD: "[| mono(f);  A <= B |] ==> f(A) <= f(B)"
   1.288 +  unfolding mono_def by blast
   1.289 +
   1.290 +lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)"
   1.291 +  by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2)
   1.292 +
   1.293 +lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)"
   1.294 +  by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2)
   1.295 +
   1.296 +
   1.297 +subsection {* Automated reasoning setup *}
   1.298 +
   1.299 +lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI
   1.300 +  and [intro] = bexI UnionI UN_I
   1.301 +  and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE
   1.302 +  and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE
   1.303 +
   1.304 +lemma mem_rews:
   1.305 +  "(a : A Un B)   <->  (a:A | a:B)"
   1.306 +  "(a : A Int B)  <->  (a:A & a:B)"
   1.307 +  "(a : Compl(B)) <->  (~a:B)"
   1.308 +  "(a : {b})      <->  (a=b)"
   1.309 +  "(a : {})       <->   False"
   1.310 +  "(a : {x. P(x)}) <->  P(a)"
   1.311 +  by blast+
   1.312 +
   1.313 +lemmas [simp] = trivial_set empty_eq mem_rews
   1.314 +  and [cong] = ball_cong bex_cong INT_cong UN_cong
   1.315 +
   1.316 +
   1.317 +section {* Equalities involving union, intersection, inclusion, etc. *}
   1.318 +
   1.319 +subsection {* Binary Intersection *}
   1.320 +
   1.321 +lemma Int_absorb: "A Int A = A"
   1.322 +  by (blast intro: equalityI)
   1.323 +
   1.324 +lemma Int_commute: "A Int B  =  B Int A"
   1.325 +  by (blast intro: equalityI)
   1.326 +
   1.327 +lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
   1.328 +  by (blast intro: equalityI)
   1.329 +
   1.330 +lemma Int_Un_distrib: "(A Un B) Int C  =  (A Int C) Un (B Int C)"
   1.331 +  by (blast intro: equalityI)
   1.332 +
   1.333 +lemma subset_Int_eq: "(A<=B) <-> (A Int B = A)"
   1.334 +  by (blast intro: equalityI elim: equalityE)
   1.335 +
   1.336 +
   1.337 +subsection {* Binary Union *}
   1.338 +
   1.339 +lemma Un_absorb: "A Un A = A"
   1.340 +  by (blast intro: equalityI)
   1.341 +
   1.342 +lemma Un_commute: "A Un B  =  B Un A"
   1.343 +  by (blast intro: equalityI)
   1.344 +
   1.345 +lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
   1.346 +  by (blast intro: equalityI)
   1.347 +
   1.348 +lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
   1.349 +  by (blast intro: equalityI)
   1.350 +
   1.351 +lemma Un_Int_crazy:
   1.352 +    "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
   1.353 +  by (blast intro: equalityI)
   1.354 +
   1.355 +lemma subset_Un_eq: "(A<=B) <-> (A Un B = B)"
   1.356 +  by (blast intro: equalityI elim: equalityE)
   1.357 +
   1.358 +
   1.359 +subsection {* Simple properties of @{text "Compl"} -- complement of a set *}
   1.360 +
   1.361 +lemma Compl_disjoint: "A Int Compl(A) = {x. False}"
   1.362 +  by (blast intro: equalityI)
   1.363 +
   1.364 +lemma Compl_partition: "A Un Compl(A) = {x. True}"
   1.365 +  by (blast intro: equalityI)
   1.366 +
   1.367 +lemma double_complement: "Compl(Compl(A)) = A"
   1.368 +  by (blast intro: equalityI)
   1.369 +
   1.370 +lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)"
   1.371 +  by (blast intro: equalityI)
   1.372 +
   1.373 +lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)"
   1.374 +  by (blast intro: equalityI)
   1.375 +
   1.376 +lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"
   1.377 +  by (blast intro: equalityI)
   1.378 +
   1.379 +lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"
   1.380 +  by (blast intro: equalityI)
   1.381 +
   1.382 +(*Halmos, Naive Set Theory, page 16.*)
   1.383 +lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)"
   1.384 +  by (blast intro: equalityI elim: equalityE)
   1.385 +
   1.386 +
   1.387 +subsection {* Big Union and Intersection *}
   1.388 +
   1.389 +lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
   1.390 +  by (blast intro: equalityI)
   1.391 +
   1.392 +lemma Union_disjoint:
   1.393 +    "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})"
   1.394 +  by (blast intro: equalityI elim: equalityE)
   1.395 +
   1.396 +lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)"
   1.397 +  by (blast intro: equalityI)
   1.398 +
   1.399 +
   1.400 +subsection {* Unions and Intersections of Families *}
   1.401 +
   1.402 +lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"
   1.403 +  by (blast intro: equalityI)
   1.404 +
   1.405 +(*Look: it has an EXISTENTIAL quantifier*)
   1.406 +lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"
   1.407 +  by (blast intro: equalityI)
   1.408 +
   1.409 +lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)"
   1.410 +  by (blast intro: equalityI)
   1.411 +
   1.412 +lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)"
   1.413 +  by (blast intro: equalityI)
   1.414 +
   1.415 +
   1.416 +section {* Monotonicity of various operations *}
   1.417 +
   1.418 +lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
   1.419 +  by blast
   1.420 +
   1.421 +lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)"
   1.422 +  by blast
   1.423 +
   1.424 +lemma UN_mono:
   1.425 +  "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==>  
   1.426 +    (UN x:A. f(x)) <= (UN x:B. g(x))"
   1.427 +  by blast
   1.428 +
   1.429 +lemma INT_anti_mono:
   1.430 +  "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==>  
   1.431 +    (INT x:A. f(x)) <= (INT x:A. g(x))"
   1.432 +  by blast
   1.433 +
   1.434 +lemma Un_mono: "[| A<=C;  B<=D |] ==> A Un B <= C Un D"
   1.435 +  by blast
   1.436 +
   1.437 +lemma Int_mono: "[| A<=C;  B<=D |] ==> A Int B <= C Int D"
   1.438 +  by blast
   1.439 +
   1.440 +lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)"
   1.441 +  by blast
   1.442  
   1.443  end
   1.444 -