src/CCL/equalities.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1459 d12da312eff4
child 3837 d7f033c74b38
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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 qed "Int_absorb";
    21 
    22 goal Set.thy "A Int B  =  B Int A";
    23 by (fast_tac eq_cs 1);
    24 qed "Int_commute";
    25 
    26 goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
    27 by (fast_tac eq_cs 1);
    28 qed "Int_assoc";
    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 qed "Int_Un_distrib";
    33 
    34 goal Set.thy "(A<=B) <-> (A Int B = A)";
    35 by (fast_tac (eq_cs addSEs [equalityE]) 1);
    36 qed "subset_Int_eq";
    37 
    38 (** Binary Union **)
    39 
    40 goal Set.thy "A Un A = A";
    41 by (fast_tac eq_cs 1);
    42 qed "Un_absorb";
    43 
    44 goal Set.thy "A Un B  =  B Un A";
    45 by (fast_tac eq_cs 1);
    46 qed "Un_commute";
    47 
    48 goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
    49 by (fast_tac eq_cs 1);
    50 qed "Un_assoc";
    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 qed "Un_Int_distrib";
    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 qed "Un_Int_crazy";
    60 
    61 goal Set.thy "(A<=B) <-> (A Un B = B)";
    62 by (fast_tac (eq_cs addSEs [equalityE]) 1);
    63 qed "subset_Un_eq";
    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 qed "Compl_disjoint";
    70 
    71 goal Set.thy "A Un Compl(A) = {x.True}";
    72 by (fast_tac eq_cs 1);
    73 qed "Compl_partition";
    74 
    75 goal Set.thy "Compl(Compl(A)) = A";
    76 by (fast_tac eq_cs 1);
    77 qed "double_complement";
    78 
    79 goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
    80 by (fast_tac eq_cs 1);
    81 qed "Compl_Un";
    82 
    83 goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
    84 by (fast_tac eq_cs 1);
    85 qed "Compl_Int";
    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 qed "Compl_UN";
    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 qed "Compl_INT";
    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 qed "Un_Int_assoc_eq";
   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 qed "Union_Un_distrib";
   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 qed "Union_disjoint";
   112 
   113 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
   114 by (best_tac eq_cs 1);
   115 qed "Inter_Un_distrib";
   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 qed "UN_eq";
   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 qed "INT_eq";
   127 
   128 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
   129 by (fast_tac eq_cs 1);
   130 qed "Int_Union_image";
   131 
   132 goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
   133 by (fast_tac eq_cs 1);
   134 qed "Un_Inter_image";