36 |
36 |
37 section {* Mkeps, Injval Properties *} |
37 section {* Mkeps, Injval Properties *} |
38 |
38 |
39 lemma mkeps_nullable: |
39 lemma mkeps_nullable: |
40 assumes "nullable(r)" |
40 assumes "nullable(r)" |
41 shows "\<turnstile> mkeps r : r" |
41 shows "\<Turnstile> mkeps r : r" |
42 using assms |
42 using assms |
43 by (induct rule: nullable.induct) |
43 by (induct rule: nullable.induct) |
44 (auto intro: Prf.intros) |
44 (auto intro: Prf.intros) |
45 |
45 |
46 lemma mkeps_flat: |
46 lemma mkeps_flat: |
47 assumes "nullable(r)" |
47 assumes "nullable(r)" |
48 shows "flat (mkeps r) = []" |
48 shows "flat (mkeps r) = []" |
49 using assms |
49 using assms |
50 by (induct rule: nullable.induct) (auto) |
50 by (induct rule: nullable.induct) (auto) |
51 |
51 |
|
52 lemma Prf_injval_flat: |
|
53 assumes "\<Turnstile> v : der c r" |
|
54 shows "flat (injval r c v) = c # (flat v)" |
|
55 using assms |
|
56 apply(induct arbitrary: v rule: der.induct) |
|
57 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits) |
|
58 done |
|
59 |
52 lemma Prf_injval: |
60 lemma Prf_injval: |
53 assumes "\<turnstile> v : der c r" |
61 assumes "\<Turnstile> v : der c r" |
54 shows "\<turnstile> (injval r c v) : r" |
62 shows "\<Turnstile> (injval r c v) : r" |
55 using assms |
63 using assms |
56 apply(induct r arbitrary: c v rule: rexp.induct) |
64 apply(induct r arbitrary: c v rule: rexp.induct) |
57 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
65 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
58 done |
66 apply(simp add: Prf_injval_flat) |
59 |
67 done |
60 lemma Prf_injval_flat: |
68 |
61 assumes "\<turnstile> v : der c r" |
69 |
62 shows "flat (injval r c v) = c # (flat v)" |
|
63 using assms |
|
64 apply(induct arbitrary: v rule: der.induct) |
|
65 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits) |
|
66 done |
|
67 |
70 |
68 text {* |
71 text {* |
69 Mkeps and injval produce, or preserve, Posix values. |
72 Mkeps and injval produce, or preserve, Posix values. |
70 *} |
73 *} |
71 |
74 |