|
1 theory Exercises |
|
2 imports Lexer "~~/src/HOL/Library/Infinite_Set" |
|
3 begin |
|
4 |
|
5 section {* some fun tests *} |
|
6 |
|
7 fun |
|
8 zeroable :: "rexp \<Rightarrow> bool" |
|
9 where |
|
10 "zeroable (ZERO) \<longleftrightarrow> True" |
|
11 | "zeroable (ONE) \<longleftrightarrow> False" |
|
12 | "zeroable (CHAR c) \<longleftrightarrow> False" |
|
13 | "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2" |
|
14 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2" |
|
15 | "zeroable (STAR r) \<longleftrightarrow> False" |
|
16 |
|
17 lemma zeroable_correctness: |
|
18 shows "zeroable r \<longleftrightarrow> L r = {}" |
|
19 apply(induct r rule: zeroable.induct) |
|
20 apply(auto simp add: Sequ_def) |
|
21 done |
|
22 |
|
23 fun |
|
24 atmostempty :: "rexp \<Rightarrow> bool" |
|
25 where |
|
26 "atmostempty (ZERO) \<longleftrightarrow> True" |
|
27 | "atmostempty (ONE) \<longleftrightarrow> True" |
|
28 | "atmostempty (CHAR c) \<longleftrightarrow> False" |
|
29 | "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2" |
|
30 | "atmostempty (SEQ r1 r2) \<longleftrightarrow> |
|
31 zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)" |
|
32 | "atmostempty (STAR r) = atmostempty r" |
|
33 |
|
34 fun |
|
35 somechars :: "rexp \<Rightarrow> bool" |
|
36 where |
|
37 "somechars (ZERO) \<longleftrightarrow> False" |
|
38 | "somechars (ONE) \<longleftrightarrow> False" |
|
39 | "somechars (CHAR c) \<longleftrightarrow> True" |
|
40 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2" |
|
41 | "somechars (SEQ r1 r2) \<longleftrightarrow> |
|
42 (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> |
|
43 (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)" |
|
44 | "somechars (STAR r) \<longleftrightarrow> somechars r" |
|
45 |
|
46 lemma somechars_correctness: |
|
47 shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)" |
|
48 apply(induct r rule: somechars.induct) |
|
49 apply(simp) |
|
50 apply(simp) |
|
51 apply(simp) |
|
52 apply(auto)[1] |
|
53 prefer 2 |
|
54 apply(simp) |
|
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 |
|
65 lemma atmostempty_correctness_aux: |
|
66 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
|
67 apply(induct r) |
|
68 apply(simp_all) |
|
69 apply(auto simp add: zeroable_correctness nullable_correctness somechars_correctness) |
|
70 done |
|
71 |
|
72 lemma atmostempty_correctness: |
|
73 shows "atmostempty r \<longleftrightarrow> L r \<subseteq> {[]}" |
|
74 by(auto simp add: atmostempty_correctness_aux somechars_correctness) |
|
75 |
|
76 fun |
|
77 infinitestrings :: "rexp \<Rightarrow> bool" |
|
78 where |
|
79 "infinitestrings (ZERO) = False" |
|
80 | "infinitestrings (ONE) = False" |
|
81 | "infinitestrings (CHAR c) = False" |
|
82 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)" |
|
83 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> |
|
84 (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)" |
|
85 | "infinitestrings (STAR r) = (\<not> atmostempty r)" |
|
86 |
|
87 lemma Star_atmostempty: |
|
88 assumes "A \<subseteq> {[]}" |
|
89 shows "A\<star> \<subseteq> {[]}" |
|
90 using assms |
|
91 using Star_string concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce |
|
92 |
|
93 lemma Star_empty_string_finite: |
|
94 shows "finite ({[]}\<star>)" |
|
95 using Star_atmostempty infinite_super by auto |
|
96 |
|
97 lemma Star_empty_finite: |
|
98 shows "finite ({}\<star>)" |
|
99 using Star_atmostempty infinite_super by auto |
|
100 |
|
101 lemma Star_concat_replicate: |
|
102 assumes "s \<in> A" |
|
103 shows "concat (replicate n s) \<in> A\<star>" |
|
104 using assms |
|
105 by (induct n) (auto) |
|
106 |
|
107 |
|
108 lemma concat_replicate_inj: |
|
109 assumes "concat (replicate n s) = concat (replicate m s)" "s \<noteq> []" |
|
110 shows "n = m" |
|
111 using assms |
|
112 apply(induct n arbitrary: m) |
|
113 apply(auto)[1] |
|
114 apply(auto) |
|
115 apply(case_tac m) |
|
116 apply(clarify) |
|
117 apply(simp only: replicate.simps concat.simps) |
|
118 apply blast |
|
119 by simp |
|
120 |
|
121 lemma A0: |
|
122 assumes "finite (A ;; B)" "B \<noteq> {}" |
|
123 shows "finite A" |
|
124 apply(subgoal_tac "\<exists>s. s \<in> B") |
|
125 apply(erule exE) |
|
126 apply(subgoal_tac "finite {s1 @ s |s1. s1 \<in> A}") |
|
127 apply(rule_tac f="\<lambda>s1. s1 @ s" in finite_imageD) |
|
128 apply(simp add: image_def) |
|
129 apply(smt Collect_cong) |
|
130 apply(simp add: inj_on_def) |
|
131 apply(rule_tac B="A ;; B" in finite_subset) |
|
132 apply(auto simp add: Sequ_def)[1] |
|
133 apply(rule assms(1)) |
|
134 using assms(2) by auto |
|
135 |
|
136 lemma A1: |
|
137 assumes "finite (A ;; B)" "A \<noteq> {}" |
|
138 shows "finite B" |
|
139 apply(subgoal_tac "\<exists>s. s \<in> A") |
|
140 apply(erule exE) |
|
141 apply(subgoal_tac "finite {s @ s1 |s1. s1 \<in> B}") |
|
142 apply(rule_tac f="\<lambda>s1. s @ s1" in finite_imageD) |
|
143 apply(simp add: image_def) |
|
144 apply(smt Collect_cong) |
|
145 apply(simp add: inj_on_def) |
|
146 apply(rule_tac B="A ;; B" in finite_subset) |
|
147 apply(auto simp add: Sequ_def)[1] |
|
148 apply(rule assms(1)) |
|
149 using assms(2) by auto |
|
150 |
|
151 lemma Sequ_Prod_finite: |
|
152 assumes "A \<noteq> {}" "B \<noteq> {}" |
|
153 shows "finite (A ;; B) \<longleftrightarrow> (finite (A \<times> B))" |
|
154 apply(rule iffI) |
|
155 apply(rule finite_cartesian_product) |
|
156 apply(erule A0) |
|
157 apply(rule assms(2)) |
|
158 apply(erule A1) |
|
159 apply(rule assms(1)) |
|
160 apply(simp add: Sequ_def) |
|
161 apply(rule finite_image_set2) |
|
162 apply(drule finite_cartesian_productD1) |
|
163 apply(rule assms(2)) |
|
164 apply(simp) |
|
165 apply(drule finite_cartesian_productD2) |
|
166 apply(rule assms(1)) |
|
167 apply(simp) |
|
168 done |
|
169 |
|
170 |
|
171 lemma Star_non_empty_string_infinite: |
|
172 assumes "s \<in> A" " s \<noteq> []" |
|
173 shows "infinite (A\<star>)" |
|
174 proof - |
|
175 have "inj (\<lambda>n. concat (replicate n s))" |
|
176 using assms(2) concat_replicate_inj |
|
177 by(auto simp add: inj_on_def) |
|
178 moreover |
|
179 have "infinite (UNIV::nat set)" by simp |
|
180 ultimately |
|
181 have "infinite ((\<lambda>n. concat (replicate n s)) ` UNIV)" |
|
182 by (simp add: range_inj_infinite) |
|
183 moreover |
|
184 have "((\<lambda>n. concat (replicate n s)) ` UNIV) \<subseteq> (A\<star>)" |
|
185 using Star_concat_replicate assms(1) by auto |
|
186 ultimately show "infinite (A\<star>)" |
|
187 using infinite_super by auto |
|
188 qed |
|
189 |
|
190 lemma infinitestrings_correctness: |
|
191 shows "infinitestrings r \<longleftrightarrow> infinite (L r)" |
|
192 apply(induct r) |
|
193 apply(simp_all) |
|
194 apply(simp add: zeroable_correctness) |
|
195 apply(rule iffI) |
|
196 apply(erule disjE) |
|
197 apply(subst Sequ_Prod_finite) |
|
198 apply(auto)[2] |
|
199 using finite_cartesian_productD2 apply blast |
|
200 apply(subst Sequ_Prod_finite) |
|
201 apply(auto)[2] |
|
202 using finite_cartesian_productD1 apply blast |
|
203 apply(subgoal_tac "L r1 \<noteq> {} \<and> L r2 \<noteq> {}") |
|
204 prefer 2 |
|
205 apply(auto simp add: Sequ_def)[1] |
|
206 apply(subst (asm) Sequ_Prod_finite) |
|
207 apply(auto)[2] |
|
208 apply(auto)[1] |
|
209 apply(simp add: atmostempty_correctness) |
|
210 apply(rule iffI) |
|
211 apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD) |
|
212 using Star_non_empty_string_infinite apply blast |
|
213 done |
|
214 |
|
215 |
|
216 end |