equal
deleted
inserted
replaced
145 assumes "POSIX v1 r1" "POSIX v2 r2" |
145 assumes "POSIX v1 r1" "POSIX v2 r2" |
146 shows "POSIX (Seq v1 v2) (SEQ r1 r2)" |
146 shows "POSIX (Seq v1 v2) (SEQ r1 r2)" |
147 using assms |
147 using assms |
148 unfolding POSIX_def |
148 unfolding POSIX_def |
149 apply(auto) |
149 apply(auto) |
150 apply(rotate_tac 4) |
150 apply(rotate_tac 2) |
151 apply(erule Prf.cases) |
151 apply(erule Prf.cases) |
152 apply(simp_all)[5] |
152 apply(simp_all)[5] |
153 apply(auto)[1] |
153 apply(auto)[1] |
154 apply(rule ValOrd.intros) |
154 apply(rule ValOrd.intros) |
155 apply(auto) |
155 |
156 done |
156 apply(auto) |
|
157 done |
|
158 *) |
157 |
159 |
158 lemma POSIX_ALT: |
160 lemma POSIX_ALT: |
159 assumes "POSIX (Left v1) (ALT r1 r2)" |
161 assumes "POSIX (Left v1) (ALT r1 r2)" |
160 shows "POSIX v1 r1" |
162 shows "POSIX v1 r1" |
161 using assms |
163 using assms |
165 apply(simp) |
167 apply(simp) |
166 apply(drule mp) |
168 apply(drule mp) |
167 apply(rule Prf.intros) |
169 apply(rule Prf.intros) |
168 apply(auto) |
170 apply(auto) |
169 apply(erule ValOrd.cases) |
171 apply(erule ValOrd.cases) |
170 apply(simp_all)[7] |
172 apply(simp_all) |
171 done |
173 done |
172 |
174 |
173 lemma POSIX_ALT1a: |
175 lemma POSIX_ALT1a: |
174 assumes "POSIX (Right v2) (ALT r1 r2)" |
176 assumes "POSIX (Right v2) (ALT r1 r2)" |
175 shows "POSIX v2 r2" |
177 shows "POSIX v2 r2" |
180 apply(simp) |
182 apply(simp) |
181 apply(drule mp) |
183 apply(drule mp) |
182 apply(rule Prf.intros) |
184 apply(rule Prf.intros) |
183 apply(auto) |
185 apply(auto) |
184 apply(erule ValOrd.cases) |
186 apply(erule ValOrd.cases) |
185 apply(simp_all)[7] |
187 apply(simp_all) |
186 done |
188 done |
|
189 |
187 |
190 |
188 lemma POSIX_ALT1b: |
191 lemma POSIX_ALT1b: |
189 assumes "POSIX (Right v2) (ALT r1 r2)" |
192 assumes "POSIX (Right v2) (ALT r1 r2)" |
190 shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flats v' = flats v2) \<longrightarrow> v2 \<succ>r2 v')" |
193 shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')" |
191 using assms |
194 using assms |
192 apply(drule_tac POSIX_ALT1a) |
195 apply(drule_tac POSIX_ALT1a) |
193 unfolding POSIX_def |
196 unfolding POSIX_def |
194 apply(auto) |
197 apply(auto) |
195 done |
198 done |
205 apply(simp_all)[5] |
208 apply(simp_all)[5] |
206 apply(auto) |
209 apply(auto) |
207 apply(rule ValOrd.intros) |
210 apply(rule ValOrd.intros) |
208 apply(auto) |
211 apply(auto) |
209 apply(rule ValOrd.intros) |
212 apply(rule ValOrd.intros) |
210 by (metis flats_flat order_refl) |
213 by simp |
211 |
214 |
212 lemma POSIX_ALT_I2: |
215 lemma POSIX_ALT_I2: |
213 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
216 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
214 shows "POSIX (Right v2) (ALT r1 r2)" |
217 shows "POSIX (Right v2) (ALT r1 r2)" |
215 using assms |
218 using assms |
217 apply(auto) |
220 apply(auto) |
218 apply(rotate_tac 3) |
221 apply(rotate_tac 3) |
219 apply(erule Prf.cases) |
222 apply(erule Prf.cases) |
220 apply(simp_all)[5] |
223 apply(simp_all)[5] |
221 apply(auto) |
224 apply(auto) |
222 prefer 2 |
|
223 apply(rule ValOrd.intros) |
225 apply(rule ValOrd.intros) |
224 apply metis |
226 apply metis |
225 apply(rule ValOrd.intros) |
227 done |
226 apply(auto) |
228 |
227 done |
229 |
228 *) |
230 section {* The ordering is reflexive *} |
229 |
231 |
230 lemma ValOrd_refl: |
232 lemma ValOrd_refl: |
231 assumes "\<turnstile> v : r" |
233 assumes "\<turnstile> v : r" |
232 shows "v \<succ>r v" |
234 shows "v \<succ>r v" |
233 using assms |
235 using assms |
519 apply(simp_all)[5] |
521 apply(simp_all)[5] |
520 using ValOrd.simps apply blast |
522 using ValOrd.simps apply blast |
521 apply(auto) |
523 apply(auto) |
522 apply(erule Prf.cases) |
524 apply(erule Prf.cases) |
523 apply(simp_all)[5] |
525 apply(simp_all)[5] |
524 prefer 2 |
526 (* base cases done *) |
525 apply(case_tac "nullable r1") |
527 (* ALT case *) |
526 apply(simp) |
528 apply(erule Prf.cases) |
527 defer |
529 apply(simp_all)[5] |
528 apply(simp) |
530 using POSIX_ALT POSIX_ALT_I1 apply blast |
529 apply(erule Prf.cases) |
531 apply(frule POSIX_ALT1a) |
530 apply(simp_all)[5] |
532 apply(drule POSIX_ALT1b) |
531 apply(auto)[1] |
533 apply(rule POSIX_ALT_I2) |
532 oops |
534 apply auto[1] |
|
535 apply(subst v4) |
|
536 apply(auto)[2] |
|
537 apply(rotate_tac 1) |
|
538 apply(drule_tac x="v2" in meta_spec) |
|
539 apply(simp) |
|
540 apply(subst (asm) (4) POSIX_def) |
|
541 apply(subst (asm) v4) |
|
542 apply(auto)[2] |
|
543 (* stuck in the ALT case *) |