87 using assms |
88 using assms |
88 apply(induct vs arbitrary: n p) |
89 apply(induct vs arbitrary: n p) |
89 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps) |
90 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps) |
90 done |
91 done |
91 |
92 |
92 lemma Two_to_Three_aux: |
93 lemma outside_lemma: |
93 assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p" |
94 assumes "p \<notin> Pos v1 \<union> Pos v2" |
94 shows "p \<in> Pos v1 \<inter> Pos v2" |
95 shows "pflat_len v1 p = pflat_len v2 p" |
95 using assms |
96 using assms by (auto simp add: pflat_len_def) |
96 apply(simp add: pflat_len_def) |
|
97 apply(auto split: if_splits) |
|
98 apply (smt inlen_bigger)+ |
|
99 done |
|
100 |
|
101 lemma Two_to_Three_orig: |
|
102 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p" |
|
103 shows "Pos v1 = Pos v2" |
|
104 using assms |
|
105 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym) |
|
106 |
|
107 lemma inj_image_eq_if: |
|
108 assumes "f ` A = f ` B" "inj f" |
|
109 shows "A = B" |
|
110 using assms |
|
111 by (simp add: inj_image_eq_iff) |
|
112 |
|
113 lemma Three_to_One: |
|
114 assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" |
|
115 and "Pos v1 = Pos v2" |
|
116 shows "v1 = v2" |
|
117 using assms |
|
118 apply(induct v1 arbitrary: r v2 rule: Pos.induct) |
|
119 (* ZERO *) |
|
120 apply(erule Prf.cases) |
|
121 apply(simp_all)[7] |
|
122 (* ONE *) |
|
123 apply(erule Prf.cases) |
|
124 apply(simp_all)[7] |
|
125 (* CHAR *) |
|
126 apply(erule Prf.cases) |
|
127 apply(simp_all)[7] |
|
128 apply(erule Prf.cases) |
|
129 apply(simp_all)[7] |
|
130 (* ALT Left *) |
|
131 apply(erule Prf.cases) |
|
132 apply(simp_all)[7] |
|
133 apply(erule Prf.cases) |
|
134 apply(simp_all)[7] |
|
135 apply(clarify) |
|
136 apply(simp add: insert_ident) |
|
137 apply(drule_tac x="r1a" in meta_spec) |
|
138 apply(drule_tac x="v1a" in meta_spec) |
|
139 apply(simp) |
|
140 apply(drule_tac meta_mp) |
|
141 apply(rule subset_antisym) |
|
142 apply(auto)[3] |
|
143 (* ALT Right *) |
|
144 apply(clarify) |
|
145 apply(simp add: insert_ident) |
|
146 using Pos_empty apply blast |
|
147 apply(erule Prf.cases) |
|
148 apply(simp_all)[7] |
|
149 apply(erule Prf.cases) |
|
150 apply(simp_all)[7] |
|
151 apply(clarify) |
|
152 apply(simp add: insert_ident) |
|
153 using Pos_empty apply blast |
|
154 apply(simp add: insert_ident) |
|
155 apply(drule_tac x="r2a" in meta_spec) |
|
156 apply(drule_tac x="v2b" in meta_spec) |
|
157 apply(simp) |
|
158 apply(drule_tac meta_mp) |
|
159 apply(rule subset_antisym) |
|
160 apply(auto)[3] |
|
161 apply(erule Prf.cases) |
|
162 apply(simp_all)[7] |
|
163 (* SEQ *) |
|
164 apply(erule Prf.cases) |
|
165 apply(simp_all)[7] |
|
166 apply(simp add: insert_ident) |
|
167 apply(clarify) |
|
168 apply(drule_tac x="r1a" in meta_spec) |
|
169 apply(drule_tac x="r2a" in meta_spec) |
|
170 apply(drule_tac x="v1b" in meta_spec) |
|
171 apply(drule_tac x="v2c" in meta_spec) |
|
172 apply(simp) |
|
173 apply(drule_tac meta_mp) |
|
174 apply(rule_tac f="op # 0" in inj_image_eq_if) |
|
175 apply(simp add: Setcompr_eq_image) |
|
176 apply(rule subset_antisym) |
|
177 apply(rule subsetI) |
|
178 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
|
179 apply(rule subsetI) |
|
180 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
|
181 apply(simp) |
|
182 apply(simp) |
|
183 apply(drule_tac meta_mp) |
|
184 apply(rule_tac f="op # (Suc 0)" in inj_image_eq_if) |
|
185 apply(simp add: Setcompr_eq_image) |
|
186 apply(rule subset_antisym) |
|
187 apply(rule subsetI) |
|
188 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
|
189 apply(rule subsetI) |
|
190 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
|
191 apply(simp) |
|
192 apply(simp) |
|
193 (* STAR empty *) |
|
194 apply(erule Prf.cases) |
|
195 apply(simp_all)[7] |
|
196 apply(erule Prf.cases) |
|
197 apply(simp_all)[7] |
|
198 apply(auto)[1] |
|
199 using Pos_empty apply fastforce |
|
200 (* STAR non-empty *) |
|
201 apply(simp) |
|
202 apply(erule Prf.cases) |
|
203 apply(simp_all del: Pos.simps) |
|
204 apply(erule Prf.cases) |
|
205 apply(simp_all del: Pos.simps) |
|
206 apply(simp) |
|
207 apply(auto)[1] |
|
208 using Pos_empty apply fastforce |
|
209 apply(clarify) |
|
210 apply(simp) |
|
211 apply(simp add: insert_ident) |
|
212 apply(drule_tac x="rb" in meta_spec) |
|
213 apply(drule_tac x="STAR rb" in meta_spec) |
|
214 apply(drule_tac x="vb" in meta_spec) |
|
215 apply(drule_tac x="Stars vsb" in meta_spec) |
|
216 apply(simp) |
|
217 apply(drule_tac meta_mp) |
|
218 apply(rule_tac f="op # 0" in inj_image_eq_if) |
|
219 apply(simp add: Setcompr_eq_image) |
|
220 apply(rule subset_antisym) |
|
221 apply(rule subsetI) |
|
222 apply (smt Un_iff image_iff list.inject mem_Collect_eq nat.discI) |
|
223 apply(rule subsetI) |
|
224 using list.inject apply blast |
|
225 apply(simp) |
|
226 apply(simp) |
|
227 apply(drule_tac meta_mp) |
|
228 apply(rule subset_antisym) |
|
229 apply(rule subsetI) |
|
230 apply(case_tac vsa) |
|
231 apply(simp) |
|
232 apply (simp add: Pos_empty) |
|
233 apply(simp) |
|
234 apply(clarify) |
|
235 apply(erule disjE) |
|
236 apply (simp add: Pos_empty) |
|
237 apply(erule disjE) |
|
238 apply(clarify) |
|
239 apply(subgoal_tac |
|
240 "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
241 prefer 2 |
|
242 apply blast |
|
243 apply(subgoal_tac "Suc 0 # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}") |
|
244 prefer 2 |
|
245 apply (metis (no_types, lifting) Un_iff) |
|
246 apply(simp) |
|
247 apply(clarify) |
|
248 apply(subgoal_tac |
|
249 "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
250 prefer 2 |
|
251 apply blast |
|
252 apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}") |
|
253 prefer 2 |
|
254 apply (metis (no_types, lifting) Un_iff) |
|
255 apply(simp) |
|
256 apply(rule subsetI) |
|
257 apply(case_tac vsb) |
|
258 apply(simp) |
|
259 apply (simp add: Pos_empty) |
|
260 apply(simp) |
|
261 apply(clarify) |
|
262 apply(erule disjE) |
|
263 apply (simp add: Pos_empty) |
|
264 apply(erule disjE) |
|
265 apply(clarify) |
|
266 apply(subgoal_tac |
|
267 "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
268 prefer 2 |
|
269 apply(simp) |
|
270 apply(subgoal_tac "Suc 0 # ps \<in> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}") |
|
271 apply blast |
|
272 using list.inject apply blast |
|
273 apply(clarify) |
|
274 apply(subgoal_tac |
|
275 "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
276 prefer 2 |
|
277 apply(simp) |
|
278 apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}") |
|
279 prefer 2 |
|
280 apply (metis (no_types, lifting) Un_iff) |
|
281 apply(simp (no_asm_use)) |
|
282 apply(simp) |
|
283 done |
|
284 |
|
285 |
97 |
286 |
98 |
287 section {* Orderings *} |
99 section {* Orderings *} |
288 |
100 |
289 |
101 |
445 apply(drule_tac x="Suc 0#q" in bspec) |
258 apply(drule_tac x="Suc 0#q" in bspec) |
446 apply(simp) |
259 apply(simp) |
447 apply(simp add: pflat_len_simps) |
260 apply(simp add: pflat_len_simps) |
448 done |
261 done |
449 |
262 |
|
263 |
|
264 lemma val_ord_SeqI1: |
|
265 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
266 shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
|
267 using assms(1) |
|
268 apply(subst (asm) val_ord_ex_def) |
|
269 apply(subst (asm) val_ord_def) |
|
270 apply(clarify) |
|
271 apply(subst val_ord_ex_def) |
|
272 apply(rule_tac x="0#p" in exI) |
|
273 apply(subst val_ord_def) |
|
274 apply(rule conjI) |
|
275 apply(simp) |
|
276 apply(rule conjI) |
|
277 apply(simp add: pflat_len_simps) |
|
278 apply(rule ballI) |
|
279 apply(rule impI) |
|
280 apply(simp only: Pos.simps) |
|
281 apply(auto)[1] |
|
282 apply(simp add: pflat_len_simps) |
|
283 using assms(2) |
|
284 apply(simp) |
|
285 apply(auto simp add: pflat_len_simps)[2] |
|
286 done |
|
287 |
|
288 lemma val_ord_SeqI2: |
|
289 assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'" |
|
290 shows "(Seq v v2) :\<sqsubset>val (Seq v v2')" |
|
291 using assms(1) |
|
292 apply(subst (asm) val_ord_ex_def) |
|
293 apply(subst (asm) val_ord_def) |
|
294 apply(clarify) |
|
295 apply(subst val_ord_ex_def) |
|
296 apply(rule_tac x="Suc 0#p" in exI) |
|
297 apply(subst val_ord_def) |
|
298 apply(rule conjI) |
|
299 apply(simp) |
|
300 apply(rule conjI) |
|
301 apply(simp add: pflat_len_simps) |
|
302 apply(rule ballI) |
|
303 apply(rule impI) |
|
304 apply(simp only: Pos.simps) |
|
305 apply(auto)[1] |
|
306 apply(simp add: pflat_len_simps) |
|
307 using assms(2) |
|
308 apply(simp) |
|
309 apply(auto simp add: pflat_len_simps) |
|
310 done |
|
311 |
|
312 lemma val_ord_SeqE: |
|
313 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
|
314 shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'" |
|
315 using assms |
|
316 apply(simp add: val_ord_ex_def) |
|
317 apply(erule exE) |
|
318 apply(case_tac p) |
|
319 apply(simp add: val_ord_def) |
|
320 apply(auto simp add: pflat_len_simps intlen_append)[1] |
|
321 apply(rule_tac x="[]" in exI) |
|
322 apply(drule_tac x="[]" in spec) |
|
323 apply(simp add: Pos_empty pflat_len_simps) |
|
324 apply(case_tac a) |
|
325 apply(rule disjI1) |
|
326 apply(simp add: val_ord_def) |
|
327 apply(auto simp add: pflat_len_simps intlen_append)[1] |
|
328 apply(rule_tac x="list" in exI) |
|
329 apply(simp) |
|
330 apply(rule ballI) |
|
331 apply(rule impI) |
|
332 apply(drule_tac x="0#q" in bspec) |
|
333 apply(simp) |
|
334 apply(simp add: pflat_len_simps) |
|
335 apply(case_tac nat) |
|
336 apply(rule disjI2) |
|
337 apply(simp add: val_ord_def) |
|
338 apply(auto simp add: pflat_len_simps intlen_append) |
|
339 apply(rule_tac x="list" in exI) |
|
340 apply(simp add: Pos_empty) |
|
341 apply(rule ballI) |
|
342 apply(rule impI) |
|
343 apply(drule_tac x="Suc 0#q" in bspec) |
|
344 apply(simp) |
|
345 apply(simp add: pflat_len_simps) |
|
346 apply(simp add: val_ord_def) |
|
347 done |
|
348 |
450 lemma val_ord_StarsI: |
349 lemma val_ord_StarsI: |
451 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
350 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
452 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
351 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
453 using assms(1) |
352 using assms(1) |
454 apply(subst (asm) val_ord_ex_def) |
353 apply(subst (asm) val_ord_ex_def) |
481 using assms(2) |
380 using assms(2) |
482 apply(simp add: pflat_len_simps intlen_append) |
381 apply(simp add: pflat_len_simps intlen_append) |
483 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
382 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
484 done |
383 done |
485 |
384 |
486 lemma val_ord_SeqI1: |
385 lemma val_ord_Stars_appendI: |
487 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
386 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
488 shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
387 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
489 using assms(1) |
388 using assms |
490 apply(subst (asm) val_ord_ex_def) |
389 apply(induct vs) |
491 apply(subst (asm) val_ord_def) |
390 apply(simp) |
492 apply(clarify) |
391 apply(simp add: val_ord_StarsI2) |
493 apply(subst val_ord_ex_def) |
392 done |
494 apply(rule_tac x="0#p" in exI) |
393 |
495 apply(subst val_ord_def) |
394 lemma val_ord_StarsE2: |
496 apply(rule conjI) |
395 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
497 apply(simp) |
396 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
498 apply(rule conjI) |
397 using assms |
499 apply(simp add: pflat_len_simps) |
|
500 apply(rule ballI) |
|
501 apply(rule impI) |
|
502 apply(simp only: Pos.simps) |
|
503 apply(auto)[1] |
|
504 apply(simp add: pflat_len_simps) |
|
505 using assms(2) |
|
506 apply(simp) |
|
507 apply(auto simp add: pflat_len_simps)[2] |
|
508 done |
|
509 |
|
510 lemma val_ord_SeqI2: |
|
511 assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'" |
|
512 shows "(Seq v v2) :\<sqsubset>val (Seq v v2')" |
|
513 using assms(1) |
|
514 apply(subst (asm) val_ord_ex_def) |
|
515 apply(subst (asm) val_ord_def) |
|
516 apply(clarify) |
|
517 apply(subst val_ord_ex_def) |
|
518 apply(rule_tac x="Suc 0#p" in exI) |
|
519 apply(subst val_ord_def) |
|
520 apply(rule conjI) |
|
521 apply(simp) |
|
522 apply(rule conjI) |
|
523 apply(simp add: pflat_len_simps) |
|
524 apply(rule ballI) |
|
525 apply(rule impI) |
|
526 apply(simp only: Pos.simps) |
|
527 apply(auto)[1] |
|
528 apply(simp add: pflat_len_simps) |
|
529 using assms(2) |
|
530 apply(simp) |
|
531 apply(auto simp add: pflat_len_simps) |
|
532 done |
|
533 |
|
534 |
|
535 lemma val_ord_SEQE_0: |
|
536 assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')" |
|
537 shows "v1 \<sqsubset>val p v1'" |
|
538 using assms(1) |
|
539 apply(simp add: val_ord_def val_ord_ex_def) |
|
540 apply(auto)[1] |
|
541 apply(simp add: pflat_len_simps) |
|
542 apply(simp add: val_ord_def pflat_len_def) |
|
543 apply(auto)[1] |
|
544 apply(drule_tac x="0#q" in bspec) |
|
545 apply(simp) |
|
546 apply(simp) |
|
547 apply(drule_tac x="0#q" in bspec) |
|
548 apply(simp) |
|
549 apply(simp) |
|
550 apply(drule_tac x="0#q" in bspec) |
|
551 apply(simp) |
|
552 apply(simp) |
|
553 apply(simp add: val_ord_def pflat_len_def) |
|
554 apply(auto)[1] |
|
555 done |
|
556 |
|
557 lemma val_ord_SEQE_1: |
|
558 assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" |
|
559 shows "v2 \<sqsubset>val p v2'" |
|
560 using assms(1) |
|
561 apply(simp add: val_ord_def pflat_len_def) |
|
562 apply(auto)[1] |
|
563 apply(drule_tac x="1#q" in bspec) |
|
564 apply(simp) |
|
565 apply(simp) |
|
566 apply(drule_tac x="1#q" in bspec) |
|
567 apply(simp) |
|
568 apply(simp) |
|
569 apply(drule_tac x="1#q" in bspec) |
|
570 apply(simp) |
|
571 apply(auto)[1] |
|
572 apply(drule_tac x="1#q" in bspec) |
|
573 apply(simp) |
|
574 apply(auto) |
|
575 apply(simp add: intlen_append) |
|
576 apply force |
|
577 apply(simp add: intlen_append) |
|
578 apply force |
|
579 apply(simp add: intlen_append) |
|
580 apply force |
|
581 apply(simp add: intlen_append) |
|
582 apply force |
|
583 done |
|
584 |
|
585 lemma val_ord_SEQE_2: |
|
586 assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" |
|
587 and "\<turnstile> v1 : r" "\<turnstile> v1' : r" |
|
588 shows "v1 = v1'" |
|
589 proof - |
|
590 have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0#q \<sqsubset>lex Suc 0#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q" |
|
591 using assms(1) |
|
592 apply(simp add: val_ord_def) |
|
593 apply(rule ballI) |
|
594 apply(clarify) |
|
595 apply(drule_tac x="0#q" in bspec) |
|
596 apply(auto)[1] |
|
597 apply(simp add: pflat_len_simps) |
|
598 done |
|
599 then have "Pos v1 = Pos v1'" |
|
600 apply(rule_tac Two_to_Three_orig) |
|
601 apply(rule ballI) |
|
602 apply(drule_tac x="pa" in bspec) |
|
603 apply(simp) |
|
604 apply(simp) |
|
605 done |
|
606 then show "v1 = v1'" |
|
607 apply(rule_tac Three_to_One) |
|
608 apply(rule assms(2)) |
|
609 apply(rule assms(3)) |
|
610 apply(simp) |
|
611 done |
|
612 qed |
|
613 |
|
614 lemma val_ord_SEQ: |
|
615 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
|
616 and "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
617 and "\<turnstile> v1 : r" "\<turnstile> v1' : r" |
|
618 shows "(v1 :\<sqsubset>val v1') \<or> (v1 = v1' \<and> (v2 :\<sqsubset>val v2'))" |
|
619 using assms(1) |
|
620 apply(subst (asm) val_ord_ex_def) |
398 apply(subst (asm) val_ord_ex_def) |
621 apply(erule exE) |
399 apply(erule exE) |
622 apply(simp only: val_ord_def) |
400 apply(case_tac p) |
623 apply(simp) |
401 apply(simp) |
624 apply(erule conjE)+ |
402 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
625 apply(erule disjE) |
|
626 prefer 2 |
|
627 apply(erule disjE) |
|
628 apply(erule exE) |
|
629 apply(rule disjI1) |
|
630 apply(simp) |
|
631 apply(subst val_ord_ex_def) |
403 apply(subst val_ord_ex_def) |
632 apply(rule_tac x="ps" in exI) |
404 apply(rule_tac x="[]" in exI) |
633 apply(rule val_ord_SEQE_0) |
405 apply(simp add: val_ord_def pflat_len_simps Pos_empty) |
634 apply(simp add: val_ord_def) |
406 apply(simp) |
635 apply(erule exE) |
407 apply(case_tac a) |
636 apply(rule disjI2) |
408 apply(clarify) |
637 apply(rule conjI) |
409 apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1] |
638 thm val_ord_SEQE_1 |
410 apply(clarify) |
639 apply(rule_tac val_ord_SEQE_2) |
411 apply(simp add: val_ord_ex_def) |
640 apply(auto simp add: val_ord_def)[3] |
412 apply(rule_tac x="nat#list" in exI) |
641 apply(rule assms(3)) |
413 apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
642 apply(rule assms(4)) |
414 apply(case_tac q) |
643 apply(subst val_ord_ex_def) |
415 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
644 apply(rule_tac x="ps" in exI) |
416 apply(clarify) |
645 apply(rule_tac val_ord_SEQE_1) |
417 apply(drule_tac x="Suc a # lista" in bspec) |
646 apply(auto simp add: val_ord_def)[1] |
418 apply(simp) |
647 apply(simp) |
419 apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
648 using assms(2) |
420 apply(case_tac q) |
649 apply(simp add: pflat_len_simps) |
421 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
650 done |
422 apply(clarify) |
651 |
423 apply(drule_tac x="Suc a # lista" in bspec) |
652 |
424 apply(simp) |
653 lemma val_ord_ex_trans: |
425 apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
|
426 done |
|
427 |
|
428 lemma val_ord_Stars_appendE: |
|
429 assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
430 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
431 using assms |
|
432 apply(induct vs) |
|
433 apply(simp) |
|
434 apply(simp add: val_ord_StarsE2) |
|
435 done |
|
436 |
|
437 lemma val_ord_Stars_append_eq: |
|
438 assumes "flat (Stars vs1) = flat (Stars vs2)" |
|
439 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
|
440 using assms |
|
441 apply(rule_tac iffI) |
|
442 apply(erule val_ord_Stars_appendE) |
|
443 apply(rule val_ord_Stars_appendI) |
|
444 apply(auto) |
|
445 done |
|
446 |
|
447 |
|
448 lemma val_ord_trans: |
654 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
449 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
655 shows "v1 :\<sqsubset>val v3" |
450 shows "v1 :\<sqsubset>val v3" |
656 using assms |
451 using assms |
657 unfolding val_ord_ex_def |
452 unfolding val_ord_ex_def |
658 apply(clarify) |
453 apply(clarify) |
695 |
493 |
696 lemma Prf_CPrf: |
494 lemma Prf_CPrf: |
697 assumes "\<Turnstile> v : r" |
495 assumes "\<Turnstile> v : r" |
698 shows "\<turnstile> v : r" |
496 shows "\<turnstile> v : r" |
699 using assms |
497 using assms |
700 apply(induct) |
498 by (induct) (auto intro: Prf.intros) |
701 apply(auto intro: Prf.intros) |
499 |
702 done |
500 lemma CPrf_stars: |
|
501 assumes "\<Turnstile> Stars vs : STAR r" |
|
502 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
|
503 using assms |
|
504 apply(induct vs) |
|
505 apply(auto) |
|
506 apply(erule CPrf.cases) |
|
507 apply(simp_all) |
|
508 apply(erule CPrf.cases) |
|
509 apply(simp_all) |
|
510 apply(erule CPrf.cases) |
|
511 apply(simp_all) |
|
512 apply(erule CPrf.cases) |
|
513 apply(simp_all) |
|
514 done |
|
515 |
|
516 lemma CPrf_Stars_appendE: |
|
517 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
518 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
519 using assms |
|
520 apply(induct vs1 arbitrary: vs2) |
|
521 apply(auto intro: CPrf.intros)[1] |
|
522 apply(erule CPrf.cases) |
|
523 apply(simp_all) |
|
524 apply(auto intro: CPrf.intros) |
|
525 done |
|
526 |
|
527 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
528 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
703 |
529 |
704 definition |
530 definition |
705 "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}" |
531 "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}" |
706 |
532 |
707 definition |
533 definition |
708 "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}" |
534 "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}" |
709 |
535 |
710 lemma CPT_CPTpre_subset: |
536 lemma CPT_CPTpre_subset: |
711 shows "CPT r s \<subseteq> CPTpre r s" |
537 shows "CPT r s \<subseteq> CPTpre r s" |
712 apply(auto simp add: CPT_def CPTpre_def) |
538 by(auto simp add: CPT_def CPTpre_def) |
713 done |
|
714 |
|
715 |
539 |
716 lemma CPTpre_subsets: |
540 lemma CPTpre_subsets: |
717 "CPTpre ZERO s = {}" |
541 "CPTpre ZERO s = {}" |
718 "CPTpre ONE s \<subseteq> {Void}" |
542 "CPTpre ONE s \<subseteq> {Void}" |
719 "CPTpre (CHAR c) s \<subseteq> {Char c}" |
543 "CPTpre (CHAR c) s \<subseteq> {Char c}" |
1094 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
918 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
1095 shows "v1 :\<sqsubseteq>val v2" |
919 shows "v1 :\<sqsubseteq>val v2" |
1096 using assms |
920 using assms |
1097 apply(rule_tac Posix_val_ord) |
921 apply(rule_tac Posix_val_ord) |
1098 apply(assumption) |
922 apply(assumption) |
1099 apply(simp add: CPTpre_def CPT_def) |
923 using CPT_CPTpre_subset by auto |
1100 done |
|
1101 |
|
1102 |
|
1103 lemma STAR_val_ord: |
|
1104 assumes "Stars (v1 # vs1) \<sqsubset>val (Suc p # ps) Stars (v2 # vs2)" "flat v1 = flat v2" |
|
1105 shows "(Stars vs1) \<sqsubset>val (p # ps) (Stars vs2)" |
|
1106 using assms(1,2) |
|
1107 apply - |
|
1108 apply(simp(no_asm) add: val_ord_def) |
|
1109 apply(rule conjI) |
|
1110 apply(simp add: val_ord_def) |
|
1111 apply(rule conjI) |
|
1112 apply(simp add: val_ord_def) |
|
1113 apply(auto simp add: pflat_len_simps)[1] |
|
1114 apply(rule ballI) |
|
1115 apply(rule impI) |
|
1116 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
1117 apply(clarify) |
|
1118 apply(case_tac q) |
|
1119 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
1120 apply(clarify) |
|
1121 apply(erule disjE) |
|
1122 prefer 2 |
|
1123 apply(drule_tac x="Suc a # list" in bspec) |
|
1124 apply(simp) |
|
1125 apply(drule mp) |
|
1126 apply(simp) |
|
1127 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
1128 apply(drule_tac x="Suc a # list" in bspec) |
|
1129 apply(simp) |
|
1130 apply(drule mp) |
|
1131 apply(simp) |
|
1132 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
1133 done |
|
1134 |
924 |
1135 |
925 |
1136 lemma Posix_val_ord_reverse: |
926 lemma Posix_val_ord_reverse: |
1137 assumes "s \<in> r \<rightarrow> v1" |
927 assumes "s \<in> r \<rightarrow> v1" |
1138 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
928 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1139 using assms |
929 using assms |
1140 by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
930 by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
1141 val_ord_ex1_def val_ord_ex_def val_ord_ex_trans) |
931 val_ord_ex1_def val_ord_ex_def val_ord_trans) |
1142 |
|
1143 |
|
1144 lemma STAR_val_ord_ex: |
|
1145 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
|
1146 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
1147 using assms |
|
1148 apply(subst (asm) val_ord_ex_def) |
|
1149 apply(erule exE) |
|
1150 apply(case_tac p) |
|
1151 apply(simp) |
|
1152 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
1153 apply(subst val_ord_ex_def) |
|
1154 apply(rule_tac x="[]" in exI) |
|
1155 apply(simp add: val_ord_def pflat_len_simps Pos_empty) |
|
1156 apply(simp) |
|
1157 apply(case_tac a) |
|
1158 apply(clarify) |
|
1159 prefer 2 |
|
1160 using STAR_val_ord val_ord_ex_def apply blast |
|
1161 apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1] |
|
1162 done |
|
1163 |
|
1164 lemma STAR_val_ord_exI: |
|
1165 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
|
1166 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
1167 using assms |
|
1168 apply(induct vs) |
|
1169 apply(simp) |
|
1170 apply(simp) |
|
1171 apply(rule val_ord_StarsI2) |
|
1172 apply(simp) |
|
1173 apply(simp) |
|
1174 done |
|
1175 |
|
1176 lemma STAR_val_ord_ex_append: |
|
1177 assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
1178 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
1179 using assms |
|
1180 apply(induct vs) |
|
1181 apply(simp) |
|
1182 apply(simp) |
|
1183 apply(drule STAR_val_ord_ex) |
|
1184 apply(simp) |
|
1185 done |
|
1186 |
|
1187 lemma STAR_val_ord_ex_append_eq: |
|
1188 assumes "flat (Stars vs1) = flat (Stars vs2)" |
|
1189 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
|
1190 using assms |
|
1191 apply(rule_tac iffI) |
|
1192 apply(erule STAR_val_ord_ex_append) |
|
1193 apply(rule STAR_val_ord_exI) |
|
1194 apply(auto) |
|
1195 done |
|
1196 |
|
1197 |
|
1198 lemma CPrf_stars: |
|
1199 assumes "\<Turnstile> Stars vs : STAR r" |
|
1200 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
|
1201 using assms |
|
1202 apply(induct vs) |
|
1203 apply(auto) |
|
1204 apply(erule CPrf.cases) |
|
1205 apply(simp_all) |
|
1206 apply(erule CPrf.cases) |
|
1207 apply(simp_all) |
|
1208 apply(erule CPrf.cases) |
|
1209 apply(simp_all) |
|
1210 apply(erule CPrf.cases) |
|
1211 apply(simp_all) |
|
1212 done |
|
1213 |
|
1214 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
1215 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
|
1216 |
|
1217 lemma exists: |
|
1218 assumes "s \<in> (L r)\<star>" |
|
1219 shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r" |
|
1220 using assms |
|
1221 apply(drule_tac Star_string) |
|
1222 apply(auto) |
|
1223 by (metis L_flat_Prf2 Prf_Stars Star_val) |
|
1224 |
932 |
1225 |
933 |
1226 lemma val_ord_Posix_Stars: |
934 lemma val_ord_Posix_Stars: |
1227 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
935 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
1228 and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
936 and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |