regexp: comparison Myhill

equal deleted inserted replaced

-:8ab3a06577cf
+:426070e68b21
 assumes a: "x \<in> A\<star>"
 and     b: "y \<in> A"
 shows "x @ y \<in> A\<star>"
 using a b by (blast intro: star_intro1 star_intro2)
+lemma star_cases:
+shows "A\<star> =  {[]} \<union> A ;; A\<star>"
+proof
+{ fix x
+have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"
+unfolding Seq_def
+by (induct rule: star_induct) (auto)
+}
+then show "A\<star> \<subseteq> {[]} \<union> A ;; A\<star>" by auto
+next
+show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"
+unfolding Seq_def by auto
+qed
 lemma star_decom:
-"\<lbrakk>x \<in> A\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>)"
+assumes a: "x \<in> A\<star>" "x \<noteq> []"
+shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"
+using a
 apply(induct rule: star_induct)
 apply(simp)
 apply(blast)
 done
-lemma lang_star_cases:
-shows "L\<star> =  {[]} \<union> L ;; L\<star>"
-proof
-{ fix x
-have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ;; L\<star>"
-unfolding Seq_def
-by (induct rule: star_induct) (auto)
-}
-then show "L\<star> \<subseteq> {[]} \<union> L ;; L\<star>" by auto
-next
-show "{[]} \<union> L ;; L\<star> \<subseteq> L\<star>"
-unfolding Seq_def by auto
-qed
 lemma
 shows seq_Union_left:  "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"
 and   seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"
 unfolding Seq_def by auto
 shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"
 proof
 assume eq: "X = B ;; A\<star>"
 have "A\<star> = {[]} \<union> A\<star> ;; A"
 unfolding seq_star_comm[symmetric]
-by (rule lang_star_cases)
+by (rule star_cases)
 then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
 by (rule seq_add_left)
 also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"
 unfolding seq_union_distrib_left by simp
 also have "\<dots> = B \<union> (B ;; A\<star>) ;; A"
 text {*
 @{text "\<approx>A"} is an equivalence class defined by language @{text "A"}.
 *}
 definition
-str_eq_rel ("\<approx>_" [100] 100)
+str_eq_rel :: "lang \<Rightarrow> (string \<times> string) set" ("\<approx>_" [100] 100)
 where
 "\<approx>A \<equiv> {(x, y).  (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
 text {*
 Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"} singles out
 those which contains the strings from @{text "A"}.
 *}
 definition
-"finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"
+finals :: "lang \<Rightarrow> lang set"
+where
+"finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"
 text {*
 The following lemma establishes the relationshipt between
 @{text "finals A"} and @{text "A"}.
 *}
 text {*
 Given a set of equivalence classes @{text "CS"} and one equivalence class @{text "X"} among
 @{text "CS"}, the term @{text "init_rhs CS X"} is used to extract the right hand side of
 the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"}
 is:
 *}
+definition
+transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
+where
+"Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
 definition
 "init_rhs CS X \<equiv>
 if ([] \<in> X) then
-{Lam(EMPTY)} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}
+{Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
 else
-{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
+{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
 text {*
 In the definition of @{text "init_rhs"}, the term
 @{text "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"} appearing on both branches
 describes the formation of strings in @{text "X"} out of transitions, while
 @{text "X"} rather than by transition. This @{text "{Lam(EMPTY)}"} corresponds to
 the $\lambda$ in \eqref{example_eqns}.
 With the help of @{text "init_rhs"}, the equitional system descrbing the formation of every
 equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}.
 *}
 definition "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
 (************ arden's lemma variation ********************)
 text {*
 With the help of the two functions immediately above, Ardens'
 transformation on right hand side @{text "rhs"} is implemented
 by the following function @{text "arden_variate X rhs"}.
-After this transformation, the recursive occurent of @{text "X"}
+After this transformation, the recursive occurence of @{text "X"}
-in @{text "rhs"} will be eliminated, while the
+in @{text "rhs"} will be eliminated, while the string set defined
-string set defined by @{text "rhs"} is kept unchanged.
+by @{text "rhs"} is kept unchanged.
 *}
 definition
 "arden_variate X rhs \<equiv>
 append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"
 definition
 "eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 text {*
-The computation of regular expressions for equivalent classes is accomplished
+The computation of regular expressions for equivalence classes is accomplished
 using a iteration principle given by the following lemma.
 *}
 lemma wf_iter [rule_format]:
 fixes f
 assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and>  (f(e'), f(e)) \<in> less_than)"
 shows pe:     "P e \<longrightarrow> (\<exists> e'. P e' \<and>  Q e')"
 subsubsection {* Intialization *}
 text {*
 The following several lemmas until @{text "init_ES_satisfy_Inv"} shows that
 the initial equational system satisfies invariant @{text "Inv"}.
 *}
 lemma defined_by_str:
 "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"
 by (auto simp:quotient_def Image_def str_eq_rel_def)
 where "Y \<in> UNIV // (\<approx>Lang)"
 and "Y ;; {[c]} \<subseteq> X"
 and "clist \<in> Y"
 using decom "(1)" every_eqclass_has_transition by blast
 hence
-"x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y ;; {[c]} \<subseteq> X}"
+"x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
-using "(1)" decom
+unfolding transition_def
+	using "(1)" decom
 by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
 thus ?thesis using X_in_eqs "(1)"
-by (simp add:eqs_def init_rhs_def)
+by (simp add: eqs_def init_rhs_def)
 qed
 qed
 next
 show "L xrhs \<subseteq> X" using X_in_eqs
-by (auto simp:eqs_def init_rhs_def)
+by (auto simp:eqs_def init_rhs_def transition_def)
 qed
 lemma finite_init_rhs:
 assumes finite: "finite CS"
 shows "finite (init_rhs CS X)"
 by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)
 moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)
 ultimately show ?thesis
 by auto
 qed
-thus ?thesis by (simp add:init_rhs_def)
+thus ?thesis by (simp add:init_rhs_def transition_def)
 qed
 lemma init_ES_satisfy_Inv:
 assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
 shows "Inv (eqs (UNIV // (\<approx>Lang)))"
 text {*
 From this point until @{text "iteration_step"}, it is proved
 that there exists iteration steps which keep @{text "Inv(ES)"} while
 decreasing the size of @{text "ES"}.
 *}
 lemma arden_variate_keeps_eq:
 assumes l_eq_r: "X = L rhs"
 and not_empty: "[] \<notin> L (rexp_of rhs X)"
 and finite: "finite rhs"
 shows "X = L (arden_variate X rhs)"

changeset 71	426070e68b21
parent 70	8ab3a06577cf
child 75	d63baacbdb16