80 apply (case_tac "s2 = []") |
80 apply (case_tac "s2 = []") |
81 apply (rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start) |
81 apply (rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start) |
82 apply (simp, (erule exE| erule conjE)+) |
82 apply (simp, (erule exE| erule conjE)+) |
83 by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step) |
83 by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step) |
84 |
84 |
|
85 |
|
86 text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *} |
|
87 datatype rexp = |
|
88 NULL |
|
89 | EMPTY |
|
90 | CHAR char |
|
91 | SEQ rexp rexp |
|
92 | ALT rexp rexp |
|
93 | STAR rexp |
|
94 |
|
95 |
|
96 text {* |
|
97 The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to |
|
98 the language represented by the syntactic object @{text "x"}. |
|
99 *} |
|
100 consts L:: "'a \<Rightarrow> string set" |
|
101 |
|
102 |
|
103 text {* |
|
104 The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the |
|
105 following overloading function @{text "L_rexp"}. |
|
106 *} |
|
107 overloading L_rexp \<equiv> "L:: rexp \<Rightarrow> string set" |
|
108 begin |
|
109 fun |
|
110 L_rexp :: "rexp \<Rightarrow> string set" |
|
111 where |
|
112 "L_rexp (NULL) = {}" |
|
113 | "L_rexp (EMPTY) = {[]}" |
|
114 | "L_rexp (CHAR c) = {[c]}" |
|
115 | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)" |
|
116 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)" |
|
117 | "L_rexp (STAR r) = (L_rexp r)\<star>" |
|
118 end |
|
119 |
|
120 (* Just a technical lemma. *) |
|
121 lemma [simp]: |
|
122 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
|
123 by simp |
|
124 |
|
125 text {* |
|
126 @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}. |
|
127 *} |
|
128 definition |
|
129 str_eq_rel ("\<approx>_" [100] 100) |
|
130 where |
|
131 "\<approx>Lang \<equiv> {(x, y). (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}" |
|
132 |
|
133 text {* |
|
134 Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out |
|
135 those which contains strings from @{text "Lang"}. |
|
136 *} |
|
137 |
|
138 definition |
|
139 "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}" |
|
140 |
|
141 text {* |
|
142 The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}. |
|
143 *} |
|
144 lemma lang_is_union_of_finals: |
|
145 "Lang = \<Union> finals(Lang)" |
|
146 proof |
|
147 show "Lang \<subseteq> \<Union> (finals Lang)" |
|
148 proof |
|
149 fix x |
|
150 assume "x \<in> Lang" |
|
151 thus "x \<in> \<Union> (finals Lang)" |
|
152 apply (simp add:finals_def, rule_tac x = "(\<approx>Lang) `` {x}" in exI) |
|
153 by (auto simp:Image_def str_eq_rel_def) |
|
154 qed |
|
155 next |
|
156 show "\<Union> (finals Lang) \<subseteq> Lang" |
|
157 apply (clarsimp simp:finals_def str_eq_rel_def) |
|
158 by (drule_tac x = "[]" in spec, auto) |
|
159 qed |
|
160 |
|
161 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*} |
|
162 |
|
163 subsection {* |
|
164 Ardens lemma |
|
165 *} |
85 text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *} |
166 text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *} |
86 |
167 |
87 theorem ardens_revised: |
168 theorem ardens_revised: |
88 assumes nemp: "[] \<notin> A" |
169 assumes nemp: "[] \<notin> A" |
89 shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)" |
170 shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)" |
142 } thus ?thesis by blast |
223 } thus ?thesis by blast |
143 qed |
224 qed |
144 qed |
225 qed |
145 qed |
226 qed |
146 |
227 |
147 |
228 subsection {* |
148 text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *} |
229 Defintions peculiar to this direction |
149 datatype rexp = |
230 *} |
150 NULL |
|
151 | EMPTY |
|
152 | CHAR char |
|
153 | SEQ rexp rexp |
|
154 | ALT rexp rexp |
|
155 | STAR rexp |
|
156 |
|
157 |
|
158 text {* |
|
159 The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to |
|
160 the language represented by the syntactic object @{text "x"}. |
|
161 *} |
|
162 consts L:: "'a \<Rightarrow> string set" |
|
163 |
|
164 |
|
165 text {* |
|
166 The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the |
|
167 following overloading function @{text "L_rexp"}. |
|
168 *} |
|
169 overloading L_rexp \<equiv> "L:: rexp \<Rightarrow> string set" |
|
170 begin |
|
171 fun |
|
172 L_rexp :: "rexp \<Rightarrow> string set" |
|
173 where |
|
174 "L_rexp (NULL) = {}" |
|
175 | "L_rexp (EMPTY) = {[]}" |
|
176 | "L_rexp (CHAR c) = {[c]}" |
|
177 | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)" |
|
178 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)" |
|
179 | "L_rexp (STAR r) = (L_rexp r)\<star>" |
|
180 end |
|
181 |
231 |
182 text {* |
232 text {* |
183 To obtain equational system out of finite set of equivalent classes, a fold operation |
233 To obtain equational system out of finite set of equivalent classes, a fold operation |
184 on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"} |
234 on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"} |
185 more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"} |
235 more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"} |
199 lemma folds_alt_simp [simp]: |
249 lemma folds_alt_simp [simp]: |
200 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
250 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
201 apply (rule set_eq_intro, simp add:folds_def) |
251 apply (rule set_eq_intro, simp add:folds_def) |
202 apply (rule someI2_ex, erule finite_imp_fold_graph) |
252 apply (rule someI2_ex, erule finite_imp_fold_graph) |
203 by (erule fold_graph.induct, auto) |
253 by (erule fold_graph.induct, auto) |
204 |
|
205 (* Just a technical lemma. *) |
|
206 lemma [simp]: |
|
207 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
|
208 by simp |
|
209 |
|
210 text {* |
|
211 @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}. |
|
212 *} |
|
213 definition |
|
214 str_eq_rel ("\<approx>_" [100] 100) |
|
215 where |
|
216 "\<approx>Lang \<equiv> {(x, y). (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}" |
|
217 |
|
218 text {* |
|
219 Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out |
|
220 those which contains strings from @{text "Lang"}. |
|
221 *} |
|
222 |
|
223 definition |
|
224 "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}" |
|
225 |
|
226 text {* |
|
227 The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}. |
|
228 *} |
|
229 lemma lang_is_union_of_finals: |
|
230 "Lang = \<Union> finals(Lang)" |
|
231 proof |
|
232 show "Lang \<subseteq> \<Union> (finals Lang)" |
|
233 proof |
|
234 fix x |
|
235 assume "x \<in> Lang" |
|
236 thus "x \<in> \<Union> (finals Lang)" |
|
237 apply (simp add:finals_def, rule_tac x = "(\<approx>Lang) `` {x}" in exI) |
|
238 by (auto simp:Image_def str_eq_rel_def) |
|
239 qed |
|
240 next |
|
241 show "\<Union> (finals Lang) \<subseteq> Lang" |
|
242 apply (clarsimp simp:finals_def str_eq_rel_def) |
|
243 by (drule_tac x = "[]" in spec, auto) |
|
244 qed |
|
245 |
|
246 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*} |
|
247 |
254 |
248 text {* |
255 text {* |
249 The relationship between equivalent classes can be described by an |
256 The relationship between equivalent classes can be described by an |
250 equational system. |
257 equational system. |
251 For example, in equational system \eqref{example_eqns}, $X_0, X_1$ are equivalent |
258 For example, in equational system \eqref{example_eqns}, $X_0, X_1$ are equivalent |