regexp: comparison Myhill.thy

equal deleted inserted replaced

-:90a57a533b0c
+:cef2893f353b
 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
 for L :: "string set"
 where
 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>)"
 proof
 definition
 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
 where
 "folds f z S \<equiv> SOME x. fold_graph f z S x"
-lemma folds_simp_null [simp]:
+lemma folds_alt_simp [simp]:
-"finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> L r)"
+"finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply (simp add: folds_def)
+apply (rule set_ext, simp add:folds_def)
-apply (rule someI2_ex)
+apply (rule someI2_ex, erule finite_imp_fold_graph)
-apply (erule finite_imp_fold_graph)
+by (erule fold_graph.induct, auto)
-apply (erule fold_graph.induct)
-apply (auto)
-done
 lemma [simp]:
 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 by simp
 definition
 str_eq_rel ("\<approx>_")
 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 *}
+datatype rhs_item =
+Lam "rexp"                           (* Lambda *)
+| Trn "string set" "rexp"              (* Transition *)
+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"
+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:: rhs_item set \<Rightarrow> string set"
+begin
+fun L_rhs:: "rhs_item set \<Rightarrow> string set"
+where
+"L_rhs rhs = \<Union> (L ` rhs)"
+end
 definition
-transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
+"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}"
+definition
+"eqs CS \<equiv> {(X, init_rhs CS X)|X.  X \<in> CS}"
+(************ arden's lemma variation ********************)
+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
+"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)"
+fun attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
 where
-"Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"
+"attach_rexp r' (Lam r)   = Lam (SEQ r r')"
+| "attach_rexp r' (Trn X r) = Trn X (SEQ r r')"
 definition
-transitions_rexp ("_ \<turnstile>\<rightarrow> _")
+"append_rhs_rexp rhs r \<equiv> (attach_rexp r) ` rhs"
-where
-"Y \<turnstile>\<rightarrow> X \<equiv> folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"
-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 \<equiv> "L:: (string set \<times> rexp) set \<Rightarrow> string set"
-begin
-fun L_rhs:: "(string set \<times> rexp) set \<Rightarrow> string set"
-where
-"L_rhs rhs = \<Union> {(Y;; L r) | Y r . (Y, r) \<in> 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
-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
-(************ arden's lemma variation ********************)
 definition
-"rexp_of rhs X \<equiv> folds ALT NULL {r. (X, r) \<in> rhs}"
+"arden_variate X rhs \<equiv> append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"
-definition
-"arden_variate X rhs \<equiv> {(Y, SEQ r (STAR (rexp_of rhs X)))| Y r. (Y, r) \<in> rhs \<and> Y \<noteq> X}"
-(************* rhs/equations property **************)
-definition
-"distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
 (*********** 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>
+"rhs_subst rhs X xrhs \<equiv> (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"
-{(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}"
 definition
 "eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 text {*
 Inv: Invairance of the equation-system, during the decrease of the equation-system, Inv holds.
 *}
 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
+"finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"
 definition
-"self_contained ES \<equiv> \<forall> X xrhs. (X, xrhs) \<in> ES
+"classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"
-\<longrightarrow> (\<forall> Y r.(Y, r) \<in> xrhs \<and> Y \<noteq> {[]} \<longrightarrow> (\<exists> yrhs. (Y, yrhs) \<in> ES))"
+definition
+"lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
 definition
-"Inv ES \<equiv> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> non_empty ES \<and> self_contained ES"
+"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
 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')"
 from pe' show "P e'" .
 qed
 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-
+by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps)
-have "\<And> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<Longrightarrow> ([] \<notin> L (rexp_of rhs X))"
+moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))"
-proof
+using l_eq_r_in_eqs by (simp add:valid_eqns_def)
-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
 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 ***** *}
+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: "(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"
-and    not_T: "card ES > 1"
+shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1" (is "\<exists> ES'. ?P ES'")
-shows "(\<exists> ES' xrhs'. Inv ES' \<and> (card ES', card ES) \<in> less_than \<and> (X, xrhs') \<in> ES')"
+proof (cases "card ES = 1")
-proof -
-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
+thus ?thesis using history X_in_ES
-by (simp add:equations_def equation_rhs_def lang_seq_def)
+by blast
-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
+thus ?thesis using history iteration_step X_in_ES
-by (rule_tac f = card in wf_iter, simp_all)
+by (rule_tac f = card in wf_iter, auto)
 qed
-lemma eqset_imp_iff': "A = B \<Longrightarrow> \<forall> x. x \<in> A \<longleftrightarrow> x \<in> B"
+lemma last_cl_exists_rexp:
-apply (auto simp:mem_def)
+assumes ES_single: "ES = {(X, xrhs)}"
-done
+and Inv_ES: "Inv ES"
+shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
-lemma set_cases2:
+proof-
-"\<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"
+let ?A = "arden_variate X xrhs"
-apply (case_tac "A = {}", simp)
+have "?P (rexp_of_lam ?A)"
-by (case_tac "\<exists> x. A = {x}", clarsimp, blast)
+proof -
+have "L (rexp_of_lam ?A) = L (lam_of ?A)"
-lemma rhs_aux:"\<lbrakk>distinct_rhs rhs; {Y. \<exists>r. (Y, r) \<in> rhs} = {X}\<rbrakk> \<Longrightarrow> (\<exists>r. rhs = {(X, r)})"
+proof(rule rexp_of_lam_eq_lam_set)
-apply (rule_tac A = rhs in set_cases2, simp)
+show "finite (arden_variate X xrhs)" using Inv_ES ES_single
-apply (drule_tac x = X in eqset_imp_iff, clarsimp)
+by (rule_tac arden_variate_keeps_finite, auto simp add:Inv_def finite_rhs_def)
-apply (drule eqset_imp_iff',clarsimp)
+qed
-apply (frule_tac x = a in spec, drule_tac x = aa in spec)
+also have "\<dots> = L ?A"
-by (auto simp:distinct_rhs_def)
+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 Quo Lang)"
+assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
-and X_in_CS: "X \<in> (UNIV Quo Lang)"
+and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))"
 shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
