diff -r b794db0b79db -r b1258b7d2789 More_Regular_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/More_Regular_Set.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -0,0 +1,170 @@
+(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
+theory More_Regular_Set
+imports "Regular_Exp" "Folds"
+begin
+
+text {* Some properties of operator @{text "@@"}. *}
+
+notation 
+  conc (infixr "\<cdot>" 100) and
+  star ("_\<star>" [101] 102)
+
+lemma conc_add_left:
+  assumes a: "A = B"
+  shows "C \<cdot> A = C \<cdot> B"
+using a by simp
+
+lemma star_cases:
+  shows "A\<star> =  {[]} \<union> A \<cdot> A\<star>"
+proof
+  { fix x
+    have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A \<cdot> A\<star>"
+      unfolding conc_def
+    by (induct rule: star_induct) (auto)
+  }
+  then show "A\<star> \<subseteq> {[]} \<union> A \<cdot> A\<star>" by auto
+next
+  show "{[]} \<union> A \<cdot> A\<star> \<subseteq> A\<star>"
+    unfolding conc_def by auto
+qed
+
+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 a
+by (induct rule: star_induct) (blast)+
+
+lemma seq_pow_comm:
+  shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A"
+by (induct n) (simp_all add: conc_assoc[symmetric])
+
+lemma seq_star_comm:
+  shows "A \<cdot> A\<star> = A\<star> \<cdot> A"
+unfolding star_def seq_pow_comm conc_UNION_distrib
+by simp
+
+
+text {* 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 b
+proof (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 auto
+next
+  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)
+qed
+
+lemma seq_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"
+    unfolding Seq_def by auto
+  from * have " n < length s2" by (rule pow_length[OF a])
+  then show "n < length s" using eq by simp
+qed
+
+
+section {* 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 simp
+next
+  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))" .
+qed
+
+theorem 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 seq_star_comm[symmetric]
+    by (rule star_cases)
+  then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"
+    by (rule conc_add_left)
+  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 seq_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 simp
+qed
+
+
+text {* 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_def
+apply(rule set_eqI)
+apply(rule someI2_ex)
+apply(rule_tac finite_imp_fold_graph[OF a])
+apply(erule fold_graph.induct)
+apply(auto)
+done
+
+end
\ No newline at end of file