89 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p" |
89 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p" |
90 shows "Pos v1 = Pos v2" |
90 shows "Pos v1 = Pos v2" |
91 using assms |
91 using assms |
92 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym) |
92 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym) |
93 |
93 |
|
94 lemma inj_image_eq_if: |
|
95 assumes "f ` A = f ` B" "inj f" |
|
96 shows "A = B" |
|
97 using assms |
|
98 by (simp add: inj_image_eq_iff) |
94 |
99 |
95 lemma Three_to_One: |
100 lemma Three_to_One: |
96 assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" |
101 assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" |
97 and "Pos v1 = Pos v2" |
102 and "Pos v1 = Pos v2" |
98 shows "v1 = v2" |
103 shows "v1 = v2" |
99 using assms |
104 using assms |
100 apply(induct v1 arbitrary: r v2 rule: Pos.induct) |
105 apply(induct v1 arbitrary: r v2 rule: Pos.induct) |
101 apply(erule Prf.cases) |
106 (* ZERO *) |
102 apply(simp_all) |
107 apply(erule Prf.cases) |
103 apply(erule Prf.cases) |
108 apply(simp_all) |
104 apply(simp_all) |
109 (* ONE *) |
105 apply(erule Prf.cases) |
110 apply(erule Prf.cases) |
106 apply(simp_all) |
111 apply(simp_all) |
107 apply(erule Prf.cases) |
112 (* CHAR *) |
108 apply(simp_all) |
113 apply(erule Prf.cases) |
|
114 apply(simp_all) |
|
115 apply(erule Prf.cases) |
|
116 apply(simp_all) |
|
117 (* ALT Left *) |
109 apply(erule Prf.cases) |
118 apply(erule Prf.cases) |
110 apply(simp_all) |
119 apply(simp_all) |
111 apply(erule Prf.cases) |
120 apply(erule Prf.cases) |
112 apply(simp_all) |
121 apply(simp_all) |
113 apply(clarify) |
122 apply(clarify) |
114 apply(simp add: insert_ident) |
123 apply(simp add: insert_ident) |
115 apply(drule_tac x="r1a" in meta_spec) |
124 apply(drule_tac x="r1a" in meta_spec) |
116 apply(drule_tac x="v1a" in meta_spec) |
125 apply(drule_tac x="v1a" in meta_spec) |
117 apply(simp) |
126 apply(simp) |
118 apply(drule_tac meta_mp) |
127 apply(drule_tac meta_mp) |
119 thm subset_antisym |
|
120 apply(rule subset_antisym) |
128 apply(rule subset_antisym) |
121 apply(auto)[3] |
129 apply(auto)[3] |
|
130 (* ALT Right *) |
122 apply(clarify) |
131 apply(clarify) |
123 apply(simp add: insert_ident) |
132 apply(simp add: insert_ident) |
124 using Pos_empty apply blast |
133 using Pos_empty apply blast |
125 apply(erule Prf.cases) |
134 apply(erule Prf.cases) |
126 apply(simp_all) |
135 apply(simp_all) |
136 apply(drule_tac meta_mp) |
145 apply(drule_tac meta_mp) |
137 apply(rule subset_antisym) |
146 apply(rule subset_antisym) |
138 apply(auto)[3] |
147 apply(auto)[3] |
139 apply(erule Prf.cases) |
148 apply(erule Prf.cases) |
140 apply(simp_all) |
149 apply(simp_all) |
|
150 (* SEQ *) |
141 apply(erule Prf.cases) |
151 apply(erule Prf.cases) |
142 apply(simp_all) |
152 apply(simp_all) |
143 apply(simp add: insert_ident) |
153 apply(simp add: insert_ident) |
144 apply(clarify) |
154 apply(clarify) |
145 apply(drule_tac x="r1a" in meta_spec) |
155 apply(drule_tac x="r1a" in meta_spec) |
146 apply(drule_tac x="r2a" in meta_spec) |
156 apply(drule_tac x="r2a" in meta_spec) |
147 apply(drule_tac x="v1b" in meta_spec) |
157 apply(drule_tac x="v1b" in meta_spec) |
148 apply(drule_tac x="v2c" in meta_spec) |
158 apply(drule_tac x="v2c" in meta_spec) |
149 apply(simp) |
159 apply(simp) |
150 apply(drule_tac meta_mp) |
160 apply(drule_tac meta_mp) |
|
161 apply(rule_tac f="op # 0" in inj_image_eq_if) |
|
162 apply(simp add: Setcompr_eq_image) |
151 apply(rule subset_antisym) |
163 apply(rule subset_antisym) |
152 apply(rule subsetI) |
164 apply(rule subsetI) |
153 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}") |
165 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
154 prefer 2 |
|
155 apply(auto)[1] |
|
156 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}") |
|
157 prefer 2 |
|
158 apply (metis (no_types, lifting) Un_iff) |
|
159 apply(simp) |
|
160 apply(rule subsetI) |
166 apply(rule subsetI) |
161 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}") |
167 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
162 prefer 2 |
168 apply(simp) |
163 apply(auto)[1] |
|
164 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}") |
|
165 prefer 2 |
|
166 apply (metis (no_types, lifting) Un_iff) |
|
167 apply(simp (no_asm_use)) |
|
168 apply(simp) |
169 apply(simp) |
169 apply(drule_tac meta_mp) |
170 apply(drule_tac meta_mp) |
|
171 apply(rule_tac f="op # (Suc 0)" in inj_image_eq_if) |
|
172 apply(simp add: Setcompr_eq_image) |
170 apply(rule subset_antisym) |
173 apply(rule subset_antisym) |
171 apply(rule subsetI) |
174 apply(rule subsetI) |
172 apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2b}") |
175 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
173 prefer 2 |
|
174 apply(auto)[1] |
|
175 apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}") |
|
176 prefer 2 |
|
177 apply (metis (no_types, lifting) Un_iff) |
|
178 apply(simp) |
|
179 apply(rule subsetI) |
176 apply(rule subsetI) |
180 apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2c}") |
177 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
181 prefer 2 |
178 apply(simp) |
182 apply(auto)[1] |
179 apply(simp) |
183 apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}") |
180 (* STAR empty *) |
184 prefer 2 |
|
185 apply (metis (no_types, lifting) Un_iff) |
|
186 apply(simp (no_asm_use)) |
|
187 apply(simp) |
|
188 apply(erule Prf.cases) |
181 apply(erule Prf.cases) |
189 apply(simp_all) |
182 apply(simp_all) |
190 apply(erule Prf.cases) |
183 apply(erule Prf.cases) |
191 apply(simp_all) |
184 apply(simp_all) |
192 apply(auto)[1] |
185 apply(auto)[1] |
193 using Pos_empty apply fastforce |
186 using Pos_empty apply fastforce |
|
187 (* STAR non-empty *) |
194 apply(erule Prf.cases) |
188 apply(erule Prf.cases) |
195 apply(simp_all) |
189 apply(simp_all) |
196 apply(erule Prf.cases) |
190 apply(erule Prf.cases) |
197 apply(simp_all) |
191 apply(simp_all) |
198 apply(auto)[1] |
192 apply(auto)[1] |
203 apply(drule_tac x="STAR rb" in meta_spec) |
197 apply(drule_tac x="STAR rb" in meta_spec) |
204 apply(drule_tac x="vb" in meta_spec) |
198 apply(drule_tac x="vb" in meta_spec) |
205 apply(drule_tac x="Stars vsb" in meta_spec) |
199 apply(drule_tac x="Stars vsb" in meta_spec) |
206 apply(simp) |
200 apply(simp) |
207 apply(drule_tac meta_mp) |
201 apply(drule_tac meta_mp) |
|
202 apply(rule_tac f="op # 0" in inj_image_eq_if) |
|
203 apply(simp add: Setcompr_eq_image) |
208 apply(rule subset_antisym) |
204 apply(rule subset_antisym) |
209 apply(rule subsetI) |
205 apply(rule subsetI) |
210 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va}") |
206 apply (smt Un_iff image_iff list.inject mem_Collect_eq nat.discI) |
211 prefer 2 |
|
212 apply(auto)[1] |
|
213 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}") |
|
214 prefer 2 |
|
215 apply (metis (no_types, lifting) Un_iff) |
|
216 apply(simp) |
|
217 apply(rule subsetI) |
207 apply(rule subsetI) |
218 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb}") |
208 using list.inject apply blast |
219 prefer 2 |
209 apply(simp) |
220 apply(auto)[1] |
|
221 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}") |
|
222 prefer 2 |
|
223 apply (metis (no_types, lifting) Un_iff) |
|
224 apply(simp (no_asm_use)) |
|
225 apply(simp) |
210 apply(simp) |
226 apply(drule_tac meta_mp) |
211 apply(drule_tac meta_mp) |
227 apply(rule subset_antisym) |
212 apply(rule subset_antisym) |
228 apply(rule subsetI) |
213 apply(rule subsetI) |
229 apply(case_tac vsa) |
214 apply(case_tac vsa) |
279 apply (metis (no_types, lifting) Un_iff) |
264 apply (metis (no_types, lifting) Un_iff) |
280 apply(simp (no_asm_use)) |
265 apply(simp (no_asm_use)) |
281 apply(simp) |
266 apply(simp) |
282 done |
267 done |
283 |
268 |
|
269 |
|
270 |
|
271 section {* Orderings *} |
|
272 |
|
273 |
284 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _") |
274 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _") |
285 where |
275 where |
286 "ps1 \<sqsubseteq>pre ps2 \<equiv> (\<exists>ps'. ps1 @ps' = ps2)" |
276 "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2" |
287 |
277 |
288 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _") |
278 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _") |
289 where |
279 where |
290 "ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)" |
280 "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2" |
291 |
281 |
292 inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _") |
282 inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _") |
293 where |
283 where |
294 "[] \<sqsubset>lex p#ps" |
284 "[] \<sqsubset>lex (p#ps)" |
295 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)" |
285 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)" |
296 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)" |
286 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)" |
297 |
287 |
298 lemma lex_irrfl: |
288 lemma lex_irrfl: |
299 fixes ps1 ps2 :: "nat list" |
289 fixes ps1 ps2 :: "nat list" |
395 apply(rule_tac x="Suc 0#p" in exI) |
385 apply(rule_tac x="Suc 0#p" in exI) |
396 using assms(2) |
386 using assms(2) |
397 apply(auto simp add: val_ord_def pflat_len_simps) |
387 apply(auto simp add: val_ord_def pflat_len_simps) |
398 done |
388 done |
399 |
389 |
400 |
390 lemma val_ord_LeftE: |
401 lemma val_ord_ALTE: |
391 assumes "(Left v1) :\<sqsubset>val (Left v2)" |
402 assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)" |
392 shows "v1 :\<sqsubset>val v2" |
403 shows "p = 0 \<and> v1 \<sqsubset>val ps v2" |
393 using assms |
404 using assms(1) |
394 apply(simp add: val_ord_ex_def) |
|
395 apply(erule exE) |
|
396 apply(case_tac "p = []") |
405 apply(simp add: val_ord_def) |
397 apply(simp add: val_ord_def) |
406 apply(auto simp add: pflat_len_simps) |
398 apply(auto simp add: pflat_len_simps) |
407 apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def) |
399 apply(rule_tac x="[]" in exI) |
408 by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def) |
400 apply(simp add: Pos_empty pflat_len_simps) |
409 |
401 apply(auto simp add: pflat_len_simps val_ord_def) |
410 lemma val_ord_ALTE2: |
402 apply(rule_tac x="ps" in exI) |
411 assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)" |
403 apply(auto) |
412 shows "p = 1 \<and> v1 \<sqsubset>val ps v2" |
404 apply(drule_tac x="0#q" in bspec) |
413 using assms(1) |
405 apply(simp) |
|
406 apply(simp add: pflat_len_simps) |
|
407 apply(drule_tac x="0#q" in bspec) |
|
408 apply(simp) |
|
409 apply(simp add: pflat_len_simps) |
|
410 done |
|
411 |
|
412 lemma val_ord_RightE: |
|
413 assumes "(Right v1) :\<sqsubset>val (Right v2)" |
|
414 shows "v1 :\<sqsubset>val v2" |
|
415 using assms |
|
416 apply(simp add: val_ord_ex_def) |
|
417 apply(erule exE) |
|
418 apply(case_tac "p = []") |
414 apply(simp add: val_ord_def) |
419 apply(simp add: val_ord_def) |
415 apply(auto simp add: pflat_len_simps) |
420 apply(auto simp add: pflat_len_simps) |
416 apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def) |
421 apply(rule_tac x="[]" in exI) |
417 by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def) |
422 apply(simp add: Pos_empty pflat_len_simps) |
|
423 apply(auto simp add: pflat_len_simps val_ord_def) |
|
424 apply(rule_tac x="ps" in exI) |
|
425 apply(auto) |
|
426 apply(drule_tac x="Suc 0#q" in bspec) |
|
427 apply(simp) |
|
428 apply(simp add: pflat_len_simps) |
|
429 apply(drule_tac x="Suc 0#q" in bspec) |
|
430 apply(simp) |
|
431 apply(simp add: pflat_len_simps) |
|
432 done |
|
433 |
418 |
434 |
419 lemma val_ord_STARI: |
435 lemma val_ord_STARI: |
420 assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
436 assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
421 shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" |
437 shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" |
422 using assms(1) |
438 using assms(1) |
433 apply(simp) |
449 apply(simp) |
434 apply(rule ballI) |
450 apply(rule ballI) |
435 apply(rule impI) |
451 apply(rule impI) |
436 apply(simp) |
452 apply(simp) |
437 apply(auto) |
453 apply(auto) |
|
454 apply(drule_tac x="[]" in bspec) |
|
455 apply(simp add: Pos_empty) |
438 using assms(2) |
456 using assms(2) |
439 apply(simp add: pflat_len_simps) |
457 apply(simp add: pflat_len_simps intlen_append) |
440 apply(auto simp add: pflat_len_Stars_simps) |
458 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
441 done |
459 done |
442 |
460 |
443 lemma val_ord_STARI2: |
461 lemma val_ord_STARI2: |
444 assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
462 assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
445 shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))" |
463 shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))" |
482 apply(auto simp add: pflat_len_def)[1] |
500 apply(auto simp add: pflat_len_def)[1] |
483 apply force |
501 apply force |
484 apply force |
502 apply force |
485 done |
503 done |
486 |
504 |
487 |
505 lemma val_ord_SeqI1: |
488 lemma val_ord_SEQI: |
506 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
489 assumes "v1 \<sqsubset>val p v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
507 shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
490 shows "(Seq v1 v2) \<sqsubset>val (0#p) (Seq v1' v2')" |
|
491 using assms(1) |
508 using assms(1) |
|
509 apply(subst (asm) val_ord_ex_def) |
492 apply(subst (asm) val_ord_def) |
510 apply(subst (asm) val_ord_def) |
493 apply(erule conjE) |
511 apply(clarify) |
|
512 apply(subst val_ord_ex_def) |
|
513 apply(rule_tac x="0#p" in exI) |
494 apply(subst val_ord_def) |
514 apply(subst val_ord_def) |
495 apply(rule conjI) |
515 apply(rule conjI) |
496 apply(simp) |
516 apply(simp) |
497 apply(rule conjI) |
517 apply(rule conjI) |
498 apply(simp add: pflat_len_simps) |
518 apply(simp add: pflat_len_simps) |
504 using assms(2) |
524 using assms(2) |
505 apply(simp) |
525 apply(simp) |
506 apply(auto simp add: pflat_len_simps)[2] |
526 apply(auto simp add: pflat_len_simps)[2] |
507 done |
527 done |
508 |
528 |
509 |
529 lemma val_ord_SeqI2: |
510 lemma val_ord_SEQI2: |
530 assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'" |
511 assumes "v2 \<sqsubset>val p v2'" "flat v2 = flat v2'" |
531 shows "(Seq v v2) :\<sqsubset>val (Seq v v2')" |
512 shows "(Seq v v2) \<sqsubset>val (1#p) (Seq v v2')" |
|
513 using assms(1) |
532 using assms(1) |
|
533 apply(subst (asm) val_ord_ex_def) |
514 apply(subst (asm) val_ord_def) |
534 apply(subst (asm) val_ord_def) |
515 apply(erule conjE)+ |
535 apply(clarify) |
|
536 apply(subst val_ord_ex_def) |
|
537 apply(rule_tac x="Suc 0#p" in exI) |
516 apply(subst val_ord_def) |
538 apply(subst val_ord_def) |
517 apply(rule conjI) |
539 apply(rule conjI) |
518 apply(simp) |
540 apply(simp) |
519 apply(rule conjI) |
541 apply(rule conjI) |
520 apply(simp add: pflat_len_simps) |
542 apply(simp add: pflat_len_simps) |
521 apply(rule ballI) |
543 apply(rule ballI) |
522 apply(rule impI) |
544 apply(rule impI) |
523 apply(simp only: Pos.simps) |
545 apply(simp only: Pos.simps) |
524 apply(auto) |
546 apply(auto)[1] |
525 apply(auto simp add: pflat_len_def intlen_append) |
547 apply(simp add: pflat_len_simps) |
526 apply(auto simp add: assms(2)) |
548 using assms(2) |
527 done |
549 apply(simp) |
|
550 apply(auto simp add: pflat_len_simps) |
|
551 done |
|
552 |
528 |
553 |
529 lemma val_ord_SEQE_0: |
554 lemma val_ord_SEQE_0: |
530 assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')" |
555 assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')" |
531 shows "v1 \<sqsubset>val p v1'" |
556 shows "v1 \<sqsubset>val p v1'" |
532 using assms(1) |
557 using assms(1) |
579 lemma val_ord_SEQE_2: |
604 lemma val_ord_SEQE_2: |
580 assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" |
605 assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" |
581 and "\<turnstile> v1 : r" "\<turnstile> v1' : r" |
606 and "\<turnstile> v1 : r" "\<turnstile> v1' : r" |
582 shows "v1 = v1'" |
607 shows "v1 = v1'" |
583 proof - |
608 proof - |
584 have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0 # q \<sqsubset>lex 1#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q" |
609 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" |
585 using assms(1) |
610 using assms(1) |
586 apply(simp add: val_ord_def) |
611 apply(simp add: val_ord_def) |
587 apply(rule ballI) |
612 apply(rule ballI) |
588 apply(clarify) |
613 apply(clarify) |
589 apply(drule_tac x="0#q" in bspec) |
614 apply(drule_tac x="0#q" in bspec) |
928 apply(drule meta_mp) |
953 apply(drule meta_mp) |
929 apply(auto simp add: CPTpre_def)[1] |
954 apply(auto simp add: CPTpre_def)[1] |
930 using append_eq_conv_conj apply blast |
955 using append_eq_conv_conj apply blast |
931 apply(subst (asm) (2)val_ord_ex1_def) |
956 apply(subst (asm) (2)val_ord_ex1_def) |
932 apply(erule disjE) |
957 apply(erule disjE) |
933 apply(subst (asm) val_ord_ex_def) |
|
934 apply(erule exE) |
|
935 apply(subst val_ord_ex1_def) |
958 apply(subst val_ord_ex1_def) |
936 apply(rule disjI1) |
959 apply(rule disjI1) |
937 apply(subst val_ord_ex_def) |
960 apply(rule val_ord_SeqI1) |
938 apply(rule_tac x="0#p" in exI) |
|
939 apply(rule val_ord_SEQI) |
|
940 apply(simp) |
961 apply(simp) |
941 apply(simp) |
962 apply(simp) |
942 apply (metis Posix1(2) append_assoc append_take_drop_id) |
963 apply (metis Posix1(2) append_assoc append_take_drop_id) |
943 apply(simp) |
964 apply(simp) |
944 apply(drule_tac x="v2b" in meta_spec) |
965 apply(drule_tac x="v2b" in meta_spec) |
945 apply(drule meta_mp) |
966 apply(drule meta_mp) |
946 apply(auto simp add: CPTpre_def)[1] |
967 apply(auto simp add: CPTpre_def)[1] |
947 apply (simp add: Posix1(2)) |
968 apply (simp add: Posix1(2)) |
948 apply(subst (asm) val_ord_ex1_def) |
969 apply(subst (asm) val_ord_ex1_def) |
949 apply(erule disjE) |
970 apply(erule disjE) |
950 apply(subst (asm) val_ord_ex_def) |
|
951 apply(erule exE) |
|
952 apply(subst val_ord_ex1_def) |
971 apply(subst val_ord_ex1_def) |
953 apply(rule disjI1) |
972 apply(rule disjI1) |
954 apply(subst val_ord_ex_def) |
973 apply(rule val_ord_SeqI2) |
955 apply(rule_tac x="1#p" in exI) |
|
956 apply(rule val_ord_SEQI2) |
|
957 apply(simp) |
974 apply(simp) |
958 apply (simp add: Posix1(2)) |
975 apply (simp add: Posix1(2)) |
959 apply(subst val_ord_ex1_def) |
976 apply(subst val_ord_ex1_def) |
960 apply(simp) |
977 apply(simp) |
961 (* ALT *) |
978 (* ALT *) |
1453 apply(auto simp add: PT_def)[1] |
1470 apply(auto simp add: PT_def)[1] |
1454 apply(drule_tac x="Seq v1a v2a" in spec) |
1471 apply(drule_tac x="Seq v1a v2a" in spec) |
1455 apply(simp) |
1472 apply(simp) |
1456 apply(drule mp) |
1473 apply(drule mp) |
1457 apply (simp add: Prf.intros(1) Prf_CPrf) |
1474 apply (simp add: Prf.intros(1) Prf_CPrf) |
1458 apply (meson val_ord_SEQI2 val_ord_ex_def) |
1475 apply (meson val_ord_SeqI2) |
1459 apply(assumption) |
1476 apply(assumption) |
1460 (* SEQ side condition *) |
1477 (* SEQ side condition *) |
1461 apply(auto simp add: PT_def) |
1478 apply(auto simp add: PT_def) |
1462 apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a") |
1479 apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a") |
1463 prefer 2 |
1480 prefer 2 |
1469 apply(drule_tac x="Seq vA vB" in spec) |
1486 apply(drule_tac x="Seq vA vB" in spec) |
1470 apply(simp) |
1487 apply(simp) |
1471 apply(drule mp) |
1488 apply(drule mp) |
1472 apply (simp add: Prf.intros(1)) |
1489 apply (simp add: Prf.intros(1)) |
1473 apply(subst (asm) (3) val_ord_ex_def) |
1490 apply(subst (asm) (3) val_ord_ex_def) |
1474 apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SEQI val_ord_ex_def val_ord_shorterI) |
1491 apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SeqI1 val_ord_ex_def val_ord_shorterI) |
1475 (* STAR *) |
1492 (* STAR *) |
1476 apply(auto simp add: CPT_def)[1] |
1493 apply(auto simp add: CPT_def)[1] |
1477 apply(erule CPrf.cases) |
1494 apply(erule CPrf.cases) |
1478 apply(simp_all)[6] |
1495 apply(simp_all)[6] |
1479 using Posix_STAR2 apply blast |
1496 using Posix_STAR2 apply blast |