# HG changeset patch
# User urbanc
# Date 1307044936 0
# Node ID 61d0a412a3ae6f27355cd4dd49015f0873baab7a
# Parent  7743d2ad71d1711dcb92554162b423dcbc5f0c78
added a journal version

diff -r 7743d2ad71d1 -r 61d0a412a3ae Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Jun 02 16:44:35 2011 +0000
+++ b/Journal/Paper.thy	Thu Jun 02 20:02:16 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Derivs" "~~/src/HOL/Library/LaTeXsugar" 
+imports "../Closure" 
 begin
 
 declare [[show_question_marks = false]]
@@ -26,7 +26,7 @@
   quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
   REL ("\<approx>") and
   UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
-  L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
+  L_rexp ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
   Lam ("\<lambda>'(_')" [100] 100) and 
   Trn ("'(_, _')" [100, 100] 100) and 
   EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
@@ -41,16 +41,52 @@
   tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
   tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
   tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
+
 lemma meta_eq_app:
   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
   by auto
 
+(* THEOREMS *)
+
+notation (Rule output)
+  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
+  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+
 (*>*)
 
 
 section {* Introduction *}
 
 text {*
+  \noindent
   Regular languages are an important and well-understood subject in Computer
   Science, with many beautiful theorems and many useful algorithms. There is a
   wide range of textbooks on this subject, many of which are aimed at students
@@ -76,7 +112,7 @@
   HOLlight support them with libraries. Even worse, reasoning about graphs and
   matrices can be a real hassle in HOL-based theorem provers.  Consider for
   example the operation of sequencing two automata, say $A_1$ and $A_2$, by
-  connecting the accepting states of $A_1$ to the initial state of $A_2$:\\[-5.5mm]  
+  connecting the accepting states of $A_1$ to the initial state of $A_2$:
   %  
   \begin{center}
   \begin{tabular}{ccc}
@@ -206,10 +242,10 @@
   an automaton that recognises all strings of the language, we define a
   regular language as:
 
-  \begin{definition}
+  \begin{dfntn}
   A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
   strings of @{text "A"}.
-  \end{definition}
+  \end{dfntn}
   
   \noindent
   The reason is that regular expressions, unlike graphs, matrices and functions, can
@@ -241,7 +277,7 @@
   being represented by the empty list, written @{term "[]"}.  \emph{Languages}
   are sets of strings. The language containing all strings is written in
   Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages 
-  is written @{term "A ;; B"} and a language raised to the power @{text n} is written 
+  is written @{term "A \<cdot> B"} and a language raised to the power @{text n} is written 
   @{term "A \<up> n"}. They are defined as usual
 
   \begin{center}
@@ -257,13 +293,13 @@
   is defined as the union over all powers, namely @{thm Star_def}. In the paper
   we will make use of the following properties of these constructions.
   
-  \begin{proposition}\label{langprops}\mbox{}\\
+  \begin{prpstn}\label{langprops}\mbox{}\\
   \begin{tabular}{@ {}ll}
   (i)   & @{thm star_cases}     \\ 
   (ii)  & @{thm[mode=IfThen] pow_length}\\
   (iii) & @{thm seq_Union_left} \\ 
   \end{tabular}
-  \end{proposition}
+  \end{prpstn}
 
   \noindent
   In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
@@ -280,24 +316,24 @@
 
   Central to our proof will be the solution of equational systems
   involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
-  which solves equations of the form @{term "X = A ;; X \<union> B"} provided
+  which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
   @{term "[] \<notin> A"}. However we will need the following `reverse' 
-  version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to
-  \mbox{@{term "X ;; A"}}).
+  version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to
+  \mbox{@{term "X \<cdot> A"}}).
 
-  \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
+  \begin{lmm}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
   If @{thm (prem 1) arden} then
   @{thm (lhs) arden} if and only if
   @{thm (rhs) arden}.
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof}
   For the right-to-left direction we assume @{thm (rhs) arden} and show
   that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} 
-  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 equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. 
+  we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"},
+  which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both 
+  sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
+  is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction. 
 
   For the other direction we assume @{thm (lhs) arden}. By a simple induction
   on @{text n}, we can establish the property
@@ -307,18 +343,18 @@
   \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 the definition
+  Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
+  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}
   we know by Prop.~\ref{langprops}@{text "(ii)"} that 
-  @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
-  (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 
+  @{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 ;; (A \<up> m))"}. This in turn
-  implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 
-  this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
+  @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
+  implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 
+  this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.\qed
   \end{proof}
 
   \noindent
@@ -381,12 +417,12 @@
   strings are related, provided there is no distinguishing extension in this
   language. This can be defined as a tertiary relation.
 
-  \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+  \begin{dfntn}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
   @{text y} are Myhill-Nerode related provided
   \begin{center}
   @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
   \end{center}
-  \end{definition}
+  \end{dfntn}
 
   \noindent
   It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
@@ -407,9 +443,9 @@
   that if there are finitely many equivalence classes, like in the example above, then 
   the language is regular. In our setting we therefore have to show:
   
-  \begin{theorem}\label{myhillnerodeone}
+  \begin{thrm}\label{myhillnerodeone}
   @{thm[mode=IfThen] Myhill_Nerode1}
-  \end{theorem}
+  \end{thrm}
 
   \noindent
   To prove this theorem, we first define the set @{term "finals A"} as those equivalence
@@ -496,8 +532,8 @@
   
   \begin{center}
   @{text "\<calL>(Y, r) \<equiv>"} %
-  @{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
-  @{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]}
+  @{thm (rhs) L_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+  @{thm L_trm.simps(1)[where r="r", THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -544,9 +580,9 @@
   for representing the right-hand sides of equations, we can 
   prove \eqref{inv1} and \eqref{inv2} more concisely as
   %
-  \begin{lemma}\label{inv}
+  \begin{lmm}\label{inv}
   If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
-  \end{lemma}
+  \end{lmm}
 
   \noindent
   Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
@@ -597,13 +633,13 @@
   \noindent
   This allows us to prove a version of Arden's Lemma on the level of equations.
 
-  \begin{lemma}\label{ardenable}
+  \begin{lmm}\label{ardenable}
   Given an equation @{text "X = rhs"}.
   If @{text "X = \<Union>\<calL> ` rhs"},
   @{thm (prem 2) Arden_keeps_eq}, and
   @{thm (prem 3) Arden_keeps_eq}, then
   @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
-  \end{lemma}
+  \end{lmm}
   
   \noindent
   Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
@@ -739,9 +775,9 @@
   It is straightforward to prove that the initial equational system satisfies the
   invariant.
 
-  \begin{lemma}\label{invzero}
+  \begin{lmm}\label{invzero}
   @{thm[mode=IfThen] Init_ES_satisfies_invariant}
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof}
   Finiteness is given by the assumption and the way how we set up the 
