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 100 2409827d8eb8
parent 99 54aa3b6dd71c
child 101 d3fe0597080a
equal deleted inserted replaced
99:54aa3b6dd71c 100:2409827d8eb8 
   485   "Test ES \<equiv> card ES \<noteq> 1"
 
   485   "Test ES \<equiv> card ES \<noteq> 1"
 
   486 
   486 
   487 definition 
   487 definition 
   488   "Solve X ES \<equiv> while Test (Iter X) ES"
 
   488   "Solve X ES \<equiv> while Test (Iter X) ES"
 
   489 
   489 
   490 
       
   491 (* test *)
 
       
   492 partial_function (tailrec)
 
       
   493   solve
 
       
   494 where
 
       
   495   "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"
 
       
   496 
       
   497 
       
   498 text {*
 
   490 text {*
 
   499   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},
 
   491   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},
 
   500   the induction principle @{thm [source] while_rule} is used to proved the desired properties
 
   492   the induction principle @{thm [source] while_rule} is used to proved the desired properties
 
   501   of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
 
   493   of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
 
   502   in terms of a series of auxilliary predicates:
 
   494   in terms of a series of auxilliary predicates:
 
   664   The following several lemmas until @{text "init_ES_satisfy_invariant"} shows that
 
   656   The following several lemmas until @{text "init_ES_satisfy_invariant"} shows that
 
   665   the initial equational system satisfies invariant @{text "invariant"}.
 
   657   the initial equational system satisfies invariant @{text "invariant"}.
 
   666 *}
 
   658 *}
 
   667 
   659 
   668 lemma defined_by_str:
 
   660 lemma defined_by_str:
 
   669   "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"
 
   661   assumes "s \<in> X" "X \<in> UNIV // \<approx>A" 
   670 by (auto simp:quotient_def Image_def str_eq_rel_def)
 
   662   shows "X = \<approx>A `` {s}"
 
       
   663 using assms
 
       
   664 unfolding quotient_def Image_def str_eq_rel_def
 
       
   665 by auto
 
   671 
   666 
   672 lemma every_eqclass_has_transition:
 
   667 lemma every_eqclass_has_transition:
 
   673   assumes has_str: "s @ [c] \<in> X"
 
   668   assumes has_str: "s @ [c] \<in> X"
 
   674   and     in_CS:   "X \<in> UNIV // (\<approx>Lang)"
 
   669   and     in_CS:   "X \<in> UNIV // \<approx>A"
 
   675   obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
 
   670   obtains Y where "Y \<in> UNIV // \<approx>A" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
 
   676 proof -
 
   671 proof -
 
   677   def Y \<equiv> "(\<approx>Lang) `` {s}"
 
   672   def Y \<equiv> "\<approx>A `` {s}"
 
   678   have "Y \<in> UNIV // (\<approx>Lang)" 
   673   have "Y \<in> UNIV // \<approx>A" 
   679     unfolding Y_def quotient_def by auto
 
   674     unfolding Y_def quotient_def by auto
 
   680   moreover
 
   675   moreover
 
   681   have "X = (\<approx>Lang) `` {s @ [c]}" 
   676   have "X = \<approx>A `` {s @ [c]}" 
   682     using has_str in_CS defined_by_str by blast
 
   677     using has_str in_CS defined_by_str by blast
 
   683   then have "Y ;; {[c]} \<subseteq> X" 
   678   then have "Y ;; {[c]} \<subseteq> X" 
   684     unfolding Y_def Image_def Seq_def
 
   679     unfolding Y_def Image_def Seq_def
 
   685     unfolding str_eq_rel_def
 
   680     unfolding str_eq_rel_def
 
   686     by clarsimp
 
   681     by clarsimp
 
   687   moreover
 
   682   moreover
 
   688   have "s \<in> Y" unfolding Y_def 
   683   have "s \<in> Y" unfolding Y_def 
   689     unfolding Image_def str_eq_rel_def by simp
 
   684     unfolding Image_def str_eq_rel_def by simp
 
   690   ultimately show thesis by (blast intro: that)
 
   685   ultimately show thesis using that by blast
 
   691 qed
 
   686 qed
 
   692 
   687 
   693 lemma l_eq_r_in_eqs:
 
   688 lemma l_eq_r_in_eqs:
 
   694   assumes X_in_eqs: "(X, xrhs) \<in> (Init (UNIV // (\<approx>Lang)))"
 
   689   assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
 
   695   shows "X = L xrhs"
 
   690   shows "X = L rhs"
 
   696 proof 
   691 proof 
   697   show "X \<subseteq> L xrhs"
 
   692   show "X \<subseteq> L rhs"
 
   698   proof
 
   693   proof
 
   699     fix x
 
   694     fix x
 
   700     assume "(1)": "x \<in> X"
 
   695     assume "(1)": "x \<in> X"
 
   701     show "x \<in> L xrhs"          
   696     show "x \<in> L rhs"          
   702     proof (cases "x = []")
 
   697     proof (cases "x = []")
 
   703       assume empty: "x = []"
 
   698       assume empty: "x = []"
 
   704       thus ?thesis using X_in_eqs "(1)"
 
   699       thus ?thesis using X_in_eqs "(1)"
 
   705         by (auto simp: Init_def Init_rhs_def)
 
   700         by (auto simp: Init_def Init_rhs_def)
 
   706     next
 
   701     next
 
   707       assume not_empty: "x \<noteq> []"
 
   702       assume not_empty: "x \<noteq> []"
 
   708       then obtain clist c where decom: "x = clist @ [c]"
 
   703       then obtain clist c where decom: "x = clist @ [c]"
 
   709         by (case_tac x rule:rev_cases, auto)
 
   704         by (case_tac x rule:rev_cases, auto)
 
   710       have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:Init_def)
 
   705       have "X \<in> UNIV // \<approx>A" using X_in_eqs by (auto simp:Init_def)
 
   711       then obtain Y 
   706       then obtain Y 
   712         where "Y \<in> UNIV // (\<approx>Lang)" 
   707         where "Y \<in> UNIV // \<approx>A" 
   713         and "Y ;; {[c]} \<subseteq> X"
 
   708         and "Y ;; {[c]} \<subseteq> X"
 
   714         and "clist \<in> Y"
 
   709         and "clist \<in> Y"
 
   715         using decom "(1)" every_eqclass_has_transition by blast
 
   710         using decom "(1)" every_eqclass_has_transition by blast
 
   716       hence 
   711       hence 
   717         "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
   712         "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
   718         unfolding transition_def
 
   713         unfolding transition_def
 
   719 	using "(1)" decom
 
   714 	using "(1)" decom
 
   720         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
 
   715         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
 
   721       thus ?thesis using X_in_eqs "(1)"	
   716       thus ?thesis using X_in_eqs "(1)"	
   722         by (simp add: Init_def Init_rhs_def)
 
   717         by (simp add: Init_def Init_rhs_def)
 
   723     qed
 
   718     qed
 
   724   qed
 
   719   qed
 
   725 next
 
   720 next
 
   726   show "L xrhs \<subseteq> X" using X_in_eqs
 
   721   show "L rhs \<subseteq> X" using X_in_eqs
 
   727     by (auto simp:Init_def Init_rhs_def transition_def) 
   722     by (auto simp:Init_def Init_rhs_def transition_def) 
   728 qed
 
   723 qed
 
       
   724 
       
   725 lemma test:
 
       
   726   assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
 
       
   727   shows "X = \<Union> (L `  rhs)"
 
       
   728 using assms
 
       
   729 by (drule_tac l_eq_r_in_eqs) (simp)
 
       
   730 
   729 
   731 
   730 lemma finite_Init_rhs: 
   732 lemma finite_Init_rhs: 
   731   assumes finite: "finite CS"
 
   733   assumes finite: "finite CS"
 
   732   shows "finite (Init_rhs CS X)"
 
   734   shows "finite (Init_rhs CS X)"
 
   733 proof-
 
   735 proof-
regexp