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