Mercurial Mercurial > hg > regexp / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Myhill_1.thy
changeset 96 3b9deda4f459
parent 95 9540c2f2ea77
child 97 70485955c934
equal deleted inserted replaced
95:9540c2f2ea77 96:3b9deda4f459 
   400    fun L_rhs:: "rhs_item set \<Rightarrow> lang"
 
   400    fun L_rhs:: "rhs_item set \<Rightarrow> lang"
 
   401    where 
   401    where 
   402      "L_rhs rhs = \<Union> (L ` rhs)"
 
   402      "L_rhs rhs = \<Union> (L ` rhs)"
 
   403 end
 
   403 end
 
   404 
   404 
       
   405 lemma L_rhs_union_distrib:
 
       
   406   fixes A B::"rhs_item set"
 
       
   407   shows "L A \<union> L B = L (A \<union> B)"
 
       
   408 by simp
 
       
   409 
       
   410 
       
   411 
   405 text {* Transitions between equivalence classes *}
 
   412 text {* Transitions between equivalence classes *}
 
   406 
   413 
   407 definition 
   414 definition 
   408   transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
 
   415   transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
 
   409 where
 
   416 where
 
   410   "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
 
   417   "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
 
   411 
   418 
   412 text {* Initial equational system *}
 
   419 text {* Initial equational system *}
 
   413 
   420 
   414 definition
 
   421 definition
 
   415   "init_rhs CS X \<equiv>  
   422   "Init_rhs CS X \<equiv>  
   416       if ([] \<in> X) then 
   423       if ([] \<in> X) then 
   417           {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
 
   424           {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
 
   418       else 
   425       else 
   419           {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
   426           {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
   420 
   427 
   421 definition 
   428 definition 
   422   "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
 
   429   "Init CS \<equiv> {(X, Init_rhs CS X) | X.  X \<in> CS}"
 
   423 
   430 
   424 
   431 
   425 
   432 
   426 section {* Arden Operation on equations *}
 
   433 section {* Arden Operation on equations *}
 
   427 
   434 
   461   equation of the equational system @{text ES}.
 
   468   equation of the equational system @{text ES}.
 
   462 *}
 
   469 *}
 
   463 
   470 
   464 definition
 
   471 definition
 
   465   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
   472   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
   466 
       
   467 
       
   468 section {* While-combinator *}
 
       
   469 
   473 
   470 text {*
 
   474 text {*
 
   471   The following term @{text "remove ES Y yrhs"} removes the equation
 
   475   The following term @{text "remove ES Y yrhs"} removes the equation
 
   472   @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
 
   476   @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
 
   473   all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}).
 
   477   all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}).
 
   474   The @{text "Y"}-definition is made non-recursive using Arden's transformation
 
   478   The @{text "Y"}-definition is made non-recursive using Arden's transformation
 
   475   @{text "arden_variate Y yrhs"}.
 
   479   @{text "arden_variate Y yrhs"}.
 
   476   *}
 
   480   *}
 
   477 
   481 
   478 definition
 
   482 definition
 
   479   "Remove ES Y yrhs \<equiv> 
   483   "Remove ES X xrhs \<equiv> 
   480       Subst_all  (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
 
   484       Subst_all  (ES - {(X, xrhs)}) X (Arden X xrhs)"
 
   481 
   485 
   482 text {*
 
   486 
   483   The following term @{text "iterm X ES"} represents one iteration in the while loop.
 
   487 section {* While-combinator *}
 
       
   488 
       
   489 text {*
 
       
   490   The following term @{text "Iter X ES"} represents one iteration in the while loop.
 
   484   It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
 
   491   It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
 
   485 *}
 
   492 *}
 
   486 
   493 
   487 definition 
   494 definition 
   488   "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)
 
   495   "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
 
   489                 in Remove ES Y yrhs)"
 
   496                 in Remove ES Y yrhs)"
 
   490 
   497 
   491 text {*
 
   498 text {*
 
   492   The following term @{text "reduce X ES"} repeatedly removes characteriztion equations
 
   499   The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
 
   493   for unknowns other than @{text "X"} until one is left.
 
   500   for unknowns other than @{text "X"} until one is left.
 
   494 *}
 
   501 *}
 
   495 
   502 
   496 definition 
   503 definition 
   497   "reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (iter X) ES"
 
   504   "Reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (Iter X) ES"
 
   498 
   505 
   499 text {*
 
   506 text {*
 
   500   Since the @{text "while"} combinator from HOL library is used to implement @{text "reduce X ES"},
 
   507   Since the @{text "while"} combinator from HOL library is used to implement @{text "Reduce X ES"},
 
   501   the induction principle @{thm [source] while_rule} is used to proved the desired properties
 
   508   the induction principle @{thm [source] while_rule} is used to proved the desired properties
 
   502   of @{text "reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
 
   509   of @{text "Reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
 
   503   in terms of a series of auxilliary predicates:
 
   510   in terms of a series of auxilliary predicates:
 
   504 *}
 
   511 *}
 
   505 
   512 
   506 section {* Invariants *}
 
   513 section {* Invariants *}
 
   507 
   514 
   571   *}
 
   578   *}
 
   572 definition 
   579 definition 
   573   "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
   580   "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
   574                   finite_rhs ES \<and> self_contained ES"
 
   581                   finite_rhs ES \<and> self_contained ES"
 
   575 
   582 
       
   583 
       
   584 lemma invariantI:
 
       
   585   assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" 
       
   586           "finite_rhs ES" "self_contained ES"
 
       
   587   shows "invariant ES"
 
       
   588 using assms by (simp add: invariant_def)
 
       
   589 
   576 subsection {* The proof of this direction *}
 
   590 subsection {* The proof of this direction *}
 
   577 
   591 
   578 subsubsection {* Basic properties *}
 
   592 subsubsection {* Basic properties *}
 
   579 
   593 
   580 text {*
 
   594 text {*
 
   581   The following are some basic properties of the above definitions.
 
   595   The following are some basic properties of the above definitions.
 
   582 *}
 
   596 *}
 
   583 
   597 
   584 lemma L_rhs_union_distrib:
 
       
   585   fixes A B::"rhs_item set"
 
       
   586   shows "L A \<union> L B = L (A \<union> B)"
 
       
   587 by simp
 
       
   588 
   598 
   589 lemma finite_Trn:
 
   599 lemma finite_Trn:
 
   590   assumes fin: "finite rhs"
 
   600   assumes fin: "finite rhs"
 
   591   shows "finite {r. Trn Y r \<in> rhs}"
 
   601   shows "finite {r. Trn Y r \<in> rhs}"
 
   592 proof -
 
   602 proof -
 
   599   then show "finite {r. Trn Y r \<in> rhs}"
 
   609   then show "finite {r. Trn Y r \<in> rhs}"
 
   600     by (erule_tac f="snd" in finite_surj) (auto simp add: image_def)
 
   610     by (erule_tac f="snd" in finite_surj) (auto simp add: image_def)
 
   601 qed
 
   611 qed
 
   602 
   612 
   603 lemma finite_Lam:
 
   613 lemma finite_Lam:
 
   604   assumes fin:"finite rhs"
 
   614   assumes fin: "finite rhs"
 
   605   shows "finite {r. Lam r \<in> rhs}"
 
   615   shows "finite {r. Lam r \<in> rhs}"
 
   606 proof -
 
   616 proof -
 
   607   have "finite {Lam r | r. Lam r \<in> rhs}"
 
   617   have "finite {Lam r | r. Lam r \<in> rhs}"
 
   608     by (rule rev_finite_subset[OF fin]) (auto)
 
   618     by (rule rev_finite_subset[OF fin]) (auto)
 
   609   then show "finite {r. Lam r \<in> rhs}"
 
   619   then show "finite {r. Lam r \<in> rhs}"
 
   612     apply(auto simp add: inj_on_def)
 
   622     apply(auto simp add: inj_on_def)
 
   613     done
 
   623     done
 
   614 qed
 
   624 qed
 
   615 
   625 
   616 lemma rexp_of_empty:
 
   626 lemma rexp_of_empty:
 
   617   assumes finite:"finite rhs"
 
   627   assumes finite: "finite rhs"
 
   618   and nonempty:"rhs_nonempty rhs"
 
   628   and nonempty: "rhs_nonempty rhs"
 
   619   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 
   629   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 
   620 using finite nonempty rhs_nonempty_def
 
   630 using finite nonempty rhs_nonempty_def
 
   621 using finite_Trn[OF finite]
 
   631 using finite_Trn[OF finite]
 
   622 by (auto)
 
   632 by (auto)
 
   623 
   633 
   624 lemma [intro!]:
 
       
   625   "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
 
       
   626 
       
   627 lemma lang_of_rexp_of:
 
   634 lemma lang_of_rexp_of:
 
   628   assumes finite:"finite rhs"
 
   635   assumes finite:"finite rhs"
 
   629   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 
   636   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 
   630 proof -
 
   637 proof -
 
   631   have "finite {r. Trn X r \<in> rhs}" 
   638   have "finite {r. Trn X r \<in> rhs}" 
   632     by (rule finite_Trn[OF finite]) 
   639     by (rule finite_Trn[OF finite]) 
   633   then show ?thesis
 
   640   then show ?thesis
 
   634     apply(auto simp add: Seq_def)
 
   641     apply(auto simp add: Seq_def)
 
   635     apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
 
   642     apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
 
       
   643     apply(auto)
 
   636     apply(rule_tac x= "Trn X xa" in exI)
 
   644     apply(rule_tac x= "Trn X xa" in exI)
 
   637     apply(auto simp: Seq_def)
 
   645     apply(auto simp add: Seq_def)
 
   638     done
 
   646     done
 
   639 qed
 
   647 qed
 
   640 
   648 
   641 lemma rexp_of_lam_eq_lam_set:
 
   649 lemma lang_of_append:
 
   642   assumes fin: "finite rhs"
 
   650   "L (append_rexp r rhs_item) = L rhs_item ;; L r"
 
   643   shows "L (\<Uplus>{r. Lam r \<in> rhs}) = L ({Lam r | r. Lam r \<in> rhs})"
 
   651 by (induct rule: append_rexp.induct)
 
   644 proof -
 
   652    (auto simp add: seq_assoc)
 
   645   have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam)
 
       
   646   then show ?thesis by auto
 
       
   647 qed
 
       
   648 
       
   649 lemma [simp]:
 
       
   650   "L (append_rexp r xb) = L xb ;; L r"
 
       
   651 apply (cases xb, auto simp: Seq_def)
 
       
   652 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
 
       
   653 apply(auto simp: Seq_def)
 
       
   654 done
 
       
   655 
   653 
   656 lemma lang_of_append_rhs:
 
   654 lemma lang_of_append_rhs:
 
   657   "L (append_rhs_rexp rhs r) = L rhs ;; L r"
 
   655   "L (append_rhs_rexp rhs r) = L rhs ;; L r"
 
   658 apply (auto simp:append_rhs_rexp_def image_def)
 
   656 unfolding append_rhs_rexp_def
 
   659 apply (auto simp:Seq_def)
 
   657 by (auto simp add: Seq_def lang_of_append)
 
   660 apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def)
 
       
   661 by (rule_tac x = "append_rexp r xb" in exI, auto simp:Seq_def)
 
       
   662 
   658 
   663 lemma classes_of_union_distrib:
 
   659 lemma classes_of_union_distrib:
 
   664   "classes_of A \<union> classes_of B = classes_of (A \<union> B)"
 
   660   shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
 
   665 by (auto simp add:classes_of_def)
 
   661 by (auto simp add: classes_of_def)
 
   666 
   662 
   667 lemma lefts_of_union_distrib:
 
   663 lemma lefts_of_union_distrib:
 
   668   "lefts_of A \<union> lefts_of B = lefts_of (A \<union> B)"
 
   664   shows "lefts_of (A \<union> B) = lefts_of A \<union> lefts_of B"
 
   669 by (auto simp:lefts_of_def)
 
   665 by (auto simp add: lefts_of_def)
 
   670 
   666 
   671 
   667 
   672 subsubsection {* Intialization *}
 
   668 subsubsection {* Intialization *}
 
   673 
   669 
   674 text {*
 
   670 text {*
 
   700     unfolding Image_def str_eq_rel_def by simp
 
   696     unfolding Image_def str_eq_rel_def by simp
 
   701   ultimately show thesis by (blast intro: that)
 
   697   ultimately show thesis by (blast intro: that)
 
   702 qed
 
   698 qed
 
   703 
   699 
   704 lemma l_eq_r_in_eqs:
 
   700 lemma l_eq_r_in_eqs:
 
   705   assumes X_in_eqs: "(X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"
 
   701   assumes X_in_eqs: "(X, xrhs) \<in> (Init (UNIV // (\<approx>Lang)))"
 
   706   shows "X = L xrhs"
 
   702   shows "X = L xrhs"
 
   707 proof 
   703 proof 
   708   show "X \<subseteq> L xrhs"
 
   704   show "X \<subseteq> L xrhs"
 
   709   proof
 
   705   proof
 
   710     fix x
 
   706     fix x
 
   711     assume "(1)": "x \<in> X"
 
   707     assume "(1)": "x \<in> X"
 
   712     show "x \<in> L xrhs"          
   708     show "x \<in> L xrhs"          
   713     proof (cases "x = []")
 
   709     proof (cases "x = []")
 
   714       assume empty: "x = []"
 
   710       assume empty: "x = []"
 
   715       thus ?thesis using X_in_eqs "(1)"
 
   711       thus ?thesis using X_in_eqs "(1)"
 
   716         by (auto simp:eqs_def init_rhs_def)
 
   712         by (auto simp: Init_def Init_rhs_def)
 
   717     next
 
   713     next
 
   718       assume not_empty: "x \<noteq> []"
 
   714       assume not_empty: "x \<noteq> []"
 
   719       then obtain clist c where decom: "x = clist @ [c]"
 
   715       then obtain clist c where decom: "x = clist @ [c]"
 
   720         by (case_tac x rule:rev_cases, auto)
 
   716         by (case_tac x rule:rev_cases, auto)
 
   721       have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:eqs_def)
 
   717       have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:Init_def)
 
   722       then obtain Y 
   718       then obtain Y 
   723         where "Y \<in> UNIV // (\<approx>Lang)" 
   719         where "Y \<in> UNIV // (\<approx>Lang)" 
   724         and "Y ;; {[c]} \<subseteq> X"
 
   720         and "Y ;; {[c]} \<subseteq> X"
 
   725         and "clist \<in> Y"
 
   721         and "clist \<in> Y"
 
   726         using decom "(1)" every_eqclass_has_transition by blast
 
   722         using decom "(1)" every_eqclass_has_transition by blast
 
   728         "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
   724         "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
   729         unfolding transition_def
 
   725         unfolding transition_def
 
   730 	using "(1)" decom
 
   726 	using "(1)" decom
 
   731         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
 
   727         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
 
   732       thus ?thesis using X_in_eqs "(1)"	
   728       thus ?thesis using X_in_eqs "(1)"	
   733         by (simp add: eqs_def init_rhs_def)
 
   729         by (simp add: Init_def Init_rhs_def)
 
   734     qed
 
   730     qed
 
   735   qed
 
   731   qed
 
   736 next
 
   732 next
 
   737   show "L xrhs \<subseteq> X" using X_in_eqs
 
   733   show "L xrhs \<subseteq> X" using X_in_eqs
 
   738     by (auto simp:eqs_def init_rhs_def transition_def) 
   734     by (auto simp:Init_def Init_rhs_def transition_def) 
   739 qed
 
   735 qed
 
   740 
   736 
   741 lemma finite_init_rhs: 
   737 lemma finite_Init_rhs: 
   742   assumes finite: "finite CS"
 
   738   assumes finite: "finite CS"
 
   743   shows "finite (init_rhs CS X)"
 
   739   shows "finite (Init_rhs CS X)"
 
   744 proof-
 
   740 proof-
 
   745   have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")
 
   741   have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")
 
   746   proof -
 
   742   proof -
 
   747     def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" 
   743     def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" 
   748     def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
 
   744     def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
 
   751       by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)
 
   747       by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)
 
   752     moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)
 
   748     moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)
 
   753     ultimately show ?thesis 
   749     ultimately show ?thesis 
   754       by auto
 
   750       by auto
 
   755   qed
 
   751   qed
 
   756   thus ?thesis by (simp add:init_rhs_def transition_def)
 
   752   thus ?thesis by (simp add:Init_rhs_def transition_def)
 
   757 qed
 
   753 qed
 
   758 
   754 
   759 lemma init_ES_satisfy_invariant:
 
   755 lemma Init_ES_satisfies_invariant:
 
   760   assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
 
   756   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
   761   shows "invariant (eqs (UNIV // (\<approx>Lang)))"
 
   757   shows "invariant (Init (UNIV // \<approx>A))"
 
   762 proof -
 
   758 proof (rule invariantI)
 
   763   have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS
 
   759   show "valid_eqns (Init (UNIV // \<approx>A))"
 
   764     by (simp add:eqs_def)
 
   760     unfolding valid_eqns_def 
   765   moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"     
   761     using l_eq_r_in_eqs by simp
 
   766     by (simp add:distinct_equas_def eqs_def)
 
   762   show "finite (Init (UNIV // \<approx>A))" using finite_CS
 
   767   moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"
 
   763     unfolding Init_def by simp
 
   768     by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps)
 
   764   show "distinct_equas (Init (UNIV // \<approx>A))"     
   769   moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))"
 
   765     unfolding distinct_equas_def Init_def by simp
 
   770     using l_eq_r_in_eqs by (simp add:valid_eqns_def)
 
   766   show "ardenable (Init (UNIV // \<approx>A))"
 
   771   moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))"
 
   767     unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
 
   772     using finite_init_rhs[OF finite_CS] 
   768     by auto
 
   773     by (auto simp:finite_rhs_def eqs_def)
 
   769   show "finite_rhs (Init (UNIV // \<approx>A))"
 
   774   moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"
 
   770     using finite_Init_rhs[OF finite_CS]
 
   775     by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)
 
   771     unfolding finite_rhs_def Init_def by auto
 
   776   ultimately show ?thesis by (simp add:invariant_def)
 
   772   show "self_contained (Init (UNIV // \<approx>A))"
 
       
   773     unfolding self_contained_def Init_def Init_rhs_def classes_of_def lefts_of_def
 
       
   774     by auto
 
   777 qed
 
   775 qed
 
   778 
   776 
   779 subsubsection {* Interation step *}
 
   777 subsubsection {* Interation step *}
 
   780 
   778 
   781 text {*
 
   779 text {*
 
   782   From this point until @{text "iteration_step"}, 
   780   From this point until @{text "iteration_step"}, 
   783   the correctness of the iteration step @{text "iter X ES"} is proved.
 
   781   the correctness of the iteration step @{text "Iter X ES"} is proved.
 
   784 *}
 
   782 *}
 
   785 
   783 
   786 lemma Arden_keeps_eq:
 
   784 lemma Arden_keeps_eq:
 
   787   assumes l_eq_r: "X = L rhs"
 
   785   assumes l_eq_r: "X = L rhs"
 
   788   and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
 
   786   and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
 
   904 by (auto simp:lefts_of_def Subst_all_def)
 
   902 by (auto simp:lefts_of_def Subst_all_def)
 
   905 
   903 
   906 lemma Subst_updates_cls:
 
   904 lemma Subst_updates_cls:
 
   907   "X \<notin> classes_of xrhs \<Longrightarrow> 
   905   "X \<notin> classes_of xrhs \<Longrightarrow> 
   908       classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
 
   906       classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
 
   909 apply (simp only:Subst_def append_rhs_keeps_cls 
   907 apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
 
   910                               classes_of_union_distrib[THEN sym])
 
       
   911 by (auto simp:classes_of_def)
 
   908 by (auto simp:classes_of_def)
 
   912 
   909 
   913 lemma Subst_all_keeps_self_contained:
 
   910 lemma Subst_all_keeps_self_contained:
 
   914   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
 
   911   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
 
   915   shows "self_contained (Subst_all ES Y (Arden Y yrhs))" 
   912   shows "self_contained (Subst_all ES Y (Arden Y yrhs))" 
   931           have "Y \<notin> classes_of (Arden Y yrhs)" 
   928           have "Y \<notin> classes_of (Arden Y yrhs)" 
   932             using Arden_removes_cl by simp
 
   929             using Arden_removes_cl by simp
 
   933           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
 
   930           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
 
   934         qed
 
   931         qed
 
   935         moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc
 
   932         moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc
 
   936           apply (simp only:self_contained_def lefts_of_union_distrib[THEN sym])
 
   933           apply (simp only:self_contained_def lefts_of_union_distrib)
 
   937           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
 
   934           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
 
   938         moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 
   935         moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 
   939           using sc 
   936           using sc 
   940           by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def)
 
   937           by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def)
 
   941         ultimately show ?thesis by auto
 
   938         ultimately show ?thesis by auto
 
   943       ultimately show ?thesis by simp
 
   940       ultimately show ?thesis by simp
 
   944     qed
 
   941     qed
 
   945   } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
 
   942   } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
 
   946 qed
 
   943 qed
 
   947 
   944 
   948 lemma Subst_all_satisfy_invariant:
 
   945 lemma Subst_all_satisfies_invariant:
 
   949   assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
 
   946   assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
 
   950   shows "invariant (Subst_all ES Y (Arden Y yrhs))"
 
   947   shows "invariant (Subst_all ES Y (Arden Y yrhs))"
 
   951 proof -  
   948 proof (rule invariantI)
 
   952   have finite_yrhs: "finite yrhs" 
   949   have Y_eq_yrhs: "Y = L yrhs" 
       
   950     using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
 
       
   951    have finite_yrhs: "finite yrhs" 
   953     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
 
   952     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
 
   954   have nonempty_yrhs: "rhs_nonempty yrhs" 
   953   have nonempty_yrhs: "rhs_nonempty yrhs" 
   955     using invariant_ES by (auto simp:invariant_def ardenable_def)
 
   954     using invariant_ES by (auto simp:invariant_def ardenable_def)
 
   956   have Y_eq_yrhs: "Y = L yrhs" 
   955   show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
 
   957     using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
 
   956   proof-
 
   958   have "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
   957     have "Y = L (Arden Y yrhs)" 
       
   958       using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
 
       
   959       by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
 
       
   960     thus ?thesis using invariant_ES 
       
   961       by (clarsimp simp add:valid_eqns_def 
       
   962         Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
 
       
   963         simp del:L_rhs.simps)
 
       
   964   qed
 
       
   965   show "finite (Subst_all ES Y (Arden Y yrhs))" 
       
   966     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
 
       
   967   show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
   959     using invariant_ES
 
   968     using invariant_ES
 
   960     by (auto simp:distinct_equas_def Subst_all_def invariant_def)
 
   969     by (auto simp:distinct_equas_def Subst_all_def invariant_def)
 
   961   moreover have "finite (Subst_all ES Y (Arden Y yrhs))" 
   970   show "ardenable (Subst_all ES Y (Arden Y yrhs))"
 
   962     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
 
   971   proof - 
   963   moreover have "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
 
   972     { fix X rhs
 
       
   973       assume "(X, rhs) \<in> ES"
 
       
   974       hence "rhs_nonempty rhs"  using prems invariant_ES  
       
   975         by (simp add:invariant_def ardenable_def)
 
       
   976       with nonempty_yrhs 
       
   977       have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
 
       
   978         by (simp add:nonempty_yrhs 
       
   979                Subst_keeps_nonempty Arden_keeps_nonempty)
 
       
   980     } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
 
       
   981   qed
 
       
   982   show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
 
   964   proof-
 
   983   proof-
 
   965     have "finite_rhs ES" using invariant_ES 
   984     have "finite_rhs ES" using invariant_ES 
   966       by (simp add:invariant_def finite_rhs_def)
 
   985       by (simp add:invariant_def finite_rhs_def)
 
   967     moreover have "finite (Arden Y yrhs)"
 
   986     moreover have "finite (Arden Y yrhs)"
 
   968     proof -
 
   987     proof -
 
   971       thus ?thesis using Arden_keeps_finite by simp
 
   990       thus ?thesis using Arden_keeps_finite by simp
 
   972     qed
 
   991     qed
 
   973     ultimately show ?thesis 
   992     ultimately show ?thesis 
   974       by (simp add:Subst_all_keeps_finite_rhs)
 
   993       by (simp add:Subst_all_keeps_finite_rhs)
 
   975   qed
 
   994   qed
 
   976   moreover have "ardenable (Subst_all ES Y (Arden Y yrhs))"
 
   995   show "self_contained (Subst_all ES Y (Arden Y yrhs))"
 
   977   proof - 
       
   978     { fix X rhs
 
       
   979       assume "(X, rhs) \<in> ES"
 
       
   980       hence "rhs_nonempty rhs"  using prems invariant_ES  
       
   981         by (simp add:invariant_def ardenable_def)
 
       
   982       with nonempty_yrhs 
       
   983       have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
 
       
   984         by (simp add:nonempty_yrhs 
       
   985                Subst_keeps_nonempty Arden_keeps_nonempty)
 
       
   986     } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
 
       
   987   qed
 
       
   988   moreover have "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
 
       
   989   proof-
 
       
   990     have "Y = L (Arden Y yrhs)" 
       
   991       using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs      
       
   992       by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
 
       
   993     thus ?thesis using invariant_ES 
       
   994       by (clarsimp simp add:valid_eqns_def 
       
   995               Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
 
       
   996                    simp del:L_rhs.simps)
 
       
   997   qed
 
       
   998   moreover 
       
   999   have self_subst: "self_contained (Subst_all ES Y (Arden Y yrhs))"
 
       
  1000     using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
 
   996     using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
 
  1001   ultimately show ?thesis using invariant_ES by (simp add:invariant_def)
 
       
  1002 qed
 
   997 qed
 
  1003 
   998 
  1004 lemma Subst_all_card_le: 
   999 lemma Subst_all_card_le: 
  1005   assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
 
  1000   assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
 
  1006   shows "card (Subst_all ES Y yrhs) <= card ES"
 
  1001   shows "card (Subst_all ES Y yrhs) <= card ES"
 
  1034 
  1029 
  1035 lemma iteration_step:
 
  1030 lemma iteration_step:
 
  1036   assumes Inv_ES: "invariant ES"
 
  1031   assumes Inv_ES: "invariant ES"
 
  1037   and    X_in_ES: "(X, xrhs) \<in> ES"
 
  1032   and    X_in_ES: "(X, xrhs) \<in> ES"
 
  1038   and    not_T: "card ES \<noteq> 1"
 
  1033   and    not_T: "card ES \<noteq> 1"
 
  1039   shows "(invariant (iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (iter X ES)) \<and> 
  1034   shows "(invariant (Iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (Iter X ES)) \<and> 
  1040                 (iter X ES, ES) \<in> measure card)"
 
  1035                 (Iter X ES, ES) \<in> measure card)"
 
  1041 proof -
 
  1036 proof -
 
  1042   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
 
  1037   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
 
  1043   then obtain Y yrhs 
  1038   then obtain Y yrhs 
  1044     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1039     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1045     using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)
 
  1040     using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)
 
  1046   let ?ES' = "iter X ES"
 
  1041   let ?ES' = "Iter X ES"
 
  1047   show ?thesis
 
  1042   show ?thesis
 
  1048   proof(unfold iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
 
  1043   proof(unfold Iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
 
  1049     from X_in_ES Y_in_ES and not_eq and Inv_ES
 
  1044     from X_in_ES Y_in_ES and not_eq and Inv_ES
 
  1050     show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
 
  1045     show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
 
  1051       by (auto simp: invariant_def distinct_equas_def)
 
  1046       by (auto simp: invariant_def distinct_equas_def)
 
  1052   next
 
  1047   next
 
  1053     fix x
 
  1048     fix x
 
  1060       show "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
 
  1055       show "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
 
  1061              (\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
 
  1056              (\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
 
  1062              card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
 
  1057              card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
 
  1063       proof -
 
  1058       proof -
 
  1064         have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" 
  1059         have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" 
  1065         proof(rule Subst_all_satisfy_invariant)
 
  1060         proof(rule Subst_all_satisfies_invariant)
 
  1066           from h have "(Y, yrhs) \<in> ES" by simp
 
  1061           from h have "(Y, yrhs) \<in> ES" by simp
 
  1067           hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
 
  1062           hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
 
  1068           with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto
 
  1063           with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto
 
  1069         qed
 
  1064         qed
 
  1070         moreover have 
  1065         moreover have 
  1102 *}
 
  1097 *}
 
  1103 
  1098 
  1104 lemma reduce_x:
 
  1099 lemma reduce_x:
 
  1105   assumes inv: "invariant ES"
 
  1100   assumes inv: "invariant ES"
 
  1106   and contain_x: "(X, xrhs) \<in> ES" 
  1101   and contain_x: "(X, xrhs) \<in> ES" 
  1107   shows "\<exists> xrhs'. reduce X ES = {(X, xrhs')} \<and> invariant(reduce X ES)"
 
  1102   shows "\<exists> xrhs'. Reduce X ES = {(X, xrhs')} \<and> invariant(Reduce X ES)"
 
  1108 proof -
 
  1103 proof -
 
  1109   let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
 
  1104   let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
 
  1110   show ?thesis
 
  1105   show ?thesis
 
  1111   proof (unfold reduce_def, 
  1106   proof (unfold Reduce_def, 
  1112          rule while_rule [where P = ?Inv and r = "measure card"])
 
  1107          rule while_rule [where P = ?Inv and r = "measure card"])
 
  1113     from inv and contain_x show "?Inv ES" by auto
 
  1108     from inv and contain_x show "?Inv ES" by auto
 
  1114   next
 
  1109   next
 
  1115     show "wf (measure card)" by simp
 
  1110     show "wf (measure card)" by simp
 
  1116   next
 
  1111   next
 
  1117     fix ES
 
  1112     fix ES
 
  1118     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1113     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1119     show "(iter X ES, ES) \<in> measure card"
 
  1114     show "(Iter X ES, ES) \<in> measure card"
 
  1120     proof -
 
  1115     proof -
 
  1121       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
 
  1116       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
 
  1122       from inv have "invariant ES" by simp
 
  1117       from inv have "invariant ES" by simp
 
  1123       from iteration_step [OF this x_in crd]
 
  1118       from iteration_step [OF this x_in crd]
 
  1124       show ?thesis by auto
 
  1119       show ?thesis by auto
 
  1125     qed
 
  1120     qed
 
  1126   next
 
  1121   next
 
  1127     fix ES
 
  1122     fix ES
 
  1128     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1123     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1129     thus "?Inv (iter X ES)" 
  1124     thus "?Inv (Iter X ES)" 
  1130     proof -
 
  1125     proof -
 
  1131       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
 
  1126       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
 
  1132       from inv have "invariant ES" by simp
 
  1127       from inv have "invariant ES" by simp
 
  1133       from iteration_step [OF this x_in crd]
 
  1128       from iteration_step [OF this x_in crd]
 
  1134       show ?thesis by auto
 
  1129       show ?thesis by auto
 
  1142   qed
 
  1137   qed
 
  1143 qed
 
  1138 qed
 
  1144 
  1139 
  1145 lemma last_cl_exists_rexp:
 
  1140 lemma last_cl_exists_rexp:
 
  1146   assumes Inv_ES: "invariant {(X, xrhs)}"
 
  1141   assumes Inv_ES: "invariant {(X, xrhs)}"
 
  1147   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
 
  1142   shows "\<exists>r::rexp. L r = X" 
  1148 proof-
 
  1143 proof-
 
  1149   def A \<equiv> "Arden X xrhs"
 
  1144   def A \<equiv> "Arden X xrhs"
 
  1150   have "?P (\<Uplus>{r. Lam r \<in> A})"
 
  1145   have eq: "{Lam r | r. Lam r \<in> A} = A"
 
  1151   proof -
 
  1146   proof -
 
  1152     have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
 
  1147     have "classes_of A = {}" using Inv_ES 
  1153     proof(rule rexp_of_lam_eq_lam_set)
 
  1148       unfolding A_def self_contained_def invariant_def lefts_of_def
 
  1154       show "finite A" 
  1149       by (simp add: Arden_removes_cl) 
  1155 	unfolding A_def
 
  1150     thus ?thesis unfolding A_def classes_of_def
 
  1156 	using Inv_ES
 
  1151       apply(auto simp only:)
 
  1157         by (rule_tac Arden_keeps_finite) 
  1152       apply(case_tac x)
 
  1158            (auto simp add: invariant_def finite_rhs_def)
 
  1153       apply(auto)
 
  1159     qed
 
  1154       done
 
  1160     also have "\<dots> = L A"
 
       
  1161     proof-
 
       
  1162       have "{Lam r | r. Lam r \<in> A} = A"
 
       
  1163       proof-
 
       
  1164         have "classes_of A = {}" using Inv_ES 
       
  1165 	  unfolding A_def
 
       
  1166           by (simp add:Arden_removes_cl 
       
  1167                        self_contained_def invariant_def lefts_of_def) 
       
  1168         thus ?thesis
 
       
  1169 	  unfolding A_def
 
       
  1170           by (auto simp only: classes_of_def, case_tac x, auto)
 
       
  1171       qed
 
       
  1172       thus ?thesis by simp
 
       
  1173     qed
 
       
  1174     also have "\<dots> = X"
 
       
  1175     unfolding A_def
 
       
  1176     proof(rule Arden_keeps_eq [THEN sym])
 
       
  1177       show "X = L xrhs" using Inv_ES 
       
  1178         by (auto simp only: invariant_def valid_eqns_def)  
       
  1179     next
 
       
  1180       from Inv_ES show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
 
       
  1181         by(simp add: invariant_def ardenable_def rexp_of_empty finite_rhs_def)
 
       
  1182     next
 
       
  1183       from Inv_ES show "finite xrhs" 
       
  1184         by (simp add: invariant_def finite_rhs_def)
 
       
  1185     qed
 
       
  1186     finally show ?thesis by simp
 
       
  1187   qed
 
  1155   qed
 
  1188   thus ?thesis by auto
 
  1156   have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
 
       
  1157     using Arden_keeps_finite by auto
 
       
  1158   then have "finite {r. Lam r \<in> A}" by (rule finite_Lam)
 
       
  1159   then have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
 
       
  1160     by auto
 
       
  1161   also have "\<dots> = L A" by (simp add: eq)
 
       
  1162   also have "\<dots> = X" 
       
  1163   proof -
 
       
  1164     have "X = L xrhs" using Inv_ES unfolding invariant_def valid_eqns_def
 
       
  1165       by auto
 
       
  1166     moreover
 
       
  1167     from Inv_ES have "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
 
       
  1168       unfolding invariant_def ardenable_def finite_rhs_def
 
       
  1169       by(simp add: rexp_of_empty)
 
       
  1170     moreover
 
       
  1171     from Inv_ES have "finite xrhs"  unfolding invariant_def finite_rhs_def
 
       
  1172       by simp
 
       
  1173     ultimately show "L A = X" unfolding A_def
 
       
  1174       by (rule  Arden_keeps_eq[symmetric])
 
       
  1175   qed
 
       
  1176   finally have "L (\<Uplus>{r. Lam r \<in> A}) = X" .
 
       
  1177   then show "\<exists>r::rexp. L r = X" by blast
 
  1189 qed
 
  1178 qed
 
  1190 
  1179 
  1191 lemma every_eqcl_has_reg: 
  1180 lemma every_eqcl_has_reg: 
  1192   assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
 
  1181   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
  1193   and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))"
 
  1182   and X_in_CS: "X \<in> (UNIV // \<approx>A)"
 
  1194   shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
 
  1183   shows "\<exists>r::rexp. L r = X"
 
  1195 proof -
 
  1184 proof -
 
  1196   let ?ES = " eqs (UNIV // \<approx>Lang)"
 
  1185   def ES \<equiv> "Init (UNIV // \<approx>A)"
 
  1197   from X_in_CS 
  1186   have "invariant ES" using finite_CS unfolding ES_def
 
  1198   obtain xrhs where "(X, xrhs) \<in> ?ES"
 
  1187     by (rule Init_ES_satisfies_invariant)
 
  1199     by (auto simp:eqs_def init_rhs_def)
 
  1188   moreover
 
  1200   from reduce_x [OF init_ES_satisfy_invariant [OF finite_CS] this]
 
  1189   from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
 
  1201   have "\<exists>xrhs'. reduce X ?ES = {(X, xrhs')} \<and> invariant (reduce X ?ES)" .
 
  1190     unfolding Init_def Init_rhs_def by auto
 
  1202   then obtain xrhs' where "invariant {(X, xrhs')}" by auto
 
  1191   ultimately
 
  1203   from last_cl_exists_rexp [OF this]
 
  1192   obtain xrhs' where "Reduce X ES = {(X, xrhs')}" "invariant (Reduce X ES)"
 
  1204   show ?thesis .
 
  1193     using reduce_x by blast
 
  1205 qed
 
  1194   then show "\<exists>r::rexp. L r = X"
 
  1206 
  1195   using last_cl_exists_rexp by auto
 
  1207 
  1196 qed
 
  1208 theorem hard_direction: 
  1197 
       
  1198 
       
  1199 lemma bchoice_finite_set:
 
       
  1200   assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" 
       
  1201   and     b: "finite S"
 
       
  1202   shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys"
 
       
  1203 using bchoice[OF a] b
 
       
  1204 apply(erule_tac exE)
 
       
  1205 apply(rule_tac x="fa ` S" in exI)
 
       
  1206 apply(auto)
 
       
  1207 done
 
       
  1208 
       
  1209 theorem Myhill_Nerode1:
 
  1209   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
  1210   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
  1210   shows   "\<exists>r::rexp. A = L r"
 
  1211   shows   "\<exists>r::rexp. A = L r"
 
  1211 proof -
 
  1212 proof -
 
  1212   have "\<forall> X \<in> (UNIV // \<approx>A). \<exists>reg::rexp. X = L reg" 
  1213   have f: "finite (finals A)" 
       
  1214     using finals_in_partitions finite_CS by (rule finite_subset)
 
       
  1215   have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r" 
  1213     using finite_CS every_eqcl_has_reg by blast
 
  1216     using finite_CS every_eqcl_has_reg by blast
 
  1214   then obtain f 
  1217   then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r"
 
  1215     where f_prop: "\<forall> X \<in> (UNIV // \<approx>A). X = L ((f X)::rexp)"
 
  1218     using finals_in_partitions by auto
 
  1216     by (auto dest: bchoice)
 
  1219   then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs"
 
  1217   def rs \<equiv> "f ` (finals A)"  
  1220     using f by (auto dest: bchoice_finite_set)
 
  1218   have "A = \<Union> (finals A)" using lang_is_union_of_finals by auto
 
  1221   then have "A = L (\<Uplus>rs)" 
  1219   also have "\<dots> = L (\<Uplus>rs)" 
  1222     unfolding lang_is_union_of_finals[symmetric] by simp
 
  1220   proof -
 
  1223   then show "\<exists>r::rexp. A = L r" by blast
 
  1221     have "finite rs"
 
       
  1222     proof -
 
       
  1223       have "finite (finals A)" 
       
  1224         using finite_CS finals_in_partitions[of "A"]   
       
  1225         by (erule_tac finite_subset, simp)
 
       
  1226       thus ?thesis using rs_def by auto
 
       
  1227     qed
 
       
  1228     thus ?thesis 
       
  1229       using f_prop rs_def finals_in_partitions[of "A"] by auto
 
       
  1230   qed
 
       
  1231   finally show ?thesis by blast
 
       
  1232 qed 
  1224 qed 
  1233 
  1225 
       
  1226 
  1234 end
 
  1227 end
regexp