(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)theory More_Regular_Setimports "Regular_Exp" "Folds"begintext {* Some properties of operator @{text "@@"}. *}notation conc (infixr "\<cdot>" 100) and star ("_\<star>" [101] 102)lemma star_decom: assumes a: "x \<in> A\<star>" "x \<noteq> []" shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"using aby (induct rule: star_induct) (blast)+lemma conc_pow_comm: shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A"by (induct n) (simp_all add: conc_assoc[symmetric])lemma conc_star_comm: shows "A \<cdot> A\<star> = A\<star> \<cdot> A"unfolding star_def conc_pow_comm conc_UNION_distribby simptext {* Two lemmas about the length of strings in @{text "A \<up> n"} *}lemma pow_length: assumes a: "[] \<notin> A" and b: "s \<in> A ^^ Suc n" shows "n < length s"using bproof (induct n arbitrary: s) case 0 have "s \<in> A ^^ Suc 0" by fact with a have "s \<noteq> []" by auto then show "0 < length s" by autonext case (Suc n) have ih: "\<And>s. s \<in> A ^^ Suc n \<Longrightarrow> n < length s" by fact have "s \<in> A ^^ Suc (Suc n)" by fact then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A ^^ Suc n" by (auto simp add: conc_def) from ih ** have "n < length s2" by simp moreover have "0 < length s1" using * a by auto ultimately show "Suc n < length s" unfolding eq by (simp only: length_append)qedlemma conc_pow_length: assumes a: "[] \<notin> A" and b: "s \<in> B \<cdot> (A ^^ Suc n)" shows "n < length s"proof - from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n" by auto from * have " n < length s2" by (rule pow_length[OF a]) then show "n < length s" using eq by simpqedsection {* A modified version of Arden's lemma *}text {* A helper lemma for Arden *}lemma arden_helper: assumes eq: "X = X \<cdot> A \<union> B" shows "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))"proof (induct n) case 0 show "X = X \<cdot> (A ^^ Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B \<cdot> (A ^^ m))" using eq by simpnext case (Suc n) have ih: "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" by fact also have "\<dots> = (X \<cdot> A \<union> B) \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" using eq by simp also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (B \<cdot> (A ^^ Suc n)) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" by (simp add: conc_Un_distrib conc_assoc) also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))" by (auto simp add: le_Suc_eq) finally show "X = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))" .qedtheorem arden: assumes nemp: "[] \<notin> A" shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>"proof assume eq: "X = B \<cdot> A\<star>" have "A\<star> = {[]} \<union> A\<star> \<cdot> A" unfolding conc_star_comm[symmetric] by(metis Un_commute star_unfold_left) then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)" by metis also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)" unfolding conc_Un_distrib by simp also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A" by (simp only: conc_assoc) finally show "X = X \<cdot> A \<union> B" using eq by blast next assume eq: "X = X \<cdot> A \<union> B" { fix n::nat have "B \<cdot> (A ^^ n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto } then have "B \<cdot> A\<star> \<subseteq> X" unfolding conc_def star_def UNION_def by auto moreover { fix s::"'a list" obtain k where "k = length s" by auto then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)" using conc_pow_length[OF nemp] by blast assume "s \<in> X" then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using arden_helper[OF eq, of "k"] by auto then have "s \<in> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using not_in by auto moreover have "(\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m)) \<subseteq> (\<Union>n. B \<cdot> (A ^^ n))" by auto ultimately have "s \<in> B \<cdot> A\<star>" unfolding conc_Un_distrib star_def by auto } then have "X \<subseteq> B \<cdot> A\<star>" by auto ultimately show "X = B \<cdot> A\<star>" by simpqedtext {* Plus-combination for a set of regular expressions *}abbreviation Setalt ("\<Uplus>_" [1000] 999) where "\<Uplus>A \<equiv> folds Plus Zero A"text {* For finite sets, @{term Setalt} is preserved under @{term lang}.*}lemma folds_alt_simp [simp]: fixes rs::"('a rexp) set" assumes a: "finite rs" shows "lang (\<Uplus>rs) = \<Union> (lang ` rs)"unfolding folds_defapply(rule set_eqI)apply(rule someI2_ex)apply(rule_tac finite_imp_fold_graph[OF a])apply(erule fold_graph.induct)apply(auto)doneend