equal
deleted
inserted
replaced
1 (* |
|
2 Conversion of automata into regular sets. |
|
3 use_thy"Auto"; |
|
4 *) |
|
5 |
|
6 Regset_of_auto = List + |
|
7 |
|
8 (* autos *) |
|
9 |
|
10 types 'a auto = "'a => nat => nat" |
|
11 |
|
12 consts deltas :: 'a auto => 'a list => nat => nat |
|
13 primrec deltas list |
|
14 "deltas A [] i = i" |
|
15 "deltas A (x#xs) i = deltas A xs (A x i)" |
|
16 |
|
17 consts trace :: 'a auto => nat => 'a list => nat list |
|
18 primrec trace list |
|
19 "trace A i [] = []" |
|
20 "trace A i (x#xs) = A x i # trace A (A x i) xs" |
|
21 |
|
22 (* regular sets *) |
|
23 |
|
24 constdefs conc :: 'a list set => 'a list set => 'a list set |
|
25 "conc A B == {xs@ys | xs ys. xs:A & ys:B}" |
|
26 |
|
27 consts star :: 'a list set => 'a list set |
|
28 inductive "star A" |
|
29 intrs |
|
30 NilI "[] : star A" |
|
31 ConsI "[| a:A; as : star A |] ==> a@as : star A" |
|
32 |
|
33 (* conversion a la Warshall *) |
|
34 |
|
35 consts regset_of :: 'a auto => nat => nat => nat => 'a list set |
|
36 primrec regset_of nat |
|
37 "regset_of A i j 0 = (if i=j then insert [] {[a] | a. A a i = j} |
|
38 else {[a] | a. A a i = j})" |
|
39 "regset_of A i j (Suc k) = regset_of A i j k Un |
|
40 conc (regset_of A i k k) |
|
41 (conc (star(regset_of A k k k)) |
|
42 (regset_of A k j k))" |
|
43 |
|
44 end |
|