|
259
|
1 |
theory Exercises
|
|
258
|
2 |
imports Lexer "~~/src/HOL/Library/Infinite_Set"
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
section {* some fun tests *}
|
|
|
6 |
|
|
|
7 |
fun
|
|
259
|
8 |
zeroable :: "rexp \<Rightarrow> bool"
|
|
258
|
9 |
where
|
|
259
|
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"
|
|
258
|
16 |
|
|
|
17 |
lemma zeroable_correctness:
|
|
259
|
18 |
shows "zeroable r \<longleftrightarrow> L r = {}"
|
|
258
|
19 |
apply(induct r rule: zeroable.induct)
|
|
|
20 |
apply(auto simp add: Sequ_def)
|
|
|
21 |
done
|
|
|
22 |
|
|
|
23 |
fun
|
|
259
|
24 |
atmostempty :: "rexp \<Rightarrow> bool"
|
|
258
|
25 |
where
|
|
259
|
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)"
|
|
258
|
32 |
| "atmostempty (STAR r) = atmostempty r"
|
|
|
33 |
|
|
|
34 |
fun
|
|
259
|
35 |
somechars :: "rexp \<Rightarrow> bool"
|
|
258
|
36 |
where
|
|
259
|
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"
|
|
258
|
45 |
|
|
|
46 |
lemma somechars_correctness:
|
|
259
|
47 |
shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)"
|
|
258
|
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:
|
|
259
|
66 |
shows "atmostempty r \<longleftrightarrow> \<not> somechars r"
|
|
258
|
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:
|
|
259
|
73 |
shows "atmostempty r \<longleftrightarrow> L r \<subseteq> {[]}"
|
|
258
|
74 |
by(auto simp add: atmostempty_correctness_aux somechars_correctness)
|
|
|
75 |
|
|
|
76 |
fun
|
|
259
|
77 |
infinitestrings :: "rexp \<Rightarrow> bool"
|
|
258
|
78 |
where
|
|
|
79 |
"infinitestrings (ZERO) = False"
|
|
|
80 |
| "infinitestrings (ONE) = False"
|
|
|
81 |
| "infinitestrings (CHAR c) = False"
|
|
259
|
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)"
|
|
258
|
86 |
|
|
|
87 |
lemma Star_atmostempty:
|
|
259
|
88 |
assumes "A \<subseteq> {[]}"
|
|
|
89 |
shows "A\<star> \<subseteq> {[]}"
|
|
258
|
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:
|
|
259
|
94 |
shows "finite ({[]}\<star>)"
|
|
258
|
95 |
using Star_atmostempty infinite_super by auto
|
|
|
96 |
|
|
|
97 |
lemma Star_empty_finite:
|
|
259
|
98 |
shows "finite ({}\<star>)"
|
|
258
|
99 |
using Star_atmostempty infinite_super by auto
|
|
|
100 |
|
|
|
101 |
lemma Star_concat_replicate:
|
|
259
|
102 |
assumes "s \<in> A"
|
|
|
103 |
shows "concat (replicate n s) \<in> A\<star>"
|
|
258
|
104 |
using assms
|
|
|
105 |
by (induct n) (auto)
|
|
|
106 |
|
|
|
107 |
|
|
|
108 |
lemma concat_replicate_inj:
|
|
259
|
109 |
assumes "concat (replicate n s) = concat (replicate m s)" "s \<noteq> []"
|
|
258
|
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:
|
|
259
|
122 |
assumes "finite (A ;; B)" "B \<noteq> {}"
|
|
258
|
123 |
shows "finite A"
|
|
259
|
124 |
apply(subgoal_tac "\<exists>s. s \<in> B")
|
|
258
|
125 |
apply(erule exE)
|
|
259
|
126 |
apply(subgoal_tac "finite {s1 @ s |s1. s1 \<in> A}")
|
|
|
127 |
apply(rule_tac f="\<lambda>s1. s1 @ s" in finite_imageD)
|
|
258
|
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:
|
|
259
|
137 |
assumes "finite (A ;; B)" "A \<noteq> {}"
|
|
258
|
138 |
shows "finite B"
|
|
259
|
139 |
apply(subgoal_tac "\<exists>s. s \<in> A")
|
|
258
|
140 |
apply(erule exE)
|
|
259
|
141 |
apply(subgoal_tac "finite {s @ s1 |s1. s1 \<in> B}")
|
|
|
142 |
apply(rule_tac f="\<lambda>s1. s @ s1" in finite_imageD)
|
|
258
|
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:
|
|
259
|
152 |
assumes "A \<noteq> {}" "B \<noteq> {}"
|
|
|
153 |
shows "finite (A ;; B) \<longleftrightarrow> (finite (A \<times> B))"
|
|
258
|
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:
|
|
259
|
172 |
assumes "s \<in> A" " s \<noteq> []"
|
|
|
173 |
shows "infinite (A\<star>)"
|
|
258
|
174 |
proof -
|
|
259
|
175 |
have "inj (\<lambda>n. concat (replicate n s))"
|
|
258
|
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
|
|
259
|
181 |
have "infinite ((\<lambda>n. concat (replicate n s)) ` UNIV)"
|
|
258
|
182 |
by (simp add: range_inj_infinite)
|
|
|
183 |
moreover
|
|
259
|
184 |
have "((\<lambda>n. concat (replicate n s)) ` UNIV) \<subseteq> (A\<star>)"
|
|
258
|
185 |
using Star_concat_replicate assms(1) by auto
|
|
259
|
186 |
ultimately show "infinite (A\<star>)"
|
|
258
|
187 |
using infinite_super by auto
|
|
|
188 |
qed
|
|
|
189 |
|
|
|
190 |
lemma infinitestrings_correctness:
|
|
259
|
191 |
shows "infinitestrings r \<longleftrightarrow> infinite (L r)"
|
|
258
|
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
|
|
259
|
203 |
apply(subgoal_tac "L r1 \<noteq> {} \<and> L r2 \<noteq> {}")
|
|
258
|
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 |