8 |
8 |
9 type_synonym 'a lang = "'a list set" |
9 type_synonym 'a lang = "'a list set" |
10 |
10 |
11 definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where |
11 definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where |
12 "A @@ B = {xs@ys | xs ys. xs:A & ys:B}" |
12 "A @@ B = {xs@ys | xs ys. xs:A & ys:B}" |
|
13 |
|
14 text {* checks the code preprocessor for set comprehensions *} |
|
15 export_code conc checking SML |
13 |
16 |
14 overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
17 overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
15 begin |
18 begin |
16 primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where |
19 primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where |
17 "lang_pow 0 A = {[]}" | |
20 "lang_pow 0 A = {[]}" | |
18 "lang_pow (Suc n) A = A @@ (lang_pow n A)" |
21 "lang_pow (Suc n) A = A @@ (lang_pow n A)" |
19 end |
22 end |
20 |
23 |
|
24 text {* for code generation *} |
|
25 |
|
26 definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where |
|
27 lang_pow_code_def [code_abbrev]: "lang_pow = compow" |
|
28 |
|
29 lemma [code]: |
|
30 "lang_pow (Suc n) A = A @@ (lang_pow n A)" |
|
31 "lang_pow 0 A = {[]}" |
|
32 by (simp_all add: lang_pow_code_def) |
|
33 |
|
34 hide_const (open) lang_pow |
|
35 |
21 definition star :: "'a lang \<Rightarrow> 'a lang" where |
36 definition star :: "'a lang \<Rightarrow> 'a lang" where |
22 "star A = (\<Union>n. A ^^ n)" |
37 "star A = (\<Union>n. A ^^ n)" |
23 |
38 |
24 |
39 |
25 subsection{* @{term "op @@"} *} |
40 subsection{* @{term "op @@"} *} |
52 lemma conc_UNION_distrib: |
67 lemma conc_UNION_distrib: |
53 shows "A @@ UNION I M = UNION I (%i. A @@ M i)" |
68 shows "A @@ UNION I M = UNION I (%i. A @@ M i)" |
54 and "UNION I M @@ A = UNION I (%i. M i @@ A)" |
69 and "UNION I M @@ A = UNION I (%i. M i @@ A)" |
55 by auto |
70 by auto |
56 |
71 |
|
72 lemma conc_subset_lists: "A \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S" |
|
73 by(fastforce simp: conc_def in_lists_conv_set) |
|
74 |
57 |
75 |
58 subsection{* @{term "A ^^ n"} *} |
76 subsection{* @{term "A ^^ n"} *} |
59 |
77 |
60 lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m" |
78 lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m" |
61 by (induct n) (auto simp: conc_assoc) |
79 by (induct n) (auto simp: conc_assoc) |
70 shows "A @@ (A ^^ n) = (A ^^ n) @@ A" |
88 shows "A @@ (A ^^ n) = (A ^^ n) @@ A" |
71 by (induct n) (simp_all add: conc_assoc[symmetric]) |
89 by (induct n) (simp_all add: conc_assoc[symmetric]) |
72 |
90 |
73 lemma length_lang_pow_ub: |
91 lemma length_lang_pow_ub: |
74 "ALL w : A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n" |
92 "ALL w : A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n" |
75 by(induct n arbitrary: w) (fastsimp simp: conc_def)+ |
93 by(induct n arbitrary: w) (fastforce simp: conc_def)+ |
76 |
94 |
77 lemma length_lang_pow_lb: |
95 lemma length_lang_pow_lb: |
78 "ALL w : A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n" |
96 "ALL w : A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n" |
79 by(induct n arbitrary: w) (fastsimp simp: conc_def)+ |
97 by(induct n arbitrary: w) (fastforce simp: conc_def)+ |
|
98 |
|
99 lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S" |
|
100 by(induction n)(auto simp: conc_subset_lists[OF assms]) |
80 |
101 |
81 |
102 |
82 subsection{* @{const star} *} |
103 subsection{* @{const star} *} |
|
104 |
|
105 lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S" |
|
106 unfolding star_def by(blast dest: lang_pow_subset_lists) |
83 |
107 |
84 lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A" |
108 lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A" |
85 by (auto simp: star_def) |
109 by (auto simp: star_def) |
86 |
110 |
87 lemma Nil_in_star[iff]: "[] : star A" |
111 lemma Nil_in_star[iff]: "[] : star A" |
159 assume "EX us. ?R w us" thus "w : star A" |
183 assume "EX us. ?R w us" thus "w : star A" |
160 by (auto simp: concat_in_star) |
184 by (auto simp: concat_in_star) |
161 qed |
185 qed |
162 |
186 |
163 lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}" |
187 lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}" |
164 by (fastsimp simp: in_star_iff_concat) |
188 by (fastforce simp: in_star_iff_concat) |
165 |
189 |
166 lemma star_insert_eps[simp]: "star (insert [] A) = star(A)" |
190 lemma star_insert_eps[simp]: "star (insert [] A) = star(A)" |
167 proof- |
191 proof- |
168 { fix us |
192 { fix us |
169 have "set us \<subseteq> insert [] A \<Longrightarrow> EX vs. concat us = concat vs \<and> set vs \<subseteq> A" |
193 have "set us \<subseteq> insert [] A \<Longrightarrow> EX vs. concat us = concat vs \<and> set vs \<subseteq> A" |
177 |
201 |
178 lemma star_decom: |
202 lemma star_decom: |
179 assumes a: "x \<in> star A" "x \<noteq> []" |
203 assumes a: "x \<in> star A" "x \<noteq> []" |
180 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A" |
204 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A" |
181 using a by (induct rule: star_induct) (blast)+ |
205 using a by (induct rule: star_induct) (blast)+ |
|
206 |
|
207 |
|
208 subsection {* Left-Quotients of languages *} |
|
209 |
|
210 definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
|
211 where "Deriv x A = { xs. x#xs \<in> A }" |
|
212 |
|
213 definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
|
214 where "Derivs xs A = { ys. xs @ ys \<in> A }" |
|
215 |
|
216 abbreviation |
|
217 Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang" |
|
218 where |
|
219 "Derivss s As \<equiv> \<Union> (Derivs s) ` As" |
|
220 |
|
221 |
|
222 lemma Deriv_empty[simp]: "Deriv a {} = {}" |
|
223 and Deriv_epsilon[simp]: "Deriv a {[]} = {}" |
|
224 and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})" |
|
225 and Deriv_union[simp]: "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B" |
|
226 and Deriv_inter[simp]: "Deriv a (A \<inter> B) = Deriv a A \<inter> Deriv a B" |
|
227 and Deriv_compl[simp]: "Deriv a (-A) = - Deriv a A" |
|
228 and Deriv_Union[simp]: "Deriv a (Union M) = Union(Deriv a ` M)" |
|
229 and Deriv_UN[simp]: "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))" |
|
230 by (auto simp: Deriv_def) |
|
231 |
|
232 lemma Der_conc [simp]: "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})" |
|
233 unfolding Deriv_def conc_def |
|
234 by (auto simp add: Cons_eq_append_conv) |
|
235 |
|
236 lemma Deriv_star [simp]: "Deriv c (star A) = (Deriv c A) @@ star A" |
|
237 proof - |
|
238 have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A" |
|
239 unfolding Deriv_def conc_def |
|
240 apply(auto simp add: Cons_eq_append_conv) |
|
241 apply(drule star_decom) |
|
242 apply(auto simp add: Cons_eq_append_conv) |
|
243 done |
|
244 |
|
245 have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})" |
|
246 by (simp only: star_unfold_left[symmetric]) |
|
247 also have "... = Deriv c (A @@ star A)" |
|
248 by (simp only: Deriv_union) (simp) |
|
249 also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})" |
|
250 by simp |
|
251 also have "... = (Deriv c A) @@ star A" |
|
252 using incl by auto |
|
253 finally show "Deriv c (star A) = (Deriv c A) @@ star A" . |
|
254 qed |
|
255 |
|
256 lemma Deriv_diff[simp]: "Deriv c (A - B) = Deriv c A - Deriv c B" |
|
257 by(auto simp add: Deriv_def) |
|
258 |
|
259 lemma Deriv_lists[simp]: "c : S \<Longrightarrow> Deriv c (lists S) = lists S" |
|
260 by(auto simp add: Deriv_def) |
|
261 |
|
262 lemma Derivs_simps [simp]: |
|
263 shows "Derivs [] A = A" |
|
264 and "Derivs (c # s) A = Derivs s (Deriv c A)" |
|
265 and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)" |
|
266 unfolding Derivs_def Deriv_def by auto |
|
267 |
182 |
268 |
183 subsection {* Arden's Lemma *} |
269 subsection {* Arden's Lemma *} |
184 |
270 |
185 lemma arden_helper: |
271 lemma arden_helper: |
186 assumes eq: "X = A @@ X \<union> B" |
272 assumes eq: "X = A @@ X \<union> B" |