167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory Matcher
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
imports "Main"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
208
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
5 |
|
882
|
6 |
section \<open>Regular Expressions\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
datatype rexp =
|
495
|
9 |
ZERO
|
|
10 |
| ONE
|
882
|
11 |
| CH char
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
| SEQ rexp rexp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
| ALT rexp rexp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
| STAR rexp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
|
882
|
17 |
section \<open>Sequential Composition of Sets of Strings\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
"A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
|
882
|
24 |
text \<open>Two Simple Properties about Sequential Composition\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
lemma seq_empty [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
shows "A ;; {[]} = A"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
and "{[]} ;; A = A"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
by (simp_all add: Seq_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
lemma seq_null [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
shows "A ;; {} = {}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
and "{} ;; A = {}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
by (simp_all add: Seq_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
|
882
|
36 |
section \<open>Kleene Star for Sets\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
inductive_set
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
for A :: "string set"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
start[intro]: "[] \<in> A\<star>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
| step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
|
882
|
46 |
text \<open>A Standard Property of Star\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
lemma star_cases:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
shows "A\<star> = {[]} \<union> A ;; A\<star>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
unfolding Seq_def
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
by (auto) (metis Star.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
lemma star_decomp:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
assumes a: "c # x \<in> A\<star>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
using a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
by (induct x\<equiv>"c # x" rule: Star.induct)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
(auto simp add: append_eq_Cons_conv)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
|
882
|
61 |
section \<open>Meaning of Regular Expressions\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
L :: "rexp \<Rightarrow> string set"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
where
|
495
|
66 |
"L (ZERO) = {}"
|
|
67 |
| "L (ONE) = {[]}"
|
882
|
68 |
| "L (CH c) = {[c]}"
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
| "L (STAR r) = (L r)\<star>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
|
882
|
73 |
section \<open>The Matcher\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
75 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
nullable :: "rexp \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
where
|
495
|
78 |
"nullable (ZERO) = False"
|
|
79 |
| "nullable (ONE) = True"
|
882
|
80 |
| "nullable (CH c) = False"
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
| "nullable (STAR r) = True"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
|
208
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
|
882
|
86 |
section \<open>Correctness Proof for Nullable\<close>
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
lemma nullable_correctness:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
|
208
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
apply(induct r)
|
495
|
91 |
(* ZERO case *)
|
|
92 |
apply(simp only: nullable.simps)
|
|
93 |
apply(simp only: L.simps)
|
|
94 |
apply(simp)
|
|
95 |
(* ONE case *)
|
|
96 |
apply(simp only: nullable.simps)
|
|
97 |
apply(simp only: L.simps)
|
|
98 |
apply(simp)
|
|
99 |
(* CHAR case *)
|
|
100 |
apply(simp only: nullable.simps)
|
|
101 |
apply(simp only: L.simps)
|
|
102 |
apply(simp)
|
|
103 |
prefer 2
|
|
104 |
(* ALT case *)
|
|
105 |
apply(simp (no_asm) only: nullable.simps)
|
|
106 |
apply(simp only:)
|
|
107 |
apply(simp only: L.simps)
|
|
108 |
apply(simp)
|
|
109 |
(* SEQ case *)
|
|
110 |
oops
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
|
495
|
112 |
lemma nullable_correctness:
|
|
113 |
shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
|
|
114 |
apply(induct r)
|
|
115 |
apply(simp_all)
|
|
116 |
(* all easy subgoals are proved except the last 2 *)
|
|
117 |
(* where the definition of Seq needs to be unfolded. *)
|
|
118 |
oops
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
|
495
|
120 |
lemma nullable_correctness:
|
|
121 |
shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
|
|
122 |
apply(induct r)
|
|
123 |
apply(simp_all add: Seq_def)
|
|
124 |
(* except the star case every thing is proved *)
|
|
125 |
(* we need to use the rule for Star.start *)
|
|
126 |
oops
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
|
495
|
128 |
lemma nullable_correctness:
|
|
129 |
shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
|
|
130 |
apply(induct r)
|
|
131 |
apply(simp_all add: Seq_def Star.start)
|
|
132 |
done
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
|
882
|
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 |
|
167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
220 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
221 |
end |