equal
deleted
inserted
replaced
1 theory Exercises |
1 theory Exercises |
2 imports Lexer "~~/src/HOL/Library/Infinite_Set" |
2 imports Lexer "~~/src/HOL/Library/Infinite_Set" |
3 begin |
3 begin |
4 |
4 |
5 section {* some fun tests *} |
5 section {* Some Fun Facts *} |
6 |
6 |
7 fun |
7 fun |
8 zeroable :: "rexp \<Rightarrow> bool" |
8 zeroable :: "rexp \<Rightarrow> bool" |
9 where |
9 where |
10 "zeroable (ZERO) \<longleftrightarrow> True" |
10 "zeroable (ZERO) \<longleftrightarrow> True" |
14 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2" |
14 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2" |
15 | "zeroable (STAR r) \<longleftrightarrow> False" |
15 | "zeroable (STAR r) \<longleftrightarrow> False" |
16 |
16 |
17 lemma zeroable_correctness: |
17 lemma zeroable_correctness: |
18 shows "zeroable r \<longleftrightarrow> L r = {}" |
18 shows "zeroable r \<longleftrightarrow> L r = {}" |
19 apply(induct r rule: zeroable.induct) |
19 by(induct r)(auto simp add: Sequ_def) |
20 apply(auto simp add: Sequ_def) |
20 |
21 done |
|
22 |
21 |
23 fun |
22 fun |
24 atmostempty :: "rexp \<Rightarrow> bool" |
23 atmostempty :: "rexp \<Rightarrow> bool" |
25 where |
24 where |
26 "atmostempty (ZERO) \<longleftrightarrow> True" |
25 "atmostempty (ZERO) \<longleftrightarrow> True" |
43 (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)" |
42 (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)" |
44 | "somechars (STAR r) \<longleftrightarrow> somechars r" |
43 | "somechars (STAR r) \<longleftrightarrow> somechars r" |
45 |
44 |
46 lemma somechars_correctness: |
45 lemma somechars_correctness: |
47 shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)" |
46 shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)" |
48 apply(induct r rule: somechars.induct) |
47 apply(induct r) |
49 apply(simp) |
48 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) |
50 apply(simp) |
49 using Nil_is_append_conv apply blast |
51 apply(simp) |
50 apply blast |
52 apply(auto)[1] |
51 apply(auto) |
53 prefer 2 |
52 using Star_string by fastforce |
54 apply(simp) |
53 |
55 apply(rule iffI) |
|
56 apply(auto)[1] |
|
57 apply (metis Star_decomp neq_Nil_conv) |
|
58 apply(rule iffI) |
|
59 apply(simp add: Sequ_def zeroable_correctness nullable_correctness) |
|
60 apply(auto)[1] |
|
61 apply(simp add: Sequ_def zeroable_correctness nullable_correctness) |
|
62 apply(auto)[1] |
|
63 done |
|
64 |
54 |
65 lemma atmostempty_correctness_aux: |
55 lemma atmostempty_correctness_aux: |
66 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
56 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
67 apply(induct r) |
57 apply(induct r) |
68 apply(simp_all) |
58 apply(simp_all) |
210 apply(rule iffI) |
200 apply(rule iffI) |
211 apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD) |
201 apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD) |
212 using Star_non_empty_string_infinite apply blast |
202 using Star_non_empty_string_infinite apply blast |
213 done |
203 done |
214 |
204 |
|
205 unused_thms |
215 |
206 |
216 end |
207 end |