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 79 bba9c80735f9
parent 76 1589bf5c1ad8
child 80 f901a26bf1ac
equal deleted inserted replaced
78:77583805123d 79:bba9c80735f9 
   333 
   333 
   334 text {* 
   334 text {* 
   335   The following lemma ensures that the arbitrary choice made by the 
   335   The following lemma ensures that the arbitrary choice made by the 
   336   @{text "SOME"} in @{text "folds"} does not affect the @{text "L"}-value 
   336   @{text "SOME"} in @{text "folds"} does not affect the @{text "L"}-value 
   337   of the resultant regular expression. 
   337   of the resultant regular expression. 
   338   *}
 
   338 *}
 
   339 
   339 
   340 lemma folds_alt_simp [simp]:
 
   340 lemma folds_alt_simp [simp]:
 
   341   assumes a: "finite rs"
 
   341   assumes a: "finite rs"
 
   342   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
 
   342   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
 
   343 apply(rule set_eqI)
 
   343 apply(rule set_eqI)
 
   386 apply(auto)
 
   386 apply(auto)
 
   387 apply(drule_tac x = "[]" in spec)
 
   387 apply(drule_tac x = "[]" in spec)
 
   388 apply(auto)
 
   388 apply(auto)
 
   389 done
 
   389 done
 
   390 
   390 
   391 lemma finals_included_in_UNIV:
 
   391 lemma finals_in_partitions:
 
   392   shows "finals A \<subseteq> UNIV // \<approx>A"
 
   392   shows "finals A \<subseteq> (UNIV // \<approx>A)"
 
   393 unfolding finals_def
 
   393 unfolding finals_def
 
   394 unfolding quotient_def
 
   394 unfolding quotient_def
 
   395 by auto
 
   395 by auto
 
   396 
       
   397 
   396 
   398 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
 
   397 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
 
   399 
   398 
   400 text {* 
   399 text {* 
   401   The relationship between equivalent classes can be described by an
 
   400   The relationship between equivalent classes can be described by an
 
   443   the_r :: "rhs_item \<Rightarrow> rexp"
 
   442   the_r :: "rhs_item \<Rightarrow> rexp"
 
   444 where 
   443 where 
   445   "the_r (Lam r) = r"
 
   444   "the_r (Lam r) = r"
 
   446 
   445 
   447 fun 
   446 fun 
   448   the_Trn:: "rhs_item \<Rightarrow> (lang \<times> rexp)"
 
   447   the_trn_rexp:: "rhs_item \<Rightarrow> rexp"
 
   449 where 
   448 where 
   450   "the_Trn (Trn Y r) = (Y, r)"
 
   449   "the_trn_rexp (Trn Y r) = r"
 
   451 
   450 
   452 text {*
 
   451 text {*
 
   453   Every right-hand side item @{text "itm"} defines a language given 
   452   Every right-hand side item @{text "itm"} defines a language given 
   454   by @{text "L(itm)"}, defined as:
 
   453   by @{text "L(itm)"}, defined as:
 
   455 *}
 
   454 *}
 
   512 
   511 
   513 
   512 
   514 (************ arden's lemma variation ********************)
 
   513 (************ arden's lemma variation ********************)
 
   515 
   514 
   516 text {* 
   515 text {* 
   517   The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.
 
   516   The following @{text "trns_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.
 
   518 *}
 
   517 *}
 
   519 
   518 
   520 definition
 
   519 definition
 
   521   "items_of rhs X \<equiv> {Trn X r | r. (Trn X r) \<in> rhs}"
 
   520   "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}"
 
   522 
   521 
   523 text {* 
   522 text {* 
   524   The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items
 
   523   The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items
 
   525   using @{text "ALT"} to form a single regular expression. 
   524   using @{text "ALT"} to form a single regular expression. 
   526   It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}.
 
   525   It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}.
 
   527   *}
 
   526   *}
 
   528 
   527 
   529 definition 
   528 definition 
   530   "rexp_of rhs X \<equiv> \<Uplus>((snd o the_Trn) ` items_of rhs X)"
 
   529   "rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}"
 
   531 
   530 
   532 text {* 
   531 text {* 
   533   The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.
 
   532   The following @{text "lam_of rhs"} returns all pure regular expression trns in @{text "rhs"}.
 
   534 *}
 
   533 *}
 
   535 
   534 
   536 definition
 
   535 definition
 
   537   "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
 
   536   "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
 
   538 
   537 
   543   is used to compute compute the regular expression corresponds to @{text "rhs"}.
 
   542   is used to compute compute the regular expression corresponds to @{text "rhs"}.
 
   544 *}
 
   543 *}
 
   545 
   544 
   546 
   545 
   547 definition
 
   546 definition
 
   548   "rexp_of_lam rhs \<equiv> \<Uplus>(the_r ` lam_of rhs)"
 
   547   "rexp_of_lam rhs \<equiv> \<Uplus> {r. Lam r \<in> rhs}"
 
   549 
   548 
   550 text {*
 
   549 text {*
 
   551   The following @{text "attach_rexp rexp' itm"} attach 
   550   The following @{text "attach_rexp rexp' itm"} attach 
   552   the regular expression @{text "rexp'"} to
 
   551   the regular expression @{text "rexp'"} to
 
   553   the right of right hand side item @{text "itm"}.
 
   552   the right of right hand side item @{text "itm"}.
 
   576   by @{text "rhs"} is kept unchanged.
 
   575   by @{text "rhs"} is kept unchanged.
 
   577 *}
 
   576 *}
 
   578 
   577 
   579 definition 
   578 definition 
   580   "arden_variate X rhs \<equiv> 
   579   "arden_variate X rhs \<equiv> 
   581         append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"
 
   580         append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
 
   582 
   581 
   583 
   582 
   584 (*********** substitution of ES *************)
 
   583 (*********** substitution of ES *************)
 
   585 
   584 
   586 text {* 
   585 text {* 
   592   union the result with all non-@{text "X"}-items of @{text "rhs"}.
 
   591   union the result with all non-@{text "X"}-items of @{text "rhs"}.
 
   593  *}
 
   592  *}
 
   594 
   593 
   595 definition 
   594 definition 
   596   "rhs_subst rhs X xrhs \<equiv> 
   595   "rhs_subst rhs X xrhs \<equiv> 
   597         (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"
 
   596         (rhs - (trns_of rhs X)) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
 
   598 
   597 
   599 text {*
 
   598 text {*
 
   600   Suppose the equation defining @{text "X"} is $X = xrhs$, the follwing
 
   599   Suppose the equation defining @{text "X"} is $X = xrhs$, the follwing
 
   601   @{text "eqs_subst ES X xrhs"} substitute @{text "xrhs"} into every equation
 
   600   @{text "eqs_subst ES X xrhs"} substitute @{text "xrhs"} into every equation
 
   602   of the equational system @{text "ES"}.
 
   601   of the equational system @{text "ES"}.
 
   726 lemma L_rhs_union_distrib:
 
   725 lemma L_rhs_union_distrib:
 
   727   fixes A B::"rhs_item set"
 
   726   fixes A B::"rhs_item set"
 
   728   shows "L A \<union> L B = L (A \<union> B)"
 
   727   shows "L A \<union> L B = L (A \<union> B)"
 
   729 by simp
 
   728 by simp
 
   730 
   729 
   731 lemma finite_snd_Trn:
 
   730 lemma finite_Trn:
 
   732   assumes finite:"finite rhs"
 
   731   assumes fin: "finite rhs"
 
   733   shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \<in> rhs}" (is "finite ?B")
 
   732   shows "finite {r. Trn Y r \<in> rhs}"
 
   734 proof-
 
   733 proof -
 
   735   def rhs' \<equiv> "{e \<in> rhs. \<exists> r. e = Trn Y r}"
 
   734   have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}"
 
   736   have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def)
 
   735     by (rule rev_finite_subset[OF fin]) (auto)
 
   737   moreover have "finite rhs'" using finite rhs'_def by auto
 
   736   then have "finite (the_trn_rexp ` {Trn Y r | Y r. Trn Y r \<in> rhs})"
 
   738   ultimately show ?thesis by simp
 
   737     by auto
 
       
   738   then show "finite {r. Trn Y r \<in> rhs}"
 
       
   739     apply(erule_tac rev_finite_subset)
 
       
   740     apply(auto simp add: image_def)
 
       
   741     apply(rule_tac x="Trn Y x" in exI)
 
       
   742     apply(auto)
 
       
   743     done
 
       
   744 qed
 
       
   745 
       
   746 lemma finite_Lam:
 
       
   747   assumes fin:"finite rhs"
 
       
   748   shows "finite {r. Lam r \<in> rhs}"
 
       
   749 proof -
 
       
   750   have "finite {Lam r | r. Lam r \<in> rhs}"
 
       
   751     by (rule rev_finite_subset[OF fin]) (auto)
 
       
   752   then have "finite (the_r ` {Lam r | r. Lam r \<in> rhs})"
 
       
   753     by auto
 
       
   754   then show "finite {r. Lam r \<in> rhs}"
 
       
   755     apply(erule_tac rev_finite_subset)
 
       
   756     apply(auto simp add: image_def)
 
       
   757     done
 
   739 qed
 
   758 qed
 
   740 
   759 
   741 lemma rexp_of_empty:
 
   760 lemma rexp_of_empty:
 
   742   assumes finite:"finite rhs"
 
   761   assumes finite:"finite rhs"
 
   743   and nonempty:"rhs_nonempty rhs"
 
   762   and nonempty:"rhs_nonempty rhs"
 
   744   shows "[] \<notin> L (rexp_of rhs X)"
 
   763   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 
   745 using finite nonempty rhs_nonempty_def
 
   764 using finite nonempty rhs_nonempty_def
 
   746 by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def)
 
   765 using finite_Trn[OF finite]
 
       
   766 by (auto)
 
   747 
   767 
   748 lemma [intro!]:
 
   768 lemma [intro!]:
 
   749   "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
 
   769   "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
 
   750 
   770 
   751 lemma finite_items_of:
 
       
   752   "finite rhs \<Longrightarrow> finite (items_of rhs X)"
 
       
   753 by (auto simp:items_of_def intro:finite_subset)
 
       
   754 
       
   755 lemma lang_of_rexp_of:
 
   771 lemma lang_of_rexp_of:
 
   756   assumes finite:"finite rhs"
 
   772   assumes finite:"finite rhs"
 
   757   shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))"
 
   773   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 
   758 proof -
 
   774 proof -
 
   759   have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto
 
   775   have "finite {r. Trn X r \<in> rhs}" 
   760   thus ?thesis
 
   776     by (rule finite_Trn[OF finite]) 
   761     apply (auto simp:rexp_of_def Seq_def items_of_def)
 
   777   then show ?thesis
 
   762     apply (rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
 
   778     apply(auto simp add: Seq_def)
 
   763     by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)
 
   779     apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
 
       
   780     apply(rule_tac x= "Trn X xa" in exI)
 
       
   781     apply(auto simp: Seq_def)
 
       
   782     done
 
   764 qed
 
   783 qed
 
   765 
   784 
   766 lemma rexp_of_lam_eq_lam_set:
 
   785 lemma rexp_of_lam_eq_lam_set:
 
   767   assumes finite: "finite rhs"
 
   786   assumes fin: "finite rhs"
 
   768   shows "L (rexp_of_lam rhs) = L (lam_of rhs)"
 
   787   shows "L (\<Uplus>{r. Lam r \<in> rhs}) = L ({Lam r | r. Lam r \<in> rhs})"
 
   769 proof -
 
   788 proof -
 
   770   have "finite (the_r ` {Lam r |r. Lam r \<in> rhs})" using finite
 
   789   have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam)
 
   771     by (rule_tac finite_imageI, auto intro:finite_subset)
 
   790   then show ?thesis by auto
 
   772   thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def)
 
       
   773 qed
 
   791 qed
 
   774 
   792 
   775 lemma [simp]:
 
   793 lemma [simp]:
 
   776   "L (attach_rexp r xb) = L xb ;; L r"
 
   794   "L (attach_rexp r xb) = L xb ;; L r"
 
   777 apply (cases xb, auto simp:Seq_def)
 
   795 apply (cases xb, auto simp: Seq_def)
 
   778 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
 
   796 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
 
   779 apply(auto simp: Seq_def)
 
   797 apply(auto simp: Seq_def)
 
   780 done
 
   798 done
 
   781 
   799 
   782 lemma lang_of_append_rhs:
 
   800 lemma lang_of_append_rhs:
 
   914   decreasing the size of @{text "ES"}.
 
   932   decreasing the size of @{text "ES"}.
 
   915 *}
 
   933 *}
 
   916 
   934 
   917 lemma arden_variate_keeps_eq:
 
   935 lemma arden_variate_keeps_eq:
 
   918   assumes l_eq_r: "X = L rhs"
 
   936   assumes l_eq_r: "X = L rhs"
 
   919   and not_empty: "[] \<notin> L (rexp_of rhs X)"
 
   937   and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
 
   920   and finite: "finite rhs"
 
   938   and finite: "finite rhs"
 
   921   shows "X = L (arden_variate X rhs)"
 
   939   shows "X = L (arden_variate X rhs)"
 
   922 proof -
 
   940 proof -
 
   923   def A \<equiv> "L (rexp_of rhs X)"
 
   941   thm rexp_of_def
 
   924   def b \<equiv> "rhs - items_of rhs X"
 
   942   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
 
       
   943   def b \<equiv> "rhs - trns_of rhs X"
 
   925   def B \<equiv> "L b" 
   944   def B \<equiv> "L b" 
   926   have "X = B ;; A\<star>"
 
   945   have "X = B ;; A\<star>"
 
   927   proof-
 
   946   proof-
 
   928     have "rhs = items_of rhs X \<union> b" by (auto simp:b_def items_of_def)
 
   947     have "L rhs = L(trns_of rhs X \<union> b)" by (auto simp: b_def trns_of_def)
 
   929     hence "L rhs = L(items_of rhs X \<union> b)" by simp
 
   948     also have "\<dots> = X ;; A \<union> B"
 
   930     hence "L rhs = L(items_of rhs X) \<union> B" by (simp only:L_rhs_union_distrib B_def)
 
   949       unfolding trns_of_def
 
   931     with lang_of_rexp_of
 
   950       unfolding L_rhs_union_distrib[symmetric]
 
   932     have "L rhs = X ;; A \<union> B " using finite by (simp only:B_def b_def A_def)
 
   951       by (simp only: lang_of_rexp_of finite B_def A_def)
 
   933     thus ?thesis
 
   952     finally show ?thesis
 
   934       using l_eq_r not_empty
 
   953       using l_eq_r not_empty
 
   935       apply (drule_tac B = B and X = X in ardens_revised)
 
   954       apply(rule_tac ardens_revised[THEN iffD1])
 
   936       by (auto simp:A_def simp del:L_rhs.simps)
 
   955       apply(simp add: A_def)
 
       
   956       apply(simp)
 
       
   957       done
 
   937   qed
 
   958   qed
 
   938   moreover have "L (arden_variate X rhs) = (B ;; A\<star>)" (is "?L = ?R")
 
   959   moreover have "L (arden_variate X rhs) = (B ;; A\<star>)"
 
   939     by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 
   960     by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 
   940                   B_def A_def b_def L_rexp.simps seq_union_distrib_left)
 
   961                   B_def A_def b_def L_rexp.simps seq_union_distrib_left)
 
   941    ultimately show ?thesis by simp
 
   962    ultimately show ?thesis by simp
 
   942 qed 
   963 qed 
   943 
   964 
   974 lemma rhs_subst_keeps_eq:
 
   995 lemma rhs_subst_keeps_eq:
 
   975   assumes substor: "X = L xrhs"
 
   996   assumes substor: "X = L xrhs"
 
   976   and finite: "finite rhs"
 
   997   and finite: "finite rhs"
 
   977   shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
 
   998   shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
 
   978 proof-
 
   999 proof-
 
   979   def A \<equiv> "L (rhs - items_of rhs X)"
 
  1000   def A \<equiv> "L (rhs - trns_of rhs X)"
 
   980   have "?Left = A \<union> L (append_rhs_rexp xrhs (rexp_of rhs X))"
 
  1001   have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
 
   981     by (simp only:rhs_subst_def L_rhs_union_distrib A_def)
 
  1002     unfolding rhs_subst_def
 
   982   moreover have "?Right = A \<union> L (items_of rhs X)"
 
  1003     unfolding L_rhs_union_distrib[symmetric]
 
       
  1004     by (simp add: A_def)
 
       
  1005   moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})"
 
   983   proof-
 
  1006   proof-
 
   984     have "rhs = (rhs - items_of rhs X) \<union> (items_of rhs X)" by (auto simp:items_of_def)
 
  1007     have "rhs = (rhs - trns_of rhs X) \<union> (trns_of rhs X)" by (auto simp add: trns_of_def)
 
   985     thus ?thesis by (simp only:L_rhs_union_distrib A_def)
 
  1008     thus ?thesis 
       
  1009       unfolding A_def
 
       
  1010       unfolding L_rhs_union_distrib
 
       
  1011       unfolding trns_of_def
 
       
  1012       by simp
 
   986   qed
 
  1013   qed
 
   987   moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)" 
  1014   moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 
   988     using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)
 
  1015     using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)
 
   989   ultimately show ?thesis by simp
 
  1016   ultimately show ?thesis by simp
 
   990 qed
 
  1017 qed
 
   991 
  1018 
   992 lemma rhs_subst_keeps_finite_rhs:
 
  1019 lemma rhs_subst_keeps_finite_rhs:
 
  1019 apply (case_tac xa, auto simp:image_def)
 
  1046 apply (case_tac xa, auto simp:image_def)
 
  1020 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
  1047 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
  1021 
  1048 
  1022 lemma arden_variate_removes_cl:
 
  1049 lemma arden_variate_removes_cl:
 
  1023   "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}"
 
  1050   "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}"
 
  1024 apply (simp add:arden_variate_def append_rhs_keeps_cls items_of_def)
 
  1051 apply (simp add:arden_variate_def append_rhs_keeps_cls trns_of_def)
 
  1025 by (auto simp:classes_of_def)
 
  1052 by (auto simp:classes_of_def)
 
  1026 
  1053 
  1027 lemma lefts_of_keeps_cls:
 
  1054 lemma lefts_of_keeps_cls:
 
  1028   "lefts_of (eqs_subst ES Y yrhs) = lefts_of ES"
 
  1055   "lefts_of (eqs_subst ES Y yrhs) = lefts_of ES"
 
  1029 by (auto simp:lefts_of_def eqs_subst_def)
 
  1056 by (auto simp:lefts_of_def eqs_subst_def)
 
  1031 lemma rhs_subst_updates_cls:
 
  1058 lemma rhs_subst_updates_cls:
 
  1032   "X \<notin> classes_of xrhs \<Longrightarrow> 
  1059   "X \<notin> classes_of xrhs \<Longrightarrow> 
  1033       classes_of (rhs_subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
 
  1060       classes_of (rhs_subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
 
  1034 apply (simp only:rhs_subst_def append_rhs_keeps_cls 
  1061 apply (simp only:rhs_subst_def append_rhs_keeps_cls 
  1035                               classes_of_union_distrib[THEN sym])
 
  1062                               classes_of_union_distrib[THEN sym])
 
  1036 by (auto simp:classes_of_def items_of_def)
 
  1063 by (auto simp:classes_of_def trns_of_def)
 
  1037 
  1064 
  1038 lemma eqs_subst_keeps_self_contained:
 
  1065 lemma eqs_subst_keeps_self_contained:
 
  1039   fixes Y
 
  1066   fixes Y
 
  1040   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
 
  1067   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
 
  1041   shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" 
  1068   shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" 
  1221 lemma last_cl_exists_rexp:
 
  1248 lemma last_cl_exists_rexp:
 
  1222   assumes ES_single: "ES = {(X, xrhs)}" 
  1249   assumes ES_single: "ES = {(X, xrhs)}" 
  1223   and Inv_ES: "Inv ES"
 
  1250   and Inv_ES: "Inv ES"
 
  1224   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
 
  1251   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
 
  1225 proof-
 
  1252 proof-
 
  1226   let ?A = "arden_variate X xrhs"
 
  1253   def A \<equiv> "arden_variate X xrhs"
 
  1227   have "?P (rexp_of_lam ?A)"
 
  1254   have "?P (rexp_of_lam A)"
 
  1228   proof -
 
  1255   proof -
 
  1229     have "L (rexp_of_lam ?A) = L (lam_of ?A)"
 
  1256     thm lam_of_def
 
       
  1257     thm rexp_of_lam_def
 
       
  1258     have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
 
  1230     proof(rule rexp_of_lam_eq_lam_set)
 
  1259     proof(rule rexp_of_lam_eq_lam_set)
 
  1231       show "finite (arden_variate X xrhs)" using Inv_ES ES_single 
  1260       show "finite A" 
  1232         by (rule_tac arden_variate_keeps_finite, 
  1261 	unfolding A_def
 
  1233                        auto simp add:Inv_def finite_rhs_def)
 
  1262 	using Inv_ES ES_single 
       
  1263         by (rule_tac arden_variate_keeps_finite) 
       
  1264            (auto simp add: Inv_def finite_rhs_def)
 
  1234     qed
 
  1265     qed
 
  1235     also have "\<dots> = L ?A"
 
  1266     also have "\<dots> = L A"
 
  1236     proof-
 
  1267     proof-
 
  1237       have "lam_of ?A = ?A"
 
  1268       have "lam_of A = A"
 
  1238       proof-
 
  1269       proof-
 
  1239         have "classes_of ?A = {}" using Inv_ES ES_single
 
  1270         have "classes_of A = {}" using Inv_ES ES_single
 
       
  1271 	  unfolding A_def
 
  1240           by (simp add:arden_variate_removes_cl 
  1272           by (simp add:arden_variate_removes_cl 
  1241                        self_contained_def Inv_def lefts_of_def) 
  1273                        self_contained_def Inv_def lefts_of_def) 
  1242         thus ?thesis 
  1274         thus ?thesis
 
       
  1275 	  unfolding A_def
 
  1243           by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)
 
  1276           by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)
 
  1244       qed
 
  1277       qed
 
  1245       thus ?thesis by simp
 
  1278       thus ?thesis unfolding lam_of_def by simp
 
  1246     qed
 
  1279     qed
 
  1247     also have "\<dots> = X"
 
  1280     also have "\<dots> = X"
 
       
  1281     unfolding A_def
 
  1248     proof(rule arden_variate_keeps_eq [THEN sym])
 
  1282     proof(rule arden_variate_keeps_eq [THEN sym])
 
  1249       show "X = L xrhs" using Inv_ES ES_single 
  1283       show "X = L xrhs" using Inv_ES ES_single 
  1250         by (auto simp only:Inv_def valid_eqns_def)  
  1284         by (auto simp only:Inv_def valid_eqns_def)  
  1251     next
 
  1285     next
 
  1252       from Inv_ES ES_single show "[] \<notin> L (rexp_of xrhs X)"
 
  1286       from Inv_ES ES_single show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
 
  1253         by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def)
 
  1287         by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def)
 
  1254     next
 
  1288     next
 
  1255       from Inv_ES ES_single show "finite xrhs" 
  1289       from Inv_ES ES_single show "finite xrhs" 
  1256         by (simp add:Inv_def finite_rhs_def)
 
  1290         by (simp add:Inv_def finite_rhs_def)
 
  1257     qed
 
  1291     qed
 
  1258     finally show ?thesis by simp
 
  1292     finally show ?thesis unfolding rexp_of_lam_def by simp
 
  1259   qed
 
  1293   qed
 
  1260   thus ?thesis by auto
 
  1294   thus ?thesis by auto
 
  1261 qed
 
  1295 qed
 
  1262    
  1296    
  1263 lemma every_eqcl_has_reg: 
  1297 lemma every_eqcl_has_reg: 
  1275   hence ES_single_equa: "ES = {(X, xrhs)}" 
  1309   hence ES_single_equa: "ES = {(X, xrhs)}" 
  1276     by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) 
  1310     by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) 
  1277   thus ?thesis using Inv_ES
 
  1311   thus ?thesis using Inv_ES
 
  1278     by (rule last_cl_exists_rexp)
 
  1312     by (rule last_cl_exists_rexp)
 
  1279 qed
 
  1313 qed
 
  1280 
       
  1281 lemma finals_in_partitions:
 
       
  1282   shows "finals A \<subseteq> (UNIV // \<approx>A)"
 
       
  1283 unfolding finals_def
 
       
  1284 unfolding quotient_def
 
       
  1285 by auto
 
       
  1286 
  1314 
  1287 theorem hard_direction: 
  1315 theorem hard_direction: 
  1288   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
  1316   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
  1289   shows   "\<exists>r::rexp. A = L r"
 
  1317   shows   "\<exists>r::rexp. A = L r"
 
  1290 proof -
 
  1318 proof -
regexp