|
1 (* Title: HOL/Library/Kleene_Algebra.thy |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 *) |
|
4 |
|
5 header "Kleene Algebra" |
|
6 |
|
7 theory Kleene_Algebra |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 text {* WARNING: This is work in progress. Expect changes in the future *} |
|
12 |
|
13 text {* A type class of Kleene algebras *} |
|
14 |
|
15 class star = |
|
16 fixes star :: "'a \<Rightarrow> 'a" |
|
17 |
|
18 class idem_add = ab_semigroup_add + |
|
19 assumes add_idem [simp]: "x + x = x" |
|
20 begin |
|
21 |
|
22 lemma add_idem2[simp]: "(x::'a) + (x + y) = x + y" |
|
23 unfolding add_assoc[symmetric] by simp |
|
24 |
|
25 end |
|
26 |
|
27 class order_by_add = idem_add + ord + |
|
28 assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b" |
|
29 assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" |
|
30 begin |
|
31 |
|
32 lemma ord_simp1[simp]: "x \<le> y \<Longrightarrow> x + y = y" |
|
33 unfolding order_def . |
|
34 |
|
35 lemma ord_simp2[simp]: "x \<le> y \<Longrightarrow> y + x = y" |
|
36 unfolding order_def add_commute . |
|
37 |
|
38 lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y" |
|
39 unfolding order_def . |
|
40 |
|
41 subclass order proof |
|
42 fix x y z :: 'a |
|
43 show "x \<le> x" unfolding order_def by simp |
|
44 show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z" |
|
45 proof (rule ord_intro) |
|
46 assume "x \<le> y" "y \<le> z" |
|
47 have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc) |
|
48 also have "\<dots> = y + z" by (simp add:`x \<le> y`) |
|
49 also have "\<dots> = z" by (simp add:`y \<le> z`) |
|
50 finally show "x + z = z" . |
|
51 qed |
|
52 show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" unfolding order_def |
|
53 by (simp add: add_commute) |
|
54 show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" by (fact strict_order_def) |
|
55 qed |
|
56 |
|
57 lemma plus_leI: |
|
58 "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z" |
|
59 unfolding order_def by (simp add: add_assoc) |
|
60 |
|
61 lemma less_add[simp]: "a \<le> a + b" "b \<le> a + b" |
|
62 unfolding order_def by (auto simp:add_ac) |
|
63 |
|
64 lemma add_est1: "a + b \<le> c \<Longrightarrow> a \<le> c" |
|
65 using less_add(1) by (rule order_trans) |
|
66 |
|
67 lemma add_est2: "a + b \<le> c \<Longrightarrow> b \<le> c" |
|
68 using less_add(2) by (rule order_trans) |
|
69 |
|
70 end |
|
71 |
|
72 class pre_kleene = semiring_1 + order_by_add |
|
73 begin |
|
74 |
|
75 subclass pordered_semiring proof |
|
76 fix x y z :: 'a |
|
77 |
|
78 assume "x \<le> y" |
|
79 |
|
80 show "z + x \<le> z + y" |
|
81 proof (rule ord_intro) |
|
82 have "z + x + (z + y) = x + y + z" by (simp add:add_ac) |
|
83 also have "\<dots> = z + y" by (simp add:`x \<le> y` add_ac) |
|
84 finally show "z + x + (z + y) = z + y" . |
|
85 qed |
|
86 |
|
87 show "z * x \<le> z * y" |
|
88 proof (rule ord_intro) |
|
89 from `x \<le> y` have "z * (x + y) = z * y" by simp |
|
90 thus "z * x + z * y = z * y" by (simp add:right_distrib) |
|
91 qed |
|
92 |
|
93 show "x * z \<le> y * z" |
|
94 proof (rule ord_intro) |
|
95 from `x \<le> y` have "(x + y) * z = y * z" by simp |
|
96 thus "x * z + y * z = y * z" by (simp add:left_distrib) |
|
97 qed |
|
98 qed |
|
99 |
|
100 lemma zero_minimum [simp]: "0 \<le> x" |
|
101 unfolding order_def by simp |
|
102 |
|
103 end |
|
104 |
|
105 class kleene = pre_kleene + star + |
|
106 assumes star1: "1 + a * star a \<le> star a" |
|
107 and star2: "1 + star a * a \<le> star a" |
|
108 and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x" |
|
109 and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x" |
|
110 begin |
|
111 |
|
112 lemma star3': |
|
113 assumes a: "b + a * x \<le> x" |
|
114 shows "star a * b \<le> x" |
|
115 proof (rule order_trans) |
|
116 from a have "b \<le> x" by (rule add_est1) |
|
117 show "star a * b \<le> star a * x" |
|
118 by (rule mult_mono) (auto simp:`b \<le> x`) |
|
119 |
|
120 from a have "a * x \<le> x" by (rule add_est2) |
|
121 with star3 show "star a * x \<le> x" . |
|
122 qed |
|
123 |
|
124 lemma star4': |
|
125 assumes a: "b + x * a \<le> x" |
|
126 shows "b * star a \<le> x" |
|
127 proof (rule order_trans) |
|
128 from a have "b \<le> x" by (rule add_est1) |
|
129 show "b * star a \<le> x * star a" |
|
130 by (rule mult_mono) (auto simp:`b \<le> x`) |
|
131 |
|
132 from a have "x * a \<le> x" by (rule add_est2) |
|
133 with star4 show "x * star a \<le> x" . |
|
134 qed |
|
135 |
|
136 lemma star_unfold_left: |
|
137 shows "1 + a * star a = star a" |
|
138 proof (rule antisym, rule star1) |
|
139 have "1 + a * (1 + a * star a) \<le> 1 + a * star a" |
|
140 apply (rule add_mono, rule) |
|
141 apply (rule mult_mono, auto) |
|
142 apply (rule star1) |
|
143 done |
|
144 with star3' have "star a * 1 \<le> 1 + a * star a" . |
|
145 thus "star a \<le> 1 + a * star a" by simp |
|
146 qed |
|
147 |
|
148 lemma star_unfold_right: "1 + star a * a = star a" |
|
149 proof (rule antisym, rule star2) |
|
150 have "1 + (1 + star a * a) * a \<le> 1 + star a * a" |
|
151 apply (rule add_mono, rule) |
|
152 apply (rule mult_mono, auto) |
|
153 apply (rule star2) |
|
154 done |
|
155 with star4' have "1 * star a \<le> 1 + star a * a" . |
|
156 thus "star a \<le> 1 + star a * a" by simp |
|
157 qed |
|
158 |
|
159 lemma star_zero[simp]: "star 0 = 1" |
|
160 by (fact star_unfold_left[of 0, simplified, symmetric]) |
|
161 |
|
162 lemma star_one[simp]: "star 1 = 1" |
|
163 by (metis add_idem2 eq_iff mult_1_right ord_simp2 star3 star_unfold_left) |
|
164 |
|
165 lemma one_less_star: "1 \<le> star x" |
|
166 by (metis less_add(1) star_unfold_left) |
|
167 |
|
168 lemma ka1: "x * star x \<le> star x" |
|
169 by (metis less_add(2) star_unfold_left) |
|
170 |
|
171 lemma star_mult_idem[simp]: "star x * star x = star x" |
|
172 by (metis add_commute add_est1 eq_iff mult_1_right right_distrib star3 star_unfold_left) |
|
173 |
|
174 lemma less_star: "x \<le> star x" |
|
175 by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum) |
|
176 |
|
177 lemma star_simulation: |
|
178 assumes a: "a * x = x * b" |
|
179 shows "star a * x = x * star b" |
|
180 proof (rule antisym) |
|
181 show "star a * x \<le> x * star b" |
|
182 proof (rule star3', rule order_trans) |
|
183 from a have "a * x \<le> x * b" by simp |
|
184 hence "a * x * star b \<le> x * b * star b" |
|
185 by (rule mult_mono) auto |
|
186 thus "x + a * (x * star b) \<le> x + x * b * star b" |
|
187 using add_mono by (auto simp: mult_assoc) |
|
188 show "\<dots> \<le> x * star b" |
|
189 proof - |
|
190 have "x * (1 + b * star b) \<le> x * star b" |
|
191 by (rule mult_mono[OF _ star1]) auto |
|
192 thus ?thesis |
|
193 by (simp add:right_distrib mult_assoc) |
|
194 qed |
|
195 qed |
|
196 show "x * star b \<le> star a * x" |
|
197 proof (rule star4', rule order_trans) |
|
198 from a have b: "x * b \<le> a * x" by simp |
|
199 have "star a * x * b \<le> star a * a * x" |
|
200 unfolding mult_assoc |
|
201 by (rule mult_mono[OF _ b]) auto |
|
202 thus "x + star a * x * b \<le> x + star a * a * x" |
|
203 using add_mono by auto |
|
204 show "\<dots> \<le> star a * x" |
|
205 proof - |
|
206 have "(1 + star a * a) * x \<le> star a * x" |
|
207 by (rule mult_mono[OF star2]) auto |
|
208 thus ?thesis |
|
209 by (simp add:left_distrib mult_assoc) |
|
210 qed |
|
211 qed |
|
212 qed |
|
213 |
|
214 lemma star_slide2[simp]: "star x * x = x * star x" |
|
215 by (metis star_simulation) |
|
216 |
|
217 lemma star_idemp[simp]: "star (star x) = star x" |
|
218 by (metis add_idem2 eq_iff less_star mult_1_right star3' star_mult_idem star_unfold_left) |
|
219 |
|
220 lemma star_slide[simp]: "star (x * y) * x = x * star (y * x)" |
|
221 by (auto simp: mult_assoc star_simulation) |
|
222 |
|
223 lemma star_one': |
|
224 assumes "p * p' = 1" "p' * p = 1" |
|
225 shows "p' * star a * p = star (p' * a * p)" |
|
226 proof - |
|
227 from assms |
|
228 have "p' * star a * p = p' * star (p * p' * a) * p" |
|
229 by simp |
|
230 also have "\<dots> = p' * p * star (p' * a * p)" |
|
231 by (simp add: mult_assoc) |
|
232 also have "\<dots> = star (p' * a * p)" |
|
233 by (simp add: assms) |
|
234 finally show ?thesis . |
|
235 qed |
|
236 |
|
237 lemma x_less_star[simp]: "x \<le> x * star a" |
|
238 proof - |
|
239 have "x \<le> x * (1 + a * star a)" by (simp add: right_distrib) |
|
240 also have "\<dots> = x * star a" by (simp only: star_unfold_left) |
|
241 finally show ?thesis . |
|
242 qed |
|
243 |
|
244 lemma star_mono: "x \<le> y \<Longrightarrow> star x \<le> star y" |
|
245 by (metis add_commute eq_iff less_star ord_simp2 order_trans star3 star4' star_idemp star_mult_idem x_less_star) |
|
246 |
|
247 lemma star_sub: "x \<le> 1 \<Longrightarrow> star x = 1" |
|
248 by (metis add_commute ord_simp1 star_idemp star_mono star_mult_idem star_one star_unfold_left) |
|
249 |
|
250 lemma star_unfold2: "star x * y = y + x * star x * y" |
|
251 by (subst star_unfold_right[symmetric]) (simp add: mult_assoc left_distrib) |
|
252 |
|
253 lemma star_absorb_one[simp]: "star (x + 1) = star x" |
|
254 by (metis add_commute eq_iff left_distrib less_add(1) less_add(2) mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star) |
|
255 |
|
256 lemma star_absorb_one'[simp]: "star (1 + x) = star x" |
|
257 by (subst add_commute) (fact star_absorb_one) |
|
258 |
|
259 lemma ka16: "(y * star x) * star (y * star x) \<le> star x * star (y * star x)" |
|
260 by (metis ka1 less_add(1) mult_assoc order_trans star_unfold2) |
|
261 |
|
262 lemma ka16': "(star x * y) * star (star x * y) \<le> star (star x * y) * star x" |
|
263 by (metis ka1 mult_assoc order_trans star_slide x_less_star) |
|
264 |
|
265 lemma ka17: "(x * star x) * star (y * star x) \<le> star x * star (y * star x)" |
|
266 by (metis ka1 mult_assoc mult_right_mono zero_minimum) |
|
267 |
|
268 lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x) |
|
269 \<le> star x * star (y * star x)" |
|
270 by (metis ka16 ka17 left_distrib mult_assoc plus_leI) |
|
271 |
|
272 lemma kleene_church_rosser: |
|
273 "star y * star x \<le> star x * star y \<Longrightarrow> star (x + y) \<le> star x * star y" |
|
274 oops |
|
275 |
|
276 lemma star_decomp: "star (a + b) = star a * star (b * star a)" |
|
277 oops |
|
278 |
|
279 lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow> star y * star x \<le> star x * star y" |
|
280 by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum) |
|
281 |
|
282 lemma ka23: "star y * star x \<le> star x * star y \<Longrightarrow> y * star x \<le> star x * star y" |
|
283 by (metis less_star mult_right_mono order_trans zero_minimum) |
|
284 |
|
285 lemma ka24: "star (x + y) \<le> star (star x * star y)" |
|
286 by (metis add_est1 add_est2 less_add(1) mult_assoc order_def plus_leI star_absorb_one star_mono star_slide2 star_unfold2 star_unfold_left x_less_star) |
|
287 |
|
288 lemma ka25: "star y * star x \<le> star x * star y \<Longrightarrow> star (star y * star x) \<le> star x * star y" |
|
289 oops |
|
290 |
|
291 lemma kleene_bubblesort: "y * x \<le> x * y \<Longrightarrow> star (x + y) \<le> star x * star y" |
|
292 oops |
|
293 |
|
294 end |
|
295 |
|
296 subsection {* Complete lattices are Kleene algebras *} |
|
297 |
|
298 lemma (in complete_lattice) le_SUPI': |
|
299 assumes "l \<le> M i" |
|
300 shows "l \<le> (SUP i. M i)" |
|
301 using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I]) |
|
302 |
|
303 class kleene_by_complete_lattice = pre_kleene |
|
304 + complete_lattice + power + star + |
|
305 assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)" |
|
306 begin |
|
307 |
|
308 subclass kleene |
|
309 proof |
|
310 fix a x :: 'a |
|
311 |
|
312 have [simp]: "1 \<le> star a" |
|
313 unfolding star_cont[of 1 a 1, simplified] |
|
314 by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I]) |
|
315 |
|
316 show "1 + a * star a \<le> star a" |
|
317 apply (rule plus_leI, simp) |
|
318 apply (simp add:star_cont[of a a 1, simplified]) |
|
319 apply (simp add:star_cont[of 1 a 1, simplified]) |
|
320 apply (subst power_Suc[symmetric]) |
|
321 by (intro SUP_leI le_SUPI UNIV_I) |
|
322 |
|
323 show "1 + star a * a \<le> star a" |
|
324 apply (rule plus_leI, simp) |
|
325 apply (simp add:star_cont[of 1 a a, simplified]) |
|
326 apply (simp add:star_cont[of 1 a 1, simplified]) |
|
327 by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc) |
|
328 |
|
329 show "a * x \<le> x \<Longrightarrow> star a * x \<le> x" |
|
330 proof - |
|
331 assume a: "a * x \<le> x" |
|
332 |
|
333 { |
|
334 fix n |
|
335 have "a ^ (Suc n) * x \<le> a ^ n * x" |
|
336 proof (induct n) |
|
337 case 0 thus ?case by (simp add: a) |
|
338 next |
|
339 case (Suc n) |
|
340 hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)" |
|
341 by (auto intro: mult_mono) |
|
342 thus ?case |
|
343 by (simp add: mult_assoc) |
|
344 qed |
|
345 } |
|
346 note a = this |
|
347 |
|
348 { |
|
349 fix n have "a ^ n * x \<le> x" |
|
350 proof (induct n) |
|
351 case 0 show ?case by simp |
|
352 next |
|
353 case (Suc n) with a[of n] |
|
354 show ?case by simp |
|
355 qed |
|
356 } |
|
357 note b = this |
|
358 |
|
359 show "star a * x \<le> x" |
|
360 unfolding star_cont[of 1 a x, simplified] |
|
361 by (rule SUP_leI) (rule b) |
|
362 qed |
|
363 |
|
364 show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *) |
|
365 proof - |
|
366 assume a: "x * a \<le> x" |
|
367 |
|
368 { |
|
369 fix n |
|
370 have "x * a ^ (Suc n) \<le> x * a ^ n" |
|
371 proof (induct n) |
|
372 case 0 thus ?case by (simp add: a) |
|
373 next |
|
374 case (Suc n) |
|
375 hence "(x * a ^ Suc n) * a \<le> (x * a ^ n) * a" |
|
376 by (auto intro: mult_mono) |
|
377 thus ?case |
|
378 by (simp add: power_commutes mult_assoc) |
|
379 qed |
|
380 } |
|
381 note a = this |
|
382 |
|
383 { |
|
384 fix n have "x * a ^ n \<le> x" |
|
385 proof (induct n) |
|
386 case 0 show ?case by simp |
|
387 next |
|
388 case (Suc n) with a[of n] |
|
389 show ?case by simp |
|
390 qed |
|
391 } |
|
392 note b = this |
|
393 |
|
394 show "x * star a \<le> x" |
|
395 unfolding star_cont[of x a 1, simplified] |
|
396 by (rule SUP_leI) (rule b) |
|
397 qed |
|
398 qed |
|
399 |
|
400 end |
|
401 |
|
402 |
|
403 subsection {* Transitive Closure *} |
|
404 |
|
405 context kleene |
|
406 begin |
|
407 |
|
408 definition |
|
409 tcl_def: "tcl x = star x * x" |
|
410 |
|
411 lemma tcl_zero: "tcl 0 = 0" |
|
412 unfolding tcl_def by simp |
|
413 |
|
414 lemma tcl_unfold_right: "tcl a = a + tcl a * a" |
|
415 proof - |
|
416 from star_unfold_right[of a] |
|
417 have "a * (1 + star a * a) = a * star a" by simp |
|
418 from this[simplified right_distrib, simplified] |
|
419 show ?thesis |
|
420 by (simp add:tcl_def mult_assoc) |
|
421 qed |
|
422 |
|
423 lemma less_tcl: "a \<le> tcl a" |
|
424 proof - |
|
425 have "a \<le> a + tcl a * a" by simp |
|
426 also have "\<dots> = tcl a" by (rule tcl_unfold_right[symmetric]) |
|
427 finally show ?thesis . |
|
428 qed |
|
429 |
|
430 end |
|
431 |
|
432 |
|
433 subsection {* Naive Algorithm to generate the transitive closure *} |
|
434 |
|
435 function (default "\<lambda>x. 0", tailrec, domintros) |
|
436 mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a" |
|
437 where |
|
438 "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))" |
|
439 by pat_completeness simp |
|
440 |
|
441 declare mk_tcl.simps[simp del] (* loops *) |
|
442 |
|
443 lemma mk_tcl_code[code]: |
|
444 "mk_tcl A X = |
|
445 (let XA = X * A |
|
446 in if XA \<le> X then X else mk_tcl A (X + XA))" |
|
447 unfolding mk_tcl.simps[of A X] Let_def .. |
|
448 |
|
449 context kleene |
|
450 begin |
|
451 |
|
452 lemma mk_tcl_lemma1: |
|
453 "(X + X * A) * star A = X * star A" |
|
454 proof - |
|
455 have "A * star A \<le> 1 + A * star A" by simp |
|
456 also have "\<dots> = star A" by (simp add:star_unfold_left) |
|
457 finally have "star A + A * star A = star A" by simp |
|
458 hence "X * (star A + A * star A) = X * star A" by simp |
|
459 thus ?thesis by (simp add:left_distrib right_distrib mult_assoc) |
|
460 qed |
|
461 |
|
462 lemma mk_tcl_lemma2: |
|
463 shows "X * A \<le> X \<Longrightarrow> X * star A = X" |
|
464 by (rule antisym) (auto simp:star4) |
|
465 |
|
466 end |
|
467 |
|
468 lemma mk_tcl_correctness: |
|
469 fixes X :: "'a::kleene" |
|
470 assumes "mk_tcl_dom (A, X)" |
|
471 shows "mk_tcl A X = X * star A" |
|
472 using assms |
|
473 by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2) |
|
474 |
|
475 |
|
476 lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x" |
|
477 by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases) |
|
478 |
|
479 lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0" |
|
480 unfolding mk_tcl_def |
|
481 by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom]) |
|
482 |
|
483 |
|
484 text {* We can replace the dom-Condition of the correctness theorem |
|
485 with something executable *} |
|
486 |
|
487 lemma mk_tcl_correctness2: |
|
488 fixes A X :: "'a :: {kleene}" |
|
489 assumes "mk_tcl A A \<noteq> 0" |
|
490 shows "mk_tcl A A = tcl A" |
|
491 using assms mk_tcl_default mk_tcl_correctness |
|
492 unfolding tcl_def |
|
493 by auto |
|
494 |
|
495 end |