|
1 theory LexerSimp |
|
2 imports "Lexer" |
|
3 begin |
|
4 |
|
5 section {* Lexer including some simplifications *} |
|
6 |
|
7 |
|
8 fun F_RIGHT where |
|
9 "F_RIGHT f v = Right (f v)" |
|
10 |
|
11 fun F_LEFT where |
|
12 "F_LEFT f v = Left (f v)" |
|
13 |
|
14 fun F_ALT where |
|
15 "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)" |
|
16 | "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)" |
|
17 | "F_ALT f1 f2 v = v" |
|
18 |
|
19 |
|
20 fun F_SEQ1 where |
|
21 "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)" |
|
22 |
|
23 fun F_SEQ2 where |
|
24 "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)" |
|
25 |
|
26 fun F_SEQ where |
|
27 "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)" |
|
28 | "F_SEQ f1 f2 v = v" |
|
29 |
|
30 fun simp_ALT where |
|
31 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
|
32 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
|
33 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
|
34 |
|
35 |
|
36 fun simp_SEQ where |
|
37 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
|
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
|
39 | "simp_SEQ (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ZERO, undefined)" |
|
40 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (ZERO, undefined)" |
|
41 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
|
42 |
|
43 lemma simp_SEQ_simps[simp]: |
|
44 "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) |
|
45 else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) |
|
46 else (if (fst p1 = ZERO) then (ZERO, undefined) |
|
47 else (if (fst p2 = ZERO) then (ZERO, undefined) |
|
48 else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))))" |
|
49 by (induct p1 p2 rule: simp_SEQ.induct) (auto) |
|
50 |
|
51 lemma simp_ALT_simps[simp]: |
|
52 "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) |
|
53 else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) |
|
54 else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))" |
|
55 by (induct p1 p2 rule: simp_ALT.induct) (auto) |
|
56 |
|
57 fun |
|
58 simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)" |
|
59 where |
|
60 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
|
61 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" |
|
62 | "simp r = (r, id)" |
|
63 |
|
64 fun |
|
65 slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
|
66 where |
|
67 "slexer r [] = (if nullable r then Some(mkeps r) else None)" |
|
68 | "slexer r (c#s) = (let (rs, fr) = simp (der c r) in |
|
69 (case (slexer rs s) of |
|
70 None \<Rightarrow> None |
|
71 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
|
72 |
|
73 |
|
74 lemma slexer_better_simp: |
|
75 "slexer r (c#s) = (case (slexer (fst (simp (der c r))) s) of |
|
76 None \<Rightarrow> None |
|
77 | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (der c r))) v)))" |
|
78 by (auto split: prod.split option.split) |
|
79 |
|
80 |
|
81 lemma L_fst_simp: |
|
82 shows "L(r) = L(fst (simp r))" |
|
83 by (induct r) (auto) |
|
84 |
|
85 lemma Posix_simp: |
|
86 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
|
87 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
|
88 using assms |
|
89 proof(induct r arbitrary: s v rule: rexp.induct) |
|
90 case (ALT r1 r2 s v) |
|
91 have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact |
|
92 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
|
93 have as: "s \<in> fst (simp (ALT r1 r2)) \<rightarrow> v" by fact |
|
94 consider (ZERO_ZERO) "fst (simp r1) = ZERO" "fst (simp r2) = ZERO" |
|
95 | (ZERO_NZERO) "fst (simp r1) = ZERO" "fst (simp r2) \<noteq> ZERO" |
|
96 | (NZERO_ZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) = ZERO" |
|
97 | (NZERO_NZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO" by auto |
|
98 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" |
|
99 proof(cases) |
|
100 case (ZERO_ZERO) |
|
101 with as have "s \<in> ZERO \<rightarrow> v" by simp |
|
102 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" by (rule Posix_elims(1)) |
|
103 next |
|
104 case (ZERO_NZERO) |
|
105 with as have "s \<in> fst (simp r2) \<rightarrow> v" by simp |
|
106 with IH2 have "s \<in> r2 \<rightarrow> snd (simp r2) v" by simp |
|
107 moreover |
|
108 from ZERO_NZERO have "fst (simp r1) = ZERO" by simp |
|
109 then have "L (fst (simp r1)) = {}" by simp |
|
110 then have "L r1 = {}" using L_fst_simp by simp |
|
111 then have "s \<notin> L r1" by simp |
|
112 ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right (snd (simp r2) v)" by (rule Posix_ALT2) |
|
113 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" |
|
114 using ZERO_NZERO by simp |
|
115 next |
|
116 case (NZERO_ZERO) |
|
117 with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp |
|
118 with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp |
|
119 then have "s \<in> ALT r1 r2 \<rightarrow> Left (snd (simp r1) v)" by (rule Posix_ALT1) |
|
120 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_ZERO by simp |
|
121 next |
|
122 case (NZERO_NZERO) |
|
123 with as have "s \<in> ALT (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
|
124 then consider (Left) v1 where "v = Left v1" "s \<in> (fst (simp r1)) \<rightarrow> v1" |
|
125 | (Right) v2 where "v = Right v2" "s \<in> (fst (simp r2)) \<rightarrow> v2" "s \<notin> L (fst (simp r1))" |
|
126 by (erule_tac Posix_elims(4)) |
|
127 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" |
|
128 proof(cases) |
|
129 case (Left) |
|
130 then have "v = Left v1" "s \<in> r1 \<rightarrow> (snd (simp r1) v1)" using IH1 by simp_all |
|
131 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO |
|
132 by (simp_all add: Posix_ALT1) |
|
133 next |
|
134 case (Right) |
|
135 then have "v = Right v2" "s \<in> r2 \<rightarrow> (snd (simp r2) v2)" "s \<notin> L r1" using IH2 L_fst_simp by simp_all |
|
136 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO |
|
137 by (simp_all add: Posix_ALT2) |
|
138 qed |
|
139 qed |
|
140 next |
|
141 case (SEQ r1 r2 s v) |
|
142 have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact |
|
143 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
|
144 have as: "s \<in> fst (simp (SEQ r1 r2)) \<rightarrow> v" by fact |
|
145 consider (ONE_ONE) "fst (simp r1) = ONE" "fst (simp r2) = ONE" |
|
146 | (ONE_NONE) "fst (simp r1) = ONE" "fst (simp r2) \<noteq> ONE" |
|
147 | (NONE_ONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) = ONE" |
|
148 | (NONE_NONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) \<noteq> ONE" |
|
149 by auto |
|
150 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" |
|
151 proof(cases) |
|
152 case (ONE_ONE) |
|
153 with as have b: "s \<in> ONE \<rightarrow> v" by simp |
|
154 from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 ONE_ONE by simp |
|
155 moreover |
|
156 from b have c: "s = []" "v = Void" using Posix_elims(2) by auto |
|
157 moreover |
|
158 have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE) |
|
159 then have "[] \<in> fst (simp r2) \<rightarrow> Void" using ONE_ONE by simp |
|
160 then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp |
|
161 ultimately have "([] @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) Void)" |
|
162 using Posix_SEQ by blast |
|
163 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using c ONE_ONE by simp |
|
164 next |
|
165 case (ONE_NONE) |
|
166 with as have b: "s \<in> fst (simp r2) \<rightarrow> v" by simp |
|
167 from b have "s \<in> r2 \<rightarrow> snd (simp r2) v" using IH2 ONE_NONE by simp |
|
168 moreover |
|
169 have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE) |
|
170 then have "[] \<in> fst (simp r1) \<rightarrow> Void" using ONE_NONE by simp |
|
171 then have "[] \<in> r1 \<rightarrow> snd (simp r1) Void" using IH1 by simp |
|
172 moreover |
|
173 from ONE_NONE(1) have "L (fst (simp r1)) = {[]}" by simp |
|
174 then have "L r1 = {[]}" by (simp add: L_fst_simp[symmetric]) |
|
175 ultimately have "([] @ s) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) v)" |
|
176 by(rule_tac Posix_SEQ) auto |
|
177 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using ONE_NONE by simp |
|
178 next |
|
179 case (NONE_ONE) |
|
180 with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp |
|
181 with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp |
|
182 moreover |
|
183 have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE) |
|
184 then have "[] \<in> fst (simp r2) \<rightarrow> Void" using NONE_ONE by simp |
|
185 then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp |
|
186 ultimately have "(s @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)" |
|
187 by(rule_tac Posix_SEQ) auto |
|
188 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp |
|
189 next |
|
190 case (NONE_NONE) |
|
191 from as have 00: "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO" |
|
192 apply(auto) |
|
193 apply(smt Posix_elims(1) fst_conv) |
|
194 by (smt NONE_NONE(2) Posix_elims(1) fstI) |
|
195 with NONE_NONE as have "s \<in> SEQ (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
|
196 then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2" |
|
197 "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2" |
|
198 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
|
199 by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) |
|
200 then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)" |
|
201 using IH1 IH2 by auto |
|
202 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE 00 |
|
203 by(auto intro: Posix_SEQ) |
|
204 qed |
|
205 qed (simp_all) |
|
206 |
|
207 |
|
208 lemma slexer_correctness: |
|
209 shows "slexer r s = lexer r s" |
|
210 proof(induct s arbitrary: r) |
|
211 case Nil |
|
212 show "slexer r [] = lexer r []" by simp |
|
213 next |
|
214 case (Cons c s r) |
|
215 have IH: "\<And>r. slexer r s = lexer r s" by fact |
|
216 show "slexer r (c # s) = lexer r (c # s)" |
|
217 proof (cases "s \<in> L (der c r)") |
|
218 case True |
|
219 assume a1: "s \<in> L (der c r)" |
|
220 then obtain v1 where a2: "lexer (der c r) s = Some v1" "s \<in> der c r \<rightarrow> v1" |
|
221 using lexer_correct_Some by auto |
|
222 from a1 have "s \<in> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp |
|
223 then obtain v2 where a3: "lexer (fst (simp (der c r))) s = Some v2" "s \<in> (fst (simp (der c r))) \<rightarrow> v2" |
|
224 using lexer_correct_Some by auto |
|
225 then have a4: "slexer (fst (simp (der c r))) s = Some v2" using IH by simp |
|
226 from a3(2) have "s \<in> der c r \<rightarrow> (snd (simp (der c r))) v2" using Posix_simp by simp |
|
227 with a2(2) have "v1 = (snd (simp (der c r))) v2" using Posix_determ by simp |
|
228 with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split) |
|
229 next |
|
230 case False |
|
231 assume b1: "s \<notin> L (der c r)" |
|
232 then have "lexer (der c r) s = None" using lexer_correct_None by simp |
|
233 moreover |
|
234 from b1 have "s \<notin> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp |
|
235 then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp |
|
236 then have "slexer (fst (simp (der c r))) s = None" using IH by simp |
|
237 ultimately show "slexer r (c # s) = lexer r (c # s)" |
|
238 by (simp del: slexer.simps add: slexer_better_simp) |
|
239 qed |
|
240 qed |
|
241 |
|
242 |
|
243 unused_thms |
|
244 |
|
245 |
|
246 end |