--- 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]