1 theory MyhillNerode

     1 theory Myhill

     2   imports "Main" "List_Prefix"

     2   imports Main List_Prefix

     5 text {* sequential composition of languages *}

     5 section {* Preliminary definitions *}

     6 

     7 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}

    36   have "A\<star> =  {[]} \<union> A\<star> ;; A" sorry 

    65   have "A\<star> =  {[]} \<union> A\<star> ;; A" 

    37   then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" unfolding Seq_def by simp

    66     by (auto simp:Seq_def star_intro3 star_decom')  

    38   also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"  unfolding Seq_def by auto

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

    39   also have "\<dots> = B \<union> (B ;; A\<star>) ;; A"  unfolding Seq_def

    68     unfolding Seq_def by simp

    40     by (auto) (metis append_assoc)+

    69   also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"  

    41   finally show "X = X ;; A \<union> B" using eq by auto

    70     unfolding Seq_def by auto

    71   also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" 

    72     by (simp only:seq_assoc)

    73   finally show "X = X ;; A \<union> B" 

    74     using eq by blast 

    43   assume "X = X ;; A \<union> B"

    76   assume eq': "X = X ;; A \<union> B"

    44   then have "B \<subseteq> X" "X ;; A \<subseteq> X" by auto

    77   hence c1': "\<And> x. x \<in> B \<Longrightarrow> x \<in> X" 

    45   thus "X = B ;; A\<star>" sorry

    78     and c2': "\<And> x y. \<lbrakk>x \<in> X; y \<in> A\<rbrakk> \<Longrightarrow> x @ y \<in> X" 

    46 qed

    79     using Seq_def by auto

    47 

    80   show "X = B ;; A\<star>" 

    81   proof

    82     show "B ;; A\<star> \<subseteq> X"

    83     proof-

    84       { fix x y

    85         have "\<lbrakk>y \<in> A\<star>; x \<in> X\<rbrakk> \<Longrightarrow> x @ y \<in> X "

    86           apply (induct arbitrary:x rule:Star.induct, simp)

    87           by (auto simp only:append_assoc[THEN sym] dest:c2')

    88       } thus ?thesis using c1' by (auto simp:Seq_def) 

    89     qed

    90   next

    91     show "X \<subseteq> B ;; A\<star>"

    92     proof-

    93       { fix x 

    94         have "x \<in> X \<Longrightarrow> x \<in> B ;; A\<star>"

    95         proof (induct x taking:length rule:measure_induct)

    96           fix z

    97           assume hyps: 

    98             "\<forall>y. length y < length z \<longrightarrow> y \<in> X \<longrightarrow> y \<in> B ;; A\<star>" 

    99             and z_in: "z \<in> X"

   100           show "z \<in> B ;; A\<star>"

   101           proof (cases "z \<in> B")

   102             case True thus ?thesis by (auto simp:Seq_def start)

   103           next

   104             case False hence "z \<in> X ;; A" using eq' z_in by auto

   105             then obtain za zb where za_in: "za \<in> X" 

   106               and zab: "z = za @ zb \<and> zb \<in> A" and zbne: "zb \<noteq> []" 

   107               using nemp unfolding Seq_def by blast

   108             from zbne zab have "length za < length z" by auto

   109             with za_in hyps have "za \<in> B ;; A\<star>" by blast

   110             hence "za @ zb \<in> B ;; A\<star>" using zab 

   111               by (clarsimp simp:Seq_def, blast dest:star_intro3)

   112             thus ?thesis using zab by simp       

   113           qed

   114         qed 

   115       } thus ?thesis by blast

   116     qed

   117   qed

   118 qed

   119 

   120 

   121 text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}

    87 definition

   183 

    88   str_eq ("_ \<approx>_ _")

   184 text {*

    89 where

   185   @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.

    90   "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"

   186 *}

    91 

    95   "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"

   190   "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"

    96 

   191 

    97 definition

   192 text {* 

    98   final :: "string set \<Rightarrow> string set \<Rightarrow> bool"

   193   Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out 

    99 where

   194   those which contains strings from @{text "Lang"}.

   100   "final X Lang \<equiv> (X \<in> UNIV // \<approx>Lang) \<and> (\<forall>s \<in> X. s \<in> Lang)"

   195 *}

   101 

   196 

   197 definition 

   198    "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}"

   199 

   200 text {* 

   201   The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}.

   202 *}

   103   "Lang = \<Union> {X. final X Lang}"

   204   "Lang = \<Union> finals(Lang)"

   105   show "Lang \<subseteq> \<Union> {X. final X Lang}"

   206   show "Lang \<subseteq> \<Union> (finals Lang)"

   109     thus "x \<in> \<Union> {X. final X Lang}"

   210     thus "x \<in> \<Union> (finals Lang)"

   110       apply (simp, rule_tac x = "(\<approx>Lang) `` {x}" in exI)      

   211       apply (simp add:finals_def, rule_tac x = "(\<approx>Lang) `` {x}" in exI)

   111       apply (auto simp:final_def quotient_def Image_def str_eq_rel_def str_eq_def)

   212       by (auto simp:Image_def str_eq_rel_def)    

   112       by (drule_tac x = "[]" in spec, simp)

   115   show "\<Union>{X. final X Lang} \<subseteq> Lang"

   215   show "\<Union> (finals Lang) \<subseteq> Lang"

   116     by (auto simp:final_def)

   216     apply (clarsimp simp:finals_def str_eq_rel_def)

   117 qed

   217     by (drule_tac x = "[]" in spec, auto)

   118 

   218 qed

   119 section {* finite \<Rightarrow> regular *}

   219 

   220 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}

   221 

   222 text {* 

   223   The relationship between equivalent classes can be described by an

   224   equational system.

   225   For example, in equational system \eqref{example_eqns},  $X_0, X_1$ are equivalent 

   226   classes. The first equation says every string in $X_0$ is obtained either by

   227   appending one $b$ to a string in $X_0$ or by appending one $a$ to a string in

   228   $X_1$ or just be an empty string (represented by the regular expression $\lambda$). Similary,

   229   the second equation tells how the strings inside $X_1$ are composed.

   230   \begin{equation}\label{example_eqns}

   231     \begin{aligned}

   232       X_0 & = X_0 b + X_1 a + \lambda \\

   233       X_1 & = X_0 a + X_1 b

   234     \end{aligned}

   235   \end{equation}

   236   The summands on the right hand side is represented by the following data type

   237   @{text "rhs_item"}, mnemonic for 'right hand side item'.

   238   Generally, there are two kinds of right hand side items, one kind corresponds to

   239   pure regular expressions, like the $\lambda$ in \eqref{example_eqns}, the other kind corresponds to

   240   transitions from one one equivalent class to another, like the $X_0 b, X_1 a$ etc.

   241   *}

   123  | Trn "string set" "rexp"              (* Transition *)

   245  | Trn "(string set)" "rexp"              (* Transition *)

   246 

   247 text {*

   248   In this formalization, pure regular expressions like $\lambda$ is 

   249   repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is represented by $Trn~X_0~(CHAR~a)$.

   250   *}

   251 

   252 text {*

   253   The functions @{text "the_r"} and @{text "the_Trn"} are used to extract

   254   subcomponents from right hand side items.

   255   *}

   256 

   257 fun the_r :: "rhs_item \<Rightarrow> rexp"

   258 where "the_r (Lam r) = r"

   128 fun the_r :: "rhs_item \<Rightarrow> rexp"

   263 text {*

   129 where "the_r (Lam r) = r"

   264   Every right hand side item @{text "itm"} defines a string set given 

   130 

   265   @{text "L(itm)"}, defined as:

   266 *}

   133 fun L_rhs_e:: "rhs_item \<Rightarrow> string set"

   269   fun L_rhs_e:: "rhs_item \<Rightarrow> string set"

   134 where

   270   where

   135   "L_rhs_e (Lam r) = L r" |

   271      "L_rhs_e (Lam r) = L r" |

   136   "L_rhs_e (Trn X r) = X ;; L r"

   272      "L_rhs_e (Trn X r) = X ;; L r"

   141 fun L_rhs:: "rhs_item set \<Rightarrow> string set"

   283    fun L_rhs:: "rhs_item set \<Rightarrow> string set"

   142 where

   284    where "L_rhs rhs = \<Union> (L ` rhs)"

   143   "L_rhs rhs = \<Union> (L ` rhs)"

   147   "init_rhs CS X \<equiv>  if ([] \<in> X)

   295   "init_rhs CS X \<equiv>  

   148                     then {Lam EMPTY} \<union> {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}

   296       if ([] \<in> X) then 

   149                     else {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"

   297           {Lam(EMPTY)} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}

   150 

   298       else 

   151 definition

   299           {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"

   152   "eqs CS \<equiv> {(X, init_rhs CS X)|X.  X \<in> CS}"

   300 

   153 

   301 text {*

   302   In the definition of @{text "init_rhs"}, the term 

   303   @{text "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"} appearing on both branches

   304   describes the formation of strings in @{text "X"} out of transitions, while 

   305   the term @{text "{Lam(EMPTY)}"} describes the empty string which is intrinsically contained in

   306   @{text "X"} rather than by transition. This @{text "{Lam(EMPTY)}"} corresponds to 

   307   the $\lambda$ in \eqref{example_eqns}.

   308 

   309   With the help of @{text "init_rhs"}, the equitional system descrbing the formation of every

   310   equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}.

   311   *}

   312 

   313 definition "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"

   162 definition 

   338 text {*

   163   "rexp_of rhs X \<equiv> folds ALT NULL ((snd o the_Trn) ` items_of rhs X)"

   339   The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"}

   340   using @{text "ALT"} to form a single regular expression. 

   341   When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"}

   342   is used to compute compute the regular expression corresponds to @{text "rhs"}.

   343   *}

   170   "attach_rexp r' (Lam r)   = Lam (SEQ r r')"

   356   "attach_rexp rexp' (Lam rexp)   = Lam (SEQ rexp rexp')"

   171 | "attach_rexp r' (Trn X r) = Trn X (SEQ r r')"

   357 | "attach_rexp rexp' (Trn X rexp) = Trn X (SEQ rexp rexp')"

   358 

   359 text {* 

   360   The following @{text "append_rhs_rexp rhs rexp"} attaches 

   361   @{text "rexp"} to every item in @{text "rhs"}.

   362   *}

   174   "append_rhs_rexp rhs r \<equiv> (attach_rexp r) ` rhs"

   365   "append_rhs_rexp rhs rexp \<equiv> (attach_rexp rexp) ` rhs"

   175 

   366 

   367 text {*

   368   With the help of the two functions immediately above, Ardens'

   369   transformation on right hand side @{text "rhs"} is implemented

   370   by the following function @{text "arden_variate X rhs"}.

   371   After this transformation, the recursive occurent of @{text "X"}

   372   in @{text "rhs"} will be eliminated, while the 

   373   string set defined by @{text "rhs"} is kept unchanged.

   374   *}

   177   "arden_variate X rhs \<equiv> append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"

   376   "arden_variate X rhs \<equiv> 

   377         append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"

   182 text {* rhs_subst rhs X xrhs: substitude all occurence of X in rhs with xrhs *}

   382 text {* 

   383   Suppose the equation defining @{text "X"} is $X = xrhs$,

   384   the purpose of @{text "rhs_subst"} is to substitute all occurences of @{text "X"} in

   385   @{text "rhs"} by @{text "xrhs"}.

   386   A litte thought may reveal that the final result

   387   should be: first append $(a_1 | a_2 | \ldots | a_n)$ to every item of @{text "xrhs"} and then

   388   union the result with all non-@{text "X"}-items of @{text "rhs"}.

   389  *}

   184   "rhs_subst rhs X xrhs \<equiv> (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"

   391   "rhs_subst rhs X xrhs \<equiv> 

   392         (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"

   393 

   394 text {*

   395   Suppose the equation defining @{text "X"} is $X = xrhs$, the follwing

   396   @{text "eqs_subst ES X xrhs"} substitute @{text "xrhs"} into every equation

   397   of the equational system @{text "ES"}.

   398   *}

   190   Inv: Invairance of the equation-system, during the decrease of the equation-system, Inv holds.

   404   The computation of regular expressions for equivalent classes is accomplished

   191 *}

   405   using a iteration principle given by the following lemma.

   192 

   406   *}

   193 definition 

   194   "distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"

   195 

   196 definition 

   197   "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"

   198 

   199 definition 

   200   "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"

   201 

   202 definition 

   203   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"

   204 

   205 definition 

   206   "non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}"

   207 

   208 definition

   209   "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"

   210 

   211 definition 

   212   "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"

   213 

   214 definition

   215   "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"

   216 

   217 definition 

   218   "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"

   219 

   220 definition 

   221   "Inv ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 

   222             non_empty ES \<and> finite_rhs ES \<and> self_contained ES"

   251 text {* ************* basic properties of definitions above ************************ *}

   435 text {*

   436   The @{text "P"} in lemma @{text "wf_iter"} is an invaiant kept throughout the iteration procedure.

   437   The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"},

   438   an invariant over equal system @{text "ES"}.

   439   Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}.

   440 *}

   441 

   442 text {* 

   443   Every variable is defined at most onece in @{text "ES"}.

   444   *}

   445 definition 

   446   "distinct_equas ES \<equiv> 

   447             \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"

   448 text {* 

   449   Every equation in @{text "ES"} (represented by @{text "(X, rhs)"}) is valid, i.e. @{text "(X = L rhs)"}.

   450   *}

   451 definition 

   452   "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"

   453 

   454 text {*

   455   @{text "rhs_nonempty rhs"} requires regular expressions occuring in transitional 

   456   items of @{text "rhs"} does not contain empty string. This is necessary for

   457   the application of Arden's transformation to @{text "rhs"}.

   458   *}

   459 definition 

   460   "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"

   461 

   462 text {*

   463   @{text "ardenable ES"} requires that Arden's transformation is applicable

   464   to every equation of equational system @{text "ES"}.

   465   *}

   466 definition 

   467   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"

   468 

   469 (* The following non_empty seems useless. *)

   470 definition 

   471   "non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}"

   472 

   473 text {*

   474   The following @{text "finite_rhs ES"} requires every equation in @{text "rhs"} be finite.

   475   *}

   476 definition

   477   "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"

   478 

   479 text {*

   480   The following @{text "classes_of rhs"} returns all variables (or equivalent classes)

   481   occuring in @{text "rhs"}.

   482   *}

   483 definition 

   484   "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"

   485 

   486 text {*

   487   The following @{text "lefts_of ES"} returns all variables 

   488   defined by equational system @{text "ES"}.

   489   *}

   490 definition

   491   "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"

   492 

   493 text {*

   494   The following @{text "self_contained ES"} requires that every

   495   variable occuring on the right hand side of equations is already defined by some

   496   equation in @{text "ES"}.

   497   *}

   498 definition 

   499   "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"

   500 

   501 

   502 text {*

   503   The invariant @{text "Inv(ES)"} is obtained by conjunctioning all the previous

   504   defined constaints on @{text "ES"}.

   505   *}

   506 definition 

   507   "Inv ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 

   508                 non_empty ES \<and> finite_rhs ES \<and> self_contained ES"

   509 

   510 subsection {* Proof for this direction *}

   511 

   512 

   513 

   514 text {*

   515   The following are some basic properties of the above definitions.

   516 *}

   322 text {* ******BEGIN: proving the initial equation-system satisfies Inv ****** *}

   587 text {*

   588   The following several lemmas until @{text "init_ES_satisfy_Inv"} are

   589   to prove that initial equational system satisfies invariant @{text "Inv"}.

   590   *}

   326 by (auto simp:quotient_def Image_def str_eq_rel_def str_eq_def)

   594 by (auto simp:quotient_def Image_def str_eq_rel_def)

   342     by (auto) (simp add: str_eq_def)

   610     by clarsimp

   345     unfolding Image_def str_eq_rel_def str_eq_def by simp

   613     unfolding Image_def str_eq_rel_def by simp

   372       hence "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y ;; {[c]} \<subseteq> X}"

   640       hence 

   641         "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y ;; {[c]} \<subseteq> X}"

   415     by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def str_eq_def)

   684     by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def)

   424 text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}

   693 text {*

   425 

   694   From this point until @{text "iteration_step"}, we are trying to prove 

   695   that there exists iteration steps which keep @{text "Inv(ES)"} while

   696   decreasing the size of @{text "ES"} with every iteration.

   697   *}

   509   have "finite {(Ya, rhs_subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" (is "finite ?A")

   781   have "finite {(Ya, rhs_subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" 

   782                                                                   (is "finite ?A")

   540   "X \<notin> classes_of xrhs \<Longrightarrow> classes_of (rhs_subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"

   813   "X \<notin> classes_of xrhs \<Longrightarrow> 

   541 apply (simp only:rhs_subst_def append_rhs_keeps_cls classes_of_union_distrib[THEN sym])

   814       classes_of (rhs_subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"

   815 apply (simp only:rhs_subst_def append_rhs_keeps_cls 

   816                               classes_of_union_distrib[THEN sym])

   547   shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" (is "self_contained ?B")

   822   shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" 

   823                                                    (is "self_contained ?B")

   559         have "classes_of xrhs' \<subseteq> classes_of xrhs \<union> classes_of (arden_variate Y yrhs) - {Y}"

   835         have "classes_of xrhs' \<subseteq> 

   836                         classes_of xrhs \<union> classes_of (arden_variate Y yrhs) - {Y}"

   561           have "Y \<notin> classes_of (arden_variate Y yrhs)" using arden_variate_removes_cl by simp

   838           have "Y \<notin> classes_of (arden_variate Y yrhs)" 

   839             using arden_variate_removes_cl by simp

   567         moreover have "classes_of (arden_variate Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" using sc

   845         moreover have "classes_of (arden_variate Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 

   846           using sc 

   580   have finite_yrhs: "finite yrhs" using Inv_ES by (auto simp:Inv_def finite_rhs_def)

   859   have finite_yrhs: "finite yrhs" 

   581   have nonempty_yrhs: "rhs_nonempty yrhs" using Inv_ES by (auto simp:Inv_def ardenable_def)

   860     using Inv_ES by (auto simp:Inv_def finite_rhs_def)

   582   have Y_eq_yrhs: "Y = L yrhs" using Inv_ES by (simp only:Inv_def valid_eqns_def, blast)

   861   have nonempty_yrhs: "rhs_nonempty yrhs" 

   583 

   862     using Inv_ES by (auto simp:Inv_def ardenable_def)

   584   have "distinct_equas (eqs_subst ES Y (arden_variate Y yrhs))" using Inv_ES

   863   have Y_eq_yrhs: "Y = L yrhs" 

   864     using Inv_ES by (simp only:Inv_def valid_eqns_def, blast)

   865   have "distinct_equas (eqs_subst ES Y (arden_variate Y yrhs))" 

   866     using Inv_ES

   586   moreover have "finite (eqs_subst ES Y (arden_variate Y yrhs))" using Inv_ES 

   868   moreover have "finite (eqs_subst ES Y (arden_variate Y yrhs))" 

   587     by (simp add:Inv_def eqs_subst_keeps_finite)

   869     using Inv_ES by (simp add:Inv_def eqs_subst_keeps_finite)

   590     have "finite_rhs ES" using Inv_ES by (simp add:Inv_def finite_rhs_def)

   872     have "finite_rhs ES" using Inv_ES 

   873       by (simp add:Inv_def finite_rhs_def)

   593       have "finite yrhs" using Inv_ES by (auto simp:Inv_def finite_rhs_def)

   876       have "finite yrhs" using Inv_ES 

   877         by (auto simp:Inv_def finite_rhs_def)

   596     ultimately show ?thesis by (simp add:eqs_subst_keeps_finite_rhs)

   880     ultimately show ?thesis 

   881       by (simp add:eqs_subst_keeps_finite_rhs)

   602       hence "rhs_nonempty rhs"  using prems Inv_ES  by (simp add:Inv_def ardenable_def)

   887       hence "rhs_nonempty rhs"  using prems Inv_ES  

   603       with nonempty_yrhs have "rhs_nonempty (rhs_subst rhs Y (arden_variate Y yrhs))"

   888         by (simp add:Inv_def ardenable_def)

   604         by (simp add:nonempty_yrhs rhs_subst_keeps_nonempty arden_variate_keeps_nonempty)

   889       with nonempty_yrhs 

   890       have "rhs_nonempty (rhs_subst rhs Y (arden_variate Y yrhs))"

   891         by (simp add:nonempty_yrhs 

   892                rhs_subst_keeps_nonempty arden_variate_keeps_nonempty)

   609     have "Y = L (arden_variate Y yrhs)" using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs      

   897     have "Y = L (arden_variate Y yrhs)" 

   610         by (rule_tac arden_variate_keeps_eq, (simp add:rexp_of_empty)+)

   898       using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs      

   899       by (rule_tac arden_variate_keeps_eq, (simp add:rexp_of_empty)+)

   612       by (clarsimp simp add:valid_eqns_def eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def

   901       by (clarsimp simp add:valid_eqns_def 

   902               eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def

   615   moreover have non_empty_subst: "non_empty (eqs_subst ES Y (arden_variate Y yrhs))"

   905   moreover have 

   906     non_empty_subst: "non_empty (eqs_subst ES Y (arden_variate Y yrhs))"

   617   moreover have self_subst: "self_contained (eqs_subst ES Y (arden_variate Y yrhs))"

   908   moreover 

   909   have self_subst: "self_contained (eqs_subst ES Y (arden_variate Y yrhs))"

   645     have "card S > 1" using card e_in finite  by (case_tac "card S", auto) 

   937     have "card S > 1" using card e_in finite  

   938       by (case_tac "card S", auto) 

   656   shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'.(X, xrhs') \<in> ES')) \<and> (card ES', card ES) \<in> less_than" (is "\<exists> ES'. ?P ES'")

   949   shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'.(X, xrhs') \<in> ES')) \<and> 

   950                 (card ES', card ES) \<in> less_than" (is "\<exists> ES'. ?P ES'")

   659   then obtain Y yrhs where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 

   953   then obtain Y yrhs 

   954     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 

   682 text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *}

   977 text {*

   978   From this point until @{text "hard_direction"}, the hard direction is proved

   979   through a simple application of the iteration principle.

   980 *}

   687   shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1" (is "\<exists> ES'. ?P ES'")

   985   shows 

   986   "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1" 

   987                                                           (is "\<exists> ES'. ?P ES'")

   709         by (rule_tac arden_variate_keeps_finite, auto simp add:Inv_def finite_rhs_def)

  1009         by (rule_tac arden_variate_keeps_finite, 

  1010                        auto simp add:Inv_def finite_rhs_def)

   716           by (simp add:arden_variate_removes_cl self_contained_def Inv_def lefts_of_def) 

  1017           by (simp add:arden_variate_removes_cl 

   717         thus ?thesis by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)

  1018                        self_contained_def Inv_def lefts_of_def) 

  1019         thus ?thesis 

  1020           by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)

   723       show "X = L xrhs" using Inv_ES ES_single by (auto simp only:Inv_def valid_eqns_def)  

  1026       show "X = L xrhs" using Inv_ES ES_single 

  1027         by (auto simp only:Inv_def valid_eqns_def)  

   728       from Inv_ES ES_single show "finite xrhs" by (simp add:Inv_def finite_rhs_def)

  1032       from Inv_ES ES_single show "finite xrhs" 

  1033         by (simp add:Inv_def finite_rhs_def)

   759   then obtain f where f_prop: "\<forall> X \<in> (UNIV // (\<approx>Lang)). X = L ((f X)::rexp)" 

  1068   then obtain f 

  1069     where f_prop: "\<forall> X \<in> (UNIV // (\<approx>Lang)). X = L ((f X)::rexp)" 

   761   def rs \<equiv> "f ` {X. final X Lang}"  

  1071   def rs \<equiv> "f ` (finals Lang)"  

   762   have "Lang = \<Union> {X. final X Lang}" using lang_is_union_of_finals by simp

  1072   have "Lang = \<Union> (finals Lang)" using lang_is_union_of_finals by auto

   765     have "finite {X. final X Lang}" using finite_CS by (auto simp:final_def)

  1075     have "finite rs"

   766     thus ?thesis  using f_prop by (auto simp:rs_def final_def)

  1076     proof -

  1077       have "finite (finals Lang)" 

  1078         using finite_CS finals_in_partitions[of "Lang"]   

  1079         by (erule_tac finite_subset, simp)

  1080       thus ?thesis using rs_def by auto

  1081     qed

  1082     thus ?thesis 

  1083       using f_prop rs_def finals_in_partitions[of "Lang"] by auto

   771 section {* regular \<Rightarrow> finite*}

  1088 section {* Direction: @{text "regular language \<Rightarrow>finite partition"} *}

   772 

  1089 

   773 lemma quot_empty_subset:

  1090 subsection {* The scheme for this direction *}

   774   "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"

  1091 

   775 proof

  1092 text {* 

   776   fix x

  1093   The following convenient notation @{text "x \<approx>Lang y"} means:

   777   assume "x \<in> UNIV // \<approx>{[]}"

  1094   string @{text "x"} and @{text "y"} are equivalent with respect to 

   778   then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" unfolding quotient_def Image_def by blast

  1095   language @{text "Lang"}.

   779   show "x \<in> {{[]}, UNIV - {[]}}" 

  1096   *}

   780   proof (cases "y = []")

  1097 

   781     case True with h

  1098 definition

   782     have "x = {[]}" by (auto simp:str_eq_rel_def str_eq_def)

  1099   str_eq ("_ \<approx>_ _")

   783     thus ?thesis by simp

  1100 where

   784   next

  1101   "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"

   785     case False with h

  1102 

   786     have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def str_eq_def)

  1103 text {*

   787     thus ?thesis by simp

  1104   The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"}

   788   qed

  1105   is by attaching tags to every string. The set of tags are carfully choosen to make it finite.

   789 qed

  1106   If it can be proved that strings with the same tag are equivlent with respect @{text "Lang"},

   790 

  1107   then the partition given rise by @{text "Lang"} must be finite. The reason for this is a lemma 

   791 lemma quot_char_subset:

  1108   in standard library (@{text "finite_imageD"}), which says: if the image of an injective 

   792   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"

  1109   function on a set @{text "A"} is finite, then @{text "A"} is finite. It can be shown that

   793 proof 

  1110   the function obtained by llifting @{text "tag"}

   794   fix x 

  1111   to the level of equalent classes (i.e. @{text "((op `) tag)"}) is injective 

   795   assume "x \<in> UNIV // \<approx>{[c]}"

  1112   (by lemma @{text "tag_image_injI"}) and the image of this function is finite 

   796   then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}" unfolding quotient_def Image_def by blast

  1113   (with the help of lemma @{text "finite_tag_imageI"}).

   797   show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"

  1114 

   798   proof -

  1115   BUT, I think this argument can be encapsulated by one lemma instead of the current presentation.

   799     { assume "y = []" hence "x = {[]}" using h by (auto simp:str_eq_rel_def str_eq_def)

  1116   *}

   800     } moreover {

   801       assume "y = [c]" hence "x = {[c]}" using h 

   802         by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def str_eq_def)

   803     } moreover {

   804       assume "y \<noteq> []" and "y \<noteq> [c]"

   805       hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)

   806       moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" by (case_tac p, auto)

   807       ultimately have "x = UNIV - {[],[c]}" using h

   808         by (auto simp add:str_eq_rel_def str_eq_def)

   809     } ultimately show ?thesis by blast

   810   qed

   811 qed

   812 

   813 text {* *************** Some common lemmas for following ALT, SEQ & STAR cases ******************* *}

   814 

   815 lemma finite_tag_imageI: 

   816   "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)"

   817 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)

   818 by (auto simp add:image_def Pow_def)

   821   "\<lbrakk>X \<in> UNIV // \<approx>lang; Y \<in> UNIV // \<approx>lang; x \<in> X; y \<in> Y; x \<approx>lang y\<rbrakk> \<Longrightarrow> X = Y"

  1119   "\<lbrakk>X \<in> UNIV // \<approx>lang; Y \<in> UNIV // \<approx>lang; x \<in> X; y \<in> Y; x \<approx>lang y\<rbrakk> 

  1120                          \<Longrightarrow> X = Y"

   825   assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>lang n"

  1124   assumes str_inj: "\<And> x y. tag x = tag (y::string) \<Longrightarrow> x \<approx>lang y"

   841 text {* **************** the SEQ case ************************ *}

  1140 lemma finite_tag_imageI: 

  1141   "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)"

  1142 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)

  1143 by (auto simp add:image_def Pow_def)

  1144 

  1145 

  1146 subsection {* A small theory for list difference *}

  1147 

  1148 text {*

  1149   The notion of list diffrence is need to make proofs more readable.

  1150   *}

   887   "x @ y = m @ n \<Longrightarrow> (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"

  1196   "x @ y = m @ n \<Longrightarrow> 

  1197                (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"

   891   "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa.  xa \<le> x \<and> xa \<in> L\<^isub>1})"

  1263   "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> 

  1264        ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa.  xa \<le> x \<and> xa \<in> L\<^isub>1})"

   894   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"

  1267   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 

  1268                               \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"

   900   shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"

  1274   shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> 

  1275           (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"

   902   from assms obtain s\<^isub>1 s\<^isub>2 where "x @ y = s\<^isub>1 @ s\<^isub>2" and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2" 

  1277   from assms obtain s\<^isub>1 s\<^isub>2 

  1278     where "x @ y = s\<^isub>1 @ s\<^isub>2" 

  1279     and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2" 

   906   moreover have "\<lbrakk>x \<le> s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\<rbrakk> \<Longrightarrow> \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2" using in_seq

  1283   moreover have "\<lbrakk>x \<le> s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\<rbrakk> \<Longrightarrow> 

   907     by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)

  1284                        \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2" 

   908   moreover have "\<lbrakk>s\<^isub>1 \<le> x; (x - s\<^isub>1) @ y = s\<^isub>2\<rbrakk> \<Longrightarrow> \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2" using in_seq

  1285     using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)

   909     by (rule_tac x = s\<^isub>1 in exI, auto)

  1286   moreover have "\<lbrakk>s\<^isub>1 \<le> x; (x - s\<^isub>1) @ y = s\<^isub>2\<rbrakk> \<Longrightarrow> 

  1287                     \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2" 

  1288     using in_seq by (rule_tac x = s\<^isub>1 in exI, auto)

   921       have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)"

  1300       have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> 

  1301                (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)"

   931                   {\<approx>L\<^isub>2 `` {y - xa} |xa. xa \<le> y \<and> xa \<in> L\<^isub>1}" (is "?Left = ?Right") 

  1311                   {\<approx>L\<^isub>2 `` {y - xa} |xa. xa \<le> y \<and> xa \<in> L\<^isub>1}" 

  1312                           (is "?Left = ?Right") 

   945           have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}" using h1 tag_xy by (auto simp:tag_str_SEQ_def)

  1326           have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}" 

   946           with h2 show ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def) 

  1327             using h1 tag_xy by (auto simp:tag_str_SEQ_def)

  1328           with h2 show ?thesis 

  1329             by (auto simp:Image_def str_eq_rel_def str_eq_def) 

   948         with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)

  1331         with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" 

  1332           by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)

   961   show "finite (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2) ` UNIV // \<approx>L\<^isub>1 ;; L\<^isub>2)" using finite1 finite2

  1345   show "finite (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2) ` UNIV // \<approx>L\<^isub>1 ;; L\<^isub>2)" 

  1346     using finite1 finite2

   970 text {* **************** the ALT case ************************ *}

  1355 subsection {* The case for @{text "ALT"} *}

   976   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> \<Longrightarrow> finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))"

  1361   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 

  1362                               \<Longrightarrow> finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))"

   985   show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` UNIV // \<approx>L\<^isub>1 \<union> L\<^isub>2)" using finite1 finite2

  1371   show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` UNIV // \<approx>L\<^isub>1 \<union> L\<^isub>2)" 

  1372     using finite1 finite2

   990     have "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n"

  1377     have "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n 

  1378                          \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n"

   996 text {* **************** the Star case ****************** *}

  1384 

   997 

  1385 subsection {*

   998 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"

  1386   The case for @{text "STAR"}

  1387   *}

  1388 

  1389 text {* 

  1390   This turned out to be the most tricky case. 

  1391   *} (* I will make some illustrations for it. *)

  1392 

  1393 definition 

  1394   "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}"

  1395 

  1396 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 

  1397            (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"

  1008     with prems obtain max where h1: "max \<in> A" and h2: "\<forall>a\<in>A. f a \<le> f max" by blast

  1407     with prems obtain max 

  1408       where h1: "max \<in> A" 

  1409       and h2: "\<forall>a\<in>A. f a \<le> f max" by blast