--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/My.thy Wed Nov 10 11:59:29 2010 +0000
@@ -0,0 +1,320 @@
+theory My
+imports Main
+begin
+
+
+definition
+ lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
+where
+ "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+
+inductive_set
+ 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>"
+
+
+datatype rexp =
+ NULL
+| EMPTY
+| CHAR char
+| SEQ rexp rexp
+| ALT rexp rexp
+| STAR rexp
+
+fun
+ L_rexp :: "rexp \<Rightarrow> string set"
+where
+ "L_rexp (NULL) = {}"
+ | "L_rexp (EMPTY) = {[]}"
+ | "L_rexp (CHAR c) = {[c]}"
+ | "L_rexp (SEQ r1 r2) = (L_rexp r1) ; (L_rexp r2)"
+ | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
+ | "L_rexp (STAR r) = (L_rexp r)\<star>"
+
+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]:
+ "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L_rexp 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_simp_empty [simp]:
+ "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L_rexp r) \<or> x = [])"
+apply (simp add: folds_def)
+apply (rule someI2_ex)
+apply (erule finite_imp_fold_graph)
+apply (erule fold_graph.induct)
+apply (auto)
+done
+
+lemma [simp]:
+ "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
+by simp
+
+definition
+ str_eq ("_ \<approx>_ _")
+where
+ "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
+
+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 -
+ have "Lang \<subseteq> \<Union> {X. final X Lang}"
+ unfolding final_def
+ unfolding quotient_def Image_def
+ unfolding str_eq_rel_def
+ apply(simp)
+ apply(auto)
+ apply(rule_tac x="(\<approx>Lang) `` {x}" in exI)
+ unfolding Image_def
+ unfolding str_eq_rel_def
+ apply(auto)
+ unfolding str_eq_def
+ apply(auto)
+ apply(drule_tac x="[]" in spec)
+ apply(simp)
+ done
+ moreover
+ have "\<Union>{X. final X Lang} \<subseteq> Lang"
+ unfolding final_def by auto
+ ultimately
+ show "Lang = \<Union> {X. final X Lang}"
+ by blast
+qed
+
+lemma all_rexp:
+ "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r"
+sorry
+
+lemma final_rexp:
+ "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r"
+unfolding final_def
+using all_rexp by blast
+
+lemma finite_f_one_to_one:
+ assumes "finite B"
+ and "\<forall>x \<in> B. \<exists>y. f y = x"
+ shows "\<exists>rs. finite rs \<and> (B = {f y | y . y \<in> rs})"
+using assms
+by (induct) (auto)
+
+lemma finite_final:
+ assumes "finite (UNIV // (\<approx>Lang))"
+ shows "finite {X. final X Lang}"
+using assms
+proof -
+ have "{X. final X Lang} \<subseteq> (UNIV // (\<approx>Lang))"
+ unfolding final_def by auto
+ with assms show "finite {X. final X Lang}"
+ using finite_subset by auto
+qed
+
+lemma finite_regular_aux:
+ fixes Lang :: "string set"
+ assumes "finite (UNIV // (\<approx>Lang))"
+ shows "\<exists>rs. Lang = L_rexp (folds ALT NULL rs)"
+apply(subst lang_is_union_of_finals)
+using assms
+apply -
+apply(drule finite_final)
+apply(drule_tac f="L_rexp" in finite_f_one_to_one)
+apply(clarify)
+apply(drule final_rexp[OF assms])
+apply(auto)[1]
+apply(clarify)
+apply(rule_tac x="rs" in exI)
+apply(simp)
+apply(rule set_eqI)
+apply(auto)
+done
+
+lemma finite_regular:
+ fixes Lang :: "string set"
+ assumes "finite (UNIV // (\<approx>Lang))"
+ shows "\<exists>r. Lang = L_rexp r"
+using assms finite_regular_aux
+by auto
+
+
+
+section {* other direction *}
+
+
+lemma inj_image_lang:
+ fixes f::"string \<Rightarrow> 'a"
+ assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y"
+ shows "inj_on (image f) (UNIV // (\<approx>Lang))"
+proof -
+ { fix x y::string
+ assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}"
+ moreover
+ have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto
+ ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast
+ then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto
+ then have "x \<approx>Lang y" unfolding str_eq_def by simp
+ then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp
+ }
+ then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y"
+ unfolding quotient_def Image_def str_eq_rel_def by simp
+ then show "inj_on (image f) (UNIV // (\<approx>Lang))"
+ unfolding inj_on_def by simp
+qed
+
+
+lemma finite_range_image:
+ assumes fin: "finite (range f)"
+ shows "finite ((image f) ` X)"
+proof -
+ from fin have "finite (Pow (f ` UNIV))" by auto
+ moreover
+ have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto
+ ultimately show "finite ((image f) ` X)" using finite_subset by auto
+qed
+
+definition
+ tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
+where
+ "tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
+
+lemma tag1_range_finite:
+ assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)"
+ and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
+ shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
+proof -
+ have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto
+ moreover
+ have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)"
+ unfolding tag1_def quotient_def by auto
+ ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
+ using finite_subset by blast
+qed
+
+lemma tag1_inj:
+ "tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
+unfolding tag1_def Image_def str_eq_rel_def str_eq_def
+by auto
+
+lemma quot_alt_cu:
+ fixes L\<^isub>1 L\<^isub>2::"string set"
+ assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)"
+ and fin2: "finite (UNIV // \<approx>L\<^isub>2)"
+ shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
+proof -
+ have "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
+ using fin1 fin2 tag1_range_finite by simp
+ then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))"
+ using finite_range_image by blast
+ moreover
+ have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
+ using tag1_inj by simp
+ then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
+ using inj_image_lang by blast
+ ultimately
+ show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
+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}"
+
+definition
+ transitions_rexp ("_ \<turnstile>\<rightarrow> _")
+where
+ "Y \<turnstile>\<rightarrow> X \<equiv> if [] \<in> X then folds ALT EMPTY (Y \<Turnstile>\<Rightarrow>X) else folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"
+
+definition
+ "rhs CS X \<equiv> if X = {[]} then {({[]}, EMPTY)} else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"
+
+definition
+ "rhs_sem CS X \<equiv> \<Union> {(Y; L_rexp r) | Y r . (Y, r) \<in> rhs CS X}"
+
+definition
+ "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"
+
+definition
+ "eqs_sem CS \<equiv> (\<Union>X \<in> CS. {(X, rhs_sem 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
+
+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 lang_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
+ moreover
+ have "True" by simp (* FIXME *)
+ note that
+ ultimately show thesis by blast
+qed
+
+lemma test:
+ assumes "[] \<in> X"
+ shows "[] \<in> L_rexp (Y \<turnstile>\<rightarrow> X)"
+using assms
+by (simp add: transitions_rexp_def)
+
+lemma rhs_sem:
+ assumes "X \<in> (UNIV // (\<approx>Lang))"
+ shows "X \<subseteq> rhs_sem (UNIV // (\<approx>Lang)) X"
+apply(case_tac "X = {[]}")
+apply(simp)
+apply(simp add: rhs_sem_def rhs_def lang_seq_def)
+apply(rule subsetI)
+apply(case_tac "x = []")
+apply(simp add: rhs_sem_def rhs_def)
+apply(rule_tac x = "X" in exI)
+apply(simp)
+apply(rule_tac x = "X" in exI)
+apply(simp add: assms)
+apply(simp add: transitions_rexp_def)
+oops
\ No newline at end of file