--- a/Myhill.thy Tue Dec 14 14:31:31 2010 +0000
+++ b/Myhill.thy Fri Dec 31 13:47:53 2010 +0000
@@ -15,6 +15,23 @@
start[intro]: "[] \<in> L\<star>"
| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>"
+lemma seq_union_distrib:
+ "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
+by (auto simp:Seq_def)
+
+lemma seq_assoc:
+ "(A ;; B) ;; C = A ;; (B ;; C)"
+unfolding Seq_def
+apply(auto)
+apply(metis)
+by (metis append_assoc)
+
+lemma union_seq:
+ "\<Union> {f x y ;; z| x y. P x y } = (\<Union> {f x y|x y. P x y });; z"
+apply (auto simp add:Seq_def)
+apply metis
+done
+
theorem ardens_revised:
assumes nemp: "[] \<notin> A"
shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"
@@ -61,14 +78,11 @@
where
"folds f z S \<equiv> SOME x. fold_graph f z S x"
-lemma folds_simp_null [simp]:
- "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> L r)"
-apply (simp add: folds_def)
-apply (rule someI2_ex)
-apply (erule finite_imp_fold_graph)
-apply (erule fold_graph.induct)
-apply (auto)
-done
+lemma folds_alt_simp [simp]:
+ "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
+apply (rule set_ext, simp add:folds_def)
+apply (rule someI2_ex, erule finite_imp_fold_graph)
+by (erule fold_graph.induct, auto)
lemma [simp]:
shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
@@ -84,71 +98,94 @@
where
"\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"
+definition
+ final :: "string set \<Rightarrow> string set \<Rightarrow> bool"
+where
+ "final X Lang \<equiv> (X \<in> UNIV // \<approx>Lang) \<and> (\<forall>s \<in> X. s \<in> Lang)"
+lemma lang_is_union_of_finals:
+ "Lang = \<Union> {X. final X Lang}"
+proof
+ show "Lang \<subseteq> \<Union> {X. final X Lang}"
+ proof
+ fix x
+ assume "x \<in> Lang"
+ thus "x \<in> \<Union> {X. final X Lang}"
+ apply (simp, rule_tac x = "(\<approx>Lang) `` {x}" in exI)
+ apply (auto simp:final_def quotient_def Image_def str_eq_rel_def str_eq_def)
+ by (drule_tac x = "[]" in spec, simp)
+ qed
+next
+ show "\<Union>{X. final X Lang} \<subseteq> Lang"
+ by (auto simp:final_def)
+qed
section {* finite \<Rightarrow> regular *}
-definition
- transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
-where
- "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"
+datatype rhs_item =
+ Lam "rexp" (* Lambda *)
+ | Trn "string set" "rexp" (* Transition *)
-definition
- transitions_rexp ("_ \<turnstile>\<rightarrow> _")
-where
- "Y \<turnstile>\<rightarrow> X \<equiv> folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"
+fun the_Trn:: "rhs_item \<Rightarrow> (string set \<times> rexp)"
+where "the_Trn (Trn Y r) = (Y, r)"
+
+fun the_r :: "rhs_item \<Rightarrow> rexp"
+where "the_r (Lam r) = r"
-definition
- "init_rhs CS X \<equiv> if X = {[]}
- then {({[]}, EMPTY)}
- else if ([] \<in> X)
- then insert ({[]}, EMPTY) {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}
- else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"
+overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> string set"
+begin
+fun L_rhs_e:: "rhs_item \<Rightarrow> string set"
+where
+ "L_rhs_e (Lam r) = L r" |
+ "L_rhs_e (Trn X r) = X ;; L r"
+end
-overloading L_rhs \<equiv> "L:: (string set \<times> rexp) set \<Rightarrow> string set"
+overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> string set"
begin
-fun L_rhs:: "(string set \<times> rexp) set \<Rightarrow> string set"
+fun L_rhs:: "rhs_item set \<Rightarrow> string set"
where
- "L_rhs rhs = \<Union> {(Y;; L r) | Y r . (Y, r) \<in> rhs}"
+ "L_rhs rhs = \<Union> (L ` rhs)"
end
definition
- "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, init_rhs CS X)})"
-
-lemma [simp]:
- shows "finite (Y \<Turnstile>\<Rightarrow> X)"
-unfolding transitions_def
-by auto
+ "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}
+ else {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
-lemma defined_by_str:
- assumes "s \<in> X"
- and "X \<in> UNIV // (\<approx>Lang)"
- shows "X = (\<approx>Lang) `` {s}"
-using assms
-unfolding quotient_def Image_def
-unfolding str_eq_rel_def str_eq_def
-by auto
-
-
+definition
+ "eqs CS \<equiv> {(X, init_rhs CS X)|X. X \<in> CS}"
(************ arden's lemma variation ********************)
-definition
- "rexp_of rhs X \<equiv> folds ALT NULL {r. (X, r) \<in> rhs}"
+
+definition
+ "items_of rhs X \<equiv> {Trn X r | r. (Trn X r) \<in> rhs}"
+
+definition
+ "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
definition
- "arden_variate X rhs \<equiv> {(Y, SEQ r (STAR (rexp_of rhs X)))| Y r. (Y, r) \<in> rhs \<and> Y \<noteq> X}"
+ "rexp_of rhs X \<equiv> folds ALT NULL ((snd o the_Trn) ` items_of rhs X)"
+
+definition
+ "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"
-(************* rhs/equations property **************)
+fun attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
+where
+ "attach_rexp r' (Lam r) = Lam (SEQ r r')"
+| "attach_rexp r' (Trn X r) = Trn X (SEQ r r')"
+
+definition
+ "append_rhs_rexp rhs r \<equiv> (attach_rexp r) ` rhs"
definition
- "distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
+ "arden_variate X rhs \<equiv> append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"
+
(*********** substitution of ES *************)
text {* rhs_subst rhs X xrhs: substitude all occurence of X in rhs with xrhs *}
definition
- "rhs_subst rhs X xrhs \<equiv> {(Y, r) | Y r. Y \<noteq> X \<and> (Y, r) \<in> rhs} \<union>
- {(X, SEQ r\<^isub>1 r\<^isub>2 ) | r\<^isub>1 r\<^isub>2. (X, r\<^isub>1) \<in> xrhs \<and> (X, r\<^isub>2) \<in> rhs}"
+ "rhs_subst rhs X xrhs \<equiv> (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"
definition
"eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
@@ -158,17 +195,35 @@
*}
definition
- "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> ([] \<notin> L (rexp_of rhs X)) \<and> X = L rhs"
+ "distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
+
+definition
+ "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"
+
+definition
+ "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
+
+definition
+ "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
definition
"non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}"
-definition
- "self_contained ES \<equiv> \<forall> X xrhs. (X, xrhs) \<in> ES
- \<longrightarrow> (\<forall> Y r.(Y, r) \<in> xrhs \<and> Y \<noteq> {[]} \<longrightarrow> (\<exists> yrhs. (Y, yrhs) \<in> ES))"
+definition
+ "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"
definition
- "Inv ES \<equiv> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> non_empty ES \<and> self_contained ES"
+ "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"
+
+definition
+ "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
+
+definition
+ "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"
+
+definition
+ "Inv ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and>
+ non_empty ES \<and> finite_rhs ES \<and> self_contained ES"
lemma wf_iter [rule_format]:
fixes f
@@ -197,63 +252,574 @@
qed
qed
+text {* ************* basic properties of definitions above ************************ *}
+
+lemma L_rhs_union_distrib:
+ " L (A::rhs_item set) \<union> L B = L (A \<union> B)"
+by simp
+
+lemma finite_snd_Trn:
+ assumes finite:"finite rhs"
+ shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \<in> rhs}" (is "finite ?B")
+proof-
+ def rhs' \<equiv> "{e \<in> rhs. \<exists> r. e = Trn Y r}"
+ have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def)
+ moreover have "finite rhs'" using finite rhs'_def by auto
+ ultimately show ?thesis by simp
+qed
+
+lemma rexp_of_empty:
+ assumes finite:"finite rhs"
+ and nonempty:"rhs_nonempty rhs"
+ shows "[] \<notin> L (rexp_of rhs X)"
+using finite nonempty rhs_nonempty_def
+by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def)
+
+lemma [intro!]:
+ "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
+
+lemma finite_items_of:
+ "finite rhs \<Longrightarrow> finite (items_of rhs X)"
+by (auto simp:items_of_def intro:finite_subset)
+
+lemma lang_of_rexp_of:
+ assumes finite:"finite rhs"
+ shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))"
+proof -
+ have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto
+ thus ?thesis
+ apply (auto simp:rexp_of_def Seq_def items_of_def)
+ apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto)
+ by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)
+qed
+
+lemma rexp_of_lam_eq_lam_set:
+ assumes finite: "finite rhs"
+ shows "L (rexp_of_lam rhs) = L (lam_of rhs)"
+proof -
+ have "finite (the_r ` {Lam r |r. Lam r \<in> rhs})" using finite
+ by (rule_tac finite_imageI, auto intro:finite_subset)
+ thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def)
+qed
+
+lemma [simp]:
+ " L (attach_rexp r xb) = L xb ;; L r"
+apply (cases xb, auto simp:Seq_def)
+by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def)
+
+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 = "attach_rexp r xb" in exI, auto simp:Seq_def)
+
+lemma classes_of_union_distrib:
+ "classes_of A \<union> classes_of B = classes_of (A \<union> 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)
+
+
text {* ******BEGIN: proving the initial equation-system satisfies 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 str_eq_def)
+
+lemma every_eqclass_has_transition:
+ assumes has_str: "s @ [c] \<in> X"
+ and in_CS: "X \<in> UNIV // (\<approx>Lang)"
+ obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
+proof -
+ def Y \<equiv> "(\<approx>Lang) `` {s}"
+ have "Y \<in> UNIV // (\<approx>Lang)"
+ unfolding Y_def quotient_def by auto
+ moreover
+ have "X = (\<approx>Lang) `` {s @ [c]}"
+ using has_str in_CS defined_by_str by blast
+ then have "Y ;; {[c]} \<subseteq> X"
+ unfolding Y_def Image_def Seq_def
+ unfolding str_eq_rel_def
+ by (auto) (simp add: str_eq_def)
+ moreover
+ have "s \<in> Y" unfolding Y_def
+ unfolding Image_def str_eq_rel_def str_eq_def by simp
+ ultimately show thesis by (blast intro: that)
+qed
+
+lemma l_eq_r_in_eqs:
+ assumes X_in_eqs: "(X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"
+ shows "X = L xrhs"
+proof
+ show "X \<subseteq> L xrhs"
+ proof
+ fix x
+ assume "(1)": "x \<in> X"
+ show "x \<in> L xrhs"
+ proof (cases "x = []")
+ assume empty: "x = []"
+ thus ?thesis using X_in_eqs "(1)"
+ by (auto simp:eqs_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)
+ then obtain Y
+ 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}"
+ 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)
+ qed
+ qed
+next
+ show "L xrhs \<subseteq> X" using X_in_eqs
+ by (auto simp:eqs_def init_rhs_def)
+qed
+
+lemma finite_init_rhs:
+ assumes finite: "finite CS"
+ 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 -
+ def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
+ def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
+ have "finite (CS \<times> (UNIV::char set))" using finite by auto
+ hence "finite S" using S_def
+ 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)
+qed
+
lemma init_ES_satisfy_Inv:
assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
- and X_in_eq_cls: "X \<in> (UNIV // (\<approx>Lang))"
shows "Inv (eqs (UNIV // (\<approx>Lang)))"
proof -
have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS
- by (auto simp add:eqs_def)
+ by (simp add:eqs_def)
moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"
- by (auto simp:distinct_equas_def eqs_def)
+ by (simp add:distinct_equas_def eqs_def)
moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"
- proof-
- have "\<And> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<Longrightarrow> ([] \<notin> L (rexp_of rhs X))"
- proof
- apply (auto simp:eqs_def rexp_of_def)
- sorry
- moreover have "\<forall> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<longrightarrow> X = L rhs"
- sorry
- ultimately show ?thesis by (simp add:ardenable_def)
- qed
+ 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 "non_empty (eqs (UNIV // (\<approx>Lang)))"
by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def str_eq_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)
+ by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)
ultimately show ?thesis by (simp add:Inv_def)
qed
+text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}
-text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}
+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)"
+proof -
+ def A \<equiv> "L (rexp_of rhs X)"
+ def b \<equiv> "rhs - items_of rhs X"
+ def B \<equiv> "L b"
+ have "X = B ;; A\<star>"
+ proof-
+ have "rhs = items_of rhs X \<union> b" by (auto simp:b_def items_of_def)
+ hence "L rhs = L(items_of rhs X \<union> b)" by simp
+ hence "L rhs = L(items_of rhs X) \<union> B" by (simp only:L_rhs_union_distrib B_def)
+ with lang_of_rexp_of
+ have "L rhs = X ;; A \<union> B " using finite by (simp only:B_def b_def A_def)
+ thus ?thesis
+ using l_eq_r not_empty
+ apply (drule_tac B = B and X = X in ardens_revised)
+ by (auto simp:A_def simp del:L_rhs.simps)
+ qed
+ moreover have "L (arden_variate X rhs) = (B ;; A\<star>)" (is "?L = ?R")
+ by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs
+ B_def A_def b_def L_rexp.simps seq_union_distrib)
+ ultimately show ?thesis by simp
+qed
+
+lemma append_keeps_finite:
+ "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
+by (auto simp:append_rhs_rexp_def)
+
+lemma arden_variate_keeps_finite:
+ "finite rhs \<Longrightarrow> finite (arden_variate X rhs)"
+by (auto simp:arden_variate_def append_keeps_finite)
+
+lemma append_keeps_nonempty:
+ "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"
+apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)
+by (case_tac x, auto simp:Seq_def)
+
+lemma nonempty_set_sub:
+ "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)"
+by (auto simp:rhs_nonempty_def)
+
+lemma nonempty_set_union:
+ "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"
+by (auto simp:rhs_nonempty_def)
+
+lemma arden_variate_keeps_nonempty:
+ "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (arden_variate X rhs)"
+by (simp only:arden_variate_def append_keeps_nonempty nonempty_set_sub)
+
+
+lemma rhs_subst_keeps_nonempty:
+ "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs_subst rhs X xrhs)"
+by (simp only:rhs_subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub)
+
+lemma rhs_subst_keeps_eq:
+ assumes substor: "X = L xrhs"
+ and finite: "finite rhs"
+ shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
+proof-
+ def A \<equiv> "L (rhs - items_of rhs X)"
+ have "?Left = A \<union> L (append_rhs_rexp xrhs (rexp_of rhs X))"
+ by (simp only:rhs_subst_def L_rhs_union_distrib A_def)
+ moreover have "?Right = A \<union> L (items_of rhs X)"
+ proof-
+ have "rhs = (rhs - items_of rhs X) \<union> (items_of rhs X)" by (auto simp:items_of_def)
+ thus ?thesis by (simp only:L_rhs_union_distrib A_def)
+ qed
+ moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)"
+ using finite substor by (simp only:lang_of_append_rhs lang_of_rexp_of)
+ ultimately show ?thesis by simp
+qed
+
+lemma rhs_subst_keeps_finite_rhs:
+ "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (rhs_subst rhs Y yrhs)"
+by (auto simp:rhs_subst_def append_keeps_finite)
+
+lemma eqs_subst_keeps_finite:
+ assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"
+ shows "finite (eqs_subst ES Y yrhs)"
+proof -
+ have "finite {(Ya, rhs_subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" (is "finite ?A")
+ proof-
+ def eqns' \<equiv> "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \<in> ES}"
+ def h \<equiv> "\<lambda> ((Ya::string set), yrhsa). (Ya, rhs_subst yrhsa Y yrhs)"
+ have "finite (h ` eqns')" using finite h_def eqns'_def by auto
+ moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def)
+ ultimately show ?thesis by auto
+ qed
+ thus ?thesis by (simp add:eqs_subst_def)
+qed
+
+lemma eqs_subst_keeps_finite_rhs:
+ "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (eqs_subst ES Y yrhs)"
+by (auto intro:rhs_subst_keeps_finite_rhs simp add:eqs_subst_def finite_rhs_def)
+
+lemma append_rhs_keeps_cls:
+ "classes_of (append_rhs_rexp rhs r) = classes_of rhs"
+apply (auto simp:classes_of_def append_rhs_rexp_def)
+apply (case_tac xa, auto simp:image_def)
+by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
+
+lemma arden_variate_removes_cl:
+ "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}"
+apply (simp add:arden_variate_def append_rhs_keeps_cls items_of_def)
+by (auto simp:classes_of_def)
+
+lemma lefts_of_keeps_cls:
+ "lefts_of (eqs_subst ES Y yrhs) = lefts_of ES"
+by (auto simp:lefts_of_def eqs_subst_def)
+
+lemma rhs_subst_updates_cls:
+ "X \<notin> classes_of xrhs \<Longrightarrow> classes_of (rhs_subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
+apply (simp only:rhs_subst_def append_rhs_keeps_cls classes_of_union_distrib[THEN sym])
+by (auto simp:classes_of_def items_of_def)
+
+lemma eqs_subst_keeps_self_contained:
+ fixes Y
+ assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
+ shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" (is "self_contained ?B")
+proof-
+ { fix X xrhs'
+ assume "(X, xrhs') \<in> ?B"
+ then obtain xrhs
+ where xrhs_xrhs': "xrhs' = rhs_subst xrhs Y (arden_variate Y yrhs)"
+ and X_in: "(X, xrhs) \<in> ES" by (simp add:eqs_subst_def, blast)
+ have "classes_of xrhs' \<subseteq> lefts_of ?B"
+ proof-
+ have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def eqs_subst_def)
+ moreover have "classes_of xrhs' \<subseteq> lefts_of ES"
+ proof-
+ have "classes_of xrhs' \<subseteq> classes_of xrhs \<union> classes_of (arden_variate Y yrhs) - {Y}"
+ proof-
+ have "Y \<notin> classes_of (arden_variate Y yrhs)" using arden_variate_removes_cl by simp
+ thus ?thesis using xrhs_xrhs' by (auto simp:rhs_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])
+ by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
+ moreover have "classes_of (arden_variate Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" using sc
+ by (auto simp add:arden_variate_removes_cl self_contained_def lefts_of_def)
+ ultimately show ?thesis by auto
+ qed
+ ultimately show ?thesis by simp
+ qed
+ } thus ?thesis by (auto simp only:eqs_subst_def self_contained_def)
+qed
+
+lemma eqs_subst_satisfy_Inv:
+ assumes Inv_ES: "Inv (ES \<union> {(Y, yrhs)})"
+ shows "Inv (eqs_subst ES Y (arden_variate Y yrhs))"
+proof -
+ have finite_yrhs: "finite yrhs" using Inv_ES by (auto simp:Inv_def finite_rhs_def)
+ have nonempty_yrhs: "rhs_nonempty yrhs" using Inv_ES by (auto simp:Inv_def ardenable_def)
+ have Y_eq_yrhs: "Y = L yrhs" using Inv_ES by (simp only:Inv_def valid_eqns_def, blast)
+
+ have "distinct_equas (eqs_subst ES Y (arden_variate Y yrhs))" using Inv_ES
+ by (auto simp:distinct_equas_def eqs_subst_def Inv_def)
+ moreover have "finite (eqs_subst ES Y (arden_variate Y yrhs))" using Inv_ES
+ by (simp add:Inv_def eqs_subst_keeps_finite)
+ moreover have "finite_rhs (eqs_subst ES Y (arden_variate Y yrhs))"
+ proof-
+ have "finite_rhs ES" using Inv_ES by (simp add:Inv_def finite_rhs_def)
+ moreover have "finite (arden_variate Y yrhs)"
+ proof -
+ have "finite yrhs" using Inv_ES by (auto simp:Inv_def finite_rhs_def)
+ thus ?thesis using arden_variate_keeps_finite by simp
+ qed
+ ultimately show ?thesis by (simp add:eqs_subst_keeps_finite_rhs)
+ qed
+ moreover have "ardenable (eqs_subst ES Y (arden_variate Y yrhs))"
+ proof -
+ { fix X rhs
+ assume "(X, rhs) \<in> ES"
+ hence "rhs_nonempty rhs" using prems Inv_ES by (simp add:Inv_def ardenable_def)
+ with nonempty_yrhs have "rhs_nonempty (rhs_subst rhs Y (arden_variate Y yrhs))"
+ by (simp add:nonempty_yrhs rhs_subst_keeps_nonempty arden_variate_keeps_nonempty)
+ } thus ?thesis by (auto simp add:ardenable_def eqs_subst_def)
+ qed
+ moreover have "valid_eqns (eqs_subst ES Y (arden_variate Y yrhs))"
+ proof-
+ have "Y = L (arden_variate Y yrhs)" using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs
+ by (rule_tac arden_variate_keeps_eq, (simp add:rexp_of_empty)+)
+ thus ?thesis using Inv_ES
+ by (clarsimp simp add:valid_eqns_def eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def
+ simp del:L_rhs.simps)
+ qed
+ moreover have non_empty_subst: "non_empty (eqs_subst ES Y (arden_variate Y yrhs))"
+ using Inv_ES by (auto simp:Inv_def non_empty_def eqs_subst_def)
+ moreover have self_subst: "self_contained (eqs_subst ES Y (arden_variate Y yrhs))"
+ using Inv_ES eqs_subst_keeps_self_contained by (simp add:Inv_def)
+ ultimately show ?thesis using Inv_ES by (simp add:Inv_def)
+qed
+
+lemma eqs_subst_card_le:
+ assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
+ shows "card (eqs_subst ES Y yrhs) <= card ES"
+proof-
+ def f \<equiv> "\<lambda> x. ((fst x)::string set, rhs_subst (snd x) Y yrhs)"
+ have "eqs_subst ES Y yrhs = f ` ES"
+ apply (auto simp:eqs_subst_def f_def image_def)
+ by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+)
+ thus ?thesis using finite by (auto intro:card_image_le)
+qed
+
+lemma eqs_subst_cls_remains:
+ "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (eqs_subst ES Y yrhs)"
+by (auto simp:eqs_subst_def)
+
+lemma card_noteq_1_has_more:
+ assumes card:"card S \<noteq> 1"
+ and e_in: "e \<in> S"
+ and finite: "finite S"
+ obtains e' where "e' \<in> S \<and> e \<noteq> e'"
+proof-
+ have "card (S - {e}) > 0"
+ proof -
+ have "card S > 1" using card e_in finite by (case_tac "card S", auto)
+ thus ?thesis using finite e_in by auto
+ qed
+ hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)
+ thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
+qed
lemma iteration_step:
assumes Inv_ES: "Inv ES"
- and X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"
- and not_T: "card ES > 1"
- shows "(\<exists> ES' xrhs'. Inv ES' \<and> (card ES', card ES) \<in> less_than \<and> (X, xrhs') \<in> ES')"
+ and X_in_ES: "(X, xrhs) \<in> ES"
+ and not_T: "card ES \<noteq> 1"
+ shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'.(X, xrhs') \<in> ES')) \<and> (card ES', card ES) \<in> less_than" (is "\<exists> ES'. ?P ES'")
proof -
+ have finite_ES: "finite ES" using Inv_ES by (simp add:Inv_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)
+ def ES' == "ES - {(Y, yrhs)}"
+ let ?ES'' = "eqs_subst ES' Y (arden_variate Y yrhs)"
+ have "?P ?ES''"
+ proof -
+ have "Inv ?ES''" using Y_in_ES Inv_ES
+ by (rule_tac eqs_subst_satisfy_Inv, simp add:ES'_def insert_absorb)
+ moreover have "\<exists>xrhs'. (X, xrhs') \<in> ?ES''" using not_eq X_in_ES
+ by (rule_tac ES = ES' in eqs_subst_cls_remains, auto simp add:ES'_def)
+ moreover have "(card ?ES'', card ES) \<in> less_than"
+ proof -
+ have "finite ES'" using finite_ES ES'_def by auto
+ moreover have "card ES' < card ES" using finite_ES Y_in_ES
+ by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less)
+ ultimately show ?thesis
+ by (auto dest:eqs_subst_card_le elim:le_less_trans)
+ qed
+ ultimately show ?thesis by simp
+ qed
+ thus ?thesis by blast
+qed
+
+text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *}
-
-
+lemma iteration_conc:
+ assumes history: "Inv ES"
+ and X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"
+ shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1" (is "\<exists> ES'. ?P ES'")
+proof (cases "card ES = 1")
+ case True
+ thus ?thesis using history X_in_ES
+ by blast
+next
+ case False
+ thus ?thesis using history iteration_step X_in_ES
+ by (rule_tac f = card in wf_iter, auto)
+qed
+
+lemma last_cl_exists_rexp:
+ assumes ES_single: "ES = {(X, xrhs)}"
+ and Inv_ES: "Inv ES"
+ shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
+proof-
+ let ?A = "arden_variate X xrhs"
+ have "?P (rexp_of_lam ?A)"
+ proof -
+ have "L (rexp_of_lam ?A) = L (lam_of ?A)"
+ proof(rule rexp_of_lam_eq_lam_set)
+ show "finite (arden_variate X xrhs)" using Inv_ES ES_single
+ by (rule_tac arden_variate_keeps_finite, auto simp add:Inv_def finite_rhs_def)
+ qed
+ also have "\<dots> = L ?A"
+ proof-
+ have "lam_of ?A = ?A"
+ proof-
+ have "classes_of ?A = {}" using Inv_ES ES_single
+ by (simp add:arden_variate_removes_cl self_contained_def Inv_def lefts_of_def)
+ thus ?thesis by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)
+ qed
+ thus ?thesis by simp
+ qed
+ also have "\<dots> = X"
+ proof(rule arden_variate_keeps_eq [THEN sym])
+ show "X = L xrhs" using Inv_ES ES_single by (auto simp only:Inv_def valid_eqns_def)
+ next
+ from Inv_ES ES_single show "[] \<notin> L (rexp_of xrhs X)"
+ by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def)
+ next
+ from Inv_ES ES_single show "finite xrhs" by (simp add:Inv_def finite_rhs_def)
+ qed
+ finally show ?thesis by simp
+ qed
+ thus ?thesis by auto
+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")
+proof -
+ from X_in_CS have "\<exists> xrhs. (X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"
+ by (auto simp:eqs_def init_rhs_def)
+ then obtain ES xrhs where Inv_ES: "Inv ES"
+ and X_in_ES: "(X, xrhs) \<in> ES"
+ and card_ES: "card ES = 1"
+ using finite_CS X_in_CS init_ES_satisfy_Inv iteration_conc
+ by blast
+ hence ES_single_equa: "ES = {(X, xrhs)}"
+ by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff)
+ thus ?thesis using Inv_ES
+ by (rule last_cl_exists_rexp)
+qed
+theorem hard_direction:
+ assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
+ shows "\<exists> (reg::rexp). Lang = L reg"
+proof -
+ have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg"
+ using finite_CS every_eqcl_has_reg by blast
+ then obtain f where f_prop: "\<forall> X \<in> (UNIV // (\<approx>Lang)). X = L ((f X)::rexp)"
+ by (auto dest:bchoice)
+ def rs \<equiv> "f ` {X. final X Lang}"
+ have "Lang = \<Union> {X. final X Lang}" using lang_is_union_of_finals by simp
+ also have "\<dots> = L (folds ALT NULL rs)"
+ proof -
+ have "finite {X. final X Lang}" using finite_CS by (auto simp:final_def)
+ thus ?thesis using f_prop by (auto simp:rs_def final_def)
+ qed
+ finally show ?thesis by blast
+qed
+section {* regular \<Rightarrow> finite*}
+
+lemma quot_empty_subset:
+ "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
+proof
+ fix x
+ assume h: "x \<in> UNIV // \<approx>{[]}"
+ show "x \<in> {{[]}, UNIV - {[]}}"
+
+ have "\<And> s. s \<approx>{[]} [] \<Longrightarrow> s = []"
+ apply (auto simp add:str_eq_def)
+ apply blast
+
+ hence "False"
+ apply (simp add:quotient_def)
-
-
-
-
-
+lemma other_direction:
+ "Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))"
+proof (induct arbitrary:Lang rule:rexp.induct)
+ case NULL
+ have "UNIV // (\<approx>{}) \<subseteq> {UNIV} "
+ by (auto simp:quotient_def str_eq_rel_def str_eq_def)
+ with prems show "?case" by (auto intro:finite_subset)
+next
+ case EMPTY
+ have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
+ sorry
+ with prems show ?case by (auto intro:finite_subset)
+next
+ case (CHAR c)
+ have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
+ sorry
+ with prems show ?case by (auto intro:finite_subset)
+next
+ case (SEQ r1 r2)
+ show ?case sorry
+next
+ case (ALT r1 r1)
+ show ?case sorry
+next
+ case (STAR r)
+ show ?case sorry
+qed
+
-
-
-
-
-
-
+
@@ -271,645 +837,9 @@
-lemma distinct_rhs_equations:
- "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs"
-by (auto simp: equations_def equation_rhs_def distinct_rhs_def empty_rhs_def dest:no_two_cls_inters)
-
-lemma every_nonempty_eqclass_has_strings:
- "\<lbrakk>X \<in> (UNIV Quo Lang); X \<noteq> {[]}\<rbrakk> \<Longrightarrow> \<exists> clist. clist \<in> X \<and> clist \<noteq> []"
-by (auto simp:quot_def equiv_class_def equiv_str_def)
-
-lemma every_eqclass_is_derived_from_empty:
- assumes not_empty: "X \<noteq> {[]}"
- shows "X \<in> (UNIV Quo Lang) \<Longrightarrow> \<exists> clist. {[]};{clist} \<subseteq> X \<and> clist \<noteq> []"
-using not_empty
-apply (drule_tac every_nonempty_eqclass_has_strings, simp)
-by (auto intro:exI[where x = clist] simp:lang_seq_def)
-
-lemma equiv_str_in_CS:
- "\<lbrakk>clist\<rbrakk>Lang \<in> (UNIV Quo Lang)"
-by (auto simp:quot_def)
-
-lemma has_str_imp_defined_by_str:
- "\<lbrakk>str \<in> X; X \<in> UNIV Quo Lang\<rbrakk> \<Longrightarrow> X = \<lbrakk>str\<rbrakk>Lang"
-by (auto simp:quot_def equiv_class_def equiv_str_def)
-
-lemma every_eqclass_has_ascendent:
- assumes has_str: "clist @ [c] \<in> X"
- and in_CS: "X \<in> UNIV Quo Lang"
- shows "\<exists> Y. Y \<in> UNIV Quo Lang \<and> Y-c\<rightarrow>X \<and> clist \<in> Y" (is "\<exists> Y. ?P Y")
-proof -
- have "?P (\<lbrakk>clist\<rbrakk>Lang)"
- proof -
- have "\<lbrakk>clist\<rbrakk>Lang \<in> UNIV Quo Lang"
- by (simp add:quot_def, rule_tac x = clist in exI, simp)
- moreover have "\<lbrakk>clist\<rbrakk>Lang-c\<rightarrow>X"
- proof -
- have "X = \<lbrakk>(clist @ [c])\<rbrakk>Lang" using has_str in_CS
- by (auto intro!:has_str_imp_defined_by_str)
- moreover have "\<forall> sl. sl \<in> \<lbrakk>clist\<rbrakk>Lang \<longrightarrow> sl @ [c] \<in> \<lbrakk>(clist @ [c])\<rbrakk>Lang"
- by (auto simp:equiv_class_def equiv_str_def)
- ultimately show ?thesis unfolding CT_def lang_seq_def
- by auto
- qed
- moreover have "clist \<in> \<lbrakk>clist\<rbrakk>Lang"
- by (auto simp:equiv_str_def equiv_class_def)
- ultimately show "?P (\<lbrakk>clist\<rbrakk>Lang)" by simp
- qed
- thus ?thesis by blast
-qed
-
-lemma finite_charset_rS:
- "finite {CHAR c |c. Y-c\<rightarrow>X}"
-by (rule_tac A = UNIV and f = CHAR in finite_surj, auto)
-
-lemma l_eq_r_in_equations:
- assumes X_in_equas: "(X, xrhs) \<in> equations (UNIV Quo Lang)"
- shows "X = L xrhs"
-proof (cases "X = {[]}")
- case True
- thus ?thesis using X_in_equas
- by (simp add:equations_def equation_rhs_def lang_seq_def)
-next
- case False
- show ?thesis
- proof
- show "X \<subseteq> L xrhs"
- proof
- fix x
- assume "(1)": "x \<in> X"
- show "x \<in> L xrhs"
- proof (cases "x = []")
- assume empty: "x = []"
- hence "x \<in> L (empty_rhs X)" using "(1)"
- by (auto simp:empty_rhs_def lang_seq_def)
- thus ?thesis using X_in_equas False empty "(1)"
- unfolding equations_def equation_rhs_def by auto
- next
- assume not_empty: "x \<noteq> []"
- hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto)
- then obtain clist c where decom: "x = clist @ [c]" by blast
- moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>
- \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"
- proof -
- fix Y
- assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang"
- and Y_CT_X: "Y-c\<rightarrow>X"
- and clist_in_Y: "clist \<in> Y"
- with finite_charset_rS
- show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"
- by (auto simp :fold_alt_null_eqs)
- qed
- hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})"
- using X_in_equas False not_empty "(1)" decom
- by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def)
- then obtain Xa where
- "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast
- hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}"
- using X_in_equas "(1)" decom
- by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa])
- thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def
- by auto
- qed
- qed
- next
- show "L xrhs \<subseteq> X"
- proof
- fix x
- assume "(2)": "x \<in> L xrhs"
- have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
- using finite_charset_rS
- by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)
- have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
- by (simp add:empty_rhs_def split:if_splits)
- show "x \<in> X" using X_in_equas False "(2)"
- by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def)
- qed
- qed
-qed
-
-
-
-lemma no_EMPTY_equations:
- "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs"
-apply (clarsimp simp add:equations_def equation_rhs_def)
-apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto)
-apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+
-done
-
-lemma init_ES_satisfy_ardenable:
- "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> ardenable (X, xrhs)"
- unfolding ardenable_def
- by (auto intro:distinct_rhs_equations no_EMPTY_equations simp:l_eq_r_in_equations simp del:L_rhs.simps)
-
-lemma init_ES_satisfy_Inv:
- assumes finite_CS: "finite (UNIV Quo Lang)"
- and X_in_eq_cls: "X \<in> UNIV Quo Lang"
- shows "Inv X (equations (UNIV Quo Lang))"
-proof -
- have "finite (equations (UNIV Quo Lang))" using finite_CS
- by (auto simp:equations_def)
- moreover have "\<exists>rhs. (X, rhs) \<in> equations (UNIV Quo Lang)" using X_in_eq_cls
- by (simp add:equations_def)
- moreover have "distinct_equas (equations (UNIV Quo Lang))"
- by (auto simp:distinct_equas_def equations_def)
- moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow>
- rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equations (UNIV Quo Lang)))"
- apply (simp add:left_eq_cls_def equations_def rhs_eq_cls_def equation_rhs_def)
- by (auto simp:empty_rhs_def split:if_splits)
- moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> X \<noteq> {}"
- by (clarsimp simp:equations_def empty_notin_CS intro:classical)
- moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> ardenable (X, xrhs)"
- by (auto intro!:init_ES_satisfy_ardenable)
- ultimately show ?thesis by (simp add:Inv_def)
-qed
-
-
-text {* *********** END: proving the initial equation-system satisfies Inv ******* *}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}
-
-lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk>
- \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A "
-apply (case_tac "insert a A = {a}")
-by (auto simp:TCon_def)
-
-lemma not_T_atleast_2[rule_format]:
- "finite S \<Longrightarrow> \<forall> x. x \<in> S \<and> (\<not> TCon S)\<longrightarrow> (\<exists> y. x \<noteq> y \<and> y \<in> S)"
-apply (erule finite.induct, simp)
-apply (clarify, case_tac "x = a")
-by (erule not_T_aux, auto)
-
-lemma exist_another_equa:
- "\<lbrakk>\<not> TCon ES; finite ES; distinct_equas ES; (X, rhl) \<in> ES\<rbrakk> \<Longrightarrow> \<exists> Y yrhl. (Y, yrhl) \<in> ES \<and> X \<noteq> Y"
-apply (drule not_T_atleast_2, simp)
-apply (clarsimp simp:distinct_equas_def)
-apply (drule_tac x= X in spec, drule_tac x = rhl in spec, drule_tac x = b in spec)
-by auto
-
-lemma Inv_mono_with_lambda:
- assumes Inv_ES: "Inv X ES"
- and X_noteq_Y: "X \<noteq> {[]}"
- shows "Inv X (ES - {({[]}, yrhs)})"
-proof -
- have "finite (ES - {({[]}, yrhs)})" using Inv_ES
- by (simp add:Inv_def)
- moreover have "\<exists>rhs. (X, rhs) \<in> ES - {({[]}, yrhs)}" using Inv_ES X_noteq_Y
- by (simp add:Inv_def)
- moreover have "distinct_equas (ES - {({[]}, yrhs)})" using Inv_ES X_noteq_Y
- apply (clarsimp simp:Inv_def distinct_equas_def)
- by (drule_tac x = Xa in spec, simp)
- moreover have "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>
- ardenable (X, xrhs) \<and> X \<noteq> {}" using Inv_ES
- by (clarify, simp add:Inv_def)
- moreover
- have "insert {[]} (left_eq_cls (ES - {({[]}, yrhs)})) = insert {[]} (left_eq_cls ES)"
- by (auto simp:left_eq_cls_def)
- hence "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>
- rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (ES - {({[]}, yrhs)}))"
- using Inv_ES by (auto simp:Inv_def)
- ultimately show ?thesis by (simp add:Inv_def)
-qed
-
-lemma non_empty_card_prop:
- "finite ES \<Longrightarrow> \<forall>e. e \<in> ES \<longrightarrow> card ES - Suc 0 < card ES"
-apply (erule finite.induct, simp)
-apply (case_tac[!] "a \<in> A")
-by (auto simp:insert_absorb)
-
-lemma ardenable_prop:
- assumes not_lambda: "Y \<noteq> {[]}"
- and ardable: "ardenable (Y, yrhs)"
- shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'")
-proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")
- case True
- thus ?thesis
- proof
- fix reg
- assume self_contained: "(Y, reg) \<in> yrhs"
- show ?thesis
- proof -
- have "?P (arden_variate Y reg yrhs)"
- proof -
- have "Y = L (arden_variate Y reg yrhs)"
- using self_contained not_lambda ardable
- by (rule_tac arden_variate_valid, simp_all add:ardenable_def)
- moreover have "distinct_rhs (arden_variate Y reg yrhs)"
- using ardable
- by (auto simp:distinct_rhs_def arden_variate_def seq_rhs_r_def del_x_paired_def ardenable_def)
- moreover have "rhs_eq_cls (arden_variate Y reg yrhs) = rhs_eq_cls yrhs - {Y}"
- proof -
- have "\<And> rhs r. rhs_eq_cls (seq_rhs_r rhs r) = rhs_eq_cls rhs"
- apply (auto simp:rhs_eq_cls_def seq_rhs_r_def image_def)
- by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "(x, ra)" in bexI, simp+)
- moreover have "\<And> rhs X. rhs_eq_cls (del_x_paired rhs X) = rhs_eq_cls rhs - {X}"
- by (auto simp:rhs_eq_cls_def del_x_paired_def)
- ultimately show ?thesis by (simp add:arden_variate_def)
- qed
- ultimately show ?thesis by simp
- qed
- thus ?thesis by (rule_tac x= "arden_variate Y reg yrhs" in exI, simp)
- qed
- qed
-next
- case False
- hence "(2)": "rhs_eq_cls yrhs - {Y} = rhs_eq_cls yrhs"
- by (auto simp:rhs_eq_cls_def)
- show ?thesis
- proof -
- have "?P yrhs" using False ardable "(2)"
- by (simp add:ardenable_def)
- thus ?thesis by blast
- qed
-qed
-
-lemma equas_subst_f_del_no_other:
- assumes self_contained: "(Y, rhs) \<in> ES"
- shows "\<exists> rhs'. (Y, rhs') \<in> (equas_subst_f X xrhs ` ES)" (is "\<exists> rhs'. ?P rhs'")
-proof -
- have "\<exists> rhs'. equas_subst_f X xrhs (Y, rhs) = (Y, rhs')"
- by (auto simp:equas_subst_f_def)
- then obtain rhs' where "equas_subst_f X xrhs (Y, rhs) = (Y, rhs')" by blast
- hence "?P rhs'" unfolding image_def using self_contained
- by (auto intro:bexI[where x = "(Y, rhs)"])
- thus ?thesis by blast
-qed
-
-lemma del_x_paired_del_only_x:
- "\<lbrakk>X \<noteq> Y; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> (X, rhs) \<in> del_x_paired ES Y"
-by (auto simp:del_x_paired_def)
-
-lemma equas_subst_del_no_other:
- "\<lbrakk>(X, rhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> (\<exists>rhs. (X, rhs) \<in> equas_subst ES Y rhs')"
-unfolding equas_subst_def
-apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other)
-by (erule exE, drule del_x_paired_del_only_x, auto)
-
-lemma equas_subst_holds_distinct:
- "distinct_equas ES \<Longrightarrow> distinct_equas (equas_subst ES Y rhs')"
-apply (clarsimp simp add:equas_subst_def distinct_equas_def del_x_paired_def equas_subst_f_def)
-by (auto split:if_splits)
-
-lemma del_x_paired_dels:
- "(X, rhs) \<in> ES \<Longrightarrow> {Y. Y \<in> ES \<and> fst Y = X} \<inter> ES \<noteq> {}"
-by (auto)
-
-lemma del_x_paired_subset:
- "(X, rhs) \<in> ES \<Longrightarrow> ES - {Y. Y \<in> ES \<and> fst Y = X} \<subset> ES"
-apply (drule del_x_paired_dels)
-by auto
-
-lemma del_x_paired_card_less:
- "\<lbrakk>finite ES; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> card (del_x_paired ES X) < card ES"
-apply (simp add:del_x_paired_def)
-apply (drule del_x_paired_subset)
-by (auto intro:psubset_card_mono)
-
-lemma equas_subst_card_less:
- "\<lbrakk>finite ES; (Y, yrhs) \<in> ES\<rbrakk> \<Longrightarrow> card (equas_subst ES Y rhs') < card ES"
-apply (simp add:equas_subst_def)
-apply (frule_tac h = "equas_subst_f Y rhs'" in finite_imageI)
-apply (drule_tac f = "equas_subst_f Y rhs'" in Finite_Set.card_image_le)
-apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other,erule exE)
-by (drule del_x_paired_card_less, auto)
-
-lemma equas_subst_holds_distinct_rhs:
- assumes dist': "distinct_rhs yrhs'"
- and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
- and X_in : "(X, xrhs) \<in> equas_subst ES Y yrhs'"
- shows "distinct_rhs xrhs"
-using X_in history
-apply (clarsimp simp:equas_subst_def del_x_paired_def)
-apply (drule_tac x = a in spec, drule_tac x = b in spec)
-apply (simp add:ardenable_def equas_subst_f_def)
-by (auto intro:rhs_subst_holds_distinct_rhs simp:dist' split:if_splits)
-
-lemma r_no_EMPTY_imp_seq_rhs_r_no_EMPTY:
- "[] \<notin> L r \<Longrightarrow> no_EMPTY_rhs (seq_rhs_r rhs r)"
-by (auto simp:no_EMPTY_rhs_def seq_rhs_r_def lang_seq_def)
-
-lemma del_x_paired_holds_no_EMPTY:
- "no_EMPTY_rhs yrhs \<Longrightarrow> no_EMPTY_rhs (del_x_paired yrhs Y)"
-by (auto simp:no_EMPTY_rhs_def del_x_paired_def)
-
-lemma rhs_subst_holds_no_EMPTY:
- "\<lbrakk>no_EMPTY_rhs yrhs; (Y, r) \<in> yrhs; Y \<noteq> {[]}\<rbrakk> \<Longrightarrow> no_EMPTY_rhs (rhs_subst yrhs Y rhs' r)"
-apply (auto simp:rhs_subst_def intro!:no_EMPTY_rhss_imp_merge_no_EMPTY r_no_EMPTY_imp_seq_rhs_r_no_EMPTY del_x_paired_holds_no_EMPTY)
-by (auto simp:no_EMPTY_rhs_def)
-
-lemma equas_subst_holds_no_EMPTY:
- assumes substor: "Y \<noteq> {[]}"
- and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
- and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"
- shows "no_EMPTY_rhs xrhs"
-proof-
- from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"
- by (auto simp add:equas_subst_def del_x_paired_def)
- then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"
- and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast
- hence dist_zrhs: "distinct_rhs zrhs" using history
- by (auto simp:ardenable_def)
- show ?thesis
- proof (cases "\<exists> r. (Y, r) \<in> zrhs")
- case True
- then obtain r where Y_in_zrhs: "(Y, r) \<in> zrhs" ..
- hence some: "(SOME r. (Y, r) \<in> zrhs) = r" using Z_in dist_zrhs
- by (auto simp:distinct_rhs_def)
- hence "no_EMPTY_rhs (rhs_subst zrhs Y yrhs' r)"
- using substor Y_in_zrhs history Z_in
- by (rule_tac rhs_subst_holds_no_EMPTY, auto simp:ardenable_def)
- thus ?thesis using X_Z True some
- by (simp add:equas_subst_def equas_subst_f_def)
- next
- case False
- hence "(X, xrhs) = (Z, zrhs)" using Z_in X_Z
- by (simp add:equas_subst_f_def)
- thus ?thesis using history Z_in
- by (auto simp:ardenable_def)
- qed
-qed
-
-lemma equas_subst_f_holds_left_eq_right:
- assumes substor: "Y = L rhs'"
- and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> distinct_rhs xrhs \<and> X = L xrhs"
- and subst: "(X, xrhs) = equas_subst_f Y rhs' (Z, zrhs)"
- and self_contained: "(Z, zrhs) \<in> ES"
- shows "X = L xrhs"
-proof (cases "\<exists> r. (Y, r) \<in> zrhs")
- case True
- from True obtain r where "(1)":"(Y, r) \<in> zrhs" ..
- show ?thesis
- proof -
- from history self_contained
- have dist: "distinct_rhs zrhs" by auto
- hence "(SOME r. (Y, r) \<in> zrhs) = r" using self_contained "(1)"
- using distinct_rhs_def by (auto intro:some_equality)
- moreover have "L zrhs = L (rhs_subst zrhs Y rhs' r)" using substor dist "(1)" self_contained
- by (rule_tac rhs_subst_prop1, auto simp:distinct_equas_rhs_def)
- ultimately show ?thesis using subst history self_contained
- by (auto simp:equas_subst_f_def split:if_splits)
- qed
-next
- case False
- thus ?thesis using history subst self_contained
- by (auto simp:equas_subst_f_def)
-qed
-
-lemma equas_subst_holds_left_eq_right:
- assumes history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
- and substor: "Y = L rhs'"
- and X_in : "(X, xrhs) \<in> equas_subst ES Y yrhs'"
- shows "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y rhs' \<longrightarrow> X = L xrhs"
-apply (clarsimp simp add:equas_subst_def del_x_paired_def)
-using substor
-apply (drule_tac equas_subst_f_holds_left_eq_right)
-using history
-by (auto simp:ardenable_def)
-
-lemma equas_subst_holds_ardenable:
- assumes substor: "Y = L yrhs'"
- and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
- and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"
- and dist': "distinct_rhs yrhs'"
- and not_lambda: "Y \<noteq> {[]}"
- shows "ardenable (X, xrhs)"
-proof -
- have "distinct_rhs xrhs" using history X_in dist'
- by (auto dest:equas_subst_holds_distinct_rhs)
- moreover have "no_EMPTY_rhs xrhs" using history X_in not_lambda
- by (auto intro:equas_subst_holds_no_EMPTY)
- moreover have "X = L xrhs" using history substor X_in
- by (auto dest: equas_subst_holds_left_eq_right simp del:L_rhs.simps)
- ultimately show ?thesis using ardenable_def by simp
-qed
-
-lemma equas_subst_holds_cls_defined:
- assumes X_in: "(X, xrhs) \<in> equas_subst ES Y yrhs'"
- and Inv_ES: "Inv X' ES"
- and subst: "(Y, yrhs) \<in> ES"
- and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}"
- shows "rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equas_subst ES Y yrhs'))"
-proof-
- have tac: "\<lbrakk> A \<subseteq> B; C \<subseteq> D; E \<subseteq> A \<union> B\<rbrakk> \<Longrightarrow> E \<subseteq> B \<union> D" by auto
- from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"
- by (auto simp add:equas_subst_def del_x_paired_def)
- then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"
- and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast
- hence "rhs_eq_cls zrhs \<subseteq> insert {[]} (left_eq_cls ES)" using Inv_ES
- by (auto simp:Inv_def)
- moreover have "rhs_eq_cls yrhs' \<subseteq> insert {[]} (left_eq_cls ES) - {Y}"
- using Inv_ES subst cls_holds_but_Y
- by (auto simp:Inv_def)
- moreover have "rhs_eq_cls xrhs \<subseteq> rhs_eq_cls zrhs \<union> rhs_eq_cls yrhs' - {Y}"
- using X_Z cls_holds_but_Y
- apply (clarsimp simp add:equas_subst_f_def rhs_subst_def split:if_splits)
- by (auto simp:rhs_eq_cls_def merge_rhs_def del_x_paired_def seq_rhs_r_def)
- moreover have "left_eq_cls (equas_subst ES Y yrhs') = left_eq_cls ES - {Y}" using subst
- by (auto simp: left_eq_cls_def equas_subst_def del_x_paired_def equas_subst_f_def
- dest: equas_subst_f_del_no_other
- split: if_splits)
- ultimately show ?thesis by blast
-qed
-
-lemma iteration_step:
- assumes Inv_ES: "Inv X ES"
- and not_T: "\<not> TCon ES"
- shows "(\<exists> ES'. Inv X ES' \<and> (card ES', card ES) \<in> less_than)"
-proof -
- from Inv_ES not_T have another: "\<exists>Y yrhs. (Y, yrhs) \<in> ES \<and> X \<noteq> Y" unfolding Inv_def
- by (clarify, rule_tac exist_another_equa[where X = X], auto)
- then obtain Y yrhs where subst: "(Y, yrhs) \<in> ES" and not_X: " X \<noteq> Y" by blast
- show ?thesis (is "\<exists> ES'. ?P ES'")
- proof (cases "Y = {[]}")
- case True
- --"in this situation, we pick a \"\<lambda>\" equation, thus directly remove it from the equation-system"
- have "?P (ES - {(Y, yrhs)})"
- proof
- show "Inv X (ES - {(Y, yrhs)})" using True not_X
- by (simp add:Inv_ES Inv_mono_with_lambda)
- next
- show "(card (ES - {(Y, yrhs)}), card ES) \<in> less_than" using Inv_ES subst
- by (auto elim:non_empty_card_prop[rule_format] simp:Inv_def)
- qed
- thus ?thesis by blast
- next
- case False
- --"in this situation, we pick a equation and using ardenable to get a
- rhs without itself in it, then use equas_subst to form a new equation-system"
- hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}"
- using subst Inv_ES
- by (auto intro:ardenable_prop simp add:Inv_def simp del:L_rhs.simps)
- then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'"
- and dist_Y': "distinct_rhs yrhs'"
- and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" by blast
- hence "?P (equas_subst ES Y yrhs')"
- proof -
- have finite_del: "\<And> S x. finite S \<Longrightarrow> finite (del_x_paired S x)"
- apply (rule_tac A = "del_x_paired S x" in finite_subset)
- by (auto simp:del_x_paired_def)
- have "finite (equas_subst ES Y yrhs')" using Inv_ES
- by (auto intro!:finite_del simp:equas_subst_def Inv_def)
- moreover have "\<exists>rhs. (X, rhs) \<in> equas_subst ES Y yrhs'" using Inv_ES not_X
- by (auto intro:equas_subst_del_no_other simp:Inv_def)
- moreover have "distinct_equas (equas_subst ES Y yrhs')" using Inv_ES
- by (auto intro:equas_subst_holds_distinct simp:Inv_def)
- moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow> ardenable (X, xrhs)"
- using Inv_ES dist_Y' False Y'_l_eq_r
- apply (clarsimp simp:Inv_def)
- by (rule equas_subst_holds_ardenable, simp_all)
- moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow> X \<noteq> {}" using Inv_ES
- by (clarsimp simp:equas_subst_def Inv_def del_x_paired_def equas_subst_f_def split:if_splits, auto)
- moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow>
- rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equas_subst ES Y yrhs'))"
- using Inv_ES subst cls_holds_but_Y
- apply (rule_tac impI | rule_tac allI)+
- by (erule equas_subst_holds_cls_defined, auto)
- moreover have "(card (equas_subst ES Y yrhs'), card ES) \<in> less_than"using Inv_ES subst
- by (simp add:equas_subst_card_less Inv_def)
- ultimately show "?P (equas_subst ES Y yrhs')" by (auto simp:Inv_def)
- qed
- thus ?thesis by blast
- qed
-qed
-
-text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *}
-
-lemma iteration_conc:
- assumes history: "Inv X ES"
- shows "\<exists> ES'. Inv X ES' \<and> TCon ES'" (is "\<exists> ES'. ?P ES'")
-proof (cases "TCon ES")
- case True
- hence "?P ES" using history by simp
- thus ?thesis by blast
-next
- case False
- thus ?thesis using history iteration_step
- by (rule_tac f = card in wf_iter, simp_all)
-qed
-
-lemma eqset_imp_iff': "A = B \<Longrightarrow> \<forall> x. x \<in> A \<longleftrightarrow> x \<in> B"
-apply (auto simp:mem_def)
-done
-
-lemma set_cases2:
- "\<lbrakk>(A = {} \<Longrightarrow> R A); \<And> x. (A = {x}) \<Longrightarrow> R A; \<And> x y. \<lbrakk>x \<noteq> y; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> R A\<rbrakk> \<Longrightarrow> R A"
-apply (case_tac "A = {}", simp)
-by (case_tac "\<exists> x. A = {x}", clarsimp, blast)
-
-lemma rhs_aux:"\<lbrakk>distinct_rhs rhs; {Y. \<exists>r. (Y, r) \<in> rhs} = {X}\<rbrakk> \<Longrightarrow> (\<exists>r. rhs = {(X, r)})"
-apply (rule_tac A = rhs in set_cases2, simp)
-apply (drule_tac x = X in eqset_imp_iff, clarsimp)
-apply (drule eqset_imp_iff',clarsimp)
-apply (frule_tac x = a in spec, drule_tac x = aa in spec)
-by (auto simp:distinct_rhs_def)
-
-lemma every_eqcl_has_reg:
- assumes finite_CS: "finite (UNIV Quo Lang)"
- and X_in_CS: "X \<in> (UNIV Quo Lang)"
- shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
-proof-
- have "\<exists>ES'. Inv X ES' \<and> TCon ES'" using finite_CS X_in_CS
- by (auto intro:init_ES_satisfy_Inv iteration_conc)
- then obtain ES' where Inv_ES': "Inv X ES'"
- and TCon_ES': "TCon ES'" by blast
- from Inv_ES' TCon_ES'
- have "\<exists> rhs. ES' = {(X, rhs)}"
- apply (clarsimp simp:Inv_def TCon_def)
- apply (rule_tac x = rhs in exI)
- by (auto dest!:card_Suc_Diff1 simp:card_eq_0_iff)
- then obtain rhs where ES'_single_equa: "ES' = {(X, rhs)}" ..
- hence X_ardenable: "ardenable (X, rhs)" using Inv_ES'
- by (simp add:Inv_def)
-
- from X_ardenable have X_l_eq_r: "X = L rhs"
- by (simp add:ardenable_def)
- hence rhs_not_empty: "rhs \<noteq> {}" using Inv_ES' ES'_single_equa
- by (auto simp:Inv_def ardenable_def)
- have rhs_eq_cls: "rhs_eq_cls rhs \<subseteq> {X, {[]}}"
- using Inv_ES' ES'_single_equa
- by (auto simp:Inv_def ardenable_def left_eq_cls_def)
- have X_not_empty: "X \<noteq> {}" using Inv_ES' ES'_single_equa
- by (auto simp:Inv_def)
- show ?thesis
- proof (cases "X = {[]}")
- case True
- hence "?E EMPTY" by (simp)
- thus ?thesis by blast
- next
- case False with X_ardenable
- have "\<exists> rhs'. X = L rhs' \<and> rhs_eq_cls rhs' = rhs_eq_cls rhs - {X} \<and> distinct_rhs rhs'"
- by (drule_tac ardenable_prop, auto)
- then obtain rhs' where X_eq_rhs': "X = L rhs'"
- and rhs'_eq_cls: "rhs_eq_cls rhs' = rhs_eq_cls rhs - {X}"
- and rhs'_dist : "distinct_rhs rhs'" by blast
- have "rhs_eq_cls rhs' \<subseteq> {{[]}}" using rhs_eq_cls False rhs'_eq_cls rhs_not_empty
- by blast
- hence "rhs_eq_cls rhs' = {{[]}}" using X_not_empty X_eq_rhs'
- by (auto simp:rhs_eq_cls_def)
- hence "\<exists> r. rhs' = {({[]}, r)}" using rhs'_dist
- by (auto intro:rhs_aux simp:rhs_eq_cls_def)
- then obtain r where "rhs' = {({[]}, r)}" ..
- hence "?E r" using X_eq_rhs' by (auto simp add:lang_seq_def)
- thus ?thesis by blast
- qed
-qed
-
-text {* definition of a regular language *}
-
-abbreviation
- reg :: "string set => bool"
-where
- "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)"
-
-theorem myhill_nerode:
- assumes finite_CS: "finite (UNIV Quo Lang)"
- shows "\<exists> (reg::rexp). Lang = L reg" (is "\<exists> r. ?P r")
-proof -
- have has_r_each: "\<forall>C\<in>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists>(r::rexp). C = L r" using finite_CS
- by (auto dest:every_eqcl_has_reg)
- have "\<exists> (rS::rexp set). finite rS \<and>
- (\<forall> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists> r \<in> rS. C = L r) \<and>
- (\<forall> r \<in> rS. \<exists> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. C = L r)"
- (is "\<exists> rS. ?Q rS")
- proof-
- have "\<And> C. C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<Longrightarrow> C = L (SOME (ra::rexp). C = L ra)"
- using has_r_each
- apply (erule_tac x = C in ballE, erule_tac exE)
- by (rule_tac a = r in someI2, simp+)
- hence "?Q ((\<lambda> C. SOME r. C = L r) ` {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang})" using has_r_each
- using finite_CS by auto
- thus ?thesis by blast
- qed
- then obtain rS where finite_rS : "finite rS"
- and has_r_each': "\<forall> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists> r \<in> (rS::rexp set). C = L r"
- and has_cl_each: "\<forall> r \<in> (rS::rexp set). \<exists> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. C = L r" by blast
- have "?P (folds ALT NULL rS)"
- proof
- show "Lang \<subseteq> L (folds ALT NULL rS)" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_r_each'
- apply (clarsimp simp:fold_alt_null_eqs) by blast
- next
- show "L (folds ALT NULL rS) \<subseteq> Lang" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_cl_each
- by (clarsimp simp:fold_alt_null_eqs)
- qed
- thus ?thesis by blast
-qed
-
-
-text {* tests by Christian *}
+apply (induct arbitrary:Lang rule:rexp.induct)
+apply (simp add:QUOT_def equiv_class_def equiv_str_def)
+by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star)
(* Alternative definition for Quo *)
definition