--- a/Paper/Paper.thy	Sun Jan 30 12:22:07 2011 +0000
+++ b/Paper/Paper.thy	Sun Jan 30 16:59:57 2011 +0000
@@ -6,7 +6,11 @@
 declare [[show_question_marks = false]]
 
 notation (latex output)
-  str_eq_rel ("\<approx>\<^bsub>_\<^esub>")
+  str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
+  Seq (infixr "\<cdot>" 100) and
+  Star ("_\<^bsup>\<star>\<^esup>") and
+  pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
+  Suc ("_+1" [100] 100)
 
 (*>*)
 
@@ -16,6 +20,45 @@
   
 *}
 
+section {* Preliminaries *}
+
+text {*
+  A central technique in our proof is the solution of equational systems
+  involving regular expressions. For this we will use the following ``reverse'' 
+  version of Arden's lemma.
+
+  \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\
+  If @{thm (prem 1) ardens_revised} then
+  @{thm (lhs) ardens_revised} has the unique solution
+  @{thm (rhs) ardens_revised}.
+  \end{lemma}
+
+  \begin{proof}
+  For right-to-left direction we assume @{thm (rhs) ardens_revised} and show
+  @{thm (lhs) ardens_revised}. From Lemma ??? we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
+  which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both 
+  sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
+  is @{term "B \<union> (B ;; A\<star>) ;; A"}. This completes this direction. 
+
+  For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction
+  on @{text n}, we can show the property
+
+  \begin{center}
+  @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper}
+  \end{center}
+  
+  \noindent
+  Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
+  all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using Lemma ???.
+  The inclusion in the other direction we establishing by assuming a string @{text s}
+  with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}
+  we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} as its length is only @{text k}. 
+  From @{text "(*)"} it follows that
+  @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
+  implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this
+  is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
+  \end{proof}
+*}
 
 section {* Regular expressions have finitely many partitions *}
 
@@ -27,7 +70,7 @@
 
   \begin{proof}
   By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
-  and @{const CHAR} are starightforward, because we can easily establish
+  and @{const CHAR} are straightforward, because we can easily establish
 
   \begin{center}
   \begin{tabular}{l}