1 theory Derivatives |
1 theory Derivatives |
2 imports Myhill_2 |
2 imports Regular_Exp |
3 begin |
3 begin |
4 |
4 |
5 section {* Left-Quotients and Derivatives *} |
5 section {* Leftquotients, Derivatives and Partial Derivatives *} |
6 |
6 |
7 subsection {* Left-Quotients *} |
7 text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *} |
8 |
8 |
9 definition |
9 subsection {* Left-Quotients of languages *} |
10 Delta :: "'a lang \<Rightarrow> 'a lang" |
10 |
11 where |
11 definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
12 "Delta A = (if [] \<in> A then {[]} else {})" |
12 where "Deriv x A = { xs. x#xs \<in> A }" |
13 |
13 |
14 definition |
14 definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
15 Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
15 where "Derivs xs A = { ys. xs @ ys \<in> A }" |
16 where |
|
17 "Der c A \<equiv> {s'. [c] @ s' \<in> A}" |
|
18 |
|
19 definition |
|
20 Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
|
21 where |
|
22 "Ders s A \<equiv> {s'. s @ s' \<in> A}" |
|
23 |
16 |
24 abbreviation |
17 abbreviation |
25 "Derss s A \<equiv> \<Union> (Ders s) ` A" |
18 Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang" |
26 |
19 where |
27 lemma Der_simps [simp]: |
20 "Derivss s As \<equiv> \<Union> (Derivs s) ` As" |
28 shows "Der c {} = {}" |
21 |
29 and "Der c {[]} = {}" |
22 |
30 and "Der c {[d]} = (if c = d then {[]} else {})" |
23 lemma Deriv_empty[simp]: "Deriv a {} = {}" |
31 and "Der c (A \<union> B) = Der c A \<union> Der c B" |
24 and Deriv_epsilon[simp]: "Deriv a {[]} = {}" |
32 unfolding Der_def by auto |
25 and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})" |
|
26 and Deriv_union[simp]: "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B" |
|
27 by (auto simp: Deriv_def) |
|
28 |
|
29 lemma Deriv_conc_subset: |
|
30 "Deriv a A @@ B \<subseteq> Deriv a (A @@ B)" (is "?L \<subseteq> ?R") |
|
31 proof |
|
32 fix w assume "w \<in> ?L" |
|
33 then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B" |
|
34 by (auto simp: Deriv_def) |
|
35 then have "a # w \<in> A @@ B" |
|
36 by (auto intro: concI[of "a # u", simplified]) |
|
37 thus "w \<in> ?R" by (auto simp: Deriv_def) |
|
38 qed |
33 |
39 |
34 lemma Der_conc [simp]: |
40 lemma Der_conc [simp]: |
35 shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)" |
41 shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})" |
36 unfolding Der_def Delta_def conc_def |
42 unfolding Deriv_def conc_def |
37 by (auto simp add: Cons_eq_append_conv) |
43 by (auto simp add: Cons_eq_append_conv) |
38 |
44 |
39 lemma Der_star [simp]: |
45 lemma Deriv_star [simp]: |
40 shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" |
46 shows "Deriv c (star A) = (Deriv c A) @@ star A" |
41 proof - |
47 proof - |
42 have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>" |
48 have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A" |
43 unfolding Der_def Delta_def conc_def |
49 unfolding Deriv_def conc_def |
44 apply(auto) |
50 apply(auto simp add: Cons_eq_append_conv) |
45 apply(drule star_decom) |
51 apply(drule star_decom) |
46 apply(auto simp add: Cons_eq_append_conv) |
52 apply(auto simp add: Cons_eq_append_conv) |
47 done |
53 done |
48 |
54 |
49 have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})" |
55 have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})" |
50 by (simp only: star_unfold_left[symmetric]) |
56 by (simp only: star_unfold_left[symmetric]) |
51 also have "... = Der c (A \<cdot> A\<star>)" |
57 also have "... = Deriv c (A @@ star A)" |
52 by (simp only: Der_simps) (simp) |
58 by (simp only: Deriv_union) (simp) |
53 also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))" |
59 also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})" |
54 by simp |
60 by simp |
55 also have "... = (Der c A) \<cdot> A\<star>" |
61 also have "... = (Deriv c A) @@ star A" |
56 using incl by auto |
62 using incl by auto |
57 finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . |
63 finally show "Deriv c (star A) = (Deriv c A) @@ star A" . |
58 qed |
64 qed |
59 |
65 |
60 lemma Ders_simps [simp]: |
66 lemma Derivs_simps [simp]: |
61 shows "Ders [] A = A" |
67 shows "Derivs [] A = A" |
62 and "Ders (c # s) A = Ders s (Der c A)" |
68 and "Derivs (c # s) A = Derivs s (Deriv c A)" |
63 and "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)" |
69 and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)" |
64 unfolding Ders_def Der_def by auto |
70 unfolding Derivs_def Deriv_def by auto |
|
71 |
|
72 (* |
|
73 lemma Deriv_insert_eps[simp]: |
|
74 "Deriv a (insert [] A) = Deriv a A" |
|
75 by (auto simp: Deriv_def) |
|
76 *) |
|
77 |
|
78 |
65 |
79 |
66 subsection {* Brozowsky's derivatives of regular expressions *} |
80 subsection {* Brozowsky's derivatives of regular expressions *} |
67 |
81 |
68 fun |
82 fun |
69 nullable :: "'a rexp \<Rightarrow> bool" |
83 nullable :: "'a rexp \<Rightarrow> bool" |
74 | "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
88 | "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
75 | "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
89 | "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
76 | "nullable (Star r) = True" |
90 | "nullable (Star r) = True" |
77 |
91 |
78 fun |
92 fun |
79 der :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
93 deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
80 where |
94 where |
81 "der c (Zero) = Zero" |
95 "deriv c (Zero) = Zero" |
82 | "der c (One) = Zero" |
96 | "deriv c (One) = Zero" |
83 | "der c (Atom c') = (if c = c' then One else Zero)" |
97 | "deriv c (Atom c') = (if c = c' then One else Zero)" |
84 | "der c (Plus r1 r2) = Plus (der c r1) (der c r2)" |
98 | "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)" |
85 | "der c (Times r1 r2) = |
99 | "deriv c (Times r1 r2) = |
86 (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)" |
100 (if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)" |
87 | "der c (Star r) = Times (der c r) (Star r)" |
101 | "deriv c (Star r) = Times (deriv c r) (Star r)" |
88 |
102 |
89 fun |
103 fun |
90 ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
104 derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
91 where |
105 where |
92 "ders [] r = r" |
106 "derivs [] r = r" |
93 | "ders (c # s) r = ders s (der c r)" |
107 | "derivs (c # s) r = derivs s (deriv c r)" |
94 |
108 |
95 |
109 |
96 lemma Delta_nullable: |
110 lemma nullable_iff: |
97 shows "Delta (lang r) = (if nullable r then {[]} else {})" |
111 shows "nullable r \<longleftrightarrow> [] \<in> lang r" |
98 unfolding Delta_def |
|
99 by (induct r) (auto simp add: conc_def split: if_splits) |
112 by (induct r) (auto simp add: conc_def split: if_splits) |
100 |
113 |
101 lemma Der_der: |
114 lemma Deriv_deriv: |
102 shows "Der c (lang r) = lang (der c r)" |
115 shows "Deriv c (lang r) = lang (deriv c r)" |
103 by (induct r) (simp_all add: Delta_nullable) |
116 by (induct r) (simp_all add: nullable_iff) |
104 |
117 |
105 lemma Ders_ders: |
118 lemma Derivs_derivs: |
106 shows "Ders s (lang r) = lang (ders s r)" |
119 shows "Derivs s (lang r) = lang (derivs s r)" |
107 by (induct s arbitrary: r) (simp_all add: Der_der) |
120 by (induct s arbitrary: r) (simp_all add: Deriv_deriv) |
108 |
121 |
109 |
122 |
110 subsection {* Antimirov's Partial Derivatives *} |
123 subsection {* Antimirov's partial derivivatives *} |
111 |
124 |
112 abbreviation |
125 abbreviation |
113 "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
126 "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
114 |
127 |
115 fun |
128 fun |
116 pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
129 pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set" |
117 where |
130 where |
118 "pder c Zero = {}" |
131 "pderiv c Zero = {}" |
119 | "pder c One = {}" |
132 | "pderiv c One = {}" |
120 | "pder c (Atom c') = (if c = c' then {One} else {})" |
133 | "pderiv c (Atom c') = (if c = c' then {One} else {})" |
121 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)" |
134 | "pderiv c (Plus r1 r2) = (pderiv c r1) \<union> (pderiv c r2)" |
122 | "pder c (Times r1 r2) = |
135 | "pderiv c (Times r1 r2) = |
123 (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)" |
136 (if nullable r1 then Timess (pderiv c r1) r2 \<union> pderiv c r2 else Timess (pderiv c r1) r2)" |
124 | "pder c (Star r) = Timess (pder c r) (Star r)" |
137 | "pderiv c (Star r) = Timess (pderiv c r) (Star r)" |
|
138 |
|
139 fun |
|
140 pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
|
141 where |
|
142 "pderivs [] r = {r}" |
|
143 | "pderivs (c # s) r = \<Union> (pderivs s) ` (pderiv c r)" |
125 |
144 |
126 abbreviation |
145 abbreviation |
127 "pder_set c rs \<equiv> \<Union> pder c ` rs" |
146 pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set" |
128 |
147 where |
129 fun |
148 "pderiv_set c rs \<equiv> \<Union> pderiv c ` rs" |
130 pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
|
131 where |
|
132 "pders [] r = {r}" |
|
133 | "pders (c # s) r = \<Union> (pders s) ` (pder c r)" |
|
134 |
149 |
135 abbreviation |
150 abbreviation |
136 "pderss s A \<equiv> \<Union> (pders s) ` A" |
151 pderivs_set :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set" |
137 |
152 where |
138 lemma pders_append: |
153 "pderivs_set s rs \<equiv> \<Union> (pderivs s) ` rs" |
139 "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)" |
154 |
|
155 lemma pderivs_append: |
|
156 "pderivs (s1 @ s2) r = \<Union> (pderivs s2) ` (pderivs s1 r)" |
140 by (induct s1 arbitrary: r) (simp_all) |
157 by (induct s1 arbitrary: r) (simp_all) |
141 |
158 |
142 lemma pders_snoc: |
159 lemma pderivs_snoc: |
143 shows "pders (s @ [c]) r = pder_set c (pders s r)" |
160 shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)" |
144 by (simp add: pders_append) |
161 by (simp add: pderivs_append) |
145 |
162 |
146 lemma pders_simps [simp]: |
163 lemma pderivs_simps [simp]: |
147 shows "pders s Zero = (if s= [] then {Zero} else {})" |
164 shows "pderivs s Zero = (if s = [] then {Zero} else {})" |
148 and "pders s One = (if s = [] then {One} else {})" |
165 and "pderivs s One = (if s = [] then {One} else {})" |
149 and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))" |
166 and "pderivs s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pderivs s r1) \<union> (pderivs s r2))" |
150 by (induct s) (simp_all) |
167 by (induct s) (simp_all) |
151 |
168 |
152 lemma pders_Atom [intro]: |
169 lemma pderivs_Atom: |
153 shows "pders s (Atom c) \<subseteq> {Atom c, One}" |
170 shows "pderivs s (Atom c) \<subseteq> {Atom c, One}" |
154 by (induct s) (simp_all) |
171 by (induct s) (simp_all) |
155 |
172 |
156 subsection {* Relating left-quotients and partial derivatives *} |
173 subsection {* Relating left-quotients and partial derivivatives *} |
157 |
174 |
158 lemma Der_pder: |
175 lemma Deriv_pderiv: |
159 shows "Der c (lang r) = \<Union> lang ` (pder c r)" |
176 shows "Deriv c (lang r) = \<Union> lang ` (pderiv c r)" |
160 by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib) |
177 by (induct r) (auto simp add: nullable_iff conc_UNION_distrib) |
161 |
178 |
162 lemma Ders_pders: |
179 lemma Derivs_pderivs: |
163 shows "Ders s (lang r) = \<Union> lang ` (pders s r)" |
180 shows "Derivs s (lang r) = \<Union> lang ` (pderivs s r)" |
164 proof (induct s arbitrary: r) |
181 proof (induct s arbitrary: r) |
165 case (Cons c s) |
182 case (Cons c s) |
166 have ih: "\<And>r. Ders s (lang r) = \<Union> lang ` (pders s r)" by fact |
183 have ih: "\<And>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)" by fact |
167 have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp |
184 have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp |
168 also have "\<dots> = Ders s (\<Union> lang ` (pder c r))" by (simp add: Der_pder) |
185 also have "\<dots> = Derivs s (\<Union> lang ` (pderiv c r))" by (simp add: Deriv_pderiv) |
169 also have "\<dots> = Derss s (lang ` (pder c r))" |
186 also have "\<dots> = Derivss s (lang ` (pderiv c r))" |
170 by (auto simp add: Ders_def) |
187 by (auto simp add: Derivs_def) |
171 also have "\<dots> = \<Union> lang ` (pderss s (pder c r))" |
188 also have "\<dots> = \<Union> lang ` (pderivs_set s (pderiv c r))" |
172 using ih by auto |
189 using ih by auto |
173 also have "\<dots> = \<Union> lang ` (pders (c # s) r)" by simp |
190 also have "\<dots> = \<Union> lang ` (pderivs (c # s) r)" by simp |
174 finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" . |
191 finally show "Derivs (c # s) (lang r) = \<Union> lang ` pderivs (c # s) r" . |
175 qed (simp add: Ders_def) |
192 qed (simp add: Derivs_def) |
176 |
193 |
177 subsection {* Relating derivatives and partial derivatives *} |
194 subsection {* Relating derivivatives and partial derivivatives *} |
178 |
195 |
179 lemma der_pder: |
196 lemma deriv_pderiv: |
180 shows "(\<Union> lang ` (pder c r)) = lang (der c r)" |
197 shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)" |
181 unfolding Der_der[symmetric] Der_pder by simp |
198 unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp |
182 |
199 |
183 lemma ders_pders: |
200 lemma derivs_pderivs: |
184 shows "(\<Union> lang ` (pders s r)) = lang (ders s r)" |
201 shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)" |
185 unfolding Ders_ders[symmetric] Ders_pders by simp |
202 unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp |
186 |
203 |
187 |
204 |
188 subsection {* There are only finitely many partial derivatives for a language *} |
205 subsection {* Finiteness property of partial derivivatives *} |
189 |
206 |
190 definition |
207 definition |
191 "pders_lang A r \<equiv> \<Union>x \<in> A. pders x r" |
208 pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set" |
192 |
209 where |
193 lemma pders_lang_subsetI [intro]: |
210 "pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r" |
194 assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C" |
211 |
195 shows "pders_lang A r \<subseteq> C" |
212 lemma pderivs_lang_subsetI: |
196 using assms unfolding pders_lang_def by (rule UN_least) |
213 assumes "\<And>s. s \<in> A \<Longrightarrow> pderivs s r \<subseteq> C" |
197 |
214 shows "pderivs_lang A r \<subseteq> C" |
198 lemma pders_lang_union: |
215 using assms unfolding pderivs_lang_def by (rule UN_least) |
199 shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)" |
216 |
200 by (simp add: pders_lang_def) |
217 lemma pderivs_lang_union: |
201 |
218 shows "pderivs_lang (A \<union> B) r = (pderivs_lang A r \<union> pderivs_lang B r)" |
202 lemma pders_lang_subset: |
219 by (simp add: pderivs_lang_def) |
203 shows "A \<subseteq> B \<Longrightarrow> pders_lang A r \<subseteq> pders_lang B r" |
220 |
204 by (auto simp add: pders_lang_def) |
221 lemma pderivs_lang_subset: |
|
222 shows "A \<subseteq> B \<Longrightarrow> pderivs_lang A r \<subseteq> pderivs_lang B r" |
|
223 by (auto simp add: pderivs_lang_def) |
205 |
224 |
206 definition |
225 definition |
207 "UNIV1 \<equiv> UNIV - {[]}" |
226 "UNIV1 \<equiv> UNIV - {[]}" |
208 |
227 |
209 lemma pders_lang_Zero [simp]: |
228 lemma pderivs_lang_Zero [simp]: |
210 shows "pders_lang UNIV1 Zero = {}" |
229 shows "pderivs_lang UNIV1 Zero = {}" |
211 unfolding UNIV1_def pders_lang_def by auto |
230 unfolding UNIV1_def pderivs_lang_def by auto |
212 |
231 |
213 lemma pders_lang_One [simp]: |
232 lemma pderivs_lang_One [simp]: |
214 shows "pders_lang UNIV1 One = {}" |
233 shows "pderivs_lang UNIV1 One = {}" |
215 unfolding UNIV1_def pders_lang_def by (auto split: if_splits) |
234 unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits) |
216 |
235 |
217 lemma pders_lang_Atom [simp]: |
236 lemma pderivs_lang_Atom [simp]: |
218 shows "pders_lang UNIV1 (Atom c) = {One}" |
237 shows "pderivs_lang UNIV1 (Atom c) = {One}" |
219 unfolding UNIV1_def pders_lang_def |
238 unfolding UNIV1_def pderivs_lang_def |
220 apply(auto) |
239 apply(auto) |
221 apply(frule rev_subsetD) |
240 apply(frule rev_subsetD) |
222 apply(rule pders_Atom) |
241 apply(rule pderivs_Atom) |
223 apply(simp) |
242 apply(simp) |
224 apply(case_tac xa) |
243 apply(case_tac xa) |
225 apply(auto split: if_splits) |
244 apply(auto split: if_splits) |
226 done |
245 done |
227 |
246 |
228 lemma pders_lang_Plus [simp]: |
247 lemma pderivs_lang_Plus [simp]: |
229 shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2" |
248 shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2" |
230 unfolding UNIV1_def pders_lang_def by auto |
249 unfolding UNIV1_def pderivs_lang_def by auto |
231 |
250 |
232 |
251 |
233 text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *} |
252 text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *} |
234 |
253 |
235 definition |
254 definition |
236 "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
255 "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
237 |
256 |
238 lemma Suf_snoc: |
257 lemma PSuf_snoc: |
239 shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}" |
258 shows "PSuf (s @ [c]) = (PSuf s) @@ {[c]} \<union> {[c]}" |
240 unfolding Suf_def conc_def |
259 unfolding PSuf_def conc_def |
241 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) |
260 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) |
242 |
261 |
243 lemma Suf_Union: |
262 lemma PSuf_Union: |
244 shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))" |
263 shows "(\<Union>v \<in> PSuf s @@ {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))" |
245 by (auto simp add: conc_def) |
264 by (auto simp add: conc_def) |
246 |
265 |
247 lemma pders_lang_snoc: |
266 lemma pderivs_lang_snoc: |
248 shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))" |
267 shows "pderivs_lang (PSuf s @@ {[c]}) r = (pderiv_set c (pderivs_lang (PSuf s) r))" |
249 unfolding pders_lang_def |
268 unfolding pderivs_lang_def |
250 by (simp add: Suf_Union pders_snoc) |
269 by (simp add: PSuf_Union pderivs_snoc) |
251 |
270 |
252 lemma pders_Times: |
271 lemma pderivs_Times: |
253 shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)" |
272 shows "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)" |
254 proof (induct s rule: rev_induct) |
273 proof (induct s rule: rev_induct) |
255 case (snoc c s) |
274 case (snoc c s) |
256 have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)" |
275 have ih: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)" |
257 by fact |
276 by fact |
258 have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" |
277 have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))" |
259 by (simp add: pders_snoc) |
278 by (simp add: pderivs_snoc) |
260 also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2))" |
279 also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2))" |
261 using ih by (auto) (blast) |
280 using ih by (auto) (blast) |
262 also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_lang (Suf s) r2)" |
281 also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)" |
263 by (simp) |
282 by (simp) |
264 also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_lang (Suf s \<cdot> {[c]}) r2" |
283 also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderivs_lang (PSuf s @@ {[c]}) r2" |
265 by (simp add: pders_lang_snoc) |
284 by (simp add: pderivs_lang_snoc) |
266 also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2" |
285 also |
|
286 have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2" |
267 by auto |
287 by auto |
268 also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2" |
288 also |
|
289 have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs s r1)) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2" |
269 by (auto simp add: if_splits) (blast) |
290 by (auto simp add: if_splits) (blast) |
270 also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2" |
291 also have "\<dots> = Timess (pderivs (s @ [c]) r1) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2" |
271 by (simp add: pders_snoc) |
292 by (simp add: pderivs_snoc) |
272 also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2" |
293 also have "\<dots> \<subseteq> Timess (pderivs (s @ [c]) r1) r2 \<union> pderivs_lang (PSuf (s @ [c])) r2" |
273 unfolding pders_lang_def by (auto simp add: Suf_snoc) |
294 unfolding pderivs_lang_def by (auto simp add: PSuf_snoc) |
274 finally show ?case . |
295 finally show ?case . |
275 qed (simp) |
296 qed (simp) |
276 |
297 |
277 lemma pders_lang_Times_aux1: |
298 lemma pderivs_lang_Times_aux1: |
278 assumes a: "s \<in> UNIV1" |
299 assumes a: "s \<in> UNIV1" |
279 shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r" |
300 shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r" |
280 using a unfolding UNIV1_def Suf_def pders_lang_def by auto |
301 using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto |
281 |
302 |
282 lemma pders_lang_Times_aux2: |
303 lemma pderivs_lang_Times_aux2: |
283 assumes a: "s \<in> UNIV1" |
304 assumes a: "s \<in> UNIV1" |
284 shows "Timess (pders s r1) r2 \<subseteq> Timess (pders_lang UNIV1 r1) r2" |
305 shows "Timess (pderivs s r1) r2 \<subseteq> Timess (pderivs_lang UNIV1 r1) r2" |
285 using a unfolding pders_lang_def by auto |
306 using a unfolding pderivs_lang_def by auto |
286 |
307 |
287 lemma pders_lang_Times [intro]: |
308 lemma pderivs_lang_Times: |
288 shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2" |
309 shows "pderivs_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2" |
289 apply(rule pders_lang_subsetI) |
310 apply(rule pderivs_lang_subsetI) |
290 apply(rule subset_trans) |
311 apply(rule subset_trans) |
291 apply(rule pders_Times) |
312 apply(rule pderivs_Times) |
292 using pders_lang_Times_aux1 pders_lang_Times_aux2 |
313 using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2 |
293 apply(blast) |
314 apply(blast) |
294 done |
315 done |
295 |
316 |
296 lemma pders_Star: |
317 lemma pderivs_Star: |
297 assumes a: "s \<noteq> []" |
318 assumes a: "s \<noteq> []" |
298 shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)" |
319 shows "pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" |
299 using a |
320 using a |
300 proof (induct s rule: rev_induct) |
321 proof (induct s rule: rev_induct) |
301 case (snoc c s) |
322 case (snoc c s) |
302 have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)" by fact |
323 have ih: "s \<noteq> [] \<Longrightarrow> pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" by fact |
303 { assume asm: "s \<noteq> []" |
324 { assume asm: "s \<noteq> []" |
304 have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc) |
325 have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc) |
305 also have "\<dots> \<subseteq> pder_set c (Timess (pders_lang (Suf s) r) (Star r))" |
326 also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))" |
306 using ih[OF asm] by (auto) (blast) |
327 using ih[OF asm] by (auto) (blast) |
307 also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)" |
328 also have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \<union> pderiv c (Star r)" |
308 by (auto split: if_splits) (blast)+ |
329 by (auto split: if_splits) (blast)+ |
309 also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))" |
330 also have "\<dots> \<subseteq> Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \<union> (Timess (pderiv c r) (Star r))" |
310 by (simp only: Suf_snoc pders_lang_snoc pders_lang_union) |
331 by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union) |
311 (auto simp add: pders_lang_def) |
332 (auto simp add: pderivs_lang_def) |
312 also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)" |
333 also have "\<dots> = Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r)" |
313 by (auto simp add: Suf_snoc Suf_Union pders_snoc pders_lang_def) |
334 by (auto simp add: PSuf_snoc PSuf_Union pderivs_snoc pderivs_lang_def) |
314 finally have ?case . |
335 finally have ?case . |
315 } |
336 } |
316 moreover |
337 moreover |
317 { assume asm: "s = []" |
338 { assume asm: "s = []" |
318 then have ?case |
339 then have ?case |
319 apply (auto simp add: pders_lang_def pders_snoc Suf_def) |
340 apply (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def) |
320 apply(rule_tac x = "[c]" in exI) |
341 apply(rule_tac x = "[c]" in exI) |
321 apply(auto) |
342 apply(auto) |
322 done |
343 done |
323 } |
344 } |
324 ultimately show ?case by blast |
345 ultimately show ?case by blast |
325 qed (simp) |
346 qed (simp) |
326 |
347 |
327 lemma pders_lang_Star [intro]: |
348 lemma pderivs_lang_Star: |
328 shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)" |
349 shows "pderivs_lang UNIV1 (Star r) \<subseteq> Timess (pderivs_lang UNIV1 r) (Star r)" |
329 apply(rule pders_lang_subsetI) |
350 apply(rule pderivs_lang_subsetI) |
330 apply(rule subset_trans) |
351 apply(rule subset_trans) |
331 apply(rule pders_Star) |
352 apply(rule pderivs_Star) |
332 apply(simp add: UNIV1_def) |
353 apply(simp add: UNIV1_def) |
333 apply(simp add: UNIV1_def Suf_def) |
354 apply(simp add: UNIV1_def PSuf_def) |
334 apply(auto simp add: pders_lang_def) |
355 apply(auto simp add: pderivs_lang_def) |
335 done |
356 done |
336 |
357 |
337 lemma finite_Timess [simp]: |
358 lemma finite_Timess [simp]: |
338 assumes a: "finite A" |
359 assumes a: "finite A" |
339 shows "finite (Timess A r)" |
360 shows "finite (Timess A r)" |
340 using a by auto |
361 using a by auto |
341 |
362 |
342 lemma finite_pders_lang_UNIV1: |
363 lemma finite_pderivs_lang_UNIV1: |
343 shows "finite (pders_lang UNIV1 r)" |
364 shows "finite (pderivs_lang UNIV1 r)" |
344 apply(induct r) |
365 apply(induct r) |
345 apply(simp_all add: |
366 apply(simp_all add: |
346 finite_subset[OF pders_lang_Times] |
367 finite_subset[OF pderivs_lang_Times] |
347 finite_subset[OF pders_lang_Star]) |
368 finite_subset[OF pderivs_lang_Star]) |
348 done |
369 done |
349 |
370 |
350 lemma pders_lang_UNIV: |
371 lemma pderivs_lang_UNIV: |
351 shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r" |
372 shows "pderivs_lang UNIV r = pderivs [] r \<union> pderivs_lang UNIV1 r" |
352 unfolding UNIV1_def pders_lang_def |
373 unfolding UNIV1_def pderivs_lang_def |
353 by blast |
374 by blast |
354 |
375 |
355 lemma finite_pders_lang_UNIV: |
376 lemma finite_pderivs_lang_UNIV: |
356 shows "finite (pders_lang UNIV r)" |
377 shows "finite (pderivs_lang UNIV r)" |
357 unfolding pders_lang_UNIV |
378 unfolding pderivs_lang_UNIV |
358 by (simp add: finite_pders_lang_UNIV1) |
379 by (simp add: finite_pderivs_lang_UNIV1) |
359 |
380 |
360 lemma finite_pders_lang: |
381 lemma finite_pderivs_lang: |
361 shows "finite (pders_lang A r)" |
382 shows "finite (pderivs_lang A r)" |
362 apply(rule rev_finite_subset[OF finite_pders_lang_UNIV]) |
383 by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV) |
363 apply(rule pders_lang_subset) |
|
364 apply(simp) |
|
365 done |
|
366 |
|
367 text {* Relating the Myhill-Nerode relation with left-quotients. *} |
|
368 |
|
369 lemma MN_Rel_Ders: |
|
370 shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A" |
|
371 unfolding Ders_def str_eq_def |
|
372 by auto |
|
373 |
|
374 subsection {* |
|
375 The second direction of the Myhill-Nerode theorem using |
|
376 partial derivatives. |
|
377 *} |
|
378 |
|
379 lemma Myhill_Nerode3: |
|
380 fixes r::"'a rexp" |
|
381 shows "finite (UNIV // \<approx>(lang r))" |
|
382 proof - |
|
383 have "finite (UNIV // =(\<lambda>x. pders x r)=)" |
|
384 proof - |
|
385 have "range (\<lambda>x. pders x r) \<subseteq> Pow (pders_lang UNIV r)" |
|
386 unfolding pders_lang_def by auto |
|
387 moreover |
|
388 have "finite (Pow (pders_lang UNIV r))" by (simp add: finite_pders_lang) |
|
389 ultimately |
|
390 have "finite (range (\<lambda>x. pders x r))" |
|
391 by (simp add: finite_subset) |
|
392 then show "finite (UNIV // =(\<lambda>x. pders x r)=)" |
|
393 by (rule finite_eq_tag_rel) |
|
394 qed |
|
395 moreover |
|
396 have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)" |
|
397 unfolding tag_eq_def |
|
398 by (auto simp add: MN_Rel_Ders Ders_pders) |
|
399 moreover |
|
400 have "equiv UNIV =(\<lambda>x. pders x r)=" |
|
401 and "equiv UNIV (\<approx>(lang r))" |
|
402 unfolding equiv_def refl_on_def sym_def trans_def |
|
403 unfolding tag_eq_def str_eq_def |
|
404 by auto |
|
405 ultimately show "finite (UNIV // \<approx>(lang r))" |
|
406 by (rule refined_partition_finite) |
|
407 qed |
|
408 |
384 |
409 |
385 |
410 end |
386 end |