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