author | paulson |
Tue, 21 May 2002 13:06:36 +0200 | |
changeset 13168 | afcbca3498b0 |
parent 13165 | 31d020705aff |
child 13169 | 394a6c649547 |
permissions | -rw-r--r-- |
13165 | 1 |
(* Title: ZF/equalities |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
6 |
Converse, domain, range of a relation or function. |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
7 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
8 |
And set theory equalities involving Union, Intersection, Inclusion, etc. |
13165 | 9 |
(Thanks also to Philippe de Groote.) |
10 |
*) |
|
11 |
||
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
12 |
theory equalities = pair + subset: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
13 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
14 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
15 |
(*** converse ***) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
16 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
17 |
lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>:r" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
18 |
apply (unfold converse_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
19 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
20 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
21 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
22 |
lemma converseI: "<a,b>:r ==> <b,a>:converse(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
23 |
apply (unfold converse_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
24 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
25 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
26 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
27 |
lemma converseD: "<a,b> : converse(r) ==> <b,a> : r" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
28 |
apply (unfold converse_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
29 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
30 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
31 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
32 |
lemma converseE [elim!]: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
33 |
"[| yx : converse(r); |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
34 |
!!x y. [| yx=<y,x>; <x,y>:r |] ==> P |] |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
35 |
==> P" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
36 |
apply (unfold converse_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
37 |
apply (blast intro: elim:); |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
38 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
39 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
40 |
lemma converse_converse: "r<=Sigma(A,B) ==> converse(converse(r)) = r" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
41 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
42 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
43 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
44 |
lemma converse_type: "r<=A*B ==> converse(r)<=B*A" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
45 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
46 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
47 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
48 |
lemma converse_prod [simp]: "converse(A*B) = B*A" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
49 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
50 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
51 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
52 |
lemma converse_empty [simp]: "converse(0) = 0" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
53 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
54 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
55 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
56 |
lemma converse_subset_iff: "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
57 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
58 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
59 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
60 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
61 |
(*** domain ***) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
62 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
63 |
lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
64 |
apply (unfold domain_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
65 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
66 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
67 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
68 |
lemma domainI [intro]: "<a,b>: r ==> a: domain(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
69 |
apply (unfold domain_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
70 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
71 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
72 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
73 |
lemma domainE [elim!]: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
74 |
"[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
75 |
apply (unfold domain_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
76 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
77 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
78 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
79 |
lemma domain_subset: "domain(Sigma(A,B)) <= A" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
80 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
81 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
82 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
83 |
(*** range ***) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
84 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
85 |
lemma rangeI [intro]: "<a,b>: r ==> b : range(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
86 |
apply (unfold range_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
87 |
apply (erule converseI [THEN domainI]) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
88 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
89 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
90 |
lemma rangeE [elim!]: "[| b : range(r); !!x. <x,b>: r ==> P |] ==> P" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
91 |
apply (unfold range_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
92 |
apply (blast intro: elim:); |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
93 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
94 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
95 |
lemma range_subset: "range(A*B) <= B" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
96 |
apply (unfold range_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
97 |
apply (subst converse_prod) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
98 |
apply (rule domain_subset) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
99 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
100 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
101 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
102 |
(*** field ***) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
103 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
104 |
lemma fieldI1: "<a,b>: r ==> a : field(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
105 |
apply (unfold field_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
106 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
107 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
108 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
109 |
lemma fieldI2: "<a,b>: r ==> b : field(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
110 |
apply (unfold field_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
111 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
112 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
113 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
114 |
lemma fieldCI [intro]: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
115 |
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
116 |
apply (unfold field_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
117 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
118 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
119 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
120 |
lemma fieldE [elim!]: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
121 |
"[| a : field(r); |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
122 |
!!x. <a,x>: r ==> P; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
123 |
!!x. <x,a>: r ==> P |] ==> P" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
124 |
apply (unfold field_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
125 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
126 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
127 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
128 |
lemma field_subset: "field(A*B) <= A Un B" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
129 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
130 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
131 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
132 |
lemma domain_subset_field: "domain(r) <= field(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
133 |
apply (unfold field_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
134 |
apply (rule Un_upper1) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
135 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
136 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
137 |
lemma range_subset_field: "range(r) <= field(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
138 |
apply (unfold field_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
139 |
apply (rule Un_upper2) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
140 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
141 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
142 |
lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
143 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
144 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
145 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
146 |
lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
147 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
148 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
149 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
150 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
151 |
(*** Image of a set under a function/relation ***) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
152 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
153 |
lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
154 |
apply (unfold image_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
155 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
156 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
157 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
158 |
lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
159 |
apply (rule image_iff [THEN iff_trans]) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
160 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
161 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
162 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
163 |
lemma imageI [intro]: "[| <a,b>: r; a:A |] ==> b : r``A" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
164 |
apply (unfold image_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
165 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
166 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
167 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
168 |
lemma imageE [elim!]: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
169 |
"[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
170 |
apply (unfold image_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
171 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
172 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
173 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
174 |
lemma image_subset: "r <= A*B ==> r``C <= B" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
175 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
176 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
177 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
178 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
179 |
(*** Inverse image of a set under a function/relation ***) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
180 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
181 |
lemma vimage_iff: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
182 |
"a : r-``B <-> (EX y:B. <a,y>:r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
183 |
apply (unfold vimage_def image_def converse_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
184 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
185 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
186 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
187 |
lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
188 |
apply (rule vimage_iff [THEN iff_trans]) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
189 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
190 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
191 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
192 |
lemma vimageI [intro]: "[| <a,b>: r; b:B |] ==> a : r-``B" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
193 |
apply (unfold vimage_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
194 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
195 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
196 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
197 |
lemma vimageE [elim!]: |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
198 |
"[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
199 |
apply (unfold vimage_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
200 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
201 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
202 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
203 |
lemma vimage_subset: "r <= A*B ==> r-``C <= A" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
204 |
apply (unfold vimage_def) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
205 |
apply (erule converse_type [THEN image_subset]) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
206 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
207 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
208 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
209 |
(** The Union of a set of relations is a relation -- Lemma for fun_Union **) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
210 |
lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==> |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
211 |
Union(S) <= domain(Union(S)) * range(Union(S))" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
212 |
by blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
213 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
214 |
(** The Union of 2 relations is a relation (Lemma for fun_Un) **) |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
215 |
lemma rel_Un: "[| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
216 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
217 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
218 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
219 |
lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
220 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
221 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
222 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
223 |
lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)" |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
224 |
apply blast |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
225 |
done |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
226 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
227 |
|
13165 | 228 |
|
229 |
(** Finite Sets **) |
|
230 |
||
231 |
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) |
|
232 |
lemma cons_eq: "{a} Un B = cons(a,B)" |
|
233 |
by blast |
|
234 |
||
235 |
lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))" |
|
236 |
by blast |
|
237 |
||
238 |
lemma cons_absorb: "a: B ==> cons(a,B) = B" |
|
239 |
by blast |
|
240 |
||
241 |
lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B" |
|
242 |
by blast |
|
243 |
||
244 |
lemma equal_singleton [rule_format]: "[| a: C; ALL y:C. y=b |] ==> C = {b}" |
|
245 |
by blast |
|
246 |
||
247 |
||
248 |
(** Binary Intersection **) |
|
249 |
||
250 |
(*NOT an equality, but it seems to belong here...*) |
|
251 |
lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)" |
|
252 |
by blast |
|
253 |
||
254 |
lemma Int_absorb [simp]: "A Int A = A" |
|
255 |
by blast |
|
256 |
||
257 |
lemma Int_left_absorb: "A Int (A Int B) = A Int B" |
|
258 |
by blast |
|
259 |
||
260 |
lemma Int_commute: "A Int B = B Int A" |
|
261 |
by blast |
|
262 |
||
263 |
lemma Int_left_commute: "A Int (B Int C) = B Int (A Int C)" |
|
264 |
by blast |
|
265 |
||
266 |
lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)" |
|
267 |
by blast |
|
268 |
||
269 |
(*Intersection is an AC-operator*) |
|
270 |
lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute |
|
271 |
||
272 |
lemma Int_Un_distrib: "A Int (B Un C) = (A Int B) Un (A Int C)" |
|
273 |
by blast |
|
274 |
||
275 |
lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)" |
|
276 |
by blast |
|
277 |
||
278 |
lemma subset_Int_iff: "A<=B <-> A Int B = A" |
|
279 |
by (blast elim!: equalityE) |
|
280 |
||
281 |
lemma subset_Int_iff2: "A<=B <-> B Int A = A" |
|
282 |
by (blast elim!: equalityE) |
|
283 |
||
284 |
lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B" |
|
285 |
by blast |
|
286 |
||
287 |
(** Binary Union **) |
|
288 |
||
289 |
lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)" |
|
290 |
by blast |
|
291 |
||
292 |
lemma Un_absorb [simp]: "A Un A = A" |
|
293 |
by blast |
|
294 |
||
295 |
lemma Un_left_absorb: "A Un (A Un B) = A Un B" |
|
296 |
by blast |
|
297 |
||
298 |
lemma Un_commute: "A Un B = B Un A" |
|
299 |
by blast |
|
300 |
||
301 |
lemma Un_left_commute: "A Un (B Un C) = B Un (A Un C)" |
|
302 |
by blast |
|
303 |
||
304 |
lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)" |
|
305 |
by blast |
|
306 |
||
307 |
(*Union is an AC-operator*) |
|
308 |
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute |
|
309 |
||
310 |
lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)" |
|
311 |
by blast |
|
312 |
||
313 |
lemma subset_Un_iff: "A<=B <-> A Un B = B" |
|
314 |
by (blast elim!: equalityE) |
|
315 |
||
316 |
lemma subset_Un_iff2: "A<=B <-> B Un A = B" |
|
317 |
by (blast elim!: equalityE) |
|
318 |
||
319 |
lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)" |
|
320 |
by blast |
|
321 |
||
322 |
lemma Un_eq_Union: "A Un B = Union({A, B})" |
|
323 |
by blast |
|
324 |
||
325 |
(** Simple properties of Diff -- set difference **) |
|
326 |
||
327 |
lemma Diff_cancel: "A - A = 0" |
|
328 |
by blast |
|
329 |
||
330 |
lemma Diff_triv: "A Int B = 0 ==> A - B = A" |
|
331 |
by blast |
|
332 |
||
333 |
lemma empty_Diff [simp]: "0 - A = 0" |
|
334 |
by blast |
|
335 |
||
336 |
lemma Diff_0 [simp]: "A - 0 = A" |
|
337 |
by blast |
|
338 |
||
339 |
lemma Diff_eq_0_iff: "A - B = 0 <-> A <= B" |
|
340 |
by (blast elim: equalityE) |
|
341 |
||
342 |
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
|
343 |
lemma Diff_cons: "A - cons(a,B) = A - B - {a}" |
|
344 |
by blast |
|
345 |
||
346 |
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
|
347 |
lemma Diff_cons2: "A - cons(a,B) = A - {a} - B" |
|
348 |
by blast |
|
349 |
||
350 |
lemma Diff_disjoint: "A Int (B-A) = 0" |
|
351 |
by blast |
|
352 |
||
353 |
lemma Diff_partition: "A<=B ==> A Un (B-A) = B" |
|
354 |
by blast |
|
355 |
||
356 |
lemma subset_Un_Diff: "A <= B Un (A - B)" |
|
357 |
by blast |
|
358 |
||
359 |
lemma double_complement: "[| A<=B; B<=C |] ==> B-(C-A) = A" |
|
360 |
by blast |
|
361 |
||
362 |
lemma double_complement_Un: "(A Un B) - (B-A) = A" |
|
363 |
by blast |
|
364 |
||
365 |
lemma Un_Int_crazy: |
|
366 |
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)" |
|
367 |
apply blast |
|
368 |
done |
|
369 |
||
370 |
lemma Diff_Un: "A - (B Un C) = (A-B) Int (A-C)" |
|
371 |
by blast |
|
372 |
||
373 |
lemma Diff_Int: "A - (B Int C) = (A-B) Un (A-C)" |
|
374 |
by blast |
|
375 |
||
376 |
lemma Un_Diff: "(A Un B) - C = (A - C) Un (B - C)" |
|
377 |
by blast |
|
378 |
||
379 |
lemma Int_Diff: "(A Int B) - C = A Int (B - C)" |
|
380 |
by blast |
|
381 |
||
382 |
lemma Diff_Int_distrib: "C Int (A-B) = (C Int A) - (C Int B)" |
|
383 |
by blast |
|
384 |
||
385 |
lemma Diff_Int_distrib2: "(A-B) Int C = (A Int C) - (B Int C)" |
|
386 |
by blast |
|
387 |
||
388 |
(*Halmos, Naive Set Theory, page 16.*) |
|
389 |
lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C) <-> C<=A" |
|
390 |
by (blast elim!: equalityE) |
|
391 |
||
392 |
||
393 |
(** Big Union and Intersection **) |
|
394 |
||
395 |
lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)" |
|
396 |
by blast |
|
397 |
||
398 |
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)" |
|
399 |
by blast |
|
400 |
||
401 |
lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)" |
|
402 |
by blast |
|
403 |
||
404 |
lemma Union_disjoint: "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)" |
|
405 |
by (blast elim!: equalityE) |
|
406 |
||
407 |
lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)" |
|
408 |
by blast |
|
409 |
||
410 |
lemma Inter_0: "Inter(0) = 0" |
|
411 |
by (unfold Inter_def, blast) |
|
412 |
||
413 |
lemma Inter_Un_subset: "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)" |
|
414 |
by blast |
|
415 |
||
416 |
(* A good challenge: Inter is ill-behaved on the empty set *) |
|
417 |
lemma Inter_Un_distrib: |
|
418 |
"[| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)" |
|
419 |
by blast |
|
420 |
||
421 |
lemma Union_singleton: "Union({b}) = b" |
|
422 |
by blast |
|
423 |
||
424 |
lemma Inter_singleton: "Inter({b}) = b" |
|
425 |
by blast |
|
426 |
||
427 |
lemma Inter_cons [simp]: |
|
428 |
"Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))" |
|
429 |
by force |
|
430 |
||
431 |
(** Unions and Intersections of Families **) |
|
432 |
||
433 |
lemma Union_eq_UN: "Union(A) = (UN x:A. x)" |
|
434 |
by blast |
|
435 |
||
436 |
lemma Inter_eq_INT: "Inter(A) = (INT x:A. x)" |
|
437 |
by (unfold Inter_def, blast) |
|
438 |
||
439 |
lemma UN_0 [simp]: "(UN i:0. A(i)) = 0" |
|
440 |
by blast |
|
441 |
||
442 |
lemma UN_singleton: "(UN x:A. {x}) = A" |
|
443 |
by blast |
|
444 |
||
445 |
lemma UN_Un: "(UN i: A Un B. C(i)) = (UN i: A. C(i)) Un (UN i:B. C(i))" |
|
446 |
by blast |
|
447 |
||
448 |
lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j) |
|
449 |
else if J=0 then INT i:I. A(i) |
|
450 |
else ((INT i:I. A(i)) Int (INT j:J. A(j))))" |
|
451 |
apply auto |
|
452 |
apply (blast intro!: equalityI) |
|
453 |
done |
|
454 |
||
455 |
lemma UN_UN_flatten: "(UN x : (UN y:A. B(y)). C(x)) = (UN y:A. UN x: B(y). C(x))" |
|
456 |
by blast |
|
457 |
||
458 |
(*Halmos, Naive Set Theory, page 35.*) |
|
459 |
lemma Int_UN_distrib: "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))" |
|
460 |
by blast |
|
461 |
||
462 |
lemma Un_INT_distrib: "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))" |
|
463 |
by blast |
|
464 |
||
465 |
lemma Int_UN_distrib2: |
|
466 |
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))" |
|
467 |
by blast |
|
468 |
||
469 |
lemma Un_INT_distrib2: "[| i:I; j:J |] ==> |
|
470 |
(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))" |
|
471 |
by blast |
|
472 |
||
473 |
lemma UN_constant: "a: A ==> (UN y:A. c) = c" |
|
474 |
by blast |
|
475 |
||
476 |
lemma INT_constant: "a: A ==> (INT y:A. c) = c" |
|
477 |
by blast |
|
478 |
||
479 |
lemma UN_RepFun [simp]: "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))" |
|
480 |
by blast |
|
481 |
||
482 |
lemma INT_RepFun [simp]: "(INT x:RepFun(A,f). B(x)) = (INT a:A. B(f(a)))" |
|
483 |
by (auto simp add: Inter_def) |
|
484 |
||
485 |
lemma INT_Union_eq: |
|
486 |
"0 ~: A ==> (INT x: Union(A). B(x)) = (INT y:A. INT x:y. B(x))" |
|
487 |
apply (simp add: Inter_def) |
|
488 |
apply (subgoal_tac "ALL x:A. x~=0") |
|
489 |
prefer 2 apply blast |
|
490 |
apply force |
|
491 |
done |
|
492 |
||
493 |
lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0) |
|
494 |
==> (INT z: (UN x:A. B(x)). C(z)) = (INT x:A. INT z: B(x). C(z))" |
|
495 |
apply (subst INT_Union_eq, blast) |
|
496 |
apply (simp add: Inter_def) |
|
497 |
done |
|
498 |
||
499 |
||
500 |
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: |
|
501 |
Union of a family of unions **) |
|
502 |
||
503 |
lemma UN_Un_distrib: |
|
504 |
"(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))" |
|
505 |
by blast |
|
506 |
||
507 |
lemma INT_Int_distrib: |
|
508 |
"i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))" |
|
509 |
by blast |
|
510 |
||
511 |
lemma UN_Int_subset: |
|
512 |
"(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))" |
|
513 |
by blast |
|
514 |
||
515 |
(** Devlin, page 12, exercise 5: Complements **) |
|
516 |
||
517 |
lemma Diff_UN: "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))" |
|
518 |
by blast |
|
519 |
||
520 |
lemma Diff_INT: "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))" |
|
521 |
by blast |
|
522 |
||
523 |
(** Unions and Intersections with General Sum **) |
|
524 |
||
525 |
(*Not suitable for rewriting: LOOPS!*) |
|
526 |
lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)" |
|
527 |
by blast |
|
528 |
||
529 |
(*Not suitable for rewriting: LOOPS!*) |
|
530 |
lemma Sigma_cons2: "A * cons(b,B) = A*{b} Un A*B" |
|
531 |
by blast |
|
532 |
||
533 |
lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)" |
|
534 |
by blast |
|
535 |
||
536 |
lemma Sigma_succ2: "A * succ(B) = A*{B} Un A*B" |
|
537 |
by blast |
|
538 |
||
539 |
lemma SUM_UN_distrib1: |
|
540 |
"(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))" |
|
541 |
by blast |
|
542 |
||
543 |
lemma SUM_UN_distrib2: |
|
544 |
"(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))" |
|
545 |
by blast |
|
546 |
||
547 |
lemma SUM_Un_distrib1: |
|
548 |
"(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))" |
|
549 |
by blast |
|
550 |
||
551 |
lemma SUM_Un_distrib2: |
|
552 |
"(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))" |
|
553 |
by blast |
|
554 |
||
555 |
(*First-order version of the above, for rewriting*) |
|
556 |
lemma prod_Un_distrib2: "I * (A Un B) = I*A Un I*B" |
|
557 |
by (rule SUM_Un_distrib2) |
|
558 |
||
559 |
lemma SUM_Int_distrib1: |
|
560 |
"(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))" |
|
561 |
by blast |
|
562 |
||
563 |
lemma SUM_Int_distrib2: |
|
564 |
"(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))" |
|
565 |
by blast |
|
566 |
||
567 |
(*First-order version of the above, for rewriting*) |
|
568 |
lemma prod_Int_distrib2: "I * (A Int B) = I*A Int I*B" |
|
569 |
by (rule SUM_Int_distrib2) |
|
570 |
||
571 |
(*Cf Aczel, Non-Well-Founded Sets, page 115*) |
|
572 |
lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))" |
|
573 |
by blast |
|
574 |
||
575 |
(** Domain **) |
|
576 |
||
577 |
lemma domain_of_prod: "b:B ==> domain(A*B) = A" |
|
578 |
by blast |
|
579 |
||
580 |
lemma domain_0 [simp]: "domain(0) = 0" |
|
581 |
by blast |
|
582 |
||
583 |
lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))" |
|
584 |
by blast |
|
585 |
||
586 |
lemma domain_Un_eq [simp]: "domain(A Un B) = domain(A) Un domain(B)" |
|
587 |
by blast |
|
588 |
||
589 |
lemma domain_Int_subset: "domain(A Int B) <= domain(A) Int domain(B)" |
|
590 |
by blast |
|
591 |
||
592 |
lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)" |
|
593 |
by blast |
|
594 |
||
595 |
lemma domain_converse [simp]: "domain(converse(r)) = range(r)" |
|
596 |
by blast |
|
124 | 597 |
|
13165 | 598 |
lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))" |
599 |
by blast |
|
600 |
||
601 |
lemma domain_Union: "domain(Union(A)) = (UN x:A. domain(x))" |
|
602 |
by blast |
|
603 |
||
604 |
||
605 |
(** Range **) |
|
606 |
||
607 |
lemma range_of_prod: "a:A ==> range(A*B) = B" |
|
608 |
by blast |
|
609 |
||
610 |
lemma range_0 [simp]: "range(0) = 0" |
|
611 |
by blast |
|
612 |
||
613 |
lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))" |
|
614 |
by blast |
|
615 |
||
616 |
lemma range_Un_eq [simp]: "range(A Un B) = range(A) Un range(B)" |
|
617 |
by blast |
|
618 |
||
619 |
lemma range_Int_subset: "range(A Int B) <= range(A) Int range(B)" |
|
620 |
by blast |
|
621 |
||
622 |
lemma range_Diff_subset: "range(A) - range(B) <= range(A - B)" |
|
623 |
by blast |
|
624 |
||
625 |
lemma range_converse [simp]: "range(converse(r)) = domain(r)" |
|
626 |
by blast |
|
627 |
||
628 |
||
629 |
(** Field **) |
|
630 |
||
631 |
lemma field_of_prod: "field(A*A) = A" |
|
632 |
by blast |
|
633 |
||
634 |
lemma field_0 [simp]: "field(0) = 0" |
|
635 |
by blast |
|
636 |
||
637 |
lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))" |
|
638 |
by blast |
|
639 |
||
640 |
lemma field_Un_eq [simp]: "field(A Un B) = field(A) Un field(B)" |
|
641 |
by blast |
|
642 |
||
643 |
lemma field_Int_subset: "field(A Int B) <= field(A) Int field(B)" |
|
644 |
by blast |
|
645 |
||
646 |
lemma field_Diff_subset: "field(A) - field(B) <= field(A - B)" |
|
647 |
by blast |
|
648 |
||
649 |
lemma field_converse [simp]: "field(converse(r)) = field(r)" |
|
650 |
by blast |
|
651 |
||
652 |
||
653 |
(** Image **) |
|
654 |
||
655 |
lemma image_0 [simp]: "r``0 = 0" |
|
656 |
by blast |
|
657 |
||
658 |
lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)" |
|
659 |
by blast |
|
660 |
||
661 |
lemma image_Int_subset: "r``(A Int B) <= (r``A) Int (r``B)" |
|
662 |
by blast |
|
663 |
||
664 |
lemma image_Int_square_subset: "(r Int A*A)``B <= (r``B) Int A" |
|
665 |
by blast |
|
666 |
||
667 |
lemma image_Int_square: "B<=A ==> (r Int A*A)``B = (r``B) Int A" |
|
668 |
by blast |
|
669 |
||
670 |
||
671 |
(*Image laws for special relations*) |
|
672 |
lemma image_0_left [simp]: "0``A = 0" |
|
673 |
by blast |
|
674 |
||
675 |
lemma image_Un_left: "(r Un s)``A = (r``A) Un (s``A)" |
|
676 |
by blast |
|
677 |
||
678 |
lemma image_Int_subset_left: "(r Int s)``A <= (r``A) Int (s``A)" |
|
679 |
by blast |
|
680 |
||
681 |
||
682 |
(** Inverse Image **) |
|
683 |
||
684 |
lemma vimage_0 [simp]: "r-``0 = 0" |
|
685 |
by blast |
|
686 |
||
687 |
lemma vimage_Un [simp]: "r-``(A Un B) = (r-``A) Un (r-``B)" |
|
688 |
by blast |
|
689 |
||
690 |
lemma vimage_Int_subset: "r-``(A Int B) <= (r-``A) Int (r-``B)" |
|
691 |
by blast |
|
692 |
||
693 |
(*NOT suitable for rewriting*) |
|
694 |
lemma vimage_eq_UN: "f -``B = (UN y:B. f-``{y})" |
|
695 |
by blast |
|
696 |
||
697 |
lemma function_vimage_Int: |
|
698 |
"function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)" |
|
699 |
by (unfold function_def, blast) |
|
700 |
||
701 |
lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)" |
|
702 |
by (unfold function_def, blast) |
|
703 |
||
704 |
lemma function_image_vimage: "function(f) ==> f `` (f-`` A) <= A" |
|
705 |
by (unfold function_def, blast) |
|
706 |
||
707 |
lemma vimage_Int_square_subset: "(r Int A*A)-``B <= (r-``B) Int A" |
|
708 |
by blast |
|
709 |
||
710 |
lemma vimage_Int_square: "B<=A ==> (r Int A*A)-``B = (r-``B) Int A" |
|
711 |
by blast |
|
712 |
||
713 |
||
714 |
||
715 |
(*Invese image laws for special relations*) |
|
716 |
lemma vimage_0_left [simp]: "0-``A = 0" |
|
717 |
by blast |
|
718 |
||
719 |
lemma vimage_Un_left: "(r Un s)-``A = (r-``A) Un (s-``A)" |
|
720 |
by blast |
|
721 |
||
722 |
lemma vimage_Int_subset_left: "(r Int s)-``A <= (r-``A) Int (s-``A)" |
|
723 |
by blast |
|
724 |
||
725 |
||
726 |
(** Converse **) |
|
727 |
||
728 |
lemma converse_Un [simp]: "converse(A Un B) = converse(A) Un converse(B)" |
|
729 |
by blast |
|
730 |
||
731 |
lemma converse_Int [simp]: "converse(A Int B) = converse(A) Int converse(B)" |
|
732 |
by blast |
|
733 |
||
734 |
lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)" |
|
735 |
by blast |
|
736 |
||
737 |
lemma converse_UN [simp]: "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))" |
|
738 |
by blast |
|
739 |
||
740 |
(*Unfolding Inter avoids using excluded middle on A=0*) |
|
741 |
lemma converse_INT [simp]: |
|
742 |
"converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))" |
|
743 |
apply (unfold Inter_def, blast) |
|
744 |
done |
|
745 |
||
746 |
(** Pow **) |
|
747 |
||
748 |
lemma Pow_0 [simp]: "Pow(0) = {0}" |
|
749 |
by blast |
|
750 |
||
751 |
lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}" |
|
752 |
apply (rule equalityI, safe) |
|
753 |
apply (erule swap) |
|
754 |
apply (rule_tac a = "x-{a}" in RepFun_eqI, auto) |
|
755 |
done |
|
756 |
||
757 |
lemma Un_Pow_subset: "Pow(A) Un Pow(B) <= Pow(A Un B)" |
|
758 |
by blast |
|
759 |
||
760 |
lemma UN_Pow_subset: "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))" |
|
761 |
by blast |
|
762 |
||
763 |
lemma subset_Pow_Union: "A <= Pow(Union(A))" |
|
764 |
by blast |
|
765 |
||
766 |
lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A" |
|
767 |
by blast |
|
768 |
||
769 |
lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)" |
|
770 |
by blast |
|
771 |
||
772 |
lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))" |
|
773 |
by blast |
|
774 |
||
775 |
(** RepFun **) |
|
776 |
||
777 |
lemma RepFun_eq_0_iff [simp]: "{f(x).x:A}=0 <-> A=0" |
|
778 |
by blast |
|
779 |
||
780 |
lemma RepFun_constant [simp]: "{c. x:A} = (if A=0 then 0 else {c})" |
|
781 |
apply auto |
|
782 |
apply blast |
|
783 |
done |
|
784 |
||
785 |
(** Collect **) |
|
2469 | 786 |
|
13165 | 787 |
lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)" |
788 |
by blast |
|
789 |
||
790 |
lemma Collect_Int: "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)" |
|
791 |
by blast |
|
792 |
||
793 |
lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)" |
|
794 |
by blast |
|
795 |
||
796 |
lemma Collect_cons: "{x:cons(a,B). P(x)} = |
|
797 |
(if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})" |
|
798 |
by (simp, blast) |
|
799 |
||
800 |
lemma Int_Collect_self_eq: "A Int Collect(A,P) = Collect(A,P)" |
|
801 |
by blast |
|
802 |
||
803 |
lemma Collect_Collect_eq [simp]: |
|
804 |
"Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))" |
|
805 |
by blast |
|
806 |
||
807 |
lemma Collect_Int_Collect_eq: |
|
808 |
"Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))" |
|
809 |
by blast |
|
810 |
||
811 |
ML |
|
812 |
{* |
|
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
813 |
val ZF_cs = claset() delrules [equalityI]; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
814 |
|
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
815 |
val converse_iff = thm "converse_iff"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
816 |
val converseI = thm "converseI"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
817 |
val converseD = thm "converseD"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
818 |
val converseE = thm "converseE"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
819 |
val converse_converse = thm "converse_converse"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
820 |
val converse_type = thm "converse_type"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
821 |
val converse_prod = thm "converse_prod"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
822 |
val converse_empty = thm "converse_empty"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
823 |
val converse_subset_iff = thm "converse_subset_iff"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
824 |
val domain_iff = thm "domain_iff"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
825 |
val domainI = thm "domainI"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
826 |
val domainE = thm "domainE"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
827 |
val domain_subset = thm "domain_subset"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
828 |
val rangeI = thm "rangeI"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
829 |
val rangeE = thm "rangeE"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
830 |
val range_subset = thm "range_subset"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
831 |
val fieldI1 = thm "fieldI1"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
832 |
val fieldI2 = thm "fieldI2"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
833 |
val fieldCI = thm "fieldCI"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
834 |
val fieldE = thm "fieldE"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
835 |
val field_subset = thm "field_subset"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
836 |
val domain_subset_field = thm "domain_subset_field"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
837 |
val range_subset_field = thm "range_subset_field"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
838 |
val domain_times_range = thm "domain_times_range"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
839 |
val field_times_field = thm "field_times_field"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
840 |
val image_iff = thm "image_iff"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
841 |
val image_singleton_iff = thm "image_singleton_iff"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
842 |
val imageI = thm "imageI"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
843 |
val imageE = thm "imageE"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
844 |
val image_subset = thm "image_subset"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
845 |
val vimage_iff = thm "vimage_iff"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
846 |
val vimage_singleton_iff = thm "vimage_singleton_iff"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
847 |
val vimageI = thm "vimageI"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
848 |
val vimageE = thm "vimageE"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
849 |
val vimage_subset = thm "vimage_subset"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
850 |
val rel_Union = thm "rel_Union"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
851 |
val rel_Un = thm "rel_Un"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
852 |
val domain_Diff_eq = thm "domain_Diff_eq"; |
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset
|
853 |
val range_Diff_eq = thm "range_Diff_eq"; |
13165 | 854 |
val cons_eq = thm "cons_eq"; |
855 |
val cons_commute = thm "cons_commute"; |
|
856 |
val cons_absorb = thm "cons_absorb"; |
|
857 |
val cons_Diff = thm "cons_Diff"; |
|
858 |
val equal_singleton = thm "equal_singleton"; |
|
859 |
val Int_cons = thm "Int_cons"; |
|
860 |
val Int_absorb = thm "Int_absorb"; |
|
861 |
val Int_left_absorb = thm "Int_left_absorb"; |
|
862 |
val Int_commute = thm "Int_commute"; |
|
863 |
val Int_left_commute = thm "Int_left_commute"; |
|
864 |
val Int_assoc = thm "Int_assoc"; |
|
865 |
val Int_Un_distrib = thm "Int_Un_distrib"; |
|
866 |
val Int_Un_distrib2 = thm "Int_Un_distrib2"; |
|
867 |
val subset_Int_iff = thm "subset_Int_iff"; |
|
868 |
val subset_Int_iff2 = thm "subset_Int_iff2"; |
|
869 |
val Int_Diff_eq = thm "Int_Diff_eq"; |
|
870 |
val Un_cons = thm "Un_cons"; |
|
871 |
val Un_absorb = thm "Un_absorb"; |
|
872 |
val Un_left_absorb = thm "Un_left_absorb"; |
|
873 |
val Un_commute = thm "Un_commute"; |
|
874 |
val Un_left_commute = thm "Un_left_commute"; |
|
875 |
val Un_assoc = thm "Un_assoc"; |
|
876 |
val Un_Int_distrib = thm "Un_Int_distrib"; |
|
877 |
val subset_Un_iff = thm "subset_Un_iff"; |
|
878 |
val subset_Un_iff2 = thm "subset_Un_iff2"; |
|
879 |
val Un_empty = thm "Un_empty"; |
|
880 |
val Un_eq_Union = thm "Un_eq_Union"; |
|
881 |
val Diff_cancel = thm "Diff_cancel"; |
|
882 |
val Diff_triv = thm "Diff_triv"; |
|
883 |
val empty_Diff = thm "empty_Diff"; |
|
884 |
val Diff_0 = thm "Diff_0"; |
|
885 |
val Diff_eq_0_iff = thm "Diff_eq_0_iff"; |
|
886 |
val Diff_cons = thm "Diff_cons"; |
|
887 |
val Diff_cons2 = thm "Diff_cons2"; |
|
888 |
val Diff_disjoint = thm "Diff_disjoint"; |
|
889 |
val Diff_partition = thm "Diff_partition"; |
|
890 |
val subset_Un_Diff = thm "subset_Un_Diff"; |
|
891 |
val double_complement = thm "double_complement"; |
|
892 |
val double_complement_Un = thm "double_complement_Un"; |
|
893 |
val Un_Int_crazy = thm "Un_Int_crazy"; |
|
894 |
val Diff_Un = thm "Diff_Un"; |
|
895 |
val Diff_Int = thm "Diff_Int"; |
|
896 |
val Un_Diff = thm "Un_Diff"; |
|
897 |
val Int_Diff = thm "Int_Diff"; |
|
898 |
val Diff_Int_distrib = thm "Diff_Int_distrib"; |
|
899 |
val Diff_Int_distrib2 = thm "Diff_Int_distrib2"; |
|
900 |
val Un_Int_assoc_iff = thm "Un_Int_assoc_iff"; |
|
901 |
val Union_cons = thm "Union_cons"; |
|
902 |
val Union_Un_distrib = thm "Union_Un_distrib"; |
|
903 |
val Union_Int_subset = thm "Union_Int_subset"; |
|
904 |
val Union_disjoint = thm "Union_disjoint"; |
|
905 |
val Union_empty_iff = thm "Union_empty_iff"; |
|
906 |
val Inter_0 = thm "Inter_0"; |
|
907 |
val Inter_Un_subset = thm "Inter_Un_subset"; |
|
908 |
val Inter_Un_distrib = thm "Inter_Un_distrib"; |
|
909 |
val Union_singleton = thm "Union_singleton"; |
|
910 |
val Inter_singleton = thm "Inter_singleton"; |
|
911 |
val Inter_cons = thm "Inter_cons"; |
|
912 |
val Union_eq_UN = thm "Union_eq_UN"; |
|
913 |
val Inter_eq_INT = thm "Inter_eq_INT"; |
|
914 |
val UN_0 = thm "UN_0"; |
|
915 |
val UN_singleton = thm "UN_singleton"; |
|
916 |
val UN_Un = thm "UN_Un"; |
|
917 |
val INT_Un = thm "INT_Un"; |
|
918 |
val UN_UN_flatten = thm "UN_UN_flatten"; |
|
919 |
val Int_UN_distrib = thm "Int_UN_distrib"; |
|
920 |
val Un_INT_distrib = thm "Un_INT_distrib"; |
|
921 |
val Int_UN_distrib2 = thm "Int_UN_distrib2"; |
|
922 |
val Un_INT_distrib2 = thm "Un_INT_distrib2"; |
|
923 |
val UN_constant = thm "UN_constant"; |
|
924 |
val INT_constant = thm "INT_constant"; |
|
925 |
val UN_RepFun = thm "UN_RepFun"; |
|
926 |
val INT_RepFun = thm "INT_RepFun"; |
|
927 |
val INT_Union_eq = thm "INT_Union_eq"; |
|
928 |
val INT_UN_eq = thm "INT_UN_eq"; |
|
929 |
val UN_Un_distrib = thm "UN_Un_distrib"; |
|
930 |
val INT_Int_distrib = thm "INT_Int_distrib"; |
|
931 |
val UN_Int_subset = thm "UN_Int_subset"; |
|
932 |
val Diff_UN = thm "Diff_UN"; |
|
933 |
val Diff_INT = thm "Diff_INT"; |
|
934 |
val Sigma_cons1 = thm "Sigma_cons1"; |
|
935 |
val Sigma_cons2 = thm "Sigma_cons2"; |
|
936 |
val Sigma_succ1 = thm "Sigma_succ1"; |
|
937 |
val Sigma_succ2 = thm "Sigma_succ2"; |
|
938 |
val SUM_UN_distrib1 = thm "SUM_UN_distrib1"; |
|
939 |
val SUM_UN_distrib2 = thm "SUM_UN_distrib2"; |
|
940 |
val SUM_Un_distrib1 = thm "SUM_Un_distrib1"; |
|
941 |
val SUM_Un_distrib2 = thm "SUM_Un_distrib2"; |
|
942 |
val prod_Un_distrib2 = thm "prod_Un_distrib2"; |
|
943 |
val SUM_Int_distrib1 = thm "SUM_Int_distrib1"; |
|
944 |
val SUM_Int_distrib2 = thm "SUM_Int_distrib2"; |
|
945 |
val prod_Int_distrib2 = thm "prod_Int_distrib2"; |
|
946 |
val SUM_eq_UN = thm "SUM_eq_UN"; |
|
947 |
val domain_of_prod = thm "domain_of_prod"; |
|
948 |
val domain_0 = thm "domain_0"; |
|
949 |
val domain_cons = thm "domain_cons"; |
|
950 |
val domain_Un_eq = thm "domain_Un_eq"; |
|
951 |
val domain_Int_subset = thm "domain_Int_subset"; |
|
952 |
val domain_Diff_subset = thm "domain_Diff_subset"; |
|
953 |
val domain_converse = thm "domain_converse"; |
|
954 |
val domain_UN = thm "domain_UN"; |
|
955 |
val domain_Union = thm "domain_Union"; |
|
956 |
val range_of_prod = thm "range_of_prod"; |
|
957 |
val range_0 = thm "range_0"; |
|
958 |
val range_cons = thm "range_cons"; |
|
959 |
val range_Un_eq = thm "range_Un_eq"; |
|
960 |
val range_Int_subset = thm "range_Int_subset"; |
|
961 |
val range_Diff_subset = thm "range_Diff_subset"; |
|
962 |
val range_converse = thm "range_converse"; |
|
963 |
val field_of_prod = thm "field_of_prod"; |
|
964 |
val field_0 = thm "field_0"; |
|
965 |
val field_cons = thm "field_cons"; |
|
966 |
val field_Un_eq = thm "field_Un_eq"; |
|
967 |
val field_Int_subset = thm "field_Int_subset"; |
|
968 |
val field_Diff_subset = thm "field_Diff_subset"; |
|
969 |
val field_converse = thm "field_converse"; |
|
970 |
val image_0 = thm "image_0"; |
|
971 |
val image_Un = thm "image_Un"; |
|
972 |
val image_Int_subset = thm "image_Int_subset"; |
|
973 |
val image_Int_square_subset = thm "image_Int_square_subset"; |
|
974 |
val image_Int_square = thm "image_Int_square"; |
|
975 |
val image_0_left = thm "image_0_left"; |
|
976 |
val image_Un_left = thm "image_Un_left"; |
|
977 |
val image_Int_subset_left = thm "image_Int_subset_left"; |
|
978 |
val vimage_0 = thm "vimage_0"; |
|
979 |
val vimage_Un = thm "vimage_Un"; |
|
980 |
val vimage_Int_subset = thm "vimage_Int_subset"; |
|
981 |
val vimage_eq_UN = thm "vimage_eq_UN"; |
|
982 |
val function_vimage_Int = thm "function_vimage_Int"; |
|
983 |
val function_vimage_Diff = thm "function_vimage_Diff"; |
|
984 |
val function_image_vimage = thm "function_image_vimage"; |
|
985 |
val vimage_Int_square_subset = thm "vimage_Int_square_subset"; |
|
986 |
val vimage_Int_square = thm "vimage_Int_square"; |
|
987 |
val vimage_0_left = thm "vimage_0_left"; |
|
988 |
val vimage_Un_left = thm "vimage_Un_left"; |
|
989 |
val vimage_Int_subset_left = thm "vimage_Int_subset_left"; |
|
990 |
val converse_Un = thm "converse_Un"; |
|
991 |
val converse_Int = thm "converse_Int"; |
|
992 |
val converse_Diff = thm "converse_Diff"; |
|
993 |
val converse_UN = thm "converse_UN"; |
|
994 |
val converse_INT = thm "converse_INT"; |
|
995 |
val Pow_0 = thm "Pow_0"; |
|
996 |
val Pow_insert = thm "Pow_insert"; |
|
997 |
val Un_Pow_subset = thm "Un_Pow_subset"; |
|
998 |
val UN_Pow_subset = thm "UN_Pow_subset"; |
|
999 |
val subset_Pow_Union = thm "subset_Pow_Union"; |
|
1000 |
val Union_Pow_eq = thm "Union_Pow_eq"; |
|
1001 |
val Pow_Int_eq = thm "Pow_Int_eq"; |
|
1002 |
val Pow_INT_eq = thm "Pow_INT_eq"; |
|
1003 |
val RepFun_eq_0_iff = thm "RepFun_eq_0_iff"; |
|
1004 |
val RepFun_constant = thm "RepFun_constant"; |
|
1005 |
val Collect_Un = thm "Collect_Un"; |
|
1006 |
val Collect_Int = thm "Collect_Int"; |
|
1007 |
val Collect_Diff = thm "Collect_Diff"; |
|
1008 |
val Collect_cons = thm "Collect_cons"; |
|
1009 |
val Int_Collect_self_eq = thm "Int_Collect_self_eq"; |
|
1010 |
val Collect_Collect_eq = thm "Collect_Collect_eq"; |
|
1011 |
val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq"; |
|
1012 |
||
1013 |
val Int_ac = thms "Int_ac"; |
|
1014 |
val Un_ac = thms "Un_ac"; |
|
1015 |
||
1016 |
*} |
|
1017 |
||
1018 |
end |
|
1019 |