55 by (induct xs arbitrary: ys) (auto) |
55 by (induct xs arbitrary: ys) (auto) |
56 |
56 |
57 lemma intlen_length: |
57 lemma intlen_length: |
58 shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys" |
58 shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys" |
59 apply(induct xs arbitrary: ys) |
59 apply(induct xs arbitrary: ys) |
60 apply(auto) |
60 apply (auto simp add: intlen_bigger not_less) |
61 apply(case_tac ys) |
61 apply (metis intlen.elims intlen_bigger le_imp_0_less) |
62 apply(simp_all) |
62 apply (smt Suc_lessI intlen.simps(2) length_Suc_conv nat_neq_iff) |
63 apply (smt intlen_bigger) |
|
64 apply (smt Suc_mono intlen.simps(2) length_Suc_conv less_antisym) |
|
65 by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
63 by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
66 |
|
67 |
64 |
68 |
65 |
69 definition pflat_len :: "val \<Rightarrow> nat list => int" |
66 definition pflat_len :: "val \<Rightarrow> nat list => int" |
70 where |
67 where |
71 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
68 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
118 assumes "ps1 \<sqsubset>lex ps2" |
115 assumes "ps1 \<sqsubset>lex ps2" |
119 shows "ps1 \<noteq> ps2" |
116 shows "ps1 \<noteq> ps2" |
120 using assms |
117 using assms |
121 by(induct rule: lex_list.induct)(auto) |
118 by(induct rule: lex_list.induct)(auto) |
122 |
119 |
123 |
|
124 lemma lex_simps [simp]: |
120 lemma lex_simps [simp]: |
125 fixes xs ys :: "nat list" |
121 fixes xs ys :: "nat list" |
126 shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []" |
122 shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []" |
127 and "xs \<sqsubset>lex [] \<longleftrightarrow> False" |
123 and "xs \<sqsubset>lex [] \<longleftrightarrow> False" |
128 and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))" |
124 and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))" |
129 apply - |
125 apply(auto elim: lex_list.cases intro: lex_list.intros) |
130 apply (metis lex_irrfl lex_list.intros(1) list.exhaust) |
126 apply(auto simp add: neq_Nil_conv not_less_iff_gr_or_eq intro: lex_list.intros) |
131 using lex_list.cases apply blast |
127 done |
132 using lex_list.cases lex_list.intros(2) lex_list.intros(3) not_less_iff_gr_or_eq by fastforce |
|
133 |
|
134 |
128 |
135 lemma lex_trans: |
129 lemma lex_trans: |
136 fixes ps1 ps2 ps3 :: "nat list" |
130 fixes ps1 ps2 ps3 :: "nat list" |
137 assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3" |
131 assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3" |
138 shows "ps1 \<sqsubset>lex ps3" |
132 shows "ps1 \<sqsubset>lex ps3" |
139 using assms |
133 using assms |
140 apply(induct arbitrary: ps3 rule: lex_list.induct) |
134 by (induct arbitrary: ps3 rule: lex_list.induct) |
141 apply(erule lex_list.cases) |
135 (auto elim: lex_list.cases) |
142 apply(simp_all) |
136 |
143 apply(rotate_tac 2) |
|
144 apply(erule lex_list.cases) |
|
145 apply(simp_all) |
|
146 apply(erule lex_list.cases) |
|
147 apply(simp_all) |
|
148 done |
|
149 |
137 |
150 lemma lex_trichotomous: |
138 lemma lex_trichotomous: |
151 fixes p q :: "nat list" |
139 fixes p q :: "nat list" |
152 shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p" |
140 shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p" |
153 apply(induct p arbitrary: q) |
141 apply(induct p arbitrary: q) |
162 section {* Ordering of values according to Okui & Suzuki *} |
150 section {* Ordering of values according to Okui & Suzuki *} |
163 |
151 |
164 |
152 |
165 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
153 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
166 where |
154 where |
167 "v1 \<sqsubset>val p v2 \<equiv> p \<in> Pos v1 \<and> |
155 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
|
156 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
|
157 |
|
158 definition PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60) |
|
159 where |
|
160 "v1 \<sqsubset>val2 p v2 \<equiv> p \<in> Pos v1 \<and> |
168 pflat_len v1 p > pflat_len v2 p \<and> |
161 pflat_len v1 p > pflat_len v2 p \<and> |
169 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
162 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
|
163 |
|
164 lemma XXX: |
|
165 "v1 \<sqsubset>val p v2 \<longleftrightarrow> v1 \<sqsubset>val2 p v2" |
|
166 apply(auto simp add: PosOrd_def PosOrd2_def) |
|
167 apply(auto simp add: pflat_len_def split: if_splits) |
|
168 by (smt intlen_bigger) |
|
169 |
|
170 |
|
171 (* some tests *) |
170 |
172 |
171 definition ValFlat_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>fval _ _") |
173 definition ValFlat_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>fval _ _") |
172 where |
174 where |
173 "v1 \<sqsubset>fval p v2 \<equiv> p \<in> Pos v1 \<and> |
175 "v1 \<sqsubset>fval p v2 \<equiv> p \<in> Pos v1 \<and> |
174 (p \<notin> Pos v2 \<or> flat (at v2 p) \<sqsubset>spre flat (at v1 p)) \<and> |
176 (p \<notin> Pos v2 \<or> flat (at v2 p) \<sqsubset>spre flat (at v1 p)) \<and> |
195 assumes "v1 \<sqsubset>val p v2" "flat (at v2 p) \<sqsubset>spre flat (at v1 p)" |
197 assumes "v1 \<sqsubset>val p v2" "flat (at v2 p) \<sqsubset>spre flat (at v1 p)" |
196 shows "v1 \<sqsubset>fval p v2" |
198 shows "v1 \<sqsubset>fval p v2" |
197 using assms |
199 using assms |
198 unfolding ValFlat_ord_def PosOrd_def |
200 unfolding ValFlat_ord_def PosOrd_def |
199 apply(clarify) |
201 apply(clarify) |
200 done |
202 oops |
201 |
203 |
202 |
204 |
203 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60) |
205 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60) |
204 where |
206 where |
205 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
207 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
226 lemma PosOrd_shorterI: |
228 lemma PosOrd_shorterI: |
227 assumes "length (flat v') < length (flat v)" |
229 assumes "length (flat v') < length (flat v)" |
228 shows "v :\<sqsubset>val v'" |
230 shows "v :\<sqsubset>val v'" |
229 using assms |
231 using assms |
230 unfolding PosOrd_ex_def |
232 unfolding PosOrd_ex_def |
231 by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def) |
233 by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def) |
232 |
234 |
233 lemma PosOrd_spreI: |
235 lemma PosOrd_spreI: |
234 assumes "(flat v') \<sqsubset>spre (flat v)" |
236 assumes "(flat v') \<sqsubset>spre (flat v)" |
235 shows "v :\<sqsubset>val v'" |
237 shows "v :\<sqsubset>val v'" |
236 using assms |
238 using assms |
241 assumes "flat v1 = flat v2" |
243 assumes "flat v1 = flat v2" |
242 shows "Left v1 :\<sqsubset>val Right v2" |
244 shows "Left v1 :\<sqsubset>val Right v2" |
243 unfolding PosOrd_ex_def |
245 unfolding PosOrd_ex_def |
244 apply(rule_tac x="[0]" in exI) |
246 apply(rule_tac x="[0]" in exI) |
245 using assms |
247 using assms |
246 apply(auto simp add: PosOrd_def pflat_len_simps Pos_empty) |
248 apply(auto simp add: PosOrd_def pflat_len_simps) |
247 apply(smt intlen_bigger) |
249 apply(smt intlen_bigger) |
248 done |
250 done |
249 |
251 |
250 lemma PosOrd_LeftI: |
252 lemma PosOrd_LeftI: |
251 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
253 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
273 assumes "(Left v1) :\<sqsubset>val (Left v2)" |
275 assumes "(Left v1) :\<sqsubset>val (Left v2)" |
274 shows "v1 :\<sqsubset>val v2" |
276 shows "v1 :\<sqsubset>val v2" |
275 using assms |
277 using assms |
276 apply(simp add: PosOrd_ex_def) |
278 apply(simp add: PosOrd_ex_def) |
277 apply(erule exE) |
279 apply(erule exE) |
278 apply(case_tac "p = []") |
280 apply(case_tac p) |
279 apply(simp add: PosOrd_def) |
281 apply(simp add: PosOrd_def) |
280 apply(auto simp add: pflat_len_simps) |
282 apply(auto simp add: pflat_len_simps) |
281 apply(rule_tac x="[]" in exI) |
283 apply(rule_tac x="[]" in exI) |
282 apply(simp add: Pos_empty pflat_len_simps) |
284 apply(simp add: Pos_empty pflat_len_simps) |
283 apply(auto simp add: pflat_len_simps PosOrd_def) |
285 apply(auto simp add: pflat_len_simps PosOrd_def) |
284 apply(rule_tac x="ps" in exI) |
286 apply(case_tac a) |
|
287 apply(auto simp add: pflat_len_simps)[1] |
|
288 apply(rule_tac x="list" in exI) |
285 apply(auto) |
289 apply(auto) |
286 apply(drule_tac x="0#q" in bspec) |
290 apply(drule_tac x="0#q" in bspec) |
287 apply(simp) |
291 apply(simp) |
288 apply(simp add: pflat_len_simps) |
292 apply(simp add: pflat_len_simps) |
289 apply(drule_tac x="0#q" in bspec) |
293 apply(drule_tac x="0#q" in bspec) |
290 apply(simp) |
294 apply(simp) |
291 apply(simp add: pflat_len_simps) |
295 apply(simp add: pflat_len_simps) |
|
296 apply(simp add: pflat_len_def) |
292 done |
297 done |
293 |
298 |
294 lemma PosOrd_RightE: |
299 lemma PosOrd_RightE: |
295 assumes "(Right v1) :\<sqsubset>val (Right v2)" |
300 assumes "(Right v1) :\<sqsubset>val (Right v2)" |
296 shows "v1 :\<sqsubset>val v2" |
301 shows "v1 :\<sqsubset>val v2" |
297 using assms |
302 using assms |
298 apply(simp add: PosOrd_ex_def) |
303 apply(simp add: PosOrd_ex_def) |
299 apply(erule exE) |
304 apply(erule exE) |
300 apply(case_tac "p = []") |
305 apply(case_tac p) |
301 apply(simp add: PosOrd_def) |
306 apply(simp add: PosOrd_def) |
302 apply(auto simp add: pflat_len_simps) |
307 apply(auto simp add: pflat_len_simps) |
303 apply(rule_tac x="[]" in exI) |
308 apply(rule_tac x="[]" in exI) |
304 apply(simp add: Pos_empty pflat_len_simps) |
309 apply(simp add: Pos_empty pflat_len_simps) |
|
310 apply(case_tac a) |
|
311 apply(simp add: pflat_len_def PosOrd_def) |
|
312 apply(case_tac nat) |
|
313 prefer 2 |
|
314 apply(simp add: pflat_len_def PosOrd_def) |
305 apply(auto simp add: pflat_len_simps PosOrd_def) |
315 apply(auto simp add: pflat_len_simps PosOrd_def) |
306 apply(rule_tac x="ps" in exI) |
316 apply(rule_tac x="list" in exI) |
307 apply(auto) |
317 apply(auto) |
308 apply(drule_tac x="Suc 0#q" in bspec) |
318 apply(drule_tac x="Suc 0#q" in bspec) |
309 apply(simp) |
319 apply(simp) |
310 apply(simp add: pflat_len_simps) |
320 apply(simp add: pflat_len_simps) |
311 apply(drule_tac x="Suc 0#q" in bspec) |
321 apply(drule_tac x="Suc 0#q" in bspec) |
346 apply(subst (asm) PosOrd_def) |
354 apply(subst (asm) PosOrd_def) |
347 apply(clarify) |
355 apply(clarify) |
348 apply(subst PosOrd_ex_def) |
356 apply(subst PosOrd_ex_def) |
349 apply(rule_tac x="Suc 0#p" in exI) |
357 apply(rule_tac x="Suc 0#p" in exI) |
350 apply(subst PosOrd_def) |
358 apply(subst PosOrd_def) |
351 apply(rule conjI) |
|
352 apply(simp) |
|
353 apply(rule conjI) |
359 apply(rule conjI) |
354 apply(simp add: pflat_len_simps) |
360 apply(simp add: pflat_len_simps) |
355 apply(rule ballI) |
361 apply(rule ballI) |
356 apply(rule impI) |
362 apply(rule impI) |
357 apply(simp only: Pos.simps) |
363 apply(simp only: Pos.simps) |
391 apply(auto simp add: pflat_len_simps intlen_append) |
397 apply(auto simp add: pflat_len_simps intlen_append) |
392 apply(rule_tac x="list" in exI) |
398 apply(rule_tac x="list" in exI) |
393 apply(simp add: Pos_empty) |
399 apply(simp add: Pos_empty) |
394 apply(rule ballI) |
400 apply(rule ballI) |
395 apply(rule impI) |
401 apply(rule impI) |
|
402 apply(auto)[1] |
396 apply(drule_tac x="Suc 0#q" in bspec) |
403 apply(drule_tac x="Suc 0#q" in bspec) |
397 apply(simp) |
404 apply(simp) |
398 apply(simp add: pflat_len_simps) |
405 apply(simp add: pflat_len_simps) |
399 apply(simp add: PosOrd_def) |
406 apply(drule_tac x="Suc 0#q" in bspec) |
|
407 apply(simp) |
|
408 apply(simp add: pflat_len_simps) |
|
409 apply(simp add: PosOrd_def pflat_len_def) |
400 done |
410 done |
401 |
411 |
402 lemma PosOrd_StarsI: |
412 lemma PosOrd_StarsI: |
403 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
413 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
404 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
414 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
457 apply(rule_tac x="[]" in exI) |
467 apply(rule_tac x="[]" in exI) |
458 apply(simp add: PosOrd_def pflat_len_simps Pos_empty) |
468 apply(simp add: PosOrd_def pflat_len_simps Pos_empty) |
459 apply(simp) |
469 apply(simp) |
460 apply(case_tac a) |
470 apply(case_tac a) |
461 apply(clarify) |
471 apply(clarify) |
462 apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def)[1] |
472 apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1] |
463 apply(clarify) |
473 apply(clarify) |
464 apply(simp add: PosOrd_ex_def) |
474 apply(simp add: PosOrd_ex_def) |
465 apply(rule_tac x="nat#list" in exI) |
475 apply(rule_tac x="nat#list" in exI) |
466 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1] |
476 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1] |
467 apply(case_tac q) |
477 apply(case_tac q) |
495 apply(erule PosOrd_Stars_appendE) |
505 apply(erule PosOrd_Stars_appendE) |
496 apply(rule PosOrd_Stars_appendI) |
506 apply(rule PosOrd_Stars_appendI) |
497 apply(auto) |
507 apply(auto) |
498 done |
508 done |
499 |
509 |
500 |
|
501 lemma PosOrd_trans: |
510 lemma PosOrd_trans: |
502 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
511 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
503 shows "v1 :\<sqsubset>val v3" |
512 shows "v1 :\<sqsubset>val v3" |
504 using assms |
513 proof - |
505 unfolding PosOrd_ex_def |
514 from assms obtain p p' |
506 apply(clarify) |
515 where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast |
507 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p") |
516 have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p" |
508 prefer 2 |
517 by (rule lex_trichotomous) |
509 apply(rule lex_trichotomous) |
518 moreover |
510 apply(erule disjE) |
519 { assume "p = p'" |
511 apply(simp) |
520 with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def |
512 apply(rule_tac x="pa" in exI) |
521 by (smt outside_lemma) |
513 apply(subst PosOrd_def) |
522 then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
514 apply(rule conjI) |
523 } |
515 apply(simp add: PosOrd_def) |
524 moreover |
516 apply(auto)[1] |
525 { assume "p \<sqsubset>lex p'" |
517 apply(simp add: PosOrd_def) |
526 with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def |
518 apply(simp add: PosOrd_def) |
527 by (metis lex_trans outside_lemma) |
519 apply(auto)[1] |
528 then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
520 using outside_lemma apply blast |
529 } |
521 apply(simp add: PosOrd_def) |
530 moreover |
522 apply(auto)[1] |
531 { assume "p' \<sqsubset>lex p" |
523 using outside_lemma apply force |
532 with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def |
524 apply auto[1] |
533 by (smt Un_iff intlen_bigger lex_trans pflat_len_def) |
525 apply(simp add: PosOrd_def) |
534 then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
526 apply(auto)[1] |
535 } |
527 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
536 ultimately show "v1 :\<sqsubset>val v3" by blast |
528 apply(simp add: PosOrd_def) |
537 qed |
529 apply(auto)[1] |
538 |
530 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def) |
|
531 |
539 |
532 lemma PosOrd_irrefl: |
540 lemma PosOrd_irrefl: |
533 assumes "v :\<sqsubset>val v" |
541 assumes "v :\<sqsubset>val v" |
534 shows "False" |
542 shows "False" |
535 using assms |
543 using assms unfolding PosOrd_ex_def PosOrd_def |
536 by(auto simp add: PosOrd_ex_def PosOrd_def) |
544 by auto |
537 |
545 |
538 lemma PosOrd_almost_trichotomous: |
546 lemma PosOrd_almost_trichotomous: |
539 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
547 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
540 apply(auto simp add: PosOrd_ex_def) |
548 apply(auto simp add: PosOrd_ex_def) |
541 apply(auto simp add: PosOrd_def) |
549 apply(auto simp add: PosOrd_def) |
840 |
848 |
841 lemma Posix_CPT: |
849 lemma Posix_CPT: |
842 assumes "s \<in> r \<rightarrow> v" |
850 assumes "s \<in> r \<rightarrow> v" |
843 shows "v \<in> CPT r s" |
851 shows "v \<in> CPT r s" |
844 using assms |
852 using assms |
845 apply(induct rule: Posix.induct) |
853 by (induct rule: Posix.induct) |
846 apply(simp add: CPT_def) |
854 (auto simp add: CPT_def intro: CPrf.intros) |
847 apply(rule CPrf.intros) |
|
848 apply(simp add: CPT_def) |
|
849 apply(rule CPrf.intros) |
|
850 apply(simp add: CPT_def) |
|
851 apply(rule CPrf.intros) |
|
852 apply(simp) |
|
853 apply(simp add: CPT_def) |
|
854 apply(rule CPrf.intros) |
|
855 apply(simp) |
|
856 apply(simp add: CPT_def) |
|
857 apply(rule CPrf.intros) |
|
858 apply(simp) |
|
859 apply(simp) |
|
860 apply(simp add: CPT_def) |
|
861 apply(rule CPrf.intros) |
|
862 apply(simp) |
|
863 apply(simp) |
|
864 apply(simp) |
|
865 apply(simp add: CPT_def) |
|
866 apply(rule CPrf.intros) |
|
867 done |
|
868 |
855 |
869 section {* The Posix Value is smaller than any other Value *} |
856 section {* The Posix Value is smaller than any other Value *} |
870 |
857 |
871 |
858 |
872 lemma Posix_PosOrd: |
859 lemma Posix_PosOrd: |
952 by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf) |
939 by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf) |
953 then show "Right v :\<sqsubseteq>val v2" by simp |
940 then show "Right v :\<sqsubseteq>val v2" by simp |
954 qed |
941 qed |
955 next |
942 next |
956 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
943 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
957 have as1: "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
944 have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
|
945 then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2)) |
958 have IH1: "\<And>v3. v3 \<in> CPT r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
946 have IH1: "\<And>v3. v3 \<in> CPT r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
959 have IH2: "\<And>v3. v3 \<in> CPT r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
947 have IH2: "\<And>v3. v3 \<in> CPT r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
960 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact |
948 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact |
961 have "v3 \<in> CPT (SEQ r1 r2) (s1 @ s2)" by fact |
949 have "v3 \<in> CPT (SEQ r1 r2) (s1 @ s2)" by fact |
962 then obtain v3a v3b where eqs: |
950 then obtain v3a v3b where eqs: |
966 with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def |
954 with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def |
967 by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv) |
955 by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv) |
968 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs |
956 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs |
969 by (simp add: sprefix_list_def append_eq_conv_conj) |
957 by (simp add: sprefix_list_def append_eq_conv_conj) |
970 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
958 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
971 using PosOrd_spreI Posix1(2) as1(1) eqs by blast |
959 using PosOrd_spreI as1(1) eqs by blast |
972 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3) |
960 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3) |
973 by (auto simp add: CPT_def) |
961 by (auto simp add: CPT_def) |
974 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
962 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
975 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
963 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
976 unfolding PosOrd_ex1_def |
964 unfolding PosOrd_ex1_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) |
977 by (metis PosOrd_SeqI1 PosOrd_SeqI2 Posix1(2) flat.simps(5)) |
|
978 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
965 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
979 next |
966 next |
980 case (Posix_STAR1 s1 r v s2 vs v3) |
967 case (Posix_STAR1 s1 r v s2 vs v3) |
981 have as1: "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
968 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
|
969 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
982 have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
970 have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
983 have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
971 have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
984 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
972 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
985 have cond2: "flat v \<noteq> []" by fact |
973 have cond2: "flat v \<noteq> []" by fact |
986 have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact |
974 have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact |
998 unfolding prefix_list_def |
986 unfolding prefix_list_def |
999 by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) |
987 by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) |
1000 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
988 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
1001 by (simp add: sprefix_list_def append_eq_conv_conj) |
989 by (simp add: sprefix_list_def append_eq_conv_conj) |
1002 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
990 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
1003 using PosOrd_spreI Posix1(2) as1(1) NonEmpty(4) by blast |
991 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
1004 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)" |
992 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)" |
1005 using NonEmpty(2,3) by (auto simp add: CPT_def) |
993 using NonEmpty(2,3) by (auto simp add: CPT_def) |
1006 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
994 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
995 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
996 unfolding PosOrd_ex1_def by auto |
1007 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
997 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
1008 unfolding PosOrd_ex1_def |
998 unfolding PosOrd_ex1_def |
1009 by (metis PosOrd_StarsI PosOrd_StarsI2 Posix1(2) flat.simps(7) val.inject(5)) |
999 by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5)) |
1010 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
1000 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
1011 next |
1001 next |
1012 case Empty |
1002 case Empty |
1013 have "v3 = Stars []" by fact |
1003 have "v3 = Stars []" by fact |
1014 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
1004 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
1030 proof - |
1020 proof - |
1031 from assms(2) have "v2 \<in> CPT r s \<or> flat v2 \<sqsubset>spre s" |
1021 from assms(2) have "v2 \<in> CPT r s \<or> flat v2 \<sqsubset>spre s" |
1032 unfolding CPTpre_def CPT_def sprefix_list_def prefix_list_def by auto |
1022 unfolding CPTpre_def CPT_def sprefix_list_def prefix_list_def by auto |
1033 moreover |
1023 moreover |
1034 { assume "v2 \<in> CPT r s" |
1024 { assume "v2 \<in> CPT r s" |
1035 with assms(1) have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd) |
1025 with assms(1) |
|
1026 have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd) |
1036 } |
1027 } |
1037 moreover |
1028 moreover |
1038 { assume "flat v2 \<sqsubset>spre s" |
1029 { assume "flat v2 \<sqsubset>spre s" |
1039 then have "flat v2 \<sqsubset>spre flat v1" using assms(1) |
1030 then have "flat v2 \<sqsubset>spre flat v1" using assms(1) |
1040 using Posix1(2) by blast |
1031 using Posix1(2) by blast |
1072 apply(simp_all) |
1063 apply(simp_all) |
1073 apply(drule meta_mp) |
1064 apply(drule meta_mp) |
1074 apply(auto simp add: CPT_def PT_def)[1] |
1065 apply(auto simp add: CPT_def PT_def)[1] |
1075 apply(erule Prf.cases) |
1066 apply(erule Prf.cases) |
1076 apply(simp_all) |
1067 apply(simp_all) |
1077 apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_PosOrd_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25)) |
1068 using CPrf_stars PosOrd_irrefl apply fastforce |
1078 apply(clarify) |
1069 apply(clarify) |
1079 apply(drule_tac x="Stars (a#v#vsa)" in spec) |
1070 apply(drule_tac x="Stars (a#v#vsa)" in spec) |
1080 apply(simp) |
1071 apply(simp) |
1081 apply(drule mp) |
1072 apply(drule mp) |
1082 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
1073 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
1121 apply (simp add: Posix1a Prf.intros(7)) |
1112 apply (simp add: Posix1a Prf.intros(7)) |
1122 apply(simp) |
1113 apply(simp) |
1123 apply(subst (asm) (2) PosOrd_ex_def) |
1114 apply(subst (asm) (2) PosOrd_ex_def) |
1124 apply(simp) |
1115 apply(simp) |
1125 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def) |
1116 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def) |
1126 proof - |
1117 by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def) |
1127 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
|
1128 assume a1: "s\<^sub>3 \<noteq> []" |
|
1129 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
|
1130 assume a3: "flat vA = flat a @ s\<^sub>3" |
|
1131 assume a4: "\<forall>p. \<not> (Stars (vA # vB) \<sqsubset>val p (Stars (a # vsa)))" |
|
1132 have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs" |
|
1133 by (meson drop_eq_Nil not_less) |
|
1134 have f6: "\<not> length (flat vA) \<le> length (flat a)" |
|
1135 using a3 a1 by simp |
|
1136 have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
|
1137 using a3 a2 by simp |
|
1138 then show False |
|
1139 using f6 f5 a4 by (metis (full_types) drop_eq_Nil PosOrd_StarsI PosOrd_ex_def PosOrd_shorterI) |
|
1140 qed |
|
1141 |
|
1142 |
|
1143 |
1118 |
1144 |
1119 |
1145 section {* The Smallest Value is indeed the Posix Value *} |
1120 section {* The Smallest Value is indeed the Posix Value *} |
1146 |
1121 |
1147 lemma PosOrd_Posix: |
1122 lemma PosOrd_Posix: |