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