|
1 (* Title: HOL/UNITY/UNITYMisc.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Some miscellaneous and add-hoc set theory concepts. |
|
7 |
|
8 *) |
|
9 |
|
10 Goalw [measure_def, less_than_def] |
|
11 "less_than(A) = {<x,y>:A*A. x<y}"; |
|
12 by Auto_tac; |
|
13 qed "less_than_equals"; |
|
14 |
|
15 Goalw [less_than_def] "wf(less_than(A))"; |
|
16 by (rtac wf_measure 1); |
|
17 qed "wf_less_than"; |
|
18 |
|
19 Goalw [less_than_def, measure_def] |
|
20 "less_than(A)<= A*A"; |
|
21 by Auto_tac; |
|
22 qed "less_than_subset"; |
|
23 |
|
24 Goalw [less_than_def, measure_def] |
|
25 "<x,y>:less_than(A) <-> (x:A & y:A & x<y)"; |
|
26 by Auto_tac; |
|
27 qed "less_than_iff"; |
|
28 |
|
29 Goalw [lessThan_def] |
|
30 "i:lessThan(k,A) <-> i:A & i<k"; |
|
31 by Auto_tac; |
|
32 qed "lessThan_iff"; |
|
33 |
|
34 Goalw [greaterThan_def] |
|
35 "i:greaterThan(k,A) <-> i:A & k<i"; |
|
36 by Auto_tac; |
|
37 qed "greaterThan_iff"; |
|
38 |
|
39 |
|
40 |
|
41 (** Needed for WF reasoning in WFair.ML **) |
|
42 |
|
43 Goal "k:A ==>less_than(A)``{k} = greaterThan(k, A)"; |
|
44 by (rtac equalityI 1); |
|
45 by (auto_tac (claset(), simpset() addsimps |
|
46 [less_than_iff,greaterThan_iff])); |
|
47 qed "Image_less_than"; |
|
48 |
|
49 Goal "k:A ==> less_than(A)-`` {k} = lessThan(k, A)"; |
|
50 by (rtac equalityI 1); |
|
51 by (auto_tac (claset(), simpset() addsimps |
|
52 [less_than_iff,lessThan_iff])); |
|
53 qed "Image_inverse_less_than"; |
|
54 |
|
55 Addsimps [Image_less_than, Image_inverse_less_than]; |
|
56 |
|
57 |
|
58 (** Ad-hoc set-theory rules **) |
|
59 |
|
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)"; |
|
93 by Auto_tac; |
|
94 qed "Int_Union_Union"; |
|
95 |
|
96 Goal "A Int Union(B) = (UN b:B. A Int b)"; |
|
97 by Auto_tac; |
|
98 qed "Int_Union_Union2"; |
|
99 |
|
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"; |
|
124 by (Blast_tac 1); |
|
125 qed "Un_Diff_Diff"; |
|
126 AddIffs [Un_Diff_Diff]; |
|
127 |
|
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 |
|
177 (** Needed in State theory for the current definition of variables |
|
178 where they are indexed by lists **) |
|
179 |
|
180 Goal "i:list(nat) ==> i:univ(0)"; |
|
181 by (dres_inst_tac [("B", "0")] list_into_univ 1); |
|
182 by (blast_tac (claset() addIs [nat_into_univ]) 1); |
|
183 by (assume_tac 1); |
|
184 qed "list_nat_into_univ"; |
|
185 |
|
186 (** To be moved to Update theory **) |
|
187 |
|
188 Goalw [update_def] |
|
189 "[| f:Pi(A,B); x:A; y:B(x) |] ==> f(x:=y):Pi(A, B)"; |
|
190 by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb, |
|
191 apply_funtype, lam_type]) 1); |
|
192 qed "update_type2"; |
|
193 |
|
194 (** Simplication rules for Collect; To be moved elsewhere **) |
|
195 Goal "{x:A. P(x)} Int A = {x:A. P(x)}"; |
|
196 by Auto_tac; |
|
197 qed "Collect_Int2"; |
|
198 |
|
199 Goal "A Int {x:A. P(x)} = {x:A. P(x)}"; |
|
200 by Auto_tac; |
|
201 qed "Collect_Int3"; |
|
202 |
|
203 AddIffs [Collect_Int2, Collect_Int3]; |
|
204 |
|
205 |
|
206 Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"; |
|
207 by Auto_tac; |
|
208 qed "Collect_disj_eq"; |
|
209 |
|
210 Goal "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"; |
|
211 by Auto_tac; |
|
212 qed "Collect_conj_eq"; |
|
213 |
|
214 |
|
215 |