--- a/Myhill_1.thy Thu Feb 10 13:10:16 2011 +0000
+++ b/Myhill_1.thy Thu Feb 10 21:00:40 2011 +0000
@@ -402,6 +402,13 @@
"L_rhs rhs = \<Union> (L ` rhs)"
end
+lemma L_rhs_union_distrib:
+ fixes A B::"rhs_item set"
+ shows "L A \<union> L B = L (A \<union> B)"
+by simp
+
+
+
text {* Transitions between equivalence classes *}
definition
@@ -412,14 +419,14 @@
text {* Initial equational system *}
definition
- "init_rhs CS X \<equiv>
+ "Init_rhs CS X \<equiv>
if ([] \<in> X) then
{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 \<Turnstile>c\<Rightarrow> X}"
definition
- "eqs CS \<equiv> {(X, init_rhs CS X) | X. X \<in> CS}"
+ "Init CS \<equiv> {(X, Init_rhs CS X) | X. X \<in> CS}"
@@ -464,9 +471,6 @@
definition
"Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
-
-section {* While-combinator *}
-
text {*
The following term @{text "remove ES Y yrhs"} removes the equation
@{text "Y = yrhs"} from equational system @{text "ES"} by replacing
@@ -476,30 +480,33 @@
*}
definition
- "Remove ES Y yrhs \<equiv>
- Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
+ "Remove ES X xrhs \<equiv>
+ Subst_all (ES - {(X, xrhs)}) X (Arden X xrhs)"
+
+
+section {* While-combinator *}
text {*
- The following term @{text "iterm X ES"} represents one iteration in the while loop.
+ The following term @{text "Iter X ES"} represents one iteration in the while loop.
It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
*}
definition
- "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)
+ "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
in Remove ES Y yrhs)"
text {*
- The following term @{text "reduce X ES"} repeatedly removes characteriztion equations
+ The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
for unknowns other than @{text "X"} until one is left.
*}
definition
- "reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (iter X) ES"
+ "Reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (Iter X) ES"
text {*
- Since the @{text "while"} combinator from HOL library is used to implement @{text "reduce X ES"},
+ Since the @{text "while"} combinator from HOL library is used to implement @{text "Reduce X ES"},
the induction principle @{thm [source] while_rule} is used to proved the desired properties
- of @{text "reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
+ of @{text "Reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
in terms of a series of auxilliary predicates:
*}
@@ -573,6 +580,13 @@
"invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and>
finite_rhs ES \<and> self_contained ES"
+
+lemma invariantI:
+ assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES"
+ "finite_rhs ES" "self_contained ES"
+ shows "invariant ES"
+using assms by (simp add: invariant_def)
+
subsection {* The proof of this direction *}
subsubsection {* Basic properties *}
@@ -581,10 +595,6 @@
The following are some basic properties of the above definitions.
*}
-lemma L_rhs_union_distrib:
- fixes A B::"rhs_item set"
- shows "L A \<union> L B = L (A \<union> B)"
-by simp
lemma finite_Trn:
assumes fin: "finite rhs"
@@ -601,7 +611,7 @@
qed
lemma finite_Lam:
- assumes fin:"finite rhs"
+ assumes fin: "finite rhs"
shows "finite {r. Lam r \<in> rhs}"
proof -
have "finite {Lam r | r. Lam r \<in> rhs}"
@@ -614,16 +624,13 @@
qed
lemma rexp_of_empty:
- assumes finite:"finite rhs"
- and nonempty:"rhs_nonempty rhs"
+ assumes finite: "finite rhs"
+ and nonempty: "rhs_nonempty rhs"
shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
using finite nonempty rhs_nonempty_def
using finite_Trn[OF finite]
by (auto)
-lemma [intro!]:
- "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
-
lemma lang_of_rexp_of:
assumes finite:"finite rhs"
shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
@@ -632,41 +639,30 @@
by (rule finite_Trn[OF finite])
then show ?thesis
apply(auto simp add: Seq_def)
- apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
+ apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
+ apply(auto)
apply(rule_tac x= "Trn X xa" in exI)
- apply(auto simp: Seq_def)
+ apply(auto simp add: Seq_def)
done
qed
-lemma rexp_of_lam_eq_lam_set:
- assumes fin: "finite rhs"
- shows "L (\<Uplus>{r. Lam r \<in> rhs}) = L ({Lam r | r. Lam r \<in> rhs})"
-proof -
- have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam)
- then show ?thesis by auto
-qed
-
-lemma [simp]:
- "L (append_rexp r xb) = L xb ;; L r"
-apply (cases xb, auto simp: Seq_def)
-apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
-apply(auto simp: Seq_def)
-done
+lemma lang_of_append:
+ "L (append_rexp r rhs_item) = L rhs_item ;; L r"
+by (induct rule: append_rexp.induct)
+ (auto simp add: seq_assoc)
lemma lang_of_append_rhs:
"L (append_rhs_rexp rhs r) = L rhs ;; L r"
-apply (auto simp:append_rhs_rexp_def image_def)
-apply (auto simp:Seq_def)
-apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def)
-by (rule_tac x = "append_rexp r xb" in exI, auto simp:Seq_def)
+unfolding append_rhs_rexp_def
+by (auto simp add: Seq_def lang_of_append)
lemma classes_of_union_distrib:
- "classes_of A \<union> classes_of B = classes_of (A \<union> B)"
-by (auto simp add:classes_of_def)
+ shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
+by (auto simp add: classes_of_def)
lemma lefts_of_union_distrib:
- "lefts_of A \<union> lefts_of B = lefts_of (A \<union> B)"
-by (auto simp:lefts_of_def)
+ shows "lefts_of (A \<union> B) = lefts_of A \<union> lefts_of B"
+by (auto simp add: lefts_of_def)
subsubsection {* Intialization *}
@@ -702,7 +698,7 @@
qed
lemma l_eq_r_in_eqs:
- assumes X_in_eqs: "(X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"
+ assumes X_in_eqs: "(X, xrhs) \<in> (Init (UNIV // (\<approx>Lang)))"
shows "X = L xrhs"
proof
show "X \<subseteq> L xrhs"
@@ -713,12 +709,12 @@
proof (cases "x = []")
assume empty: "x = []"
thus ?thesis using X_in_eqs "(1)"
- by (auto simp:eqs_def init_rhs_def)
+ by (auto simp: Init_def Init_rhs_def)
next
assume not_empty: "x \<noteq> []"
then obtain clist c where decom: "x = clist @ [c]"
by (case_tac x rule:rev_cases, auto)
- have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:eqs_def)
+ have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:Init_def)
then obtain Y
where "Y \<in> UNIV // (\<approx>Lang)"
and "Y ;; {[c]} \<subseteq> X"
@@ -730,17 +726,17 @@
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: Init_def Init_rhs_def)
qed
qed
next
show "L xrhs \<subseteq> X" using X_in_eqs
- by (auto simp:eqs_def init_rhs_def transition_def)
+ by (auto simp:Init_def Init_rhs_def transition_def)
qed
-lemma finite_init_rhs:
+lemma finite_Init_rhs:
assumes finite: "finite CS"
- shows "finite (init_rhs CS X)"
+ shows "finite (Init_rhs CS X)"
proof-
have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")
proof -
@@ -753,34 +749,36 @@
ultimately show ?thesis
by auto
qed
- thus ?thesis by (simp add:init_rhs_def transition_def)
+ thus ?thesis by (simp add:Init_rhs_def transition_def)
qed
-lemma init_ES_satisfy_invariant:
- assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
- shows "invariant (eqs (UNIV // (\<approx>Lang)))"
-proof -
- have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS
- by (simp add:eqs_def)
- moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"
- by (simp add:distinct_equas_def eqs_def)
- moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"
- by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps)
- moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))"
- using l_eq_r_in_eqs by (simp add:valid_eqns_def)
- moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))"
- using finite_init_rhs[OF finite_CS]
- by (auto simp:finite_rhs_def eqs_def)
- moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"
- by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)
- ultimately show ?thesis by (simp add:invariant_def)
+lemma Init_ES_satisfies_invariant:
+ assumes finite_CS: "finite (UNIV // \<approx>A)"
+ shows "invariant (Init (UNIV // \<approx>A))"
+proof (rule invariantI)
+ show "valid_eqns (Init (UNIV // \<approx>A))"
+ unfolding valid_eqns_def
+ using l_eq_r_in_eqs by simp
+ show "finite (Init (UNIV // \<approx>A))" using finite_CS
+ unfolding Init_def by simp
+ show "distinct_equas (Init (UNIV // \<approx>A))"
+ unfolding distinct_equas_def Init_def by simp
+ show "ardenable (Init (UNIV // \<approx>A))"
+ unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
+ by auto
+ show "finite_rhs (Init (UNIV // \<approx>A))"
+ using finite_Init_rhs[OF finite_CS]
+ unfolding finite_rhs_def Init_def by auto
+ show "self_contained (Init (UNIV // \<approx>A))"
+ unfolding self_contained_def Init_def Init_rhs_def classes_of_def lefts_of_def
+ by auto
qed
subsubsection {* Interation step *}
text {*
From this point until @{text "iteration_step"},
- the correctness of the iteration step @{text "iter X ES"} is proved.
+ the correctness of the iteration step @{text "Iter X ES"} is proved.
*}
lemma Arden_keeps_eq:
@@ -906,8 +904,7 @@
lemma Subst_updates_cls:
"X \<notin> classes_of xrhs \<Longrightarrow>
classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
-apply (simp only:Subst_def append_rhs_keeps_cls
- classes_of_union_distrib[THEN sym])
+apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
by (auto simp:classes_of_def)
lemma Subst_all_keeps_self_contained:
@@ -933,7 +930,7 @@
thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
qed
moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc
- apply (simp only:self_contained_def lefts_of_union_distrib[THEN sym])
+ apply (simp only:self_contained_def lefts_of_union_distrib)
by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}"
using sc
@@ -945,22 +942,44 @@
} thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
qed
-lemma Subst_all_satisfy_invariant:
+lemma Subst_all_satisfies_invariant:
assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
shows "invariant (Subst_all ES Y (Arden Y yrhs))"
-proof -
- have finite_yrhs: "finite yrhs"
+proof (rule invariantI)
+ have Y_eq_yrhs: "Y = L yrhs"
+ using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
+ have finite_yrhs: "finite yrhs"
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
have nonempty_yrhs: "rhs_nonempty yrhs"
using invariant_ES by (auto simp:invariant_def ardenable_def)
- have Y_eq_yrhs: "Y = L yrhs"
- using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
- have "distinct_equas (Subst_all ES Y (Arden Y yrhs))"
+ show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
+ proof-
+ have "Y = L (Arden Y yrhs)"
+ using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
+ by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
+ thus ?thesis using invariant_ES
+ by (clarsimp simp add:valid_eqns_def
+ Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
+ simp del:L_rhs.simps)
+ qed
+ show "finite (Subst_all ES Y (Arden Y yrhs))"
+ using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
+ show "distinct_equas (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES
by (auto simp:distinct_equas_def Subst_all_def invariant_def)
- moreover have "finite (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
- moreover have "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
+ show "ardenable (Subst_all ES Y (Arden Y yrhs))"
+ proof -
+ { fix X rhs
+ assume "(X, rhs) \<in> ES"
+ hence "rhs_nonempty rhs" using prems invariant_ES
+ by (simp add:invariant_def ardenable_def)
+ with nonempty_yrhs
+ have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
+ by (simp add:nonempty_yrhs
+ Subst_keeps_nonempty Arden_keeps_nonempty)
+ } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
+ qed
+ show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
proof-
have "finite_rhs ES" using invariant_ES
by (simp add:invariant_def finite_rhs_def)
@@ -973,32 +992,8 @@
ultimately show ?thesis
by (simp add:Subst_all_keeps_finite_rhs)
qed
- moreover have "ardenable (Subst_all ES Y (Arden Y yrhs))"
- proof -
- { fix X rhs
- assume "(X, rhs) \<in> ES"
- hence "rhs_nonempty rhs" using prems invariant_ES
- by (simp add:invariant_def ardenable_def)
- with nonempty_yrhs
- have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
- by (simp add:nonempty_yrhs
- Subst_keeps_nonempty Arden_keeps_nonempty)
- } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
- qed
- moreover have "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
- proof-
- have "Y = L (Arden Y yrhs)"
- using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
- by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
- thus ?thesis using invariant_ES
- by (clarsimp simp add:valid_eqns_def
- Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
- simp del:L_rhs.simps)
- qed
- moreover
- have self_subst: "self_contained (Subst_all ES Y (Arden Y yrhs))"
+ show "self_contained (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
- ultimately show ?thesis using invariant_ES by (simp add:invariant_def)
qed
lemma Subst_all_card_le:
@@ -1036,16 +1031,16 @@
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
and not_T: "card ES \<noteq> 1"
- shows "(invariant (iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (iter X ES)) \<and>
- (iter X ES, ES) \<in> measure card)"
+ shows "(invariant (Iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (Iter X ES)) \<and>
+ (Iter X ES, ES) \<in> measure card)"
proof -
have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
then obtain Y yrhs
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)
- let ?ES' = "iter X ES"
+ let ?ES' = "Iter X ES"
show ?thesis
- proof(unfold iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
+ proof(unfold Iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
from X_in_ES Y_in_ES and not_eq and Inv_ES
show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
by (auto simp: invariant_def distinct_equas_def)
@@ -1062,7 +1057,7 @@
card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
proof -
have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
- proof(rule Subst_all_satisfy_invariant)
+ proof(rule Subst_all_satisfies_invariant)
from h have "(Y, yrhs) \<in> ES" by simp
hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto
@@ -1104,11 +1099,11 @@
lemma reduce_x:
assumes inv: "invariant ES"
and contain_x: "(X, xrhs) \<in> ES"
- shows "\<exists> xrhs'. reduce X ES = {(X, xrhs')} \<and> invariant(reduce X ES)"
+ shows "\<exists> xrhs'. Reduce X ES = {(X, xrhs')} \<and> invariant(Reduce X ES)"
proof -
let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
show ?thesis
- proof (unfold reduce_def,
+ proof (unfold Reduce_def,
rule while_rule [where P = ?Inv and r = "measure card"])
from inv and contain_x show "?Inv ES" by auto
next
@@ -1116,7 +1111,7 @@
next
fix ES
assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
- show "(iter X ES, ES) \<in> measure card"
+ show "(Iter X ES, ES) \<in> measure card"
proof -
from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
from inv have "invariant ES" by simp
@@ -1126,7 +1121,7 @@
next
fix ES
assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
- thus "?Inv (iter X ES)"
+ thus "?Inv (Iter X ES)"
proof -
from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
from inv have "invariant ES" by simp
@@ -1144,91 +1139,89 @@
lemma last_cl_exists_rexp:
assumes Inv_ES: "invariant {(X, xrhs)}"
- shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
+ shows "\<exists>r::rexp. L r = X"
proof-
def A \<equiv> "Arden X xrhs"
- have "?P (\<Uplus>{r. Lam r \<in> A})"
+ have eq: "{Lam r | r. Lam r \<in> A} = A"
proof -
- have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})"
- proof(rule rexp_of_lam_eq_lam_set)
- show "finite A"
- unfolding A_def
- using Inv_ES
- by (rule_tac Arden_keeps_finite)
- (auto simp add: invariant_def finite_rhs_def)
- qed
- also have "\<dots> = L A"
- proof-
- have "{Lam r | r. Lam r \<in> A} = A"
- proof-
- have "classes_of A = {}" using Inv_ES
- unfolding A_def
- by (simp add:Arden_removes_cl
- self_contained_def invariant_def lefts_of_def)
- thus ?thesis
- unfolding A_def
- by (auto simp only: classes_of_def, case_tac x, auto)
- qed
- thus ?thesis by simp
- qed
- also have "\<dots> = X"
- unfolding A_def
- proof(rule Arden_keeps_eq [THEN sym])
- show "X = L xrhs" using Inv_ES
- by (auto simp only: invariant_def valid_eqns_def)
- next
- from Inv_ES show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
- by(simp add: invariant_def ardenable_def rexp_of_empty finite_rhs_def)
- next
- from Inv_ES show "finite xrhs"
- by (simp add: invariant_def finite_rhs_def)
- qed
- finally show ?thesis by simp
+ have "classes_of A = {}" using Inv_ES
+ unfolding A_def self_contained_def invariant_def lefts_of_def
+ by (simp add: Arden_removes_cl)
+ thus ?thesis unfolding A_def classes_of_def
+ apply(auto simp only:)
+ apply(case_tac x)
+ apply(auto)
+ done
qed
- thus ?thesis by auto
+ have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
+ using Arden_keeps_finite by auto
+ then have "finite {r. Lam r \<in> A}" by (rule finite_Lam)
+ then have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})"
+ by auto
+ also have "\<dots> = L A" by (simp add: eq)
+ also have "\<dots> = X"
+ proof -
+ have "X = L xrhs" using Inv_ES unfolding invariant_def valid_eqns_def
+ by auto
+ moreover
+ from Inv_ES have "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
+ unfolding invariant_def ardenable_def finite_rhs_def
+ by(simp add: rexp_of_empty)
+ moreover
+ from Inv_ES have "finite xrhs" unfolding invariant_def finite_rhs_def
+ by simp
+ ultimately show "L A = X" unfolding A_def
+ by (rule Arden_keeps_eq[symmetric])
+ qed
+ finally have "L (\<Uplus>{r. Lam r \<in> A}) = X" .
+ then show "\<exists>r::rexp. L r = X" by blast
qed
lemma every_eqcl_has_reg:
- assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
- and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))"
- shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
+ assumes finite_CS: "finite (UNIV // \<approx>A)"
+ and X_in_CS: "X \<in> (UNIV // \<approx>A)"
+ shows "\<exists>r::rexp. L r = X"
proof -
- let ?ES = " eqs (UNIV // \<approx>Lang)"
- from X_in_CS
- obtain xrhs where "(X, xrhs) \<in> ?ES"
- by (auto simp:eqs_def init_rhs_def)
- from reduce_x [OF init_ES_satisfy_invariant [OF finite_CS] this]
- have "\<exists>xrhs'. reduce X ?ES = {(X, xrhs')} \<and> invariant (reduce X ?ES)" .
- then obtain xrhs' where "invariant {(X, xrhs')}" by auto
- from last_cl_exists_rexp [OF this]
- show ?thesis .
+ def ES \<equiv> "Init (UNIV // \<approx>A)"
+ have "invariant ES" using finite_CS unfolding ES_def
+ by (rule Init_ES_satisfies_invariant)
+ moreover
+ from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
+ unfolding Init_def Init_rhs_def by auto
+ ultimately
+ obtain xrhs' where "Reduce X ES = {(X, xrhs')}" "invariant (Reduce X ES)"
+ using reduce_x by blast
+ then show "\<exists>r::rexp. L r = X"
+ using last_cl_exists_rexp by auto
qed
-theorem hard_direction:
+lemma bchoice_finite_set:
+ assumes a: "\<forall>x \<in> S. \<exists>y. x = f y"
+ and b: "finite S"
+ shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys"
+using bchoice[OF a] b
+apply(erule_tac exE)
+apply(rule_tac x="fa ` S" in exI)
+apply(auto)
+done
+
+theorem Myhill_Nerode1:
assumes finite_CS: "finite (UNIV // \<approx>A)"
shows "\<exists>r::rexp. A = L r"
proof -
- have "\<forall> X \<in> (UNIV // \<approx>A). \<exists>reg::rexp. X = L reg"
+ have f: "finite (finals A)"
+ using finals_in_partitions finite_CS by (rule finite_subset)
+ have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r"
using finite_CS every_eqcl_has_reg by blast
- then obtain f
- where f_prop: "\<forall> X \<in> (UNIV // \<approx>A). X = L ((f X)::rexp)"
- by (auto dest: bchoice)
- def rs \<equiv> "f ` (finals A)"
- have "A = \<Union> (finals A)" using lang_is_union_of_finals by auto
- also have "\<dots> = L (\<Uplus>rs)"
- proof -
- have "finite rs"
- proof -
- have "finite (finals A)"
- using finite_CS finals_in_partitions[of "A"]
- by (erule_tac finite_subset, simp)
- thus ?thesis using rs_def by auto
- qed
- thus ?thesis
- using f_prop rs_def finals_in_partitions[of "A"] by auto
- qed
- finally show ?thesis by blast
+ then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r"
+ using finals_in_partitions by auto
+ then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs"
+ using f by (auto dest: bchoice_finite_set)
+ then have "A = L (\<Uplus>rs)"
+ unfolding lang_is_union_of_finals[symmetric] by simp
+ then show "\<exists>r::rexp. A = L r" by blast
qed
+
end
\ No newline at end of file