theory Myimports Main Infinite_Setbegindefinition 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>"lemma lang_star_cases: shows "L\<star> = {[]} \<union> L ;; L\<star>"unfolding Seq_defby (auto) (metis Star.simps)lemma lang_star_cases2: shows "L ;; L\<star> = L\<star> ;; L"sorrytheorem ardens_revised: assumes nemp: "[] \<notin> A" shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"proof assume eq: "X = B ;; A\<star>" have "A\<star> = {[]} \<union> A\<star> ;; A" sorry then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" unfolding Seq_def by simp also have "\<dots> = B \<union> B ;; (A\<star> ;; A)" unfolding Seq_def by auto also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" unfolding Seq_def by (auto) (metis append_assoc)+ finally show "X = X ;; A \<union> B" using eq by autonext assume "X = X ;; A \<union> B" then have "B \<subseteq> X" "X ;; A \<subseteq> X" by auto show "X = B ;; A\<star>" sorryqeddatatype rexp = NULL| EMPTY| CHAR char| SEQ rexp rexp| ALT rexp rexp| STAR rexpfun Sem :: "rexp \<Rightarrow> string set" ("\<lparr>_\<rparr>" [0] 1000)where "\<lparr>NULL\<rparr> = {}" | "\<lparr>EMPTY\<rparr> = {[]}" | "\<lparr>CHAR c\<rparr> = {[c]}" | "\<lparr>SEQ r1 r2\<rparr> = \<lparr>r1\<rparr> ;; \<lparr>r2\<rparr>" | "\<lparr>ALT r1 r2\<rparr> = \<lparr>r1\<rparr> \<union> \<lparr>r2\<rparr>" | "\<lparr>STAR r\<rparr> = \<lparr>r\<rparr>\<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> \<lparr>folds ALT NULL rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>)"apply (simp add: folds_def)apply (rule someI2_ex)apply (erule finite_imp_fold_graph)apply (erule fold_graph.induct)apply (auto)donelemma folds_simp_empty [simp]: "finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT EMPTY rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>) \<or> x = []"apply (simp add: folds_def)apply (rule someI2_ex)apply (erule finite_imp_fold_graph)apply (erule fold_graph.induct)apply (auto)donelemma [simp]: shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"by simpdefinition 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 blastqedlemma all_rexp: "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"sorrylemma final_rexp: "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"unfolding final_defusing all_rexp by blastlemma 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 assmsby (induct) (auto)lemma finite_final: assumes "finite (UNIV // (\<approx>Lang))" shows "finite {X. final X Lang}"using assmsproof - 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 autoqedlemma finite_regular_aux: fixes Lang :: "string set" assumes "finite (UNIV // (\<approx>Lang))" shows "\<exists>rs. Lang = \<lparr>folds ALT NULL rs\<rparr>"apply(subst lang_is_union_of_finals)using assmsapply -apply(drule finite_final)apply(drule_tac f="Sem" 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)donelemma finite_regular: fixes Lang :: "string set" assumes "finite (UNIV // (\<approx>Lang))" shows "\<exists>r. Lang = \<lparr>r\<rparr>"using assms finite_regular_auxby autosection {* 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 simpqedlemma 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 autoqeddefinition 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 blastqedlemma 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_defby autolemma 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)qedsection {* 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;; \<lparr>r\<rparr>) | 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_defby autolemma defined_by_str: assumes "s \<in> X" and "X \<in> UNIV // (\<approx>Lang)" shows "X = (\<approx>Lang) `` {s}"using assmsunfolding quotient_def Image_defunfolding str_eq_rel_def str_eq_defby autolemma 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 (*moreover have "True" by simp FIXME *) ultimately show thesis by (blast intro: that)qedlemma test: assumes "[] \<in> X" shows "[] \<in> \<lparr>Y \<turnstile>\<rightarrow> X\<rparr>"using assmsby (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 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(*fun power :: "string \<Rightarrow> nat \<Rightarrow> string" (infixr "\<Up>" 100)where "s \<Up> 0 = s"| "s \<Up> (Suc n) = s @ (s \<Up> n)"definition "Lone = {(''0'' \<Up> n) @ (''1'' \<Up> n) | n. True }"lemma "infinite (UNIV // (\<approx>Lone))"unfolding infinite_iff_countable_subsetapply(rule_tac x="\<lambda>n. {(''0'' \<Up> n) @ (''1'' \<Up> i) | i. i \<in> {..n} }" in exI)apply(auto)prefer 2unfolding Lone_defunfolding quotient_defunfolding Image_defapply(simp)unfolding str_eq_rel_defunfolding str_eq_defapply(auto)apply(rule_tac x="''0'' \<Up> n" in exI)apply(auto)unfolding infinite_nat_iff_unboundedunfolding Lone_def*)text {* Derivatives *}definition DERS :: "string \<Rightarrow> string set \<Rightarrow> string set"where "DERS s L \<equiv> {s'. s @ s' \<in> L}"lemma shows "x \<approx>L y \<longleftrightarrow> DERS x L = DERS y L"unfolding DERS_def str_eq_defby auto