diff -r b794db0b79db -r b1258b7d2789 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Jun 03 13:59:21 2011 +0000
+++ b/Paper/Paper.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -15,17 +15,33 @@
 abbreviation
   "Append_rexp2 r_itm r == Append_rexp r r_itm"
 
+abbreviation
+  "pow" (infixl "\<up>" 100)
+where
+  "A \<up> n \<equiv> A ^^ n"
+
+
+abbreviation "NULL \<equiv> Zero"
+abbreviation "EMPTY \<equiv> One"
+abbreviation "CHAR \<equiv> Atom"
+abbreviation "ALT \<equiv> Plus"
+abbreviation "SEQ \<equiv> Times"
+abbreviation "STAR \<equiv> Star"
+
+
+ML {* @{term "op ^^"} *}
+
 notation (latex output)
   str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
   str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
-  Seq (infixr "\<cdot>" 100) and
-  Star ("_\<^bsup>\<star>\<^esup>") and
+  conc (infixr "\<cdot>" 100) and
+  star ("_\<^bsup>\<star>\<^esup>") and
   pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
   Suc ("_+1" [100] 100) and
   quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
   REL ("\<approx>") and
   UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
-  L_rexp ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
+  lang ("\<^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
@@ -35,18 +51,27 @@
   Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
   
   uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
-  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
-  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
-  tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
-  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)
+  tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
+  tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
+  tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+  tag_str_Times ("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
 
+lemma conc_def':
+  "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
+unfolding conc_def by simp
+
 (* THEOREMS *)
+
+lemma conc_Union_left: 
+  shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))"
+unfolding conc_def by auto
+
 notation (Rule output)
   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
 
@@ -277,23 +302,23 @@
   @{term "A \<up> n"}. They are defined as usual
 
   \begin{center}
-  @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
+  @{thm conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}
   \hspace{7mm}
-  @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
+  @{thm lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}
   \hspace{7mm}
-  @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+  @{thm lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
   \end{center}
 
   \noindent
   where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
-  is defined as the union over all powers, namely @{thm Star_def}. In the paper
+  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{tabular}{@ {}ll}
   (i)   & @{thm star_cases}     \\ 
   (ii)  & @{thm[mode=IfThen] pow_length}\\
-  (iii) & @{thm seq_Union_left} \\ 
+  (iii) & @{thm conc_Union_left} \\ 
   \end{tabular}
   \end{proposition}
 
@@ -372,18 +397,18 @@
   \begin{center}
   \begin{tabular}{c@ {\hspace{10mm}}c}
   \begin{tabular}{rcl}
-  @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
-  @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
-  @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
+  @{thm (lhs) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\
+  @{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(2)}\\
+  @{thm (lhs) lang.simps(3)[where a="c"]} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(3)[where a="c"]}\\
   \end{tabular}
   &
   \begin{tabular}{rcl}
-  @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
-       @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
-       @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
-      @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
+  @{thm (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
+       @{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+  @{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
+       @{thm (rhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+  @{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+      @{thm (rhs) lang.simps(6)[where r="r"]}\\
   \end{tabular}
   \end{tabular}
   \end{center}
@@ -528,8 +553,8 @@
   
   \begin{center}
   @{text "\<calL>(Y, r) \<equiv>"} %
-  @{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]}
+  @{thm (rhs) lang_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+  @{thm lang_trm.simps(1)[where r="r", THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -568,9 +593,14 @@
   @{thm (lhs) Init_def}     & @{text "\<equiv>"} & @{thm (rhs) Init_def}
   \end{tabular}}
   \end{equation}
+*}(*<*)
 
-  
+lemma test:
+  assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
+  shows "X = \<Union> (lang_trm `  rhs)"
+using assms l_eq_r_in_eqs by (simp)
 
+(*>*)text {*
   \noindent
   Because we use sets of terms 
   for representing the right-hand sides of equations, we can 
@@ -926,9 +956,9 @@
 
   \begin{center}
   \begin{tabular}{l}
-  @{thm quot_null_eq}\\
-  @{thm quot_empty_subset}\\
-  @{thm quot_char_subset}
+  @{thm quot_zero_eq}\\
+  @{thm quot_one_subset}\\
+  @{thm quot_atom_subset}
   \end{tabular}
   \end{center}
 
@@ -1021,7 +1051,7 @@
   We take as tagging-function 
   %
   \begin{center}
-  @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
+  @{thm tag_str_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
   \end{center}
 
   \noindent
@@ -1154,7 +1184,7 @@
   following tagging-function
   %
   \begin{center}
-  @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+  @{thm tag_str_Times_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
   \end{center}
 
   \noindent
@@ -1268,7 +1298,7 @@
   the following tagging-function:
   %
   \begin{center}
-  @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
+  @{thm tag_str_Star_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
   \end{center}
 
   \begin{proof}[@{const STAR}-Case]