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

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

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

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

   184 qed

   184 qed

   185 

   185 

   186 

   186 

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

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

   190 

   188 

   191 text {*  A helper lemma for Arden *}

   189 text {*  A helper lemma for Arden *}

   192 

   190 

   193 lemma arden_helper:

   191 lemma arden_helper:

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

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

   304 apply(erule fold_graph.induct)

   302 apply(erule fold_graph.induct)

   305 apply(auto)

   303 apply(auto)

   306 done

   304 done

   307 

   305 

   308 

   306 

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

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

   311 

   308 

   312 

   309 

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

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

   314 

   311 

   347 lemma finals_in_partitions:

   344 lemma finals_in_partitions:

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

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

   349 unfolding finals_def quotient_def

   346 unfolding finals_def quotient_def

   350 by auto

   347 by auto

   351 

   348 

   353 section {* Equational systems *}

   349 section {* Equational systems *}

   355 

   350 

   356 text {* The two kinds of terms in the rhs of equations. *}

   351 text {* The two kinds of terms in the rhs of equations. *}

   357 

   352 

   358 datatype rhs_item = 

   353 datatype rhs_item = 

   359    Lam "rexp"            (* Lambda-marker *)

   354    Lam "rexp"            (* Lambda-marker *)

   496 (* test *)

   491 (* test *)

   497 partial_function (tailrec)

   492 partial_function (tailrec)

   498   solve

   493   solve

   499 where

   494 where

   500   "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"

   495   "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"

   503 

   496 

   504 

   497 

   505 text {*

   498 text {*

   506   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},

   499   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},

   507   the induction principle @{thm [source] while_rule} is used to proved the desired properties

   500   the induction principle @{thm [source] while_rule} is used to proved the desired properties