(* 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+
−