13 |
13 |
14 regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as) |
14 regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as) |
15 else atoms d i j as |
15 else atoms d i j as |
16 *) |
16 *) |
17 |
17 |
18 RegSet_of_nat_DA = RegSet + DA + |
18 theory RegSet_of_nat_DA = RegSet + DA: |
19 |
19 |
20 types 'a nat_next = "'a => nat => nat" |
20 types 'a nat_next = "'a => nat => nat" |
21 |
21 |
22 syntax deltas :: 'a nat_next => 'a list => nat => nat |
22 syntax deltas :: "'a nat_next => 'a list => nat => nat" |
23 translations "deltas" == "foldl2" |
23 translations "deltas" == "foldl2" |
24 |
24 |
25 consts trace :: 'a nat_next => nat => 'a list => nat list |
25 consts trace :: "'a nat_next => nat => 'a list => nat list" |
26 primrec |
26 primrec |
27 "trace d i [] = []" |
27 "trace d i [] = []" |
28 "trace d i (x#xs) = d x i # trace d (d x i) xs" |
28 "trace d i (x#xs) = d x i # trace d (d x i) xs" |
29 |
29 |
30 (* conversion a la Warshall *) |
30 (* conversion a la Warshall *) |
31 |
31 |
32 consts regset :: 'a nat_next => nat => nat => nat => 'a list set |
32 consts regset :: "'a nat_next => nat => nat => nat => 'a list set" |
33 primrec |
33 primrec |
34 "regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j} |
34 "regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j} |
35 else {[a] | a. d a i = j})" |
35 else {[a] | a. d a i = j})" |
36 "regset d i j (Suc k) = regset d i j k Un |
36 "regset d i j (Suc k) = regset d i j k Un |
37 conc (regset d i k k) |
37 conc (regset d i k k) |
38 (conc (star(regset d k k k)) |
38 (conc (star(regset d k k k)) |
39 (regset d k j k))" |
39 (regset d k j k))" |
40 |
40 |
41 constdefs |
41 constdefs |
42 regset_of_DA :: ('a,nat)da => nat => 'a list set |
42 regset_of_DA :: "('a,nat)da => nat => 'a list set" |
43 "regset_of_DA A k == UN j:{j. j<k & fin A j}. regset (next A) (start A) j k" |
43 "regset_of_DA A k == UN j:{j. j<k & fin A j}. regset (next A) (start A) j k" |
44 |
44 |
45 bounded :: "'a => nat => bool" |
45 bounded :: "'a => nat => bool" |
46 "bounded d k == !n. n < k --> (!x. d x n < k)" |
46 "bounded d k == !n. n < k --> (!x. d x n < k)" |
47 |
47 |
|
48 declare |
|
49 in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp] |
|
50 |
|
51 (* Lists *) |
|
52 |
|
53 lemma butlast_empty[iff]: |
|
54 "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])" |
|
55 by (case_tac "xs") simp_all |
|
56 |
|
57 lemma in_set_butlast_concatI: |
|
58 "x:set(butlast xs) ==> xs:set xss ==> x:set(butlast(concat xss))" |
|
59 apply (induct "xss") |
|
60 apply simp |
|
61 apply (simp add: butlast_append del: ball_simps) |
|
62 apply (rule conjI) |
|
63 apply (clarify) |
|
64 apply (erule disjE) |
|
65 apply (blast) |
|
66 apply (subgoal_tac "xs=[]") |
|
67 apply simp |
|
68 apply (blast) |
|
69 apply (blast dest: in_set_butlastD) |
|
70 done |
|
71 |
|
72 (* Regular sets *) |
|
73 |
|
74 (* The main lemma: |
|
75 how to decompose a trace into a prefix, a list of loops and a suffix. |
|
76 *) |
|
77 lemma decompose[rule_format]: |
|
78 "!i. k : set(trace d i xs) --> (EX pref mids suf. |
|
79 xs = pref @ concat mids @ suf & |
|
80 deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) & |
|
81 (!mid:set mids. (deltas d mid k = k) & |
|
82 (!n:set(butlast(trace d k mid)). n ~= k)) & |
|
83 (!n:set(butlast(trace d k suf)). n ~= k))" |
|
84 apply (induct "xs") |
|
85 apply (simp) |
|
86 apply (rename_tac a as) |
|
87 apply (intro strip) |
|
88 apply (case_tac "d a i = k") |
|
89 apply (rule_tac x = "[a]" in exI) |
|
90 apply simp |
|
91 apply (case_tac "k : set(trace d (d a i) as)") |
|
92 apply (erule allE) |
|
93 apply (erule impE) |
|
94 apply (assumption) |
|
95 apply (erule exE)+ |
|
96 apply (rule_tac x = "pref#mids" in exI) |
|
97 apply (rule_tac x = "suf" in exI) |
|
98 apply simp |
|
99 apply (rule_tac x = "[]" in exI) |
|
100 apply (rule_tac x = "as" in exI) |
|
101 apply simp |
|
102 apply (blast dest: in_set_butlastD) |
|
103 apply simp |
|
104 apply (erule allE) |
|
105 apply (erule impE) |
|
106 apply (assumption) |
|
107 apply (erule exE)+ |
|
108 apply (rule_tac x = "a#pref" in exI) |
|
109 apply (rule_tac x = "mids" in exI) |
|
110 apply (rule_tac x = "suf" in exI) |
|
111 apply simp |
|
112 done |
|
113 |
|
114 lemma length_trace[simp]: "!!i. length(trace d i xs) = length xs" |
|
115 by (induct "xs") simp_all |
|
116 |
|
117 lemma deltas_append[simp]: |
|
118 "!!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)" |
|
119 by (induct "xs") simp_all |
|
120 |
|
121 lemma trace_append[simp]: |
|
122 "!!i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys" |
|
123 by (induct "xs") simp_all |
|
124 |
|
125 lemma trace_concat[simp]: |
|
126 "(!xs: set xss. deltas d xs i = i) ==> |
|
127 trace d i (concat xss) = concat (map (trace d i) xss)" |
|
128 by (induct "xss") simp_all |
|
129 |
|
130 lemma trace_is_Nil[simp]: "!!i. (trace d i xs = []) = (xs = [])" |
|
131 by (case_tac "xs") simp_all |
|
132 |
|
133 lemma trace_is_Cons_conv[simp]: |
|
134 "(trace d i xs = n#ns) = |
|
135 (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)" |
|
136 apply (case_tac "xs") |
|
137 apply simp_all |
|
138 apply (blast) |
|
139 done |
|
140 |
|
141 lemma set_trace_conv: |
|
142 "!!i. set(trace d i xs) = |
|
143 (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))" |
|
144 apply (induct "xs") |
|
145 apply (simp) |
|
146 apply (simp add: insert_commute) |
|
147 done |
|
148 |
|
149 lemma deltas_concat[simp]: |
|
150 "(!mid:set mids. deltas d mid k = k) ==> deltas d (concat mids) k = k" |
|
151 by (induct mids) simp_all |
|
152 |
|
153 lemma lem: "[| n < Suc k; n ~= k |] ==> n < k" |
|
154 by arith |
|
155 |
|
156 lemma regset_spec: |
|
157 "!!i j xs. xs : regset d i j k = |
|
158 ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)" |
|
159 apply (induct k) |
|
160 apply(simp split: list.split) |
|
161 apply(fastsimp) |
|
162 apply (simp add: conc_def) |
|
163 apply (rule iffI) |
|
164 apply (erule disjE) |
|
165 apply simp |
|
166 apply (erule exE conjE)+ |
|
167 apply simp |
|
168 apply (subgoal_tac |
|
169 "(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n") |
|
170 apply (simp add: set_trace_conv butlast_append ball_Un) |
|
171 apply (erule star.induct) |
|
172 apply (simp) |
|
173 apply (simp add: set_trace_conv butlast_append ball_Un) |
|
174 apply (case_tac "n : set(butlast(trace d i xs))") |
|
175 prefer 2 apply (rule disjI1) |
|
176 apply (blast intro:lem) |
|
177 apply (rule disjI2) |
|
178 apply (drule in_set_butlastD[THEN decompose]) |
|
179 apply (clarify) |
|
180 apply (rule_tac x = "pref" in exI) |
|
181 apply simp |
|
182 apply (rule conjI) |
|
183 apply (rule ballI) |
|
184 apply (rule lem) |
|
185 prefer 2 apply simp |
|
186 apply (drule bspec) prefer 2 apply assumption |
|
187 apply simp |
|
188 apply (rule_tac x = "concat mids" in exI) |
|
189 apply (simp) |
|
190 apply (rule conjI) |
|
191 apply (rule concat_in_star) |
|
192 apply simp |
|
193 apply (rule ballI) |
|
194 apply (rule ballI) |
|
195 apply (rule lem) |
|
196 prefer 2 apply simp |
|
197 apply (drule bspec) prefer 2 apply assumption |
|
198 apply (simp add: image_eqI in_set_butlast_concatI) |
|
199 apply (rule ballI) |
|
200 apply (rule lem) |
|
201 apply auto |
|
202 done |
|
203 |
|
204 lemma trace_below: |
|
205 "bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)" |
|
206 apply (unfold bounded_def) |
|
207 apply (induct "xs") |
|
208 apply simp |
|
209 apply (simp (no_asm)) |
|
210 apply (blast) |
|
211 done |
|
212 |
|
213 lemma regset_below: |
|
214 "[| bounded d k; i < k; j < k |] ==> |
|
215 regset d i j k = {xs. deltas d xs i = j}" |
|
216 apply (rule set_ext) |
|
217 apply (simp add: regset_spec) |
|
218 apply (blast dest: trace_below in_set_butlastD) |
|
219 done |
|
220 |
|
221 lemma deltas_below: |
|
222 "!!i. bounded d k ==> i < k ==> deltas d w i < k" |
|
223 apply (unfold bounded_def) |
|
224 apply (induct "w") |
|
225 apply simp_all |
|
226 done |
|
227 |
|
228 lemma regset_DA_equiv: |
|
229 "[| bounded (next A) k; start A < k; j < k |] ==> \ |
|
230 \ w : regset_of_DA A k = accepts A w" |
|
231 apply(unfold regset_of_DA_def) |
|
232 apply (simp cong: conj_cong |
|
233 add: regset_below deltas_below accepts_def delta_def) |
|
234 done |
|
235 |
48 end |
236 end |