diff -r b04cc5e4e84c -r 7743d2ad71d1 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue May 31 20:32:49 2011 +0000
+++ b/Paper/Paper.thy	Thu Jun 02 16:44:35 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Myhill_2" "~~/src/HOL/Library/LaTeXsugar" 
+imports "../Myhill_2"
 begin
 
 declare [[show_question_marks = false]]
@@ -25,7 +25,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,10 +41,44 @@
   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" ("_")
+
+
 (*>*)
 
 
@@ -239,7 +273,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}
@@ -278,10 +312,10 @@
 
   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{}\\
   If @{thm (prem 1) arden} then
@@ -292,10 +326,10 @@
   \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
@@ -305,18 +339,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
@@ -494,8 +528,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
@@ -1026,12 +1060,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} 
   %
@@ -1052,8 +1086,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@ {}}
@@ -1073,7 +1107,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)$)
@@ -1100,7 +1134,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)$)
@@ -1116,7 +1150,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}
@@ -1134,7 +1168,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
@@ -1159,13 +1193,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}