equal
deleted
inserted
replaced
81 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
81 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
82 |
82 |
83 lemma Pow_empty [simp]: |
83 lemma Pow_empty [simp]: |
84 shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)" |
84 shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)" |
85 by(induct n) (auto simp add: Sequ_def) |
85 by(induct n) (auto simp add: Sequ_def) |
86 |
|
87 lemma Pow_plus: |
|
88 "A \<up> (n + m) = A \<up> n ;; A \<up> m" |
|
89 by (induct n) (simp_all add: seq_assoc) |
|
90 |
|
91 |
86 |
92 section {* Kleene Star for Languages *} |
87 section {* Kleene Star for Languages *} |
93 |
88 |
94 inductive_set |
89 inductive_set |
95 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
90 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
221 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
216 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
222 apply(induct r) |
217 apply(induct r) |
223 apply(auto simp add: Sequ_def) |
218 apply(auto simp add: Sequ_def) |
224 done |
219 done |
225 |
220 |
226 lemma Suc_reduce_Union: |
|
227 "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))" |
|
228 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) |
|
229 |
221 |
230 lemma Suc_reduce_Union2: |
222 lemma Suc_reduce_Union2: |
231 "(\<Union>x\<in>{Suc n..}. B x) = (\<Union>x\<in>{n..}. B (Suc x))" |
223 "(\<Union>x\<in>{Suc n..}. B x) = (\<Union>x\<in>{n..}. B (Suc x))" |
232 apply(auto) |
224 apply(auto) |
233 apply(rule_tac x="xa - 1" in bexI) |
225 apply(rule_tac x="xa - 1" in bexI) |
235 apply(simp) |
227 apply(simp) |
236 done |
228 done |
237 |
229 |
238 lemma Seq_UNION: |
230 lemma Seq_UNION: |
239 shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)" |
231 shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)" |
240 by (auto simp add: Sequ_def) |
|
241 |
|
242 lemma Seq_Union: |
|
243 shows "A ;; (\<Union>x\<in>B. C x) = (\<Union>x\<in>B. A ;; C x)" |
|
244 by (auto simp add: Sequ_def) |
232 by (auto simp add: Sequ_def) |
245 |
233 |
246 lemma Der_Pow [simp]: |
234 lemma Der_Pow [simp]: |
247 shows "Der c (A \<up> (Suc n)) = |
235 shows "Der c (A \<up> (Suc n)) = |
248 (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})" |
236 (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})" |
279 apply(case_tac "[] \<in> L r") |
267 apply(case_tac "[] \<in> L r") |
280 apply(simp) |
268 apply(simp) |
281 apply(simp) |
269 apply(simp) |
282 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem) |
270 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem) |
283 |
271 |
284 lemma Der_Pow_in: |
272 |
285 assumes "[] \<in> A" |
|
286 shows "Der c (A \<up> n) = (\<Union>x\<le>n. Der c (A \<up> x))" |
|
287 using assms |
|
288 apply(induct n) |
|
289 apply(simp) |
|
290 apply(simp add: Suc_Union) |
|
291 done |
|
292 |
273 |
293 lemma Der_Pow_notin: |
274 lemma Der_Pow_notin: |
294 assumes "[] \<notin> A" |
275 assumes "[] \<notin> A" |
295 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" |
276 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" |
296 using assms |
277 using assms |
1275 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
1256 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
1276 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
1257 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
1277 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
1258 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
1278 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
1259 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
1279 |
1260 |
1280 |
1261 unused_thms |
1281 end |
1262 end |