1 theory Myhill_1

     2   imports Main 

     3 begin

     4 

     5 (*

     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 

    27 section {* Preliminary definitions *}

    28 

    29 types lang = "string set"

    30 

    31 text {*  Sequential composition of two languages *}

    32 

    33 definition 

    34   Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)

    35 where 

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

    37 

    38 

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

    40 

    41 lemma seq_add_left:

    42   assumes a: "A = B"

    43   shows "C ;; A = C ;; B"

    44 using a by simp

    45 

    46 lemma seq_union_distrib_right:

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

    48 unfolding Seq_def by auto

    49 

    50 lemma seq_union_distrib_left:

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

    52 unfolding Seq_def by  auto

    53 

    54 lemma seq_intro:

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

    56   shows "x @ y \<in> A ;; B "

    57 using a by (auto simp: Seq_def)

    58 

    59 lemma seq_assoc:

    60   shows "(A ;; B) ;; C = A ;; (B ;; C)"

    61 unfolding Seq_def

    62 apply(auto)

    63 apply(blast)

    64 by (metis append_assoc)

    65 

    66 lemma seq_empty [simp]:

    67   shows "A ;; {[]} = A"

    68   and   "{[]} ;; A = A"

    69 by (simp_all add: Seq_def)

    70 

    71 

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

    73 

    74 fun 

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

    76 where

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

    78 | "A \<up> (Suc n) =  A ;; (A \<up> n)" 

    79 

    80 definition

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

    82 where

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

    84 

    85 

    86 lemma star_start[intro]:

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

    88 proof -

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

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

    91 qed

    92 

    93 lemma star_step [intro]:

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

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

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

    97 proof -

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

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

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

   101 qed

   102 

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

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

   105   and     b: "P []"

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

   107   shows "P x"

   108 proof -

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

   110   then show "P x"

   111     by (induct n arbitrary: x)

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

   113 qed

   114     

   115 lemma star_intro1:

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

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

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

   119 using a b

   120 by (induct rule: star_induct) (auto)

   121 

   122 lemma star_intro2: 

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

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

   125 proof -

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

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

   128 qed

   129 

   130 lemma star_intro3:

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

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

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

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

   135 

   136 lemma star_cases:

   137   shows "A\<star> =  {[]} \<union> A ;; A\<star>"

   138 proof

   139   { fix x

   140     have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"

   141       unfolding Seq_def

   142     by (induct rule: star_induct) (auto)

   143   }

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

   145 next

   146   show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"

   147     unfolding Seq_def by auto

   148 qed

   149 

   150 lemma star_decom: 

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

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

   153 using a

   154 apply(induct rule: star_induct)

   155 apply(simp)

   156 apply(blast)

   157 done

   158 

   159 lemma

   160   shows seq_Union_left:  "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"

   161   and   seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"

   162 unfolding Seq_def by auto

   163 

   164 lemma seq_pow_comm:

   165   shows "A ;; (A \<up> n) = (A \<up> n) ;; A"

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

   167 

   168 lemma seq_star_comm:

   169   shows "A ;; A\<star> = A\<star> ;; A"

   170 unfolding Star_def

   171 unfolding seq_Union_left

   172 unfolding seq_pow_comm

   173 unfolding seq_Union_right 

   174 by simp

   175 

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

   177 

   178 lemma pow_length:

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

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

   181   shows "n < length s"

   182 using b

   183 proof (induct n arbitrary: s)

   184   case 0

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

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

   187   then show "0 < length s" by auto

   188 next

   189   case (Suc n)

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

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

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

   193     by (auto simp add: Seq_def)

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

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

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

   197     by (simp only: length_append)

   198 qed

   199 

   200 lemma seq_pow_length:

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

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

   203   shows "n < length s"

   204 proof -

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

   206     unfolding Seq_def by auto

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

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

   209 qed

   210 

   211 

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

   213 

   214 

   215 text {*  A helper lemma for Arden *}

   216 

   217 lemma ardens_helper:

   218   assumes eq: "X = X ;; A \<union> B"

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

   220 proof (induct n)

   221   case 0 

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

   223     using eq by simp

   224 next

   225   case (Suc n)

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

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

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

   229     by (simp add: seq_union_distrib_right seq_assoc)

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

   231     by (auto simp add: le_Suc_eq)

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

   233 qed

   234 

   235 theorem ardens_revised:

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

   237   shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"

   238 proof

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

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

   241     unfolding seq_star_comm[symmetric]

   242     by (rule star_cases)

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

   244     by (rule seq_add_left)

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

   246     unfolding seq_union_distrib_left by simp

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

   248     by (simp only: seq_assoc)

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

   250     using eq by blast 

   251 next

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

   253   { fix n::nat

   254     have "B ;; (A \<up> n) \<subseteq> X" using ardens_helper[OF eq, of "n"] by auto }

   255   then have "B ;; A\<star> \<subseteq> X" 

   256     unfolding Seq_def Star_def UNION_def

   257     by auto

   258   moreover

   259   { fix s::string

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

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

   262       using seq_pow_length[OF nemp] by blast

   263     assume "s \<in> X"

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

   265       using ardens_helper[OF eq, of "k"] by auto

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

   267     moreover

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

   269     ultimately 

   270     have "s \<in> B ;; A\<star>" 

   271       unfolding seq_Union_left Star_def

   272       by auto }

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

   274   ultimately 

   275   show "X = B ;; A\<star>" by simp

   276 qed

   277 

   278 

   279 section {* Regular Expressions *}

   280 

   281 datatype rexp =

   282   NULL

   283 | EMPTY

   284 | CHAR char

   285 | SEQ rexp rexp

   286 | ALT rexp rexp

   287 | STAR rexp

   288 

   289 

   290 text {* 

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

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

   293 *}

   294 

   295 consts L:: "'a \<Rightarrow> lang"

   296 

   297 text {* The @{text "L (rexp)"} for regular expressions. *}

   298 

   299 overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"

   300 begin

   301 fun

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

   303 where

   304     "L_rexp (NULL) = {}"

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

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

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

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

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

   310 end

   311 

   312 

   313 section {* Folds for Sets *}

   314 

   315 text {*

   316   To obtain equational system out of finite set of equivalence classes, a fold operation

   317   on finite sets @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "folds"}

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

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

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

   321 *}

   322 

   323 

   324 definition 

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

   326 where

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

   328 

   329 abbreviation

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

   331 where

   332   "\<Uplus>A == folds ALT NULL A"

   333 

   334 text {* 

   335   The following lemma ensures that the arbitrary choice made by the 

   336   @{text "SOME"} in @{text "folds"} does not affect the @{text "L"}-value 

   337   of the resultant regular expression. 

   338 *}

   339 

   340 lemma folds_alt_simp [simp]:

   341   assumes a: "finite rs"

   342   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"

   343 apply(rule set_eqI)

   344 apply(simp add: folds_def)

   345 apply(rule someI2_ex)

   346 apply(rule_tac finite_imp_fold_graph[OF a])

   347 apply(erule fold_graph.induct)

   348 apply(auto)

   349 done

   350 

   351 

   352 text {* Just a technical lemma for collections and pairs *}

   353 

   354 lemma Pair_Collect[simp]:

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

   356 by simp

   357 

   358 text {*

   359   @{text "\<approx>A"} is an equivalence class defined by language @{text "A"}.

   360 *}

   361 definition

   362   str_eq_rel :: "lang \<Rightarrow> (string \<times> string) set" ("\<approx>_" [100] 100)

   363 where

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

   365 

   366 text {* 

   367   Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"} singles out 

   368   those which contains the strings from @{text "A"}.

   369 *}

   370 

   371 definition 

   372   finals :: "lang \<Rightarrow> lang set"

   373 where

   374   "finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"

   375 

   376 text {* 

   377   The following lemma establishes the relationshipt between 

   378   @{text "finals A"} and @{text "A"}.

   379 *}

   380 

   381 lemma lang_is_union_of_finals: 

   382   shows "A = \<Union> finals A"

   383 unfolding finals_def

   384 unfolding Image_def

   385 unfolding str_eq_rel_def

   386 apply(auto)

   387 apply(drule_tac x = "[]" in spec)

   388 apply(auto)

   389 done

   390 

   391 lemma finals_in_partitions:

   392   shows "finals A \<subseteq> (UNIV // \<approx>A)"

   393 unfolding finals_def

   394 unfolding quotient_def

   395 by auto

   396 

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

   398 

   399 text {* 

   400   The relationship between equivalent classes can be described by an

   401   equational system.  For example, in equational system \eqref{example_eqns},

   402   $X_0, X_1$ are equivalent classes. The first equation says every string in

   403   $X_0$ is obtained either by appending one $b$ to a string in $X_0$ or by

   404   appending one $a$ to a string in $X_1$ or just be an empty string

   405   (represented by the regular expression $\lambda$). Similary, the second

   406   equation tells how the strings inside $X_1$ are composed.

   407 

   408   \begin{equation}\label{example_eqns}

   409     \begin{aligned}

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

   411       X_1 & = X_0 a + X_1 b

   412     \end{aligned}

   413   \end{equation}

   414 

   415   \noindent

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

   417   type @{text "rhs_item"}, mnemonic for 'right hand side item'.  Generally,

   418   there are two kinds of right hand side items, one kind corresponds to pure

   419   regular expressions, like the $\lambda$ in \eqref{example_eqns}, the other

   420   kind corresponds to transitions from one one equivalent class to another,

   421   like the $X_0 b, X_1 a$ etc.

   422 

   423 *}

   424 

   425 datatype rhs_item = 

   426    Lam "rexp"            (* Lambda *)

   427  | Trn "lang" "rexp"     (* Transition *)

   428 

   429 

   430 text {*

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

   432   repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is 

   433   represented by @{term "Trn X\<^isub>0 (CHAR a)"}.

   434 *}

   435 

   436 text {*

   437   Every right-hand side item @{text "itm"} defines a language given 

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

   439 *}

   440 

   441 overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> lang"

   442 begin

   443   fun L_rhs_e:: "rhs_item \<Rightarrow> lang"

   444   where

   445     "L_rhs_e (Lam r) = L r" 

   446   | "L_rhs_e (Trn X r) = X ;; L r"

   447 end

   448 

   449 text {*

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

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

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

   453 *}

   454 

   455 overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> lang"

   456 begin

   457    fun L_rhs:: "rhs_item set \<Rightarrow> lang"

   458    where 

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

   460 end

   461 

   462 text {* 

   463   Given a set of equivalence classes @{text "CS"} and one equivalence class @{text "X"} among

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

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

   466   is:

   467 *}

   468 

   469 definition 

   470   transition :: "lang \<Rightarrow> rexp \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)

   471 where

   472   "Y \<Turnstile>r\<Rightarrow> X \<equiv> Y ;; (L r) \<subseteq> X"

   473 

   474 definition

   475   "init_rhs CS X \<equiv>  

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

   477           {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}

   478       else 

   479           {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"

   480 

   481 text {*

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

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

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

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

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

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

   488 

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

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

   491 *}

   492 

   493 

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

   495 

   496 

   497 

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

   499 

   500 text {* 

   501   The following @{text "trns_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.

   502 *}

   503 

   504 definition

   505   "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}"

   506 

   507 text {*

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

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

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

   511 *}

   512 

   513 fun 

   514   attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"

   515 where

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

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

   518 

   519 text {* 

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

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

   522 *}

   523 

   524 definition

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

   526 

   527 text {*

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

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

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

   531   After this transformation, the recursive occurence of @{text "X"}

   532   in @{text "rhs"} will be eliminated, while the string set defined 

   533   by @{text "rhs"} is kept unchanged.

   534 *}

   535 

   536 definition 

   537   "arden_variate X rhs \<equiv> 

   538         append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"

   539 

   540 

   541 (*********** substitution of ES *************)

   542 

   543 text {* 

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

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

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

   547   A litte thought may reveal that the final result

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

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

   550  *}

   551 

   552 definition 

   553   "rhs_subst rhs X xrhs \<equiv> 

   554         (rhs - (trns_of rhs X)) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"

   555 

   556 text {*

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

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

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

   560   *}

   561 

   562 definition

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

   564 

   565 text {*

   566   The computation of regular expressions for equivalence classes is accomplished

   567   using a iteration principle given by the following lemma.

   568 *}

   569 

   570 lemma wf_iter [rule_format]: 

   571   fixes f

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

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

   574 proof(induct e rule: wf_induct 

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

   576   fix x 

   577   assume h [rule_format]: 

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

   579     and px: "P x"

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

   581   proof(cases "Q x")

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

   583   next

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

   585     from step [OF px nq]

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

   587     show ?thesis

   588     proof(rule h)

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

   590 	by (simp add:inv_image_def)

   591     next

   592       from pe' show "P e'" .

   593     qed

   594   qed

   595 qed

   596 

   597 text {*

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

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

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

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

   602 *}

   603 

   604 text {* 

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

   606   *}

   607 

   608 definition 

   609   "distinct_equas ES \<equiv> 

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

   611 

   612 text {* 

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

   614   *}

   615 definition 

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

   617 

   618 text {*

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

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

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

   622   *}

   623 

   624 definition 

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

   626 

   627 text {*

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

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

   630   *}

   631 

   632 definition 

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

   634 

   635 (* The following non_empty seems useless. *)

   636 definition 

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

   638 

   639 text {*

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

   641   *}

   642 definition

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

   644 

   645 text {*

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

   647   occuring in @{text "rhs"}.

   648   *}

   649 definition 

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

   651 

   652 text {*

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

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

   655   *}

   656 definition

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

   658 

   659 text {*

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

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

   662   equation in @{text "ES"}.

   663   *}

   664 definition 

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

   666 

   667 

   668 text {*

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

   670   *}

   671 definition 

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

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

   674 

   675 subsection {* The proof of this direction *}

   676 

   677 subsubsection {* Basic properties *}

   678 

   679 text {*

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

   681 *}

   682 

   683 lemma L_rhs_union_distrib:

   684   fixes A B::"rhs_item set"

   685   shows "L A \<union> L B = L (A \<union> B)"

   686 by simp

   687 

   688 lemma finite_Trn:

   689   assumes fin: "finite rhs"

   690   shows "finite {r. Trn Y r \<in> rhs}"

   691 proof -

   692   have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}"

   693     by (rule rev_finite_subset[OF fin]) (auto)

   694   then have "finite ((\<lambda>(Y, r). Trn Y r) ` {(Y, r) | Y r. Trn Y r \<in> rhs})"

   695     by (simp add: image_Collect)

   696   then have "finite {(Y, r) | Y r. Trn Y r \<in> rhs}"

   697     by (erule_tac finite_imageD) (simp add: inj_on_def)

   698   then show "finite {r. Trn Y r \<in> rhs}"

   699     by (erule_tac f="snd" in finite_surj) (auto simp add: image_def)

   700 qed

   701 

   702 lemma finite_Lam:

   703   assumes fin:"finite rhs"

   704   shows "finite {r. Lam r \<in> rhs}"

   705 proof -

   706   have "finite {Lam r | r. Lam r \<in> rhs}"

   707     by (rule rev_finite_subset[OF fin]) (auto)

   708   then show "finite {r. Lam r \<in> rhs}"

   709     apply(simp add: image_Collect[symmetric])

   710     apply(erule finite_imageD)

   711     apply(auto simp add: inj_on_def)

   712     done

   713 qed

   714 

   715 lemma rexp_of_empty:

   716   assumes finite:"finite rhs"

   717   and nonempty:"rhs_nonempty rhs"

   718   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"

   719 using finite nonempty rhs_nonempty_def

   720 using finite_Trn[OF finite]

   721 by (auto)

   722 

   723 lemma [intro!]:

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

   725 

   726 lemma lang_of_rexp_of:

   727   assumes finite:"finite rhs"

   728   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"

   729 proof -

   730   have "finite {r. Trn X r \<in> rhs}" 

   731     by (rule finite_Trn[OF finite]) 

   732   then show ?thesis

   733     apply(auto simp add: Seq_def)

   734     apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)

   735     apply(rule_tac x= "Trn X xa" in exI)

   736     apply(auto simp: Seq_def)

   737     done

   738 qed

   739 

   740 lemma rexp_of_lam_eq_lam_set:

   741   assumes fin: "finite rhs"

   742   shows "L (\<Uplus>{r. Lam r \<in> rhs}) = L ({Lam r | r. Lam r \<in> rhs})"

   743 proof -

   744   have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam)

   745   then show ?thesis by auto

   746 qed

   747 

   748 lemma [simp]:

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

   750 apply (cases xb, auto simp: Seq_def)

   751 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)

   752 apply(auto simp: Seq_def)

   753 done

   754 

   755 lemma lang_of_append_rhs:

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

   757 apply (auto simp:append_rhs_rexp_def image_def)

   758 apply (auto simp:Seq_def)

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

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

   761 

   762 lemma classes_of_union_distrib:

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

   764 by (auto simp add:classes_of_def)

   765 

   766 lemma lefts_of_union_distrib:

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

   768 by (auto simp:lefts_of_def)

   769 

   770 

   771 subsubsection {* Intialization *}

   772 

   773 text {*

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

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

   776 *}

   777 

   778 lemma defined_by_str:

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

   780 by (auto simp:quotient_def Image_def str_eq_rel_def)

   781 

   782 lemma every_eqclass_has_transition:

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

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

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

   786 proof -

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

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

   789     unfolding Y_def quotient_def by auto

   790   moreover

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

   792     using has_str in_CS defined_by_str by blast

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

   794     unfolding Y_def Image_def Seq_def

   795     unfolding str_eq_rel_def

   796     by clarsimp

   797   moreover

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

   799     unfolding Image_def str_eq_rel_def by simp

   800   ultimately show thesis by (blast intro: that)

   801 qed

   802 

   803 lemma l_eq_r_in_eqs:

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

   805   shows "X = L xrhs"

   806 proof 

   807   show "X \<subseteq> L xrhs"

   808   proof

   809     fix x

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

   811     show "x \<in> L xrhs"          

   812     proof (cases "x = []")

   813       assume empty: "x = []"

   814       thus ?thesis using X_in_eqs "(1)"

   815         by (auto simp:eqs_def init_rhs_def)

   816     next

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

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

   819         by (case_tac x rule:rev_cases, auto)

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

   821       then obtain Y 

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

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

   824         and "clist \<in> Y"

   825         using decom "(1)" every_eqclass_has_transition by blast

   826       hence 

   827         "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"

   828         unfolding transition_def

   829 	using "(1)" decom

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

   831       thus ?thesis using X_in_eqs "(1)"	

   832         by (simp add: eqs_def init_rhs_def)

   833     qed

   834   qed

   835 next

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

   837     by (auto simp:eqs_def init_rhs_def transition_def) 

   838 qed

   839 

   840 lemma finite_init_rhs: 

   841   assumes finite: "finite CS"

   842   shows "finite (init_rhs CS X)"

   843 proof-

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

   845   proof -

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

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

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

   849     hence "finite S" using S_def 

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

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

   852     ultimately show ?thesis 

   853       by auto

   854   qed

   855   thus ?thesis by (simp add:init_rhs_def transition_def)

   856 qed

   857 

   858 lemma init_ES_satisfy_Inv:

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

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

   861 proof -

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

   863     by (simp add:eqs_def)

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

   865     by (simp add:distinct_equas_def eqs_def)

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

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

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

   869     using l_eq_r_in_eqs by (simp add:valid_eqns_def)

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

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

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

   873     using finite_init_rhs[OF finite_CS] 

   874     by (auto simp:finite_rhs_def eqs_def)

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

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

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

   878 qed

   879 

   880 subsubsection {* 

   881   Interation step

   882   *}

   883 

   884 text {*

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

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

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

   888 *}

   889 

   890 lemma arden_variate_keeps_eq:

   891   assumes l_eq_r: "X = L rhs"

   892   and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"

   893   and finite: "finite rhs"

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

   895 proof -

   896   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"

   897   def b \<equiv> "rhs - trns_of rhs X"

   898   def B \<equiv> "L b" 

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

   900   proof-

   901     have "L rhs = L(trns_of rhs X \<union> b)" by (auto simp: b_def trns_of_def)

   902     also have "\<dots> = X ;; A \<union> B"

   903       unfolding trns_of_def

   904       unfolding L_rhs_union_distrib[symmetric]

   905       by (simp only: lang_of_rexp_of finite B_def A_def)

   906     finally show ?thesis

   907       using l_eq_r not_empty

   908       apply(rule_tac ardens_revised[THEN iffD1])

   909       apply(simp add: A_def)

   910       apply(simp)

   911       done

   912   qed

   913   moreover have "L (arden_variate X rhs) = (B ;; A\<star>)"

   914     by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 

   915                   B_def A_def b_def L_rexp.simps seq_union_distrib_left)

   916    ultimately show ?thesis by simp

   917 qed 

   918 

   919 lemma append_keeps_finite:

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

   921 by (auto simp:append_rhs_rexp_def)

   922 

   923 lemma arden_variate_keeps_finite:

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

   925 by (auto simp:arden_variate_def append_keeps_finite)

   926 

   927 lemma append_keeps_nonempty:

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

   929 apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)

   930 by (case_tac x, auto simp:Seq_def)

   931 

   932 lemma nonempty_set_sub:

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

   934 by (auto simp:rhs_nonempty_def)

   935 

   936 lemma nonempty_set_union:

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

   938 by (auto simp:rhs_nonempty_def)

   939 

   940 lemma arden_variate_keeps_nonempty:

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

   942 by (simp only:arden_variate_def append_keeps_nonempty nonempty_set_sub)

   943 

   944 

   945 lemma rhs_subst_keeps_nonempty:

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

   947 by (simp only:rhs_subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)

   948 

   949 lemma rhs_subst_keeps_eq:

   950   assumes substor: "X = L xrhs"

   951   and finite: "finite rhs"

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

   953 proof-

   954   def A \<equiv> "L (rhs - trns_of rhs X)"

   955   have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"

   956     unfolding rhs_subst_def

   957     unfolding L_rhs_union_distrib[symmetric]

   958     by (simp add: A_def)

   959   moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})"

   960   proof-

   961     have "rhs = (rhs - trns_of rhs X) \<union> (trns_of rhs X)" by (auto simp add: trns_of_def)

   962     thus ?thesis 

   963       unfolding A_def

   964       unfolding L_rhs_union_distrib

   965       unfolding trns_of_def

   966       by simp

   967   qed

   968   moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 

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

   970   ultimately show ?thesis by simp

   971 qed

   972 

   973 lemma rhs_subst_keeps_finite_rhs:

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

   975 by (auto simp:rhs_subst_def append_keeps_finite)

   976 

   977 lemma eqs_subst_keeps_finite:

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

   979   shows "finite (eqs_subst ES Y yrhs)"

   980 proof -

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

   982                                                                   (is "finite ?A")

   983   proof-

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

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

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

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

   988     ultimately show ?thesis by auto      

   989   qed

   990   thus ?thesis by (simp add:eqs_subst_def)

   991 qed

   992 

   993 lemma eqs_subst_keeps_finite_rhs:

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

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

   996 

   997 lemma append_rhs_keeps_cls:

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

   999 apply (auto simp:classes_of_def append_rhs_rexp_def)

  1000 apply (case_tac xa, auto simp:image_def)

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

  1002 

  1003 lemma arden_variate_removes_cl:

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

  1005 apply (simp add:arden_variate_def append_rhs_keeps_cls trns_of_def)

  1006 by (auto simp:classes_of_def)

  1007 

  1008 lemma lefts_of_keeps_cls:

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

  1010 by (auto simp:lefts_of_def eqs_subst_def)

  1011 

  1012 lemma rhs_subst_updates_cls:

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

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

  1015 apply (simp only:rhs_subst_def append_rhs_keeps_cls 

  1016                               classes_of_union_distrib[THEN sym])

  1017 by (auto simp:classes_of_def trns_of_def)

  1018 

  1019 lemma eqs_subst_keeps_self_contained:

  1020   fixes Y

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

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

  1023                                                    (is "self_contained ?B")

  1024 proof-

  1025   { fix X xrhs'

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

  1027     then obtain xrhs 

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

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

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

  1031     proof-

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

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

  1034       proof-

  1035         have "classes_of xrhs' \<subseteq> 

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

  1037         proof-

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

  1039             using arden_variate_removes_cl by simp

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

  1041         qed

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

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

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

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

  1046           using sc 

  1047           by (auto simp add:arden_variate_removes_cl self_contained_def lefts_of_def)

  1048         ultimately show ?thesis by auto

  1049       qed

  1050       ultimately show ?thesis by simp

  1051     qed

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

  1053 qed

  1054 

  1055 lemma eqs_subst_satisfy_Inv:

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

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

  1058 proof -  

  1059   have finite_yrhs: "finite yrhs" 

  1060     using Inv_ES by (auto simp:Inv_def finite_rhs_def)

  1061   have nonempty_yrhs: "rhs_nonempty yrhs" 

  1062     using Inv_ES by (auto simp:Inv_def ardenable_def)

  1063   have Y_eq_yrhs: "Y = L yrhs" 

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

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

  1066     using Inv_ES

  1067     by (auto simp:distinct_equas_def eqs_subst_def Inv_def)

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

  1069     using Inv_ES by (simp add:Inv_def eqs_subst_keeps_finite)

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

  1071   proof-

  1072     have "finite_rhs ES" using Inv_ES 

  1073       by (simp add:Inv_def finite_rhs_def)

  1074     moreover have "finite (arden_variate Y yrhs)"

  1075     proof -

  1076       have "finite yrhs" using Inv_ES 

  1077         by (auto simp:Inv_def finite_rhs_def)

  1078       thus ?thesis using arden_variate_keeps_finite by simp

  1079     qed

  1080     ultimately show ?thesis 

  1081       by (simp add:eqs_subst_keeps_finite_rhs)

  1082   qed

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

  1084   proof - 

  1085     { fix X rhs

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

  1087       hence "rhs_nonempty rhs"  using prems Inv_ES  

  1088         by (simp add:Inv_def ardenable_def)

  1089       with nonempty_yrhs 

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

  1091         by (simp add:nonempty_yrhs 

  1092                rhs_subst_keeps_nonempty arden_variate_keeps_nonempty)

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

  1094   qed

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

  1096   proof-

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

  1098       using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs      

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

  1100     thus ?thesis using Inv_ES 

  1101       by (clarsimp simp add:valid_eqns_def 

  1102               eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def

  1103                    simp del:L_rhs.simps)

  1104   qed

  1105   moreover have 

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

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

  1108   moreover 

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

  1110     using Inv_ES eqs_subst_keeps_self_contained by (simp add:Inv_def)

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

  1112 qed

  1113 

  1114 lemma eqs_subst_card_le: 

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

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

  1117 proof-

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

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

  1120     apply (auto simp:eqs_subst_def f_def image_def)

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

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

  1123 qed

  1124 

  1125 lemma eqs_subst_cls_remains: 

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

  1127 by (auto simp:eqs_subst_def)

  1128 

  1129 lemma card_noteq_1_has_more:

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

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

  1132   and finite: "finite S"

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

  1134 proof-

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