author | paulson |
Thu, 12 Apr 2001 12:45:05 +0200 | |
changeset 11251 | a6816d47f41d |
parent 11175 | 56ab6a5ba351 |
child 12516 | d09d0f160888 |
permissions | -rw-r--r-- |
10496 | 1 |
(* Title: HOL/BCV/Semilat.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 2000 TUM |
|
5 |
||
6 |
Semilattices |
|
7 |
*) |
|
8 |
||
9 |
header "Semilattices" |
|
10 |
||
11 |
theory Semilat = Main: |
|
12 |
||
13 |
types 'a ord = "'a => 'a => bool" |
|
14 |
'a binop = "'a => 'a => 'a" |
|
15 |
'a sl = "'a set * 'a ord * 'a binop" |
|
16 |
||
17 |
consts |
|
18 |
"@lesub" :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50) |
|
19 |
"@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50) |
|
20 |
defs |
|
21 |
lesub_def: "x <=_r y == r x y" |
|
22 |
lesssub_def: "x <_r y == x <=_r y & x ~= y" |
|
23 |
||
24 |
consts |
|
25 |
"@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65) |
|
26 |
defs |
|
27 |
plussub_def: "x +_f y == f x y" |
|
28 |
||
29 |
||
30 |
constdefs |
|
31 |
ord :: "('a*'a)set => 'a ord" |
|
32 |
"ord r == %x y. (x,y):r" |
|
33 |
||
34 |
order :: "'a ord => bool" |
|
35 |
"order r == (!x. x <=_r x) & |
|
36 |
(!x y. x <=_r y & y <=_r x --> x=y) & |
|
37 |
(!x y z. x <=_r y & y <=_r z --> x <=_r z)" |
|
38 |
||
39 |
acc :: "'a ord => bool" |
|
40 |
"acc r == wf{(y,x) . x <_r y}" |
|
41 |
||
42 |
top :: "'a ord => 'a => bool" |
|
43 |
"top r T == !x. x <=_r T" |
|
44 |
||
45 |
closed :: "'a set => 'a binop => bool" |
|
46 |
"closed A f == !x:A. !y:A. x +_f y : A" |
|
47 |
||
48 |
semilat :: "'a sl => bool" |
|
49 |
"semilat == %(A,r,f). order r & closed A f & |
|
50 |
(!x:A. !y:A. x <=_r x +_f y) & |
|
51 |
(!x:A. !y:A. y <=_r x +_f y) & |
|
52 |
(!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)" |
|
53 |
||
54 |
is_ub :: "('a*'a)set => 'a => 'a => 'a => bool" |
|
55 |
"is_ub r x y u == (x,u):r & (y,u):r" |
|
56 |
||
57 |
is_lub :: "('a*'a)set => 'a => 'a => 'a => bool" |
|
58 |
"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)" |
|
59 |
||
60 |
some_lub :: "('a*'a)set => 'a => 'a => 'a" |
|
61 |
"some_lub r x y == SOME z. is_lub r x y z" |
|
62 |
||
63 |
||
64 |
lemma order_refl [simp, intro]: |
|
65 |
"order r ==> x <=_r x"; |
|
66 |
by (simp add: order_def) |
|
67 |
||
68 |
lemma order_antisym: |
|
69 |
"[| order r; x <=_r y; y <=_r x |] ==> x = y" |
|
70 |
apply (unfold order_def) |
|
71 |
apply (simp (no_asm_simp)) |
|
72 |
done |
|
73 |
||
74 |
lemma order_trans: |
|
75 |
"[| order r; x <=_r y; y <=_r z |] ==> x <=_r z" |
|
76 |
apply (unfold order_def) |
|
77 |
apply blast |
|
78 |
done |
|
79 |
||
80 |
lemma order_less_irrefl [intro, simp]: |
|
81 |
"order r ==> ~ x <_r x" |
|
82 |
apply (unfold order_def lesssub_def) |
|
83 |
apply blast |
|
84 |
done |
|
85 |
||
86 |
lemma order_less_trans: |
|
87 |
"[| order r; x <_r y; y <_r z |] ==> x <_r z" |
|
88 |
apply (unfold order_def lesssub_def) |
|
89 |
apply blast |
|
90 |
done |
|
91 |
||
92 |
lemma topD [simp, intro]: |
|
93 |
"top r T ==> x <=_r T" |
|
94 |
by (simp add: top_def) |
|
95 |
||
96 |
lemma top_le_conv [simp]: |
|
97 |
"[| order r; top r T |] ==> (T <=_r x) = (x = T)" |
|
98 |
by (blast intro: order_antisym) |
|
99 |
||
100 |
lemma semilat_Def: |
|
101 |
"semilat(A,r,f) == order r & closed A f & |
|
102 |
(!x:A. !y:A. x <=_r x +_f y) & |
|
103 |
(!x:A. !y:A. y <=_r x +_f y) & |
|
104 |
(!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)" |
|
10918 | 105 |
apply (unfold semilat_def split_conv [THEN eq_reflection]) |
10496 | 106 |
apply (rule refl [THEN eq_reflection]) |
107 |
done |
|
108 |
||
109 |
lemma semilatDorderI [simp, intro]: |
|
110 |
"semilat(A,r,f) ==> order r" |
|
111 |
by (simp add: semilat_Def) |
|
112 |
||
113 |
lemma semilatDclosedI [simp, intro]: |
|
114 |
"semilat(A,r,f) ==> closed A f" |
|
115 |
apply (unfold semilat_Def) |
|
116 |
apply simp |
|
117 |
done |
|
118 |
||
119 |
lemma semilat_ub1 [simp]: |
|
120 |
"[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y" |
|
121 |
by (unfold semilat_Def, simp) |
|
122 |
||
123 |
lemma semilat_ub2 [simp]: |
|
124 |
"[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y" |
|
125 |
by (unfold semilat_Def, simp) |
|
126 |
||
127 |
lemma semilat_lub [simp]: |
|
128 |
"[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z"; |
|
129 |
by (unfold semilat_Def, simp) |
|
130 |
||
131 |
||
132 |
lemma plus_le_conv [simp]: |
|
133 |
"[| x:A; y:A; z:A; semilat(A,r,f) |] |
|
134 |
==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)" |
|
135 |
apply (unfold semilat_Def) |
|
136 |
apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans) |
|
137 |
done |
|
138 |
||
139 |
lemma le_iff_plus_unchanged: |
|
140 |
"[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)" |
|
141 |
apply (rule iffI) |
|
142 |
apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+) |
|
143 |
apply (erule subst) |
|
144 |
apply simp |
|
145 |
done |
|
146 |
||
147 |
lemma le_iff_plus_unchanged2: |
|
148 |
"[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)" |
|
149 |
apply (rule iffI) |
|
150 |
apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+) |
|
151 |
apply (erule subst) |
|
152 |
apply simp |
|
153 |
done |
|
154 |
||
155 |
||
156 |
lemma closedD: |
|
157 |
"[| closed A f; x:A; y:A |] ==> x +_f y : A" |
|
158 |
apply (unfold closed_def) |
|
159 |
apply blast |
|
160 |
done |
|
161 |
||
162 |
lemma closed_UNIV [simp]: "closed UNIV f" |
|
163 |
by (simp add: closed_def) |
|
164 |
||
165 |
||
166 |
lemma is_lubD: |
|
167 |
"is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)" |
|
168 |
by (simp add: is_lub_def) |
|
169 |
||
170 |
lemma is_ubI: |
|
171 |
"[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u" |
|
172 |
by (simp add: is_ub_def) |
|
173 |
||
174 |
lemma is_ubD: |
|
175 |
"is_ub r x y u ==> (x,u) : r & (y,u) : r" |
|
176 |
by (simp add: is_ub_def) |
|
177 |
||
178 |
||
179 |
lemma is_lub_bigger1 [iff]: |
|
180 |
"is_lub (r^* ) x y y = ((x,y):r^* )" |
|
181 |
apply (unfold is_lub_def is_ub_def) |
|
182 |
apply blast |
|
183 |
done |
|
184 |
||
185 |
lemma is_lub_bigger2 [iff]: |
|
186 |
"is_lub (r^* ) x y x = ((y,x):r^* )" |
|
187 |
apply (unfold is_lub_def is_ub_def) |
|
188 |
apply blast |
|
189 |
done |
|
190 |
||
191 |
lemma extend_lub: |
|
10797 | 192 |
"[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |] |
10496 | 193 |
==> EX v. is_lub (r^* ) x' y v" |
194 |
apply (unfold is_lub_def is_ub_def) |
|
195 |
apply (case_tac "(y,x) : r^*") |
|
196 |
apply (case_tac "(y,x') : r^*") |
|
197 |
apply blast |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
11085
diff
changeset
|
198 |
apply (blast elim: converse_rtranclE dest: single_valuedD) |
10496 | 199 |
apply (rule exI) |
200 |
apply (rule conjI) |
|
10797 | 201 |
apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD) |
10496 | 202 |
apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2 |
10797 | 203 |
elim: converse_rtranclE dest: single_valuedD) |
10496 | 204 |
done |
205 |
||
10797 | 206 |
lemma single_valued_has_lubs [rule_format]: |
207 |
"[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> |
|
10496 | 208 |
(EX z. is_lub (r^* ) x y z))" |
209 |
apply (erule converse_rtrancl_induct) |
|
210 |
apply clarify |
|
211 |
apply (erule converse_rtrancl_induct) |
|
212 |
apply blast |
|
213 |
apply (blast intro: rtrancl_into_rtrancl2) |
|
214 |
apply (blast intro: extend_lub) |
|
215 |
done |
|
216 |
||
217 |
lemma some_lub_conv: |
|
218 |
"[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u" |
|
219 |
apply (unfold some_lub_def is_lub_def) |
|
220 |
apply (rule someI2) |
|
221 |
apply assumption |
|
222 |
apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl) |
|
223 |
done |
|
224 |
||
225 |
lemma is_lub_some_lub: |
|
10797 | 226 |
"[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] |
10496 | 227 |
==> is_lub (r^* ) x y (some_lub (r^* ) x y)"; |
10797 | 228 |
by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv) |
10496 | 229 |
|
230 |
end |