(* 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 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 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_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 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 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 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 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