equal
deleted
inserted
replaced
182 | Seq val val |
182 | Seq val val |
183 | Right val |
183 | Right val |
184 | Left val |
184 | Left val |
185 | Stars "val list" |
185 | Stars "val list" |
186 |
186 |
|
187 datatype_compat val |
|
188 |
|
189 |
187 section {* The string behind a value *} |
190 section {* The string behind a value *} |
188 |
191 |
189 fun |
192 fun |
190 flat :: "val \<Rightarrow> string" |
193 flat :: "val \<Rightarrow> string" |
191 where |
194 where |
350 apply(simp_all)[7] |
353 apply(simp_all)[7] |
351 (* ONE *) |
354 (* ONE *) |
352 apply(erule Prf.cases) |
355 apply(erule Prf.cases) |
353 apply(simp_all)[7] |
356 apply(simp_all)[7] |
354 (* CHAR *) |
357 (* CHAR *) |
355 apply(case_tac "c = char") |
358 apply(case_tac "c = x") |
356 apply(simp) |
359 apply(simp) |
357 apply(erule Prf.cases) |
360 apply(erule Prf.cases) |
358 apply(simp_all)[7] |
361 apply(simp_all)[7] |
359 apply(rule Prf.intros(5)) |
362 apply(rule Prf.intros(5)) |
360 apply(simp) |
363 apply(simp) |
361 apply(erule Prf.cases) |
364 apply(erule Prf.cases) |
362 apply(simp_all)[7] |
365 apply(simp_all)[7] |
363 (* SEQ *) |
366 (* SEQ *) |
364 apply(case_tac "nullable rexp1") |
367 apply(case_tac "nullable x1") |
365 apply(simp) |
368 apply(simp) |
366 apply(erule Prf.cases) |
369 apply(erule Prf.cases) |
367 apply(simp_all)[7] |
370 apply(simp_all)[7] |
368 apply(auto)[1] |
371 apply(auto)[1] |
369 apply(erule Prf.cases) |
372 apply(erule Prf.cases) |
489 apply(simp) |
492 apply(simp) |
490 apply (metis nullable_correctness) |
493 apply (metis nullable_correctness) |
491 apply(metis PMatch.intros(7)) |
494 apply(metis PMatch.intros(7)) |
492 done |
495 done |
493 |
496 |
|
497 find_theorems Stars |
|
498 thm compat_val_list.induct compat_val.induct |
|
499 |
|
500 |
494 lemma PMatch_determ: |
501 lemma PMatch_determ: |
495 shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2" |
502 shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2" |
496 and "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2" |
503 and "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2" |
497 apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts) |
504 apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: compat_val.induct compat_val_list.induct) |
498 apply(erule PMatch.cases) |
505 apply(erule PMatch.cases) |
499 apply(simp_all)[7] |
506 apply(simp_all)[7] |
500 apply(erule PMatch.cases) |
507 apply(erule PMatch.cases) |
501 apply(simp_all)[7] |
508 apply(simp_all)[7] |
502 apply(erule PMatch.cases) |
509 apply(erule PMatch.cases) |
602 apply(simp_all)[7] |
609 apply(simp_all)[7] |
603 (* ONE case *) |
610 (* ONE case *) |
604 apply(erule PMatch.cases) |
611 apply(erule PMatch.cases) |
605 apply(simp_all)[7] |
612 apply(simp_all)[7] |
606 (* CHAR case *) |
613 (* CHAR case *) |
607 apply(case_tac "c = char") |
614 apply(case_tac "c = x") |
608 apply(simp) |
615 apply(simp) |
609 apply(erule PMatch.cases) |
616 apply(erule PMatch.cases) |
610 apply(simp_all)[7] |
617 apply(simp_all)[7] |
611 apply (metis PMatch.intros(2)) |
618 apply (metis PMatch.intros(2)) |
612 apply(simp) |
619 apply(simp) |
620 apply(clarify) |
627 apply(clarify) |
621 apply(rule PMatch.intros) |
628 apply(rule PMatch.intros) |
622 apply metis |
629 apply metis |
623 apply(simp add: der_correctness Der_def) |
630 apply(simp add: der_correctness Der_def) |
624 (* SEQ case *) |
631 (* SEQ case *) |
625 apply(case_tac "nullable rexp1") |
632 apply(case_tac "nullable x1") |
626 apply(simp) |
633 apply(simp) |
627 prefer 2 |
634 prefer 2 |
628 (* not-nullbale case *) |
635 (* not-nullbale case *) |
629 apply(simp) |
636 apply(simp) |
630 apply(erule PMatch.cases) |
637 apply(erule PMatch.cases) |
995 |
1002 |
996 lemma NPrf_Prf_val: |
1003 lemma NPrf_Prf_val: |
997 shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r" |
1004 shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r" |
998 and "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r" |
1005 and "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r" |
999 using assms |
1006 using assms |
1000 apply(induct v and vs arbitrary: r and r rule: val.inducts) |
1007 apply(induct v and vs arbitrary: r and r rule: compat_val.induct compat_val_list.induct) |
1001 apply(auto)[1] |
1008 apply(auto)[1] |
1002 apply(erule Prf.cases) |
1009 apply(erule Prf.cases) |
1003 apply(simp_all)[7] |
1010 apply(simp_all)[7] |
1004 apply(rule_tac x="Void" in exI) |
1011 apply(rule_tac x="Void" in exI) |
1005 apply(simp) |
1012 apply(simp) |