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

     2 theory Regular

     3 imports Main Folds

     4 begin

     5 

     6 section {* Preliminary definitions *}

     7 

     8 type_synonym lang = "string set"

     9 

    10 

    11 text {*  Sequential composition of two languages *}

    12 

    13 definition 

    14   Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr "\<cdot>" 100)

    15 where 

    16   "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"

    17 

    18 

    19 text {* Some properties of operator @{text "\<cdot>"}. *}

    20 

    21 lemma seq_add_left:

    22   assumes a: "A = B"

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

    24 using a by simp

    25 

    26 lemma seq_union_distrib_right:

    27   shows "(A \<union> B) \<cdot> C = (A \<cdot> C) \<union> (B \<cdot> C)"

    28 unfolding Seq_def by auto

    29 

    30 lemma seq_union_distrib_left:

    31   shows "C \<cdot> (A \<union> B) = (C \<cdot> A) \<union> (C \<cdot> B)"

    32 unfolding Seq_def by  auto

    33 

    34 lemma seq_intro:

    35   assumes a: "x \<in> A" "y \<in> B"

    36   shows "x @ y \<in> A \<cdot> B "

    37 using a by (auto simp: Seq_def)

    38 

    39 lemma seq_assoc:

    40   shows "(A \<cdot> B) \<cdot> C = A \<cdot> (B \<cdot> C)"

    41 unfolding Seq_def

    42 apply(auto)

    43 apply(blast)

    44 by (metis append_assoc)

    45 

    46 lemma seq_empty [simp]:

    47   shows "A \<cdot> {[]} = A"

    48   and   "{[]} \<cdot> A = A"

    49 by (simp_all add: Seq_def)

    50 

    51 lemma seq_null [simp]:

    52   shows "A \<cdot> {} = {}"

    53   and   "{} \<cdot> A = {}"

    54 by (simp_all add: Seq_def)

    55 

    56 

    57 text {* Power and Star of a language *}

    58 

    59 fun 

    60   pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)

    61 where

    62   "A \<up> 0 = {[]}"

    63 | "A \<up> (Suc n) =  A \<cdot> (A \<up> n)" 

    64 

    65 definition

    66   Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)

    67 where

    68   "A\<star> \<equiv> (\<Union>n. A \<up> n)"

    69 

    70 lemma star_start[intro]:

    71   shows "[] \<in> A\<star>"

    72 proof -

    73   have "[] \<in> A \<up> 0" by auto

    74   then show "[] \<in> A\<star>" unfolding Star_def by blast

    75 qed

    76 

    77 lemma star_step [intro]:

    78   assumes a: "s1 \<in> A" 

    79   and     b: "s2 \<in> A\<star>"

    80   shows "s1 @ s2 \<in> A\<star>"

    81 proof -

    82   from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto

    83   then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)

    84   then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast

    85 qed

    86 

    87 lemma star_induct[consumes 1, case_names start step]:

    88   assumes a: "x \<in> A\<star>" 

    89   and     b: "P []"

    90   and     c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"

    91   shows "P x"

    92 proof -

    93   from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto

    94   then show "P x"

    95     by (induct n arbitrary: x)

    96        (auto intro!: b c simp add: Seq_def Star_def)

    97 qed

    98     

    99 lemma star_intro1:

   100   assumes a: "x \<in> A\<star>"

   101   and     b: "y \<in> A\<star>"

   102   shows "x @ y \<in> A\<star>"

   103 using a b

   104 by (induct rule: star_induct) (auto)

   105 

   106 lemma star_intro2: 

   107   assumes a: "y \<in> A"

   108   shows "y \<in> A\<star>"

   109 proof -

   110   from a have "y @ [] \<in> A\<star>" by blast

   111   then show "y \<in> A\<star>" by simp

   112 qed

   113 

   114 lemma star_intro3:

   115   assumes a: "x \<in> A\<star>"

   116   and     b: "y \<in> A"

   117   shows "x @ y \<in> A\<star>"

   118 using a b by (blast intro: star_intro1 star_intro2)

   119 

   120 lemma star_cases:

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

   122 proof

   123   { fix x

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

   125       unfolding Seq_def

   126     by (induct rule: star_induct) (auto)

   127   }

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

   129 next

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

   131     unfolding Seq_def by auto

   132 qed

   133 

   134 lemma star_decom: 

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

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

   137 using a

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

   139 

   140 lemma seq_Union_left: 

   141   shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))"

   142 unfolding Seq_def by auto

   143 

   144 lemma seq_Union_right: 

   145   shows "(\<Union>n. A \<up> n) \<cdot> B = (\<Union>n. (A \<up> n) \<cdot> B)"

   146 unfolding Seq_def by auto

   147 

   148 lemma seq_pow_comm:

   149   shows "A \<cdot> (A \<up> n) = (A \<up> n) \<cdot> A"

   150 by (induct n) (simp_all add: seq_assoc[symmetric])

   151 

   152 lemma seq_star_comm:

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

   154 unfolding Star_def seq_Union_left

   155 unfolding seq_pow_comm seq_Union_right 

   156 by simp

   157 

   158 

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

   160 

   161 lemma pow_length:

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

   163   and     b: "s \<in> A \<up> Suc n"

   164   shows "n < length s"

   165 using b

   166 proof (induct n arbitrary: s)

   167   case 0

   168   have "s \<in> A \<up> Suc 0" by fact

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

   170   then show "0 < length s" by auto

   171 next

   172   case (Suc n)

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

   174   have "s \<in> A \<up> Suc (Suc n)" by fact

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

   176     by (auto simp add: Seq_def)

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

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

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

   180     by (simp only: length_append)

   181 qed

   182 

   183 lemma seq_pow_length:

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

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

   186   shows "n < length s"

   187 proof -

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

   189     unfolding Seq_def by auto

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

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

   192 qed

   193 

   194 

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

   196 

   197 text {*  A helper lemma for Arden *}

   198 

   199 lemma arden_helper:

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

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

   202 proof (induct n)

   203   case 0 

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

   205     using eq by simp

   206 next

   207   case (Suc n)

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

   209   also have "\<dots> = (X \<cdot> A \<union> B) \<cdot> (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A \<up> m))" using eq by simp

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

   211     by (simp add: seq_union_distrib_right seq_assoc)

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

   213     by (auto simp add: le_Suc_eq)

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

   215 qed

   216 

   217 theorem arden:

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

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

   220 proof

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

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

   223     unfolding seq_star_comm[symmetric]

   224     by (rule star_cases)

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

   226     by (rule seq_add_left)

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

   228     unfolding seq_union_distrib_left by simp

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

   230     by (simp only: seq_assoc)

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

   232     using eq by blast 

   233 next

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

   235   { fix n::nat

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

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

   238     unfolding Seq_def Star_def UNION_def by auto

   239   moreover

   240   { fix s::string

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

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

   243       using seq_pow_length[OF nemp] by blast

   244     assume "s \<in> X"

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

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

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

   248     moreover

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

   250     ultimately 

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

   252       unfolding seq_Union_left Star_def by auto }

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

   254   ultimately 

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

   256 qed

   257 

   258 

   259 section {* Regular Expressions *}

   260 

   261 datatype rexp =

   262   NULL

   263 | EMPTY

   264 | CHAR char

   265 | SEQ rexp rexp

   266 | ALT rexp rexp

   267 | STAR rexp

   268 

   269 fun

   270   L_rexp :: "rexp \<Rightarrow> lang"

   271 where

   272     "L_rexp (NULL) = {}"

   273   | "L_rexp (EMPTY) = {[]}"

   274   | "L_rexp (CHAR c) = {[c]}"

   275   | "L_rexp (SEQ r1 r2) = (L_rexp r1) \<cdot> (L_rexp r2)"

   276   | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"

   277   | "L_rexp (STAR r) = (L_rexp r)\<star>"

   278 

   279 text {* ALT-combination for a set of regular expressions *}

   280 

   281 abbreviation

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

   283 where

   284   "\<Uplus>A \<equiv> folds ALT NULL A"

   285 

   286 text {* 

   287   For finite sets, @{term Setalt} is preserved under @{term L_exp}.

   288 *}

   289 

   290 lemma folds_alt_simp [simp]:

   291   fixes rs::"rexp set"

   292   assumes a: "finite rs"

   293   shows "L_rexp (\<Uplus>rs) = \<Union> (L_rexp ` rs)"

   294 unfolding folds_def

   295 apply(rule set_eqI)

   296 apply(rule someI2_ex)

   297 apply(rule_tac finite_imp_fold_graph[OF a])

   298 apply(erule fold_graph.induct)

   299 apply(auto)

   300 done

   301 

   302 end