1 theory MyhillNerode

     2   imports "Main" "List_Prefix"

     3 begin

     4 

     5 text {* sequential composition of languages *}

     6 definition

     7   Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)

     8 where 

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

    10 

    11 inductive_set

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

    13   for L :: "string set"

    14 where

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

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

    17 

    18 theorem ardens_revised:

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

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

    21 proof

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

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

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

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

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

    27     by (auto) (metis append_assoc)+

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

    29 next

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

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

    32   show "X = B ;; A\<star>" sorry

    33 qed

    34 

    35 datatype rexp =

    36   NULL

    37 | EMPTY

    38 | CHAR char

    39 | SEQ rexp rexp

    40 | ALT rexp rexp

    41 | STAR rexp

    42 

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

    44 

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

    46 begin

    47 

    48 fun

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

    50 where

    51     "L_rexp (NULL) = {}"

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

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

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

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

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

    57 end

    58 

    59 definition 

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

    61 where

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

    63 

    64 lemma folds_simp_null [simp]:

    65   "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> L r)"

    66 apply (simp add: folds_def)

    67 apply (rule someI2_ex)

    68 apply (erule finite_imp_fold_graph)

    69 apply (erule fold_graph.induct)

    70 apply (auto)

    71 done

    72 

    73 lemma [simp]:

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

    75 by simp

    76 

    77 definition

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

    79 where

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

    81 

    82 definition

    83   str_eq_rel ("\<approx>_")

    84 where

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

    86 

    87 

    88 

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

    90 

    91 definition

    92   transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")

    93 where

    94   "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"

    95 

    96 definition

    97   transitions_rexp ("_ \<turnstile>\<rightarrow> _")

    98 where

    99   "Y \<turnstile>\<rightarrow> X \<equiv> folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"

   100 

   101 definition

   102   "init_rhs CS X \<equiv> if X = {[]} 

   103                    then {({[]}, EMPTY)} 

   104                    else if ([] \<in> X)

   105                         then insert ({[]}, EMPTY) {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}

   106                         else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"

   107 

   108 overloading L_rhs \<equiv> "L:: (string set \<times> rexp) set \<Rightarrow> string set"

   109 begin

   110 fun L_rhs:: "(string set \<times> rexp) set \<Rightarrow> string set"

   111 where

   112   "L_rhs rhs = \<Union> {(Y;; L r) | Y r . (Y, r) \<in> rhs}"

   113 end

   114 

   115 definition

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

   117 

   118 lemma [simp]:

   119   shows "finite (Y \<Turnstile>\<Rightarrow> X)"

   120 unfolding transitions_def

   121 by auto

   122 

   123 lemma defined_by_str:

   124   assumes "s \<in> X" 

   125   and "X \<in> UNIV // (\<approx>Lang)"

   126   shows "X = (\<approx>Lang) `` {s}"

   127 using assms

   128 unfolding quotient_def Image_def

   129 unfolding str_eq_rel_def str_eq_def

   130 by auto

   131 

   132 

   133 

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

   135 definition 

   136   "rexp_of rhs X \<equiv> folds ALT NULL {r. (X, r) \<in> rhs}"

   137 

   138 definition 

   139   "arden_variate X rhs \<equiv> {(Y, SEQ r (STAR (rexp_of rhs X)))| Y r. (Y, r) \<in> rhs \<and> Y \<noteq> X}"

   140 

   141 (************* rhs/equations property **************)

   142 

   143 definition 

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

   145 

   146 (*********** substitution of ES *************)

   147 

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

   149 definition 

   150   "rhs_subst rhs X xrhs \<equiv> {(Y, r) | Y r. Y \<noteq> X \<and> (Y, r) \<in> rhs} \<union> 

   151                           {(X, SEQ r\<^isub>1 r\<^isub>2 ) | r\<^isub>1 r\<^isub>2. (X, r\<^isub>1) \<in> xrhs \<and> (X, r\<^isub>2) \<in> rhs}"

   152 

   153 definition

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

   155 

   156 text {*

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

   158 *}

   159 

   160 definition 

   161   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> ([] \<notin> L (rexp_of rhs X)) \<and> X = L rhs"

   162 

   163 definition 

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

   165 

   166 definition 

   167   "self_contained ES \<equiv> \<forall> X xrhs. (X, xrhs) \<in> ES 

   168                              \<longrightarrow> (\<forall> Y r.(Y, r) \<in> xrhs \<and> Y \<noteq> {[]} \<longrightarrow> (\<exists> yrhs. (Y, yrhs) \<in> ES))"

   169 

   170 definition 

   171   "Inv ES \<equiv> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> non_empty ES \<and> self_contained ES"

   172 

   173 lemma wf_iter [rule_format]: 

   174   fixes f

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

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

   177 proof(induct e rule: wf_induct 

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

   179   fix x 

   180   assume h [rule_format]: 

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

   182     and px: "P x"

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

   184   proof(cases "Q x")

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

   186   next

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

   188     from step [OF px nq]

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

   190     show ?thesis

   191     proof(rule h)

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

   193 	by (simp add:inv_image_def)

   194     next

   195       from pe' show "P e'" .

   196     qed

   197   qed

   198 qed

   199 

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

   201 

   202 lemma init_ES_satisfy_Inv:

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

   204   and X_in_eq_cls: "X \<in> (UNIV // (\<approx>Lang))"

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

   206 proof -

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

   208     by (auto simp add:eqs_def)

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

   210     by (auto simp:distinct_equas_def eqs_def)

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

   212   proof-

   213     have "\<And> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<Longrightarrow> ([] \<notin> L (rexp_of rhs X))"

   214     proof 

   215       apply (auto simp:eqs_def rexp_of_def)

   216       sorry

   217     moreover have "\<forall> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<longrightarrow> X = L rhs"

   218       sorry

   219     ultimately show ?thesis by (simp add:ardenable_def)

   220   qed

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

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

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

   224     by (auto simp:self_contained_def eqs_def init_rhs_def)

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

   226 qed

   227 

   228 

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

   230 

   231 lemma iteration_step: 

   232   assumes Inv_ES: "Inv ES"

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

   234   and    not_T: "card ES > 1"

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

   236 proof -

   237 

   238  

   239 

   240 

   241 

   242  

   243 

   244 

   245 

   246   

   247 

   248 

   249 

   250 

   251 

   252 

   253 

   254 

   255 

   256 

   257 

   258 

   259 

   260 

   261 

   262 

   263 

   264 

   265 

   266 

   267 

   268 

   269 

   270 

   271 

   272 

   273 

   274 lemma distinct_rhs_equations:

   275   "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs"

   276 by (auto simp: equations_def equation_rhs_def distinct_rhs_def empty_rhs_def dest:no_two_cls_inters)

   277 

   278 lemma every_nonempty_eqclass_has_strings:

   279   "\<lbrakk>X \<in> (UNIV Quo Lang); X \<noteq> {[]}\<rbrakk> \<Longrightarrow> \<exists> clist. clist \<in> X \<and> clist \<noteq> []"

   280 by (auto simp:quot_def equiv_class_def equiv_str_def)

   281 

   282 lemma every_eqclass_is_derived_from_empty:

   283   assumes not_empty: "X \<noteq> {[]}"

   284   shows "X \<in> (UNIV Quo Lang) \<Longrightarrow> \<exists> clist. {[]};{clist} \<subseteq> X \<and> clist \<noteq> []"

   285 using not_empty

   286 apply (drule_tac every_nonempty_eqclass_has_strings, simp)

   287 by (auto intro:exI[where x = clist] simp:lang_seq_def)

   288 

   289 lemma equiv_str_in_CS:

   290   "\<lbrakk>clist\<rbrakk>Lang \<in> (UNIV Quo Lang)"

   291 by (auto simp:quot_def)

   292 

   293 lemma has_str_imp_defined_by_str:

   294   "\<lbrakk>str \<in> X; X \<in> UNIV Quo Lang\<rbrakk> \<Longrightarrow> X = \<lbrakk>str\<rbrakk>Lang"

   295 by (auto simp:quot_def equiv_class_def equiv_str_def)

   296 

   297 lemma every_eqclass_has_ascendent:

   298   assumes has_str: "clist @ [c] \<in> X"

   299   and     in_CS:   "X \<in> UNIV Quo Lang"

   300   shows "\<exists> Y. Y \<in> UNIV Quo Lang \<and> Y-c\<rightarrow>X \<and> clist \<in> Y" (is "\<exists> Y. ?P Y")

   301 proof -

   302   have "?P (\<lbrakk>clist\<rbrakk>Lang)" 

   303   proof -

   304     have "\<lbrakk>clist\<rbrakk>Lang \<in> UNIV Quo Lang"       

   305       by (simp add:quot_def, rule_tac x = clist in exI, simp)

   306     moreover have "\<lbrakk>clist\<rbrakk>Lang-c\<rightarrow>X" 

   307     proof -

   308       have "X = \<lbrakk>(clist @ [c])\<rbrakk>Lang" using has_str in_CS

   309         by (auto intro!:has_str_imp_defined_by_str)

   310       moreover have "\<forall> sl. sl \<in> \<lbrakk>clist\<rbrakk>Lang \<longrightarrow> sl @ [c] \<in> \<lbrakk>(clist @ [c])\<rbrakk>Lang"

   311         by (auto simp:equiv_class_def equiv_str_def)

   312       ultimately show ?thesis unfolding CT_def lang_seq_def

   313         by auto

   314     qed

   315     moreover have "clist \<in> \<lbrakk>clist\<rbrakk>Lang" 

   316       by (auto simp:equiv_str_def equiv_class_def)

   317     ultimately show "?P (\<lbrakk>clist\<rbrakk>Lang)" by simp

   318   qed

   319   thus ?thesis by blast

   320 qed

   321 

   322 lemma finite_charset_rS:

   323   "finite {CHAR c |c. Y-c\<rightarrow>X}"

   324 by (rule_tac A = UNIV and f = CHAR in finite_surj, auto)

   325 

   326 lemma l_eq_r_in_equations:

   327   assumes X_in_equas: "(X, xrhs) \<in> equations (UNIV Quo Lang)"

   328   shows "X = L xrhs"    

   329 proof (cases "X = {[]}")

   330   case True

   331   thus ?thesis using X_in_equas 

   332     by (simp add:equations_def equation_rhs_def lang_seq_def)

   333 next

   334   case False 

   335   show ?thesis

   336   proof 

   337     show "X \<subseteq> L xrhs"

   338     proof

   339       fix x

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

   341       show "x \<in> L xrhs"          

   342       proof (cases "x = []")

   343         assume empty: "x = []"

   344         hence "x \<in> L (empty_rhs X)" using "(1)"

   345           by (auto simp:empty_rhs_def lang_seq_def)

   346         thus ?thesis using X_in_equas False empty "(1)" 

   347           unfolding equations_def equation_rhs_def by auto

   348       next

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

   350         hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto)

   351         then obtain clist c where decom: "x = clist @ [c]" by blast

   352         moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>

   353           \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

   354         proof -

   355           fix Y

   356           assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang"

   357             and Y_CT_X: "Y-c\<rightarrow>X"

   358             and clist_in_Y: "clist \<in> Y"

   359           with finite_charset_rS 

   360           show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

   361             by (auto simp :fold_alt_null_eqs)

   362         qed

   363         hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" 

   364           using X_in_equas False not_empty "(1)" decom

   365           by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def)

   366         then obtain Xa where 

   367           "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast

   368         hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" 

   369           using X_in_equas "(1)" decom

   370           by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa])

   371         thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def

   372           by auto

   373       qed

   374     qed

   375   next

   376     show "L xrhs \<subseteq> X"

   377     proof

   378       fix x 

   379       assume "(2)": "x \<in> L xrhs"

   380       have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"

   381         using finite_charset_rS

   382         by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)

   383       have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"

   384         by (simp add:empty_rhs_def split:if_splits)

   385       show "x \<in> X" using X_in_equas False "(2)"         

   386         by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def)

   387     qed

   388   qed

   389 qed

   390 

   391 

   392 

   393 lemma no_EMPTY_equations:

   394   "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs"

   395 apply (clarsimp simp add:equations_def equation_rhs_def)

   396 apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto)

   397 apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+

   398 done

   399 

   400 lemma init_ES_satisfy_ardenable:

   401   "(X, xrhs) \<in> equations (UNIV Quo Lang)  \<Longrightarrow> ardenable (X, xrhs)"  

   402   unfolding ardenable_def

   403   by (auto intro:distinct_rhs_equations no_EMPTY_equations simp:l_eq_r_in_equations simp del:L_rhs.simps)

   404 

   405 lemma init_ES_satisfy_Inv:

   406   assumes finite_CS: "finite (UNIV Quo Lang)"

   407   and X_in_eq_cls: "X \<in> UNIV Quo Lang"

   408   shows "Inv X (equations (UNIV Quo Lang))"

   409 proof -

   410   have "finite (equations (UNIV Quo Lang))" using finite_CS

   411     by (auto simp:equations_def)    

   412   moreover have "\<exists>rhs. (X, rhs) \<in> equations (UNIV Quo Lang)" using X_in_eq_cls 

   413     by (simp add:equations_def)

   414   moreover have "distinct_equas (equations (UNIV Quo Lang))" 

   415     by (auto simp:distinct_equas_def equations_def)

   416   moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow>

   417                  rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equations (UNIV Quo Lang)))" 

   418     apply (simp add:left_eq_cls_def equations_def rhs_eq_cls_def equation_rhs_def)

   419     by (auto simp:empty_rhs_def split:if_splits)

   420   moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> X \<noteq> {}"

   421     by (clarsimp simp:equations_def empty_notin_CS intro:classical)

   422   moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> ardenable (X, xrhs)"

   423     by (auto intro!:init_ES_satisfy_ardenable)

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

   425 qed

   426 

   427 

   428 text {* *********** END: proving the initial equation-system satisfies Inv ******* *}

   429 

   430 

   431 

   432 

   433 

   434 

   435 

   436 

   437 

   438 

   439 

   440 

   441 

   442 

   443 

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

   445 

   446 lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk>

   447        \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A "

   448 apply (case_tac "insert a A = {a}")

   449 by (auto simp:TCon_def)

   450 

   451 lemma not_T_atleast_2[rule_format]:

   452   "finite S \<Longrightarrow> \<forall> x. x \<in> S \<and> (\<not> TCon S)\<longrightarrow> (\<exists> y. x \<noteq> y \<and> y \<in> S)"

   453 apply (erule finite.induct, simp)

   454 apply (clarify, case_tac "x = a")

   455 by (erule not_T_aux, auto)

   456 

   457 lemma exist_another_equa: 

   458   "\<lbrakk>\<not> TCon ES; finite ES; distinct_equas ES; (X, rhl) \<in> ES\<rbrakk> \<Longrightarrow> \<exists> Y yrhl. (Y, yrhl) \<in> ES \<and> X \<noteq> Y"

   459 apply (drule not_T_atleast_2, simp)

   460 apply (clarsimp simp:distinct_equas_def)

   461 apply (drule_tac x= X in spec, drule_tac x = rhl in spec, drule_tac x = b in spec)

   462 by auto

   463 

   464 lemma Inv_mono_with_lambda:

   465   assumes Inv_ES: "Inv X ES"

   466   and X_noteq_Y:  "X \<noteq> {[]}"

   467   shows "Inv X (ES - {({[]}, yrhs)})"

   468 proof -

   469   have "finite (ES - {({[]}, yrhs)})" using Inv_ES

   470     by (simp add:Inv_def)

   471   moreover have "\<exists>rhs. (X, rhs) \<in> ES - {({[]}, yrhs)}" using Inv_ES X_noteq_Y

   472     by (simp add:Inv_def)

   473   moreover have "distinct_equas (ES - {({[]}, yrhs)})" using Inv_ES X_noteq_Y

   474     apply (clarsimp simp:Inv_def distinct_equas_def)

   475     by (drule_tac x = Xa in spec, simp)    

   476   moreover have "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>

   477                           ardenable (X, xrhs) \<and> X \<noteq> {}" using Inv_ES

   478     by (clarify, simp add:Inv_def)

   479   moreover 

   480   have "insert {[]} (left_eq_cls (ES - {({[]}, yrhs)})) = insert {[]} (left_eq_cls ES)"

   481     by (auto simp:left_eq_cls_def)

   482   hence "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>

   483                           rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (ES - {({[]}, yrhs)}))"

   484     using Inv_ES by (auto simp:Inv_def)

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

   486 qed

   487 

   488 lemma non_empty_card_prop:

   489   "finite ES \<Longrightarrow> \<forall>e. e \<in> ES \<longrightarrow> card ES - Suc 0 < card ES"

   490 apply (erule finite.induct, simp)

   491 apply (case_tac[!] "a \<in> A")

   492 by (auto simp:insert_absorb)

   493 

   494 lemma ardenable_prop:

   495   assumes not_lambda: "Y \<noteq> {[]}"

   496   and ardable: "ardenable (Y, yrhs)"

   497   shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'")

   498 proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")

   499   case True

   500   thus ?thesis 

   501   proof 

   502     fix reg

   503     assume self_contained: "(Y, reg) \<in> yrhs"

   504     show ?thesis 

   505     proof -

   506       have "?P (arden_variate Y reg yrhs)"

   507       proof -

   508         have "Y = L (arden_variate Y reg yrhs)" 

   509           using self_contained not_lambda ardable

   510           by (rule_tac arden_variate_valid, simp_all add:ardenable_def)

   511         moreover have "distinct_rhs (arden_variate Y reg yrhs)" 

   512           using ardable 

   513           by (auto simp:distinct_rhs_def arden_variate_def seq_rhs_r_def del_x_paired_def ardenable_def)

   514         moreover have "rhs_eq_cls (arden_variate Y reg yrhs) = rhs_eq_cls yrhs - {Y}"

   515         proof -

   516           have "\<And> rhs r. rhs_eq_cls (seq_rhs_r rhs r) = rhs_eq_cls rhs"

   517             apply (auto simp:rhs_eq_cls_def seq_rhs_r_def image_def)

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

   519           moreover have "\<And> rhs X. rhs_eq_cls (del_x_paired rhs X) = rhs_eq_cls rhs - {X}"

   520             by (auto simp:rhs_eq_cls_def del_x_paired_def)

   521           ultimately show ?thesis by (simp add:arden_variate_def)

   522         qed

   523         ultimately show ?thesis by simp

   524       qed

   525       thus ?thesis by (rule_tac x= "arden_variate Y reg yrhs" in exI, simp)

   526     qed

   527   qed

   528 next

   529   case False

   530   hence "(2)": "rhs_eq_cls yrhs - {Y} = rhs_eq_cls yrhs"

   531     by (auto simp:rhs_eq_cls_def)

   532   show ?thesis 

   533   proof -

   534     have "?P yrhs" using False ardable "(2)" 

   535       by (simp add:ardenable_def)      

   536     thus ?thesis by blast

   537   qed

   538 qed

   539 

   540 lemma equas_subst_f_del_no_other:

   541   assumes self_contained: "(Y, rhs) \<in> ES"

   542   shows "\<exists> rhs'. (Y, rhs') \<in> (equas_subst_f X xrhs ` ES)" (is "\<exists> rhs'. ?P rhs'")

   543 proof -

   544   have "\<exists> rhs'. equas_subst_f X xrhs (Y, rhs) = (Y, rhs')"

   545     by (auto simp:equas_subst_f_def)

   546   then obtain rhs' where "equas_subst_f X xrhs (Y, rhs) = (Y, rhs')" by blast

   547   hence "?P rhs'" unfolding image_def using self_contained

   548     by (auto intro:bexI[where x = "(Y, rhs)"])

   549   thus ?thesis by blast

   550 qed

   551 

   552 lemma del_x_paired_del_only_x: 

   553   "\<lbrakk>X \<noteq> Y; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> (X, rhs) \<in> del_x_paired ES Y"

   554 by (auto simp:del_x_paired_def)

   555 

   556 lemma equas_subst_del_no_other:

   557  "\<lbrakk>(X, rhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> (\<exists>rhs. (X, rhs) \<in> equas_subst ES Y rhs')"

   558 unfolding equas_subst_def

   559 apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other)

   560 by (erule exE, drule del_x_paired_del_only_x, auto)

   561 

   562 lemma equas_subst_holds_distinct:

   563   "distinct_equas ES \<Longrightarrow> distinct_equas (equas_subst ES Y rhs')"

   564 apply (clarsimp simp add:equas_subst_def distinct_equas_def del_x_paired_def equas_subst_f_def)

   565 by (auto split:if_splits)

   566 

   567 lemma del_x_paired_dels: 

   568   "(X, rhs) \<in> ES \<Longrightarrow> {Y. Y \<in> ES \<and> fst Y = X} \<inter> ES \<noteq> {}"

   569 by (auto)

   570 

   571 lemma del_x_paired_subset:

   572   "(X, rhs) \<in> ES \<Longrightarrow> ES - {Y. Y \<in> ES \<and> fst Y = X} \<subset> ES"

   573 apply (drule del_x_paired_dels)

   574 by auto

   575 

   576 lemma del_x_paired_card_less: 

   577   "\<lbrakk>finite ES; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> card (del_x_paired ES X) < card ES"

   578 apply (simp add:del_x_paired_def)

   579 apply (drule del_x_paired_subset)

   580 by (auto intro:psubset_card_mono)

   581 

   582 lemma equas_subst_card_less:

   583   "\<lbrakk>finite ES; (Y, yrhs) \<in> ES\<rbrakk> \<Longrightarrow> card (equas_subst ES Y rhs') < card ES"

   584 apply (simp add:equas_subst_def)

   585 apply (frule_tac h = "equas_subst_f Y rhs'" in finite_imageI)

   586 apply (drule_tac f = "equas_subst_f Y rhs'" in Finite_Set.card_image_le)

   587 apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other,erule exE)

   588 by (drule del_x_paired_card_less, auto)

   589 

   590 lemma equas_subst_holds_distinct_rhs:

   591   assumes   dist': "distinct_rhs yrhs'"

   592   and     history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

   593   and     X_in :  "(X, xrhs) \<in> equas_subst ES Y yrhs'"

   594   shows "distinct_rhs xrhs"

   595 using X_in history

   596 apply (clarsimp simp:equas_subst_def del_x_paired_def)

   597 apply (drule_tac x = a in spec, drule_tac x = b in spec)

   598 apply (simp add:ardenable_def equas_subst_f_def)

   599 by (auto intro:rhs_subst_holds_distinct_rhs simp:dist' split:if_splits)

   600 

   601 lemma r_no_EMPTY_imp_seq_rhs_r_no_EMPTY:

   602   "[] \<notin> L r \<Longrightarrow> no_EMPTY_rhs (seq_rhs_r rhs r)"

   603 by (auto simp:no_EMPTY_rhs_def seq_rhs_r_def lang_seq_def)

   604 

   605 lemma del_x_paired_holds_no_EMPTY:

   606   "no_EMPTY_rhs yrhs \<Longrightarrow> no_EMPTY_rhs (del_x_paired yrhs Y)"

   607 by (auto simp:no_EMPTY_rhs_def del_x_paired_def)

   608 

   609 lemma rhs_subst_holds_no_EMPTY:

   610   "\<lbrakk>no_EMPTY_rhs yrhs; (Y, r) \<in> yrhs; Y \<noteq> {[]}\<rbrakk> \<Longrightarrow> no_EMPTY_rhs (rhs_subst yrhs Y rhs' r)"

   611 apply (auto simp:rhs_subst_def intro!:no_EMPTY_rhss_imp_merge_no_EMPTY r_no_EMPTY_imp_seq_rhs_r_no_EMPTY del_x_paired_holds_no_EMPTY)

   612 by (auto simp:no_EMPTY_rhs_def)

   613 

   614 lemma equas_subst_holds_no_EMPTY:

   615   assumes substor: "Y \<noteq> {[]}"

   616   and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

   617   and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"

   618   shows "no_EMPTY_rhs xrhs"

   619 proof-

   620   from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"

   621     by (auto simp add:equas_subst_def del_x_paired_def)

   622   then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"

   623                        and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast

   624   hence dist_zrhs: "distinct_rhs zrhs" using history

   625     by (auto simp:ardenable_def)

   626   show ?thesis

   627   proof (cases "\<exists> r. (Y, r) \<in> zrhs")

   628     case True

   629     then obtain r where Y_in_zrhs: "(Y, r) \<in> zrhs" ..

   630     hence some: "(SOME r. (Y, r) \<in> zrhs) = r" using Z_in dist_zrhs

   631       by (auto simp:distinct_rhs_def)

   632     hence "no_EMPTY_rhs (rhs_subst zrhs Y yrhs' r)"

   633       using substor Y_in_zrhs history Z_in

   634       by (rule_tac rhs_subst_holds_no_EMPTY, auto simp:ardenable_def)

   635     thus ?thesis using X_Z True some

   636       by (simp add:equas_subst_def equas_subst_f_def)

   637   next

   638     case False

   639     hence "(X, xrhs) = (Z, zrhs)" using Z_in X_Z

   640       by (simp add:equas_subst_f_def)

   641     thus ?thesis using history Z_in

   642       by (auto simp:ardenable_def)

   643   qed

   644 qed

   645 

   646 lemma equas_subst_f_holds_left_eq_right:

   647   assumes substor: "Y = L rhs'"

   648   and     history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> distinct_rhs xrhs \<and> X = L xrhs"

   649   and       subst: "(X, xrhs) = equas_subst_f Y rhs' (Z, zrhs)"

   650   and     self_contained: "(Z, zrhs) \<in> ES"

   651   shows "X = L xrhs"

   652 proof (cases "\<exists> r. (Y, r) \<in> zrhs")

   653   case True

   654   from True obtain r where "(1)":"(Y, r) \<in> zrhs" ..

   655   show ?thesis

   656   proof -

   657     from history self_contained

   658     have dist: "distinct_rhs zrhs" by auto

   659     hence "(SOME r. (Y, r) \<in> zrhs) = r" using self_contained "(1)"

   660       using distinct_rhs_def by (auto intro:some_equality)

   661     moreover have "L zrhs = L (rhs_subst zrhs Y rhs' r)" using substor dist "(1)" self_contained

   662       by (rule_tac rhs_subst_prop1, auto simp:distinct_equas_rhs_def)

   663     ultimately show ?thesis using subst history self_contained

   664       by (auto simp:equas_subst_f_def split:if_splits)

   665   qed

   666 next

   667   case False

   668   thus ?thesis using history subst self_contained

   669     by (auto simp:equas_subst_f_def)

   670 qed

   671 

   672 lemma equas_subst_holds_left_eq_right:

   673   assumes history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

   674   and     substor: "Y = L rhs'"

   675   and     X_in :  "(X, xrhs) \<in> equas_subst ES Y yrhs'"

   676   shows "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y rhs' \<longrightarrow> X = L xrhs"

   677 apply (clarsimp simp add:equas_subst_def del_x_paired_def)

   678 using substor

   679 apply (drule_tac equas_subst_f_holds_left_eq_right)

   680 using history

   681 by (auto simp:ardenable_def)

   682 

   683 lemma equas_subst_holds_ardenable:

   684   assumes substor: "Y = L yrhs'"

   685   and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

   686   and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"

   687   and dist': "distinct_rhs yrhs'"

   688   and not_lambda: "Y \<noteq> {[]}"

   689   shows "ardenable (X, xrhs)"

   690 proof -

   691   have "distinct_rhs xrhs" using history X_in dist' 

   692     by (auto dest:equas_subst_holds_distinct_rhs)

   693   moreover have "no_EMPTY_rhs xrhs" using history X_in not_lambda

   694     by (auto intro:equas_subst_holds_no_EMPTY)

   695   moreover have "X = L xrhs" using history substor X_in

   696   by (auto dest: equas_subst_holds_left_eq_right simp del:L_rhs.simps)

   697   ultimately show ?thesis using ardenable_def by simp

   698 qed

   699 

   700 lemma equas_subst_holds_cls_defined:

   701   assumes         X_in: "(X, xrhs) \<in> equas_subst ES Y yrhs'"

   702   and           Inv_ES: "Inv X' ES"

   703   and            subst: "(Y, yrhs) \<in> ES"

   704   and  cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}"

   705   shows "rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equas_subst ES Y yrhs'))"

   706 proof-

   707   have tac: "\<lbrakk> A \<subseteq> B; C \<subseteq> D; E \<subseteq> A \<union> B\<rbrakk> \<Longrightarrow> E \<subseteq> B \<union> D" by auto

   708   from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"

   709     by (auto simp add:equas_subst_def del_x_paired_def)

   710   then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"

   711                        and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast

   712   hence "rhs_eq_cls zrhs \<subseteq> insert {[]} (left_eq_cls ES)" using Inv_ES

   713     by (auto simp:Inv_def)

   714   moreover have "rhs_eq_cls yrhs' \<subseteq> insert {[]} (left_eq_cls ES) - {Y}" 

   715     using Inv_ES subst cls_holds_but_Y

   716     by (auto simp:Inv_def)

   717   moreover have "rhs_eq_cls xrhs \<subseteq> rhs_eq_cls zrhs \<union> rhs_eq_cls yrhs' - {Y}"

   718     using X_Z cls_holds_but_Y

   719     apply (clarsimp simp add:equas_subst_f_def rhs_subst_def split:if_splits)

   720     by (auto simp:rhs_eq_cls_def merge_rhs_def del_x_paired_def seq_rhs_r_def)

   721   moreover have "left_eq_cls (equas_subst ES Y yrhs') = left_eq_cls ES - {Y}" using subst

   722     by (auto simp: left_eq_cls_def equas_subst_def del_x_paired_def equas_subst_f_def

   723              dest: equas_subst_f_del_no_other

   724              split: if_splits)

   725   ultimately show ?thesis by blast

   726 qed

   727 

   728 lemma iteration_step: 

   729   assumes Inv_ES: "Inv X ES"

   730   and    not_T: "\<not> TCon ES"

   731   shows "(\<exists> ES'. Inv X ES' \<and> (card ES', card ES) \<in> less_than)" 

   732 proof -

   733   from Inv_ES not_T have another: "\<exists>Y yrhs. (Y, yrhs) \<in> ES \<and> X \<noteq> Y" unfolding Inv_def

   734     by (clarify, rule_tac exist_another_equa[where X = X], auto)

   735   then obtain Y yrhs where subst: "(Y, yrhs) \<in> ES" and not_X: " X \<noteq> Y" by blast

   736   show ?thesis (is "\<exists> ES'. ?P ES'")

   737   proof (cases "Y = {[]}") 

   738     case True

   739       --"in this situation, we pick a \"\<lambda>\" equation, thus directly remove it from the equation-system"

   740     have "?P (ES - {(Y, yrhs)})" 

   741     proof 

   742       show "Inv X (ES - {(Y, yrhs)})" using True not_X

   743         by (simp add:Inv_ES Inv_mono_with_lambda)

   744     next 

   745       show "(card (ES - {(Y, yrhs)}), card ES) \<in> less_than" using Inv_ES subst

   746         by (auto elim:non_empty_card_prop[rule_format] simp:Inv_def)

   747     qed

   748     thus ?thesis by blast

   749   next

   750     case False

   751       --"in this situation, we pick a equation and using ardenable to get a 

   752         rhs without itself in it, then use equas_subst to form a new equation-system"

   753     hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" 

   754       using subst Inv_ES

   755       by (auto intro:ardenable_prop simp add:Inv_def simp del:L_rhs.simps)

   756     then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'"

   757       and dist_Y': "distinct_rhs yrhs'"

   758       and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" by blast

   759     hence "?P (equas_subst ES Y yrhs')"

   760     proof -

   761       have finite_del: "\<And> S x. finite S \<Longrightarrow> finite (del_x_paired S x)" 

   762         apply (rule_tac A = "del_x_paired S x" in finite_subset)

   763         by (auto simp:del_x_paired_def)

   764       have "finite (equas_subst ES Y yrhs')" using Inv_ES 

   765         by (auto intro!:finite_del simp:equas_subst_def Inv_def)

   766       moreover have "\<exists>rhs. (X, rhs) \<in> equas_subst ES Y yrhs'" using Inv_ES not_X

   767         by (auto intro:equas_subst_del_no_other simp:Inv_def)

   768       moreover have "distinct_equas (equas_subst ES Y yrhs')" using Inv_ES

   769         by (auto intro:equas_subst_holds_distinct simp:Inv_def)

   770       moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow> ardenable (X, xrhs)"

   771         using Inv_ES dist_Y' False Y'_l_eq_r

   772         apply (clarsimp simp:Inv_def)

   773         by (rule equas_subst_holds_ardenable, simp_all)

   774       moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow> X \<noteq> {}" using Inv_ES

   775         by (clarsimp simp:equas_subst_def Inv_def del_x_paired_def equas_subst_f_def split:if_splits, auto)

   776       moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow>

   777                                rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equas_subst ES Y yrhs'))"

   778         using Inv_ES subst cls_holds_but_Y

   779         apply (rule_tac impI | rule_tac allI)+

   780         by (erule equas_subst_holds_cls_defined, auto)

   781       moreover have "(card (equas_subst ES Y yrhs'), card ES) \<in> less_than"using Inv_ES subst

   782         by (simp add:equas_subst_card_less Inv_def)

   783       ultimately show "?P (equas_subst ES Y yrhs')" by (auto simp:Inv_def)      

   784     qed

   785     thus ?thesis by blast

   786   qed

   787 qed

   788 

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

   790 

   791 lemma iteration_conc: 

   792   assumes history: "Inv X ES"

   793   shows "\<exists> ES'. Inv X ES' \<and> TCon ES'" (is "\<exists> ES'. ?P ES'")

   794 proof (cases "TCon ES")

   795   case True

   796   hence "?P ES" using history by simp

   797   thus ?thesis by blast

   798 next

   799   case False  

   800   thus ?thesis using history iteration_step

   801     by (rule_tac f = card in wf_iter, simp_all)

   802 qed

   803 

   804 lemma eqset_imp_iff': "A = B \<Longrightarrow> \<forall> x. x \<in> A \<longleftrightarrow> x \<in> B"

   805 apply (auto simp:mem_def)

   806 done

   807 

   808 lemma set_cases2:

   809   "\<lbrakk>(A = {} \<Longrightarrow> R A); \<And> x. (A = {x}) \<Longrightarrow> R A; \<And> x y. \<lbrakk>x \<noteq> y; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> R A\<rbrakk> \<Longrightarrow> R A"

   810 apply (case_tac "A = {}", simp)

   811 by (case_tac "\<exists> x. A = {x}", clarsimp, blast)

   812 

   813 lemma rhs_aux:"\<lbrakk>distinct_rhs rhs; {Y. \<exists>r. (Y, r) \<in> rhs} = {X}\<rbrakk> \<Longrightarrow> (\<exists>r. rhs = {(X, r)})"

   814 apply (rule_tac A = rhs in set_cases2, simp)

   815 apply (drule_tac x = X in eqset_imp_iff, clarsimp)

   816 apply (drule eqset_imp_iff',clarsimp)

   817 apply (frule_tac x = a in spec, drule_tac x = aa in spec)

   818 by (auto simp:distinct_rhs_def)

   819 

   820 lemma every_eqcl_has_reg: 

   821   assumes finite_CS: "finite (UNIV Quo Lang)"

   822   and X_in_CS: "X \<in> (UNIV Quo Lang)"

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

   824 proof-

   825   have "\<exists>ES'. Inv X ES' \<and> TCon ES'" using finite_CS X_in_CS

   826     by (auto intro:init_ES_satisfy_Inv iteration_conc)

   827   then obtain ES' where Inv_ES': "Inv X ES'" 

   828                    and  TCon_ES': "TCon ES'" by blast

   829   from Inv_ES' TCon_ES' 

   830   have "\<exists> rhs. ES' = {(X, rhs)}"

   831     apply (clarsimp simp:Inv_def TCon_def)

   832     apply (rule_tac x = rhs in exI)

   833     by (auto dest!:card_Suc_Diff1 simp:card_eq_0_iff)  

   834   then obtain rhs where ES'_single_equa: "ES' = {(X, rhs)}" ..

   835   hence X_ardenable: "ardenable (X, rhs)" using Inv_ES'

   836     by (simp add:Inv_def)

   837   

   838   from X_ardenable have X_l_eq_r: "X = L rhs"

   839     by (simp add:ardenable_def)

   840   hence rhs_not_empty: "rhs \<noteq> {}" using Inv_ES' ES'_single_equa

   841     by (auto simp:Inv_def ardenable_def)

   842   have rhs_eq_cls: "rhs_eq_cls rhs \<subseteq> {X, {[]}}"

   843     using Inv_ES' ES'_single_equa

   844     by (auto simp:Inv_def ardenable_def left_eq_cls_def)

   845   have X_not_empty: "X \<noteq> {}" using Inv_ES' ES'_single_equa

   846     by (auto simp:Inv_def)    

   847   show ?thesis

   848   proof (cases "X = {[]}")

   849     case True

   850     hence "?E EMPTY" by (simp)

   851     thus ?thesis by blast

   852   next

   853     case False with  X_ardenable

   854     have "\<exists> rhs'. X = L rhs' \<and> rhs_eq_cls rhs' = rhs_eq_cls rhs - {X} \<and> distinct_rhs rhs'"

   855       by (drule_tac ardenable_prop, auto)

   856     then obtain rhs' where X_eq_rhs': "X = L rhs'"

   857       and rhs'_eq_cls: "rhs_eq_cls rhs' = rhs_eq_cls rhs - {X}" 

   858       and rhs'_dist : "distinct_rhs rhs'" by blast

   859     have "rhs_eq_cls rhs' \<subseteq> {{[]}}" using rhs_eq_cls False rhs'_eq_cls rhs_not_empty 

   860       by blast

   861     hence "rhs_eq_cls rhs' = {{[]}}" using X_not_empty X_eq_rhs'

   862       by (auto simp:rhs_eq_cls_def)

   863     hence "\<exists> r. rhs' = {({[]}, r)}" using rhs'_dist

   864       by (auto intro:rhs_aux simp:rhs_eq_cls_def)

   865     then obtain r where "rhs' = {({[]}, r)}" ..

   866     hence "?E r" using X_eq_rhs' by (auto simp add:lang_seq_def)

   867     thus ?thesis by blast     

   868   qed

   869 qed

   870 

   871 text {* definition of a regular language *}

   872 

   873 abbreviation

   874   reg :: "string set => bool"

   875 where

   876   "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)"

   877 

   878 theorem myhill_nerode: 

   879   assumes finite_CS: "finite (UNIV Quo Lang)"

   880   shows   "\<exists> (reg::rexp). Lang = L reg" (is "\<exists> r. ?P r")

   881 proof -

   882   have has_r_each: "\<forall>C\<in>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists>(r::rexp). C = L r" using finite_CS

   883     by (auto dest:every_eqcl_has_reg)  

   884   have "\<exists> (rS::rexp set). finite rS \<and> 

   885                           (\<forall> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists> r \<in> rS. C = L r) \<and> 

   886                           (\<forall> r \<in> rS. \<exists> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. C = L r)" 

   887        (is "\<exists> rS. ?Q rS")

   888   proof-

   889     have "\<And> C. C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<Longrightarrow> C = L (SOME (ra::rexp). C = L ra)"

   890       using has_r_each

   891       apply (erule_tac x = C in ballE, erule_tac exE)

   892       by (rule_tac a = r in someI2, simp+)

   893     hence "?Q ((\<lambda> C. SOME r. C = L r) ` {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang})" using has_r_each

   894       using finite_CS by auto

   895     thus ?thesis by blast    

   896   qed

   897   then obtain rS where finite_rS : "finite rS"

   898     and has_r_each': "\<forall> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists> r \<in> (rS::rexp set). C = L r"

   899     and has_cl_each: "\<forall> r \<in> (rS::rexp set). \<exists> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. C = L r" by blast

   900   have "?P (folds ALT NULL rS)"

   901   proof

   902     show "Lang \<subseteq> L (folds ALT NULL rS)" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_r_each'

   903       apply (clarsimp simp:fold_alt_null_eqs) by blast

   904   next 

   905     show "L (folds ALT NULL rS) \<subseteq> Lang" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_cl_each

   906       by (clarsimp simp:fold_alt_null_eqs)

   907   qed

   908   thus ?thesis by blast

   909 qed 

   910 

   911 

   912 text {* tests by Christian *}

   913 

   914 (* Alternative definition for Quo *)

   915 definition 

   916   QUOT :: "string set \<Rightarrow> (string set) set"  

   917 where

   918   "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})"

   919 

   920 lemma test: 

   921   "UNIV Quo Lang = QUOT Lang"

   922 by (auto simp add: quot_def QUOT_def)

   923 

   924 lemma test1:

   925   assumes finite_CS: "finite (QUOT Lang)"

   926   shows "reg Lang"

   927 using finite_CS

   928 unfolding test[symmetric]

   929 by (auto dest: myhill_nerode)

   930 

   931 lemma cons_one: "x @ y \<in> {z} \<Longrightarrow> x @ y = z"

   932 by simp

   933 

   934 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"

   935 proof 

   936   show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"

   937   proof 

   938     fix x 

   939     assume in_quot: "x \<in> QUOT {[]}"

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

   941     proof -

   942       from in_quot 

   943       have "x = {[]} \<or> x = UNIV - {[]}"

   944         unfolding QUOT_def equiv_class_def

   945       proof 

   946         fix xa

   947         assume in_univ: "xa \<in> UNIV"

   948            and in_eqiv: "x \<in> {{y. xa \<equiv>{[]}\<equiv> y}}"

   949         show "x = {[]} \<or> x = UNIV - {[]}"

   950         proof(cases "xa = []")

   951           case True

   952           hence "{y. xa \<equiv>{[]}\<equiv> y} = {[]}" using in_eqiv

   953             by (auto simp add:equiv_str_def)

   954           thus ?thesis using in_eqiv by (rule_tac disjI1, simp)

   955         next

   956           case False

   957           hence "{y. xa \<equiv>{[]}\<equiv> y} = UNIV - {[]}" using in_eqiv

   958             by (auto simp:equiv_str_def)

   959           thus ?thesis using in_eqiv by (rule_tac disjI2, simp)

   960         qed

   961       qed

   962       thus ?thesis by simp

   963     qed

   964   qed

   965 next

   966   show "{{[]}, UNIV - {[]}} \<subseteq> QUOT {[]}"

   967   proof

   968     fix x

   969     assume in_res: "x \<in> {{[]}, (UNIV::string set) - {[]}}"

   970     show "x \<in> (QUOT {[]})"

   971     proof -

   972       have "x = {[]} \<Longrightarrow> x \<in> QUOT {[]}"

   973         apply (simp add:QUOT_def equiv_class_def equiv_str_def)

   974         by (rule_tac x = "[]" in exI, auto)

   975       moreover have "x = UNIV - {[]} \<Longrightarrow> x \<in> QUOT {[]}"

   976         apply (simp add:QUOT_def equiv_class_def equiv_str_def)

   977         by (rule_tac x = "''a''" in exI, auto)

   978       ultimately show ?thesis using in_res by blast

   979     qed

   980   qed

   981 qed

   982 

   983 lemma quot_single_aux: "\<lbrakk>x \<noteq> []; x \<noteq> [c]\<rbrakk> \<Longrightarrow> x @ z \<noteq> [c]"

   984 by (induct x, auto)

   985 

   986 lemma quot_single: "\<And> (c::char). QUOT {[c]} = {{[]}, {[c]}, UNIV - {[], [c]}}"

   987 proof - 

   988   fix c::"char" 

   989   have exist_another: "\<exists> a. a \<noteq> c" 

   990     apply (case_tac "c = CHR ''a''")

   991     apply (rule_tac x = "CHR ''b''" in exI, simp)

   992     by (rule_tac x = "CHR ''a''" in exI, simp)  

   993   show "QUOT {[c]} = {{[]}, {[c]}, UNIV - {[], [c]}}"

   994   proof

   995     show "QUOT {[c]} \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"

   996     proof 

   997       fix x 

   998       assume in_quot: "x \<in> QUOT {[c]}"

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

  1000       proof -

  1001         from in_quot 

  1002         have "x = {[]} \<or> x = {[c]} \<or> x = UNIV - {[],[c]}"

  1003           unfolding QUOT_def equiv_class_def

  1004         proof 

  1005           fix xa

  1006           assume in_eqiv: "x \<in> {{y. xa \<equiv>{[c]}\<equiv> y}}"

  1007           show "x = {[]} \<or> x = {[c]} \<or> x = UNIV - {[], [c]}"

  1008           proof-

  1009             have "xa = [] \<Longrightarrow> x = {[]}" using in_eqiv 

  1010               by (auto simp add:equiv_str_def)

  1011             moreover have "xa = [c] \<Longrightarrow> x = {[c]}"

  1012             proof -

  1013               have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv

  1014                 apply (simp add:equiv_str_def)

  1015                 apply (rule set_ext, rule iffI, simp)

  1016                 apply (drule_tac x = "[]" in spec, auto)

  1017                 done   

  1018               thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp 

  1019             qed

  1020             moreover have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}"

  1021             proof -

  1022               have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = UNIV - {[],[c]}" 

  1023                 apply (clarsimp simp add:equiv_str_def)

  1024                 apply (rule set_ext, rule iffI, simp)

  1025                 apply (rule conjI)

  1026                 apply (drule_tac x = "[c]" in spec, simp)

  1027                 apply (drule_tac x = "[]" in spec, simp)

  1028                 by (auto dest:quot_single_aux)

  1029               thus "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}" using in_eqiv by simp

  1030             qed

  1031             ultimately show ?thesis by blast

  1032           qed

  1033         qed

  1034         thus ?thesis by simp

  1035       qed

  1036     qed

  1037   next

  1038     show "{{[]}, {[c]}, UNIV - {[],[c]}} \<subseteq> QUOT {[c]}"

  1039     proof

  1040       fix x

  1041       assume in_res: "x \<in> {{[]},{[c]}, (UNIV::string set) - {[],[c]}}"

  1042       show "x \<in> (QUOT {[c]})"

  1043       proof -

  1044         have "x = {[]} \<Longrightarrow> x \<in> QUOT {[c]}"

  1045           apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1046           by (rule_tac x = "[]" in exI, auto)

  1047         moreover have "x = {[c]} \<Longrightarrow> x \<in> QUOT {[c]}"

  1048           apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1049           apply (rule_tac x = "[c]" in exI, simp)

  1050           apply (rule set_ext, rule iffI, simp+)

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

  1052         moreover have "x = UNIV - {[],[c]} \<Longrightarrow> x \<in> QUOT {[c]}"

  1053           using exist_another

  1054           apply (clarsimp simp add:QUOT_def equiv_class_def equiv_str_def)        

  1055           apply (rule_tac x = "[a]" in exI, simp)

  1056           apply (rule set_ext, rule iffI, simp)

  1057           apply (clarsimp simp:quot_single_aux, simp)

  1058           apply (rule conjI)

  1059           apply (drule_tac x = "[c]" in spec, simp)

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

  1061         ultimately show ?thesis using in_res by blast

  1062       qed

  1063     qed

  1064   qed

  1065 qed

  1066 

  1067 lemma eq_class_imp_eq_str:

  1068   "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang \<Longrightarrow> x \<equiv>lang\<equiv> y"

  1069 by (auto simp:equiv_class_def equiv_str_def)

  1070 

  1071 lemma finite_tag_image: 

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

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

  1074 by (auto simp add:image_def Pow_def)

  1075 

  1076 lemma str_inj_imps:

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

  1078   shows "inj_on ((op `) tag) (QUOT lang)"

  1079 proof (clarsimp simp add:inj_on_def QUOT_def)

  1080   fix x y

  1081   assume eq_tag: "tag ` \<lbrakk>x\<rbrakk>lang = tag ` \<lbrakk>y\<rbrakk>lang"

  1082   show "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang"

  1083   proof -

  1084     have aux1:"\<And>a b. a \<in> (\<lbrakk>b\<rbrakk>lang) \<Longrightarrow> (a \<equiv>lang\<equiv> b)"

  1085       by (simp add:equiv_class_def equiv_str_def)

  1086     have aux2: "\<And> A B f. \<lbrakk>f ` A = f ` B; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> a b. a \<in> A \<and> b \<in> B \<and> f a = f b"

  1087       by auto

  1088     have aux3: "\<And> a l. \<lbrakk>a\<rbrakk>l \<noteq> {}" 

  1089       by (auto simp:equiv_class_def equiv_str_def)

  1090     show ?thesis using eq_tag

  1091       apply (drule_tac aux2, simp add:aux3, clarsimp)

  1092       apply (drule_tac str_inj, (drule_tac aux1)+)

  1093       by (simp add:equiv_str_def equiv_class_def)

  1094   qed

  1095 qed

  1096 

  1097 definition tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"

  1098 where

  1099   "tag_str_ALT L\<^isub>1 L\<^isub>2 x \<equiv> (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)"

  1100 

  1101 lemma tag_str_alt_range_finite:

  1102   assumes finite1: "finite (QUOT L\<^isub>1)"

  1103   and finite2: "finite (QUOT L\<^isub>2)"

  1104   shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))"

  1105 proof -

  1106   have "{y. \<exists>x. y = (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"

  1107     by (auto simp:QUOT_def)

  1108   thus ?thesis using finite1 finite2

  1109     by (auto simp: image_def tag_str_ALT_def UNION_def 

  1110             intro: finite_subset[where B = "(QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"])

  1111 qed

  1112 

  1113 lemma tag_str_alt_inj:

  1114   "tag_str_ALT L\<^isub>1 L\<^isub>2 x = tag_str_ALT L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<equiv>(L\<^isub>1 \<union> L\<^isub>2)\<equiv> y"

  1115 apply (simp add:tag_str_ALT_def equiv_class_def equiv_str_def)

  1116 by blast

  1117   

  1118 lemma quot_alt:

  1119   assumes finite1: "finite (QUOT L\<^isub>1)"

  1120   and finite2: "finite (QUOT L\<^isub>2)"

  1121   shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))"

  1122 proof (rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD)

  1123   show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))"

  1124     using finite_tag_image tag_str_alt_range_finite finite1 finite2

  1125     by auto

  1126 next

  1127   show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"

  1128     apply (rule_tac str_inj_imps)

  1129     by (erule_tac tag_str_alt_inj)

  1130 qed

  1131 

  1132 (* list_diff:: list substract, once different return tailer *)

  1133 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)

  1134 where

  1135   "list_diff []  xs = []" |