
diff -r 09e6f3719cbc -r 5d724fe0e096 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Aug 19 20:39:07 2011 +0000
+++ b/Journal/Paper.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -37,6 +37,10 @@
 abbreviation "TIMESS \<equiv> Timess"
 abbreviation "STAR \<equiv> Star"
 
+definition
+  Delta :: "'a lang \<Rightarrow> 'a lang"
+where
+  "Delta A = (if [] \<in> A then {[]} else {})"
 
 notation (latex output)
   str_eq ("\<approx>\<^bsub>_\<^esub>") and
@@ -71,12 +75,32 @@
   nullable ("\<delta>'(_')") and
   Cons ("_ :: _" [100, 100] 100) and
   Rev ("Rev _" [1000] 100) and
-  Der ("Der _ _" [1000, 1000] 100) and
+  Deriv ("Der _ _" [1000, 1000] 100) and
+  Derivs ("Ders") and
   ONE ("ONE" 999) and
   ZERO ("ZERO" 999) and
-  pders_lang ("pdersl") and
+  pderivs_lang ("pdersl") and
   UNIV1 ("UNIV\<^isup>+") and
-  Ders_lang ("Dersl")
+  Deriv_lang ("Dersl") and
+  deriv ("der") and
+  derivs ("ders") and
+  pderiv ("pder") and
+  pderivs ("pders") and
+  pderivs_set ("pderss")
+  
+  
+lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union
+
+definition
+  Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where
+  "Der c A \<equiv> {s. [c] @ s \<in> A}"
+
+definition
+  Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where
+  "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+
 
 lemma meta_eq_app:
   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -133,6 +157,27 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
+lemma pow_length:
+  assumes a: "[] \<notin> A"
+  and     b: "s \<in> A \<up> Suc n"
+  shows "n < length s"
+using b
+proof (induct n arbitrary: s)
+  case 0
+  have "s \<in> A \<up> Suc 0" by fact
+  with a have "s \<noteq> []" by auto
+  then show "0 < length s" by auto
+next
+  case (Suc n)
+  have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
+  have "s \<in> A \<up> Suc (Suc n)" by fact
+  then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
+    by (auto simp add: Seq_def)
+  from ih ** have "n < length s2" by simp
+  moreover have "0 < length s1" using * a by auto
+  ultimately show "Suc n < length s" unfolding eq 
+    by (simp only: length_append)
+qed
 
 (*>*)
 
@@ -445,25 +490,25 @@
   \mbox{@{term "X \<cdot> A"}}).
 
   \begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\
-  If @{thm (prem 1) arden} then
-  @{thm (lhs) arden} if and only if
-  @{thm (rhs) arden}.
+  If @{thm (prem 1) reversed_Arden} then
+  @{thm (lhs) reversed_Arden} if and only if
+  @{thm (rhs) reversed_Arden}.
   \end{lmm}
 
   \begin{proof}
-  For the right-to-left direction we assume @{thm (rhs) arden} and show
-  that @{thm (lhs) arden} holds. From Property~\ref{langprops}@{text "(i)"} 
+  For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
+  that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"} 
   we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
   which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both 
   sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
   is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation 
   completes this direction. 
 
-  For the other direction we assume @{thm (lhs) arden}. By a simple induction
+  For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
   on @{text n}, we can establish the property
 
   \begin{center}
-  @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
+  @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
   \end{center}
   
   \noindent
@@ -471,12 +516,12 @@
   all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
   of @{text "\<star>"}.
   For the inclusion in the other direction we assume a string @{text s}
-  with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
+  with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
   we know by Property~\ref{langprops}@{text "(ii)"} that 
   @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
   (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). 
   From @{text "(*)"} it follows then that
-  @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
+  @{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
   implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"} 
   this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
   \end{proof}
@@ -520,7 +565,7 @@
   set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}
   %
   \begin{equation}\label{uplus}
-  \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+  \mbox{@{thm (lhs) folds_plus_simp} @{text "= \<Union> (\<calL> ` rs)"}}
   \end{equation}
 
   \noindent
