regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:b794db0b79db
+:b1258b7d2789
 "EClass x R \<equiv> R `` {x}"
 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
+conc (infixr "\<cdot>" 100) and
-Star ("_\<^bsup>\<star>\<^esup>") 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
 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
 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_Plus ("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_Plus ("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_Times ("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_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) and
-tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
+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:}}>")
 syntax (Rule output)
 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
 Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
 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}
-@{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}
 \noindent
 In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
 and the language matched by a regular expression is defined as
 \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) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\
-@{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
+@{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.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(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 (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
-@{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+@{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
-@{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+@{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
-@{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+@{thm (rhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
-@{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+@{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &
-@{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
+@{thm (rhs) lang.simps(6)[where r="r"]}\\
 \end{tabular}
 \end{tabular}
 \end{center}
 Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
 Overloading the function @{text \<calL>} for the two kinds of terms in the
 equational system, we have
 \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 (rhs) lang_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 lang_trm.simps(1)[where r="r", THEN eq_reflection]}
 \end{center}
 \noindent
 and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
 %
 & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
 & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
 @{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
 prove \eqref{inv1} and \eqref{inv2} more concisely as
 %
 The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because
 we can easily establish that
 \begin{center}
 \begin{tabular}{l}
-@{thm quot_null_eq}\\
+@{thm quot_zero_eq}\\
-@{thm quot_empty_subset}\\
+@{thm quot_one_subset}\\
-@{thm quot_char_subset}
+@{thm quot_atom_subset}
 \end{tabular}
 \end{center}
 \noindent
 hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
 \begin{proof}[@{const "ALT"}-Case]
 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
 where @{text "A"} and @{text "B"} are some arbitrary languages.
 We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
 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 \<cdot> B"}. For this we use the
 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
 with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
 is in the language @{text B}.
 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
 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]
 If @{term "finite (UNIV // \<approx>A)"}
 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of

changeset 170	b1258b7d2789
parent 166	7743d2ad71d1
child 334	d47c2143ab8a