@@ -754,9 +790,9 @@
   \noindent
   Next we show that @{text Iter} preserves the invariant.
 
-  \begin{lemma}\label{iterone}
+  \begin{lmm}\label{iterone}
   @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof} 
   The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
@@ -786,9 +822,9 @@
   \noindent
   We also need the fact that @{text Iter} decreases the termination measure.
 
-  \begin{lemma}\label{itertwo}
+  \begin{lmm}\label{itertwo}
   @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof}
   By assumption we know that @{text "ES"} is finite and has more than one element.
@@ -803,11 +839,11 @@
   This brings us to our property we want to establish for @{text Solve}.
 
 
-  \begin{lemma}
+  \begin{lmm}
   If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
   a @{text rhs} such that  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
   and @{term "invariant {(X, rhs)}"}.
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof} 
   In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
@@ -835,9 +871,9 @@
   With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
   there exists a regular expression.
 
-  \begin{lemma}\label{every_eqcl_has_reg}
+  \begin{lmm}\label{every_eqcl_has_reg}
   @{thm[mode=IfThen] every_eqcl_has_reg}
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof}
   By the preceding lemma, we know that there exists a @{text "rhs"} such
@@ -879,9 +915,9 @@
   We will prove in this section the second part of the Myhill-Nerode
   theorem. It can be formulated in our setting as follows:
 
-  \begin{theorem}
+  \begin{thrm}
   Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
-  \end{theorem}  
+  \end{thrm}  
 
   \noindent
   The proof will be by induction on the structure of @{text r}. It turns out
@@ -919,12 +955,12 @@
   is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
   We formally define the notion of a \emph{tagging-relation} as follows.
 
-  \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
+  \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
   and @{text y} are \emph{tag-related} provided
   \begin{center}
   @{text "x =tag= y \<equiv> tag x = tag y"}\;.
   \end{center}
-  \end{definition}
+  \end{dfntn}
 
 
   In order to establish finiteness of a set @{text A}, we shall use the following powerful
@@ -939,9 +975,9 @@
   is finite, then the set @{text A} itself must be finite. We can use it to establish the following 
   two lemmas.
 
-  \begin{lemma}\label{finone}
+  \begin{lmm}\label{finone}
   @{thm[mode=IfThen] finite_eq_tag_rel}
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof}
   We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
@@ -955,12 +991,12 @@
   and @{text Y} must be equal.\qed
   \end{proof}
 
-  \begin{lemma}\label{fintwo} 
+  \begin{lmm}\label{fintwo} 
   Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
   @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
   If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
   then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
-  \end{lemma}
+  \end{lmm}
 
   \begin{proof}
   We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
@@ -1028,12 +1064,12 @@
   to be able to infer that 
   %
   \begin{center}
