|
1 (* Title: POSIX Lexing with Derivatives of Regular Expressions |
|
2 Authors: Fahad Ausaf <fahad.ausaf at icloud.com>, 2016 |
|
3 Roy Dyckhoff <roy.dyckhoff at st-andrews.ac.uk>, 2016 |
|
4 Christian Urban <christian.urban at kcl.ac.uk>, 2016 |
|
5 Maintainer: Christian Urban <christian.urban at kcl.ac.uk> |
|
6 *) |
|
7 |
|
8 theory Simplifying |
|
9 imports "Lexer" |
|
10 begin |
|
11 |
|
12 section {* Lexer including simplifications *} |
|
13 |
|
14 |
|
15 fun F_RIGHT where |
|
16 "F_RIGHT f v = Right (f v)" |
|
17 |
|
18 fun F_LEFT where |
|
19 "F_LEFT f v = Left (f v)" |
|
20 |
|
21 fun F_Plus where |
|
22 "F_Plus f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)" |
|
23 | "F_Plus f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)" |
|
24 | "F_Plus f1 f2 v = v" |
|
25 |
|
26 |
|
27 fun F_Times1 where |
|
28 "F_Times1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)" |
|
29 |
|
30 fun F_Times2 where |
|
31 "F_Times2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)" |
|
32 |
|
33 fun F_Times where |
|
34 "F_Times 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)" |
|
35 | "F_Times f1 f2 v = v" |
|
36 |
|
37 fun simp_Plus where |
|
38 "simp_Plus (Zero, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
|
39 | "simp_Plus (r\<^sub>1, f\<^sub>1) (Zero, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
|
40 | "simp_Plus (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (Plus r\<^sub>1 r\<^sub>2, F_Plus f\<^sub>1 f\<^sub>2)" |
|
41 |
|
42 fun simp_Times where |
|
43 "simp_Times (One, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_Times1 f\<^sub>1 f\<^sub>2)" |
|
44 | "simp_Times (r\<^sub>1, f\<^sub>1) (One, f\<^sub>2) = (r\<^sub>1, F_Times2 f\<^sub>1 f\<^sub>2)" |
|
45 | "simp_Times (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (Times r\<^sub>1 r\<^sub>2, F_Times f\<^sub>1 f\<^sub>2)" |
|
46 |
|
47 lemma simp_Times_simps[simp]: |
|
48 "simp_Times p1 p2 = (if (fst p1 = One) then (fst p2, F_Times1 (snd p1) (snd p2)) |
|
49 else (if (fst p2 = One) then (fst p1, F_Times2 (snd p1) (snd p2)) |
|
50 else (Times (fst p1) (fst p2), F_Times (snd p1) (snd p2))))" |
|
51 by (induct p1 p2 rule: simp_Times.induct) (auto) |
|
52 |
|
53 lemma simp_Plus_simps[simp]: |
|
54 "simp_Plus p1 p2 = (if (fst p1 = Zero) then (fst p2, F_RIGHT (snd p2)) |
|
55 else (if (fst p2 = Zero) then (fst p1, F_LEFT (snd p1)) |
|
56 else (Plus (fst p1) (fst p2), F_Plus (snd p1) (snd p2))))" |
|
57 by (induct p1 p2 rule: simp_Plus.induct) (auto) |
|
58 |
|
59 fun |
|
60 simp :: "'a rexp \<Rightarrow> 'a rexp * ('a val \<Rightarrow> 'a val)" |
|
61 where |
|
62 "simp (Plus r1 r2) = simp_Plus (simp r1) (simp r2)" |
|
63 | "simp (Times r1 r2) = simp_Times (simp r1) (simp r2)" |
|
64 | "simp r = (r, id)" |
|
65 |
|
66 fun |
|
67 slexer :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> ('a val) option" |
|
68 where |
|
69 "slexer r [] = (if nullable r then Some(mkeps r) else None)" |
|
70 | "slexer r (c#s) = (let (rs, fr) = simp (deriv c r) in |
|
71 (case (slexer rs s) of |
|
72 None \<Rightarrow> None |
|
73 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
|
74 |
|
75 lemma slexer_better_simp: |
|
76 "slexer r (c#s) = (case (slexer (fst (simp (deriv c r))) s) of |
|
77 None \<Rightarrow> None |
|
78 | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (deriv c r))) v)))" |
|
79 by (auto split: prod.split option.split) |
|
80 |
|
81 |
|
82 lemma L_fst_simp: |
|
83 shows "lang r = lang (fst (simp r))" |
|
84 using assms |
|
85 by (induct r) (auto) |
|
86 |
|
87 lemma Posix_simp: |
|
88 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
|
89 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
|
90 using assms |
|
91 proof(induct r arbitrary: s v rule: rexp.induct) |
|
92 case (Plus r1 r2 s v) |
|
93 have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact |
|
94 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
|
95 have as: "s \<in> fst (simp (Plus r1 r2)) \<rightarrow> v" by fact |
|
96 consider (Zero_Zero) "fst (simp r1) = Zero" "fst (simp r2) = Zero" |
|
97 | (Zero_NZero) "fst (simp r1) = Zero" "fst (simp r2) \<noteq> Zero" |
|
98 | (NZero_Zero) "fst (simp r1) \<noteq> Zero" "fst (simp r2) = Zero" |
|
99 | (NZero_NZero) "fst (simp r1) \<noteq> Zero" "fst (simp r2) \<noteq> Zero" by auto |
|
100 then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" |
|
101 proof(cases) |
|
102 case (Zero_Zero) |
|
103 with as have "s \<in> Zero \<rightarrow> v" by simp |
|
104 then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" by (rule Posix_elims(1)) |
|
105 next |
|
106 case (Zero_NZero) |
|
107 with as have "s \<in> fst (simp r2) \<rightarrow> v" by simp |
|
108 with IH2 have "s \<in> r2 \<rightarrow> snd (simp r2) v" by simp |
|
109 moreover |
|
110 from Zero_NZero have "fst (simp r1) = Zero" by simp |
|
111 then have "lang (fst (simp r1)) = {}" by simp |
|
112 then have "lang r1 = {}" using L_fst_simp by auto |
|
113 then have "s \<notin> lang r1" by simp |
|
114 ultimately have "s \<in> Plus r1 r2 \<rightarrow> Right (snd (simp r2) v)" by (rule Posix_Plus2) |
|
115 then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" |
|
116 using Zero_NZero by simp |
|
117 next |
|
118 case (NZero_Zero) |
|
119 with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp |
|
120 with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp |
|
121 then have "s \<in> Plus r1 r2 \<rightarrow> Left (snd (simp r1) v)" by (rule Posix_Plus1) |
|
122 then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" using NZero_Zero by simp |
|
123 next |
|
124 case (NZero_NZero) |
|
125 with as have "s \<in> Plus (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
|
126 then consider (Left) v1 where "v = Left v1" "s \<in> (fst (simp r1)) \<rightarrow> v1" |
|
127 | (Right) v2 where "v = Right v2" "s \<in> (fst (simp r2)) \<rightarrow> v2" "s \<notin> lang (fst (simp r1))" |
|
128 by (erule_tac Posix_elims(4)) |
|
129 then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" |
|
130 proof(cases) |
|
131 case (Left) |
|
132 then have "v = Left v1" "s \<in> r1 \<rightarrow> (snd (simp r1) v1)" using IH1 by simp_all |
|
133 then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" using NZero_NZero |
|
134 by (simp_all add: Posix_Plus1) |
|
135 next |
|
136 case (Right) |
|
137 then have "v = Right v2" "s \<in> r2 \<rightarrow> (snd (simp r2) v2)" "s \<notin> lang r1" using IH2 L_fst_simp by auto |
|
138 then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" using NZero_NZero |
|
139 by (simp_all add: Posix_Plus2) |
|
140 qed |
|
141 qed |
|
142 next |
|
143 case (Times r1 r2 s v) |
|
144 have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact |
|
145 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
|
146 have as: "s \<in> fst (simp (Times r1 r2)) \<rightarrow> v" by fact |
|
147 consider (One_One) "fst (simp r1) = One" "fst (simp r2) = One" |
|
148 | (One_NOne) "fst (simp r1) = One" "fst (simp r2) \<noteq> One" |
|
149 | (NOne_One) "fst (simp r1) \<noteq> One" "fst (simp r2) = One" |
|
150 | (NOne_NOne) "fst (simp r1) \<noteq> One" "fst (simp r2) \<noteq> One" by auto |
|
151 then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" |
|
152 proof(cases) |
|
153 case (One_One) |
|
154 with as have b: "s \<in> One \<rightarrow> v" by simp |
|
155 from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 One_One by simp |
|
156 moreover |
|
157 from b have c: "s = []" "v = Void" using Posix_elims(2) by auto |
|
158 moreover |
|
159 have "[] \<in> One \<rightarrow> Void" by (simp add: Posix_One) |
|
160 then have "[] \<in> fst (simp r2) \<rightarrow> Void" using One_One by simp |
|
161 then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp |
|
162 ultimately have "([] @ []) \<in> Times r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) Void)" |
|
163 using Posix_Times by blast |
|
164 then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using c One_One by simp |
|
165 next |
|
166 case (One_NOne) |
|
167 with as have b: "s \<in> fst (simp r2) \<rightarrow> v" by simp |
|
168 from b have "s \<in> r2 \<rightarrow> snd (simp r2) v" using IH2 One_NOne by simp |
|
169 moreover |
|
170 have "[] \<in> One \<rightarrow> Void" by (simp add: Posix_One) |
|
171 then have "[] \<in> fst (simp r1) \<rightarrow> Void" using One_NOne by simp |
|
172 then have "[] \<in> r1 \<rightarrow> snd (simp r1) Void" using IH1 by simp |
|
173 moreover |
|
174 from One_NOne(1) have "lang (fst (simp r1)) = {[]}" by simp |
|
175 then have "lang r1 = {[]}" by (simp add: L_fst_simp[symmetric]) |
|
176 ultimately have "([] @ s) \<in> Times r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) v)" |
|
177 by(rule_tac Posix_Times) auto |
|
178 then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using One_NOne by simp |
|
179 next |
|
180 case (NOne_One) |
|
181 with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp |
|
182 with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp |
|
183 moreover |
|
184 have "[] \<in> One \<rightarrow> Void" by (simp add: Posix_One) |
|
185 then have "[] \<in> fst (simp r2) \<rightarrow> Void" using NOne_One by simp |
|
186 then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp |
|
187 ultimately have "(s @ []) \<in> Times r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)" |
|
188 by(rule_tac Posix_Times) auto |
|
189 then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using NOne_One by simp |
|
190 next |
|
191 case (NOne_NOne) |
|
192 with as have "s \<in> Times (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
|
193 then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2" |
|
194 "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2" |
|
195 "\<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> lang r1 \<and> s\<^sub>4 \<in> lang r2)" |
|
196 by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) |
|
197 then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)" |
|
198 using IH1 IH2 by auto |
|
199 then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using eqs NOne_NOne |
|
200 by(auto intro: Posix_Times) |
|
201 qed |
|
202 qed (simp_all) |
|
203 |
|
204 |
|
205 lemma slexer_correctness: |
|
206 shows "slexer r s = lexer r s" |
|
207 proof(induct s arbitrary: r) |
|
208 case Nil |
|
209 show "slexer r [] = lexer r []" by simp |
|
210 next |
|
211 case (Cons c s r) |
|
212 have IH: "\<And>r. slexer r s = lexer r s" by fact |
|
213 show "slexer r (c # s) = lexer r (c # s)" |
|
214 proof (cases "s \<in> lang (deriv c r)") |
|
215 case True |
|
216 assume a1: "s \<in> lang (deriv c r)" |
|
217 then obtain v1 where a2: "lexer (deriv c r) s = Some v1" "s \<in> deriv c r \<rightarrow> v1" |
|
218 using lexer_correct_Some by auto |
|
219 from a1 have "s \<in> lang (fst (simp (deriv c r)))" using L_fst_simp[symmetric] by auto |
|
220 then obtain v2 where a3: "lexer (fst (simp (deriv c r))) s = Some v2" "s \<in> (fst (simp (deriv c r))) \<rightarrow> v2" |
|
221 using lexer_correct_Some by auto |
|
222 then have a4: "slexer (fst (simp (deriv c r))) s = Some v2" using IH by simp |
|
223 from a3(2) have "s \<in> deriv c r \<rightarrow> (snd (simp (deriv c r))) v2" using Posix_simp by auto |
|
224 with a2(2) have "v1 = (snd (simp (deriv c r))) v2" using Posix_determ by auto |
|
225 with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split) |
|
226 next |
|
227 case False |
|
228 assume b1: "s \<notin> lang (deriv c r)" |
|
229 then have "lexer (deriv c r) s = None" using lexer_correct_None by auto |
|
230 moreover |
|
231 from b1 have "s \<notin> lang (fst (simp (deriv c r)))" using L_fst_simp[symmetric] by auto |
|
232 then have "lexer (fst (simp (deriv c r))) s = None" using lexer_correct_None by auto |
|
233 then have "slexer (fst (simp (deriv c r))) s = None" using IH by simp |
|
234 ultimately show "slexer r (c # s) = lexer r (c # s)" |
|
235 by (simp del: slexer.simps add: slexer_better_simp) |
|
236 qed |
|
237 qed |
|
238 |
|
239 end |