equal
deleted
inserted
replaced
44 fun intlen :: "'a list \<Rightarrow> int" |
44 fun intlen :: "'a list \<Rightarrow> int" |
45 where |
45 where |
46 "intlen [] = 0" |
46 "intlen [] = 0" |
47 | "intlen (x#xs) = 1 + intlen xs" |
47 | "intlen (x#xs) = 1 + intlen xs" |
48 |
48 |
49 lemma inlen_bigger: |
49 lemma intlen_bigger: |
50 shows "0 \<le> intlen xs" |
50 shows "0 \<le> intlen xs" |
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" |
60 using assms |
60 using assms |
61 apply(induct xs arbitrary: ys) |
61 apply(induct xs arbitrary: ys) |
62 apply(auto) |
62 apply(auto) |
63 apply(case_tac ys) |
63 apply(case_tac ys) |
64 apply(simp_all) |
64 apply(simp_all) |
65 apply (smt inlen_bigger) |
65 apply (smt intlen_bigger) |
66 by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
66 by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
|
67 |
|
68 lemma length_intlen: |
|
69 assumes "intlen xs < intlen ys" |
|
70 shows "length xs < length ys" |
|
71 using assms |
|
72 apply(induct xs arbitrary: ys) |
|
73 apply(auto) |
|
74 apply(case_tac ys) |
|
75 apply(simp_all) |
|
76 by (smt intlen_bigger) |
67 |
77 |
68 |
78 |
69 definition pflat_len :: "val \<Rightarrow> nat list => int" |
79 definition pflat_len :: "val \<Rightarrow> nat list => int" |
70 where |
80 where |
71 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
81 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
176 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
186 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
177 |
187 |
178 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
188 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
179 where |
189 where |
180 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
190 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
|
191 |
|
192 lemma val_ord_shorterE: |
|
193 assumes "v1 :\<sqsubset>val v2" |
|
194 shows "length (flat v2) \<le> length (flat v1)" |
|
195 using assms |
|
196 apply(auto simp add: val_ord_ex_def val_ord_def) |
|
197 apply(case_tac p) |
|
198 apply(simp add: pflat_len_simps) |
|
199 apply(drule length_intlen) |
|
200 apply(simp) |
|
201 apply(drule_tac x="[]" in bspec) |
|
202 apply(simp add: Pos_empty) |
|
203 apply(simp add: pflat_len_simps) |
|
204 by (metis intlen_length le_less less_irrefl linear) |
|
205 |
181 |
206 |
182 lemma val_ord_shorterI: |
207 lemma val_ord_shorterI: |
183 assumes "length (flat v') < length (flat v)" |
208 assumes "length (flat v') < length (flat v)" |
184 shows "v :\<sqsubset>val v'" |
209 shows "v :\<sqsubset>val v'" |
185 using assms |
210 using assms |
472 apply(simp add: val_ord_def) |
497 apply(simp add: val_ord_def) |
473 apply(auto)[1] |
498 apply(auto)[1] |
474 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
499 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
475 apply(simp add: val_ord_def) |
500 apply(simp add: val_ord_def) |
476 apply(auto)[1] |
501 apply(auto)[1] |
477 by (smt inlen_bigger lex_trans outside_lemma pflat_len_def) |
502 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def) |
478 |
503 |
479 |
504 |
480 section {* CPT and CPTpre *} |
505 section {* CPT and CPTpre *} |
481 |
506 |
482 |
507 |
814 apply(subst val_ord_def) |
839 apply(subst val_ord_def) |
815 apply(rule conjI) |
840 apply(rule conjI) |
816 apply(simp add: Pos_empty) |
841 apply(simp add: Pos_empty) |
817 apply(rule conjI) |
842 apply(rule conjI) |
818 apply(simp add: pflat_len_simps) |
843 apply(simp add: pflat_len_simps) |
819 apply (smt inlen_bigger) |
844 apply (smt intlen_bigger) |
820 apply(simp) |
845 apply(simp) |
821 apply(rule conjI) |
846 apply(rule conjI) |
822 apply(simp add: pflat_len_simps) |
847 apply(simp add: pflat_len_simps) |
823 using Posix1(2) apply auto[1] |
848 using Posix1(2) apply auto[1] |
824 apply(rule ballI) |
849 apply(rule ballI) |
1091 apply(simp) |
1116 apply(simp) |
1092 apply(simp add: pflat_len_simps) |
1117 apply(simp add: pflat_len_simps) |
1093 apply(drule_tac x="[0]" in spec) |
1118 apply(drule_tac x="[0]" in spec) |
1094 apply(simp add: pflat_len_simps Pos_empty) |
1119 apply(simp add: pflat_len_simps Pos_empty) |
1095 apply(drule mp) |
1120 apply(drule mp) |
1096 apply (smt inlen_bigger) |
1121 apply (smt intlen_bigger) |
1097 apply(erule disjE) |
1122 apply(erule disjE) |
1098 apply blast |
1123 apply blast |
1099 apply auto[1] |
1124 apply auto[1] |
1100 apply (meson L_flat_Prf2) |
1125 apply (meson L_flat_Prf2) |
1101 (* SEQ *) |
1126 (* SEQ *) |