30 |
30 |
31 |
31 |
32 ML {* @{term "op ^^"} *} |
32 ML {* @{term "op ^^"} *} |
33 |
33 |
34 notation (latex output) |
34 notation (latex output) |
35 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
35 str_eq ("\<approx>\<^bsub>_\<^esub>") and |
36 str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and |
36 str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and |
37 conc (infixr "\<cdot>" 100) and |
37 conc (infixr "\<cdot>" 100) and |
38 star ("_\<^bsup>\<star>\<^esup>") and |
38 star ("_\<^bsup>\<star>\<^esup>") and |
39 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
39 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
40 Suc ("_+1" [100] 100) and |
40 Suc ("_+1" [100] 100) and |
41 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and |
41 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and |
49 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
49 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
50 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
50 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
51 Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and |
51 Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and |
52 |
52 |
53 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and |
53 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and |
54 tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and |
54 tag_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and |
55 tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and |
55 tag_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and |
56 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and |
56 tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and |
57 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and |
57 tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and |
58 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and |
58 tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and |
59 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) |
59 tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) |
60 |
60 |
61 lemma meta_eq_app: |
61 lemma meta_eq_app: |
62 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x" |
62 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x" |
63 by auto |
63 by auto |
64 |
64 |
65 lemma conc_def': |
65 lemma conc_def': |
66 "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}" |
66 "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}" |
67 unfolding conc_def by simp |
67 unfolding conc_def by simp |
|
68 |
|
69 lemma str_eq_def': |
|
70 shows "x \<approx>A y \<equiv> (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)" |
|
71 unfolding str_eq_def by simp |
68 |
72 |
69 (* THEOREMS *) |
73 (* THEOREMS *) |
70 |
74 |
71 lemma conc_Union_left: |
75 lemma conc_Union_left: |
72 shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))" |
76 shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))" |
101 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
105 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
102 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
106 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
103 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
107 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
104 "_asm" :: "prop \<Rightarrow> asms" ("_") |
108 "_asm" :: "prop \<Rightarrow> asms" ("_") |
105 |
109 |
|
110 lemma pow_length: |
|
111 assumes a: "[] \<notin> A" |
|
112 and b: "s \<in> A \<up> Suc n" |
|
113 shows "n < length s" |
|
114 using b |
|
115 proof (induct n arbitrary: s) |
|
116 case 0 |
|
117 have "s \<in> A \<up> Suc 0" by fact |
|
118 with a have "s \<noteq> []" by auto |
|
119 then show "0 < length s" by auto |
|
120 next |
|
121 case (Suc n) |
|
122 have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact |
|
123 have "s \<in> A \<up> Suc (Suc n)" by fact |
|
124 then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n" |
|
125 by (auto simp add: Seq_def) |
|
126 from ih ** have "n < length s2" by simp |
|
127 moreover have "0 < length s1" using * a by auto |
|
128 ultimately show "Suc n < length s" unfolding eq |
|
129 by (simp only: length_append) |
|
130 qed |
106 |
131 |
107 (*>*) |
132 (*>*) |
108 |
133 |
109 |
134 |
110 section {* Introduction *} |
135 section {* Introduction *} |
314 is defined as the union over all powers, namely @{thm star_def}. In the paper |
339 is defined as the union over all powers, namely @{thm star_def}. In the paper |
315 we will make use of the following properties of these constructions. |
340 we will make use of the following properties of these constructions. |
316 |
341 |
317 \begin{proposition}\label{langprops}\mbox{}\\ |
342 \begin{proposition}\label{langprops}\mbox{}\\ |
318 \begin{tabular}{@ {}ll} |
343 \begin{tabular}{@ {}ll} |
319 (i) & @{thm star_cases} \\ |
344 (i) & @{thm star_unfold_left} \\ |
320 (ii) & @{thm[mode=IfThen] pow_length}\\ |
345 (ii) & @{thm[mode=IfThen] pow_length}\\ |
321 (iii) & @{thm conc_Union_left} \\ |
346 (iii) & @{thm conc_Union_left} \\ |
322 \end{tabular} |
347 \end{tabular} |
323 \end{proposition} |
348 \end{proposition} |
324 |
349 |
341 @{term "[] \<notin> A"}. However we will need the following `reverse' |
366 @{term "[] \<notin> A"}. However we will need the following `reverse' |
342 version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to |
367 version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to |
343 \mbox{@{term "X \<cdot> A"}}). |
368 \mbox{@{term "X \<cdot> A"}}). |
344 |
369 |
345 \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\ |
370 \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\ |
346 If @{thm (prem 1) arden} then |
371 If @{thm (prem 1) reversed_Arden} then |
347 @{thm (lhs) arden} if and only if |
372 @{thm (lhs) reversed_Arden} if and only if |
348 @{thm (rhs) arden}. |
373 @{thm (rhs) reversed_Arden}. |
349 \end{lemma} |
374 \end{lemma} |
350 |
375 |
351 \begin{proof} |
376 \begin{proof} |
352 For the right-to-left direction we assume @{thm (rhs) arden} and show |
377 For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show |
353 that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} |
378 that @{thm (lhs) reversed_Arden} holds. From Prop.~\ref{langprops}@{text "(i)"} |
354 we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"}, |
379 we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"}, |
355 which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both |
380 which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both |
356 sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side |
381 sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side |
357 is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction. |
382 is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction. |
358 |
383 |
359 For the other direction we assume @{thm (lhs) arden}. By a simple induction |
384 For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction |
360 on @{text n}, we can establish the property |
385 on @{text n}, we can establish the property |
361 |
386 |
362 \begin{center} |
387 \begin{center} |
363 @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper} |
388 @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper} |
364 \end{center} |
389 \end{center} |
365 |
390 |
366 \noindent |
391 \noindent |
367 Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for |
392 Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for |
368 all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition |
393 all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition |
369 of @{text "\<star>"}. |
394 of @{text "\<star>"}. |
370 For the inclusion in the other direction we assume a string @{text s} |
395 For the inclusion in the other direction we assume a string @{text s} |
371 with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden} |
396 with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden} |
372 we know by Prop.~\ref{langprops}@{text "(ii)"} that |
397 we know by Prop.~\ref{langprops}@{text "(ii)"} that |
373 @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k} |
398 @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k} |
374 (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). |
399 (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). |
375 From @{text "(*)"} it follows then that |
400 From @{text "(*)"} it follows then that |
376 @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn |
401 @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn |
419 of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's |
444 of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's |
420 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the |
445 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the |
421 set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs} |
446 set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs} |
422 % |
447 % |
423 \begin{equation}\label{uplus} |
448 \begin{equation}\label{uplus} |
424 \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}} |
449 \mbox{@{thm (lhs) folds_plus_simp} @{text "= \<Union> (\<calL> ` rs)"}} |
425 \end{equation} |
450 \end{equation} |
426 |
451 |
427 \noindent |
452 \noindent |
428 holds, whereby @{text "\<calL> ` rs"} stands for the |
453 holds, whereby @{text "\<calL> ` rs"} stands for the |
429 image of the set @{text rs} under function @{text "\<calL>"}. |
454 image of the set @{text rs} under function @{text "\<calL>"}. |
660 This allows us to prove a version of Arden's Lemma on the level of equations. |
685 This allows us to prove a version of Arden's Lemma on the level of equations. |
661 |
686 |
662 \begin{lemma}\label{ardenable} |
687 \begin{lemma}\label{ardenable} |
663 Given an equation @{text "X = rhs"}. |
688 Given an equation @{text "X = rhs"}. |
664 If @{text "X = \<Union>\<calL> ` rhs"}, |
689 If @{text "X = \<Union>\<calL> ` rhs"}, |
665 @{thm (prem 2) Arden_keeps_eq}, and |
690 @{thm (prem 2) Arden_preserves_soundness}, and |
666 @{thm (prem 3) Arden_keeps_eq}, then |
691 @{thm (prem 3) Arden_preserves_soundness}, then |
667 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}. |
692 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}. |
668 \end{lemma} |
693 \end{lemma} |
669 |
694 |
670 \noindent |
695 \noindent |
671 Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma, |
696 Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma, |