equal
deleted
inserted
replaced
541 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
541 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
542 qed |
542 qed |
543 |
543 |
544 |
544 |
545 text {* |
545 text {* |
546 Our POSIX value is a canonical value. |
546 Our POSIX value is a lexical value. |
547 *} |
547 *} |
548 |
548 |
549 lemma Posix_LV: |
549 lemma Posix_LV: |
550 assumes "s \<in> r \<rightarrow> v" |
550 assumes "s \<in> r \<rightarrow> v" |
551 shows "v \<in> LV r s" |
551 shows "v \<in> LV r s" |
552 using assms |
552 using assms unfolding LV_def |
553 apply(induct rule: Posix.induct) |
553 apply(induct rule: Posix.induct) |
554 apply(auto simp add: LV_def intro: Prf.intros elim: Prf.cases) |
554 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) |
555 apply(rotate_tac 5) |
|
556 apply(erule Prf.cases) |
|
557 apply(simp_all) |
|
558 apply(rule Prf.intros) |
|
559 apply(simp_all) |
|
560 done |
555 done |
561 |
556 |
562 (* |
|
563 lemma test2: |
|
564 assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
|
565 shows "(Stars vs) \<in> LV (STAR r) (flat (Stars vs))" |
|
566 using assms |
|
567 apply(induct vs) |
|
568 apply(auto simp add: LV_def) |
|
569 apply(rule Prf.intros) |
|
570 apply(simp) |
|
571 apply(rule Prf.intros) |
|
572 apply(simp_all) |
|
573 by (metis (no_types, lifting) LV_def Posix_LV mem_Collect_eq) |
|
574 *) |
|
575 |
|
576 end |
557 end |