equal
deleted
inserted
replaced
1 theory Myhill_1 |
1 theory Myhill_1 |
2 imports More_Regular_Set |
2 imports "Folds" |
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 {* First direction of MN: @{text "finite partition \<Rightarrow> regular language"} *} |
|
7 |
|
8 notation |
|
9 conc (infixr "\<cdot>" 100) and |
|
10 star ("_\<star>" [101] 102) |
7 |
11 |
8 lemma Pair_Collect [simp]: |
12 lemma Pair_Collect [simp]: |
9 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
13 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
10 by simp |
14 by simp |
11 |
15 |
12 text {* Myhill-Nerode relation *} |
16 text {* Myhill-Nerode relation *} |
13 |
|
14 |
17 |
15 definition |
18 definition |
16 str_eq :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100) |
19 str_eq :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100) |
17 where |
20 where |
18 "\<approx>A \<equiv> {(x, y). (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}" |
21 "\<approx>A \<equiv> {(x, y). (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}" |
37 lemma finals_in_partitions: |
40 lemma finals_in_partitions: |
38 shows "finals A \<subseteq> (UNIV // \<approx>A)" |
41 shows "finals A \<subseteq> (UNIV // \<approx>A)" |
39 unfolding finals_def quotient_def |
42 unfolding finals_def quotient_def |
40 by auto |
43 by auto |
41 |
44 |
42 section {* Equational systems *} |
45 subsection {* Equational systems *} |
43 |
46 |
44 text {* The two kinds of terms in the rhs of equations. *} |
47 text {* The two kinds of terms in the rhs of equations. *} |
45 |
48 |
46 datatype 'a trm = |
49 datatype 'a trm = |
47 Lam "'a rexp" (* Lambda-marker *) |
50 Lam "'a rexp" (* Lambda-marker *) |
85 |
88 |
86 definition |
89 definition |
87 "Init CS \<equiv> {(X, Init_rhs CS X) | X. X \<in> CS}" |
90 "Init CS \<equiv> {(X, Init_rhs CS X) | X. X \<in> CS}" |
88 |
91 |
89 |
92 |
90 section {* Arden Operation on equations *} |
93 subsection {* Arden Operation on equations *} |
91 |
94 |
92 fun |
95 fun |
93 Append_rexp :: "'a rexp \<Rightarrow> 'a trm \<Rightarrow> 'a trm" |
96 Append_rexp :: "'a rexp \<Rightarrow> 'a trm \<Rightarrow> 'a trm" |
94 where |
97 where |
95 "Append_rexp r (Lam rexp) = Lam (Times rexp r)" |
98 "Append_rexp r (Lam rexp) = Lam (Times rexp r)" |
102 definition |
105 definition |
103 "Arden X rhs \<equiv> |
106 "Arden X rhs \<equiv> |
104 Append_rexp_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs}) (Star (\<Uplus> {r. Trn X r \<in> rhs}))" |
107 Append_rexp_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs}) (Star (\<Uplus> {r. Trn X r \<in> rhs}))" |
105 |
108 |
106 |
109 |
107 section {* Substitution Operation on equations *} |
110 subsection {* Substitution Operation on equations *} |
108 |
111 |
109 definition |
112 definition |
110 "Subst rhs X xrhs \<equiv> |
113 "Subst rhs X xrhs \<equiv> |
111 (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (Append_rexp_rhs xrhs (\<Uplus> {r. Trn X r \<in> rhs}))" |
114 (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (Append_rexp_rhs xrhs (\<Uplus> {r. Trn X r \<in> rhs}))" |
112 |
115 |
118 definition |
121 definition |
119 "Remove ES X xrhs \<equiv> |
122 "Remove ES X xrhs \<equiv> |
120 Subst_all (ES - {(X, xrhs)}) X (Arden X xrhs)" |
123 Subst_all (ES - {(X, xrhs)}) X (Arden X xrhs)" |
121 |
124 |
122 |
125 |
123 section {* While-combinator *} |
126 subsection {* While-combinator and invariants *} |
124 |
127 |
125 definition |
128 definition |
126 "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y |
129 "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y |
127 in Remove ES Y yrhs)" |
130 in Remove ES Y yrhs)" |
128 |
131 |
139 |
142 |
140 definition |
143 definition |
141 "Solve X ES \<equiv> while Cond (Iter X) ES" |
144 "Solve X ES \<equiv> while Cond (Iter X) ES" |
142 |
145 |
143 |
146 |
144 section {* Invariants *} |
|
145 |
|
146 definition |
147 definition |
147 "distinctness ES \<equiv> |
148 "distinctness ES \<equiv> |
148 \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'" |
149 \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'" |
149 |
150 |
150 definition |
151 definition |
194 assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES" |
195 assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES" |
195 "finite_rhs ES" "validity ES" |
196 "finite_rhs ES" "validity ES" |
196 shows "invariant ES" |
197 shows "invariant ES" |
197 using assms by (simp add: invariant_def) |
198 using assms by (simp add: invariant_def) |
198 |
199 |
199 |
|
200 subsection {* The proof of this direction *} |
|
201 |
200 |
202 lemma finite_Trn: |
201 lemma finite_Trn: |
203 assumes fin: "finite rhs" |
202 assumes fin: "finite rhs" |
204 shows "finite {r. Trn Y r \<in> rhs}" |
203 shows "finite {r. Trn Y r \<in> rhs}" |
205 proof - |
204 proof - |
245 "lang_rhs (Append_rexp_rhs rhs r) = lang_rhs rhs \<cdot> lang r" |
244 "lang_rhs (Append_rexp_rhs rhs r) = lang_rhs rhs \<cdot> lang r" |
246 unfolding Append_rexp_rhs_def |
245 unfolding Append_rexp_rhs_def |
247 by (auto simp add: conc_def lang_of_append_rexp) |
246 by (auto simp add: conc_def lang_of_append_rexp) |
248 |
247 |
249 |
248 |
250 subsubsection {* Intial Equational System *} |
249 subsection {* Intial Equational Systems *} |
251 |
250 |
252 lemma defined_by_str: |
251 lemma defined_by_str: |
253 assumes "s \<in> X" "X \<in> UNIV // \<approx>A" |
252 assumes "s \<in> X" "X \<in> UNIV // \<approx>A" |
254 shows "X = \<approx>A `` {s}" |
253 shows "X = \<approx>A `` {s}" |
255 using assms |
254 using assms |
351 show "validity (Init (UNIV // \<approx>A))" |
350 show "validity (Init (UNIV // \<approx>A))" |
352 unfolding validity_def Init_def Init_rhs_def rhss_def lhss_def |
351 unfolding validity_def Init_def Init_rhs_def rhss_def lhss_def |
353 by auto |
352 by auto |
354 qed |
353 qed |
355 |
354 |
356 subsubsection {* Interation step *} |
355 subsection {* Interations *} |
357 |
356 |
358 lemma Arden_preserves_soundness: |
357 lemma Arden_preserves_soundness: |
359 assumes l_eq_r: "X = lang_rhs rhs" |
358 assumes l_eq_r: "X = lang_rhs rhs" |
360 and not_empty: "ardenable rhs" |
359 and not_empty: "ardenable rhs" |
361 and finite: "finite rhs" |
360 and finite: "finite rhs" |
375 unfolding trm_soundness[OF finite] |
374 unfolding trm_soundness[OF finite] |
376 unfolding A_def |
375 unfolding A_def |
377 by blast |
376 by blast |
378 finally have "X = X \<cdot> A \<union> B" . |
377 finally have "X = X \<cdot> A \<union> B" . |
379 then have "X = B \<cdot> A\<star>" |
378 then have "X = B \<cdot> A\<star>" |
380 by (simp add: arden[OF not_empty2]) |
379 by (simp add: reversed_Arden[OF not_empty2]) |
381 also have "\<dots> = lang_rhs (Arden X rhs)" |
380 also have "\<dots> = lang_rhs (Arden X rhs)" |
382 unfolding Arden_def A_def B_def b_def |
381 unfolding Arden_def A_def B_def b_def |
383 by (simp only: lang_of_append_rexp_rhs lang.simps) |
382 by (simp only: lang_of_append_rexp_rhs lang.simps) |
384 finally show "X = lang_rhs (Arden X rhs)" by simp |
383 finally show "X = lang_rhs (Arden X rhs)" by simp |
385 qed |
384 qed |
674 apply(auto) |
673 apply(auto) |
675 done |
674 done |
676 qed |
675 qed |
677 |
676 |
678 |
677 |
679 subsubsection {* Conclusion of the proof *} |
678 subsection {* The conclusion of the first direction *} |
680 |
679 |
681 lemma Solve: |
680 lemma Solve: |
682 fixes A::"('a::finite) lang" |
681 fixes A::"('a::finite) lang" |
683 assumes fin: "finite (UNIV // \<approx>A)" |
682 assumes fin: "finite (UNIV // \<approx>A)" |
684 and X_in: "X \<in> (UNIV // \<approx>A)" |
683 and X_in: "X \<in> (UNIV // \<approx>A)" |