-proof-
+proof -
-have "\<exists>ES'. Inv X ES' \<and> TCon ES'" using finite_CS X_in_CS
+from X_in_CS have "\<exists> xrhs. (X, xrhs) \<in> (eqs (UNIV  // (\<approx>Lang)))"
-by (auto intro:init_ES_satisfy_Inv iteration_conc)
+by (auto simp:eqs_def init_rhs_def)
-then obtain ES' where Inv_ES': "Inv X ES'"
+then obtain ES xrhs where Inv_ES: "Inv ES"
-and  TCon_ES': "TCon ES'" by blast
+and X_in_ES: "(X, xrhs) \<in> ES"
-from Inv_ES' TCon_ES'
+and card_ES: "card ES = 1"
-have "\<exists> rhs. ES' = {(X, rhs)}"
+using finite_CS X_in_CS init_ES_satisfy_Inv iteration_conc
-apply (clarsimp simp:Inv_def TCon_def)
+by blast
-apply (rule_tac x = rhs in exI)
+hence ES_single_equa: "ES = {(X, xrhs)}"
-by (auto dest!:card_Suc_Diff1 simp:card_eq_0_iff)
+by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff)
-then obtain rhs where ES'_single_equa: "ES' = {(X, rhs)}" ..
+thus ?thesis using Inv_ES
-hence X_ardenable: "ardenable (X, rhs)" using Inv_ES'
+by (rule last_cl_exists_rexp)
-by (simp add:Inv_def)
+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
-from X_ardenable have X_l_eq_r: "X = L rhs"
+hence "False"
-by (simp add:ardenable_def)
+apply (simp add:quotient_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, {[]}}"
+lemma other_direction:
-using Inv_ES' ES'_single_equa
+"Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))"
-by (auto simp:Inv_def ardenable_def left_eq_cls_def)
+proof (induct arbitrary:Lang rule:rexp.induct)
-have X_not_empty: "X \<noteq> {}" using Inv_ES' ES'_single_equa
+case NULL
-by (auto simp:Inv_def)
+have "UNIV // (\<approx>{}) \<subseteq> {UNIV} "
-show ?thesis
+by (auto simp:quotient_def str_eq_rel_def str_eq_def)
-proof (cases "X = {[]}")
+with prems show "?case" by (auto intro:finite_subset)
-case True
+next
-hence "?E EMPTY" by (simp)
+case EMPTY
-thus ?thesis by blast
+have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
-next
+sorry
-case False with  X_ardenable
+with prems show ?case by (auto intro:finite_subset)
-have "\<exists> rhs'. X = L rhs' \<and> rhs_eq_cls rhs' = rhs_eq_cls rhs - {X} \<and> distinct_rhs rhs'"
+next
-by (drule_tac ardenable_prop, auto)
+case (CHAR c)
-then obtain rhs' where X_eq_rhs': "X = L rhs'"
+have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
-and rhs'_eq_cls: "rhs_eq_cls rhs' = rhs_eq_cls rhs - {X}"
+sorry
-and rhs'_dist : "distinct_rhs rhs'" by blast
+with prems show ?case by (auto intro:finite_subset)
-have "rhs_eq_cls rhs' \<subseteq> {{[]}}" using rhs_eq_cls False rhs'_eq_cls rhs_not_empty
+next
-by blast
+case (SEQ r1 r2)
-hence "rhs_eq_cls rhs' = {{[]}}" using X_not_empty X_eq_rhs'
+show ?case sorry
-by (auto simp:rhs_eq_cls_def)
+next
-hence "\<exists> r. rhs' = {({[]}, r)}" using rhs'_dist
+case (ALT r1 r1)
-by (auto intro:rhs_aux simp:rhs_eq_cls_def)
+show ?case sorry
-then obtain r where "rhs' = {({[]}, r)}" ..
+next
-hence "?E r" using X_eq_rhs' by (auto simp add:lang_seq_def)
+case (STAR r)
-thus ?thesis by blast
+show ?case sorry
 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)"
+apply (induct arbitrary:Lang rule:rexp.induct)
-using has_r_each
+apply (simp add:QUOT_def equiv_class_def equiv_str_def)
-apply (erule_tac x = C in ballE, erule_tac exE)
+by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star)
-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 *}
 (* Alternative definition for Quo *)
 definition
 QUOT :: "string set \<Rightarrow> (string set) set"
 where

changeset 28	cef2893f353b
parent 27	90a57a533b0c
child 29	c64241fa4dff