35 "i:greaterThan(k,A) <-> i:A & k<i"; |
35 "i:greaterThan(k,A) <-> i:A & k<i"; |
36 by Auto_tac; |
36 by Auto_tac; |
37 qed "greaterThan_iff"; |
37 qed "greaterThan_iff"; |
38 |
38 |
39 |
39 |
40 |
|
41 (** Needed for WF reasoning in WFair.ML **) |
40 (** Needed for WF reasoning in WFair.ML **) |
42 |
41 |
43 Goal "k:A ==>less_than(A)``{k} = greaterThan(k, A)"; |
42 Goal "k:A ==>less_than(A)``{k} = greaterThan(k, A)"; |
44 by (rtac equalityI 1); |
43 by (rtac equalityI 1); |
45 by (auto_tac (claset(), simpset() addsimps |
44 by (auto_tac (claset(), simpset() addsimps |
55 Addsimps [Image_less_than, Image_inverse_less_than]; |
54 Addsimps [Image_less_than, Image_inverse_less_than]; |
56 |
55 |
57 |
56 |
58 (** Ad-hoc set-theory rules **) |
57 (** Ad-hoc set-theory rules **) |
59 |
58 |
60 Goal "(C Int A) Un (C Int B) = C Int (A Un B)"; |
|
61 by (Blast_tac 1); |
|
62 qed "Int_Un_distrib2"; |
|
63 |
|
64 Goal "C Int (A - B) = (C Int A) - (C Int B)"; |
|
65 by (Blast_tac 1); |
|
66 qed "Diff_Int_distrib"; |
|
67 |
|
68 Goal "(A - B) Int C = (A Int C) - (B Int C)"; |
|
69 by (Blast_tac 1); |
|
70 qed "Diff_Int_distrib2"; |
|
71 |
|
72 Goal "A Un (A Un B) = A Un B"; |
|
73 by (Blast_tac 1); |
|
74 qed "double_Un"; |
|
75 |
|
76 Goal "A Un (B Un C) = B Un (A Un C)"; |
|
77 by (Blast_tac 1); |
|
78 qed "Un_assoc2"; |
|
79 |
|
80 |
|
81 val Un_ac = [Un_assoc, double_Un, Un_commute, Un_assoc2, Un_absorb]; |
|
82 |
|
83 Goal "A Un B = Union({A, B})"; |
|
84 by (Blast_tac 1); |
|
85 qed "Un_eq_Union"; |
|
86 |
|
87 Goal "(UN x:A. {x}) = A"; |
|
88 by (Blast_tac 1); |
|
89 qed "UN_singleton"; |
|
90 |
|
91 |
|
92 Goal "Union(B) Int A = (UN b:B. b Int A)"; |
59 Goal "Union(B) Int A = (UN b:B. b Int A)"; |
93 by Auto_tac; |
60 by Auto_tac; |
94 qed "Int_Union_Union"; |
61 qed "Int_Union_Union"; |
95 |
62 |
96 Goal "A Int Union(B) = (UN b:B. A Int b)"; |
63 Goal "A Int Union(B) = (UN b:B. A Int b)"; |
97 by Auto_tac; |
64 by Auto_tac; |
98 qed "Int_Union_Union2"; |
65 qed "Int_Union_Union2"; |
99 |
66 |
100 (** Intersection **) |
|
101 Goal "A Int (A Int B) = A Int B"; |
|
102 by (Blast_tac 1); |
|
103 qed "double_Int"; |
|
104 |
|
105 Goal "A Int (B Int C) = B Int (A Int C)"; |
|
106 by (Blast_tac 1); |
|
107 qed "Int_assoc2"; |
|
108 |
|
109 val Int_ac = [Int_assoc, double_Int, Int_commute, Int_assoc2]; |
|
110 |
|
111 Goal "A Int B = 0 ==> A - B = A"; |
|
112 by (Blast_tac 1); |
|
113 qed "Diff_triv"; |
|
114 |
|
115 Goal "A Int B - C = A Int (B - C)"; |
|
116 by (Blast_tac 1); |
|
117 qed "Int_Diff"; |
|
118 |
|
119 Goal "f -``B = (UN y:B. f-``{y})"; |
|
120 by (Blast_tac 1); |
|
121 qed "vimage_eq_UN"; |
|
122 |
|
123 Goal "A Un B - (A - B) = B"; |
67 Goal "A Un B - (A - B) = B"; |
124 by (Blast_tac 1); |
68 by (Blast_tac 1); |
125 qed "Un_Diff_Diff"; |
69 qed "Un_Diff_Diff"; |
126 AddIffs [Un_Diff_Diff]; |
70 AddIffs [Un_Diff_Diff]; |
127 |
71 |
128 (*** INT simps ***) |
|
129 |
|
130 Goal |
|
131 "i:I ==> (INT i:I. A(i)) Un B = (INT i:I. A(i) Un B)"; |
|
132 by Auto_tac; |
|
133 qed "INT_Un_distrib"; |
|
134 |
|
135 Goal |
|
136 "!!C. c: C ==> (INT x:C. cons(a, B(x))) = cons(a, (INT x:C. B(x)))"; |
|
137 by Auto_tac; |
|
138 qed "INT_cons"; |
|
139 |
|
140 Goal |
|
141 "i:I ==> (INT i:I. A(i)) Int B = (INT i:I. A(i) Int B)"; |
|
142 by Auto_tac; |
|
143 qed "INT_Int_distrib2"; |
|
144 |
|
145 Goal |
|
146 "i:I ==> B Int (INT i:I. A(i)) = (INT i:I. B Int A(i))"; |
|
147 by Auto_tac; |
|
148 qed "Int_INT_distrib"; |
|
149 |
|
150 val INT_simps = [Un_INT_distrib, Un_INT_distrib2, |
|
151 INT_constant, INT_Int_distrib, Diff_INT, |
|
152 INT_Un_distrib,INT_cons, INT_Int_distrib2, Int_INT_distrib, Inter_0]; |
|
153 |
|
154 |
|
155 (*** UN ***) |
|
156 Goal |
|
157 "!!C. c: C ==> cons(a, (UN x:C. B(x))) = (UN x:C. cons(a, B(x)))"; |
|
158 by Auto_tac; |
|
159 qed "UN_cons"; |
|
160 |
|
161 Goal |
|
162 "!!C. c: C ==> B Un (UN x:C. A(x)) = (UN x:C. B Un A(x))"; |
|
163 by Auto_tac; |
|
164 qed "Un_UN_distrib"; |
|
165 |
|
166 Goal |
|
167 "!!C. c: C ==> (UN x:C. B(x)) Un A = (UN x:C. B(x) Un A)"; |
|
168 by Auto_tac; |
|
169 qed "UN_Un_distrib2"; |
|
170 |
|
171 Goal "(UN x:C. B(x)) Int A = (UN x:C. B(x) Int A)"; |
|
172 by Auto_tac; |
|
173 qed "UN_Int_distrib"; |
|
174 |
|
175 val UN_simps = [UN_cons, Un_UN_distrib, UN_Un_distrib2, UN_Un_distrib, UN_Int_distrib, UN_0]; |
|
176 |
72 |
177 (** Needed in State theory for the current definition of variables |
73 (** Needed in State theory for the current definition of variables |
178 where they are indexed by lists **) |
74 where they are indexed by lists **) |
179 |
75 |
180 Goal "i:list(nat) ==> i:univ(0)"; |
76 Goal "i:list(nat) ==> i:univ(0)"; |