equal
deleted
inserted
replaced
131 assumes "v1 \<succ>r v2" |
131 assumes "v1 \<succ>r v2" |
132 shows "hd (flats v2) = hd (flats v1)" |
132 shows "hd (flats v2) = hd (flats v1)" |
133 using assms |
133 using assms |
134 apply(induct) |
134 apply(induct) |
135 apply(auto) |
135 apply(auto) |
136 done |
136 oops |
137 |
137 |
138 |
138 |
139 section {* Posix definition *} |
139 section {* Posix definition *} |
140 |
140 |
141 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
141 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
209 apply(auto)[1] |
209 apply(auto)[1] |
210 apply(case_tac "v1 = v1a") |
210 apply(case_tac "v1 = v1a") |
211 apply(auto) |
211 apply(auto) |
212 apply (metis ValOrd.intros(1)) |
212 apply (metis ValOrd.intros(1)) |
213 apply (rule ValOrd.intros(2)) |
213 apply (rule ValOrd.intros(2)) |
|
214 oops |
214 |
215 |
215 lemma POSIX_ALT2: |
216 lemma POSIX_ALT2: |
216 assumes "POSIX (Left v1) (ALT r1 r2)" |
217 assumes "POSIX (Left v1) (ALT r1 r2)" |
217 shows "POSIX v1 r1" |
218 shows "POSIX v1 r1" |
218 using assms |
219 using assms |
591 using assms |
592 using assms |
592 apply(induct arbitrary: v rule: der.induct) |
593 apply(induct arbitrary: v rule: der.induct) |
593 apply(simp) |
594 apply(simp) |
594 apply(erule Prf.cases) |
595 apply(erule Prf.cases) |
595 apply(simp_all)[5] |
596 apply(simp_all)[5] |
|
597 apply(simp) |
596 apply(erule Prf.cases) |
598 apply(erule Prf.cases) |
597 apply(simp_all)[5] |
599 apply(simp_all)[5] |
598 apply(case_tac "c = c'") |
600 apply(case_tac "c = c'") |
599 apply(simp) |
601 apply(simp) |
600 apply(erule Prf.cases) |
602 apply(erule Prf.cases) |
601 apply(simp_all)[5] |
603 apply(simp_all)[5] |
602 apply (metis Prf.intros(5)) |
604 apply (metis Prf.intros(5)) |
603 apply(erule Prf.cases) |
605 apply(simp) |
604 apply(simp_all)[5] |
606 apply(erule Prf.cases) |
|
607 apply(simp_all)[5] |
|
608 apply(simp) |
605 apply(erule Prf.cases) |
609 apply(erule Prf.cases) |
606 apply(simp_all)[5] |
610 apply(simp_all)[5] |
607 apply (metis Prf.intros(2)) |
611 apply (metis Prf.intros(2)) |
608 apply (metis Prf.intros(3)) |
612 apply (metis Prf.intros(3)) |
609 apply(simp) |
613 apply(simp) |