@@ -1574,7 +1619,7 @@
   relation by using derivatives of regular expressions~\cite{Brzozowski64}. 
 
   Assume the following two definitions for the \emph{left-quotient} of a language,
-  which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c}
+  which we write as @{term "Deriv c A"} and @{term "Derivs s A"} where @{text c}
   is a character and @{text s} a string, respectively:
 
   \begin{center}
@@ -1588,7 +1633,7 @@
   In order to aid readability, we shall make use of the following abbreviation
 
   \begin{center}
-  @{abbrev "Derss s As"}
+  @{abbrev "Derivss s As"}
   \end{center}
   
   \noindent
@@ -1597,7 +1642,7 @@
   (Definition~\ref{myhillneroderel}) and left-quotients
 
   \begin{equation}\label{mhders}
-  @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"}
+  @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Derivs x A = Derivs y A"}
   \end{equation}
 
   \noindent
@@ -1605,16 +1650,16 @@
   
   \begin{equation}
   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
-  @{thm (lhs) Der_simps(1)} & $=$ & @{thm (rhs) Der_simps(1)}\\
-  @{thm (lhs) Der_simps(2)} & $=$ & @{thm (rhs) Der_simps(2)}\\
-  @{thm (lhs) Der_simps(3)} & $=$ & @{thm (rhs) Der_simps(3)}\\
-  @{thm (lhs) Der_simps(4)} & $=$ & @{thm (rhs) Der_simps(4)}\\
+  @{thm (lhs) Deriv_simps(1)} & $=$ & @{thm (rhs) Deriv_simps(1)}\\
+  @{thm (lhs) Deriv_simps(2)} & $=$ & @{thm (rhs) Deriv_simps(2)}\\
+  @{thm (lhs) Deriv_simps(3)} & $=$ & @{thm (rhs) Deriv_simps(3)}\\
+  @{thm (lhs) Deriv_simps(4)} & $=$ & @{thm (rhs) Deriv_simps(4)}\\
   @{thm (lhs) Der_conc}  & $=$ & @{thm (rhs) Der_conc}\\
