src/CCL/Set.thy
author wenzelm
Tue Jul 18 02:22:38 2006 +0200 (2006-07-18)
changeset 20140 98acc6d0fab6
parent 17456 bcf7544875b2
child 24825 c4f13ab78f9d
permissions -rw-r--r--
removed obsolete ML files;
     1 (*  Title:      CCL/Set.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Extending FOL by a modified version of HOL set theory *}
     6 
     7 theory Set
     8 imports FOL
     9 begin
    10 
    11 global
    12 
    13 typedecl 'a set
    14 arities set :: ("term") "term"
    15 
    16 consts
    17   Collect       :: "['a => o] => 'a set"                    (*comprehension*)
    18   Compl         :: "('a set) => 'a set"                     (*complement*)
    19   Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
    20   Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
    21   Union         :: "(('a set)set) => 'a set"                (*...of a set*)
    22   Inter         :: "(('a set)set) => 'a set"                (*...of a set*)
    23   UNION         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
    24   INTER         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
    25   Ball          :: "['a set, 'a => o] => o"                 (*bounded quants*)
    26   Bex           :: "['a set, 'a => o] => o"                 (*bounded quants*)
    27   mono          :: "['a set => 'b set] => o"                (*monotonicity*)
    28   ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
    29   "<="          :: "['a set, 'a set] => o"              (infixl 50)
    30   singleton     :: "'a => 'a set"                       ("{_}")
    31   empty         :: "'a set"                             ("{}")
    32   "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)
    33 
    34 syntax
    35   "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
    36 
    37   (* Big Intersection / Union *)
    38 
    39   "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
    40   "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
    41 
    42   (* Bounded Quantifiers *)
    43 
    44   "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    45   "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    46 
    47 translations
    48   "{x. P}"      == "Collect(%x. P)"
    49   "INT x:A. B"  == "INTER(A, %x. B)"
    50   "UN x:A. B"   == "UNION(A, %x. B)"
    51   "ALL x:A. P"  == "Ball(A, %x. P)"
    52   "EX x:A. P"   == "Bex(A, %x. P)"
    53 
    54 local
    55 
    56 axioms
    57   mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
    58   set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
    59 
    60 defs
    61   Ball_def:      "Ball(A, P)  == ALL x. x:A --> P(x)"
    62   Bex_def:       "Bex(A, P)   == EX x. x:A & P(x)"
    63   mono_def:      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
    64   subset_def:    "A <= B      == ALL x:A. x:B"
    65   singleton_def: "{a}         == {x. x=a}"
    66   empty_def:     "{}          == {x. False}"
    67   Un_def:        "A Un B      == {x. x:A | x:B}"
    68   Int_def:       "A Int B     == {x. x:A & x:B}"
    69   Compl_def:     "Compl(A)    == {x. ~x:A}"
    70   INTER_def:     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
    71   UNION_def:     "UNION(A, B) == {y. EX x:A. y: B(x)}"
    72   Inter_def:     "Inter(S)    == (INT x:S. x)"
    73   Union_def:     "Union(S)    == (UN x:S. x)"
    74 
    75 
    76 lemma CollectI: "[| P(a) |] ==> a : {x. P(x)}"
    77   apply (rule mem_Collect_iff [THEN iffD2])
    78   apply assumption
    79   done
    80 
    81 lemma CollectD: "[| a : {x. P(x)} |] ==> P(a)"
    82   apply (erule mem_Collect_iff [THEN iffD1])
    83   done
    84 
    85 lemmas CollectE = CollectD [elim_format]
    86 
    87 lemma set_ext: "[| !!x. x:A <-> x:B |] ==> A = B"
    88   apply (rule set_extension [THEN iffD2])
    89   apply simp
    90   done
    91 
    92 
    93 subsection {* Bounded quantifiers *}
    94 
    95 lemma ballI: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
    96   by (simp add: Ball_def)
    97 
    98 lemma bspec: "[| ALL x:A. P(x);  x:A |] ==> P(x)"
    99   by (simp add: Ball_def)
   100 
   101 lemma ballE: "[| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q"
   102   unfolding Ball_def by blast
   103 
   104 lemma bexI: "[| P(x);  x:A |] ==> EX x:A. P(x)"
   105   unfolding Bex_def by blast
   106 
   107 lemma bexCI: "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A. P(x)"
   108   unfolding Bex_def by blast
   109 
   110 lemma bexE: "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q"
   111   unfolding Bex_def by blast
   112 
   113 (*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
   114 lemma ball_rew: "(ALL x:A. True) <-> True"
   115   by (blast intro: ballI)
   116 
   117 
   118 subsection {* Congruence rules *}
   119 
   120 lemma ball_cong:
   121   "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
   122     (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
   123   by (blast intro: ballI elim: ballE)
   124 
   125 lemma bex_cong:
   126   "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
   127     (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
   128   by (blast intro: bexI elim: bexE)
   129 
   130 
   131 subsection {* Rules for subsets *}
   132 
   133 lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B"
   134   unfolding subset_def by (blast intro: ballI)
   135 
   136 (*Rule in Modus Ponens style*)
   137 lemma subsetD: "[| A <= B;  c:A |] ==> c:B"
   138   unfolding subset_def by (blast elim: ballE)
   139 
   140 (*Classical elimination rule*)
   141 lemma subsetCE: "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P"
   142   by (blast dest: subsetD)
   143 
   144 lemma subset_refl: "A <= A"
   145   by (blast intro: subsetI)
   146 
   147 lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
   148   by (blast intro: subsetI dest: subsetD)
   149 
   150 
   151 subsection {* Rules for equality *}
   152 
   153 (*Anti-symmetry of the subset relation*)
   154 lemma subset_antisym: "[| A <= B;  B <= A |] ==> A = B"
   155   by (blast intro: set_ext dest: subsetD)
   156 
   157 lemmas equalityI = subset_antisym
   158 
   159 (* Equality rules from ZF set theory -- are they appropriate here? *)
   160 lemma equalityD1: "A = B ==> A<=B"
   161   and equalityD2: "A = B ==> B<=A"
   162   by (simp_all add: subset_refl)
   163 
   164 lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
   165   by (simp add: subset_refl)
   166 
   167 lemma equalityCE:
   168     "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P"
   169   by (blast elim: equalityE subsetCE)
   170 
   171 lemma trivial_set: "{x. x:A} = A"
   172   by (blast intro: equalityI subsetI CollectI dest: CollectD)
   173 
   174 
   175 subsection {* Rules for binary union *}
   176 
   177 lemma UnI1: "c:A ==> c : A Un B"
   178   and UnI2: "c:B ==> c : A Un B"
   179   unfolding Un_def by (blast intro: CollectI)+
   180 
   181 (*Classical introduction rule: no commitment to A vs B*)
   182 lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B"
   183   by (blast intro: UnI1 UnI2)
   184 
   185 lemma UnE: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
   186   unfolding Un_def by (blast dest: CollectD)
   187 
   188 
   189 subsection {* Rules for small intersection *}
   190 
   191 lemma IntI: "[| c:A;  c:B |] ==> c : A Int B"
   192   unfolding Int_def by (blast intro: CollectI)
   193 
   194 lemma IntD1: "c : A Int B ==> c:A"
   195   and IntD2: "c : A Int B ==> c:B"
   196   unfolding Int_def by (blast dest: CollectD)+
   197 
   198 lemma IntE: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
   199   by (blast dest: IntD1 IntD2)
   200 
   201 
   202 subsection {* Rules for set complement *}
   203 
   204 lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)"
   205   unfolding Compl_def by (blast intro: CollectI)
   206 
   207 (*This form, with negated conclusion, works well with the Classical prover.
   208   Negated assumptions behave like formulae on the right side of the notional
   209   turnstile...*)
   210 lemma ComplD: "[| c : Compl(A) |] ==> ~c:A"
   211   unfolding Compl_def by (blast dest: CollectD)
   212 
   213 lemmas ComplE = ComplD [elim_format]
   214 
   215 
   216 subsection {* Empty sets *}
   217 
   218 lemma empty_eq: "{x. False} = {}"
   219   by (simp add: empty_def)
   220 
   221 lemma emptyD: "a : {} ==> P"
   222   unfolding empty_def by (blast dest: CollectD)
   223 
   224 lemmas emptyE = emptyD [elim_format]
   225 
   226 lemma not_emptyD:
   227   assumes "~ A={}"
   228   shows "EX x. x:A"
   229 proof -
   230   have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"
   231     by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
   232   with prems show ?thesis by blast
   233 qed
   234 
   235 
   236 subsection {* Singleton sets *}
   237 
   238 lemma singletonI: "a : {a}"
   239   unfolding singleton_def by (blast intro: CollectI)
   240 
   241 lemma singletonD: "b : {a} ==> b=a"
   242   unfolding singleton_def by (blast dest: CollectD)
   243 
   244 lemmas singletonE = singletonD [elim_format]
   245 
   246 
   247 subsection {* Unions of families *}
   248 
   249 (*The order of the premises presupposes that A is rigid; b may be flexible*)
   250 lemma UN_I: "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))"
   251   unfolding UNION_def by (blast intro: bexI CollectI)
   252 
   253 lemma UN_E: "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R"
   254   unfolding UNION_def by (blast dest: CollectD elim: bexE)
   255 
   256 lemma UN_cong:
   257   "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
   258     (UN x:A. C(x)) = (UN x:B. D(x))"
   259   by (simp add: UNION_def cong: bex_cong)
   260 
   261 
   262 subsection {* Intersections of families *}
   263 
   264 lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"
   265   unfolding INTER_def by (blast intro: CollectI ballI)
   266 
   267 lemma INT_D: "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)"
   268   unfolding INTER_def by (blast dest: CollectD bspec)
   269 
   270 (*"Classical" elimination rule -- does not require proving X:C *)
   271 lemma INT_E: "[| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R"
   272   unfolding INTER_def by (blast dest: CollectD bspec)
   273 
   274 lemma INT_cong:
   275   "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
   276     (INT x:A. C(x)) = (INT x:B. D(x))"
   277   by (simp add: INTER_def cong: ball_cong)
   278 
   279 
   280 subsection {* Rules for Unions *}
   281 
   282 (*The order of the premises presupposes that C is rigid; A may be flexible*)
   283 lemma UnionI: "[| X:C;  A:X |] ==> A : Union(C)"
   284   unfolding Union_def by (blast intro: UN_I)
   285 
   286 lemma UnionE: "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R"
   287   unfolding Union_def by (blast elim: UN_E)
   288 
   289 
   290 subsection {* Rules for Inter *}
   291 
   292 lemma InterI: "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"
   293   unfolding Inter_def by (blast intro: INT_I)
   294 
   295 (*A "destruct" rule -- every X in C contains A as an element, but
   296   A:X can hold when X:C does not!  This rule is analogous to "spec". *)
   297 lemma InterD: "[| A : Inter(C);  X:C |] ==> A:X"
   298   unfolding Inter_def by (blast dest: INT_D)
   299 
   300 (*"Classical" elimination rule -- does not require proving X:C *)
   301 lemma InterE: "[| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R"
   302   unfolding Inter_def by (blast elim: INT_E)
   303 
   304 
   305 section {* Derived rules involving subsets; Union and Intersection as lattice operations *}
   306 
   307 subsection {* Big Union -- least upper bound of a set *}
   308 
   309 lemma Union_upper: "B:A ==> B <= Union(A)"
   310   by (blast intro: subsetI UnionI)
   311 
   312 lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"
   313   by (blast intro: subsetI dest: subsetD elim: UnionE)
   314 
   315 
   316 subsection {* Big Intersection -- greatest lower bound of a set *}
   317 
   318 lemma Inter_lower: "B:A ==> Inter(A) <= B"
   319   by (blast intro: subsetI dest: InterD)
   320 
   321 lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"
   322   by (blast intro: subsetI InterI dest: subsetD)
   323 
   324 
   325 subsection {* Finite Union -- the least upper bound of 2 sets *}
   326 
   327 lemma Un_upper1: "A <= A Un B"
   328   by (blast intro: subsetI UnI1)
   329 
   330 lemma Un_upper2: "B <= A Un B"
   331   by (blast intro: subsetI UnI2)
   332 
   333 lemma Un_least: "[| A<=C;  B<=C |] ==> A Un B <= C"
   334   by (blast intro: subsetI elim: UnE dest: subsetD)
   335 
   336 
   337 subsection {* Finite Intersection -- the greatest lower bound of 2 sets *}
   338 
   339 lemma Int_lower1: "A Int B <= A"
   340   by (blast intro: subsetI elim: IntE)
   341 
   342 lemma Int_lower2: "A Int B <= B"
   343   by (blast intro: subsetI elim: IntE)
   344 
   345 lemma Int_greatest: "[| C<=A;  C<=B |] ==> C <= A Int B"
   346   by (blast intro: subsetI IntI dest: subsetD)
   347 
   348 
   349 subsection {* Monotonicity *}
   350 
   351 lemma monoI: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"
   352   unfolding mono_def by blast
   353 
   354 lemma monoD: "[| mono(f);  A <= B |] ==> f(A) <= f(B)"
   355   unfolding mono_def by blast
   356 
   357 lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)"
   358   by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2)
   359 
   360 lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)"
   361   by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2)
   362 
   363 
   364 subsection {* Automated reasoning setup *}
   365 
   366 lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI
   367   and [intro] = bexI UnionI UN_I
   368   and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE
   369   and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE
   370 
   371 lemma mem_rews:
   372   "(a : A Un B)   <->  (a:A | a:B)"
   373   "(a : A Int B)  <->  (a:A & a:B)"
   374   "(a : Compl(B)) <->  (~a:B)"
   375   "(a : {b})      <->  (a=b)"
   376   "(a : {})       <->   False"
   377   "(a : {x. P(x)}) <->  P(a)"
   378   by blast+
   379 
   380 lemmas [simp] = trivial_set empty_eq mem_rews
   381   and [cong] = ball_cong bex_cong INT_cong UN_cong
   382 
   383 
   384 section {* Equalities involving union, intersection, inclusion, etc. *}
   385 
   386 subsection {* Binary Intersection *}
   387 
   388 lemma Int_absorb: "A Int A = A"
   389   by (blast intro: equalityI)
   390 
   391 lemma Int_commute: "A Int B  =  B Int A"
   392   by (blast intro: equalityI)
   393 
   394 lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
   395   by (blast intro: equalityI)
   396 
   397 lemma Int_Un_distrib: "(A Un B) Int C  =  (A Int C) Un (B Int C)"
   398   by (blast intro: equalityI)
   399 
   400 lemma subset_Int_eq: "(A<=B) <-> (A Int B = A)"
   401   by (blast intro: equalityI elim: equalityE)
   402 
   403 
   404 subsection {* Binary Union *}
   405 
   406 lemma Un_absorb: "A Un A = A"
   407   by (blast intro: equalityI)
   408 
   409 lemma Un_commute: "A Un B  =  B Un A"
   410   by (blast intro: equalityI)
   411 
   412 lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
   413   by (blast intro: equalityI)
   414 
   415 lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
   416   by (blast intro: equalityI)
   417 
   418 lemma Un_Int_crazy:
   419     "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
   420   by (blast intro: equalityI)
   421 
   422 lemma subset_Un_eq: "(A<=B) <-> (A Un B = B)"
   423   by (blast intro: equalityI elim: equalityE)
   424 
   425 
   426 subsection {* Simple properties of @{text "Compl"} -- complement of a set *}
   427 
   428 lemma Compl_disjoint: "A Int Compl(A) = {x. False}"
   429   by (blast intro: equalityI)
   430 
   431 lemma Compl_partition: "A Un Compl(A) = {x. True}"
   432   by (blast intro: equalityI)
   433 
   434 lemma double_complement: "Compl(Compl(A)) = A"
   435   by (blast intro: equalityI)
   436 
   437 lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)"
   438   by (blast intro: equalityI)
   439 
   440 lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)"
   441   by (blast intro: equalityI)
   442 
   443 lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"
   444   by (blast intro: equalityI)
   445 
   446 lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"
   447   by (blast intro: equalityI)
   448 
   449 (*Halmos, Naive Set Theory, page 16.*)
   450 lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)"
   451   by (blast intro: equalityI elim: equalityE)
   452 
   453 
   454 subsection {* Big Union and Intersection *}
   455 
   456 lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
   457   by (blast intro: equalityI)
   458 
   459 lemma Union_disjoint:
   460     "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})"
   461   by (blast intro: equalityI elim: equalityE)
   462 
   463 lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)"
   464   by (blast intro: equalityI)
   465 
   466 
   467 subsection {* Unions and Intersections of Families *}
   468 
   469 lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"
   470   by (blast intro: equalityI)
   471 
   472 (*Look: it has an EXISTENTIAL quantifier*)
   473 lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"
   474   by (blast intro: equalityI)
   475 
   476 lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)"
   477   by (blast intro: equalityI)
   478 
   479 lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)"
   480   by (blast intro: equalityI)
   481 
   482 
   483 section {* Monotonicity of various operations *}
   484 
   485 lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
   486   by blast
   487 
   488 lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)"
   489   by blast
   490 
   491 lemma UN_mono:
   492   "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==>  
   493     (UN x:A. f(x)) <= (UN x:B. g(x))"
   494   by blast
   495 
   496 lemma INT_anti_mono:
   497   "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==>  
   498     (INT x:A. f(x)) <= (INT x:A. g(x))"
   499   by blast
   500 
   501 lemma Un_mono: "[| A<=C;  B<=D |] ==> A Un B <= C Un D"
   502   by blast
   503 
   504 lemma Int_mono: "[| A<=C;  B<=D |] ==> A Int B <= C Int D"
   505   by blast
   506 
   507 lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)"
   508   by blast
   509 
   510 end