-  @{text "\<dots>"}@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+  @{text "\<dots>"}@{term "x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
   \end{center}
   %
   \noindent
   using the information given by the appropriate tagging-function. The complication 
-  is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
+  is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A \<cdot> B"}
   (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
   notions of \emph{string prefixes} 
   %
@@ -1054,8 +1090,8 @@
   \noindent
   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. 
   
-  Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' 
-  this string to be in @{term "A ;; B"}:
+  Now assuming  @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split' 
+  this string to be in @{term "A \<cdot> B"}:
   %
   \begin{center}
   \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
@@ -1075,7 +1111,7 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
-               node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+               node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
@@ -1102,7 +1138,7 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
-               node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+               node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
@@ -1118,7 +1154,7 @@
   \noindent
   Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
   or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
-  In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
+  In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. For this we use the 
   following tagging-function
   %
   \begin{center}
@@ -1136,7 +1172,7 @@
   We have to show injectivity of this tagging-function as
   %
   \begin{center}
-  @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+  @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
   \end{center}
   %
   \noindent
@@ -1161,13 +1197,13 @@
   @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
   relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
   have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
-  @{term "y @ z \<in> A ;; B"}, as needed in this case.
+  @{term "y @ z \<in> A \<cdot> B"}, as needed in this case.
 
   Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
   By the assumption about @{term "tag_str_SEQ A B"} we have
   @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
   relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
-  with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case
+  with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const SEQ}-case
   by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed 
   \end{proof}
   
@@ -1309,9 +1345,9 @@
   this point of view. We have established in Isabelle/HOL both directions 
   of the Myhill-Nerode theorem.
   %
-  \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
+  \begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
   A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
-  \end{theorem}
+  \end{thrm}
   %
   \noindent
   Having formalised this theorem means we
diff -r 7743d2ad71d1 -r 61d0a412a3ae Journal/ROOT.ML
--- a/Journal/ROOT.ML	Thu Jun 02 16:44:35 2011 +0000
+++ b/Journal/ROOT.ML	Thu Jun 02 20:02:16 2011 +0000
@@ -1,6 +1,3 @@
-no_document use_thy "../Myhill";
-no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
-no_document use_thy "../Derivs";
 no_document use_thy "../Closure";
 
 use_thy "Paper"
\ No newline at end of file
diff -r 7743d2ad71d1 -r 61d0a412a3ae Journal/document/ita.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/ita.cls	Thu Jun 02 20:02:16 2011 +0000
@@ -0,0 +1,391 @@
+\NeedsTeXFormat{LaTeX2e}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%      ita  class for LaTeX2e                         %%
+%%%      Pierre Damphousse                              %%
+%%%      Copyright (C) EDP Sciences                     %%
+%%%      Version 1.2. September 2002                    %%
+%%%      tex-support@edpsciences.com                    %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% --> THE CLASS OPTION MATERIAL
+%% --> THE CLASS PRESENTATION MATERIAL
+%% --> THE SECTIONING MATERIAL
+%% --> THE METRIC DATA
+%% --> THE TOP MATTER MATERIAL
+%----  (A) The MAKETITLE command and its components
+%----  (B) Preparing the MAKETITLE components
+%          -1-   Heading
+%          -2-   Title and Running Title
+%          -3-   Authors and Running authors
+%          -4-   Date
+%          -5-   Subject Class
+%          -6-   Resume
+%          -7-   Abstract
+%          -8-   Address (\address, given after the \author command)
+%          -9-   Thanks  (given after the title: \thanks)
+%% --> MISCELLANEOUS
+%% --> MESSAGES
+%% --> VARIOUS MACROS
+%----  (A) LATIN ABBREVIATIONS
+%----  (B) REFERENCES
+%----  (C) NEWTHEOREM AND ENVIRONMENTS
+%----  (D) MATHEMATICS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%-----------------------------------------------------------------------------
+%% --> THE CLASS OPTION MATERIAL
+%%-----------------------------------------------------------------------------
+\ProvidesClass{ita}[1999/03/01 v1.1 EDP-Sciences]
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{amsart}}
+\ProcessOptions\relax
+%%-----------------------------------------------------------------------------
+%% --> THE CLASS PRESENTATION MATERIAL
+%%-----------------------------------------------------------------------------
+\LoadClass[reqno]{amsart}[1996/10/24]
+\RequirePackage{cite}
+%%-----------------------------------------------------------------------------
+%% --> THE SECTIONING MATERIAL
+%%-----------------------------------------------------------------------------
+\def\section{\@startsection{section}{1}\z@{1.2\linespacing\@plus\linespacing}%
+{\linespacing} {\fontsize{12}{14}\selectfont\scshape\centering}}
+\def\subsection{\@startsection{subsection}{2}\z@{\linespacing\@plus.8\linespacing}%
+{.8\linespacing}{\fontsize{10}{12}\selectfont\scshape}}
+\def\subsubsection{\@startsection{subsubsection}{3}\z@{.7\linespacing\@plus.5\linespacing}%
+{.5\linespacing}{\normalfont\itshape}}
+\def\paragraph{\@startsection{paragraph}{4}\z@\z@{-\fontdimen2\font}\normalfont}
+\def\subparagraph{\@startsection{subparagraph}{5}\z@\z@{-\fontdimen2\font}\normalfont}
+%%-----------------------------------------------------------------------------
+%% --> THE METRIC DATA
+%%-----------------------------------------------------------------------------
+\setlength\oddsidemargin {15pt}\setlength\evensidemargin{15pt}
+\setlength{\textwidth}{125mm}\setlength{\textheight}{190mm}
+\setlength{\headheight}{18pt}
+%%-----------------------------------------------------------------------------
+%% --> THE TOP MATTER MATERIAL
+%%-----------------------------------------------------------------------------
+% =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   
+%----  (A) The MAKETITLE command and its components
+\def\@maketitle{%
+  \normalfont\normalsize
+  \let\@makefnmark\relax \let\@thefnmark\relax
+  \global\def\shorttitle{\@MSSG@RNNGTTL}
+  \global\def\shortauthors{\@MSSG@RNNGTHR}
+  \@mkboth{\@nx\shortauthors}{\@nx\shorttitle}%
+  \global\topskip42\p@\relax
+  \@SKIP@Aa
+  \vbox{\hbox to\hsize{{\fontsize{10}{12}\selectfont{\bf\@NMJRNL@E}}\hfill%
+  {\fontsize{8}{9}\selectfont\@JRNL@X}}
+  \hbox to\hsize{\fontsize{8}{9}\selectfont{\@NMJRNL@F}\hfill}}
+  \@SKIP@Ab
+  \@setkeywords
+  \@settitle
+  \@setauthors
+  \@setabstract
+  \@setresume
+  \@setsubjclass
+  \normalsize
+  \if@titlepage\newpage\else\dimen@34\p@\advance\dimen@-\baselineskip\vskip\dimen@\relax\fi
+  \gdef\thanks##1{\relax}\gdef\address##1{\relax}
+}% end \@maketitle
+% =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   =   
+%----  (B) Preparing the MAKETITLE components
+%................ ................ ................ ................  ................
+%          -1-   Heading
+%................ ................ ................ ................  ................
+\def\@SKIP@Aa{\vspace*{-1.5cm}}%
+\def\@SKIP@Ab{\vspace*{1.5cm}}%
+\def\@NMJRNL@F{{Informatique Th\'eorique et Applications}}%
+\def\@NMJRNL@E{{Theoretical Informatics and Applications}}%
+\def\@JRNL@X{{Will be set by the publisher}}%
+\def\idline#1page#2{\global\def\@JRNL@X{#1}\setcounter{page}{#2}}
+%................ ................ ................ ................  ................
+%          -2-   Title and Running Title
+%................ ................ ................ ................  ................
+\def\@settitle{\begin{center}\fontsize{11}{15}\selectfont\bfseries
+    \uppercasenonmath\@title\@title\@thnks@i\@thnks@ii\@thnks@iii\@thnks@iv\@thnks@v
+\ifnum\the\@c@thnks@=0\else\footnote{\box\@b@thnks@}\fi
+\end{center}}
+\newbox\@b@rnngttl
+\def\runningtitle#1{\setbox\@b@rnngttl=\hbox{\fontsize{7}{9}\selectfont\rm\uppercase{#1}}}
+%................ ................ ................ ................  ................
+%          -3-   Authors and Running authors
+%................ ................ ................ ................  ................
+\def\@setauthors{\begingroup\trivlist
+  \centering\footnotesize \@topsep30\p@\relax\advance\@topsep by -\baselineskip
+  \item\relax\fontsize{12}{14}\selectfont\scshape\@@th@rs\ignorespaces
+  \footnote{\box\@b@ddrss@}\endtrivlist\endgroup}
+\def\email#1{{e-mail: \tt#1}}
+\newbox\@b@rnngthr
+\def\runningauthors#1{\setbox\@b@rnngthr=\hbox{#1}%
+\global\def\@rnngthrs{\fontsize{7}{9}\selectfont\rm\uppercase{#1}}}
+\newcount\@c@thr@\@c@thr@=0
+\def\author#1{\global\advance\@c@thr@ by 1
+          \global\expandafter\edef\csname @thr@\romannumeral\@c@thr@\endcsname{#1}
+          \global\expandafter\edef\csname @Mthr@\romannumeral\@c@thr@\endcsname{\uppercase{#1}}
+          \global\expandafter\def\csname @ddrss@\romannumeral\@c@thr@\endcsname{}
+          \global\expandafter\def\csname @scndddrss@\romannumeral\@c@thr@\endcsname{}
+          \global\expandafter\def\csname @smddrss@\romannumeral\@c@thr@\endcsname{}}%\author
+%    Elaborating the two author lists (First page and heading)
+\newcount\@y\newcount\@x
+\def\@cnjctn{\ifnum\the\@c@thr@=1\null\else{{\ and\ }}\fi}
+\def\@Mcnjctn{\ifnum\the\@c@thr@=1\null\else{{\ AND\ }}\fi}
+\def\@@th@rs{\@x=0\global\@y=\@c@thr@\global\advance\@y by -1
+\loop\advance\@x by 1
+\ifnum\the\@x<\the\@y\csname  @thr@\romannumeral\@x\endcsname\ignorespaces
+            ${}^{\csname  @ddrss@\romannumeral\@x\endcsname
+                 \csname  @smddrss@\romannumeral\@x\endcsname
+                 \csname  @scndddrss@\romannumeral\@x\endcsname}$,
+\repeat
+\csname  @thr@\romannumeral\@y\endcsname\ignorespaces
+            ${}^{\csname  @ddrss@\romannumeral\@y\endcsname
+                 \csname  @smddrss@\romannumeral\@y\endcsname
+                 \csname  @scndddrss@\romannumeral\@y\endcsname}$\@cnjctn
+\csname  @thr@\romannumeral\@c@thr@\endcsname\ignorespaces
+            ${}^{\csname  @ddrss@\romannumeral\@c@thr@\endcsname
+                 \csname  @smddrss@\romannumeral\@c@thr@\endcsname
+                 \csname  @scndddrss@\romannumeral\@c@thr@\endcsname}$}%\@@th@rs
+\def\M@@th@rs{\@x=0\global\@y=\@c@thr@\global\advance\@y by -1
+\loop\advance\@x by 1
+\ifnum\the\@x<\the\@y\csname  @Mthr@\romannumeral\@x\endcsname,
+\repeat
+\csname  @Mthr@\romannumeral\@y\endcsname\@Mcnjctn
+\csname  @Mthr@\romannumeral\@c@thr@\endcsname}%\M@@th@rs
+\def\@qq#1#2{\vrule height#1 depth#2 width0pt}
+%................ ................ ................ ................  ................
+%          -4-   Date and editor 
+%................ ................ ................ ................  ................
+\let\@date\@empty
+\def\@setdate{\noindent\fontsize{8}{10}\selectfont\hbox{\@date\@addpunct.}}
+\def\editor#1{\def\@editor{#1}}
+\let\@editor\@empty
+\def\@seteditor{\vskip6\p@\noindent\fontsize{8}{10}\selectfont\noindent\hbox{Communicated by 
+\@editor\@addpunct.}}
+%................ ................ ................ ................  ................
+%          -5-   Subject Class
+%................ ................ ................ ................  ................
+%
+\def\@setsubjclass{\skip@20\p@\advance\skip@-\lastskip\advance\skip@-\baselineskip\vskip\skip@
+  \moveright 3pc\hbox{{\bfseries\subjclassname.}\enspace \@subjclass \@addpunct.}} %
+\renewcommand{\subjclassname}{AMS Subject Classification}
+%
+\newbox\@b@kwrds
+\def\keywords#1{\global\setbox\@b@kwrds\vtop{\advance\hsize by-12pt
+    \noindent\footnotesize\textit{\@MSSG@KWRD@0K}#1\@qq{0pt}{4pt}}}
+\def\@setkeywords{\ifvoid\@b@kwrds\else\footnote{\box\@b@kwrds}\fi}
+%................ ................ ................ ................  ................
+%          -6-   Resume
+%................ ................ ................ ................  ................
+\newbox\resumebox
+\newenvironment{resume}{\ifx\maketitle\relax\ClassWarning{\@classname}{\@MSSG@CLSSWRNG}\fi
+  \global\setbox\resumebox=\vtop\bgroup\fontsize{9}{11}\selectfont\advance \hsize -6pc
+  \trivlist 
+    \labelsep.5em\item[\hskip\labelsep{\scshape\fontsize{10}{12}\selectfont\bf R\'esum\'e}.]}
+{\endtrivlist\egroup\ifx\@setresume\relax \@setresumea \fi}
+\def\@setresume{\@setresumea\global\let\@setresume\relax}
+\def\@setresumea{\skip@20\p@\advance\skip@-\lastskip\advance\skip@-\baselineskip \vskip\skip@
+  \ifvoid\resumebox\else\moveright 3pc \box\resumebox\fi}
+%................ ................ ................ ................  ................
+%          -7-   Abstract
+%................ ................ ................ ................  ................
+\newbox\abstractbox
+\renewenvironment{abstract}{\ifx\maketitle\relax\ClassWarning{\@classname}{\@MSSG@CLSSWRNGBSTRCT}\fi
+  \global\setbox\abstractbox=\vtop\bgroup\fontsize{9}{11}\selectfont 
+  \advance \hsize -6pc
+  \trivlist 
+    \labelsep.5em\item[\hskip\labelsep{\scshape\fontsize{10}{12}\selectfont\bf Abstract}.]}
+{\endtrivlist\egroup\ifx\@setabstract\relax \@setabstracta \fi}
+\def\@setabstract{\@setabstracta\global\let\@setabstract\relax}
+\def\@setabstracta{\skip@20\p@ \advance\skip@-\lastskip \advance\skip@-\baselineskip \vskip\skip@
+  \ifvoid\abstractbox{\hbox to\hsize{\kern3pc\fontsize{10}{12}
+          \selectfont\bf \hbox to55pt{Abstract\hfill}\qquad\@MSSG@BSTRCT\hfill}}
+    \else\moveright 3pc \box\abstractbox \fi}
+%................ ................ ................ ................  ................
+%                Address         (\address, given after the \author command)
+%         -8-    Same Address    (\sameaddress, given after the \author command)
+%                Second Address  (\secondaddress, given after the \author command)
+%................ ................ ................ ................  ................
+\def\@spc{\kern1pt}\def\@spcc{\kern2pt}
+\newcount\@c@ddrss@\newbox\@b@ddrss@
+%
+\def\@dd@ddrss@#1{%
+\global\setbox51=\vbox{\advance\hsize by-12pt\unvbox\@b@ddrss@
+  \vtop{\footnotesize\noindent{${}^{\the\@c@ddrss@}$\ }\@qq{10pt}{0pt}\textrm{#1}}}
+  \global\setbox\@b@ddrss@=\vbox{\unvbox51}}%
+%
+\def\@dd@scndddrss@#1{%
+\global\setbox51=\vbox{\advance\hsize by-12pt\unvbox\@b@ddrss@
+  \vtop{\footnotesize\noindent{${}^{\the\@c@ddrss@}$\ }\@qq{10pt}{0pt}\textrm{#1}}}
+  \global\setbox\@b@ddrss@=\vbox{\unvbox51}}
+%
+\def\address#1{\global\advance\@c@ddrss@ by 1\@dd@ddrss@{#1}
+  \expandafter\edef\csname @ddrss@\romannumeral\@c@thr@\endcsname{\@spc\number\@c@ddrss@}}
+\def\secondaddress#1{\global\advance\@c@ddrss@ by 1\@dd@ddrss@{#1}
+  \expandafter\edef\csname @scndddrss@\romannumeral\@c@thr@\endcsname%
+{,\@spcc\number\@c@ddrss@}}%\secondaddress#1
+\def\sameaddress#1{\expandafter\edef\csname @smddrss@\romannumeral\@c@thr@\endcsname{\@spc{}#1}}
+%................ ................ ................ ................  ................
+%          -9-   Thanks  (given in the title: \thanks)
+%................ ................ ................ ................  ................
+\def\@rmnnmrl#1{\ifcase#1\null\or*\or**\or***\or****\or*****\else\@MSSG@THNKS\fi}
+\def\@thnks@i{}\def\@thnks@ii{}\def\@thnks@iii{}\def\@thnks@iv{}\def\@thnks@v{}
+\newcount\@c@thnks@\newbox\@b@thnks@
+\def\@dd@thnks@#1{%
+\global\setbox50=\vbox{\advance\hsize by-12pt\unvbox\@b@thnks@
+  \vtop{\noindent\footnotesize{${}^{\@rmnnmrl\@c@thnks@}$\ }\@qq{10pt}{0pt}\textit{#1}\hfill}}
+\global\setbox\@b@thnks@=\vbox{\unvbox50}}%
+\def\thanks#1{\global\advance\@c@thnks@ by 1\@dd@thnks@{#1}%
+\global\expandafter\edef\csname @thnks@\romannumeral\@c@thnks@\endcsname{%
+\ifnum\the\@c@thnks@=1\@spcc${}^{\@rmnnmrl\@c@thnks@}$\else$^{,\@spcc\@rmnnmrl\@c@thnks@}$\fi}}
+%%-----------------------------------------------------------------------------
+%% --> MISCELLANEOUS
+%%-----------------------------------------------------------------------------
+\DeclareRobustCommand*\cal{\@fontswitch\relax\mathcal}
+%
+\renewcommand\normalsize{\@xsetfontsize\normalsize 6%
+  \@adjustvertspacing \let\@listi\@listI 
+  \abovedisplayskip 11pt \@plus2pt \@minus2pt
+  \belowdisplayskip \abovedisplayskip}
+%
+\def\ps@firstpage{\ps@plain
+  \def\@oddfoot{\hfill{\scriptsize \copyright\ EDP Sciences 1999}}%
+  \let\@evenfoot\@oddfoot\def\@oddhead{\null\hss}
+  \let\@evenhead\@oddhead}% in case an article starts on a left-hand page
+%
+\def\ps@headings{\ps@empty
+  \def\@evenhead{\normalfont\scriptsize\llap{\normalsize\thepage\kern-4pt}\hfil\scriptsize\leftmark{}{}\hfil}%
+  \def\@oddhead{\normalfont\scriptsize\hfil\rightmark{}{}\hfil\rlap{\kern-4pt\normalsize{\thepage}}}%
+  \let\@mkboth\markboth}
+\def\ps@myheadings{\ps@headings \let\@mkboth\@gobbletwo}\pagestyle{headings}
+%%-----------------------------------------------------------------------------
+%% --> MESSAGES
+%%-----------------------------------------------------------------------------
+\def\@MSSG@THNKS{At most 5 thanks allowed}
+\def\@MSSG@CLSSWRNGRSM{Resume should precede \protect\maketitle\space in AMS documentclasses; reported}
+\def\@MSSG@CLSSWRNGBSTRCT{Abstract should precede \protect\maketitle\space in AMS documentclasses; 
+           reported}
+\def\@MSSG@KWRD{{WARNING:  --- Give at least one key words ---}}
+\def\@MSSG@KWRD@0K{{Keywords and phrases:\ }}
+\def\@MSSG@SBJCTCLSS{{--- Give AMS classification codes  ---}}
+\def\@MSSG@RSM{{WARNING:  --- Il est obligatoire de donner un r\'esum\'e en fran\c cais! ---}}
+\def\@MSSG@BSTRCT{{WARNING:  --- An English abstract is mandatory! ---}}
+\def\@MSSG@DT{{(The dates will be set by the publisher)}}
+\def\@MSSG@DTR{{(The editor will be set by the publisher)}}
+%% September 2002
+\def\@MSSG@RNNGTTL{\uppercase{Title will be set by the publisher}}
+\def\@MSSG@RNNGTHR{\uppercase{Title will be set by the publisher}}
+%
+\def\@date{\@MSSG@DT}
+\def\@editor{\@MSSG@DTR}
+\def\@subjclass#1{\@MSSG@SBJCTCLSS}
+%%-----------------------------------------------------------------------------
+%% --> VARIOUS MACROS
+%%-----------------------------------------------------------------------------
+%................ ................ ................ ................  ................
+%----  (A) LATIN ABBREVIATIONS
+%................ ................ ................ ................  ................
+\def\cf{\emph{cf.\/}}\def\ie{\emph{i.e.\/}}\def\etc{\emph{etc\/}}
+\def\apriori{\emph{a priori\/}}\def\afortiori{\emph{a fortiori\/}}
+\def\loccit{\emph{a loc. cit.\/}}\def\etal{\emph{et al.\/}}
+\def\vg{\emph{v.g.\/}}
+%................ ................ ................ ................  ................
+%----  (B) REFERENCES
+%................ ................ ................ ................  ................
+\def\@Rref#1{\hbox{\rm \ref{#1}}}
+\def\Rref#1{\@Rref{#1}}
+%................ ................ ................ ................  ................
+%----  (C) NEWTHEOREM AND ENVIRONMENTS
+%................ ................ ................ ................  ................
+%-------------------
+\theoremstyle{plain}
+%-------------------
+\newtheorem{thrm}{Theorem}[section]
+\newtheorem{lmm}[thrm]{Lemma}
+\newtheorem{crllr}[thrm]{Corollary}
+\newtheorem{prpstn}[thrm]{Proposition}
+\newtheorem{crtrn}[thrm]{Criterion}
+\newtheorem{lgrthm}[thrm]{Algorithm}
+%------------------------
+\theoremstyle{definition}
+%------------------------
+\newtheorem{dfntn}[thrm]{Definition}
+\newtheorem{cnjctr}[thrm]{Conjecture}
+\newtheorem{xmpl}[thrm]{Example}
+\newtheorem{prblm}[thrm]{Problem}
+\newtheorem{rmrk}[thrm]{Remark}
+\newtheorem{nt}[thrm]{Note}
+\newtheorem{clm}[thrm]{Claim}
+\newtheorem{smmr}[thrm]{Summary}
+\newtheorem{cs}[thrm]{Case}
+\newtheorem{bsrvtn}[thrm]{Observation}
+%
+%-------------------
+\theoremstyle{plain}
+%-------------------
+\newenvironment{acknowledgement}{\par\addvspace{17pt}\small\rmfamily\noindent}{\par\addvspace{6pt}}
+%................ ................ ................ ................  ................
+%----  (D) MACROS FOR MATHEMATICS
+%................ ................ ................ ................  ................
+\def\xQuaternion{\mathbb{H}} \def\xC{\mathbb{C}} \def\xR{\mathbb{R}}
+\def\xQ{\mathbb{Q}} \def\xZ{\mathbb{Z}} \def\xN{\mathbb{N}}
+\def\xP{\mathbb{P}} \def\xA{\mathbb{A}}
+%--
+\def\xCzero{{\rm C}^{0}}
+\def\xCone{{\rm C}^{1}} 
+\def\xCtwo{{\rm C}^{2}} 
+\def\xCinfty{{\rm C}^{\infty}} 
+\def\xCn#1{{\rm C}^#1}
+%--
+\def\xHzero{{\rm H}^{0}}
+\def\xHone{{\rm H}^{1}}
+\def\xHtwo{{\rm H}^{2}} 
+\def\xHinfty{{\rm H}^{\infty}}
+\def\xHn#1{{\rm H}^#1}
+%
+\def\xWzero{{\rm W}^{0}}
+\def\xWone{{\rm W}^{1}}
+\def\xWtwo{{\rm W}^{2}} 
+\def\xWinfty{{\rm W}^{\infty}}
+\def\xWn#1{{\rm W}^#1}
+%
+\def\xLzero{{\rm L}^{0}}
+\def\xLone{{\rm L}^{1}}
+\def\xLtwo{{\rm L}^{2}} 
+\def\xLinfty{{\rm L}^{\infty}} 
+\def\xLn#1{{\rm L}^#1}
+%-- 
+\def\xDif{{\rm D}}
+\def\xdif{\,{\rm d}}
+%-- 
+\def\xdrv#1#2{\frac{{\rm d}#1}{{\rm d}#2}}%  "d#1 over d#2"
+\def\xDrv#1#2{\frac{{\rm d}}{{\rm d}#2}#1}%  "d   over d#2  #1"
+%--
+\def\xker{\mathop{\rm ker\,}\nolimits}
+\def\xcoker{\mathop{\rm coker\,}\nolimits}
+\def\xim{\mathop{\rm im\,}\nolimits}
+\def\xcoim{\mathop{\rm coim\,}\nolimits}
+\def\xdim{\mathop{\rm dim\,}\nolimits}
+\def\xcodim{\mathop{\rm codim\,}\nolimits}
+\def\xtr{\mathop{\rm tr\,}\nolimits}
+\def\xHom{\mathop{\rm Hom\,}\nolimits}
+\def\xExt{\mathop{\rm Ext\,}\nolimits}
+\def\xTor{\mathop{\rm Tor\,}\nolimits}
+%--
+\def\xGL{\mathop{\rm GL\,}\nolimits}
+\def\xSL{\mathop{\rm SL\,}\nolimits}
+\def\xPSL{\mathop{\rm PSL\,}\nolimits}
+\def\xSO{\mathop{\rm SO\,}\nolimits}
+\def\xSU{\mathop{\rm SU\,}\nolimits}
+%
+\def\xProof{
+  \normalfont
+  \medskip
+  {\noindent\itshape Proof.\hspace*{6pt}\ignorespaces}}
+%
+\def\enddoc@text{\ifx\@empty\@translators \else\@settranslators\fi
+  \ifx\@empty\@editor \else\@seteditor\\\fi
+  \ifx\@empty\@date \else\@setdate\fi}
+%
+%
+\endinput
diff -r 7743d2ad71d1 -r 61d0a412a3ae Journal/document/root.tex
--- a/Journal/document/root.tex	Thu Jun 02 16:44:35 2011 +0000
+++ b/Journal/document/root.tex	Thu Jun 02 20:02:16 2011 +0000
@@ -1,4 +1,4 @@
-\documentclass[runningheads]{llncs}
+\documentclass{ita}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
@@ -16,8 +16,6 @@
 %%\usepackage{mathabx}
 \usepackage{stmaryrd}
 
-\titlerunning{Myhill-Nerode using Regular Expressions}
-
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -36,13 +34,13 @@
 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}
 \begin{document}
 
-\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
-  Expressions (Proof Pearl)}
-\author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
-\institute{PLA University of Science and Technology, China \and TU Munich, Germany}
-\maketitle
+\title{A Formalisation of the Myhill-Nerode Theorem based on Regular
+  Expressions}
+\author{Chunhan Wu}\address{PLA University of Science and Technology, China}
+\author{Xingyuan Zhang}\sameaddress{1}
+\author{Christian Urban}\address{TU Munich,
+  Germany}\secondaddress{corresponding author}
 
-%\mbox{}\\[-10mm]
 \begin{abstract} 
 There are numerous textbooks on regular languages. Nearly all of them
 introduce the subject by describing finite automata and only mentioning on the
@@ -55,9 +53,8 @@
 reasoning infrastructure comes for free. We show in this paper that a central
 result from formal language theory---the Myhill-Nerode theorem---can be
 recreated using only regular expressions.
-
 \end{abstract}
-
+\maketitle
 
 \input{session}