1 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)

     2 theory More_Regular_Set

     3 imports "Regular_Exp" "Folds"

     4 begin

     5 

     6 text {* Some properties of operator @{text "@@"}. *}

     7 

     8 notation 

     9   conc (infixr "\<cdot>" 100) and

    10   star ("_\<star>" [101] 102)

    11 

    12 lemma conc_add_left:

    13   assumes a: "A = B"

    14   shows "C \<cdot> A = C \<cdot> B"

    15 using a by simp

    16 

    17 lemma star_cases:

    18   shows "A\<star> =  {[]} \<union> A \<cdot> A\<star>"

    19 proof

    20   { fix x

    21     have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A \<cdot> A\<star>"

    22       unfolding conc_def

    23     by (induct rule: star_induct) (auto)

    24   }

    25   then show "A\<star> \<subseteq> {[]} \<union> A \<cdot> A\<star>" by auto

    26 next

    27   show "{[]} \<union> A \<cdot> A\<star> \<subseteq> A\<star>"

    28     unfolding conc_def by auto

    29 qed

    30 

    31 lemma star_decom: 

    32   assumes a: "x \<in> A\<star>" "x \<noteq> []"

    33   shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"

    34 using a

    35 by (induct rule: star_induct) (blast)+

    36 

    37 lemma seq_pow_comm:

    38   shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A"

    39 by (induct n) (simp_all add: conc_assoc[symmetric])

    40 

    41 lemma seq_star_comm:

    42   shows "A \<cdot> A\<star> = A\<star> \<cdot> A"

    43 unfolding star_def seq_pow_comm conc_UNION_distrib

    44 by simp

    45 

    46 

    47 text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}

    48 

    49 lemma pow_length:

    50   assumes a: "[] \<notin> A"

    51   and     b: "s \<in> A ^^ Suc n"

    52   shows "n < length s"

    53 using b

    54 proof (induct n arbitrary: s)

    55   case 0

    56   have "s \<in> A ^^ Suc 0" by fact

    57   with a have "s \<noteq> []" by auto

    58   then show "0 < length s" by auto

    59 next

    60   case (Suc n)

    61   have ih: "\<And>s. s \<in> A ^^ Suc n \<Longrightarrow> n < length s" by fact

    62   have "s \<in> A ^^ Suc (Suc n)" by fact

    63   then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A ^^ Suc n"

    64     by (auto simp add: conc_def)

    65   from ih ** have "n < length s2" by simp

    66   moreover have "0 < length s1" using * a by auto

    67   ultimately show "Suc n < length s" unfolding eq 

    68     by (simp only: length_append)

    69 qed

    70 

    71 lemma seq_pow_length:

    72   assumes a: "[] \<notin> A"

    73   and     b: "s \<in> B \<cdot> (A ^^ Suc n)"

    74   shows "n < length s"

    75 proof -

    76   from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n"

    77     unfolding Seq_def by auto

    78   from * have " n < length s2" by (rule pow_length[OF a])

    79   then show "n < length s" using eq by simp

    80 qed

    81 

    82 

    83 section {* A modified version of Arden's lemma *}

    84 

    85 text {*  A helper lemma for Arden *}

    86 

    87 lemma arden_helper:

    88   assumes eq: "X = X \<cdot> A \<union> B"

    89   shows "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))"

    90 proof (induct n)

    91   case 0 

    92   show "X = X \<cdot> (A ^^ Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B \<cdot> (A ^^ m))"

    93     using eq by simp

    94 next

    95   case (Suc n)

    96   have ih: "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" by fact

    97   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

    98   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))"

    99     by (simp add: conc_Un_distrib conc_assoc)

   100   also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))"

   101     by (auto simp add: le_Suc_eq)

   102   finally show "X = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))" .

   103 qed

   104 

   105 theorem arden:

   106   assumes nemp: "[] \<notin> A"

   107   shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>"

   108 proof

   109   assume eq: "X = B \<cdot> A\<star>"

   110   have "A\<star> = {[]} \<union> A\<star> \<cdot> A" 

   111     unfolding seq_star_comm[symmetric]

   112     by (rule star_cases)

   113   then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"

   114     by (rule conc_add_left)

   115   also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)"

   116     unfolding conc_Un_distrib by simp

   117   also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A" 

   118     by (simp only: conc_assoc)

   119   finally show "X = X \<cdot> A \<union> B" 

   120     using eq by blast 

   121 next

   122   assume eq: "X = X \<cdot> A \<union> B"

   123   { fix n::nat

   124     have "B \<cdot> (A ^^ n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }

   125   then have "B \<cdot> A\<star> \<subseteq> X" 

   126     unfolding conc_def star_def UNION_def by auto

   127   moreover

   128   { fix s::"'a list"

   129     obtain k where "k = length s" by auto

   130     then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)" 

   131       using seq_pow_length[OF nemp] by blast

   132     assume "s \<in> X"

   133     then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))"

   134       using arden_helper[OF eq, of "k"] by auto

   135     then have "s \<in> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using not_in by auto

   136     moreover

   137     have "(\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m)) \<subseteq> (\<Union>n. B \<cdot> (A ^^ n))" by auto

   138     ultimately 

   139     have "s \<in> B \<cdot> A\<star>" 

   140       unfolding conc_Un_distrib star_def by auto }

   141   then have "X \<subseteq> B \<cdot> A\<star>" by auto

   142   ultimately 

   143   show "X = B \<cdot> A\<star>" by simp

   144 qed

   145 

   146 

   147 text {* Plus-combination for a set of regular expressions *}

   148 

   149 abbreviation

   150   Setalt  ("\<Uplus>_" [1000] 999) 

   151 where

   152   "\<Uplus>A \<equiv> folds Plus Zero A"

   153 

   154 text {* 

   155   For finite sets, @{term Setalt} is preserved under @{term lang}.

   156 *}

   157 

   158 lemma folds_alt_simp [simp]:

   159   fixes rs::"('a rexp) set"

   160   assumes a: "finite rs"

   161   shows "lang (\<Uplus>rs) = \<Union> (lang ` rs)"

   162 unfolding folds_def

   163 apply(rule set_eqI)

   164 apply(rule someI2_ex)

   165 apply(rule_tac finite_imp_fold_graph[OF a])

   166 apply(erule fold_graph.induct)

   167 apply(auto)

   168 done

   169 

   170 end