src/ZF/equalities.ML
author paulson
Thu, 13 Jul 2000 13:02:20 +0200
changeset 9303 f1ad1ed0d110
parent 9180 3bda56c0d70d
child 9907 473a6604da94
permissions -rw-r--r--
fixed a failing proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1056
diff changeset
     1
(*  Title:      ZF/equalities
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1056
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Set Theory examples: Union, Intersection, Inclusion, etc.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
    (Thanks also to Philippe de Groote.)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
(** Finite Sets **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
520
806d3f00590d ZF/equalities/Sigma_cons: new
lcp
parents: 517
diff changeset
    12
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    13
Goal "{a} Un B = cons(a,B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    14
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    15
qed "cons_eq";
520
806d3f00590d ZF/equalities/Sigma_cons: new
lcp
parents: 517
diff changeset
    16
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    17
Goal "cons(a, cons(b, C)) = cons(b, cons(a, C))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    18
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    19
qed "cons_commute";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    21
Goal "a: B ==> cons(a,B) = B";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    22
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    23
qed "cons_absorb";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    25
Goal "a: B ==> cons(a, B-{a}) = B";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    26
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    27
qed "cons_Diff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    29
Goal "[| a: C;  ALL y:C. y=b |] ==> C = {b}";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    30
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    31
qed "equal_singleton_lemma";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
val equal_singleton = ballI RSN (2,equal_singleton_lemma);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(** Binary Intersection **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
(*NOT an equality, but it seems to belong here...*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    38
Goal "cons(a,B) Int C <= cons(a, B Int C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    39
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    40
qed "Int_cons";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    42
Goal "A Int A = A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    43
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    44
qed "Int_absorb";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    46
Goal "A Int B = B Int A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    47
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    48
qed "Int_commute";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    50
Goal "(A Int B) Int C  =  A Int (B Int C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    51
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    52
qed "Int_assoc";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    54
Goal "(A Un B) Int C  =  (A Int C) Un (B Int C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    55
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    56
qed "Int_Un_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    58
Goal "A<=B <-> A Int B = A";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2925
diff changeset
    59
by (blast_tac (claset() addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    60
qed "subset_Int_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    62
Goal "A<=B <-> B Int A = A";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2925
diff changeset
    63
by (blast_tac (claset() addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    64
qed "subset_Int_iff2";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    65
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    66
Goal "C<=A ==> (A-B) Int C = C-B";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    67
by (Blast_tac 1);
1035
279a4fd3c5ce Proved Int_Diff_eq.
lcp
parents: 839
diff changeset
    68
qed "Int_Diff_eq";
279a4fd3c5ce Proved Int_Diff_eq.
lcp
parents: 839
diff changeset
    69
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(** Binary Union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    72
Goal "cons(a,B) Un C = cons(a, B Un C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    73
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    74
qed "Un_cons";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    76
Goal "A Un A = A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    77
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    78
qed "Un_absorb";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    80
Goal "A Un B = B Un A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    81
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    82
qed "Un_commute";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    84
Goal "(A Un B) Un C  =  A Un (B Un C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    85
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    86
qed "Un_assoc";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    88
Goal "(A Int B) Un C  =  (A Un C) Int (B Un C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    89
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    90
qed "Un_Int_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    92
Goal "A<=B <-> A Un B = B";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2925
diff changeset
    93
by (blast_tac (claset() addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    94
qed "subset_Un_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    96
Goal "A<=B <-> B Un A = B";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2925
diff changeset
    97
by (blast_tac (claset() addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    98
qed "subset_Un_iff2";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    99
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(** Simple properties of Diff -- set difference **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   102
Goal "A-A = 0";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   103
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   104
qed "Diff_cancel";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   106
Goal "0-A = 0";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   107
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   108
qed "empty_Diff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   110
Goal "A-0 = A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   111
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   112
qed "Diff_0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   114
Goal "A-B=0 <-> A<=B";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2925
diff changeset
   115
by (blast_tac (claset() addEs [equalityE]) 1);
787
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   116
qed "Diff_eq_0_iff";
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   117
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   119
Goal "A - cons(a,B) = A - B - {a}";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   120
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   121
qed "Diff_cons";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   124
Goal "A - cons(a,B) = A - {a} - B";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   125
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   126
qed "Diff_cons2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   128
Goal "A Int (B-A) = 0";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   129
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   130
qed "Diff_disjoint";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   132
Goal "A<=B ==> A Un (B-A) = B";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   133
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   134
qed "Diff_partition";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   136
Goal "A <= B Un (A - B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   137
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   138
qed "subset_Un_Diff";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   139
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   140
Goal "[| A<=B; B<=C |] ==> B-(C-A) = A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   141
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   142
qed "double_complement";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   144
Goal "(A Un B) - (B-A) = A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   145
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   146
qed "double_complement_Un";
268
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   147
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   148
Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   150
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   151
qed "Un_Int_crazy";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   153
Goal "A - (B Un C) = (A-B) Int (A-C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   154
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   155
qed "Diff_Un";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   157
Goal "A - (B Int C) = (A-B) Un (A-C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   158
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   159
qed "Diff_Int";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
(*Halmos, Naive Set Theory, page 16.*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   162
Goal "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2925
diff changeset
   163
by (blast_tac (claset() addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   164
qed "Un_Int_assoc_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
(** Big Union and Intersection **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   169
Goal "Union(cons(a,B)) = a Un Union(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   170
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   171
qed "Union_cons";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   173
Goal "Union(A Un B) = Union(A) Un Union(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   174
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   175
qed "Union_Un_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   177
Goal "Union(A Int B) <= Union(A) Int Union(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   178
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   179
qed "Union_Int_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   180
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   181
Goal "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2925
diff changeset
   182
by (blast_tac (claset() addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   183
qed "Union_disjoint";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5321
diff changeset
   185
Goal "Union(A) = 0 <-> (ALL B:A. B=0)";
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5321
diff changeset
   186
by (Blast_tac 1);
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5321
diff changeset
   187
qed "Union_empty_iff";
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5321
diff changeset
   188
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5321
diff changeset
   189
Goalw [Inter_def] "Inter(0) = 0";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   190
by (Blast_tac 1);
1652
9b78ce58d6b1 Proved Inter_0 and converse_INT
paulson
parents: 1611
diff changeset
   191
qed "Inter_0";
9b78ce58d6b1 Proved Inter_0 and converse_INT
paulson
parents: 1611
diff changeset
   192
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   193
Goal "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   194
by (Blast_tac 1);
1568
630d881b51bd New theorem: Inter_Un_subset
paulson
parents: 1461
diff changeset
   195
qed "Inter_Un_subset";
630d881b51bd New theorem: Inter_Un_subset
paulson
parents: 1461
diff changeset
   196
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
(* A good challenge: Inter is ill-behaved on the empty set *)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   198
Goal "[| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   199
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   200
qed "Inter_Un_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   202
Goal "Union({b}) = b";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   203
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   204
qed "Union_singleton";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   206
Goal "Inter({b}) = b";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   207
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   208
qed "Inter_singleton";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
(** Unions and Intersections of Families **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   212
Goal "Union(A) = (UN x:A. x)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   213
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   214
qed "Union_eq_UN";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5321
diff changeset
   216
Goalw [Inter_def] "Inter(A) = (INT x:A. x)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   217
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   218
qed "Inter_eq_INT";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   220
Goal "(UN i:0. A(i)) = 0";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   221
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   222
qed "UN_0";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   223
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
(*Halmos, Naive Set Theory, page 35.*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   225
Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   226
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   227
qed "Int_UN_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   229
Goal "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   230
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   231
qed "Un_INT_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   233
Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   234
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   235
qed "Int_UN_distrib2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   237
Goal "[| i:I;  j:J |] ==> \
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   238
\     (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   239
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   240
qed "Un_INT_distrib2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   242
Goal "a: A ==> (UN y:A. c) = c";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   243
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   244
qed "UN_constant";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   246
Goal "a: A ==> (INT y:A. c) = c";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   247
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   248
qed "INT_constant";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   250
Goal "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
4242
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   251
by (Blast_tac 1);
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   252
qed "UN_RepFun";
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   253
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   254
Goal "x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
4242
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   255
by (Blast_tac 1);
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   256
qed "INT_RepFun";
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   257
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   258
Addsimps [UN_RepFun, INT_RepFun];
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   259
97601cf26262 Two new rewrites
paulson
parents: 4091
diff changeset
   260
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
    Union of a family of unions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   264
Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   265
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   266
qed "UN_Un_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   268
Goal "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   269
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   270
qed "INT_Int_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   272
Goal "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   273
by (Blast_tac 1);
1784
036a7f301623 Added a new theorem, UN_Int_subset
paulson
parents: 1652
diff changeset
   274
qed "UN_Int_subset";
036a7f301623 Added a new theorem, UN_Int_subset
paulson
parents: 1652
diff changeset
   275
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
(** Devlin, page 12, exercise 5: Complements **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   278
Goal "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   279
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   280
qed "Diff_UN";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   282
Goal "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   283
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   284
qed "Diff_INT";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
(** Unions and Intersections with General Sum **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   288
(*Not suitable for rewriting: LOOPS!*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   289
Goal "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   290
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   291
qed "Sigma_cons1";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   292
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   293
(*Not suitable for rewriting: LOOPS!*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   294
Goal "A * cons(b,B) = A*{b} Un A*B";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   295
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   296
qed "Sigma_cons2";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   297
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   298
Goal "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   299
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   300
qed "Sigma_succ1";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   301
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   302
Goal "A * succ(B) = A*{B} Un A*B";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   303
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   304
qed "Sigma_succ2";
520
806d3f00590d ZF/equalities/Sigma_cons: new
lcp
parents: 517
diff changeset
   305
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   306
Goal "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   307
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   308
qed "SUM_UN_distrib1";
182
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   309
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   310
Goal "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   311
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   312
qed "SUM_UN_distrib2";
182
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   313
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   314
Goal "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   315
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   316
qed "SUM_Un_distrib1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   318
Goal "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   319
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   320
qed "SUM_Un_distrib2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   322
(*First-order version of the above, for rewriting*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   323
Goal "I * (A Un B) = I*A Un I*B";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1056
diff changeset
   324
by (rtac SUM_Un_distrib2 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   325
qed "prod_Un_distrib2";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   326
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   327
Goal "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   328
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   329
qed "SUM_Int_distrib1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   331
Goal "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   332
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   333
qed "SUM_Int_distrib2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   335
(*First-order version of the above, for rewriting*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   336
Goal "I * (A Int B) = I*A Int I*B";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1056
diff changeset
   337
by (rtac SUM_Int_distrib2 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   338
qed "prod_Int_distrib2";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   339
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   340
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   341
Goal "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   342
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   343
qed "SUM_eq_UN";
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   344
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   345
(** Domain **)
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   346
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   347
Goal "b:B ==> domain(A*B) = A";
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   348
by (Blast_tac 1);
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   349
qed "domain_of_prod";
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   350
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   351
Goal "domain(0) = 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   352
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   353
qed "domain_0";
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   354
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   355
Goal "domain(cons(<a,b>,r)) = cons(a, domain(r))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   356
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   357
qed "domain_cons";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   359
Goal "domain(A Un B) = domain(A) Un domain(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   360
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   361
qed "domain_Un_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   363
Goal "domain(A Int B) <= domain(A) Int domain(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   364
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   365
qed "domain_Int_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   367
Goal "domain(A) - domain(B) <= domain(A - B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   368
by (Blast_tac 1);
1056
097b3255bf3a Renamed domain_diff_subset, range_diff_subset,
lcp
parents: 1035
diff changeset
   369
qed "domain_Diff_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   371
Goal "domain(converse(r)) = range(r)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   372
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   373
qed "domain_converse";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   374
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   375
Addsimps [domain_0, domain_cons, domain_Un_eq, domain_converse];
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   376
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   377
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   378
(** Range **)
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   379
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   380
Goal "a:A ==> range(A*B) = B";
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   381
by (Blast_tac 1);
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   382
qed "range_of_prod";
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   383
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   384
Goal "range(0) = 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   385
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   386
qed "range_0"; 
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   387
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   388
Goal "range(cons(<a,b>,r)) = cons(b, range(r))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   389
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   390
qed "range_cons";
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   391
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   392
Goal "range(A Un B) = range(A) Un range(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   393
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   394
qed "range_Un_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   396
Goal "range(A Int B) <= range(A) Int range(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   397
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   398
qed "range_Int_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   400
Goal "range(A) - range(B) <= range(A - B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   401
by (Blast_tac 1);
1056
097b3255bf3a Renamed domain_diff_subset, range_diff_subset,
lcp
parents: 1035
diff changeset
   402
qed "range_Diff_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   404
Goal "range(converse(r)) = domain(r)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   405
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   406
qed "range_converse";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   407
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   408
Addsimps [range_0, range_cons, range_Un_eq, range_converse];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   409
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   410
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   411
(** Field **)
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   412
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   413
Goal "field(A*A) = A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   414
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   415
qed "field_of_prod"; 
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   416
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   417
Goal "field(0) = 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   418
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   419
qed "field_0"; 
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   420
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   421
Goal "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   422
by (rtac equalityI 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   423
by (ALLGOALS Blast_tac) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 6298
diff changeset
   424
qed "field_cons";
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   425
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   426
Goal "field(A Un B) = field(A) Un field(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   427
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   428
qed "field_Un_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   430
Goal "field(A Int B) <= field(A) Int field(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   431
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   432
qed "field_Int_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   434
Goal "field(A) - field(B) <= field(A - B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   435
by (Blast_tac 1);
1056
097b3255bf3a Renamed domain_diff_subset, range_diff_subset,
lcp
parents: 1035
diff changeset
   436
qed "field_Diff_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   438
Goal "field(converse(r)) = field(r)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   439
by (Blast_tac 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   440
qed "field_converse";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   441
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   442
Addsimps [field_0, field_cons, field_Un_eq, field_converse];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   443
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   445
(** Image **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   446
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   447
Goal "r``0 = 0";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   448
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   449
qed "image_0";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   450
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   451
Goal "r``(A Un B) = (r``A) Un (r``B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   452
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   453
qed "image_Un";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   454
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   455
Goal "r``(A Int B) <= (r``A) Int (r``B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   456
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   457
qed "image_Int_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   458
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   459
Goal "(r Int A*A)``B <= (r``B) Int A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   460
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   461
qed "image_Int_square_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   462
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   463
Goal "B<=A ==> (r Int A*A)``B = (r``B) Int A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   464
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   465
qed "image_Int_square";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   466
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   467
Addsimps [image_0, image_Un];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   468
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   469
(*Image laws for special relations*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   470
Goal "0``A = 0";
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   471
by (Blast_tac 1);
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   472
qed "image_0_left";
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   473
Addsimps [image_0_left];
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   474
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   475
Goal "(r Un s)``A = (r``A) Un (s``A)";
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   476
by (Blast_tac 1);
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   477
qed "image_Un_left";
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   478
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   479
Goal "(r Int s)``A <= (r``A) Int (s``A)";
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   480
by (Blast_tac 1);
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   481
qed "image_Int_subset_left";
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   482
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   483
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   484
(** Inverse Image **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   485
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   486
Goal "r-``0 = 0";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   487
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   488
qed "vimage_0";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   489
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   490
Goal "r-``(A Un B) = (r-``A) Un (r-``B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   491
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   492
qed "vimage_Un";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   493
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   494
Goal "r-``(A Int B) <= (r-``A) Int (r-``B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   495
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   496
qed "vimage_Int_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   497
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   498
Goalw [function_def] "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)";
4660
63f0b2601792 New vimage laws
paulson
parents: 4242
diff changeset
   499
by (Blast_tac 1);
63f0b2601792 New vimage laws
paulson
parents: 4242
diff changeset
   500
qed "function_vimage_Int";
63f0b2601792 New vimage laws
paulson
parents: 4242
diff changeset
   501
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   502
Goalw [function_def] "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
4660
63f0b2601792 New vimage laws
paulson
parents: 4242
diff changeset
   503
by (Blast_tac 1);
63f0b2601792 New vimage laws
paulson
parents: 4242
diff changeset
   504
qed "function_vimage_Diff";
63f0b2601792 New vimage laws
paulson
parents: 4242
diff changeset
   505
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   506
Goalw [function_def] "function(f) ==> f `` (f-`` A) <= A";
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   507
by (Blast_tac 1);
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   508
qed "function_image_vimage";
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   509
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   510
Goal "(r Int A*A)-``B <= (r-``B) Int A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   511
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   512
qed "vimage_Int_square_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   513
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   514
Goal "B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   515
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   516
qed "vimage_Int_square";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   517
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   518
Addsimps [vimage_0, vimage_Un];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   519
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   520
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   521
(*Invese image laws for special relations*)
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   522
Goal "0-``A = 0";
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   523
by (Blast_tac 1);
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   524
qed "vimage_0_left";
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   525
Addsimps [vimage_0_left];
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   526
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   527
Goal "(r Un s)-``A = (r-``A) Un (s-``A)";
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   528
by (Blast_tac 1);
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   529
qed "vimage_Un_left";
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   530
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   531
Goal "(r Int s)-``A <= (r-``A) Int (s-``A)";
4840
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   532
by (Blast_tac 1);
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   533
qed "vimage_Int_subset_left";
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   534
b8f2ec739530 new thms image_0_left, image_Un_left, etc.
paulson
parents: 4660
diff changeset
   535
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
(** Converse **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   538
Goal "converse(A Un B) = converse(A) Un converse(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   539
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   540
qed "converse_Un";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   541
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   542
Goal "converse(A Int B) = converse(A) Int converse(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   543
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   544
qed "converse_Int";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   545
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   546
Goal "converse(A - B) = converse(A) - converse(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   547
by (Blast_tac 1);
1056
097b3255bf3a Renamed domain_diff_subset, range_diff_subset,
lcp
parents: 1035
diff changeset
   548
qed "converse_Diff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   550
Goal "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   551
by (Blast_tac 1);
787
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   552
qed "converse_UN";
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   553
1652
9b78ce58d6b1 Proved Inter_0 and converse_INT
paulson
parents: 1611
diff changeset
   554
(*Unfolding Inter avoids using excluded middle on A=0*)
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5321
diff changeset
   555
Goalw [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   556
by (Blast_tac 1);
1652
9b78ce58d6b1 Proved Inter_0 and converse_INT
paulson
parents: 1611
diff changeset
   557
qed "converse_INT";
9b78ce58d6b1 Proved Inter_0 and converse_INT
paulson
parents: 1611
diff changeset
   558
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   559
Addsimps [converse_Un, converse_Int, converse_Diff, converse_UN, converse_INT];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   560
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   561
(** Pow **)
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   562
6288
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   563
Goal "Pow(0) = {0}";
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   564
by (Blast_tac 1);
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   565
qed "Pow_0";
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   566
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   567
Goal "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}";
6298
a336f80158c8 expandshort
paulson
parents: 6288
diff changeset
   568
by (rtac equalityI 1);
6288
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   569
by Safe_tac;
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   570
by (etac swap 1);
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   571
by (res_inst_tac [("a", "x-{a}")] RepFun_eqI 1);
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   572
by (ALLGOALS Blast_tac);
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   573
qed "Pow_insert";
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   574
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   575
Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   576
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   577
qed "Un_Pow_subset";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   578
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   579
Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   580
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   581
qed "UN_Pow_subset";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   582
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   583
Goal "A <= Pow(Union(A))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   584
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   585
qed "subset_Pow_Union";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   586
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   587
Goal "Union(Pow(A)) = A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   588
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   589
qed "Union_Pow_eq";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   590
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   591
Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   592
by (Blast_tac 1);
6288
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   593
qed "Pow_Int_eq";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   594
6288
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   595
Goal "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   596
by (Blast_tac 1);
6288
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   597
qed "Pow_INT_eq";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   598
6288
694c9c1910e8 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents: 6068
diff changeset
   599
Addsimps [Pow_0, Union_Pow_eq, Pow_Int_eq];
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1784
diff changeset
   600
839
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   601
(** RepFun **)
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   602
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   603
Goal "{f(x).x:A}=0 <-> A=0";
9303
f1ad1ed0d110 fixed a failing proof
paulson
parents: 9180
diff changeset
   604
by (Blast_tac 1);
839
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   605
qed "RepFun_eq_0_iff";
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   606
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   607
(** Collect **)
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   608
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   609
Goal "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   610
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   611
qed "Collect_Un";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   612
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   613
Goal "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   614
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   615
qed "Collect_Int";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   616
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   617
Goal "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   618
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   619
qed "Collect_Diff";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   620
6068
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5325
diff changeset
   621
Goal "{x:cons(a,B). P(x)} = \
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5325
diff changeset
   622
\     (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})";
5116
8eb343ab5748 Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents: 5067
diff changeset
   623
by (simp_tac (simpset() addsplits [split_if]) 1);
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   624
by (Blast_tac 1);
1611
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   625
qed "Collect_cons";
35e0fd1b1775 New results from AC/Cardinal_aux.ML
paulson
parents: 1568
diff changeset
   626