1 theory Matcher |
1 theory Matcher |
2 imports "Main" |
2 imports "Main" |
3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 section {* Regular Expressions *} |
6 section \<open>Regular Expressions\<close> |
7 |
7 |
8 datatype rexp = |
8 datatype rexp = |
9 ZERO |
9 ZERO |
10 | ONE |
10 | ONE |
11 | CHAR char |
11 | CH char |
12 | SEQ rexp rexp |
12 | SEQ rexp rexp |
13 | ALT rexp rexp |
13 | ALT rexp rexp |
14 | STAR rexp |
14 | STAR rexp |
15 |
15 |
16 |
16 |
17 section {* Sequential Composition of Sets *} |
17 section \<open>Sequential Composition of Sets of Strings\<close> |
18 |
18 |
19 definition |
19 definition |
20 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
20 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
21 where |
21 where |
22 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
22 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
23 |
23 |
24 text {* Two Simple Properties about Sequential Composition *} |
24 text \<open>Two Simple Properties about Sequential Composition\<close> |
25 |
25 |
26 lemma seq_empty [simp]: |
26 lemma seq_empty [simp]: |
27 shows "A ;; {[]} = A" |
27 shows "A ;; {[]} = A" |
28 and "{[]} ;; A = A" |
28 and "{[]} ;; A = A" |
29 by (simp_all add: Seq_def) |
29 by (simp_all add: Seq_def) |
31 lemma seq_null [simp]: |
31 lemma seq_null [simp]: |
32 shows "A ;; {} = {}" |
32 shows "A ;; {} = {}" |
33 and "{} ;; A = {}" |
33 and "{} ;; A = {}" |
34 by (simp_all add: Seq_def) |
34 by (simp_all add: Seq_def) |
35 |
35 |
36 section {* Kleene Star for Sets *} |
36 section \<open>Kleene Star for Sets\<close> |
37 |
37 |
38 inductive_set |
38 inductive_set |
39 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
39 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
40 for A :: "string set" |
40 for A :: "string set" |
41 where |
41 where |
42 start[intro]: "[] \<in> A\<star>" |
42 start[intro]: "[] \<in> A\<star>" |
43 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
43 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
44 |
44 |
45 |
45 |
46 text {* A Standard Property of Star *} |
46 text \<open>A Standard Property of Star\<close> |
47 |
47 |
48 lemma star_cases: |
48 lemma star_cases: |
49 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
49 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
50 unfolding Seq_def |
50 unfolding Seq_def |
51 by (auto) (metis Star.simps) |
51 by (auto) (metis Star.simps) |
56 using a |
56 using a |
57 by (induct x\<equiv>"c # x" rule: Star.induct) |
57 by (induct x\<equiv>"c # x" rule: Star.induct) |
58 (auto simp add: append_eq_Cons_conv) |
58 (auto simp add: append_eq_Cons_conv) |
59 |
59 |
60 |
60 |
61 section {* Semantics of Regular Expressions *} |
61 section \<open>Meaning of Regular Expressions\<close> |
62 |
62 |
63 fun |
63 fun |
64 L :: "rexp \<Rightarrow> string set" |
64 L :: "rexp \<Rightarrow> string set" |
65 where |
65 where |
66 "L (ZERO) = {}" |
66 "L (ZERO) = {}" |
67 | "L (ONE) = {[]}" |
67 | "L (ONE) = {[]}" |
68 | "L (CHAR c) = {[c]}" |
68 | "L (CH c) = {[c]}" |
69 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
69 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
70 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
70 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
71 | "L (STAR r) = (L r)\<star>" |
71 | "L (STAR r) = (L r)\<star>" |
72 |
72 |
73 section {* The Matcher *} |
73 section \<open>The Matcher\<close> |
74 |
74 |
75 fun |
75 fun |
76 nullable :: "rexp \<Rightarrow> bool" |
76 nullable :: "rexp \<Rightarrow> bool" |
77 where |
77 where |
78 "nullable (ZERO) = False" |
78 "nullable (ZERO) = False" |
79 | "nullable (ONE) = True" |
79 | "nullable (ONE) = True" |
80 | "nullable (CHAR c) = False" |
80 | "nullable (CH c) = False" |
81 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
81 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
82 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
82 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
83 | "nullable (STAR r) = True" |
83 | "nullable (STAR r) = True" |
84 |
84 |
85 |
85 |
86 section {* Correctness Proof for Nullable *} |
86 section \<open>Correctness Proof for Nullable\<close> |
87 |
87 |
88 lemma nullable_correctness: |
88 lemma nullable_correctness: |
89 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
89 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
90 apply(induct r) |
90 apply(induct r) |
91 (* ZERO case *) |
91 (* ZERO case *) |
129 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
129 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
130 apply(induct r) |
130 apply(induct r) |
131 apply(simp_all add: Seq_def Star.start) |
131 apply(simp_all add: Seq_def Star.start) |
132 done |
132 done |
133 |
133 |
|
134 section \<open>Derivative Operation\<close> |
|
135 |
|
136 fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
|
137 where |
|
138 "der c (ZERO) = ZERO" |
|
139 | "der c (ONE) = ZERO" |
|
140 | "der c (CH d) = (if c = d then ONE else ZERO)" |
|
141 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
|
142 | "der c (SEQ r1 r2) = (if nullable r1 then ALT (SEQ (der c r1) r2) (der c r2) |
|
143 else SEQ (der c r1) r2)" |
|
144 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
|
145 |
|
146 fun |
|
147 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
|
148 where |
|
149 "ders [] r = r" |
|
150 | "ders (c # s) r = ders s (der c r)" |
|
151 |
|
152 fun |
|
153 matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool" |
|
154 where |
|
155 "matcher r s = nullable (ders s r)" |
|
156 |
|
157 definition |
|
158 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
159 where |
|
160 "Der c A \<equiv> {s. [c] @ s \<in> A}" |
|
161 |
|
162 lemma Der_null [simp]: |
|
163 shows "Der c {} = {}" |
|
164 unfolding Der_def |
|
165 by auto |
|
166 |
|
167 lemma Der_empty [simp]: |
|
168 shows "Der c {[]} = {}" |
|
169 unfolding Der_def |
|
170 by auto |
|
171 |
|
172 lemma Der_char [simp]: |
|
173 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
174 unfolding Der_def |
|
175 by auto |
|
176 |
|
177 lemma Der_union [simp]: |
|
178 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
179 unfolding Der_def |
|
180 by auto |
|
181 |
|
182 lemma Der_insert_nil [simp]: |
|
183 shows "Der c (insert [] A) = Der c A" |
|
184 unfolding Der_def |
|
185 by auto |
|
186 |
|
187 lemma Der_seq [simp]: |
|
188 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
189 unfolding Der_def Seq_def |
|
190 by (auto simp add: Cons_eq_append_conv) |
|
191 |
|
192 lemma Der_star [simp]: |
|
193 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
194 proof - |
|
195 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
196 by (simp only: star_cases[symmetric]) |
|
197 also have "... = Der c (A ;; A\<star>)" |
|
198 by (simp only: Der_union Der_empty) (simp) |
|
199 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
|
200 by simp |
|
201 also have "... = (Der c A) ;; A\<star>" |
|
202 unfolding Seq_def Der_def |
|
203 by (auto dest: star_decomp) |
|
204 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
205 qed |
|
206 |
|
207 lemma der_correctness: |
|
208 shows "L (der c r) = Der c (L r)" |
|
209 apply(induct rule: der.induct) |
|
210 apply(auto simp add: nullable_correctness) |
|
211 done |
|
212 |
|
213 |
|
214 lemma matcher_correctness: |
|
215 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
|
216 by (induct s arbitrary: r) |
|
217 (simp_all add: nullable_correctness der_correctness Der_def) |
|
218 |
|
219 |
134 |
220 |
135 end |
221 end |