equal
deleted
inserted
replaced
1 |
1 |
2 theory Re |
2 theory ReStar |
3 imports "Main" |
3 imports "Main" |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Sequential Composition of Sets *} |
7 section {* Sequential Composition of Sets *} |
56 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
56 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
57 |
57 |
58 lemma star1: |
58 lemma star1: |
59 shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n" |
59 shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n" |
60 apply(induct rule: Star.induct) |
60 apply(induct rule: Star.induct) |
61 apply (metis Re.pow.simps(1) insertI1) |
61 apply (metis pow.simps(1) insertI1) |
62 apply(auto) |
62 apply(auto) |
63 apply(rule_tac x="Suc n" in exI) |
63 apply(rule_tac x="Suc n" in exI) |
64 apply(auto simp add: Sequ_def) |
64 apply(auto simp add: Sequ_def) |
65 done |
65 done |
66 |
66 |
67 lemma star2: |
67 lemma star2: |
68 shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>" |
68 shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>" |
69 apply(induct n arbitrary: s) |
69 apply(induct n arbitrary: s) |
70 apply (metis Re.pow.simps(1) Star.simps empty_iff insertE) |
70 apply (metis pow.simps(1) Star.simps empty_iff insertE) |
71 apply(auto simp add: Sequ_def) |
71 apply(auto simp add: Sequ_def) |
72 done |
72 done |
73 |
73 |
74 lemma star3: |
74 lemma star3: |
75 shows "A\<star> = (\<Union>i. A \<up> i)" |
75 shows "A\<star> = (\<Union>i. A \<up> i)" |
611 apply(simp_all)[7] |
611 apply(simp_all)[7] |
612 apply(auto) |
612 apply(auto) |
613 apply (metis Prf.intros(6) Prf.intros(7)) |
613 apply (metis Prf.intros(6) Prf.intros(7)) |
614 by (metis Prf.intros(7)) |
614 by (metis Prf.intros(7)) |
615 |
615 |
|
616 lemma v3_NP: |
|
617 assumes "\<Turnstile> v : der c r" |
|
618 shows "\<Turnstile> (injval r c v) : r" |
|
619 using assms |
|
620 apply(induct arbitrary: v rule: der.induct) |
|
621 apply(simp) |
|
622 apply(erule NPrf.cases) |
|
623 apply(simp_all)[7] |
|
624 apply(simp) |
|
625 apply(erule NPrf.cases) |
|
626 apply(simp_all)[7] |
|
627 apply(case_tac "c = c'") |
|
628 apply(simp) |
|
629 apply(erule NPrf.cases) |
|
630 apply(simp_all)[7] |
|
631 apply (metis NPrf.intros(5)) |
|
632 apply(simp) |
|
633 apply(erule NPrf.cases) |
|
634 apply(simp_all)[7] |
|
635 apply(simp) |
|
636 apply(erule NPrf.cases) |
|
637 apply(simp_all)[7] |
|
638 apply (metis NPrf.intros(2)) |
|
639 apply (metis NPrf.intros(3)) |
|
640 apply(simp) |
|
641 apply(case_tac "nullable r1") |
|
642 apply(simp) |
|
643 apply(erule NPrf.cases) |
|
644 apply(simp_all)[7] |
|
645 apply(auto)[1] |
|
646 apply(erule NPrf.cases) |
|
647 apply(simp_all)[7] |
|
648 apply(auto)[1] |
|
649 apply (metis NPrf.intros(1)) |
|
650 apply(auto)[1] |
|
651 oops |
|
652 |
616 lemma v3_proj: |
653 lemma v3_proj: |
617 assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s" |
654 assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s" |
618 shows "\<Turnstile> (projval r c v) : der c r" |
655 shows "\<Turnstile> (projval r c v) : der c r" |
619 using assms |
656 using assms |
620 apply(induct rule: NPrf.induct) |
657 apply(induct rule: NPrf.induct) |