equal
deleted
inserted
replaced
254 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
254 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
255 shows "\<turnstile> Stars vs : STAR r" |
255 shows "\<turnstile> Stars vs : STAR r" |
256 using assms |
256 using assms |
257 by(induct vs) (auto intro: Prf.intros) |
257 by(induct vs) (auto intro: Prf.intros) |
258 |
258 |
|
259 lemma Prf_Stars_append: |
|
260 assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r" |
|
261 shows "\<turnstile> Stars (vs1 @ vs2) : STAR r" |
|
262 using assms |
|
263 apply(induct vs1 arbitrary: vs2) |
|
264 apply(auto intro: Prf.intros) |
|
265 apply(erule Prf.cases) |
|
266 apply(simp_all) |
|
267 apply(auto intro: Prf.intros) |
|
268 done |
|
269 |
|
270 |
259 lemma Star_string: |
271 lemma Star_string: |
260 assumes "s \<in> A\<star>" |
272 assumes "s \<in> A\<star>" |
261 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
273 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
262 using assms |
274 using assms |
263 apply(induct rule: Star.induct) |
275 apply(induct rule: Star.induct) |
266 apply(simp) |
278 apply(simp) |
267 apply(rule_tac x="s1#ss" in exI) |
279 apply(rule_tac x="s1#ss" in exI) |
268 apply(simp) |
280 apply(simp) |
269 done |
281 done |
270 |
282 |
271 |
|
272 lemma Star_val: |
283 lemma Star_val: |
273 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
284 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
274 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
285 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
275 using assms |
286 using assms |
276 apply(induct ss) |
287 apply(induct ss) |
277 apply(auto) |
288 apply(auto) |
278 apply (metis empty_iff list.set(1)) |
289 apply (metis empty_iff list.set(1)) |
279 by (metis concat.simps(2) list.simps(9) set_ConsD) |
290 by (metis concat.simps(2) list.simps(9) set_ConsD) |
|
291 |
280 |
292 |
281 lemma L_flat_Prf1: |
293 lemma L_flat_Prf1: |
282 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
294 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
283 using assms |
295 using assms |
284 by (induct)(auto simp add: Sequ_def) |
296 by (induct)(auto simp add: Sequ_def) |
303 done |
315 done |
304 |
316 |
305 lemma L_flat_Prf: |
317 lemma L_flat_Prf: |
306 "L(r) = {flat v | v. \<turnstile> v : r}" |
318 "L(r) = {flat v | v. \<turnstile> v : r}" |
307 using L_flat_Prf1 L_flat_Prf2 by blast |
319 using L_flat_Prf1 L_flat_Prf2 by blast |
|
320 |
|
321 lemma Star_values_exists: |
|
322 assumes "s \<in> (L r)\<star>" |
|
323 shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r" |
|
324 using assms |
|
325 apply(drule_tac Star_string) |
|
326 apply(auto) |
|
327 |
|
328 by (metis L_flat_Prf2 Prf_Stars Star_val) |
|
329 |
308 |
330 |
309 |
331 |
310 section {* Sulzmann and Lu functions *} |
332 section {* Sulzmann and Lu functions *} |
311 |
333 |
312 fun |
334 fun |