500 

   502   fixes v w

   503   assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"

   504   shows "(v::string) \<approx>(L\<^isub>1\<star>) w"

   505 proof-

   506     -- {* 

   507     \begin{minipage}{0.9\textwidth}

   508     According to the definition of @{text "\<approx>Lang"}, 

   509     proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to

   510     showing: for any string @{text "u"},

   511     if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa.

   512     The reasoning pattern for both directions are the same, as derived

   513     in the following:

   514     \end{minipage}

   515     *}

   516   { fix x y z

   517     assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 

   518       and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"

   519     have "y @ z \<in> L\<^isub>1\<star>"

   520     proof(cases "x = []")

   521       -- {* 

   522         The degenerated case when @{text "x"} is a null string is easy to prove:

   523         *}

   524       case True

   525       with tag_xy have "y = []" 

   526         by (auto simp:tag_str_STAR_def strict_prefix_def)

   527       thus ?thesis using xz_in_star True by simp

   528     next

   529         -- {*

   530         \begin{minipage}{0.9\textwidth}

   531         The case when @{text "x"} is not null, and

   532         @{text "x @ z"} is in @{text "L\<^isub>1\<star>"}, 

   533         \end{minipage}

   534         *}

   535       case False

   536       -- {* 

   537         \begin{minipage}{0.9\textwidth}

   538         Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splited

   539         by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such

   540         that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\<star>"},

   541         and there could be many such splittings.Therefore, the following set @{text "?S"} 

   542         is nonempty, and finite as well:

   543         \end{minipage}

   544         *}

   545       let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"

   546       have "finite ?S"

   547         by (rule_tac B = "{xa. xa < x}" in finite_subset, 

   548           auto simp:finite_strict_prefix_set)

   549       moreover have "?S \<noteq> {}" using False xz_in_star

   550         by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)

   551       -- {* Since @{text "?S"} is finite, we can always single out the longest

   552           and name it @{text "xa_max"}:

   553           *}

   554       ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 

   555         using finite_set_has_max by blast

   556       then obtain xa_max 

   557         where h1: "xa_max < x" 

   558         and h2: "xa_max \<in> L\<^isub>1\<star>" 

   559         and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>" 

   560         and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>  

   561                                      \<longrightarrow> length xa \<le> length xa_max"

   562         by blast

   563       -- {*

   564           \begin{minipage}{0.9\textwidth}

   565           By the equality of tags, the counterpart of @{text "xa_max"} among 

   566           @{text "y"}-prefixes, named @{text "ya"}, can be found:

   567           \end{minipage}

   568           *}

   569       obtain ya 

   570         where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" 

   571         and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"

   572       proof-

   573         from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = 

   574           {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")

   575           by (auto simp:tag_str_STAR_def)

   576         moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto

   577         ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp

   578         with prems show ?thesis apply 

   579           (simp add:Image_def str_eq_rel_def str_eq_def) by blast

   580       qed 

   581       -- {*

   582           \begin{minipage}{0.9\textwidth}

   583           If the following proposition can be proved, then the @{text "?thesis"}:

   584           @{text "y @ z \<in> L\<^isub>1\<star>"} is just a simple consequence.

   585           \end{minipage}

   586           *}

   587       have "(y - ya) @ z \<in> L\<^isub>1\<star>" 

   588       proof-

   589         -- {* The idea is to split the suffix @{text "z"} into @{text "za"} and @{text "zb"}, 

   590           such that: *}

   591         obtain za zb where eq_zab: "z = za @ zb" 

   592           and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"

   593         proof -

   594           -- {* 

   595             \begin{minipage}{0.9\textwidth}

   596             Since @{text  "(x - xa_max) @ z"} is in @{text "L\<^isub>1\<star>"}, it can be split into

   597             @{text "a"} and @{text "b"} such that:

   598             \end{minipage}

   599             *}

   600           from h1 have "(x - xa_max) @ z \<noteq> []" 

   601             by (auto simp:strict_prefix_def elim:prefixE)

   602           from star_decom [OF h3 this]

   603           obtain a b where a_in: "a \<in> L\<^isub>1" 

   604             and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 

   605             and ab_max: "(x - xa_max) @ z = a @ b" by blast

   606           -- {* Now the candiates for @{text "za"} and @{text "zb"} are found:*}

   607           let ?za = "a - (x - xa_max)" and ?zb = "b"

   608           have pfx: "(x - xa_max) \<le> a" (is "?P1") 

   609             and eq_z: "z = ?za @ ?zb" (is "?P2")

   610           proof -

   611             -- {* 

   612               \begin{minipage}{0.9\textwidth}

   613               Since @{text "(x - xa_max) @ z = a @ b"}, the string @{text "(x - xa_max) @ z"}

   614               could be splited in two ways:

   615               \end{minipage}

   616               *}

   617             have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> 

   618               (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" 

   619               using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)

   620             moreover {

   621               -- {* However, the undsired way can be refuted by absurdity: *}

   622               assume np: "a < (x - xa_max)" 

   623                 and b_eqs: "((x - xa_max) - a) @ z = b"

   624               have "False"

   625               proof -

   626                 let ?xa_max' = "xa_max @ a"

   627                 have "?xa_max' < x" 

   628                   using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 

   629                 moreover have "?xa_max' \<in> L\<^isub>1\<star>" 

   630                   using a_in h2 by (simp add:star_intro3) 

   631                 moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" 

   632                   using b_eqs b_in np h1 by (simp add:diff_diff_appd)

   633                 moreover have "\<not> (length ?xa_max' \<le> length xa_max)" 

   634                   using a_neq by simp

   635                 ultimately show ?thesis using h4 by blast

   636               qed }

   637             -- {* Now it can be shown that the splitting goes the way we desired. *}

   638             ultimately show ?P1 and ?P2 by auto

   639           qed

   640           hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)

   641           -- {* Now candidates @{text "?za"} and @{text "?zb"} have all the requred properteis. *}

   642           with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" 

   643             by (auto simp:str_eq_def str_eq_rel_def)

   644            with eq_z and b_in prems

   645           show ?thesis by blast

   646         qed

   647         -- {* 

   648             \begin{minipage}{0.9\textwidth}

   649             From the properties of @{text "za"} and @{text "zb"} such obtained,

   650               @{text "?thesis"} can be shown easily. 

   651             \end{minipage}

   652             *}

   653         from step [OF l_za ls_zb]

   654         have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" .

   655         with eq_zab show ?thesis by simp

   656       qed

   657       with h5 h6 show ?thesis 

   658         by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)

   659     qed

   660   } 

   661   -- {* By instantiating the reasoning pattern just derived for both directions:*} 

   662   from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]

   663   -- {* The thesis is proved as a trival consequence: *} 

   664     show  ?thesis by (unfold str_eq_def str_eq_rel_def, blast)

   665 qed

   666 

   667 

   668 lemma -- {* The oringal version with a poor readability*}

   793 subsubsection{* The conclusion *}