64 (case (slexer rs s) of |
64 (case (slexer rs s) of |
65 None \<Rightarrow> None |
65 None \<Rightarrow> None |
66 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
66 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
67 |
67 |
68 |
68 |
|
69 lemma slexer_better_simp: |
|
70 "slexer r (c#s) = (case (slexer (fst (simp (der c r))) s) of |
|
71 None \<Rightarrow> None |
|
72 | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (der c r))) v)))" |
|
73 by (auto split: prod.split option.split) |
|
74 |
|
75 |
69 lemma L_fst_simp: |
76 lemma L_fst_simp: |
70 shows "L(r) = L(fst (simp r))" |
77 shows "L(r) = L(fst (simp r))" |
71 using assms |
78 using assms |
72 by (induct r) (auto) |
79 by (induct r) (auto) |
73 |
80 |
74 |
|
75 lemma |
|
76 shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))" |
|
77 using assms |
|
78 apply(induct r arbitrary: v rule: simp.induct) |
|
79 apply(auto intro: Prf.intros) |
|
80 using Prf_elims(3) apply blast |
|
81 apply(erule Prf_elims) |
|
82 apply(simp) |
|
83 apply(clarify) |
|
84 apply(blast) |
|
85 apply(simp) |
|
86 apply(erule Prf_elims) |
|
87 apply(simp) |
|
88 apply(simp) |
|
89 apply(clarify) |
|
90 apply(blast) |
|
91 apply(erule Prf_elims) |
|
92 apply(case_tac v) |
|
93 apply(simp_all) |
|
94 apply(rule Prf.intros) |
|
95 apply(clarify) |
|
96 apply(simp) |
|
97 apply(case_tac v) |
|
98 apply(simp_all) |
|
99 apply(rule Prf.intros) |
|
100 apply(clarify) |
|
101 apply(simp) |
|
102 apply(erule Prf_elims) |
|
103 apply(simp) |
|
104 apply(rule Prf.intros) |
|
105 apply(simp) |
|
106 apply(simp) |
|
107 apply(rule Prf.intros) |
|
108 apply(simp) |
|
109 apply(erule Prf_elims) |
|
110 apply(simp) |
|
111 apply(blast) |
|
112 apply(rule Prf.intros) |
|
113 apply(erule Prf_elims) |
|
114 apply(simp) |
|
115 apply(rule Prf.intros) |
|
116 apply(erule Prf_elims) |
|
117 apply(simp) |
|
118 apply(rule Prf.intros) |
|
119 apply(erule Prf_elims) |
|
120 apply(simp) |
|
121 apply(clarify) |
|
122 apply(blast) |
|
123 apply(rule Prf.intros) |
|
124 apply(blast) |
|
125 using Prf.intros(4) apply blast |
|
126 apply(erule Prf_elims) |
|
127 apply(simp) |
|
128 apply(clarify) |
|
129 apply(blast) |
|
130 apply(rule Prf.intros) |
|
131 using Prf.intros(4) apply blast |
|
132 apply blast |
|
133 apply(erule Prf_elims) |
|
134 apply(case_tac v) |
|
135 apply(simp_all) |
|
136 apply(rule Prf.intros) |
|
137 apply(clarify) |
|
138 apply(simp) |
|
139 apply(clarify) |
|
140 apply(blast) |
|
141 apply(erule Prf_elims) |
|
142 apply(case_tac v) |
|
143 apply(simp_all) |
|
144 apply(rule Prf.intros) |
|
145 apply(clarify) |
|
146 apply(simp) |
|
147 apply(simp) |
|
148 done |
|
149 |
|
150 lemma Posix_simp_nullable: |
|
151 assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v" |
|
152 shows "((snd (simp r)) v) = mkeps r" |
|
153 using assms |
|
154 apply(induct r arbitrary: v) |
|
155 apply(auto) |
|
156 apply(erule Posix_elims) |
|
157 apply(simp) |
|
158 apply(erule Posix_elims) |
|
159 apply(clarify) |
|
160 using Posix.intros(1) apply blast |
|
161 using Posix.intros(1) apply blast |
|
162 using Posix.intros(1) apply blast |
|
163 apply(erule Posix_elims) |
|
164 apply(simp) |
|
165 apply(erule Posix_elims) |
|
166 apply (metis L_fst_simp nullable.simps(1) nullable_correctness) |
|
167 apply(erule Posix_elims) |
|
168 apply(clarify) |
|
169 apply(simp) |
|
170 apply(clarify) |
|
171 apply(simp) |
|
172 apply(simp only: L_fst_simp[symmetric]) |
|
173 apply (simp add: nullable_correctness) |
|
174 apply(erule Posix_elims) |
|
175 using L_fst_simp Posix1(1) nullable_correctness apply blast |
|
176 apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable) |
|
177 apply(erule Posix_elims) |
|
178 apply(clarify) |
|
179 apply(simp) |
|
180 apply(simp only: L_fst_simp[symmetric]) |
|
181 apply (simp add: nullable_correctness) |
|
182 apply(erule Posix_elims) |
|
183 apply(clarify) |
|
184 apply(simp) |
|
185 using L_fst_simp Posix1(1) nullable_correctness apply blast |
|
186 apply(simp) |
|
187 apply(erule Posix_elims) |
|
188 apply(clarify) |
|
189 apply(simp) |
|
190 using Posix1(2) apply auto[1] |
|
191 apply(simp) |
|
192 done |
|
193 |
|
194 lemma Posix_simp: |
81 lemma Posix_simp: |
195 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
82 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
196 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
83 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
197 using assms |
84 using assms |
198 apply(induct r arbitrary: s v rule: rexp.induct) |
85 apply(induct r arbitrary: s v rule: simp.induct) |
199 apply(auto split: if_splits) |
86 apply(simp_all) |
200 prefer 3 |
87 apply(auto)[1] |
|
88 using Posix_elims(1) apply blast |
|
89 apply (simp add: Posix_ALT1) |
|
90 apply (metis L.simps(1) L_fst_simp Posix_ALT2 empty_iff) |
|
91 apply (smt F_ALT.simps(1) F_ALT.simps(2) L_fst_simp Posix_ALT1 Posix_ALT2 Posix_elims(4)) |
|
92 apply(auto)[1] |
|
93 apply (metis (no_types, lifting) Nil_is_append_conv Posix_SEQ Posix_elims(2)) |
|
94 apply(subst append_Nil2[symmetric]) |
|
95 apply(rule Posix_SEQ) |
|
96 apply(simp) |
|
97 using Posix_ONE apply blast |
|
98 apply blast |
|
99 apply(subst append_Nil[symmetric]) |
|
100 apply(rule Posix_SEQ) |
|
101 using Posix_ONE apply blast |
|
102 apply blast |
|
103 apply(auto)[1] |
|
104 apply (metis L.simps(2) L_fst_simp ex_in_conv insert_iff) |
201 apply(erule Posix_elims) |
105 apply(erule Posix_elims) |
202 apply(clarify) |
|
203 apply(simp) |
|
204 apply(rule Posix.intros) |
|
205 apply(blast) |
|
206 apply(blast) |
|
207 apply(auto)[1] |
|
208 apply(simp add: L_fst_simp[symmetric]) |
|
209 apply(auto)[1] |
|
210 prefer 3 |
|
211 apply(rule Posix.intros) |
|
212 apply(blast) |
|
213 apply (metis L.simps(1) L_fst_simp equals0D) |
|
214 prefer 3 |
|
215 apply(rule Posix.intros) |
|
216 apply(blast) |
|
217 prefer 3 |
|
218 apply(erule Posix_elims) |
|
219 apply(clarify) |
|
220 apply(simp) |
|
221 apply(rule Posix.intros) |
|
222 apply(blast) |
|
223 apply(simp) |
|
224 apply(rule Posix.intros) |
|
225 apply(blast) |
|
226 apply(simp add: L_fst_simp[symmetric]) |
|
227 apply(subst append.simps[symmetric]) |
|
228 apply(rule Posix.intros) |
|
229 prefer 2 |
|
230 apply(blast) |
|
231 prefer 2 |
|
232 apply(auto)[1] |
|
233 apply (metis L_fst_simp Posix_elims(2) lexer_correct_Some) |
|
234 apply(subst Posix_simp_nullable) |
|
235 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
236 apply(simp) |
|
237 apply(rule Posix.intros) |
|
238 apply(rule Posix_mkeps) |
|
239 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
240 apply(subst append_Nil2[symmetric]) |
|
241 apply(rule Posix.intros) |
|
242 apply(blast) |
|
243 apply(subst Posix_simp_nullable) |
|
244 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
245 apply(simp) |
|
246 apply(rule Posix.intros) |
|
247 apply(rule Posix_mkeps) |
|
248 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
249 apply(auto) |
106 apply(auto) |
250 done |
107 using L_fst_simp Posix_SEQ by auto |
|
108 |
251 |
109 |
252 lemma slexer_correctness: |
110 lemma slexer_correctness: |
253 shows "slexer r s = lexer r s" |
111 shows "slexer r s = lexer r s" |
254 apply(induct s arbitrary: r) |
112 proof(induct s arbitrary: r) |
255 apply(simp) |
113 case Nil |
256 apply(auto split: option.split prod.split) |
114 show "slexer r [] = lexer r []" by simp |
257 apply (metis L_fst_simp fst_conv lexer_correct_None) |
115 next |
258 using L_fst_simp lexer_correct_None apply fastforce |
116 case (Cons c s r) |
259 by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv) |
117 have IH: "\<And>r. slexer r s = lexer r s" by fact |
260 |
118 show "slexer r (c # s) = lexer r (c # s)" |
261 |
119 proof (cases "s \<in> L (der c r)") |
|
120 case True |
|
121 assume a1: "s \<in> L (der c r)" |
|
122 then obtain v1 where a2: "lexer (der c r) s = Some v1" "s \<in> der c r \<rightarrow> v1" |
|
123 using lexer_correct_Some by auto |
|
124 from a1 have "s \<in> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp |
|
125 then obtain v2 where a3: "lexer (fst (simp (der c r))) s = Some v2" "s \<in> (fst (simp (der c r))) \<rightarrow> v2" |
|
126 using lexer_correct_Some by auto |
|
127 then have a4: "slexer (fst (simp (der c r))) s = Some v2" using IH by simp |
|
128 from a3(2) have "s \<in> der c r \<rightarrow> (snd (simp (der c r))) v2" using Posix_simp by simp |
|
129 with a2(2) have "v1 = (snd (simp (der c r))) v2" using Posix_determ by simp |
|
130 with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split) |
|
131 next |
|
132 case False |
|
133 assume b1: "s \<notin> L (der c r)" |
|
134 then have "lexer (der c r) s = None" using lexer_correct_None by simp |
|
135 moreover |
|
136 from b1 have "s \<notin> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp |
|
137 then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp |
|
138 then have "slexer (fst (simp (der c r))) s = None" using IH by simp |
|
139 ultimately show "slexer r (c # s) = lexer r (c # s)" |
|
140 by (simp del: slexer.simps add: slexer_better_simp) |
|
141 qed |
|
142 qed |
262 |
143 |
263 end |
144 end |