2   imports Main List_Prefix Prefix_subtract Prelude

     2   imports Myhill_1

     5 (*

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

     6 text {*

     7      \begin{figure}

     8     \centering

     9     \scalebox{0.95}{

    10     \begin{tikzpicture}[->,>=latex,shorten >=1pt,auto,node distance=1.2cm, semithick]

    11         \node[state,initial] (n1)                   {$1$};

    12         \node[state,accepting] (n2) [right = 10em of n1]   {$2$};

    13 

    14         \path (n1) edge [bend left] node {$0$} (n2)

    15             (n1) edge [loop above] node{$1$} (n1)

    16             (n2) edge [loop above] node{$0$} (n2)

    17             (n2) edge [bend left]  node {$1$} (n1)

    18             ;

    19     \end{tikzpicture}}

    20     \caption{An example automaton (or partition)}\label{fig:example_automata}

    21     \end{figure}

    22 *}

    23 

    24 *)

    25 

    26 section {* Preliminary definitions *}

    27 

    28 types lang = "string set"

    29 

    30 text {* 

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

    32 *}

    33 

    34 

    35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100)

    36 where 

    37   "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"

    38 

    39 text {* Transitive closure of language @{text "L"}. *}

    40 inductive_set

    41   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

    42   for L :: "string set"

    43 where

    44   start[intro]: "[] \<in> L\<star>"

    45 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" 

    46 

    47 text {* Some properties of operator @{text ";;"}.*}

    48 

    49 lemma seq_union_distrib:

    50   "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"

    51 by (auto simp:Seq_def)

    52 

    53 lemma seq_intro:

    54   "\<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x @ y \<in> A ;; B "

    55 by (auto simp:Seq_def)

    56 

    57 lemma seq_assoc:

    58   "(A ;; B) ;; C = A ;; (B ;; C)"

    59 apply(auto simp:Seq_def)

    60 apply blast

    61 by (metis append_assoc)

    62 

    63 lemma star_intro1[rule_format]: "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>"

    64 by (erule Star.induct, auto)

    65 

    66 lemma star_intro2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>"

    67 by (drule step[of y lang "[]"], auto simp:start)

    68 

    69 lemma star_intro3[rule_format]: 

    70   "x \<in> lang\<star> \<Longrightarrow> \<forall>y . y \<in> lang \<longrightarrow> x @ y \<in> lang\<star>"

    71 by (erule Star.induct, auto intro:star_intro2)

    72 

    73 lemma star_decom: 

    74   "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> lang \<and> b \<in> lang\<star>)"

    75 by (induct x rule: Star.induct, simp, blast)

    76 

    77 lemma star_decom': 

    78   "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. x = a @ b \<and> a \<in> lang\<star> \<and> b \<in> lang"

    79 apply (induct x rule:Star.induct, simp)

    80 apply (case_tac "s2 = []")

    81 apply (rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start)

    82 apply (simp, (erule exE| erule conjE)+)

    83 by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step)

    84 

    85 text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *}

    86 

    87 theorem ardens_revised:

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

    89   shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"

    90 proof

    91   assume eq: "X = B ;; A\<star>"

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

    93     by (auto simp:Seq_def star_intro3 star_decom')  

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

    95     unfolding Seq_def by simp

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

    97     unfolding Seq_def by auto

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

    99     by (simp only:seq_assoc)

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

   101     using eq by blast 

   102 next

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

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

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

   106     using Seq_def by auto

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

   108   proof

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

   110     proof-

   111       { fix x y

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

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

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

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

   116     qed

   117   next

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

   119     proof-

   120       { fix x 

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

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

   123           fix z

   124           assume hyps: 

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

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

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

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

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

   130           next

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

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

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

   134               using nemp unfolding Seq_def by blast

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

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

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

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

   139             thus ?thesis using zab by simp       

   140           qed

   141         qed 

   142       } thus ?thesis by blast

   143     qed

   144   qed

   145 qed

   146 

   147 

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

   149 datatype rexp =

   150   NULL

   151 | EMPTY

   152 | CHAR char

   153 | SEQ rexp rexp

   154 | ALT rexp rexp

   155 | STAR rexp

   156 

   157 

   158 text {* 

   159   The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to 

   160   the language represented by the syntactic object @{text "x"}.

   161 *}

   162 consts L:: "'a \<Rightarrow> string set"

   163 

   164 

   165 text {* 

   166   The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the 

   167   following overloading function @{text "L_rexp"}.

   168 *}

   169 overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> string set"

   170 begin

   171 fun

   172   L_rexp :: "rexp \<Rightarrow> string set"

   173 where

   174     "L_rexp (NULL) = {}"

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

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

   177   | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"

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

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

   180 end

   181 

   182 text {*

   183   To obtain equational system out of finite set of equivalent classes, a fold operation

   184   on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"}

   185   more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"}

   186   makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"},

   187   while @{text "fold f"} does not.  

   188 *}

   189 

   190 definition 

   191   folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"

   192 where

   193   "folds f z S \<equiv> SOME x. fold_graph f z S x"

   194 

   195 text {* 

   196   The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"}

   197   does not affect the @{text "L"}-value of the resultant regular expression. 

   198   *}

   199 lemma folds_alt_simp [simp]:

   200   "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"

   201 apply (rule set_eq_intro, simp add:folds_def)

   202 apply (rule someI2_ex, erule finite_imp_fold_graph)

   203 by (erule fold_graph.induct, auto)

   204 

   205 (* Just a technical lemma. *)

   206 lemma [simp]:

   207   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"

   208 by simp

   209 

   210 text {*

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

   212 *}

   213 

   214 definition

   215   str_eq_rel ("\<approx>_" [100] 100)

   216 where

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

   218 

   219 text {* 

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

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

   222 *}

   223 

   224 definition 

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

   226 

   227 text {* 

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

   229 *}

   230 lemma lang_is_union_of_finals: 

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

   232 proof 

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

   234   proof

   235     fix x

   236     assume "x \<in> Lang"   

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

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

   239       by (auto simp:Image_def str_eq_rel_def)    

   240   qed

   241 next

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

   243     apply (clarsimp simp:finals_def str_eq_rel_def)

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

   245 qed

   246 

   247 

   248 

   249 

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

   251 

   252 text {* 

   253   The relationship between equivalent classes can be described by an

   254   equational system.

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

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

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

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

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

   260   \begin{equation}\label{example_eqns}

   261     \begin{aligned}

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

   263       X_1 & = X_0 a + X_1 b

   264     \end{aligned}

   265   \end{equation}

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

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

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

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

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

   271   *}

   272 

   273 datatype rhs_item = 

   274    Lam "rexp"                           (* Lambda *)

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

   276 

   277 text {*

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

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

   280   *}

   281 

   282 text {*

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

   284   subcomponents from right hand side items.

   285   *}

   286 

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

   288 where "the_r (Lam r) = r"

   289 

   290 fun the_Trn:: "rhs_item \<Rightarrow> (string set \<times> rexp)"

   291 where "the_Trn (Trn Y r) = (Y, r)"

   292 

   293 text {*

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

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

   296 *}

   297 overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> string set"

   298 begin

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

   300   where

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

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

   303 end

   304 

   305 text {*

   306   The right hand side of every equation is represented by a set of

   307   items. The string set defined by such a set @{text "itms"} is given

   308   by @{text "L(itms)"}, defined as:

   309 *}

   310 

   311 overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> string set"

   312 begin

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

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

   315 end

   316 

   317 text {* 

   318   Given a set of equivalent classses @{text "CS"} and one equivalent class @{text "X"} among

   319   @{text "CS"}, the term @{text "init_rhs CS X"} is used to extract the right hand side of

   320   the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"}

   321   is:

   322   *}

   323 

   324 definition

   325   "init_rhs CS X \<equiv>  

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

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

   328       else 

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

   330 

   331 text {*

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

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

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

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

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

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

   338 

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

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

   341   *}

   342 

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

   344 (************ arden's lemma variation ********************)

   345 

   346 text {* 

   347   The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.

   348   *}

   349 definition

   350   "items_of rhs X \<equiv> {Trn X r | r. (Trn X r) \<in> rhs}"

   351 

   352 text {* 

   353   The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items

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

   355   It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}.

   356   *}

   357 

   358 definition 

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

   360 

   361 text {* 

   362   The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.

   363   *}

   364 

   365 definition

   366   "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"

   367 

   368 text {*

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

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

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

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

   373   *}

   374 

   375 definition

   376   "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"

   377 

   378 text {*

   379   The following @{text "attach_rexp rexp' itm"} attach 

   380   the regular expression @{text "rexp'"} to

   381   the right of right hand side item @{text "itm"}.

   382   *}

   383 

   384 fun attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"

   385 where

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

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

   388 

   389 text {* 

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

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

   392   *}

   393 

   394 definition

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

   396 

   397 text {*

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

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

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

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

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

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

   404   *}

   405 definition 

   406   "arden_variate X rhs \<equiv> 

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

   408 

   409 

   410 (*********** substitution of ES *************)

   411 

   412 text {* 

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

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

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

   416   A litte thought may reveal that the final result

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

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

   419  *}

   420 definition 

   421   "rhs_subst rhs X xrhs \<equiv> 

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

   423 

   424 text {*

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

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

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

   428   *}

   429 

   430 definition

   431   "eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"

   432 

   433 text {*

   434   The computation of regular expressions for equivalent classes is accomplished

   435   using a iteration principle given by the following lemma.

   436   *}

   437 

   438 lemma wf_iter [rule_format]: 

   439   fixes f

   440   assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and>  (f(e'), f(e)) \<in> less_than)"

   441   shows pe:     "P e \<longrightarrow> (\<exists> e'. P e' \<and>  Q e')"

   442 proof(induct e rule: wf_induct 

   443            [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify)

   444   fix x 

   445   assume h [rule_format]: 

   446     "\<forall>y. (y, x) \<in> inv_image less_than f \<longrightarrow> P y \<longrightarrow> (\<exists>e'. P e' \<and> Q e')"

   447     and px: "P x"

   448   show "\<exists>e'. P e' \<and> Q e'"

   449   proof(cases "Q x")

   450     assume "Q x" with px show ?thesis by blast

   451   next

   452     assume nq: "\<not> Q x"

   453     from step [OF px nq]

   454     obtain e' where pe': "P e'" and ltf: "(f e', f x) \<in> less_than" by auto

   455     show ?thesis

   456     proof(rule h)

   457       from ltf show "(e', x) \<in> inv_image less_than f" 

   458 	by (simp add:inv_image_def)

   459     next

   460       from pe' show "P e'" .

   461     qed

   462   qed

   463 qed

   464 

   465 text {*

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

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

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

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

   470 *}

   471 

   472 text {* 

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

   474   *}

   475 definition 

   476   "distinct_equas ES \<equiv> 

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

   478 text {* 

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

   480   *}

   481 definition 

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

   483 

   484 text {*

   485   The following @{text "rhs_nonempty rhs"} requires regular expressions occuring in transitional 

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

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

   488   *}

   489 definition 

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

   491 

   492 text {*

   493   The following @{text "ardenable ES"} requires that Arden's transformation is applicable

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

   495   *}

   496 definition 

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

   498 

   499 (* The following non_empty seems useless. *)

   500 definition 

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

   502 

   503 text {*

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

   505   *}

   506 definition

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

   508 

   509 text {*

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

   511   occuring in @{text "rhs"}.

   512   *}

   513 definition 

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

   515 

   516 text {*

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

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

   519   *}

   520 definition

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

   522 

   523 text {*

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

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

   526   equation in @{text "ES"}.

   527   *}

   528 definition 

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

   530 

   531 

   532 text {*

   533   The invariant @{text "Inv(ES)"} is a conjunction of all the previously defined constaints.

   534   *}

   535 definition 

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

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

   538 

   539 subsection {* The proof of this direction *}

   540 

   541 subsubsection {* Basic properties *}

   542 

   543 text {*

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

   545 *}

   546 

   547 lemma L_rhs_union_distrib:

   548   " L (A::rhs_item set) \<union> L B = L (A \<union> B)"

   549 by simp

   550 

   551 lemma finite_snd_Trn:

   552   assumes finite:"finite rhs"

   553   shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \<in> rhs}" (is "finite ?B")

   554 proof-

   555   def rhs' \<equiv> "{e \<in> rhs. \<exists> r. e = Trn Y r}"

   556   have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def)

   557   moreover have "finite rhs'" using finite rhs'_def by auto

   558   ultimately show ?thesis by simp

   559 qed

   560 

   561 lemma rexp_of_empty:

   562   assumes finite:"finite rhs"

   563   and nonempty:"rhs_nonempty rhs"

   564   shows "[] \<notin> L (rexp_of rhs X)"

   565 using finite nonempty rhs_nonempty_def

   566 by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def)

   567 

   568 lemma [intro!]:

   569   "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto

   570 

   571 lemma finite_items_of:

   572   "finite rhs \<Longrightarrow> finite (items_of rhs X)"

   573 by (auto simp:items_of_def intro:finite_subset)

   574 

   575 lemma lang_of_rexp_of:

   576   assumes finite:"finite rhs"

   577   shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))"

   578 proof -

   579   have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto

   580   thus ?thesis

   581     apply (auto simp:rexp_of_def Seq_def items_of_def)

   582     apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto)

   583     by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)

   584 qed

   585 

   586 lemma rexp_of_lam_eq_lam_set:

   587   assumes finite: "finite rhs"

   588   shows "L (rexp_of_lam rhs) = L (lam_of rhs)"

   589 proof -

   590   have "finite (the_r ` {Lam r |r. Lam r \<in> rhs})" using finite

   591     by (rule_tac finite_imageI, auto intro:finite_subset)

   592   thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def)

   593 qed

   594 

   595 lemma [simp]:

   596   " L (attach_rexp r xb) = L xb ;; L r"

   597 apply (cases xb, auto simp:Seq_def)

   598 by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def)

   599 

   600 lemma lang_of_append_rhs:

   601   "L (append_rhs_rexp rhs r) = L rhs ;; L r"

   602 apply (auto simp:append_rhs_rexp_def image_def)

   603 apply (auto simp:Seq_def)

   604 apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def)

   605 by (rule_tac x = "attach_rexp r xb" in exI, auto simp:Seq_def)

   606 

   607 lemma classes_of_union_distrib:

   608   "classes_of A \<union> classes_of B = classes_of (A \<union> B)"

   609 by (auto simp add:classes_of_def)

   610 

   611 lemma lefts_of_union_distrib:

   612   "lefts_of A \<union> lefts_of B = lefts_of (A \<union> B)"

   613 by (auto simp:lefts_of_def)

   614 

   615 

   616 subsubsection {* Intialization *}

   617 

   618 text {*

   619   The following several lemmas until @{text "init_ES_satisfy_Inv"} shows that

   620   the initial equational system satisfies invariant @{text "Inv"}.

   621   *}

   622 

   623 lemma defined_by_str:

   624   "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"

   625 by (auto simp:quotient_def Image_def str_eq_rel_def)

   626 

   627 lemma every_eqclass_has_transition:

   628   assumes has_str: "s @ [c] \<in> X"

   629   and     in_CS:   "X \<in> UNIV // (\<approx>Lang)"

   630   obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"

   631 proof -

   632   def Y \<equiv> "(\<approx>Lang) `` {s}"

   633   have "Y \<in> UNIV // (\<approx>Lang)" 

   634     unfolding Y_def quotient_def by auto

   635   moreover

   636   have "X = (\<approx>Lang) `` {s @ [c]}" 

   637     using has_str in_CS defined_by_str by blast

   638   then have "Y ;; {[c]} \<subseteq> X" 

   639     unfolding Y_def Image_def Seq_def

   640     unfolding str_eq_rel_def

   641     by clarsimp

   642   moreover

   643   have "s \<in> Y" unfolding Y_def 

   644     unfolding Image_def str_eq_rel_def by simp

   645   ultimately show thesis by (blast intro: that)

   646 qed

   647 

   648 lemma l_eq_r_in_eqs:

   649   assumes X_in_eqs: "(X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"

   650   shows "X = L xrhs"

   651 proof 

   652   show "X \<subseteq> L xrhs"

   653   proof

   654     fix x

   655     assume "(1)": "x \<in> X"

   656     show "x \<in> L xrhs"          

   657     proof (cases "x = []")

   658       assume empty: "x = []"

   659       thus ?thesis using X_in_eqs "(1)"

   660         by (auto simp:eqs_def init_rhs_def)

   661     next

   662       assume not_empty: "x \<noteq> []"

   663       then obtain clist c where decom: "x = clist @ [c]"

   664         by (case_tac x rule:rev_cases, auto)

   665       have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:eqs_def)

   666       then obtain Y 

   667         where "Y \<in> UNIV // (\<approx>Lang)" 

   668         and "Y ;; {[c]} \<subseteq> X"

   669         and "clist \<in> Y"

   670         using decom "(1)" every_eqclass_has_transition by blast

   671       hence 

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

   673         using "(1)" decom

   674         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)

   675       thus ?thesis using X_in_eqs "(1)"

   676         by (simp add:eqs_def init_rhs_def)

   677     qed

   678   qed

   679 next

   680   show "L xrhs \<subseteq> X" using X_in_eqs

   681     by (auto simp:eqs_def init_rhs_def) 

   682 qed

   683 

   684 lemma finite_init_rhs: 

   685   assumes finite: "finite CS"

   686   shows "finite (init_rhs CS X)"

   687 proof-

   688   have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")

   689   proof -

   690     def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" 

   691     def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"

   692     have "finite (CS \<times> (UNIV::char set))" using finite by auto

   693     hence "finite S" using S_def 

   694       by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)

   695     moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)

   696     ultimately show ?thesis 

   697       by auto

   698   qed

   699   thus ?thesis by (simp add:init_rhs_def)

   700 qed

   701 

   702 lemma init_ES_satisfy_Inv:

   703   assumes finite_CS: "finite (UNIV // (\<approx>Lang))"

   704   shows "Inv (eqs (UNIV // (\<approx>Lang)))"

   705 proof -

   706   have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS

   707     by (simp add:eqs_def)

   708   moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"     

   709     by (simp add:distinct_equas_def eqs_def)

   710   moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"

   711     by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps)

   712   moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))"

   713     using l_eq_r_in_eqs by (simp add:valid_eqns_def)

   714   moreover have "non_empty (eqs (UNIV // (\<approx>Lang)))"

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

   716   moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))"

   717     using finite_init_rhs[OF finite_CS] 

   718     by (auto simp:finite_rhs_def eqs_def)

   719   moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"

   720     by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)

   721   ultimately show ?thesis by (simp add:Inv_def)

   722 qed

   723 

   724 subsubsection {* 

   725   Interation step

   726   *}

   727 

   728 text {*

   729   From this point until @{text "iteration_step"}, it is proved

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

   731   decreasing the size of @{text "ES"}.

   732   *}

   733 lemma arden_variate_keeps_eq:

   734   assumes l_eq_r: "X = L rhs"

   735   and not_empty: "[] \<notin> L (rexp_of rhs X)"

   736   and finite: "finite rhs"

   737   shows "X = L (arden_variate X rhs)"

   738 proof -

   739   def A \<equiv> "L (rexp_of rhs X)"

   740   def b \<equiv> "rhs - items_of rhs X"

   741   def B \<equiv> "L b" 

   742   have "X = B ;; A\<star>"

   743   proof-

   744     have "rhs = items_of rhs X \<union> b" by (auto simp:b_def items_of_def)

   745     hence "L rhs = L(items_of rhs X \<union> b)" by simp

   746     hence "L rhs = L(items_of rhs X) \<union> B" by (simp only:L_rhs_union_distrib B_def)

   747     with lang_of_rexp_of

   748     have "L rhs = X ;; A \<union> B " using finite by (simp only:B_def b_def A_def)

   749     thus ?thesis

   750       using l_eq_r not_empty

   751       apply (drule_tac B = B and X = X in ardens_revised)

   752       by (auto simp:A_def simp del:L_rhs.simps)

   753   qed

   754   moreover have "L (arden_variate X rhs) = (B ;; A\<star>)" (is "?L = ?R")

   755     by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 

   756                   B_def A_def b_def L_rexp.simps seq_union_distrib)

   757    ultimately show ?thesis by simp

   758 qed 

   759 

   760 lemma append_keeps_finite:

   761   "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"

   762 by (auto simp:append_rhs_rexp_def)

   763 

   764 lemma arden_variate_keeps_finite:

   765   "finite rhs \<Longrightarrow> finite (arden_variate X rhs)"

   766 by (auto simp:arden_variate_def append_keeps_finite)

   767 

   768 lemma append_keeps_nonempty:

   769   "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"

   770 apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)

   771 by (case_tac x, auto simp:Seq_def)

   772 

   773 lemma nonempty_set_sub:

   774   "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)"

   775 by (auto simp:rhs_nonempty_def)

   776 

   777 lemma nonempty_set_union:

   778   "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"

   779 by (auto simp:rhs_nonempty_def)

   780 

   781 lemma arden_variate_keeps_nonempty:

   782   "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (arden_variate X rhs)"

   783 by (simp only:arden_variate_def append_keeps_nonempty nonempty_set_sub)

   784 

   785 

   786 lemma rhs_subst_keeps_nonempty:

   787   "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs_subst rhs X xrhs)"

   788 by (simp only:rhs_subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)

   789 

   790 lemma rhs_subst_keeps_eq:

   791   assumes substor: "X = L xrhs"

   792   and finite: "finite rhs"

   793   shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right")

   794 proof-

   795   def A \<equiv> "L (rhs - items_of rhs X)"

   796   have "?Left = A \<union> L (append_rhs_rexp xrhs (rexp_of rhs X))"

   797     by (simp only:rhs_subst_def L_rhs_union_distrib A_def)

   798   moreover have "?Right = A \<union> L (items_of rhs X)"

   799   proof-

   800     have "rhs = (rhs - items_of rhs X) \<union> (items_of rhs X)" by (auto simp:items_of_def)

   801     thus ?thesis by (simp only:L_rhs_union_distrib A_def)

   802   qed

   803   moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)" 

   804     using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)

   805   ultimately show ?thesis by simp

   806 qed

   807 

   808 lemma rhs_subst_keeps_finite_rhs:

   809   "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (rhs_subst rhs Y yrhs)"

   810 by (auto simp:rhs_subst_def append_keeps_finite)

   811 

   812 lemma eqs_subst_keeps_finite:

   813   assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"

   814   shows "finite (eqs_subst ES Y yrhs)"

   815 proof -

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

   817                                                                   (is "finite ?A")

   818   proof-

   819     def eqns' \<equiv> "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \<in> ES}"

   820     def h \<equiv> "\<lambda> ((Ya::string set), yrhsa). (Ya, rhs_subst yrhsa Y yrhs)"

   821     have "finite (h ` eqns')" using finite h_def eqns'_def by auto

   822     moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def)

   823     ultimately show ?thesis by auto      

   824   qed

   825   thus ?thesis by (simp add:eqs_subst_def)

   826 qed

   827 

   828 lemma eqs_subst_keeps_finite_rhs:

   829   "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (eqs_subst ES Y yrhs)"

   830 by (auto intro:rhs_subst_keeps_finite_rhs simp add:eqs_subst_def finite_rhs_def)

   831 

   832 lemma append_rhs_keeps_cls:

   833   "classes_of (append_rhs_rexp rhs r) = classes_of rhs"

   834 apply (auto simp:classes_of_def append_rhs_rexp_def)

   835 apply (case_tac xa, auto simp:image_def)

   836 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)

   837 

   838 lemma arden_variate_removes_cl:

   839   "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}"

   840 apply (simp add:arden_variate_def append_rhs_keeps_cls items_of_def)

   841 by (auto simp:classes_of_def)

   842 

   843 lemma lefts_of_keeps_cls:

   844   "lefts_of (eqs_subst ES Y yrhs) = lefts_of ES"

   845 by (auto simp:lefts_of_def eqs_subst_def)

   846 

   847 lemma rhs_subst_updates_cls:

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

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

   850 apply (simp only:rhs_subst_def append_rhs_keeps_cls 

   851                               classes_of_union_distrib[THEN sym])

   852 by (auto simp:classes_of_def items_of_def)

   853 

   854 lemma eqs_subst_keeps_self_contained:

   855   fixes Y

   856   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")

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

   858                                                    (is "self_contained ?B")

   859 proof-

   860   { fix X xrhs'

   861     assume "(X, xrhs') \<in> ?B"

   862     then obtain xrhs 

   863       where xrhs_xrhs': "xrhs' = rhs_subst xrhs Y (arden_variate Y yrhs)"

   864       and X_in: "(X, xrhs) \<in> ES" by (simp add:eqs_subst_def, blast)    

   865     have "classes_of xrhs' \<subseteq> lefts_of ?B"

   866     proof-

   867       have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def eqs_subst_def)

   868       moreover have "classes_of xrhs' \<subseteq> lefts_of ES"

   869       proof-

   870         have "classes_of xrhs' \<subseteq> 

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

   872         proof-

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

   874             using arden_variate_removes_cl by simp

   875           thus ?thesis using xrhs_xrhs' by (auto simp:rhs_subst_updates_cls)

   876         qed

   877         moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc

   878           apply (simp only:self_contained_def lefts_of_union_distrib[THEN sym])

   879           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)

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

   881           using sc 

   882           by (auto simp add:arden_variate_removes_cl self_contained_def lefts_of_def)

   883         ultimately show ?thesis by auto

   884       qed

   885       ultimately show ?thesis by simp

   886     qed

   887   } thus ?thesis by (auto simp only:eqs_subst_def self_contained_def)

   888 qed

   889 

   890 lemma eqs_subst_satisfy_Inv:

   891   assumes Inv_ES: "Inv (ES \<union> {(Y, yrhs)})"

   892   shows "Inv (eqs_subst ES Y (arden_variate Y yrhs))"

   893 proof -  

   894   have finite_yrhs: "finite yrhs" 

   895     using Inv_ES by (auto simp:Inv_def finite_rhs_def)

   896   have nonempty_yrhs: "rhs_nonempty yrhs" 

   897     using Inv_ES by (auto simp:Inv_def ardenable_def)

   898   have Y_eq_yrhs: "Y = L yrhs" 

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

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

   901     using Inv_ES

   902     by (auto simp:distinct_equas_def eqs_subst_def Inv_def)

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

   904     using Inv_ES by (simp add:Inv_def eqs_subst_keeps_finite)

   905   moreover have "finite_rhs (eqs_subst ES Y (arden_variate Y yrhs))"

   906   proof-

   907     have "finite_rhs ES" using Inv_ES 

   908       by (simp add:Inv_def finite_rhs_def)

   909     moreover have "finite (arden_variate Y yrhs)"

   910     proof -

   911       have "finite yrhs" using Inv_ES 

   912         by (auto simp:Inv_def finite_rhs_def)

   913       thus ?thesis using arden_variate_keeps_finite by simp

   914     qed

   915     ultimately show ?thesis 

   916       by (simp add:eqs_subst_keeps_finite_rhs)

   917   qed

   918   moreover have "ardenable (eqs_subst ES Y (arden_variate Y yrhs))"

   919   proof - 

   920     { fix X rhs

   921       assume "(X, rhs) \<in> ES"

   922       hence "rhs_nonempty rhs"  using prems Inv_ES  

   923         by (simp add:Inv_def ardenable_def)

   924       with nonempty_yrhs 

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

   926         by (simp add:nonempty_yrhs 

   927                rhs_subst_keeps_nonempty arden_variate_keeps_nonempty)

   928     } thus ?thesis by (auto simp add:ardenable_def eqs_subst_def)

   929   qed

   930   moreover have "valid_eqns (eqs_subst ES Y (arden_variate Y yrhs))"

   931   proof-

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

   933       using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs      

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

   935     thus ?thesis using Inv_ES 

   936       by (clarsimp simp add:valid_eqns_def 

   937               eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def

   938                    simp del:L_rhs.simps)

   939   qed

   940   moreover have 

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

   942     using Inv_ES by (auto simp:Inv_def non_empty_def eqs_subst_def)

   943   moreover 

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

   945     using Inv_ES eqs_subst_keeps_self_contained by (simp add:Inv_def)

   946   ultimately show ?thesis using Inv_ES by (simp add:Inv_def)

   947 qed

   948 

   949 lemma eqs_subst_card_le: 

   950   assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"

   951   shows "card (eqs_subst ES Y yrhs) <= card ES"

   952 proof-

   953   def f \<equiv> "\<lambda> x. ((fst x)::string set, rhs_subst (snd x) Y yrhs)"

   954   have "eqs_subst ES Y yrhs = f ` ES" 

   955     apply (auto simp:eqs_subst_def f_def image_def)

   956     by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+)

   957   thus ?thesis using finite by (auto intro:card_image_le)

   958 qed

   959 

   960 lemma eqs_subst_cls_remains: 

   961   "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (eqs_subst ES Y yrhs)"

   962 by (auto simp:eqs_subst_def)

   963 

   964 lemma card_noteq_1_has_more:

   965   assumes card:"card S \<noteq> 1"

   966   and e_in: "e \<in> S"

   967   and finite: "finite S"

   968   obtains e' where "e' \<in> S \<and> e \<noteq> e'" 

   969 proof-

   970   have "card (S - {e}) > 0"

   971   proof -

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

   973       by (case_tac "card S", auto) 

   974     thus ?thesis using finite e_in by auto

   975   qed

   976   hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)

   977   thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto

   978 qed

   979 

   980 lemma iteration_step: 

   981   assumes Inv_ES: "Inv ES"

   982   and    X_in_ES: "(X, xrhs) \<in> ES"

   983   and    not_T: "card ES \<noteq> 1"

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

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

   986 proof -

   987   have finite_ES: "finite ES" using Inv_ES by (simp add:Inv_def)

   988   then obtain Y yrhs 

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

   990     using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)

   991   def ES' == "ES - {(Y, yrhs)}"

   992   let ?ES'' = "eqs_subst ES' Y (arden_variate Y yrhs)"

   993   have "?P ?ES''"

   994   proof -

   995     have "Inv ?ES''" using Y_in_ES Inv_ES

   996       by (rule_tac eqs_subst_satisfy_Inv, simp add:ES'_def insert_absorb)

   997     moreover have "\<exists>xrhs'. (X, xrhs') \<in> ?ES''"  using not_eq X_in_ES

   998       by (rule_tac ES = ES' in eqs_subst_cls_remains, auto simp add:ES'_def)

   999     moreover have "(card ?ES'', card ES) \<in> less_than" 

  1000     proof -

  1001       have "finite ES'" using finite_ES ES'_def by auto

  1002       moreover have "card ES' < card ES" using finite_ES Y_in_ES

  1003         by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less)

  1004       ultimately show ?thesis 

  1005         by (auto dest:eqs_subst_card_le elim:le_less_trans)

  1006     qed

  1007     ultimately show ?thesis by simp

  1008   qed

  1009   thus ?thesis by blast

  1010 qed

  1011 

  1012 subsubsection {*

  1013   Conclusion of the proof

  1014   *}

  1015 

  1016 text {*

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

  1018   through a simple application of the iteration principle.

  1019 *}

  1020 

  1021 lemma iteration_conc: 

  1022   assumes history: "Inv ES"

  1023   and    X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"

  1024   shows 

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

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

  1027 proof (cases "card ES = 1")

  1028   case True

  1029   thus ?thesis using history X_in_ES

  1030     by blast

  1031 next

  1032   case False  

  1033   thus ?thesis using history iteration_step X_in_ES

  1034     by (rule_tac f = card in wf_iter, auto)

  1035 qed

  1036   

  1037 lemma last_cl_exists_rexp:

  1038   assumes ES_single: "ES = {(X, xrhs)}" 

  1039   and Inv_ES: "Inv ES"

  1040   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")

  1041 proof-

  1042   let ?A = "arden_variate X xrhs"

  1043   have "?P (rexp_of_lam ?A)"

  1044   proof -

  1045     have "L (rexp_of_lam ?A) = L (lam_of ?A)"

  1046     proof(rule rexp_of_lam_eq_lam_set)

  1047       show "finite (arden_variate X xrhs)" using Inv_ES ES_single 

  1048         by (rule_tac arden_variate_keeps_finite, 

  1049                        auto simp add:Inv_def finite_rhs_def)

  1050     qed

  1051     also have "\<dots> = L ?A"

  1052     proof-

  1053       have "lam_of ?A = ?A"

  1054       proof-

  1055         have "classes_of ?A = {}" using Inv_ES ES_single

  1056           by (simp add:arden_variate_removes_cl 

  1057                        self_contained_def Inv_def lefts_of_def) 

  1058         thus ?thesis 

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

  1060       qed

  1061       thus ?thesis by simp

  1062     qed

  1063     also have "\<dots> = X"

  1064     proof(rule arden_variate_keeps_eq [THEN sym])

  1065       show "X = L xrhs" using Inv_ES ES_single 

  1066         by (auto simp only:Inv_def valid_eqns_def)  

  1067     next

  1068       from Inv_ES ES_single show "[] \<notin> L (rexp_of xrhs X)"

  1069         by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def)

  1070     next

  1071       from Inv_ES ES_single show "finite xrhs" 

  1072         by (simp add:Inv_def finite_rhs_def)

  1073     qed

  1074     finally show ?thesis by simp

  1075   qed

  1076   thus ?thesis by auto

  1077 qed

  1078    

  1079 lemma every_eqcl_has_reg: 

  1080   assumes finite_CS: "finite (UNIV // (\<approx>Lang))"

  1081   and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))"

  1082   shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")

  1083 proof -

  1084   from X_in_CS have "\<exists> xrhs. (X, xrhs) \<in> (eqs (UNIV  // (\<approx>Lang)))"

  1085     by (auto simp:eqs_def init_rhs_def)

  1086   then obtain ES xrhs where Inv_ES: "Inv ES" 

  1087     and X_in_ES: "(X, xrhs) \<in> ES"

  1088     and card_ES: "card ES = 1"

  1089     using finite_CS X_in_CS init_ES_satisfy_Inv iteration_conc

  1090     by blast

  1091   hence ES_single_equa: "ES = {(X, xrhs)}" 

  1092     by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) 

  1093   thus ?thesis using Inv_ES

  1094     by (rule last_cl_exists_rexp)

  1095 qed

  1096 

  1097 lemma finals_in_partitions:

  1098   "finals Lang \<subseteq> (UNIV // (\<approx>Lang))"

  1099   by (auto simp:finals_def quotient_def)   

  1100 

  1101 theorem hard_direction: 

  1102   assumes finite_CS: "finite (UNIV // (\<approx>Lang))"

  1103   shows   "\<exists> (reg::rexp). Lang = L reg"

  1104 proof -

  1105   have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg" 

  1106     using finite_CS every_eqcl_has_reg by blast

  1107   then obtain f 

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

  1109     by (auto dest:bchoice)

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

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

  1112   also have "\<dots> = L (folds ALT NULL rs)" 

  1113   proof -

  1114     have "finite rs"

  1115     proof -

  1116       have "finite (finals Lang)" 

  1117         using finite_CS finals_in_partitions[of "Lang"]   

  1118         by (erule_tac finite_subset, simp)

  1119       thus ?thesis using rs_def by auto

  1120     qed

  1121     thus ?thesis 

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

  1123   qed

  1124   finally show ?thesis by blast

  1125 qed 

  1126 

  1127 

  1128 

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