src/CCL/equalities.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 757 2ca12511676d
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	CCL/equalities
     2     ID:         $Id$
     3 
     4 Modified version of
     5     Title: 	HOL/equalities
     6     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     7     Copyright   1991  University of Cambridge
     8 
     9 Equalities involving union, intersection, inclusion, etc.
    10 *)
    11 
    12 writeln"File HOL/equalities";
    13 
    14 val eq_cs = set_cs addSIs [equalityI];
    15 
    16 (** Binary Intersection **)
    17 
    18 goal Set.thy "A Int A = A";
    19 by (fast_tac eq_cs 1);
    20 val Int_absorb = result();
    21 
    22 goal Set.thy "A Int B  =  B Int A";
    23 by (fast_tac eq_cs 1);
    24 val Int_commute = result();
    25 
    26 goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
    27 by (fast_tac eq_cs 1);
    28 val Int_assoc = result();
    29 
    30 goal Set.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
    31 by (fast_tac eq_cs 1);
    32 val Int_Un_distrib = result();
    33 
    34 goal Set.thy "(A<=B) <-> (A Int B = A)";
    35 by (fast_tac (eq_cs addSEs [equalityE]) 1);
    36 val subset_Int_eq = result();
    37 
    38 (** Binary Union **)
    39 
    40 goal Set.thy "A Un A = A";
    41 by (fast_tac eq_cs 1);
    42 val Un_absorb = result();
    43 
    44 goal Set.thy "A Un B  =  B Un A";
    45 by (fast_tac eq_cs 1);
    46 val Un_commute = result();
    47 
    48 goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
    49 by (fast_tac eq_cs 1);
    50 val Un_assoc = result();
    51 
    52 goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
    53 by (fast_tac eq_cs 1);
    54 val Un_Int_distrib = result();
    55 
    56 goal Set.thy
    57  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
    58 by (fast_tac eq_cs 1);
    59 val Un_Int_crazy = result();
    60 
    61 goal Set.thy "(A<=B) <-> (A Un B = B)";
    62 by (fast_tac (eq_cs addSEs [equalityE]) 1);
    63 val subset_Un_eq = result();
    64 
    65 (** Simple properties of Compl -- complement of a set **)
    66 
    67 goal Set.thy "A Int Compl(A) = {x.False}";
    68 by (fast_tac eq_cs 1);
    69 val Compl_disjoint = result();
    70 
    71 goal Set.thy "A Un Compl(A) = {x.True}";
    72 by (fast_tac eq_cs 1);
    73 val Compl_partition = result();
    74 
    75 goal Set.thy "Compl(Compl(A)) = A";
    76 by (fast_tac eq_cs 1);
    77 val double_complement = result();
    78 
    79 goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
    80 by (fast_tac eq_cs 1);
    81 val Compl_Un = result();
    82 
    83 goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
    84 by (fast_tac eq_cs 1);
    85 val Compl_Int = result();
    86 
    87 goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
    88 by (fast_tac eq_cs 1);
    89 val Compl_UN = result();
    90 
    91 goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
    92 by (fast_tac eq_cs 1);
    93 val Compl_INT = result();
    94 
    95 (*Halmos, Naive Set Theory, page 16.*)
    96 
    97 goal Set.thy "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)";
    98 by (fast_tac (eq_cs addSEs [equalityE]) 1);
    99 val Un_Int_assoc_eq = result();
   100 
   101 
   102 (** Big Union and Intersection **)
   103 
   104 goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
   105 by (fast_tac eq_cs 1);
   106 val Union_Un_distrib = result();
   107 
   108 val prems = goal Set.thy
   109    "(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
   110 by (fast_tac (eq_cs addSEs [equalityE]) 1);
   111 val Union_disjoint = result();
   112 
   113 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
   114 by (best_tac eq_cs 1);
   115 val Inter_Un_distrib = result();
   116 
   117 (** Unions and Intersections of Families **)
   118 
   119 goal Set.thy "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})";
   120 by (fast_tac eq_cs 1);
   121 val UN_eq = result();
   122 
   123 (*Look: it has an EXISTENTIAL quantifier*)
   124 goal Set.thy "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})";
   125 by (fast_tac eq_cs 1);
   126 val INT_eq = result();
   127 
   128 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
   129 by (fast_tac eq_cs 1);
   130 val Int_Union_image = result();
   131 
   132 goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
   133 by (fast_tac eq_cs 1);
   134 val Un_Inter_image = result();