3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 *) |
5 *) |
6 |
6 |
7 Goalw [order_def] "order r ==> x <=_r x"; |
7 Goalw [order_def] "order r ==> x <=_r x"; |
8 by(Asm_simp_tac 1); |
8 by (Asm_simp_tac 1); |
9 qed "order_refl"; |
9 qed "order_refl"; |
10 Addsimps [order_refl]; |
10 Addsimps [order_refl]; |
11 AddIs [order_refl]; |
11 AddIs [order_refl]; |
12 |
12 |
13 Goalw [order_def] "[| order r; x <=_r y; y <=_r x |] ==> x = y"; |
13 Goalw [order_def] "[| order r; x <=_r y; y <=_r x |] ==> x = y"; |
14 by(Asm_simp_tac 1); |
14 by (Asm_simp_tac 1); |
15 qed "order_antisym"; |
15 qed "order_antisym"; |
16 |
16 |
17 Goalw [order_def] "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"; |
17 Goalw [order_def] "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"; |
18 by(Blast_tac 1); |
18 by (Blast_tac 1); |
19 qed "order_trans"; |
19 qed "order_trans"; |
20 |
20 |
21 Goalw [order_def,lesssub_def] "order r ==> ~ x <_r x"; |
21 Goalw [order_def,lesssub_def] "order r ==> ~ x <_r x"; |
22 by(Blast_tac 1); |
22 by (Blast_tac 1); |
23 qed "order_less_irrefl"; |
23 qed "order_less_irrefl"; |
24 AddIs [order_less_irrefl]; |
24 AddIs [order_less_irrefl]; |
25 Addsimps [order_less_irrefl]; |
25 Addsimps [order_less_irrefl]; |
26 |
26 |
27 Goalw [order_def,lesssub_def] "[| order r; x <_r y; y <_r z |] ==> x <_r z"; |
27 Goalw [order_def,lesssub_def] "[| order r; x <_r y; y <_r z |] ==> x <_r z"; |
28 by(Blast_tac 1); |
28 by (Blast_tac 1); |
29 qed "order_less_trans"; |
29 qed "order_less_trans"; |
30 |
30 |
31 Goalw [top_def] "top r T ==> x <=_r T"; |
31 Goalw [top_def] "top r T ==> x <=_r T"; |
32 by(Asm_simp_tac 1); |
32 by (Asm_simp_tac 1); |
33 qed "topD"; |
33 qed "topD"; |
34 Addsimps [topD]; |
34 Addsimps [topD]; |
35 AddIs [topD]; |
35 AddIs [topD]; |
36 |
36 |
37 Goal "[| order r; top r T |] ==> (T <=_r x) = (x = T)"; |
37 Goal "[| order r; top r T |] ==> (T <=_r x) = (x = T)"; |
38 by(blast_tac (claset() addIs [order_antisym]) 1); |
38 by (blast_tac (claset() addIs [order_antisym]) 1); |
39 qed "top_le_conv"; |
39 qed "top_le_conv"; |
40 Addsimps [top_le_conv]; |
40 Addsimps [top_le_conv]; |
41 |
41 |
42 Goalw [semilat_def,split RS eq_reflection] |
42 Goalw [semilat_def,split RS eq_reflection] |
43 "semilat(A,r,f) == order r & closed A f & \ |
43 "semilat(A,r,f) == order r & closed A f & \ |
44 \ (!x:A. !y:A. x <=_r x +_f y) & \ |
44 \ (!x:A. !y:A. x <=_r x +_f y) & \ |
45 \ (!x:A. !y:A. y <=_r x +_f y) & \ |
45 \ (!x:A. !y:A. y <=_r x +_f y) & \ |
46 \ (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"; |
46 \ (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"; |
47 br (refl RS eq_reflection) 1; |
47 by (rtac (refl RS eq_reflection) 1); |
48 qed "semilat_Def"; |
48 qed "semilat_Def"; |
49 |
49 |
50 Goalw [semilat_Def] "semilat(A,r,f) ==> order r"; |
50 Goalw [semilat_Def] "semilat(A,r,f) ==> order r"; |
51 by(Asm_simp_tac 1); |
51 by (Asm_simp_tac 1); |
52 qed "semilatDorderI"; |
52 qed "semilatDorderI"; |
53 Addsimps [semilatDorderI]; |
53 Addsimps [semilatDorderI]; |
54 AddIs [semilatDorderI]; |
54 AddIs [semilatDorderI]; |
55 |
55 |
56 Goalw [semilat_Def] "semilat(A,r,f) ==> closed A f"; |
56 Goalw [semilat_Def] "semilat(A,r,f) ==> closed A f"; |
57 by(Asm_simp_tac 1); |
57 by (Asm_simp_tac 1); |
58 qed "semilatDclosedI"; |
58 qed "semilatDclosedI"; |
59 Addsimps [semilatDclosedI]; |
59 Addsimps [semilatDclosedI]; |
60 AddIs [semilatDclosedI]; |
60 AddIs [semilatDclosedI]; |
61 |
61 |
62 Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"; |
62 Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"; |
63 by(Asm_simp_tac 1); |
63 by (Asm_simp_tac 1); |
64 qed "semilat_ub1"; |
64 qed "semilat_ub1"; |
65 |
65 |
66 Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"; |
66 Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"; |
67 by(Asm_simp_tac 1); |
67 by (Asm_simp_tac 1); |
68 qed "semilat_ub2"; |
68 qed "semilat_ub2"; |
69 |
69 |
70 Goalw [semilat_Def] |
70 Goalw [semilat_Def] |
71 "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z"; |
71 "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z"; |
72 by(Asm_simp_tac 1); |
72 by (Asm_simp_tac 1); |
73 qed "semilat_lub"; |
73 qed "semilat_lub"; |
74 |
74 |
75 Addsimps [semilat_ub1,semilat_ub2,semilat_lub]; |
75 Addsimps [semilat_ub1,semilat_ub2,semilat_lub]; |
76 |
76 |
77 Goalw [semilat_Def] |
77 Goalw [semilat_Def] |
96 qed "le_iff_plus_unchanged2"; |
96 qed "le_iff_plus_unchanged2"; |
97 |
97 |
98 (*** closed ***) |
98 (*** closed ***) |
99 |
99 |
100 Goalw [closed_def] "[| closed A f; x:A; y:A |] ==> x +_f y : A"; |
100 Goalw [closed_def] "[| closed A f; x:A; y:A |] ==> x +_f y : A"; |
101 by(Blast_tac 1); |
101 by (Blast_tac 1); |
102 qed "closedD"; |
102 qed "closedD"; |
103 |
103 |
104 Goalw [closed_def] "closed UNIV f"; |
104 Goalw [closed_def] "closed UNIV f"; |
105 by(Simp_tac 1); |
105 by (Simp_tac 1); |
106 qed "closed_UNIV"; |
106 qed "closed_UNIV"; |
107 AddIffs [closed_UNIV]; |
107 AddIffs [closed_UNIV]; |
108 |
108 |
109 (*** lub ***) |
109 (*** lub ***) |
110 |
110 |
111 Goalw [is_lub_def] |
111 Goalw [is_lub_def] |
112 "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"; |
112 "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"; |
113 ba 1; |
113 by (assume_tac 1); |
114 qed "is_lubD"; |
114 qed "is_lubD"; |
115 |
115 |
116 Goalw [is_ub_def] |
116 Goalw [is_ub_def] |
117 "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"; |
117 "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"; |
118 by(Asm_simp_tac 1); |
118 by (Asm_simp_tac 1); |
119 qed "is_ubI"; |
119 qed "is_ubI"; |
120 |
120 |
121 Goalw [is_ub_def] |
121 Goalw [is_ub_def] |
122 "is_ub r x y u ==> (x,u) : r & (y,u) : r"; |
122 "is_ub r x y u ==> (x,u) : r & (y,u) : r"; |
123 ba 1; |
123 by (assume_tac 1); |
124 qed "is_ubD"; |
124 qed "is_ubD"; |
125 |
125 |
126 |
126 |
127 Goalw [is_lub_def,is_ub_def] "is_lub (r^*) x y y = ((x,y):r^*)"; |
127 Goalw [is_lub_def,is_ub_def] "is_lub (r^*) x y y = ((x,y):r^*)"; |
128 by (Blast_tac 1); |
128 by (Blast_tac 1); |
136 |
136 |
137 |
137 |
138 Goalw [is_lub_def,is_ub_def] |
138 Goalw [is_lub_def,is_ub_def] |
139 "[| univalent r; is_lub (r^*) x y u; (x',x) : r |] ==> \ |
139 "[| univalent r; is_lub (r^*) x y u; (x',x) : r |] ==> \ |
140 \ EX v. is_lub (r^*) x' y v"; |
140 \ EX v. is_lub (r^*) x' y v"; |
141 by(case_tac "(y,x) : r^*" 1); |
141 by (case_tac "(y,x) : r^*" 1); |
142 by(case_tac "(y,x') : r^*" 1); |
142 by (case_tac "(y,x') : r^*" 1); |
143 by (Blast_tac 1); |
143 by (Blast_tac 1); |
144 by(blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE] |
144 by (blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE] |
145 addDs [univalentD]) 1); |
145 addDs [univalentD]) 1); |
146 br exI 1; |
146 by (rtac exI 1); |
147 br conjI 1; |
147 by (rtac conjI 1); |
148 by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1); |
148 by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1); |
149 by(blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2] |
149 by (blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2] |
150 addEs [converse_rtranclE] addDs [univalentD]) 1); |
150 addEs [converse_rtranclE] addDs [univalentD]) 1); |
151 qed "extend_lub"; |
151 qed "extend_lub"; |
152 |
152 |
153 Goal "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \ |
153 Goal "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \ |
154 \ (EX z. is_lub (r^*) x y z))"; |
154 \ (EX z. is_lub (r^*) x y z))"; |
155 by(etac converse_rtrancl_induct 1); |
155 by (etac converse_rtrancl_induct 1); |
156 by(Clarify_tac 1); |
156 by (Clarify_tac 1); |
157 by(etac converse_rtrancl_induct 1); |
157 by (etac converse_rtrancl_induct 1); |
158 by(Blast_tac 1); |
158 by (Blast_tac 1); |
159 by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
159 by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
160 by(blast_tac (claset() addIs [extend_lub]) 1); |
160 by (blast_tac (claset() addIs [extend_lub]) 1); |
161 qed_spec_mp "univalent_has_lubs"; |
161 qed_spec_mp "univalent_has_lubs"; |
162 |
162 |
163 Goalw [some_lub_def,is_lub_def] |
163 Goalw [some_lub_def,is_lub_def] |
164 "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u"; |
164 "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u"; |
165 br someI2 1; |
165 by (rtac someI2 1); |
166 ba 1; |
166 by (assume_tac 1); |
167 by(blast_tac (claset() addIs [antisymD] |
167 by (blast_tac (claset() addIs [antisymD] |
168 addSDs [acyclic_impl_antisym_rtrancl]) 1); |
168 addSDs [acyclic_impl_antisym_rtrancl]) 1); |
169 qed "some_lub_conv"; |
169 qed "some_lub_conv"; |
170 |
170 |
171 Goal |
171 Goal |
172 "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \ |
172 "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \ |
173 \ is_lub (r^*) x y (some_lub (r^*) x y)"; |
173 \ is_lub (r^*) x y (some_lub (r^*) x y)"; |
174 by(fast_tac |
174 by (fast_tac |
175 (claset() addDs [univalent_has_lubs] |
175 (claset() addDs [univalent_has_lubs] |
176 addss (simpset() addsimps [some_lub_conv])) 1); |
176 addss (simpset() addsimps [some_lub_conv])) 1); |
177 qed "is_lub_some_lub"; |
177 qed "is_lub_some_lub"; |