regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:b04cc5e4e84c
+:7743d2ad71d1
 (*<*)
 theory Paper
-imports "../Myhill_2" "~~/src/HOL/Library/LaTeXsugar"
+imports "../Myhill_2"
 begin
 declare [[show_question_marks = false]]
 consts
 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 ("\<^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
 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) 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)
 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 {*
 Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
 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}
 @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
 \hspace{7mm}
 as \mbox{@{text "{y | y \<approx> x}"}}.
 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
+version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to
-\mbox{@{term "X ;; A"}}).
+\mbox{@{term "X \<cdot> A"}}).
 \begin{lemma}[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}
 \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>"},
+we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"},
-which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both
+which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both
-sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
+sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
-is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction.
+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
 \begin{center}
 @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
 \end{center}
 \noindent
-Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
+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 ;; A\<star> \<subseteq> X"} using the definition
+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}
+@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
-(the strings in @{term "X ;; (A \<up> Suc k)"} are all longer).
+(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
+@{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 ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
+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 ;; A\<star>"}, as we needed to show.\qed
+this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.\qed
 \end{proof}
 \noindent
 Regular expressions are defined as the inductive datatype
 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_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+@{thm (rhs) L_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 L_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
 %
 The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
 they are slightly more complicated. In the @{const SEQ}-case we essentially have
 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}
 %
 \begin{center}
 @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
 \end{center}
 %
 \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'
+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 ;; B"}:
+this string to be in @{term "A \<cdot> B"}:
 %
 \begin{center}
 \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 \scalebox{0.7}{
 \begin{tikzpicture}
 (z.north west) -- ($(z.north east)+(0em,0em)$)
 node[midway, above=0.5em]{@{text z}};
 \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)$)
 node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
 ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
 node[midway, above=0.5em]{@{text z}};
 \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)$)
 node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
 \end{center}
 %
 \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}
 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
 \end{center}
 then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
 @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
 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
 There are two cases to be considered (see pictures above). First, there exists
 a @{text "x'"} such that
 That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and
 @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
 @{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}
 \noindent
 The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When

changeset 166	7743d2ad71d1
parent 162	e93760534354
child 170	b1258b7d2789