20 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}" |
20 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}" |
21 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}" |
21 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}" |
22 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" |
22 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" |
23 | "Pos (Stars []) = {[]}" |
23 | "Pos (Stars []) = {[]}" |
24 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}" |
24 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}" |
|
25 |
|
26 lemma Pos_stars: |
|
27 "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})" |
|
28 apply(induct vs) |
|
29 apply(simp) |
|
30 apply(simp) |
|
31 apply(simp add: insert_ident) |
|
32 apply(rule subset_antisym) |
|
33 apply(auto) |
|
34 apply(auto)[1] |
|
35 using less_Suc_eq_0_disj by auto |
|
36 |
|
37 |
25 |
38 |
26 lemma Pos_empty: |
39 lemma Pos_empty: |
27 shows "[] \<in> Pos v" |
40 shows "[] \<in> Pos v" |
28 by (induct v rule: Pos.induct)(auto) |
41 by (induct v rule: Pos.induct)(auto) |
29 |
42 |
103 shows "v1 = v2" |
116 shows "v1 = v2" |
104 using assms |
117 using assms |
105 apply(induct v1 arbitrary: r v2 rule: Pos.induct) |
118 apply(induct v1 arbitrary: r v2 rule: Pos.induct) |
106 (* ZERO *) |
119 (* ZERO *) |
107 apply(erule Prf.cases) |
120 apply(erule Prf.cases) |
108 apply(simp_all) |
121 apply(simp_all)[7] |
109 (* ONE *) |
122 (* ONE *) |
110 apply(erule Prf.cases) |
123 apply(erule Prf.cases) |
111 apply(simp_all) |
124 apply(simp_all)[7] |
112 (* CHAR *) |
125 (* CHAR *) |
113 apply(erule Prf.cases) |
126 apply(erule Prf.cases) |
114 apply(simp_all) |
127 apply(simp_all)[7] |
115 apply(erule Prf.cases) |
128 apply(erule Prf.cases) |
116 apply(simp_all) |
129 apply(simp_all)[7] |
117 (* ALT Left *) |
130 (* ALT Left *) |
118 apply(erule Prf.cases) |
131 apply(erule Prf.cases) |
119 apply(simp_all) |
132 apply(simp_all)[7] |
120 apply(erule Prf.cases) |
133 apply(erule Prf.cases) |
121 apply(simp_all) |
134 apply(simp_all)[7] |
122 apply(clarify) |
135 apply(clarify) |
123 apply(simp add: insert_ident) |
136 apply(simp add: insert_ident) |
124 apply(drule_tac x="r1a" in meta_spec) |
137 apply(drule_tac x="r1a" in meta_spec) |
125 apply(drule_tac x="v1a" in meta_spec) |
138 apply(drule_tac x="v1a" in meta_spec) |
126 apply(simp) |
139 apply(simp) |
130 (* ALT Right *) |
143 (* ALT Right *) |
131 apply(clarify) |
144 apply(clarify) |
132 apply(simp add: insert_ident) |
145 apply(simp add: insert_ident) |
133 using Pos_empty apply blast |
146 using Pos_empty apply blast |
134 apply(erule Prf.cases) |
147 apply(erule Prf.cases) |
135 apply(simp_all) |
148 apply(simp_all)[7] |
136 apply(erule Prf.cases) |
149 apply(erule Prf.cases) |
137 apply(simp_all) |
150 apply(simp_all)[7] |
138 apply(clarify) |
151 apply(clarify) |
139 apply(simp add: insert_ident) |
152 apply(simp add: insert_ident) |
140 using Pos_empty apply blast |
153 using Pos_empty apply blast |
141 apply(simp add: insert_ident) |
154 apply(simp add: insert_ident) |
142 apply(drule_tac x="r2a" in meta_spec) |
155 apply(drule_tac x="r2a" in meta_spec) |
144 apply(simp) |
157 apply(simp) |
145 apply(drule_tac meta_mp) |
158 apply(drule_tac meta_mp) |
146 apply(rule subset_antisym) |
159 apply(rule subset_antisym) |
147 apply(auto)[3] |
160 apply(auto)[3] |
148 apply(erule Prf.cases) |
161 apply(erule Prf.cases) |
149 apply(simp_all) |
162 apply(simp_all)[7] |
150 (* SEQ *) |
163 (* SEQ *) |
151 apply(erule Prf.cases) |
164 apply(erule Prf.cases) |
152 apply(simp_all) |
165 apply(simp_all)[7] |
153 apply(simp add: insert_ident) |
166 apply(simp add: insert_ident) |
154 apply(clarify) |
167 apply(clarify) |
155 apply(drule_tac x="r1a" in meta_spec) |
168 apply(drule_tac x="r1a" in meta_spec) |
156 apply(drule_tac x="r2a" in meta_spec) |
169 apply(drule_tac x="r2a" in meta_spec) |
157 apply(drule_tac x="v1b" in meta_spec) |
170 apply(drule_tac x="v1b" in meta_spec) |
177 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
190 apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0) |
178 apply(simp) |
191 apply(simp) |
179 apply(simp) |
192 apply(simp) |
180 (* STAR empty *) |
193 (* STAR empty *) |
181 apply(erule Prf.cases) |
194 apply(erule Prf.cases) |
182 apply(simp_all) |
195 apply(simp_all)[7] |
183 apply(erule Prf.cases) |
196 apply(erule Prf.cases) |
184 apply(simp_all) |
197 apply(simp_all)[7] |
185 apply(auto)[1] |
198 apply(auto)[1] |
186 using Pos_empty apply fastforce |
199 using Pos_empty apply fastforce |
187 (* STAR non-empty *) |
200 (* STAR non-empty *) |
188 apply(erule Prf.cases) |
201 apply(simp) |
189 apply(simp_all) |
202 apply(erule Prf.cases) |
190 apply(erule Prf.cases) |
203 apply(simp_all del: Pos.simps) |
191 apply(simp_all) |
204 apply(erule Prf.cases) |
|
205 apply(simp_all del: Pos.simps) |
|
206 apply(simp) |
192 apply(auto)[1] |
207 apply(auto)[1] |
193 using Pos_empty apply fastforce |
208 using Pos_empty apply fastforce |
194 apply(clarify) |
209 apply(clarify) |
|
210 apply(simp) |
195 apply(simp add: insert_ident) |
211 apply(simp add: insert_ident) |
196 apply(drule_tac x="rb" in meta_spec) |
212 apply(drule_tac x="rb" in meta_spec) |
197 apply(drule_tac x="STAR rb" in meta_spec) |
213 apply(drule_tac x="STAR rb" in meta_spec) |
198 apply(drule_tac x="vb" in meta_spec) |
214 apply(drule_tac x="vb" in meta_spec) |
199 apply(drule_tac x="Stars vsb" in meta_spec) |
215 apply(drule_tac x="Stars vsb" in meta_spec) |
429 apply(drule_tac x="Suc 0#q" in bspec) |
445 apply(drule_tac x="Suc 0#q" in bspec) |
430 apply(simp) |
446 apply(simp) |
431 apply(simp add: pflat_len_simps) |
447 apply(simp add: pflat_len_simps) |
432 done |
448 done |
433 |
449 |
434 |
450 lemma val_ord_StarsI: |
435 lemma val_ord_STARI: |
451 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
436 assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
452 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
437 shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" |
|
438 using assms(1) |
453 using assms(1) |
|
454 apply(subst (asm) val_ord_ex_def) |
439 apply(subst (asm) val_ord_def) |
455 apply(subst (asm) val_ord_def) |
440 apply(erule conjE) |
456 apply(clarify) |
|
457 apply(subst val_ord_ex_def) |
441 apply(subst val_ord_def) |
458 apply(subst val_ord_def) |
442 apply(rule conjI) |
459 apply(rule_tac x="0#p" in exI) |
443 apply(simp) |
460 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
444 apply(rule conjI) |
|
445 apply(subst pflat_len_Stars_simps) |
|
446 apply(simp) |
|
447 apply(subst pflat_len_Stars_simps) |
|
448 apply(simp) |
|
449 apply(simp) |
|
450 apply(rule ballI) |
|
451 apply(rule impI) |
|
452 apply(simp) |
|
453 apply(auto) |
|
454 apply(drule_tac x="[]" in bspec) |
|
455 apply(simp add: Pos_empty) |
|
456 using assms(2) |
461 using assms(2) |
457 apply(simp add: pflat_len_simps intlen_append) |
462 apply(simp add: pflat_len_simps intlen_append) |
458 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
463 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
459 done |
464 done |
460 |
465 |
461 lemma val_ord_STARI2: |
466 lemma val_ord_StarsI2: |
462 assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
467 assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
463 shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))" |
468 shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))" |
464 using assms(1) |
469 using assms(1) |
|
470 apply(subst (asm) val_ord_ex_def) |
465 apply(subst (asm) val_ord_def) |
471 apply(subst (asm) val_ord_def) |
466 apply(erule conjE)+ |
472 apply(clarify) |
|
473 apply(subst val_ord_ex_def) |
467 apply(subst val_ord_def) |
474 apply(subst val_ord_def) |
468 apply(rule conjI) |
475 apply(case_tac p) |
469 apply(simp) |
476 apply(simp add: pflat_len_simps) |
470 apply(rule conjI) |
477 apply(rule_tac x="[]" in exI) |
471 apply(case_tac vs1) |
478 apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append) |
472 apply(simp) |
479 apply(rule_tac x="Suc a#list" in exI) |
473 apply(simp) |
480 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
474 apply(auto)[1] |
|
475 apply(case_tac vs2) |
|
476 apply(simp) |
|
477 apply (simp add: pflat_len_def) |
|
478 apply(simp) |
|
479 apply(auto)[1] |
|
480 apply (simp add: pflat_len_Stars_simps) |
|
481 using pflat_len_def apply auto[1] |
|
482 apply(rule ballI) |
|
483 apply(rule impI) |
|
484 apply(simp) |
|
485 using assms(2) |
481 using assms(2) |
486 apply(auto) |
482 apply(simp add: pflat_len_simps intlen_append) |
487 apply (simp add: pflat_len_simps(9)) |
483 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
488 apply (simp add: pflat_len_Stars_simps) |
|
489 using assms(2) |
|
490 apply(auto simp add: pflat_len_def)[1] |
|
491 apply force |
|
492 apply force |
|
493 apply(auto simp add: pflat_len_def)[1] |
|
494 apply force |
|
495 apply force |
|
496 apply(auto simp add: pflat_len_def)[1] |
|
497 apply(auto simp add: pflat_len_def)[1] |
|
498 apply force |
|
499 apply force |
|
500 apply(auto simp add: pflat_len_def)[1] |
|
501 apply force |
|
502 apply force |
|
503 done |
484 done |
504 |
485 |
505 lemma val_ord_SeqI1: |
486 lemma val_ord_SeqI1: |
506 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
487 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
507 shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
488 shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
1093 apply(drule meta_mp) |
1074 apply(drule meta_mp) |
1094 apply(auto simp add: CPTpre_def)[1] |
1075 apply(auto simp add: CPTpre_def)[1] |
1095 apply (simp add: Posix1(2)) |
1076 apply (simp add: Posix1(2)) |
1096 apply (subst (asm) val_ord_ex1_def) |
1077 apply (subst (asm) val_ord_ex1_def) |
1097 apply(erule disjE) |
1078 apply(erule disjE) |
1098 apply (subst (asm) val_ord_ex_def) |
|
1099 apply(erule exE) |
|
1100 apply (subst val_ord_ex1_def) |
1079 apply (subst val_ord_ex1_def) |
1101 apply(rule disjI1) |
1080 apply(rule disjI1) |
1102 apply (subst val_ord_ex_def) |
1081 apply(rule val_ord_StarsI2) |
1103 apply(case_tac p) |
1082 apply(simp) |
1104 apply(simp) |
1083 using Posix1(2) apply force |
1105 apply (metis Posix1(2) append_eq_conv_conj flat_Stars not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_def) |
|
1106 |
|
1107 |
|
1108 |
|
1109 using Posix1(2) val_ord_STARI2 apply fastforce |
|
1110 apply(simp add: val_ord_ex1_def) |
1084 apply(simp add: val_ord_ex1_def) |
1111 apply (subst (asm) val_ord_ex_def) |
|
1112 apply(erule exE) |
|
1113 apply (subst val_ord_ex1_def) |
1085 apply (subst val_ord_ex1_def) |
1114 apply(rule disjI1) |
1086 apply(rule disjI1) |
1115 apply (subst val_ord_ex_def) |
1087 apply(rule val_ord_StarsI) |
1116 by (metis Posix1(2) flat.simps(7) flat_Stars val_ord_STARI) |
1088 apply(simp) |
|
1089 apply(simp add: Posix1) |
|
1090 using Posix1(2) by force |
|
1091 |
1117 |
1092 |
1118 lemma Posix_val_ord_stronger: |
1093 lemma Posix_val_ord_stronger: |
1119 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
1094 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
1120 shows "v1 :\<sqsubseteq>val v2" |
1095 shows "v1 :\<sqsubseteq>val v2" |
1121 using assms |
1096 using assms |
1285 apply(simp) |
1251 apply(simp) |
1286 apply(drule mp) |
1252 apply(drule mp) |
1287 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
1253 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
1288 apply(subst (asm) (2) val_ord_ex_def) |
1254 apply(subst (asm) (2) val_ord_ex_def) |
1289 apply(simp) |
1255 apply(simp) |
1290 apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def) |
1256 apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_ex_def) |
1291 apply(auto simp add: CPT_def PT_def)[1] |
1257 apply(auto simp add: CPT_def PT_def)[1] |
1292 using CPrf_stars apply auto[1] |
1258 using CPrf_stars apply auto[1] |
1293 apply(auto)[1] |
1259 apply(auto)[1] |
1294 apply(auto simp add: CPT_def PT_def)[1] |
1260 apply(auto simp add: CPT_def PT_def)[1] |
1295 apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r") |
1261 apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r") |
1325 apply(drule mp) |
1291 apply(drule mp) |
1326 apply (simp add: Posix1a Prf.intros(7)) |
1292 apply (simp add: Posix1a Prf.intros(7)) |
1327 apply(simp) |
1293 apply(simp) |
1328 apply(subst (asm) (2) val_ord_ex_def) |
1294 apply(subst (asm) (2) val_ord_ex_def) |
1329 apply(simp) |
1295 apply(simp) |
1330 apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def) |
1296 apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_ex_def) |
1331 proof - |
1297 proof - |
1332 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
1298 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
1333 assume a1: "s\<^sub>3 \<noteq> []" |
1299 assume a1: "s\<^sub>3 \<noteq> []" |
1334 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
1300 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
1335 assume a3: "flat vA = flat a @ s\<^sub>3" |
1301 assume a3: "flat vA = flat a @ s\<^sub>3" |
1339 have f6: "\<not> length (flat vA) \<le> length (flat a)" |
1305 have f6: "\<not> length (flat vA) \<le> length (flat a)" |
1340 using a3 a1 by simp |
1306 using a3 a1 by simp |
1341 have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
1307 have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
1342 using a3 a2 by simp |
1308 using a3 a2 by simp |
1343 then show False |
1309 then show False |
1344 using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_STARI val_ord_ex_def val_ord_shorterI) |
1310 using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_StarsI val_ord_ex_def val_ord_shorterI) |
1345 qed |
1311 qed |
1346 |
1312 |
1347 lemma Prf_Stars_append: |
1313 lemma Prf_Stars_append: |
1348 assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r" |
1314 assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r" |
1349 shows "\<turnstile> Stars (vs1 @ vs2) : STAR r" |
1315 shows "\<turnstile> Stars (vs1 @ vs2) : STAR r" |
1506 apply(auto)[1] |
1472 apply(auto)[1] |
1507 apply(drule_tac x="Stars (v2#vs)" in spec) |
1473 apply(drule_tac x="Stars (v2#vs)" in spec) |
1508 apply(simp) |
1474 apply(simp) |
1509 apply(drule mp) |
1475 apply(drule mp) |
1510 using Prf.intros(7) Prf_CPrf apply blast |
1476 using Prf.intros(7) Prf_CPrf apply blast |
1511 apply(subst (asm) (2) val_ord_ex_def) |
1477 apply(simp add: val_ord_StarsI) |
1512 apply(simp) |
|
1513 using val_ord_STARI val_ord_ex_def apply fastforce |
|
1514 apply(assumption) |
1478 apply(assumption) |
1515 apply(drule_tac x="flat va" in meta_spec) |
1479 apply(drule_tac x="flat va" in meta_spec) |
1516 apply(drule_tac x="va" in meta_spec) |
1480 apply(drule_tac x="va" in meta_spec) |
1517 apply(simp) |
1481 apply(simp) |
1518 apply(drule meta_mp) |
1482 apply(drule meta_mp) |