31990
|
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)"
|
32238
|
277 |
proof (rule antisym)
|
|
278 |
have "1 + (a + b) * star a * star (b * star a) \<le>
|
|
279 |
1 + a * star a * star (b * star a) + b * star a * star (b * star a)"
|
|
280 |
by (metis add_commute add_left_commute eq_iff left_distrib mult_assoc)
|
|
281 |
also have "\<dots> \<le> star a * star (b * star a)"
|
|
282 |
by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
|
|
283 |
finally show "star (a + b) \<le> star a * star (b * star a)"
|
|
284 |
by (metis mult_1_right mult_assoc star3')
|
|
285 |
next
|
|
286 |
show "star a * star (b * star a) \<le> star (a + b)"
|
|
287 |
by (metis add_assoc add_est1 add_est2 add_left_commute less_star mult_mono'
|
|
288 |
star_absorb_one star_absorb_one' star_idemp star_mono star_mult_idem zero_minimum)
|
|
289 |
qed
|
31990
|
290 |
|
|
291 |
lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow> star y * star x \<le> star x * star y"
|
|
292 |
by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)
|
|
293 |
|
|
294 |
lemma ka23: "star y * star x \<le> star x * star y \<Longrightarrow> y * star x \<le> star x * star y"
|
|
295 |
by (metis less_star mult_right_mono order_trans zero_minimum)
|
|
296 |
|
|
297 |
lemma ka24: "star (x + y) \<le> star (star x * star y)"
|
|
298 |
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)
|
|
299 |
|
|
300 |
lemma ka25: "star y * star x \<le> star x * star y \<Longrightarrow> star (star y * star x) \<le> star x * star y"
|
|
301 |
oops
|
|
302 |
|
|
303 |
lemma kleene_bubblesort: "y * x \<le> x * y \<Longrightarrow> star (x + y) \<le> star x * star y"
|
|
304 |
oops
|
|
305 |
|
|
306 |
end
|
|
307 |
|
|
308 |
subsection {* Complete lattices are Kleene algebras *}
|
|
309 |
|
|
310 |
lemma (in complete_lattice) le_SUPI':
|
|
311 |
assumes "l \<le> M i"
|
|
312 |
shows "l \<le> (SUP i. M i)"
|
|
313 |
using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
|
|
314 |
|
|
315 |
class kleene_by_complete_lattice = pre_kleene
|
|
316 |
+ complete_lattice + power + star +
|
|
317 |
assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
|
|
318 |
begin
|
|
319 |
|
|
320 |
subclass kleene
|
|
321 |
proof
|
|
322 |
fix a x :: 'a
|
|
323 |
|
|
324 |
have [simp]: "1 \<le> star a"
|
|
325 |
unfolding star_cont[of 1 a 1, simplified]
|
|
326 |
by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
|
|
327 |
|
|
328 |
show "1 + a * star a \<le> star a"
|
|
329 |
apply (rule plus_leI, simp)
|
|
330 |
apply (simp add:star_cont[of a a 1, simplified])
|
|
331 |
apply (simp add:star_cont[of 1 a 1, simplified])
|
|
332 |
apply (subst power_Suc[symmetric])
|
|
333 |
by (intro SUP_leI le_SUPI UNIV_I)
|
|
334 |
|
|
335 |
show "1 + star a * a \<le> star a"
|
|
336 |
apply (rule plus_leI, simp)
|
|
337 |
apply (simp add:star_cont[of 1 a a, simplified])
|
|
338 |
apply (simp add:star_cont[of 1 a 1, simplified])
|
|
339 |
by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
|
|
340 |
|
|
341 |
show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
|
|
342 |
proof -
|
|
343 |
assume a: "a * x \<le> x"
|
|
344 |
|
|
345 |
{
|
|
346 |
fix n
|
|
347 |
have "a ^ (Suc n) * x \<le> a ^ n * x"
|
|
348 |
proof (induct n)
|
|
349 |
case 0 thus ?case by (simp add: a)
|
|
350 |
next
|
|
351 |
case (Suc n)
|
|
352 |
hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
|
|
353 |
by (auto intro: mult_mono)
|
|
354 |
thus ?case
|
|
355 |
by (simp add: mult_assoc)
|
|
356 |
qed
|
|
357 |
}
|
|
358 |
note a = this
|
|
359 |
|
|
360 |
{
|
|
361 |
fix n have "a ^ n * x \<le> x"
|
|
362 |
proof (induct n)
|
|
363 |
case 0 show ?case by simp
|
|
364 |
next
|
|
365 |
case (Suc n) with a[of n]
|
|
366 |
show ?case by simp
|
|
367 |
qed
|
|
368 |
}
|
|
369 |
note b = this
|
|
370 |
|
|
371 |
show "star a * x \<le> x"
|
|
372 |
unfolding star_cont[of 1 a x, simplified]
|
|
373 |
by (rule SUP_leI) (rule b)
|
|
374 |
qed
|
|
375 |
|
|
376 |
show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
|
|
377 |
proof -
|
|
378 |
assume a: "x * a \<le> x"
|
|
379 |
|
|
380 |
{
|
|
381 |
fix n
|
|
382 |
have "x * a ^ (Suc n) \<le> x * a ^ n"
|
|
383 |
proof (induct n)
|
|
384 |
case 0 thus ?case by (simp add: a)
|
|
385 |
next
|
|
386 |
case (Suc n)
|
|
387 |
hence "(x * a ^ Suc n) * a \<le> (x * a ^ n) * a"
|
|
388 |
by (auto intro: mult_mono)
|
|
389 |
thus ?case
|
|
390 |
by (simp add: power_commutes mult_assoc)
|
|
391 |
qed
|
|
392 |
}
|
|
393 |
note a = this
|
|
394 |
|
|
395 |
{
|
|
396 |
fix n have "x * a ^ n \<le> x"
|
|
397 |
proof (induct n)
|
|
398 |
case 0 show ?case by simp
|
|
399 |
next
|
|
400 |
case (Suc n) with a[of n]
|
|
401 |
show ?case by simp
|
|
402 |
qed
|
|
403 |
}
|
|
404 |
note b = this
|
|
405 |
|
|
406 |
show "x * star a \<le> x"
|
|
407 |
unfolding star_cont[of x a 1, simplified]
|
|
408 |
by (rule SUP_leI) (rule b)
|
|
409 |
qed
|
|
410 |
qed
|
|
411 |
|
|
412 |
end
|
|
413 |
|
|
414 |
|
|
415 |
subsection {* Transitive Closure *}
|
|
416 |
|
|
417 |
context kleene
|
|
418 |
begin
|
|
419 |
|
|
420 |
definition
|
|
421 |
tcl_def: "tcl x = star x * x"
|
|
422 |
|
|
423 |
lemma tcl_zero: "tcl 0 = 0"
|
|
424 |
unfolding tcl_def by simp
|
|
425 |
|
|
426 |
lemma tcl_unfold_right: "tcl a = a + tcl a * a"
|
|
427 |
proof -
|
|
428 |
from star_unfold_right[of a]
|
|
429 |
have "a * (1 + star a * a) = a * star a" by simp
|
|
430 |
from this[simplified right_distrib, simplified]
|
|
431 |
show ?thesis
|
|
432 |
by (simp add:tcl_def mult_assoc)
|
|
433 |
qed
|
|
434 |
|
|
435 |
lemma less_tcl: "a \<le> tcl a"
|
|
436 |
proof -
|
|
437 |
have "a \<le> a + tcl a * a" by simp
|
|
438 |
also have "\<dots> = tcl a" by (rule tcl_unfold_right[symmetric])
|
|
439 |
finally show ?thesis .
|
|
440 |
qed
|
|
441 |
|
|
442 |
end
|
|
443 |
|
|
444 |
|
|
445 |
subsection {* Naive Algorithm to generate the transitive closure *}
|
|
446 |
|
|
447 |
function (default "\<lambda>x. 0", tailrec, domintros)
|
|
448 |
mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
449 |
where
|
|
450 |
"mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
|
|
451 |
by pat_completeness simp
|
|
452 |
|
|
453 |
declare mk_tcl.simps[simp del] (* loops *)
|
|
454 |
|
|
455 |
lemma mk_tcl_code[code]:
|
|
456 |
"mk_tcl A X =
|
|
457 |
(let XA = X * A
|
|
458 |
in if XA \<le> X then X else mk_tcl A (X + XA))"
|
|
459 |
unfolding mk_tcl.simps[of A X] Let_def ..
|
|
460 |
|
|
461 |
context kleene
|
|
462 |
begin
|
|
463 |
|
|
464 |
lemma mk_tcl_lemma1:
|
|
465 |
"(X + X * A) * star A = X * star A"
|
|
466 |
proof -
|
|
467 |
have "A * star A \<le> 1 + A * star A" by simp
|
|
468 |
also have "\<dots> = star A" by (simp add:star_unfold_left)
|
|
469 |
finally have "star A + A * star A = star A" by simp
|
|
470 |
hence "X * (star A + A * star A) = X * star A" by simp
|
|
471 |
thus ?thesis by (simp add:left_distrib right_distrib mult_assoc)
|
|
472 |
qed
|
|
473 |
|
|
474 |
lemma mk_tcl_lemma2:
|
|
475 |
shows "X * A \<le> X \<Longrightarrow> X * star A = X"
|
|
476 |
by (rule antisym) (auto simp:star4)
|
|
477 |
|
|
478 |
end
|
|
479 |
|
|
480 |
lemma mk_tcl_correctness:
|
|
481 |
fixes X :: "'a::kleene"
|
|
482 |
assumes "mk_tcl_dom (A, X)"
|
|
483 |
shows "mk_tcl A X = X * star A"
|
|
484 |
using assms
|
|
485 |
by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2)
|
|
486 |
|
|
487 |
|
|
488 |
lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
|
|
489 |
by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
|
|
490 |
|
|
491 |
lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
|
|
492 |
unfolding mk_tcl_def
|
|
493 |
by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
|
|
494 |
|
|
495 |
|
|
496 |
text {* We can replace the dom-Condition of the correctness theorem
|
|
497 |
with something executable *}
|
|
498 |
|
|
499 |
lemma mk_tcl_correctness2:
|
|
500 |
fixes A X :: "'a :: {kleene}"
|
|
501 |
assumes "mk_tcl A A \<noteq> 0"
|
|
502 |
shows "mk_tcl A A = tcl A"
|
|
503 |
using assms mk_tcl_default mk_tcl_correctness
|
|
504 |
unfolding tcl_def
|
|
505 |
by auto
|
|
506 |
|
|
507 |
end
|