-  @{thm (lhs) Der_star}  & $=$ & @{thm (rhs) Der_star}\\
-  @{thm (lhs) Ders_simps(1)} & $=$ & @{thm (rhs) Ders_simps(1)}\\
-  @{thm (lhs) Ders_simps(2)} & $=$ & @{thm (rhs) Ders_simps(2)}\\
-  %@{thm (lhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}  & $=$ 
-  %   & @{thm (rhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+  @{thm (lhs) Deriv_star}  & $=$ & @{thm (rhs) Deriv_star}\\
+  @{thm (lhs) Derivs_simps(1)} & $=$ & @{thm (rhs) Derivs_simps(1)}\\
+  @{thm (lhs) Derivs_simps(2)} & $=$ & @{thm (rhs) Derivs_simps(2)}\\
+  %@{thm (lhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}  & $=$ 
+  %   & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
   \end{tabular}}
   \end{equation}
 
@@ -1624,8 +1669,8 @@
   accordingly.  Note also that in the last equation we use the list-cons operator written
   \mbox{@{text "_ :: _"}}.  The only interesting case is the case of @{term "A\<star>"}
   where we use Property~\ref{langprops}@{text "(i)"} in order to infer that
-  @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can then complete the proof by
-  using the fifth equation and noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der
+  @{term "Deriv c (A\<star>) = Deriv c (A \<cdot> A\<star>)"}. We can then complete the proof by
+  using the fifth equation and noting that @{term "Delta A \<cdot> Deriv c (A\<star>) \<subseteq> (Deriv
   c A) \<cdot> A\<star>"}. 
 
   Brzozowski observed that the left-quotients for languages of
@@ -1635,19 +1680,19 @@
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
-  @{thm (lhs) der.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(1)}\\
-  @{thm (lhs) der.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(2)}\\
-  @{thm (lhs) der.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(3)[where c'="d"]}\\
-  @{thm (lhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{thm (rhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
+  @{thm (lhs) deriv.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(1)}\\
+  @{thm (lhs) deriv.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(2)}\\
+  @{thm (lhs) deriv.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(3)[where c'="d"]}\\
+  @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
+     & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) deriv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
      & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
-       @{term "Plus (Times (der c r\<^isub>1) r\<^isub>2) (der c r\<^isub>2)"}\\
+       @{term "Plus (Times (deriv c r\<^isub>1) r\<^isub>2) (deriv c r\<^isub>2)"}\\
      &             & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  
-                    @{term "Times (der c r\<^isub>1) r\<^isub>2"}\\ 
-  @{thm (lhs) der.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(6)}\smallskip\\
-  @{thm (lhs) ders.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) ders.simps(1)}\\
-  @{thm (lhs) ders.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) ders.simps(2)}\\
+                    @{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\ 
+  @{thm (lhs) deriv.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(6)}\smallskip\\
+  @{thm (lhs) derivs.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(1)}\\
+  @{thm (lhs) derivs.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(2)}\\
   \end{tabular}
   \end{center}
 
@@ -1679,8 +1724,8 @@
 
   \begin{equation}\label{Dersders}
   \mbox{\begin{tabular}{c}
-  @{thm Der_der}\\
-  @{thm Ders_ders}
+  @{thm Deriv_deriv}\\
+  @{thm Derivs_derivs}
   \end{tabular}}
   \end{equation}
 
@@ -1691,14 +1736,14 @@
 
   \begin{center}
   @{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}
-  @{term "lang (ders x r) = lang (ders y r)"}. 
+  @{term "lang (derivs x r) = lang (derivs y r)"}. 
   \end{center}
 
   \noindent
   holds and hence
 
   \begin{equation}
-  @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"}
+  @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "derivs x r = derivs y r"}
   \end{equation}
 
 
@@ -1743,19 +1788,19 @@
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
-  @{thm (lhs) pder.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) pder.simps(1)}\\
-  @{thm (lhs) pder.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) pder.simps(2)}\\
-  @{thm (lhs) pder.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) pder.simps(3)[where c'="d"]}\\
-  @{thm (lhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{thm (rhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
+  @{thm (lhs) pderiv.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(1)}\\
+  @{thm (lhs) pderiv.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(2)}\\
+  @{thm (lhs) pderiv.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(3)[where c'="d"]}\\
+  @{thm (lhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
+     & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) pderiv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
      & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
-       @{term "(Timess (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
+       @{term "(Timess (pderiv c r\<^isub>1) r\<^isub>2) \<union> (pderiv c r\<^isub>2)"}\\
      & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  
-                    @{term "Timess (pder c r\<^isub>1) r\<^isub>2"}\\ 
-  @{thm (lhs) pder.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) pder.simps(6)}\smallskip\\
-  @{thm (lhs) pders.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) pders.simps(1)}\\
-  @{thm (lhs) pders.simps(2)}  & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
+                    @{term "Timess (pderiv c r\<^isub>1) r\<^isub>2"}\\ 
+  @{thm (lhs) pderiv.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(6)}\smallskip\\
+  @{thm (lhs) pderivs.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(1)}\\
+  @{thm (lhs) pderivs.simps(2)}  & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
   \end{tabular}
   \end{center}
 
@@ -1773,19 +1818,19 @@
   in order to `sequence' a regular expression with a set of regular
   expressions. Note that in the last clause we first build the set of partial
   derivatives w.r.t~the character @{text c}, then build the image of this set under the
-  function @{term "pders s"} and finally `union up' all resulting sets. It will be
+  function @{term "pderivs s"} and finally `union up' all resulting sets. It will be
   convenient to introduce for this the following abbreviation
 
   \begin{center}
-  @{abbrev "pderss s rs"}
+  @{abbrev "pderivs_set s rs"}
   \end{center}
 
   \noindent
-  which simplifies the last clause of @{const "pders"} to
+  which simplifies the last clause of @{const "pderivs"} to
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
-  @{thm (lhs) pders.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
+  @{thm (lhs) pderivs.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(2)}\\
   \end{tabular}
   \end{center}
 
@@ -1797,8 +1842,8 @@
 
   \begin{equation}\label{Derspders}
   \mbox{\begin{tabular}{lc}
-  @{text "(i)"}  & @{thm Der_pder}\\
-  @{text "(ii)"} & @{thm Ders_pders}
+  @{text "(i)"}  & @{thm Deriv_pderiv}\\
+  @{text "(ii)"} & @{thm Derivs_pderivs}
   \end{tabular}}
   \end{equation} 
 
@@ -1809,7 +1854,7 @@
   induction hypothesis is
 
   \begin{center}
-  @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Ders s (lang r) = \<Union> lang ` (pders s r)"}
+  @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)"}
   \end{center}
 
   \noindent
@@ -1817,12 +1862,12 @@
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll}
-  @{term "Ders (c # s) (lang r)"} 
-    & @{text "="} & @{term "Ders s (Der c (lang r))"} & by def.\\
-    & @{text "="} & @{term "Ders s (\<Union> lang ` (pder c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
-    & @{text "="} & @{term "\<Union> (Ders s) ` (lang ` (pder c r))"} & by def.~of @{text "Ders"}\\
-    & @{text "="} & @{term "\<Union> lang ` (\<Union> pders s ` (pder c r))"} & by IH\\
-    & @{text "="} & @{term "\<Union> lang ` (pders (c # s) r)"} & by def.\\
+  @{term "Derivs (c # s) (lang r)"} 
+    & @{text "="} & @{term "Derivs s (Deriv c (lang r))"} & by def.\\
+    & @{text "="} & @{term "Derivs s (\<Union> lang ` (pderiv c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
+    & @{text "="} & @{term "\<Union> (Derivs s) ` (lang ` (pderiv c r))"} & by def.~of @{text "Ders"}\\
+    & @{text "="} & @{term "\<Union> lang ` (\<Union> pderivs s ` (pderiv c r))"} & by IH\\
+    & @{text "="} & @{term "\<Union> lang ` (pderivs (c # s) r)"} & by def.\\
   \end{tabular}
   \end{center}
   
@@ -1838,8 +1883,8 @@
 
   \begin{equation}
   \mbox{\begin{tabular}{lc}
-  @{text "(i)"}  & @{thm der_pder[symmetric]}\\
-  @{text "(ii)"} & @{thm ders_pders[symmetric]}
+  @{text "(i)"}  & @{thm deriv_pderiv[symmetric]}\\
+  @{text "(ii)"} & @{thm derivs_pderivs[symmetric]}
   \end{tabular}}
   \end{equation} 
 
@@ -1853,12 +1898,12 @@
   derivatives of @{text r} w.r.t.~a language @{text A} is defined as
 
   \begin{equation}\label{Pdersdef}
-  @{thm pders_lang_def}
+  @{thm pderivs_lang_def}
   \end{equation}
 
   \begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}
   For every language @{text A} and every regular expression @{text r}, 
-  \mbox{@{thm finite_pders_lang}}.
+  \mbox{@{thm finite_pderivs_lang}}.
   \end{thrm}
 
   \noindent
@@ -1867,12 +1912,12 @@
 
   \begin{equation}\label{pdersunivone}
   \mbox{\begin{tabular}{l}
-  @{thm pders_lang_Zero}\\
-  @{thm pders_lang_One}\\
-  @{thm pders_lang_Atom}\\
-  @{thm pders_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm pders_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm pders_lang_Star}\\
+  @{thm pderivs_lang_Zero}\\
+  @{thm pderivs_lang_One}\\
+  @{thm pderivs_lang_Atom}\\
+  @{thm pderivs_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm pderivs_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm pderivs_lang_Star}\\
   \end{tabular}}
   \end{equation}
 
@@ -1880,19 +1925,19 @@
   from which one can deduce by induction on @{text r} that
 
   \begin{center}
-  @{thm finite_pders_lang_UNIV1}
+  @{thm finite_pderivs_lang_UNIV1}
   \end{center}
 
   \noindent
   holds. Now Antimirov's theorem follows because
 
   \begin{center}
-  @{thm pders_lang_UNIV}\\
+  @{thm pderivs_lang_UNIV}\\
   \end{center}
 
   \noindent
-  and for all languages @{text "A"}, @{term "pders_lang A r"} is a subset of
-  @{term "pders_lang UNIV r"}.  Since we follow Antimirov's proof quite
+  and for all languages @{text "A"}, @{term "pderivs_lang A r"} is a subset of
+  @{term "pderivs_lang UNIV r"}.  Since we follow Antimirov's proof quite
   closely in our formalisation (only the last two cases of
   \eqref{pdersunivone} involve some non-routine induction arguments), we omit
   the details.
@@ -1907,23 +1952,23 @@
   and \eqref{Derspders} we can easily infer that
 
   \begin{center}
-  @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pders x r = pders y r"}
+  @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pderivs x r = pderivs y r"}
   \end{center}
 
   \noindent
   which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} refines @{term "\<approx>(lang r)"}.
   So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\<approx>(lang r)))"}} 
-  holds if @{term "finite (UNIV // (=(\<lambda>x. pders x r)=))"}. In order to establish 
+  holds if @{term "finite (UNIV // (=(\<lambda>x. pderivs x r)=))"}. In order to establish 
   the latter, we can use Lemma~\ref{finone} and show that the range of the 
-  tagging-function \mbox{@{term "\<lambda>x. pders x r"}} is finite. For this recall Definition
+  tagging-function \mbox{@{term "\<lambda>x. pderivs x r"}} is finite. For this recall Definition
   \ref{Pdersdef}, which gives us that 
 
   \begin{center}
-  @{thm pders_lang_def[where A="UNIV", simplified]}
+  @{thm pderivs_lang_def[where A="UNIV", simplified]}
   \end{center}
 
   \noindent
-  Now the range of @{term "\<lambda>x. pders x r"} is a subset of @{term "Pow (pders_lang UNIV r)"},
+  Now the range of @{term "\<lambda>x. pderivs x r"} is a subset of @{term "Pow (pderivs_lang UNIV r)"},
   which we know is finite by Theorem~\ref{antimirov}. Consequently there 
   are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"},
   which refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the 
@@ -2007,29 +2052,29 @@
   left-quotient. Define
 
   \begin{center}
-  @{abbrev "Ders_lang B A"}
+  @{abbrev "Deriv_lang B A"}
   \end{center}
 
   \noindent
   and assume @{text B} is any language and @{text A} is regular, then @{term
-  "Ders_lang B A"} is regular. To see this consider the following argument
+  "Deriv_lang B A"} is regular. To see this consider the following argument
   using partial derivatives: From @{text A} being regular we know there exists
   a regular expression @{text r} such that @{term "A = lang r"}. We also know
-  that @{term "pders_lang B r"} is finite for every language @{text B} and 
+  that @{term "pderivs_lang B r"} is finite for every language @{text B} and 
   regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition 
   and \eqref{Derspders} therefore
 
   
   \begin{equation}\label{eqq}
-  @{term "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"}
+  @{term "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))"}
   \end{equation}
 
   \noindent
-  Since there are only finitely many regular expressions in @{term "pders_lang
+  Since there are only finitely many regular expressions in @{term "pderivs_lang
   B r"}, we know by \eqref{uplus} that there exists a regular expression so that
-  the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pders_lang B
-  r))"}}. Thus the regular expression @{term "\<Uplus>(pders_lang B r)"} verifies that
-  @{term "Ders_lang B A"} is regular.
+  the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pderivs_lang B
+  r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that
+  @{term "Deriv_lang B A"} is regular.
 *}
 
 




