--- a/Myhill_1.thy Sun Feb 06 11:21:12 2011 +0000
+++ b/Myhill_1.thy Mon Feb 07 10:23:23 2011 +0000
@@ -133,27 +133,29 @@
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)"
@@ -237,7 +239,7 @@
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)"
@@ -351,7 +353,7 @@
@{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)}"
@@ -361,7 +363,9 @@
*}
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
@@ -464,14 +468,19 @@
@{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
@@ -483,7 +492,7 @@
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}"
@@ -546,10 +555,11 @@
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"}
- in @{text "rhs"} will be eliminated, while the
- string set defined by @{text "rhs"} is kept unchanged.
- *}
+ After this transformation, the recursive occurence of @{text "X"}
+ in @{text "rhs"} will be eliminated, while the string set defined
+ 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))"
@@ -580,9 +590,9 @@
"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
@@ -773,7 +783,7 @@
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}"
@@ -824,16 +834,17 @@
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}"
- using "(1)" decom
+ "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
+ 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)
+ thus ?thesis using X_in_eqs "(1)"
+ 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:
@@ -851,7 +862,7 @@
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:
@@ -884,7 +895,8 @@
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)"