--- a/Paper/Paper.thy Wed Feb 16 06:51:58 2011 +0000
+++ b/Paper/Paper.thy Wed Feb 16 12:25:53 2011 +0000
@@ -749,7 +749,7 @@
that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
and that the invariant holds for this equation. That means we
know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
- this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties in the
+ this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the
invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"},
we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
@@ -804,16 +804,23 @@
\end{center}
\end{proof}
+
+
+ @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
+
+ @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]}
+
+ @{thm tag_str_STAR_def[where ?L1.0="A"]}
*}
section {* Conclusion and Related Work *}
text {*
- In this paper we took the view that a regular language as one where there exists
+ In this paper we took the view that a regular language is one where there exists
a regular expression that matches all its strings. For us it was important to find
out how far we can push this point of view. Having formalised the Myhill-Nerode
- theorem means pushed very far. Having the Myhill-Nerode theorem means we can
+ theorem means pushed quite far. Having the Myhill-Nerode theorem means we can
formalise much of the textbook results in this subject.