author | Chengsong |
Mon, 10 Jul 2023 01:33:45 +0100 | |
changeset 660 | eddc4eaba7c4 |
parent 436 | 222333d2bdc2 |
permissions | -rw-r--r-- |
365 | 1 |
|
2 |
theory PDerivs |
|
3 |
imports Spec |
|
4 |
begin |
|
5 |
||
6 |
||
7 |
||
8 |
abbreviation |
|
9 |
"SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})" |
|
10 |
||
11 |
lemma SEQs_eq_image: |
|
12 |
"SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs" |
|
13 |
by auto |
|
14 |
||
405
3cfea5bb5e23
updated some of the text and cardinality proof
Christian Urban <christian.urban@kcl.ac.uk>
parents:
389
diff
changeset
|
15 |
fun |
365 | 16 |
pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set" |
17 |
where |
|
18 |
"pder c ZERO = {}" |
|
19 |
| "pder c ONE = {}" |
|
378 | 20 |
| "pder c (CH d) = (if c = d then {ONE} else {})" |
365 | 21 |
| "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)" |
22 |
| "pder c (SEQ r1 r2) = |
|
23 |
(if nullable r1 then SEQs (pder c r1) r2 \<union> pder c r2 else SEQs (pder c r1) r2)" |
|
24 |
| "pder c (STAR r) = SEQs (pder c r) (STAR r)" |
|
25 |
||
405
3cfea5bb5e23
updated some of the text and cardinality proof
Christian Urban <christian.urban@kcl.ac.uk>
parents:
389
diff
changeset
|
26 |
fun |
365 | 27 |
pders :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set" |
28 |
where |
|
29 |
"pders [] r = {r}" |
|
30 |
| "pders (c # s) r = \<Union> (pders s ` pder c r)" |
|
31 |
||
32 |
abbreviation |
|
33 |
pder_set :: "char \<Rightarrow> rexp set \<Rightarrow> rexp set" |
|
34 |
where |
|
35 |
"pder_set c rs \<equiv> \<Union> (pder c ` rs)" |
|
36 |
||
37 |
abbreviation |
|
38 |
pders_set :: "char list \<Rightarrow> rexp set \<Rightarrow> rexp set" |
|
39 |
where |
|
40 |
"pders_set s rs \<equiv> \<Union> (pders s ` rs)" |
|
41 |
||
42 |
lemma pders_append: |
|
43 |
"pders (s1 @ s2) r = \<Union> (pders s2 ` pders s1 r)" |
|
44 |
by (induct s1 arbitrary: r) (simp_all) |
|
45 |
||
46 |
lemma pders_snoc: |
|
47 |
shows "pders (s @ [c]) r = pder_set c (pders s r)" |
|
48 |
by (simp add: pders_append) |
|
49 |
||
50 |
lemma pders_simps [simp]: |
|
51 |
shows "pders s ZERO = (if s = [] then {ZERO} else {})" |
|
52 |
and "pders s ONE = (if s = [] then {ONE} else {})" |
|
53 |
and "pders s (ALT r1 r2) = (if s = [] then {ALT r1 r2} else (pders s r1) \<union> (pders s r2))" |
|
54 |
by (induct s) (simp_all) |
|
55 |
||
56 |
lemma pders_CHAR: |
|
378 | 57 |
shows "pders s (CH c) \<subseteq> {CH c, ONE}" |
365 | 58 |
by (induct s) (simp_all) |
59 |
||
60 |
subsection \<open>Relating left-quotients and partial derivatives\<close> |
|
61 |
||
62 |
lemma Sequ_UNION_distrib: |
|
63 |
shows "A ;; \<Union>(M ` I) = \<Union>((\<lambda>i. A ;; M i) ` I)" |
|
64 |
and "\<Union>(M ` I) ;; A = \<Union>((\<lambda>i. M i ;; A) ` I)" |
|
65 |
by (auto simp add: Sequ_def) |
|
66 |
||
67 |
||
68 |
lemma Der_pder: |
|
69 |
shows "Der c (L r) = \<Union> (L ` pder c r)" |
|
70 |
by (induct r) (simp_all add: nullable_correctness Sequ_UNION_distrib) |
|
71 |
||
72 |
lemma Ders_pders: |
|
73 |
shows "Ders s (L r) = \<Union> (L ` pders s r)" |
|
74 |
proof (induct s arbitrary: r) |
|
75 |
case (Cons c s) |
|
76 |
have ih: "\<And>r. Ders s (L r) = \<Union> (L ` pders s r)" by fact |
|
77 |
have "Ders (c # s) (L r) = Ders s (Der c (L r))" by (simp add: Ders_def Der_def) |
|
78 |
also have "\<dots> = Ders s (\<Union> (L ` pder c r))" by (simp add: Der_pder) |
|
79 |
also have "\<dots> = (\<Union>A\<in>(L ` (pder c r)). (Ders s A))" |
|
80 |
by (auto simp add: Ders_def) |
|
81 |
also have "\<dots> = \<Union> (L ` (pders_set s (pder c r)))" |
|
82 |
using ih by auto |
|
83 |
also have "\<dots> = \<Union> (L ` (pders (c # s) r))" by simp |
|
84 |
finally show "Ders (c # s) (L r) = \<Union> (L ` pders (c # s) r)" . |
|
85 |
qed (simp add: Ders_def) |
|
86 |
||
87 |
subsection \<open>Relating derivatives and partial derivatives\<close> |
|
88 |
||
89 |
lemma der_pder: |
|
90 |
shows "\<Union> (L ` (pder c r)) = L (der c r)" |
|
91 |
unfolding der_correctness Der_pder by simp |
|
92 |
||
93 |
lemma ders_pders: |
|
94 |
shows "\<Union> (L ` (pders s r)) = L (ders s r)" |
|
95 |
unfolding der_correctness ders_correctness Ders_pders by simp |
|
96 |
||
97 |
||
98 |
subsection \<open>Finiteness property of partial derivatives\<close> |
|
99 |
||
100 |
definition |
|
101 |
pders_Set :: "string set \<Rightarrow> rexp \<Rightarrow> rexp set" |
|
102 |
where |
|
103 |
"pders_Set A r \<equiv> \<Union>x \<in> A. pders x r" |
|
104 |
||
105 |
lemma pders_Set_subsetI: |
|
106 |
assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C" |
|
107 |
shows "pders_Set A r \<subseteq> C" |
|
108 |
using assms unfolding pders_Set_def by (rule UN_least) |
|
109 |
||
110 |
lemma pders_Set_union: |
|
111 |
shows "pders_Set (A \<union> B) r = (pders_Set A r \<union> pders_Set B r)" |
|
112 |
by (simp add: pders_Set_def) |
|
113 |
||
114 |
lemma pders_Set_subset: |
|
115 |
shows "A \<subseteq> B \<Longrightarrow> pders_Set A r \<subseteq> pders_Set B r" |
|
116 |
by (auto simp add: pders_Set_def) |
|
117 |
||
118 |
definition |
|
119 |
"UNIV1 \<equiv> UNIV - {[]}" |
|
120 |
||
121 |
lemma pders_Set_ZERO [simp]: |
|
122 |
shows "pders_Set UNIV1 ZERO = {}" |
|
123 |
unfolding UNIV1_def pders_Set_def by auto |
|
124 |
||
125 |
lemma pders_Set_ONE [simp]: |
|
126 |
shows "pders_Set UNIV1 ONE = {}" |
|
127 |
unfolding UNIV1_def pders_Set_def by (auto split: if_splits) |
|
128 |
||
129 |
lemma pders_Set_CHAR [simp]: |
|
378 | 130 |
shows "pders_Set UNIV1 (CH c) = {ONE}" |
365 | 131 |
unfolding UNIV1_def pders_Set_def |
132 |
apply(auto) |
|
133 |
apply(frule rev_subsetD) |
|
134 |
apply(rule pders_CHAR) |
|
135 |
apply(simp) |
|
136 |
apply(case_tac xa) |
|
137 |
apply(auto split: if_splits) |
|
138 |
done |
|
139 |
||
140 |
lemma pders_Set_ALT [simp]: |
|
141 |
shows "pders_Set UNIV1 (ALT r1 r2) = pders_Set UNIV1 r1 \<union> pders_Set UNIV1 r2" |
|
142 |
unfolding UNIV1_def pders_Set_def by auto |
|
143 |
||
144 |
||
145 |
text \<open>Non-empty suffixes of a string (needed for the cases of @{const SEQ} and @{const STAR} below)\<close> |
|
146 |
||
147 |
definition |
|
148 |
"PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
|
149 |
||
150 |
lemma PSuf_snoc: |
|
151 |
shows "PSuf (s @ [c]) = (PSuf s) ;; {[c]} \<union> {[c]}" |
|
152 |
unfolding PSuf_def Sequ_def |
|
153 |
by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) |
|
154 |
||
155 |
lemma PSuf_Union: |
|
156 |
shows "(\<Union>v \<in> PSuf s ;; {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))" |
|
157 |
by (auto simp add: Sequ_def) |
|
158 |
||
159 |
lemma pders_Set_snoc: |
|
160 |
shows "pders_Set (PSuf s ;; {[c]}) r = (pder_set c (pders_Set (PSuf s) r))" |
|
161 |
unfolding pders_Set_def |
|
162 |
by (simp add: PSuf_Union pders_snoc) |
|
163 |
||
164 |
lemma pders_SEQ: |
|
165 |
shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" |
|
166 |
proof (induct s rule: rev_induct) |
|
167 |
case (snoc c s) |
|
168 |
have ih: "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" |
|
169 |
by fact |
|
170 |
have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" |
|
171 |
by (simp add: pders_snoc) |
|
172 |
also have "\<dots> \<subseteq> pder_set c (SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2))" |
|
173 |
using ih by fastforce |
|
174 |
also have "\<dots> = pder_set c (SEQs (pders s r1) r2) \<union> pder_set c (pders_Set (PSuf s) r2)" |
|
175 |
by (simp) |
|
176 |
also have "\<dots> = pder_set c (SEQs (pders s r1) r2) \<union> pders_Set (PSuf s ;; {[c]}) r2" |
|
177 |
by (simp add: pders_Set_snoc) |
|
178 |
also |
|
179 |
have "\<dots> \<subseteq> pder_set c (SEQs (pders s r1) r2) \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2" |
|
180 |
by auto |
|
181 |
also |
|
182 |
have "\<dots> \<subseteq> SEQs (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2" |
|
183 |
by (auto simp add: if_splits) |
|
184 |
also have "\<dots> = SEQs (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2" |
|
185 |
by (simp add: pders_snoc) |
|
186 |
also have "\<dots> \<subseteq> SEQs (pders (s @ [c]) r1) r2 \<union> pders_Set (PSuf (s @ [c])) r2" |
|
187 |
unfolding pders_Set_def by (auto simp add: PSuf_snoc) |
|
188 |
finally show ?case . |
|
189 |
qed (simp) |
|
190 |
||
191 |
lemma pders_Set_SEQ_aux1: |
|
192 |
assumes a: "s \<in> UNIV1" |
|
193 |
shows "pders_Set (PSuf s) r \<subseteq> pders_Set UNIV1 r" |
|
194 |
using a unfolding UNIV1_def PSuf_def pders_Set_def by auto |
|
195 |
||
196 |
lemma pders_Set_SEQ_aux2: |
|
197 |
assumes a: "s \<in> UNIV1" |
|
198 |
shows "SEQs (pders s r1) r2 \<subseteq> SEQs (pders_Set UNIV1 r1) r2" |
|
199 |
using a unfolding pders_Set_def by auto |
|
200 |
||
201 |
lemma pders_Set_SEQ: |
|
202 |
shows "pders_Set UNIV1 (SEQ r1 r2) \<subseteq> SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2" |
|
203 |
apply(rule pders_Set_subsetI) |
|
204 |
apply(rule subset_trans) |
|
205 |
apply(rule pders_SEQ) |
|
206 |
using pders_Set_SEQ_aux1 pders_Set_SEQ_aux2 |
|
207 |
apply auto |
|
208 |
apply blast |
|
209 |
done |
|
210 |
||
211 |
lemma pders_STAR: |
|
212 |
assumes a: "s \<noteq> []" |
|
213 |
shows "pders s (STAR r) \<subseteq> SEQs (pders_Set (PSuf s) r) (STAR r)" |
|
214 |
using a |
|
215 |
proof (induct s rule: rev_induct) |
|
216 |
case (snoc c s) |
|
217 |
have ih: "s \<noteq> [] \<Longrightarrow> pders s (STAR r) \<subseteq> SEQs (pders_Set (PSuf s) r) (STAR r)" by fact |
|
218 |
{ assume asm: "s \<noteq> []" |
|
219 |
have "pders (s @ [c]) (STAR r) = pder_set c (pders s (STAR r))" by (simp add: pders_snoc) |
|
220 |
also have "\<dots> \<subseteq> pder_set c (SEQs (pders_Set (PSuf s) r) (STAR r))" |
|
221 |
using ih[OF asm] by fast |
|
222 |
also have "\<dots> \<subseteq> SEQs (pder_set c (pders_Set (PSuf s) r)) (STAR r) \<union> pder c (STAR r)" |
|
223 |
by (auto split: if_splits) |
|
224 |
also have "\<dots> \<subseteq> SEQs (pders_Set (PSuf (s @ [c])) r) (STAR r) \<union> (SEQs (pder c r) (STAR r))" |
|
225 |
by (simp only: PSuf_snoc pders_Set_snoc pders_Set_union) |
|
226 |
(auto simp add: pders_Set_def) |
|
227 |
also have "\<dots> = SEQs (pders_Set (PSuf (s @ [c])) r) (STAR r)" |
|
228 |
by (auto simp add: PSuf_snoc PSuf_Union pders_snoc pders_Set_def) |
|
229 |
finally have ?case . |
|
230 |
} |
|
231 |
moreover |
|
232 |
{ assume asm: "s = []" |
|
233 |
then have ?case by (auto simp add: pders_Set_def pders_snoc PSuf_def) |
|
234 |
} |
|
235 |
ultimately show ?case by blast |
|
236 |
qed (simp) |
|
237 |
||
238 |
lemma pders_Set_STAR: |
|
239 |
shows "pders_Set UNIV1 (STAR r) \<subseteq> SEQs (pders_Set UNIV1 r) (STAR r)" |
|
240 |
apply(rule pders_Set_subsetI) |
|
241 |
apply(rule subset_trans) |
|
242 |
apply(rule pders_STAR) |
|
243 |
apply(simp add: UNIV1_def) |
|
244 |
apply(simp add: UNIV1_def PSuf_def) |
|
245 |
apply(auto simp add: pders_Set_def) |
|
246 |
done |
|
247 |
||
248 |
lemma finite_SEQs [simp]: |
|
249 |
assumes a: "finite A" |
|
250 |
shows "finite (SEQs A r)" |
|
251 |
using a by auto |
|
252 |
||
253 |
thm finite.intros |
|
254 |
||
255 |
lemma finite_pders_Set_UNIV1: |
|
256 |
shows "finite (pders_Set UNIV1 r)" |
|
257 |
apply(induct r) |
|
258 |
apply(simp_all add: |
|
259 |
finite_subset[OF pders_Set_SEQ] |
|
260 |
finite_subset[OF pders_Set_STAR]) |
|
261 |
done |
|
262 |
||
263 |
lemma pders_Set_UNIV: |
|
264 |
shows "pders_Set UNIV r = pders [] r \<union> pders_Set UNIV1 r" |
|
265 |
unfolding UNIV1_def pders_Set_def |
|
266 |
by blast |
|
267 |
||
268 |
lemma finite_pders_Set_UNIV: |
|
269 |
shows "finite (pders_Set UNIV r)" |
|
270 |
unfolding pders_Set_UNIV |
|
271 |
by (simp add: finite_pders_Set_UNIV1) |
|
272 |
||
273 |
lemma finite_pders_set: |
|
274 |
shows "finite (pders_Set A r)" |
|
275 |
by (metis finite_pders_Set_UNIV pders_Set_subset rev_finite_subset subset_UNIV) |
|
276 |
||
277 |
||
278 |
text \<open>The following relationship between the alphabetic width of regular expressions |
|
279 |
(called \<open>awidth\<close> below) and the number of partial derivatives was proved |
|
280 |
by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close> |
|
281 |
||
282 |
fun awidth :: "rexp \<Rightarrow> nat" where |
|
283 |
"awidth ZERO = 0" | |
|
284 |
"awidth ONE = 0" | |
|
378 | 285 |
"awidth (CH a) = 1" | |
365 | 286 |
"awidth (ALT r1 r2) = awidth r1 + awidth r2" | |
287 |
"awidth (SEQ r1 r2) = awidth r1 + awidth r2" | |
|
288 |
"awidth (STAR r1) = awidth r1" |
|
289 |
||
290 |
lemma card_SEQs_pders_Set_le: |
|
291 |
shows "card (SEQs (pders_Set A r) s) \<le> card (pders_Set A r)" |
|
292 |
using finite_pders_set |
|
293 |
unfolding SEQs_eq_image |
|
294 |
by (rule card_image_le) |
|
295 |
||
296 |
lemma card_pders_set_UNIV1_le_awidth: |
|
297 |
shows "card (pders_Set UNIV1 r) \<le> awidth r" |
|
298 |
proof (induction r) |
|
299 |
case (ALT r1 r2) |
|
300 |
have "card (pders_Set UNIV1 (ALT r1 r2)) = card (pders_Set UNIV1 r1 \<union> pders_Set UNIV1 r2)" by simp |
|
301 |
also have "\<dots> \<le> card (pders_Set UNIV1 r1) + card (pders_Set UNIV1 r2)" |
|
302 |
by(simp add: card_Un_le) |
|
303 |
also have "\<dots> \<le> awidth (ALT r1 r2)" using ALT.IH by simp |
|
304 |
finally show ?case . |
|
305 |
next |
|
306 |
case (SEQ r1 r2) |
|
307 |
have "card (pders_Set UNIV1 (SEQ r1 r2)) \<le> card (SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2)" |
|
308 |
by (simp add: card_mono finite_pders_set pders_Set_SEQ) |
|
309 |
also have "\<dots> \<le> card (SEQs (pders_Set UNIV1 r1) r2) + card (pders_Set UNIV1 r2)" |
|
310 |
by (simp add: card_Un_le) |
|
311 |
also have "\<dots> \<le> card (pders_Set UNIV1 r1) + card (pders_Set UNIV1 r2)" |
|
312 |
by (simp add: card_SEQs_pders_Set_le) |
|
313 |
also have "\<dots> \<le> awidth (SEQ r1 r2)" using SEQ.IH by simp |
|
314 |
finally show ?case . |
|
315 |
next |
|
316 |
case (STAR r) |
|
317 |
have "card (pders_Set UNIV1 (STAR r)) \<le> card (SEQs (pders_Set UNIV1 r) (STAR r))" |
|
318 |
by (simp add: card_mono finite_pders_set pders_Set_STAR) |
|
319 |
also have "\<dots> \<le> card (pders_Set UNIV1 r)" by (rule card_SEQs_pders_Set_le) |
|
320 |
also have "\<dots> \<le> awidth (STAR r)" by (simp add: STAR.IH) |
|
321 |
finally show ?case . |
|
322 |
qed (auto) |
|
323 |
||
324 |
text\<open>Antimirov's Theorem 3.4:\<close> |
|
325 |
||
326 |
theorem card_pders_set_UNIV_le_awidth: |
|
327 |
shows "card (pders_Set UNIV r) \<le> awidth r + 1" |
|
328 |
proof - |
|
329 |
have "card (insert r (pders_Set UNIV1 r)) \<le> Suc (card (pders_Set UNIV1 r))" |
|
330 |
by(auto simp: card_insert_if[OF finite_pders_Set_UNIV1]) |
|
331 |
also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pders_set_UNIV1_le_awidth) |
|
332 |
finally show ?thesis by(simp add: pders_Set_UNIV) |
|
333 |
qed |
|
334 |
||
335 |
text\<open>Antimirov's Corollary 3.5:\<close> |
|
387 | 336 |
(*W stands for word set*) |
365 | 337 |
corollary card_pders_set_le_awidth: |
387 | 338 |
shows "card (pders_Set W r) \<le> awidth r + 1" |
365 | 339 |
proof - |
387 | 340 |
have "card (pders_Set W r) \<le> card (pders_Set UNIV r)" |
365 | 341 |
by (simp add: card_mono finite_pders_set pders_Set_subset) |
342 |
also have "... \<le> awidth r + 1" |
|
343 |
by (rule card_pders_set_UNIV_le_awidth) |
|
387 | 344 |
finally show "card (pders_Set W r) \<le> awidth r + 1" by simp |
365 | 345 |
qed |
346 |
||
347 |
(* other result by antimirov *) |
|
348 |
||
349 |
lemma card_pders_awidth: |
|
350 |
shows "card (pders s r) \<le> awidth r + 1" |
|
351 |
proof - |
|
352 |
have "pders s r \<subseteq> pders_Set UNIV r" |
|
353 |
using pders_Set_def by auto |
|
354 |
then have "card (pders s r) \<le> card (pders_Set UNIV r)" |
|
355 |
by (simp add: card_mono finite_pders_set) |
|
356 |
then show "card (pders s r) \<le> awidth r + 1" |
|
357 |
using card_pders_set_le_awidth order_trans by blast |
|
358 |
qed |
|
359 |
||
360 |
||
361 |
||
362 |
||
363 |
||
364 |
fun subs :: "rexp \<Rightarrow> rexp set" where |
|
365 |
"subs ZERO = {ZERO}" | |
|
366 |
"subs ONE = {ONE}" | |
|
378 | 367 |
"subs (CH a) = {CH a, ONE}" | |
365 | 368 |
"subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" | |
369 |
"subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union> SEQs (subs r1) r2)" | |
|
370 |
"subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))" |
|
371 |
||
372 |
lemma subs_finite: |
|
373 |
shows "finite (subs r)" |
|
374 |
apply(induct r) |
|
375 |
apply(simp_all) |
|
376 |
done |
|
377 |
||
378 |
||
379 |
||
380 |
lemma pders_subs: |
|
381 |
shows "pders s r \<subseteq> subs r" |
|
382 |
apply(induct r arbitrary: s) |
|
383 |
apply(simp) |
|
384 |
apply(simp) |
|
385 |
apply(simp add: pders_CHAR) |
|
386 |
(* SEQ case *) |
|
387 |
apply(simp) |
|
388 |
apply(rule subset_trans) |
|
389 |
apply(rule pders_SEQ) |
|
390 |
defer |
|
391 |
(* ALT case *) |
|
392 |
apply(simp) |
|
393 |
apply(rule impI) |
|
394 |
apply(rule conjI) |
|
395 |
apply blast |
|
396 |
apply blast |
|
397 |
(* STAR case *) |
|
398 |
apply(case_tac s) |
|
399 |
apply(simp) |
|
400 |
apply(rule subset_trans) |
|
401 |
thm pders_STAR |
|
402 |
apply(rule pders_STAR) |
|
436 | 403 |
apply(simp) |
404 |
apply(auto simp add: pders_Set_def)[1] |
|
405 |
(* rest of SEQ case *) |
|
365 | 406 |
apply(simp) |
407 |
apply(rule conjI) |
|
408 |
apply blast |
|
409 |
apply(auto simp add: pders_Set_def)[1] |
|
410 |
done |
|
411 |
||
412 |
fun size2 :: "rexp \<Rightarrow> nat" where |
|
413 |
"size2 ZERO = 1" | |
|
414 |
"size2 ONE = 1" | |
|
378 | 415 |
"size2 (CH c) = 1" | |
365 | 416 |
"size2 (ALT r1 r2) = Suc (size2 r1 + size2 r2)" | |
417 |
"size2 (SEQ r1 r2) = Suc (size2 r1 + size2 r2)" | |
|
418 |
"size2 (STAR r1) = Suc (size2 r1)" |
|
419 |
||
420 |
||
421 |
lemma size_rexp: |
|
422 |
fixes r :: rexp |
|
423 |
shows "1 \<le> size2 r" |
|
424 |
apply(induct r) |
|
425 |
apply(simp) |
|
426 |
apply(simp_all) |
|
427 |
done |
|
428 |
||
378 | 429 |
(* |
365 | 430 |
lemma subs_card: |
431 |
shows "card (subs r) \<le> Suc (size2 r + size2 r)" |
|
432 |
apply(induct r) |
|
433 |
apply(auto) |
|
434 |
apply(subst card_insert) |
|
435 |
apply(simp add: subs_finite) |
|
436 |
apply(simp add: subs_finite) |
|
437 |
oops |
|
378 | 438 |
*) |
365 | 439 |
|
440 |
lemma subs_size2: |
|
441 |
shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)" |
|
442 |
apply(induct r) |
|
443 |
apply(simp) |
|
444 |
apply(simp) |
|
445 |
apply(simp) |
|
446 |
(* SEQ case *) |
|
447 |
apply(simp) |
|
448 |
apply(auto)[1] |
|
449 |
apply (smt Suc_n_not_le_n add.commute distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
|
450 |
apply (smt Suc_le_mono Suc_n_not_le_n le_trans nat_le_linear power2_eq_square power2_sum semiring_normalization_rules(23) trans_le_add2) |
|
451 |
apply (smt Groups.add_ac(3) Suc_n_not_le_n distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
|
452 |
(* ALT case *) |
|
453 |
apply(simp) |
|
454 |
apply(auto)[1] |
|
455 |
apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n le_add2 linear order_trans power2_eq_square power2_sum) |
|
456 |
apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n left_add_mult_distrib linear mult.commute order.trans trans_le_add1) |
|
457 |
(* STAR case *) |
|
458 |
apply(auto)[1] |
|
459 |
apply(drule_tac x="r'" in bspec) |
|
460 |
apply(simp) |
|
461 |
apply(rule le_trans) |
|
462 |
apply(assumption) |
|
463 |
apply(simp) |
|
464 |
using size_rexp |
|
465 |
apply(simp) |
|
466 |
done |
|
467 |
||
468 |
lemma awidth_size: |
|
469 |
shows "awidth r \<le> size2 r" |
|
470 |
apply(induct r) |
|
471 |
apply(simp_all) |
|
472 |
done |
|
473 |
||
474 |
lemma Sum1: |
|
475 |
fixes A B :: "nat set" |
|
476 |
assumes "A \<subseteq> B" "finite A" "finite B" |
|
477 |
shows "\<Sum>A \<le> \<Sum>B" |
|
478 |
using assms |
|
479 |
by (simp add: sum_mono2) |
|
480 |
||
481 |
lemma Sum2: |
|
482 |
fixes A :: "rexp set" |
|
483 |
and f g :: "rexp \<Rightarrow> nat" |
|
484 |
assumes "finite A" "\<forall>x \<in> A. f x \<le> g x" |
|
485 |
shows "sum f A \<le> sum g A" |
|
486 |
using assms |
|
487 |
apply(induct A) |
|
488 |
apply(auto) |
|
489 |
done |
|
490 |
||
491 |
||
492 |
||
493 |
||
494 |
||
495 |
lemma pders_max_size: |
|
496 |
shows "(sum size2 (pders s r)) \<le> (Suc (size2 r)) ^ 3" |
|
497 |
proof - |
|
498 |
have "(sum size2 (pders s r)) \<le> sum (\<lambda>_. Suc (size2 r * size2 r)) (pders s r)" |
|
499 |
apply(rule_tac Sum2) |
|
500 |
apply (meson pders_subs rev_finite_subset subs_finite) |
|
501 |
using pders_subs subs_size2 by blast |
|
502 |
also have "... \<le> (Suc (size2 r * size2 r)) * (sum (\<lambda>_. 1) (pders s r))" |
|
503 |
by simp |
|
504 |
also have "... \<le> (Suc (size2 r * size2 r)) * card (pders s r)" |
|
505 |
by simp |
|
506 |
also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (awidth r))" |
|
507 |
using Suc_eq_plus1 card_pders_awidth mult_le_mono2 by presburger |
|
508 |
also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (size2 r))" |
|
509 |
using Suc_le_mono awidth_size mult_le_mono2 by presburger |
|
510 |
also have "... \<le> (Suc (size2 r)) ^ 3" |
|
511 |
by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp) |
|
512 |
finally show ?thesis . |
|
513 |
qed |
|
514 |
||
515 |
lemma pders_Set_max_size: |
|
516 |
shows "(sum size2 (pders_Set A r)) \<le> (Suc (size2 r)) ^ 3" |
|
517 |
proof - |
|
518 |
have "(sum size2 (pders_Set A r)) \<le> sum (\<lambda>_. Suc (size2 r * size2 r)) (pders_Set A r)" |
|
519 |
apply(rule_tac Sum2) |
|
520 |
apply (simp add: finite_pders_set) |
|
521 |
by (meson pders_Set_subsetI pders_subs subs_size2 subsetD) |
|
522 |
also have "... \<le> (Suc (size2 r * size2 r)) * (sum (\<lambda>_. 1) (pders_Set A r))" |
|
523 |
by simp |
|
524 |
also have "... \<le> (Suc (size2 r * size2 r)) * card (pders_Set A r)" |
|
525 |
by simp |
|
526 |
also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (awidth r))" |
|
527 |
using Suc_eq_plus1 card_pders_set_le_awidth mult_le_mono2 by presburger |
|
528 |
also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (size2 r))" |
|
529 |
using Suc_le_mono awidth_size mult_le_mono2 by presburger |
|
530 |
also have "... \<le> (Suc (size2 r)) ^ 3" |
|
531 |
by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp) |
|
532 |
finally show ?thesis . |
|
533 |
qed |
|
534 |
||
535 |
fun height :: "rexp \<Rightarrow> nat" where |
|
536 |
"height ZERO = 1" | |
|
537 |
"height ONE = 1" | |
|
378 | 538 |
"height (CH c) = 1" | |
365 | 539 |
"height (ALT r1 r2) = Suc (max (height r1) (height r2))" | |
540 |
"height (SEQ r1 r2) = Suc (max (height r1) (height r2))" | |
|
541 |
"height (STAR r1) = Suc (height r1)" |
|
542 |
||
543 |
lemma height_size2: |
|
544 |
shows "height r \<le> size2 r" |
|
545 |
apply(induct r) |
|
546 |
apply(simp_all) |
|
547 |
done |
|
548 |
||
549 |
lemma height_rexp: |
|
550 |
fixes r :: rexp |
|
551 |
shows "1 \<le> height r" |
|
552 |
apply(induct r) |
|
553 |
apply(simp_all) |
|
554 |
done |
|
555 |
||
556 |
lemma subs_height: |
|
557 |
shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)" |
|
558 |
apply(induct r) |
|
559 |
apply(auto)+ |
|
560 |
done |
|
378 | 561 |
|
562 |
fun lin_concat :: "(char \<times> rexp) \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp)" (infixl "[.]" 91) |
|
563 |
where |
|
564 |
"(c, ZERO) [.] t = (c, ZERO)" |
|
565 |
| "(c, ONE) [.] t = (c, t)" |
|
566 |
| "(c, p) [.] t = (c, SEQ p t)" |
|
567 |
||
568 |
||
569 |
fun circle_concat :: "(char \<times> rexp ) set \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp) set" ( infixl "\<circle>" 90) |
|
570 |
where |
|
571 |
"l \<circle> ZERO = {}" |
|
572 |
| "l \<circle> ONE = l" |
|
573 |
| "l \<circle> t = ( (\<lambda>p. p [.] t) ` l ) " |
|
574 |
||
575 |
||
576 |
||
577 |
fun linear_form :: "rexp \<Rightarrow>( char \<times> rexp ) set" |
|
578 |
where |
|
579 |
"linear_form ZERO = {}" |
|
580 |
| "linear_form ONE = {}" |
|
581 |
| "linear_form (CH c) = {(c, ONE)}" |
|
582 |
| "linear_form (ALT r1 r2) = (linear_form) r1 \<union> (linear_form r2)" |
|
583 |
| "linear_form (SEQ r1 r2) = (if (nullable r1) then (linear_form r1) \<circle> r2 \<union> linear_form r2 else (linear_form r1) \<circle> r2) " |
|
584 |
| "linear_form (STAR r ) = (linear_form r) \<circle> (STAR r)" |
|
585 |
||
586 |
||
587 |
value "linear_form (SEQ (STAR (CH x)) (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) )" |
|
588 |
||
589 |
||
590 |
value "linear_form (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) " |
|
591 |
||
592 |
fun pdero :: "char \<Rightarrow> rexp \<Rightarrow> rexp set" |
|
593 |
where |
|
594 |
"pdero c t = \<Union> ((\<lambda>(d, p). if d = c then {p} else {}) ` (linear_form t) )" |
|
595 |
||
596 |
fun pderso :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set" |
|
597 |
where |
|
598 |
"pderso [] r = {r}" |
|
599 |
| "pderso (c # s) r = \<Union> ( pderso s ` (pdero c r) )" |
|
600 |
||
601 |
lemma alternative_pder: |
|
602 |
shows "pderso s r = pders s r" |
|
603 |
sledgehammer |
|
604 |
oops |
|
605 |
||
387 | 606 |
lemma pdero_result: |
607 |
shows "pdero c (STAR (ALT (CH c) (SEQ (CH c) (CH c)))) = {SEQ (CH c)(STAR (ALT (CH c) (SEQ (CH c) (CH c)))),(STAR (ALT (CH c) (SEQ (CH c) (CH c))))}" |
|
608 |
apply(simp) |
|
609 |
by auto |
|
610 |
||
611 |
fun concatLen :: "rexp \<Rightarrow> nat" where |
|
612 |
"concatLen ZERO = 0" | |
|
613 |
"concatLen ONE = 0" | |
|
614 |
"concatLen (CH c) = 0" | |
|
615 |
"concatLen (SEQ v1 v2) = Suc (max (concatLen v1) (concatLen v2))" | |
|
616 |
" concatLen (ALT v1 v2) = max (concatLen v1) (concatLen v2)" | |
|
617 |
" concatLen (STAR v) = Suc (concatLen v)" |
|
618 |
||
388 | 619 |
text\<open>Antimirov's Theorem 3.8:\<close> |
620 |
lemma Maxsubterms38: |
|
621 |
shows "\<forall>pt \<in> (pders_Set UNIV t). pt \<in> (subs t) \<or> pt = ONE \<or> pt = (SEQ t0 t1)" |
|
389 | 622 |
oops |
623 |
||
388 | 624 |
|
387 | 625 |
|
378 | 626 |
|
627 |
export_code height pders subs pderso in Scala module_name Pders |
|
628 |
export_code pdero pderso in Scala module_name Pderso |
|
629 |
export_code pdero pderso in Scala module_name Pderso |
|
630 |
||
631 |
||
365 | 632 |
|
633 |
end |