51 by (induct xs)(auto) |
51 by (induct xs)(auto) |
52 |
52 |
53 lemma intlen_append: |
53 lemma intlen_append: |
54 shows "intlen (xs @ ys) = intlen xs + intlen ys" |
54 shows "intlen (xs @ ys) = intlen xs + intlen ys" |
55 by (induct xs arbitrary: ys) (auto) |
55 by (induct xs arbitrary: ys) (auto) |
|
56 |
|
57 lemma intlen_length: |
|
58 shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys" |
|
59 apply(induct xs arbitrary: ys) |
|
60 apply(auto) |
|
61 apply(case_tac ys) |
|
62 apply(simp_all) |
|
63 apply (smt intlen_bigger) |
|
64 (* HERE *) |
|
65 oops |
|
66 |
56 |
67 |
57 lemma intlen_length: |
68 lemma intlen_length: |
58 assumes "length xs < length ys" |
69 assumes "length xs < length ys" |
59 shows "intlen xs < intlen ys" |
70 shows "intlen xs < intlen ys" |
60 using assms |
71 using assms |
183 |
194 |
184 definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _") |
195 definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _") |
185 where |
196 where |
186 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
197 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
187 |
198 |
|
199 |
|
200 |
|
201 |
188 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
202 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
189 where |
203 where |
190 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
204 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
191 |
205 |
192 lemma val_ord_shorterE: |
206 lemma val_ord_shorterE: |
215 assumes "(flat v') \<sqsubset>spre (flat v)" |
229 assumes "(flat v') \<sqsubset>spre (flat v)" |
216 shows "v :\<sqsubset>val v'" |
230 shows "v :\<sqsubset>val v'" |
217 using assms |
231 using assms |
218 apply(rule_tac val_ord_shorterI) |
232 apply(rule_tac val_ord_shorterI) |
219 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all) |
233 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all) |
|
234 |
220 |
235 |
221 |
236 |
222 lemma val_ord_LeftI: |
237 lemma val_ord_LeftI: |
223 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
238 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
224 shows "(Left v) :\<sqsubset>val (Left v')" |
239 shows "(Left v) :\<sqsubset>val (Left v')" |
499 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
514 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
500 apply(simp add: val_ord_def) |
515 apply(simp add: val_ord_def) |
501 apply(auto)[1] |
516 apply(auto)[1] |
502 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def) |
517 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def) |
503 |
518 |
|
519 lemma val_ord_irrefl: |
|
520 assumes "v :\<sqsubset>val v" |
|
521 shows "False" |
|
522 using assms |
|
523 by(auto simp add: val_ord_ex_def val_ord_def) |
|
524 |
|
525 lemma val_ord_almost_trichotomous: |
|
526 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
|
527 apply(auto simp add: val_ord_ex_def) |
|
528 apply(auto simp add: val_ord_def) |
|
529 apply(rule_tac x="[]" in exI) |
|
530 apply(auto simp add: Pos_empty pflat_len_simps) |
|
531 apply(drule_tac x="[]" in spec) |
|
532 apply(auto simp add: Pos_empty pflat_len_simps) |
|
533 done |
|
534 |
|
535 lemma WW1: |
|
536 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1" |
|
537 shows "False" |
|
538 using assms |
|
539 apply(auto simp add: val_ord_ex_def val_ord_def) |
|
540 using assms(1) assms(2) val_ord_irrefl val_ord_trans by blast |
|
541 |
|
542 lemma WW2: |
|
543 assumes "\<not>(v1 :\<sqsubset>val v2)" |
|
544 shows "v1 = v2 \<or> v2 :\<sqsubset>val v1" |
|
545 using assms |
|
546 oops |
|
547 |
|
548 lemma val_ord_SeqE2: |
|
549 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
|
550 shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')" |
|
551 using assms |
|
552 apply(frule_tac val_ord_SeqE) |
|
553 apply(erule disjE) |
|
554 apply(simp) |
|
555 apply(auto) |
|
556 apply(case_tac "v1 :\<sqsubset>val v1'") |
|
557 apply(simp) |
|
558 apply(auto simp add: val_ord_ex_def) |
|
559 apply(case_tac "v1 = v1'") |
|
560 apply(simp) |
|
561 oops |
504 |
562 |
505 section {* CPT and CPTpre *} |
563 section {* CPT and CPTpre *} |
506 |
564 |
507 |
565 |
508 inductive |
566 inductive |
519 lemma Prf_CPrf: |
577 lemma Prf_CPrf: |
520 assumes "\<Turnstile> v : r" |
578 assumes "\<Turnstile> v : r" |
521 shows "\<turnstile> v : r" |
579 shows "\<turnstile> v : r" |
522 using assms |
580 using assms |
523 by (induct) (auto intro: Prf.intros) |
581 by (induct) (auto intro: Prf.intros) |
|
582 |
|
583 lemma pflat_len_equal_iff: |
|
584 assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r" |
|
585 and "\<forall>p. pflat_len v1 p = pflat_len v2 p" |
|
586 shows "v1 = v2" |
|
587 using assms |
|
588 apply(induct v1 r arbitrary: v2 rule: CPrf.induct) |
|
589 apply(rotate_tac 4) |
|
590 apply(erule CPrf.cases) |
|
591 apply(simp_all)[7] |
|
592 apply (metis pflat_len_simps(1) pflat_len_simps(2)) |
|
593 apply(rotate_tac 2) |
|
594 apply(erule CPrf.cases) |
|
595 apply(simp_all)[7] |
|
596 apply (metis pflat_len_simps(3)) |
|
597 apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9)) |
|
598 apply(rotate_tac 2) |
|
599 apply(erule CPrf.cases) |
|
600 apply(simp_all)[7] |
|
601 apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9)) |
|
602 apply (metis pflat_len_simps(5)) |
|
603 apply(erule CPrf.cases) |
|
604 apply(simp_all)[7] |
|
605 apply(erule CPrf.cases) |
|
606 apply(simp_all)[7] |
|
607 apply(erule CPrf.cases) |
|
608 apply(simp_all)[7] |
|
609 apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv neq_Nil_conv not_less_iff_gr_or_eq pflat_len_simps(9)) |
|
610 apply(rotate_tac 5) |
|
611 apply(erule CPrf.cases) |
|
612 apply(simp_all)[7] |
|
613 apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv list.distinct(1) list.exhaust not_less_iff_gr_or_eq pflat_len_simps(9)) |
|
614 apply(auto) |
|
615 apply (metis pflat_len_simps(8)) |
|
616 apply(subgoal_tac "v = va") |
|
617 prefer 2 |
|
618 apply (metis pflat_len_simps(8)) |
|
619 apply(simp) |
|
620 apply(rotate_tac 3) |
|
621 apply(drule_tac x="Stars vsa" in meta_spec) |
|
622 apply(simp) |
|
623 apply(drule_tac meta_mp) |
|
624 apply(rule allI) |
|
625 apply(case_tac p) |
|
626 apply(simp add: pflat_len_simps) |
|
627 apply(drule_tac x="[]" in spec) |
|
628 apply(simp add: pflat_len_simps intlen_append) |
|
629 apply(drule_tac x="Suc a#list" in spec) |
|
630 apply(simp add: pflat_len_simps intlen_append) |
|
631 apply(simp) |
|
632 done |
|
633 |
|
634 lemma val_ord_trichotomous_stronger: |
|
635 assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r" |
|
636 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)" |
|
637 oops |
524 |
638 |
525 lemma CPrf_stars: |
639 lemma CPrf_stars: |
526 assumes "\<Turnstile> Stars vs : STAR r" |
640 assumes "\<Turnstile> Stars vs : STAR r" |
527 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
641 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
528 using assms |
642 using assms |