equal
deleted
inserted
replaced
392 apply(auto) |
392 apply(auto) |
393 apply(case_tac q) |
393 apply(case_tac q) |
394 apply(auto) |
394 apply(auto) |
395 done |
395 done |
396 |
396 |
|
397 (* |
397 definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" |
398 definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" |
398 where |
399 where |
399 "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)" |
400 "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)" |
400 |
401 *) |
401 definition |
|
402 "DPos v1 v2 \<equiv> {p. dpos v1 v2 p}" |
|
403 |
402 |
404 lemma outside_lemma: |
403 lemma outside_lemma: |
405 assumes "p \<notin> Pos v1 \<union> Pos v2" |
404 assumes "p \<notin> Pos v1 \<union> Pos v2" |
406 shows "pflat_len v1 p = pflat_len v2 p" |
405 shows "pflat_len v1 p = pflat_len v2 p" |
407 using assms |
406 using assms |
408 apply(auto simp add: pflat_len_def) |
407 apply(auto simp add: pflat_len_def) |
409 done |
408 done |
410 |
409 |
|
410 (* |
411 lemma dpos_lemma_aux: |
411 lemma dpos_lemma_aux: |
412 assumes "p \<in> Pos v1 \<union> Pos v2" |
412 assumes "p \<in> Pos v1 \<union> Pos v2" |
413 and "pflat_len v1 p = pflat_len v2 p" |
413 and "pflat_len v1 p = pflat_len v2 p" |
414 shows "p \<in> Pos v1 \<inter> Pos v2" |
414 shows "p \<in> Pos v1 \<inter> Pos v2" |
415 using assms |
415 using assms |
432 assumes "p \<in> Pos v1 \<union> Pos v2" |
432 assumes "p \<in> Pos v1 \<union> Pos v2" |
433 and "dpos v1 v2 p" |
433 and "dpos v1 v2 p" |
434 shows "pflat_len v1 p \<noteq> pflat_len v2 p" |
434 shows "pflat_len v1 p \<noteq> pflat_len v2 p" |
435 using assms |
435 using assms |
436 using dpos_lemma by blast |
436 using dpos_lemma by blast |
437 |
437 *) |
438 lemma DPos_lemma: |
|
439 assumes "p \<in> DPos v1 v2" |
|
440 shows "pflat_len v1 p \<noteq> pflat_len v2 p" |
|
441 using assms |
|
442 unfolding DPos_def |
|
443 apply(auto simp add: pflat_len_def dpos_def) |
|
444 apply (smt inlen_bigger) |
|
445 by (smt inlen_bigger) |
|
446 |
|
447 |
438 |
448 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _") |
439 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _") |
449 where |
440 where |
450 "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and> |
441 "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and> |
451 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))" |
442 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))" |
802 apply(simp add: val_ord_def) |
793 apply(simp add: val_ord_def) |
803 apply(auto)[1] |
794 apply(auto)[1] |
804 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma) |
795 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma) |
805 |
796 |
806 |
797 |
807 definition fdpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" |
|
808 where |
|
809 "fdpos v1 v2 p \<equiv> ({q. q \<sqsubset>lex p} \<inter> DPos v1 v2 = {})" |
|
810 |
|
811 |
|
812 lemma pos_append: |
|
813 assumes "p @ q \<in> Pos v" |
|
814 shows "q \<in> Pos (at v p)" |
|
815 using assms |
|
816 apply(induct arbitrary: p q rule: Pos.induct) |
|
817 apply(simp_all) |
|
818 apply(auto)[1] |
|
819 apply(simp add: append_eq_Cons_conv) |
|
820 apply(auto)[1] |
|
821 apply(auto)[1] |
|
822 apply(simp add: append_eq_Cons_conv) |
|
823 apply(auto)[1] |
|
824 apply(auto)[1] |
|
825 apply(simp add: append_eq_Cons_conv) |
|
826 apply(auto)[1] |
|
827 apply(simp add: append_eq_Cons_conv) |
|
828 apply(auto)[1] |
|
829 apply(auto)[1] |
|
830 apply(simp add: append_eq_Cons_conv) |
|
831 apply(auto)[1] |
|
832 apply(simp add: append_eq_Cons_conv) |
|
833 apply(auto)[1] |
|
834 by (metis append_Cons at.simps(6)) |
|
835 |
|
836 |
|
837 lemma Pos_pre: |
798 lemma Pos_pre: |
838 assumes "p \<in> Pos v" "q \<sqsubseteq>pre p" |
799 assumes "p \<in> Pos v" "q \<sqsubseteq>pre p" |
839 shows "q \<in> Pos v" |
800 shows "q \<in> Pos v" |
840 using assms |
801 using assms |
841 apply(induct v arbitrary: p q rule: Pos.induct) |
802 apply(induct v arbitrary: p q rule: Pos.induct) |
989 apply(simp add: CPTpre_simps) |
950 apply(simp add: CPTpre_simps) |
990 apply(auto simp add: CPTpre_def) |
951 apply(auto simp add: CPTpre_def) |
991 apply (simp add: prefix_list_def) |
952 apply (simp add: prefix_list_def) |
992 by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5)) |
953 by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5)) |
993 |
954 |
994 lemma Cond_prefix: |
955 term "{vs. Stars vs \<in> A}" |
995 assumes "\<forall>s\<^sub>3. s1 @ s\<^sub>3 \<in> L r1 \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s1 @ s\<^sub>3 @ s\<^sub>4 \<sqsubseteq>pre s1 @ s2 \<longrightarrow> s\<^sub>4 \<notin> L r2)" |
|
996 and "t1 \<in> L r1" "t2 \<in> L r2" "t1 @ t2 \<sqsubseteq>pre s1 @ s2" |
|
997 shows "t1 \<sqsubseteq>pre s1" |
|
998 using assms |
|
999 apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2) |
|
1000 done |
|
1001 |
|
1002 |
|
1003 |
956 |
1004 lemma test: |
957 lemma test: |
1005 assumes "finite A" |
958 assumes "finite A" |
1006 shows "finite {vs. Stars vs \<in> A}" |
959 shows "finite {vs. Stars vs \<in> A}" |
1007 using assms |
960 using assms |
1047 apply(rule finite_subset) |
1000 apply(rule finite_subset) |
1048 apply(rule CPTpre_subsets) |
1001 apply(rule CPTpre_subsets) |
1049 apply(simp) |
1002 apply(simp) |
1050 apply(rule finite_subset) |
1003 apply(rule finite_subset) |
1051 apply(rule CPTpre_subsets) |
1004 apply(rule CPTpre_subsets) |
1052 thm finite_subset |
|
1053 apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset) |
1005 apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset) |
1054 apply(auto)[1] |
1006 apply(auto)[1] |
1055 apply(rule finite_imageI) |
1007 apply(rule finite_imageI) |
1056 apply(simp add: Collect_case_prod_Sigma) |
1008 apply(simp add: Collect_case_prod_Sigma) |
1057 apply(rule finite_subset) |
1009 apply(rule finite_subset) |