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