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