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 179 edacc141060f
parent 170 b1258b7d2789
child 181 97090fc7aa9f
equal deleted inserted replaced
178:c6ebfe052109 179:edacc141060f 
     3         "~~/src/HOL/Library/While_Combinator" 
     3         "~~/src/HOL/Library/While_Combinator" 
     4 begin
 
     4 begin
 
     5 
     5 
     6 section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
 
     6 section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
 
     7 
     7 
     8 lemma Pair_Collect[simp]:
 
     8 lemma Pair_Collect [simp]:
 
     9   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 
     9   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 
    10 by simp
 
    10 by simp
 
    11 
    11 
    12 text {* Myhill-Nerode relation *}
 
    12 text {* Myhill-Nerode relation *}
 
    13 
    13 
    55 lemma lang_rhs_set:
 
    55 lemma lang_rhs_set:
 
    56   shows "lang_rhs {Trn X r | r. P r} = \<Union>{lang_trm (Trn X r) | r. P r}"
 
    56   shows "lang_rhs {Trn X r | r. P r} = \<Union>{lang_trm (Trn X r) | r. P r}"
 
    57 by (auto)
 
    57 by (auto)
 
    58 
    58 
    59 lemma lang_rhs_union_distrib:
 
    59 lemma lang_rhs_union_distrib:
 
    60   fixes A B::"('a trm) set"
 
       
    61   shows "lang_rhs A \<union> lang_rhs B = lang_rhs (A \<union> B)"
 
    60   shows "lang_rhs A \<union> lang_rhs B = lang_rhs (A \<union> B)"
 
    62 by simp
 
    61 by simp
 
    63 
    62 
    64 
    63 
    65 text {* Transitions between equivalence classes *}
 
    64 text {* Transitions between equivalence classes *}
 
   348     by auto
 
   347     by auto
 
   349 qed
 
   348 qed
 
   350 
   349 
   351 subsubsection {* Interation step *}
 
   350 subsubsection {* Interation step *}
 
   352 
   351 
   353 lemma Arden_keeps_eq:
 
   352 lemma Arden_preserves_soundness:
 
   354   assumes l_eq_r: "X = lang_rhs rhs"
 
   353   assumes l_eq_r: "X = lang_rhs rhs"
 
   355   and not_empty: "ardenable rhs"
 
   354   and not_empty: "ardenable rhs"
 
   356   and finite: "finite rhs"
 
   355   and finite: "finite rhs"
 
   357   shows "X = lang_rhs (Arden X rhs)"
 
   356   shows "X = lang_rhs (Arden X rhs)"
 
   358 proof -
 
   357 proof -
 
   377     unfolding Arden_def A_def B_def b_def
 
   376     unfolding Arden_def A_def B_def b_def
 
   378     by (simp only: lang_of_append_rexp_rhs lang.simps)
 
   377     by (simp only: lang_of_append_rexp_rhs lang.simps)
 
   379   finally show "X = lang_rhs (Arden X rhs)" by simp
 
   378   finally show "X = lang_rhs (Arden X rhs)" by simp
 
   380 qed 
   379 qed 
   381 
   380 
   382 lemma Append_keeps_finite:
 
   381 lemma Append_preserves_finite:
 
   383   "finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
 
   382   "finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
 
   384 by (auto simp: Append_rexp_rhs_def)
 
   383 by (auto simp: Append_rexp_rhs_def)
 
   385 
   384 
   386 lemma Arden_keeps_finite:
 
   385 lemma Arden_preserves_finite:
 
   387   "finite rhs \<Longrightarrow> finite (Arden X rhs)"
 
   386   "finite rhs \<Longrightarrow> finite (Arden X rhs)"
 
   388 by (auto simp: Arden_def Append_keeps_finite)
 
   387 by (auto simp: Arden_def Append_preserves_finite)
 
   389 
   388 
   390 lemma Append_keeps_nonempty:
 
   389 lemma Append_preserves_ardenable:
 
   391   "ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
 
   390   "ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
 
   392 apply (auto simp: ardenable_def Append_rexp_rhs_def)
 
   391 apply (auto simp: ardenable_def Append_rexp_rhs_def)
 
   393 by (case_tac x, auto simp: conc_def)
 
   392 by (case_tac x, auto simp: conc_def)
 
   394 
   393 
   395 lemma nonempty_set_sub:
 
   394 lemma ardenable_set_sub:
 
   396   "ardenable rhs \<Longrightarrow> ardenable (rhs - A)"
 
   395   "ardenable rhs \<Longrightarrow> ardenable (rhs - A)"
 
   397 by (auto simp:ardenable_def)
 
   396 by (auto simp:ardenable_def)
 
   398 
   397 
   399 lemma nonempty_set_union:
 
   398 lemma ardenable_set_union:
 
   400   "\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')"
 
   399   "\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')"
 
   401 by (auto simp:ardenable_def)
 
   400 by (auto simp:ardenable_def)
 
   402 
   401 
   403 lemma Arden_keeps_nonempty:
 
   402 lemma Arden_preserves_ardenable:
 
   404   "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
 
   403   "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
 
   405 by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub)
 
   404 by (simp only:Arden_def Append_preserves_ardenable ardenable_set_sub)
 
   406 
   405 
   407 
   406 
   408 lemma Subst_keeps_nonempty:
 
   407 lemma Subst_preserves_ardenable:
 
   409   "\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)"
 
   408   "\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)"
 
   410 by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub)
 
   409 by (simp only: Subst_def Append_preserves_ardenable ardenable_set_union ardenable_set_sub)
 
   411 
   410 
   412 lemma Subst_keeps_eq:
 
   411 lemma Subst_preserves_soundness:
 
   413   assumes substor: "X = lang_rhs xrhs"
 
   412   assumes substor: "X = lang_rhs xrhs"
 
   414   and finite: "finite rhs"
 
   413   and finite: "finite rhs"
 
   415   shows "lang_rhs (Subst rhs X xrhs) = lang_rhs rhs" (is "?Left = ?Right")
 
   414   shows "lang_rhs (Subst rhs X xrhs) = lang_rhs rhs" (is "?Left = ?Right")
 
   416 proof-
 
   415 proof-
 
   417   def A \<equiv> "lang_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs})"
 
   416   def A \<equiv> "lang_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs})"
 
   431   have "lang_rhs (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = lang_rhs {Trn X r | r. Trn X r \<in> rhs}" 
   430   have "lang_rhs (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = lang_rhs {Trn X r | r. Trn X r \<in> rhs}" 
   432     using finite substor by (simp only: lang_of_append_rexp_rhs trm_soundness)
 
   431     using finite substor by (simp only: lang_of_append_rexp_rhs trm_soundness)
 
   433   ultimately show ?thesis by simp
 
   432   ultimately show ?thesis by simp
 
   434 qed
 
   433 qed
 
   435 
   434 
   436 lemma Subst_keeps_finite_rhs:
 
   435 lemma Subst_preserves_finite_rhs:
 
   437   "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
 
   436   "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
 
   438 by (auto simp: Subst_def Append_keeps_finite)
 
   437 by (auto simp: Subst_def Append_preserves_finite)
 
   439 
   438 
   440 lemma Subst_all_keeps_finite:
 
   439 lemma Subst_all_preserves_finite:
 
   441   assumes finite: "finite ES"
 
   440   assumes finite: "finite ES"
 
   442   shows "finite (Subst_all ES Y yrhs)"
 
   441   shows "finite (Subst_all ES Y yrhs)"
 
   443 proof -
 
   442 proof -
 
   444   def eqns \<equiv> "{(X::'a lang, rhs) |X rhs. (X, rhs) \<in> ES}"
 
   443   def eqns \<equiv> "{(X::'a lang, rhs) |X rhs. (X, rhs) \<in> ES}"
 
   445   def h \<equiv> "\<lambda>(X::'a lang, rhs). (X, Subst rhs Y yrhs)"
 
   444   def h \<equiv> "\<lambda>(X::'a lang, rhs). (X, Subst rhs Y yrhs)"
 
   448   have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto
 
   447   have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto
 
   449   ultimately
 
   448   ultimately
 
   450   show "finite (Subst_all ES Y yrhs)" by simp
 
   449   show "finite (Subst_all ES Y yrhs)" by simp
 
   451 qed
 
   450 qed
 
   452 
   451 
   453 lemma Subst_all_keeps_finite_rhs:
 
   452 lemma Subst_all_preserves_finite_rhs:
 
   454   "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
 
   453   "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
 
   455 by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
 
   454 by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def)
 
   456 
   455 
   457 lemma append_rhs_keeps_cls:
 
   456 lemma append_rhs_preserves_cls:
 
   458   "rhss (Append_rexp_rhs rhs r) = rhss rhs"
 
   457   "rhss (Append_rexp_rhs rhs r) = rhss rhs"
 
   459 apply (auto simp: rhss_def Append_rexp_rhs_def)
 
   458 apply (auto simp: rhss_def Append_rexp_rhs_def)
 
   460 apply (case_tac xa, auto simp: image_def)
 
   459 apply (case_tac xa, auto simp: image_def)
 
   461 by (rule_tac x = "Times ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
   460 by (rule_tac x = "Times ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
   462 
   461 
   463 lemma Arden_removes_cl:
 
   462 lemma Arden_removes_cl:
 
   464   "rhss (Arden Y yrhs) = rhss yrhs - {Y}"
 
   463   "rhss (Arden Y yrhs) = rhss yrhs - {Y}"
 
   465 apply (simp add:Arden_def append_rhs_keeps_cls)
 
   464 apply (simp add:Arden_def append_rhs_preserves_cls)
 
   466 by (auto simp: rhss_def)
 
   465 by (auto simp: rhss_def)
 
   467 
   466 
   468 lemma lhss_keeps_cls:
 
   467 lemma lhss_preserves_cls:
 
   469   "lhss (Subst_all ES Y yrhs) = lhss ES"
 
   468   "lhss (Subst_all ES Y yrhs) = lhss ES"
 
   470 by (auto simp: lhss_def Subst_all_def)
 
   469 by (auto simp: lhss_def Subst_all_def)
 
   471 
   470 
   472 lemma Subst_updates_cls:
 
   471 lemma Subst_updates_cls:
 
   473   "X \<notin> rhss xrhs \<Longrightarrow> 
   472   "X \<notin> rhss xrhs \<Longrightarrow> 
   474       rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}"
 
   473       rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}"
 
   475 apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
 
   474 apply (simp only:Subst_def append_rhs_preserves_cls rhss_union_distrib)
 
   476 by (auto simp: rhss_def)
 
   475 by (auto simp: rhss_def)
 
   477 
   476 
   478 lemma Subst_all_keeps_validity:
 
   477 lemma Subst_all_preserves_validity:
 
   479   assumes sc: "validity (ES \<union> {(Y, yrhs)})"        (is "validity ?A")
 
   478   assumes sc: "validity (ES \<union> {(Y, yrhs)})"        (is "validity ?A")
 
   480   shows "validity (Subst_all ES Y (Arden Y yrhs))"  (is "validity ?B")
 
   479   shows "validity (Subst_all ES Y (Arden Y yrhs))"  (is "validity ?B")
 
   481 proof -
 
   480 proof -
 
   482   { fix X xrhs'
 
   481   { fix X xrhs'
 
   483     assume "(X, xrhs') \<in> ?B"
 
   482     assume "(X, xrhs') \<in> ?B"
 
   514 proof (rule invariantI)
 
   513 proof (rule invariantI)
 
   515   have Y_eq_yrhs: "Y = lang_rhs yrhs" 
   514   have Y_eq_yrhs: "Y = lang_rhs yrhs" 
   516     using invariant_ES by (simp only:invariant_def soundness_def, blast)
 
   515     using invariant_ES by (simp only:invariant_def soundness_def, blast)
 
   517    have finite_yrhs: "finite yrhs" 
   516    have finite_yrhs: "finite yrhs" 
   518     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
 
   517     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
 
   519   have nonempty_yrhs: "ardenable yrhs" 
   518   have ardenable_yrhs: "ardenable yrhs" 
   520     using invariant_ES by (auto simp:invariant_def ardenable_all_def)
 
   519     using invariant_ES by (auto simp:invariant_def ardenable_all_def)
 
   521   show "soundness (Subst_all ES Y (Arden Y yrhs))"
 
   520   show "soundness (Subst_all ES Y (Arden Y yrhs))"
 
   522   proof -
 
   521   proof -
 
   523     have "Y = lang_rhs (Arden Y yrhs)" 
   522     have "Y = lang_rhs (Arden Y yrhs)" 
   524       using Y_eq_yrhs invariant_ES finite_yrhs
 
   523       using Y_eq_yrhs invariant_ES finite_yrhs
 
   525       using finite_Trn[OF finite_yrhs]
 
   524       using finite_Trn[OF finite_yrhs]
 
   526       apply(rule_tac Arden_keeps_eq)
 
   525       apply(rule_tac Arden_preserves_soundness)
 
   527       apply(simp_all)
 
   526       apply(simp_all)
 
   528       unfolding invariant_def ardenable_all_def ardenable_def
 
   527       unfolding invariant_def ardenable_all_def ardenable_def
 
   529       apply(auto)
 
   528       apply(auto)
 
   530       done
 
   529       done
 
   531     thus ?thesis using invariant_ES
 
   530     thus ?thesis using invariant_ES
 
   532       unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
 
   531       unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
 
   533       by (auto simp add: Subst_keeps_eq simp del: lang_rhs.simps)
 
   532       by (auto simp add: Subst_preserves_soundness simp del: lang_rhs.simps)
 
   534   qed
 
   533   qed
 
   535   show "finite (Subst_all ES Y (Arden Y yrhs))" 
   534   show "finite (Subst_all ES Y (Arden Y yrhs))" 
   536     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
 
   535     using invariant_ES by (simp add:invariant_def Subst_all_preserves_finite)
 
   537   show "distinctness (Subst_all ES Y (Arden Y yrhs))" 
   536   show "distinctness (Subst_all ES Y (Arden Y yrhs))" 
   538     using invariant_ES 
   537     using invariant_ES 
   539     unfolding distinctness_def Subst_all_def invariant_def by auto
 
   538     unfolding distinctness_def Subst_all_def invariant_def by auto
 
   540   show "ardenable_all (Subst_all ES Y (Arden Y yrhs))"
 
   539   show "ardenable_all (Subst_all ES Y (Arden Y yrhs))"
 
   541   proof - 
   540   proof - 
   542     { fix X rhs
 
   541     { fix X rhs
 
   543       assume "(X, rhs) \<in> ES"
 
   542       assume "(X, rhs) \<in> ES"
 
   544       hence "ardenable rhs"  using invariant_ES  
   543       hence "ardenable rhs"  using invariant_ES  
   545         by (auto simp add:invariant_def ardenable_all_def)
 
   544         by (auto simp add:invariant_def ardenable_all_def)
 
   546       with nonempty_yrhs 
   545       with ardenable_yrhs 
   547       have "ardenable (Subst rhs Y (Arden Y yrhs))"
 
   546       have "ardenable (Subst rhs Y (Arden Y yrhs))"
 
   548         by (simp add:nonempty_yrhs 
   547         by (simp add:ardenable_yrhs 
   549                Subst_keeps_nonempty Arden_keeps_nonempty)
 
   548                Subst_preserves_ardenable Arden_preserves_ardenable)
 
   550     } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def)
 
   549     } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def)
 
   551   qed
 
   550   qed
 
   552   show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
 
   551   show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
 
   553   proof-
 
   552   proof-
 
   554     have "finite_rhs ES" using invariant_ES 
   553     have "finite_rhs ES" using invariant_ES 
   555       by (simp add:invariant_def finite_rhs_def)
 
   554       by (simp add:invariant_def finite_rhs_def)
 
   556     moreover have "finite (Arden Y yrhs)"
 
   555     moreover have "finite (Arden Y yrhs)"
 
   557     proof -
 
   556     proof -
 
   558       have "finite yrhs" using invariant_ES 
   557       have "finite yrhs" using invariant_ES 
   559         by (auto simp:invariant_def finite_rhs_def)
 
   558         by (auto simp:invariant_def finite_rhs_def)
 
   560       thus ?thesis using Arden_keeps_finite by auto
 
   559       thus ?thesis using Arden_preserves_finite by auto
 
   561     qed
 
   560     qed
 
   562     ultimately show ?thesis 
   561     ultimately show ?thesis 
   563       by (simp add:Subst_all_keeps_finite_rhs)
 
   562       by (simp add:Subst_all_preserves_finite_rhs)
 
   564   qed
 
   563   qed
 
   565   show "validity (Subst_all ES Y (Arden Y yrhs))"
 
   564   show "validity (Subst_all ES Y (Arden Y yrhs))"
 
   566     using invariant_ES Subst_all_keeps_validity by (auto simp add: invariant_def)
 
   565     using invariant_ES Subst_all_preserves_validity by (auto simp add: invariant_def)
 
   567 qed
 
   566 qed
 
   568 
   567 
   569 lemma Remove_in_card_measure:
 
   568 lemma Remove_in_card_measure:
 
   570   assumes finite: "finite ES"
 
   569   assumes finite: "finite ES"
 
   571   and     in_ES: "(X, rhs) \<in> ES"
 
   570   and     in_ES: "(X, rhs) \<in> ES"
 
   732     by (simp add: Arden_removes_cl)
 
   731     by (simp add: Arden_removes_cl)
 
   733   then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def
 
   732   then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def
 
   734     by (auto, case_tac x, auto)
 
   733     by (auto, case_tac x, auto)
 
   735   
   734   
   736   have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
 
   735   have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
 
   737     using Arden_keeps_finite by auto
 
   736     using Arden_preserves_finite by auto
 
   738   then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
 
   737   then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
 
   739 
   738 
   740   have "X = lang_rhs xrhs" using Inv_ES unfolding invariant_def soundness_def
 
   739   have "X = lang_rhs xrhs" using Inv_ES unfolding invariant_def soundness_def
 
   741     by simp
 
   740     by simp
 
   742   then have "X = lang_rhs A" using Inv_ES 
   741   then have "X = lang_rhs A" using Inv_ES 
   743     unfolding A_def invariant_def ardenable_all_def finite_rhs_def 
   742     unfolding A_def invariant_def ardenable_all_def finite_rhs_def 
   744     by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
 
   743     by (rule_tac Arden_preserves_soundness) (simp_all add: finite_Trn)
 
   745   then have "X = lang_rhs {Lam r | r. Lam r \<in> A}" using eq by simp
 
   744   then have "X = lang_rhs {Lam r | r. Lam r \<in> A}" using eq by simp
 
   746   then have "X = lang (\<Uplus>{r. Lam r \<in> A})" using fin by auto
 
   745   then have "X = lang (\<Uplus>{r. Lam r \<in> A})" using fin by auto
 
   747   then show "\<exists>r. X = lang r" by blast
 
   746   then show "\<exists>r. X = lang r" by blast
 
   748 qed
 
   747 qed
 
   749 
   748
regexp