160 |
160 |
161 |
161 |
162 section {* Ordering of values according to Okui & Suzuki *} |
162 section {* Ordering of values according to Okui & Suzuki *} |
163 |
163 |
164 |
164 |
165 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _") |
165 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
166 where |
166 where |
167 "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> |
167 "v1 \<sqsubset>val p v2 \<equiv> p \<in> Pos v1 \<and> |
168 pflat_len v1 p > pflat_len v2 p \<and> |
168 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))" |
169 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
170 |
170 |
171 |
171 definition ValFlat_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>fval _ _") |
172 definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _") |
172 where |
|
173 "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> |
|
175 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> (pflat_len v1 q = pflat_len v2 q))" |
|
176 |
|
177 lemma |
|
178 assumes "v1 \<sqsubset>fval p v2" |
|
179 shows "v1 \<sqsubset>val p v2" |
|
180 using assms |
|
181 unfolding ValFlat_ord_def PosOrd_def |
|
182 apply(clarify) |
|
183 apply(simp add: pflat_len_def) |
|
184 apply(auto)[1] |
|
185 apply(smt intlen_bigger) |
|
186 apply(simp add: sprefix_list_def prefix_list_def) |
|
187 apply(auto)[1] |
|
188 apply(drule sym) |
|
189 apply(simp add: intlen_append) |
|
190 apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3)) |
|
191 apply(smt intlen_bigger) |
|
192 done |
|
193 |
|
194 lemma |
|
195 assumes "v1 \<sqsubset>val p v2" "flat (at v2 p) \<sqsubset>spre flat (at v1 p)" |
|
196 shows "v1 \<sqsubset>fval p v2" |
|
197 using assms |
|
198 unfolding ValFlat_ord_def PosOrd_def |
|
199 apply(clarify) |
|
200 done |
|
201 |
|
202 |
|
203 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60) |
173 where |
204 where |
174 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
205 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
175 |
206 |
176 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
207 definition PosOrd_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60) |
177 where |
208 where |
178 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
209 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
179 |
210 |
180 lemma val_ord_shorterE: |
211 lemma PosOrd_shorterE: |
181 assumes "v1 :\<sqsubset>val v2" |
212 assumes "v1 :\<sqsubset>val v2" |
182 shows "length (flat v2) \<le> length (flat v1)" |
213 shows "length (flat v2) \<le> length (flat v1)" |
183 using assms |
214 using assms |
184 apply(auto simp add: val_ord_ex_def val_ord_def) |
215 apply(auto simp add: PosOrd_ex_def PosOrd_def) |
185 apply(case_tac p) |
216 apply(case_tac p) |
186 apply(simp add: pflat_len_simps) |
217 apply(simp add: pflat_len_simps) |
187 apply(simp add: intlen_length) |
218 apply(simp add: intlen_length) |
188 apply(simp) |
219 apply(simp) |
189 apply(drule_tac x="[]" in bspec) |
220 apply(drule_tac x="[]" in bspec) |
190 apply(simp add: Pos_empty) |
221 apply(simp add: Pos_empty) |
191 apply(simp add: pflat_len_simps) |
222 apply(simp add: pflat_len_simps) |
192 by (metis intlen_length le_less less_irrefl linear) |
223 by (metis intlen_length le_less less_irrefl linear) |
193 |
224 |
194 |
225 |
195 lemma val_ord_shorterI: |
226 lemma PosOrd_shorterI: |
196 assumes "length (flat v') < length (flat v)" |
227 assumes "length (flat v') < length (flat v)" |
197 shows "v :\<sqsubset>val v'" |
228 shows "v :\<sqsubset>val v'" |
198 using assms |
229 using assms |
199 unfolding val_ord_ex_def |
230 unfolding PosOrd_ex_def |
200 by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) val_ord_def) |
231 by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def) |
201 |
232 |
202 lemma val_ord_spreI: |
233 lemma PosOrd_spreI: |
203 assumes "(flat v') \<sqsubset>spre (flat v)" |
234 assumes "(flat v') \<sqsubset>spre (flat v)" |
204 shows "v :\<sqsubset>val v'" |
235 shows "v :\<sqsubset>val v'" |
205 using assms |
236 using assms |
206 apply(rule_tac val_ord_shorterI) |
237 apply(rule_tac PosOrd_shorterI) |
207 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all) |
238 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all) |
208 |
239 |
209 |
240 lemma PosOrd_Left_Right: |
210 |
241 assumes "flat v1 = flat v2" |
211 lemma val_ord_LeftI: |
242 shows "Left v1 :\<sqsubset>val Right v2" |
|
243 unfolding PosOrd_ex_def |
|
244 apply(rule_tac x="[0]" in exI) |
|
245 using assms |
|
246 apply(auto simp add: PosOrd_def pflat_len_simps Pos_empty) |
|
247 apply(smt intlen_bigger) |
|
248 done |
|
249 |
|
250 lemma PosOrd_LeftI: |
212 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
251 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
213 shows "(Left v) :\<sqsubset>val (Left v')" |
252 shows "(Left v) :\<sqsubset>val (Left v')" |
214 using assms(1) |
253 using assms(1) |
215 unfolding val_ord_ex_def |
254 unfolding PosOrd_ex_def |
216 apply(auto) |
255 apply(auto) |
217 apply(rule_tac x="0#p" in exI) |
256 apply(rule_tac x="0#p" in exI) |
218 using assms(2) |
257 using assms(2) |
219 apply(auto simp add: val_ord_def pflat_len_simps) |
258 apply(auto simp add: PosOrd_def pflat_len_simps) |
220 done |
259 done |
221 |
260 |
222 lemma val_ord_RightI: |
261 lemma PosOrd_RightI: |
223 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
262 assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
224 shows "(Right v) :\<sqsubset>val (Right v')" |
263 shows "(Right v) :\<sqsubset>val (Right v')" |
225 using assms(1) |
264 using assms(1) |
226 unfolding val_ord_ex_def |
265 unfolding PosOrd_ex_def |
227 apply(auto) |
266 apply(auto) |
228 apply(rule_tac x="Suc 0#p" in exI) |
267 apply(rule_tac x="Suc 0#p" in exI) |
229 using assms(2) |
268 using assms(2) |
230 apply(auto simp add: val_ord_def pflat_len_simps) |
269 apply(auto simp add: PosOrd_def pflat_len_simps) |
231 done |
270 done |
232 |
271 |
233 lemma val_ord_LeftE: |
272 lemma PosOrd_LeftE: |
234 assumes "(Left v1) :\<sqsubset>val (Left v2)" |
273 assumes "(Left v1) :\<sqsubset>val (Left v2)" |
235 shows "v1 :\<sqsubset>val v2" |
274 shows "v1 :\<sqsubset>val v2" |
236 using assms |
275 using assms |
237 apply(simp add: val_ord_ex_def) |
276 apply(simp add: PosOrd_ex_def) |
238 apply(erule exE) |
277 apply(erule exE) |
239 apply(case_tac "p = []") |
278 apply(case_tac "p = []") |
240 apply(simp add: val_ord_def) |
279 apply(simp add: PosOrd_def) |
241 apply(auto simp add: pflat_len_simps) |
280 apply(auto simp add: pflat_len_simps) |
242 apply(rule_tac x="[]" in exI) |
281 apply(rule_tac x="[]" in exI) |
243 apply(simp add: Pos_empty pflat_len_simps) |
282 apply(simp add: Pos_empty pflat_len_simps) |
244 apply(auto simp add: pflat_len_simps val_ord_def) |
283 apply(auto simp add: pflat_len_simps PosOrd_def) |
245 apply(rule_tac x="ps" in exI) |
284 apply(rule_tac x="ps" in exI) |
246 apply(auto) |
285 apply(auto) |
247 apply(drule_tac x="0#q" in bspec) |
286 apply(drule_tac x="0#q" in bspec) |
248 apply(simp) |
287 apply(simp) |
249 apply(simp add: pflat_len_simps) |
288 apply(simp add: pflat_len_simps) |
250 apply(drule_tac x="0#q" in bspec) |
289 apply(drule_tac x="0#q" in bspec) |
251 apply(simp) |
290 apply(simp) |
252 apply(simp add: pflat_len_simps) |
291 apply(simp add: pflat_len_simps) |
253 done |
292 done |
254 |
293 |
255 lemma val_ord_RightE: |
294 lemma PosOrd_RightE: |
256 assumes "(Right v1) :\<sqsubset>val (Right v2)" |
295 assumes "(Right v1) :\<sqsubset>val (Right v2)" |
257 shows "v1 :\<sqsubset>val v2" |
296 shows "v1 :\<sqsubset>val v2" |
258 using assms |
297 using assms |
259 apply(simp add: val_ord_ex_def) |
298 apply(simp add: PosOrd_ex_def) |
260 apply(erule exE) |
299 apply(erule exE) |
261 apply(case_tac "p = []") |
300 apply(case_tac "p = []") |
262 apply(simp add: val_ord_def) |
301 apply(simp add: PosOrd_def) |
263 apply(auto simp add: pflat_len_simps) |
302 apply(auto simp add: pflat_len_simps) |
264 apply(rule_tac x="[]" in exI) |
303 apply(rule_tac x="[]" in exI) |
265 apply(simp add: Pos_empty pflat_len_simps) |
304 apply(simp add: Pos_empty pflat_len_simps) |
266 apply(auto simp add: pflat_len_simps val_ord_def) |
305 apply(auto simp add: pflat_len_simps PosOrd_def) |
267 apply(rule_tac x="ps" in exI) |
306 apply(rule_tac x="ps" in exI) |
268 apply(auto) |
307 apply(auto) |
269 apply(drule_tac x="Suc 0#q" in bspec) |
308 apply(drule_tac x="Suc 0#q" in bspec) |
270 apply(simp) |
309 apply(simp) |
271 apply(simp add: pflat_len_simps) |
310 apply(simp add: pflat_len_simps) |
321 using assms(2) |
360 using assms(2) |
322 apply(simp) |
361 apply(simp) |
323 apply(auto simp add: pflat_len_simps) |
362 apply(auto simp add: pflat_len_simps) |
324 done |
363 done |
325 |
364 |
326 lemma val_ord_SeqE: |
365 lemma PosOrd_SeqE: |
327 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
366 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
328 shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'" |
367 shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'" |
329 using assms |
368 using assms |
330 apply(simp add: val_ord_ex_def) |
369 apply(simp add: PosOrd_ex_def) |
331 apply(erule exE) |
370 apply(erule exE) |
332 apply(case_tac p) |
371 apply(case_tac p) |
333 apply(simp add: val_ord_def) |
372 apply(simp add: PosOrd_def) |
334 apply(auto simp add: pflat_len_simps intlen_append)[1] |
373 apply(auto simp add: pflat_len_simps intlen_append)[1] |
335 apply(rule_tac x="[]" in exI) |
374 apply(rule_tac x="[]" in exI) |
336 apply(drule_tac x="[]" in spec) |
375 apply(drule_tac x="[]" in spec) |
337 apply(simp add: Pos_empty pflat_len_simps) |
376 apply(simp add: Pos_empty pflat_len_simps) |
338 apply(case_tac a) |
377 apply(case_tac a) |
339 apply(rule disjI1) |
378 apply(rule disjI1) |
340 apply(simp add: val_ord_def) |
379 apply(simp add: PosOrd_def) |
341 apply(auto simp add: pflat_len_simps intlen_append)[1] |
380 apply(auto simp add: pflat_len_simps intlen_append)[1] |
342 apply(rule_tac x="list" in exI) |
381 apply(rule_tac x="list" in exI) |
343 apply(simp) |
382 apply(simp) |
344 apply(rule ballI) |
383 apply(rule ballI) |
345 apply(rule impI) |
384 apply(rule impI) |
346 apply(drule_tac x="0#q" in bspec) |
385 apply(drule_tac x="0#q" in bspec) |
347 apply(simp) |
386 apply(simp) |
348 apply(simp add: pflat_len_simps) |
387 apply(simp add: pflat_len_simps) |
349 apply(case_tac nat) |
388 apply(case_tac nat) |
350 apply(rule disjI2) |
389 apply(rule disjI2) |
351 apply(simp add: val_ord_def) |
390 apply(simp add: PosOrd_def) |
352 apply(auto simp add: pflat_len_simps intlen_append) |
391 apply(auto simp add: pflat_len_simps intlen_append) |
353 apply(rule_tac x="list" in exI) |
392 apply(rule_tac x="list" in exI) |
354 apply(simp add: Pos_empty) |
393 apply(simp add: Pos_empty) |
355 apply(rule ballI) |
394 apply(rule ballI) |
356 apply(rule impI) |
395 apply(rule impI) |
357 apply(drule_tac x="Suc 0#q" in bspec) |
396 apply(drule_tac x="Suc 0#q" in bspec) |
358 apply(simp) |
397 apply(simp) |
359 apply(simp add: pflat_len_simps) |
398 apply(simp add: pflat_len_simps) |
360 apply(simp add: val_ord_def) |
399 apply(simp add: PosOrd_def) |
361 done |
400 done |
362 |
401 |
363 lemma val_ord_StarsI: |
402 lemma PosOrd_StarsI: |
364 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
403 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
365 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
404 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
366 using assms(1) |
405 using assms(1) |
367 apply(subst (asm) val_ord_ex_def) |
406 apply(subst (asm) PosOrd_ex_def) |
368 apply(subst (asm) val_ord_def) |
407 apply(subst (asm) PosOrd_def) |
369 apply(clarify) |
408 apply(clarify) |
370 apply(subst val_ord_ex_def) |
409 apply(subst PosOrd_ex_def) |
371 apply(subst val_ord_def) |
410 apply(subst PosOrd_def) |
372 apply(rule_tac x="0#p" in exI) |
411 apply(rule_tac x="0#p" in exI) |
373 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
412 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
374 using assms(2) |
413 using assms(2) |
375 apply(simp add: pflat_len_simps intlen_append) |
414 apply(simp add: pflat_len_simps intlen_append) |
376 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
415 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
377 done |
416 done |
378 |
417 |
379 lemma val_ord_StarsI2: |
418 lemma PosOrd_StarsI2: |
380 assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
419 assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
381 shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))" |
420 shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))" |
382 using assms(1) |
421 using assms(1) |
383 apply(subst (asm) val_ord_ex_def) |
422 apply(subst (asm) PosOrd_ex_def) |
384 apply(subst (asm) val_ord_def) |
423 apply(subst (asm) PosOrd_def) |
385 apply(clarify) |
424 apply(clarify) |
386 apply(subst val_ord_ex_def) |
425 apply(subst PosOrd_ex_def) |
387 apply(subst val_ord_def) |
426 apply(subst PosOrd_def) |
388 apply(case_tac p) |
427 apply(case_tac p) |
389 apply(simp add: pflat_len_simps) |
428 apply(simp add: pflat_len_simps) |
390 apply(rule_tac x="[]" in exI) |
429 apply(rule_tac x="[]" in exI) |
391 apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append) |
430 apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append) |
392 apply(rule_tac x="Suc a#list" in exI) |
431 apply(rule_tac x="Suc a#list" in exI) |
394 using assms(2) |
433 using assms(2) |
395 apply(simp add: pflat_len_simps intlen_append) |
434 apply(simp add: pflat_len_simps intlen_append) |
396 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
435 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
397 done |
436 done |
398 |
437 |
399 lemma val_ord_Stars_appendI: |
438 lemma PosOrd_Stars_appendI: |
400 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
439 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
401 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
440 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
402 using assms |
441 using assms |
403 apply(induct vs) |
442 apply(induct vs) |
404 apply(simp) |
443 apply(simp) |
405 apply(simp add: val_ord_StarsI2) |
444 apply(simp add: PosOrd_StarsI2) |
406 done |
445 done |
407 |
446 |
408 lemma val_ord_StarsE2: |
447 lemma PosOrd_StarsE2: |
409 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
448 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
410 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
449 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
411 using assms |
450 using assms |
412 apply(subst (asm) val_ord_ex_def) |
451 apply(subst (asm) PosOrd_ex_def) |
413 apply(erule exE) |
452 apply(erule exE) |
414 apply(case_tac p) |
453 apply(case_tac p) |
415 apply(simp) |
454 apply(simp) |
416 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
455 apply(simp add: PosOrd_def pflat_len_simps intlen_append) |
417 apply(subst val_ord_ex_def) |
456 apply(subst PosOrd_ex_def) |
418 apply(rule_tac x="[]" in exI) |
457 apply(rule_tac x="[]" in exI) |
419 apply(simp add: val_ord_def pflat_len_simps Pos_empty) |
458 apply(simp add: PosOrd_def pflat_len_simps Pos_empty) |
420 apply(simp) |
459 apply(simp) |
421 apply(case_tac a) |
460 apply(case_tac a) |
422 apply(clarify) |
461 apply(clarify) |
423 apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1] |
462 apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def)[1] |
424 apply(clarify) |
463 apply(clarify) |
425 apply(simp add: val_ord_ex_def) |
464 apply(simp add: PosOrd_ex_def) |
426 apply(rule_tac x="nat#list" in exI) |
465 apply(rule_tac x="nat#list" in exI) |
427 apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
466 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1] |
428 apply(case_tac q) |
467 apply(case_tac q) |
429 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
468 apply(simp add: PosOrd_def pflat_len_simps intlen_append) |
430 apply(clarify) |
469 apply(clarify) |
431 apply(drule_tac x="Suc a # lista" in bspec) |
470 apply(drule_tac x="Suc a # lista" in bspec) |
432 apply(simp) |
471 apply(simp) |
433 apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
472 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1] |
434 apply(case_tac q) |
473 apply(case_tac q) |
435 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
474 apply(simp add: PosOrd_def pflat_len_simps intlen_append) |
436 apply(clarify) |
475 apply(clarify) |
437 apply(drule_tac x="Suc a # lista" in bspec) |
476 apply(drule_tac x="Suc a # lista" in bspec) |
438 apply(simp) |
477 apply(simp) |
439 apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
478 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1] |
440 done |
479 done |
441 |
480 |
442 lemma val_ord_Stars_appendE: |
481 lemma PosOrd_Stars_appendE: |
443 assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
482 assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
444 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
483 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
445 using assms |
484 using assms |
446 apply(induct vs) |
485 apply(induct vs) |
447 apply(simp) |
486 apply(simp) |
448 apply(simp add: val_ord_StarsE2) |
487 apply(simp add: PosOrd_StarsE2) |
449 done |
488 done |
450 |
489 |
451 lemma val_ord_Stars_append_eq: |
490 lemma PosOrd_Stars_append_eq: |
452 assumes "flat (Stars vs1) = flat (Stars vs2)" |
491 assumes "flat (Stars vs1) = flat (Stars vs2)" |
453 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
492 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
454 using assms |
493 using assms |
455 apply(rule_tac iffI) |
494 apply(rule_tac iffI) |
456 apply(erule val_ord_Stars_appendE) |
495 apply(erule PosOrd_Stars_appendE) |
457 apply(rule val_ord_Stars_appendI) |
496 apply(rule PosOrd_Stars_appendI) |
458 apply(auto) |
497 apply(auto) |
459 done |
498 done |
460 |
499 |
461 |
500 |
462 lemma val_ord_trans: |
501 lemma PosOrd_trans: |
463 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
502 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
464 shows "v1 :\<sqsubset>val v3" |
503 shows "v1 :\<sqsubset>val v3" |
465 using assms |
504 using assms |
466 unfolding val_ord_ex_def |
505 unfolding PosOrd_ex_def |
467 apply(clarify) |
506 apply(clarify) |
468 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p") |
507 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p") |
469 prefer 2 |
508 prefer 2 |
470 apply(rule lex_trichotomous) |
509 apply(rule lex_trichotomous) |
471 apply(erule disjE) |
510 apply(erule disjE) |
472 apply(simp) |
511 apply(simp) |
473 apply(rule_tac x="pa" in exI) |
512 apply(rule_tac x="pa" in exI) |
474 apply(subst val_ord_def) |
513 apply(subst PosOrd_def) |
475 apply(rule conjI) |
514 apply(rule conjI) |
476 apply(simp add: val_ord_def) |
515 apply(simp add: PosOrd_def) |
477 apply(auto)[1] |
516 apply(auto)[1] |
478 apply(simp add: val_ord_def) |
517 apply(simp add: PosOrd_def) |
479 apply(simp add: val_ord_def) |
518 apply(simp add: PosOrd_def) |
480 apply(auto)[1] |
519 apply(auto)[1] |
481 using outside_lemma apply blast |
520 using outside_lemma apply blast |
482 apply(simp add: val_ord_def) |
521 apply(simp add: PosOrd_def) |
483 apply(auto)[1] |
522 apply(auto)[1] |
484 using outside_lemma apply force |
523 using outside_lemma apply force |
485 apply auto[1] |
524 apply auto[1] |
486 apply(simp add: val_ord_def) |
525 apply(simp add: PosOrd_def) |
487 apply(auto)[1] |
526 apply(auto)[1] |
488 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
527 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
489 apply(simp add: val_ord_def) |
528 apply(simp add: PosOrd_def) |
490 apply(auto)[1] |
529 apply(auto)[1] |
491 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def) |
530 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def) |
492 |
531 |
493 lemma val_ord_irrefl: |
532 lemma PosOrd_irrefl: |
494 assumes "v :\<sqsubset>val v" |
533 assumes "v :\<sqsubset>val v" |
495 shows "False" |
534 shows "False" |
496 using assms |
535 using assms |
497 by(auto simp add: val_ord_ex_def val_ord_def) |
536 by(auto simp add: PosOrd_ex_def PosOrd_def) |
498 |
537 |
499 lemma val_ord_almost_trichotomous: |
538 lemma PosOrd_almost_trichotomous: |
500 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
539 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
501 apply(auto simp add: val_ord_ex_def) |
540 apply(auto simp add: PosOrd_ex_def) |
502 apply(auto simp add: val_ord_def) |
541 apply(auto simp add: PosOrd_def) |
503 apply(rule_tac x="[]" in exI) |
542 apply(rule_tac x="[]" in exI) |
504 apply(auto simp add: Pos_empty pflat_len_simps) |
543 apply(auto simp add: Pos_empty pflat_len_simps) |
505 apply(drule_tac x="[]" in spec) |
544 apply(drule_tac x="[]" in spec) |
506 apply(auto simp add: Pos_empty pflat_len_simps) |
545 apply(auto simp add: Pos_empty pflat_len_simps) |
507 done |
546 done |
508 |
547 |
509 lemma WW1: |
548 lemma WW1: |
510 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1" |
549 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1" |
511 shows "False" |
550 shows "False" |
512 using assms |
551 using assms |
513 apply(auto simp add: val_ord_ex_def val_ord_def) |
552 apply(auto simp add: PosOrd_ex_def PosOrd_def) |
514 using assms(1) assms(2) val_ord_irrefl val_ord_trans by blast |
553 using assms(1) assms(2) PosOrd_irrefl PosOrd_trans by blast |
515 |
554 |
516 lemma WW2: |
555 lemma WW2: |
517 assumes "\<not>(v1 :\<sqsubset>val v2)" |
556 assumes "\<not>(v1 :\<sqsubset>val v2)" |
518 shows "v1 = v2 \<or> v2 :\<sqsubset>val v1" |
557 shows "v1 = v2 \<or> v2 :\<sqsubset>val v1" |
519 using assms |
558 using assms |
520 oops |
559 oops |
521 |
560 |
522 lemma val_ord_SeqE2: |
561 lemma PosOrd_SeqE2: |
523 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
562 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
524 shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')" |
563 shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')" |
525 using assms |
564 using assms |
526 apply(frule_tac val_ord_SeqE) |
565 apply(frule_tac PosOrd_SeqE) |
527 apply(erule disjE) |
566 apply(erule disjE) |
528 apply(simp) |
567 apply(simp) |
529 apply(auto) |
568 apply(auto) |
530 apply(case_tac "v1 :\<sqsubset>val v1'") |
569 apply(case_tac "v1 :\<sqsubset>val v1'") |
531 apply(simp) |
570 apply(simp) |
532 apply(auto simp add: val_ord_ex_def) |
571 apply(auto simp add: PosOrd_ex_def) |
533 apply(case_tac "v1 = v1'") |
572 apply(case_tac "v1 = v1'") |
534 apply(simp) |
573 apply(simp) |
535 oops |
574 oops |
536 |
575 |
537 section {* CPT and CPTpre *} |
576 section {* CPT and CPTpre *} |
825 apply(simp) |
864 apply(simp) |
826 apply(simp add: CPT_def) |
865 apply(simp add: CPT_def) |
827 apply(rule CPrf.intros) |
866 apply(rule CPrf.intros) |
828 done |
867 done |
829 |
868 |
830 lemma Posix_val_ord: |
869 section {* The Posix Value is smaller than any other Value *} |
|
870 |
|
871 lemma Posix_PosOrd: |
831 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" |
872 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" |
832 shows "v1 :\<sqsubseteq>val v2" |
873 shows "v1 :\<sqsubseteq>val v2" |
833 using assms |
874 using assms |
834 apply(induct arbitrary: v2 rule: Posix.induct) |
875 proof (induct arbitrary: v2 rule: Posix.induct) |
835 apply(simp add: CPTpre_def) |
876 case (Posix_ONE v) |
836 apply(clarify) |
877 have "v \<in> CPTpre ONE []" by fact |
837 apply(erule CPrf.cases) |
878 then show "Void :\<sqsubseteq>val v" |
838 apply(simp_all) |
879 by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases) |
839 apply(simp add: val_ord_ex1_def) |
880 next |
840 apply(simp add: CPTpre_def) |
881 case (Posix_CHAR c v) |
841 apply(clarify) |
882 have "v \<in> CPTpre (CHAR c) [c]" by fact |
842 apply(erule CPrf.cases) |
883 then show "Char c :\<sqsubseteq>val v" |
843 apply(simp_all) |
884 by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases) |
844 apply(simp add: val_ord_ex1_def) |
885 next |
845 (* ALT1 *) |
886 case (Posix_ALT1 s r1 v r2 v2) |
846 prefer 3 |
887 have as1: "s \<in> r1 \<rightarrow> v" by fact |
847 (* SEQ case *) |
888 have IH: "\<And>v2. v2 \<in> CPTpre r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
848 apply(subst (asm) (3) CPTpre_def) |
889 have "v2 \<in> CPTpre (ALT r1 r2) s" by fact |
849 apply(clarify) |
890 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 \<sqsubseteq>pre s" |
850 apply(erule CPrf.cases) |
891 by(auto simp add: CPTpre_def prefix_list_def) |
851 apply(simp_all) |
892 then consider |
852 apply(case_tac "s' = []") |
893 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 \<sqsubseteq>pre s" |
853 apply(simp) |
894 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 \<sqsubseteq>pre s" |
854 prefer 2 |
895 by (auto elim: CPrf.cases) |
855 apply(simp add: val_ord_ex1_def) |
896 then show "Left v :\<sqsubseteq>val v2" |
856 apply(clarify) |
897 proof(cases) |
857 apply(simp) |
898 case (Left v3) |
858 apply(simp add: val_ord_ex_def) |
899 have "v3 \<in> CPTpre r1 s" using Left(2,3) |
859 apply(simp (no_asm) add: val_ord_def) |
900 by (auto simp add: CPTpre_def prefix_list_def) |
860 apply(rule_tac x="[]" in exI) |
901 with IH have "v :\<sqsubseteq>val v3" by simp |
861 apply(simp add: pflat_len_simps) |
902 moreover |
862 apply(simp only: intlen_length) |
903 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Left(3) |
863 apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le) |
904 by (simp add: Posix1(2) sprefix_list_def) |
864 apply(subgoal_tac "length (flat v1a) \<le> length s1") |
905 ultimately have "Left v :\<sqsubseteq>val Left v3" |
865 prefer 2 |
906 by (auto simp add: PosOrd_ex1_def PosOrd_LeftI PosOrd_spreI) |
866 apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil) |
907 then show "Left v :\<sqsubseteq>val v2" unfolding Left . |
867 apply(subst (asm) append_eq_append_conv_if) |
908 next |
868 apply(simp) |
909 case (Right v3) |
869 apply(clarify) |
910 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Right(3) |
870 apply(drule_tac x="v1a" in meta_spec) |
911 by (simp add: Posix1(2) sprefix_list_def) |
871 apply(drule meta_mp) |
912 then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 |
872 apply(auto simp add: CPTpre_def)[1] |
913 by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right PosOrd_spreI) |
873 using append_eq_conv_conj apply blast |
914 then show "Left v :\<sqsubseteq>val v2" unfolding Right . |
874 apply(subst (asm) (2)val_ord_ex1_def) |
915 qed |
875 apply(erule disjE) |
916 next |
876 apply(subst val_ord_ex1_def) |
917 case (Posix_ALT2 s r2 v r1 v2) |
877 apply(rule disjI1) |
918 have as1: "s \<in> r2 \<rightarrow> v" by fact |
878 apply(rule val_ord_SeqI1) |
919 have as2: "s \<notin> L r1" by fact |
879 apply(simp) |
920 have IH: "\<And>v2. v2 \<in> CPTpre r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
880 apply(simp) |
921 have "v2 \<in> CPTpre (ALT r1 r2) s" by fact |
881 apply (metis Posix1(2) append_assoc append_take_drop_id) |
922 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 \<sqsubseteq>pre s" |
882 apply(simp) |
923 by(auto simp add: CPTpre_def prefix_list_def) |
883 apply(drule_tac x="v2b" in meta_spec) |
924 then consider |
884 apply(drule meta_mp) |
925 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 \<sqsubseteq>pre s" |
885 apply(auto simp add: CPTpre_def)[1] |
926 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 \<sqsubseteq>pre s" |
886 apply (simp add: Posix1(2)) |
927 by (auto elim: CPrf.cases) |
887 apply(subst (asm) val_ord_ex1_def) |
928 then show "Right v :\<sqsubseteq>val v2" |
888 apply(erule disjE) |
929 proof (cases) |
889 apply(subst val_ord_ex1_def) |
930 case (Right v3) |
890 apply(rule disjI1) |
931 have "v3 \<in> CPTpre r2 s" using Right(2,3) |
891 apply(rule val_ord_SeqI2) |
932 by (auto simp add: CPTpre_def prefix_list_def) |
892 apply(simp) |
933 with IH have "v :\<sqsubseteq>val v3" by simp |
893 apply (simp add: Posix1(2)) |
934 moreover |
894 apply(subst val_ord_ex1_def) |
935 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Right(3) |
895 apply(simp) |
936 by (simp add: Posix1(2) sprefix_list_def) |
896 (* ALT *) |
937 ultimately have "Right v :\<sqsubseteq>val Right v3" |
897 apply(subst (asm) (2) CPTpre_def) |
938 by (auto simp add: PosOrd_ex1_def PosOrd_RightI PosOrd_spreI) |
898 apply(clarify) |
939 then show "Right v :\<sqsubseteq>val v2" unfolding Right . |
899 apply(erule CPrf.cases) |
940 next |
900 apply(simp_all) |
941 case (Left v3) |
901 apply(clarify) |
942 have w: "v3 \<in> CPTpre r1 s" using Left(2,3) as2 |
902 apply(case_tac "s' = []") |
943 by (auto simp add: CPTpre_def prefix_list_def) |
903 apply(simp) |
944 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Left(3) |
904 apply(drule_tac x="v1" in meta_spec) |
945 by (simp add: Posix1(2) sprefix_list_def) |
905 apply(drule meta_mp) |
946 then have "flat v3 \<sqsubset>spre flat v \<or> \<Turnstile> v3 : r1" using w |
906 apply(auto simp add: CPTpre_def)[1] |
947 by(auto simp add: CPTpre_def) |
907 apply(subst (asm) val_ord_ex1_def) |
948 then have "flat v3 \<sqsubset>spre flat v" using as1 as2 Left |
908 apply(erule disjE) |
949 by (auto simp add: prefix_list_def sprefix_list_def Posix1(2) L_flat_Prf1 Prf_CPrf) |
909 apply(subst (asm) val_ord_ex_def) |
950 then have "Right v :\<sqsubseteq>val Left v3" |
910 apply(erule exE) |
951 by (simp add: PosOrd_ex1_def PosOrd_spreI) |
911 apply(subst val_ord_ex1_def) |
952 then show "Right v :\<sqsubseteq>val v2" unfolding Left . |
912 apply(rule disjI1) |
953 qed |
913 apply(rule val_ord_LeftI) |
954 next |
914 apply(subst val_ord_ex_def) |
955 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
915 apply(auto)[1] |
956 have as1: "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
916 using Posix1(2) apply blast |
957 have IH1: "\<And>v3. v3 \<in> CPTpre r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
917 using val_ord_ex1_def apply blast |
958 have IH2: "\<And>v3. v3 \<in> CPTpre r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
918 apply(subst val_ord_ex1_def) |
959 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 |
919 apply(rule disjI1) |
960 have "v3 \<in> CPTpre (SEQ r1 r2) (s1 @ s2)" by fact |
920 apply (simp add: Posix1(2) val_ord_shorterI) |
961 then obtain v3a v3b where eqs: |
921 apply(subst val_ord_ex1_def) |
962 "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2" |
922 apply(rule disjI1) |
963 "flat v3a @ flat v3b \<sqsubseteq>pre s1 @ s2" |
923 apply(case_tac "s' = []") |
964 by (force simp add: prefix_list_def CPTpre_def elim: CPrf.cases) |
924 apply(simp) |
965 then have "flat v3a @ flat v3b \<sqsubset>spre s1 @ s2 \<or> flat v3a @ flat v3b = s1 @ s2" |
925 apply(subst val_ord_ex_def) |
966 by (simp add: sprefix_list_def) |
926 apply(rule_tac x="[0]" in exI) |
967 moreover |
927 apply(subst val_ord_def) |
968 { assume "flat v3a @ flat v3b \<sqsubset>spre s1 @ s2" |
928 apply(rule conjI) |
969 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using as1 |
929 apply(simp add: Pos_empty) |
970 by (auto simp add: PosOrd_ex1_def PosOrd_spreI Posix1(2)) |
930 apply(rule conjI) |
971 } |
931 apply(simp add: pflat_len_simps) |
972 moreover |
932 apply (smt intlen_bigger) |
973 { assume q1: "flat v3a @ flat v3b = s1 @ s2" |
933 apply(simp) |
974 then have "flat v3a \<sqsubseteq>pre s1" using eqs(2,3) cond |
934 apply(rule conjI) |
975 unfolding prefix_list_def |
935 apply(simp add: pflat_len_simps) |
976 by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv) |
936 using Posix1(2) apply auto[1] |
977 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using q1 |
937 apply(rule ballI) |
978 by (simp add: sprefix_list_def append_eq_conv_conj) |
938 apply(rule impI) |
979 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
939 apply(case_tac "q = []") |
980 using PosOrd_spreI Posix1(2) as1(1) q1 by blast |
940 using Posix1(2) apply auto[1] |
981 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPTpre r1 s1 \<and> v3b \<in> CPTpre r2 s2)" using eqs(2,3) |
941 apply(auto)[1] |
982 by (auto simp add: CPTpre_def) |
942 apply(rule val_ord_shorterI) |
983 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
943 apply(simp) |
984 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using q1 q2 as1 |
944 apply (simp add: Posix1(2)) |
985 unfolding PosOrd_ex1_def |
945 (* ALT RIGHT *) |
986 by (metis PosOrd_SeqI1 PosOrd_SeqI2 Posix1(2) flat.simps(5)) |
946 apply(subst (asm) (2) CPTpre_def) |
987 } |
947 apply(clarify) |
988 ultimately show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
948 apply(erule CPrf.cases) |
989 next |
949 apply(simp_all) |
990 case (Posix_STAR1 s1 r v s2 vs v3) |
950 apply(clarify) |
991 have as1: "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
951 apply(case_tac "s' = []") |
992 have IH1: "\<And>v3. v3 \<in> CPTpre r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
952 apply(simp) |
993 have IH2: "\<And>v3. v3 \<in> CPTpre (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
953 apply (simp add: L_flat_Prf1 Prf_CPrf) |
994 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 |
954 apply(subst val_ord_ex1_def) |
995 have cond2: "flat v \<noteq> []" by fact |
955 apply(rule disjI1) |
996 have "v3 \<in> CPTpre (STAR r) (s1 @ s2)" by fact |
956 apply(rule val_ord_shorterI) |
997 then consider |
957 apply(simp) |
998 (NonEmpty) v3a vs3 where |
958 apply (simp add: Posix1(2)) |
999 "v3 = Stars (v3a # vs3)" "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r" |
959 apply(case_tac "s' = []") |
1000 "flat v3a @ flat (Stars vs3) \<sqsubseteq>pre s1 @ s2" |
960 apply(simp) |
1001 | (Empty) "v3 = Stars []" |
961 apply(drule_tac x="v2a" in meta_spec) |
1002 by (force simp add: CPTpre_def prefix_list_def elim: CPrf.cases) |
962 apply(drule meta_mp) |
1003 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
963 apply(auto simp add: CPTpre_def)[1] |
1004 proof (cases) |
964 apply(subst (asm) val_ord_ex1_def) |
1005 case (NonEmpty v3a vs3) |
965 apply(erule disjE) |
1006 then have "flat (Stars (v3a # vs3)) \<sqsubset>spre s1 @ s2 \<or> flat (Stars (v3a # vs3)) = s1 @ s2" |
966 apply(subst val_ord_ex1_def) |
1007 by (simp add: sprefix_list_def) |
967 apply(rule disjI1) |
1008 moreover |
968 apply(rule val_ord_RightI) |
1009 { assume "flat (Stars (v3a # vs3)) \<sqsubset>spre s1 @ s2" |
969 apply(simp) |
1010 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using as1 |
970 using Posix1(2) apply blast |
1011 by (metis PosOrd_ex1_def PosOrd_spreI Posix1(2) flat.simps(7)) |
971 apply (simp add: val_ord_ex1_def) |
1012 } |
972 apply(subst val_ord_ex1_def) |
1013 moreover |
973 apply(rule disjI1) |
1014 { assume q1: "flat (Stars (v3a # vs3)) = s1 @ s2" |
974 apply(rule val_ord_shorterI) |
1015 then have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) cond |
975 apply(simp) |
1016 unfolding prefix_list_def |
976 apply (simp add: Posix1(2)) |
1017 by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) |
977 (* STAR empty case *) |
1018 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using q1 |
978 prefer 2 |
1019 by (simp add: sprefix_list_def append_eq_conv_conj) |
979 apply(subst (asm) CPTpre_def) |
1020 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
980 apply(clarify) |
1021 using PosOrd_spreI Posix1(2) as1(1) q1 by blast |
981 apply(erule CPrf.cases) |
1022 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPTpre r s1 \<and> Stars vs3 \<in> CPTpre (STAR r) s2)" |
982 apply(simp_all) |
1023 using NonEmpty(2,3) by (auto simp add: CPTpre_def) |
983 apply(clarify) |
1024 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
984 apply (simp add: val_ord_ex1_def) |
1025 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using q1 q2 as1 |
985 (* STAR non-empty case *) |
1026 unfolding PosOrd_ex1_def |
986 apply(subst (asm) (3) CPTpre_def) |
1027 by (metis PosOrd_StarsI PosOrd_StarsI2 Posix1(2) flat.simps(7) val.inject(5)) |
987 apply(clarify) |
1028 } |
988 apply(erule CPrf.cases) |
1029 ultimately show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
989 apply(simp_all) |
1030 next |
990 apply(clarify) |
1031 case Empty |
991 apply (simp add: val_ord_ex1_def) |
1032 have "v3 = Stars []" by fact |
992 apply(rule val_ord_shorterI) |
1033 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
993 apply(simp) |
1034 unfolding PosOrd_ex1_def using cond2 |
994 apply(case_tac "s' = []") |
1035 by (simp add: PosOrd_shorterI) |
995 apply(simp) |
1036 qed |
996 prefer 2 |
1037 next |
997 apply (simp add: val_ord_ex1_def) |
1038 case (Posix_STAR2 r v2) |
998 apply(rule disjI1) |
1039 have "v2 \<in> CPTpre (STAR r) []" by fact |
999 apply(rule val_ord_shorterI) |
1040 then have "v2 = Stars []" using CPTpre_subsets by auto |
1000 apply(simp) |
1041 then show "Stars [] :\<sqsubseteq>val v2" |
1001 apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_all flat.simps(7) flat_Stars length_append not_less) |
1042 by (simp add: PosOrd_ex1_def) |
1002 apply(drule_tac x="va" in meta_spec) |
1043 qed |
1003 apply(drule meta_mp) |
1044 |
1004 apply(auto simp add: CPTpre_def)[1] |
1045 |
1005 apply (smt L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv2 flat_Stars self_append_conv) |
1046 lemma Posix_PosOrd_stronger: |
1006 apply (subst (asm) (2) val_ord_ex1_def) |
|
1007 apply(erule disjE) |
|
1008 prefer 2 |
|
1009 apply(simp) |
|
1010 apply(drule_tac x="Stars vsa" in meta_spec) |
|
1011 apply(drule meta_mp) |
|
1012 apply(auto simp add: CPTpre_def)[1] |
|
1013 apply (simp add: Posix1(2)) |
|
1014 apply (subst (asm) val_ord_ex1_def) |
|
1015 apply(erule disjE) |
|
1016 apply (subst val_ord_ex1_def) |
|
1017 apply(rule disjI1) |
|
1018 apply(rule val_ord_StarsI2) |
|
1019 apply(simp) |
|
1020 using Posix1(2) apply force |
|
1021 apply(simp add: val_ord_ex1_def) |
|
1022 apply (subst val_ord_ex1_def) |
|
1023 apply(rule disjI1) |
|
1024 apply(rule val_ord_StarsI) |
|
1025 apply(simp) |
|
1026 apply(simp add: Posix1) |
|
1027 using Posix1(2) by force |
|
1028 |
|
1029 |
|
1030 lemma Posix_val_ord_stronger: |
|
1031 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
1047 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
1032 shows "v1 :\<sqsubseteq>val v2" |
1048 shows "v1 :\<sqsubseteq>val v2" |
1033 using assms |
1049 using assms Posix_PosOrd |
1034 apply(rule_tac Posix_val_ord) |
1050 using CPT_CPTpre_subset by blast |
1035 apply(assumption) |
1051 |
1036 using CPT_CPTpre_subset by auto |
1052 |
1037 |
1053 lemma Posix_PosOrd_reverse: |
1038 |
|
1039 lemma Posix_val_ord_reverse: |
|
1040 assumes "s \<in> r \<rightarrow> v1" |
1054 assumes "s \<in> r \<rightarrow> v1" |
1041 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1055 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1042 using assms |
1056 using assms |
1043 by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
1057 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def |
1044 val_ord_ex1_def val_ord_ex_def val_ord_trans) |
1058 PosOrd_ex1_def PosOrd_ex_def PosOrd_trans) |
1045 |
1059 |
1046 |
1060 |
1047 lemma val_ord_Posix_Stars: |
1061 lemma PosOrd_Posix_Stars: |
1048 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
1062 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
1049 and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
1063 and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
1050 shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
1064 shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
1051 using assms |
1065 using assms |
1052 apply(induct vs) |
1066 apply(induct vs) |
1105 apply(simp_all) |
1119 apply(simp_all) |
1106 apply(clarify) |
1120 apply(clarify) |
1107 apply(rotate_tac 3) |
1121 apply(rotate_tac 3) |
1108 apply(erule Prf.cases) |
1122 apply(erule Prf.cases) |
1109 apply(simp_all) |
1123 apply(simp_all) |
1110 apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def) |
1124 apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) PosOrd_def PosOrd_ex_def) |
1111 apply(drule_tac x="Stars (v#va#vsb)" in spec) |
1125 apply(drule_tac x="Stars (v#va#vsb)" in spec) |
1112 apply(drule mp) |
1126 apply(drule mp) |
1113 apply (simp add: Posix1a Prf.intros(7)) |
1127 apply (simp add: Posix1a Prf.intros(7)) |
1114 apply(simp) |
1128 apply(simp) |
1115 apply(subst (asm) (2) val_ord_ex_def) |
1129 apply(subst (asm) (2) PosOrd_ex_def) |
1116 apply(simp) |
1130 apply(simp) |
1117 apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_ex_def) |
1131 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def) |
1118 proof - |
1132 proof - |
1119 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
1133 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
1120 assume a1: "s\<^sub>3 \<noteq> []" |
1134 assume a1: "s\<^sub>3 \<noteq> []" |
1121 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
1135 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
1122 assume a3: "flat vA = flat a @ s\<^sub>3" |
1136 assume a3: "flat vA = flat a @ s\<^sub>3" |
1123 assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)" |
1137 assume a4: "\<forall>p. \<not> (Stars (vA # vB) \<sqsubset>val p (Stars (a # vsa)))" |
1124 have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs" |
1138 have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs" |
1125 by (meson drop_eq_Nil not_less) |
1139 by (meson drop_eq_Nil not_less) |
1126 have f6: "\<not> length (flat vA) \<le> length (flat a)" |
1140 have f6: "\<not> length (flat vA) \<le> length (flat a)" |
1127 using a3 a1 by simp |
1141 using a3 a1 by simp |
1128 have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
1142 have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
1129 using a3 a2 by simp |
1143 using a3 a2 by simp |
1130 then show False |
1144 then show False |
1131 using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_StarsI val_ord_ex_def val_ord_shorterI) |
1145 using f6 f5 a4 by (metis (full_types) drop_eq_Nil PosOrd_StarsI PosOrd_ex_def PosOrd_shorterI) |
1132 qed |
1146 qed |
1133 |
1147 |
1134 |
1148 |
1135 |
1149 |
1136 |
1150 |
1137 |
1151 section {* The Smallest Value is indeed the Posix Value *} |
1138 lemma val_ord_Posix: |
1152 |
1139 assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)" |
1153 lemma PosOrd_Posix: |
|
1154 assumes "v1 \<in> CPT r s" "\<forall>v2 \<in> PT r s. \<not> v2 :\<sqsubset>val v1" |
1140 shows "s \<in> r \<rightarrow> v1" |
1155 shows "s \<in> r \<rightarrow> v1" |
1141 using assms |
1156 using assms |
1142 apply(induct r arbitrary: s v1) |
1157 proof(induct r arbitrary: s v1) |
1143 apply(auto simp add: CPT_def PT_def)[1] |
1158 case (ZERO s v1) |
1144 apply(erule CPrf.cases) |
1159 have "v1 \<in> CPT ZERO s" by fact |
1145 apply(simp_all) |
1160 then show "s \<in> ZERO \<rightarrow> v1" unfolding CPT_def |
1146 (* ONE *) |
1161 by (auto elim: CPrf.cases) |
1147 apply(auto simp add: CPT_def)[1] |
1162 next |
1148 apply(erule CPrf.cases) |
1163 case (ONE s v1) |
1149 apply(simp_all) |
1164 have "v1 \<in> CPT ONE s" by fact |
1150 apply(rule Posix.intros) |
1165 then show "s \<in> ONE \<rightarrow> v1" unfolding CPT_def |
1151 (* CHAR *) |
1166 by(auto elim!: CPrf.cases intro: Posix.intros) |
1152 apply(auto simp add: CPT_def)[1] |
1167 next |
1153 apply(erule CPrf.cases) |
1168 case (CHAR c s v1) |
1154 apply(simp_all) |
1169 have "v1 \<in> CPT (CHAR c) s" by fact |
1155 apply(rule Posix.intros) |
1170 then show "s \<in> CHAR c \<rightarrow> v1" unfolding CPT_def |
1156 prefer 2 |
1171 by (auto elim!: CPrf.cases intro: Posix.intros) |
1157 (* ALT *) |
1172 next |
1158 apply(auto simp add: CPT_def PT_def)[1] |
1173 case (ALT r1 r2 s v1) |
1159 apply(erule CPrf.cases) |
1174 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
1160 apply(simp_all) |
1175 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
1161 apply(rule Posix.intros) |
1176 have as1: "\<forall>v2\<in>PT (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
1162 apply(drule_tac x="flat v1a" in meta_spec) |
1177 have as2: "v1 \<in> CPT (ALT r1 r2) s" by fact |
1163 apply(drule_tac x="v1a" in meta_spec) |
1178 then consider |
1164 apply(drule meta_mp) |
1179 (Left) v1' where |
1165 apply(simp) |
1180 "v1 = Left v1'" "s = flat v1'" |
1166 apply(drule meta_mp) |
1181 "v1' \<in> CPT r1 s" |
1167 apply(auto)[1] |
1182 | (Right) v1' where |
1168 apply(drule_tac x="Left v2" in spec) |
1183 "v1 = Right v1'" "s = flat v1'" |
1169 apply(simp) |
1184 "v1' \<in> CPT r2 s" |
1170 apply(drule mp) |
1185 unfolding CPT_def by (auto elim: CPrf.cases) |
1171 apply(rule Prf.intros) |
1186 then show "s \<in> ALT r1 r2 \<rightarrow> v1" |
1172 apply(simp) |
1187 proof (cases) |
1173 apply (meson val_ord_LeftI) |
1188 case (Left v1') |
1174 apply(assumption) |
1189 have "v1' \<in> CPT r1 s" using as2 |
1175 (* ALT Right *) |
1190 unfolding CPT_def Left by (auto elim: CPrf.cases) |
1176 apply(auto simp add: CPT_def)[1] |
1191 moreover |
1177 apply(rule Posix.intros) |
1192 have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
1178 apply(rotate_tac 1) |
1193 unfolding PT_def Left using Prf.intros(2) PosOrd_LeftI by force |
1179 apply(drule_tac x="flat v2" in meta_spec) |
1194 ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp |
1180 apply(drule_tac x="v2" in meta_spec) |
1195 then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros) |
1181 apply(drule meta_mp) |
1196 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp |
1182 apply(simp) |
1197 next |
1183 apply(drule meta_mp) |
1198 case (Right v1') |
1184 apply(auto)[1] |
1199 have "v1' \<in> CPT r2 s" using as2 |
1185 apply(drule_tac x="Right v2a" in spec) |
1200 unfolding CPT_def Right by (auto elim: CPrf.cases) |
1186 apply(simp) |
1201 moreover |
1187 apply(drule mp) |
1202 have "\<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
1188 apply(rule Prf.intros) |
1203 unfolding PT_def Right using Prf.intros(3) PosOrd_RightI by force |
1189 apply(simp) |
1204 ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp |
1190 apply(drule val_ord_RightI) |
1205 moreover |
1191 apply(assumption) |
1206 { assume "s \<in> L r1" |
1192 apply(auto simp add: val_ord_ex_def)[1] |
1207 then obtain v' where "v' \<in> PT r1 s" |
1193 apply(assumption) |
1208 unfolding PT_def using L_flat_Prf2 by blast |
1194 apply(auto)[1] |
1209 then have "Left v' \<in> PT (ALT r1 r2) s" |
1195 apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a") |
1210 unfolding PT_def by (auto intro: Prf.intros) |
1196 apply(clarify) |
1211 with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" |
1197 apply(drule_tac x="Left v2'" in spec) |
1212 unfolding PT_def Right by (auto) |
1198 apply(simp) |
1213 then have False using PosOrd_Left_Right Right by blast |
1199 apply(drule mp) |
1214 } |
1200 apply(rule Prf.intros) |
1215 then have "s \<notin> L r1" by rule |
1201 apply(assumption) |
1216 ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros) |
1202 apply(simp add: val_ord_ex_def) |
1217 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp |
1203 apply(subst (asm) (3) val_ord_def) |
1218 qed |
1204 apply(simp) |
1219 next |
1205 apply(simp add: pflat_len_simps) |
1220 case (SEQ r1 r2 s v1) |
1206 apply(drule_tac x="[0]" in spec) |
1221 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
1207 apply(simp add: pflat_len_simps Pos_empty) |
1222 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
1208 apply(drule mp) |
1223 have as1: "\<forall>v2\<in>PT (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
1209 apply (smt intlen_bigger) |
1224 have as2: "v1 \<in> CPT (SEQ r1 r2) s" by fact |
1210 apply(erule disjE) |
1225 then obtain |
1211 apply blast |
1226 v1a v1b where eqs: |
1212 apply auto[1] |
1227 "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b" |
1213 apply (meson L_flat_Prf2) |
1228 "v1a \<in> CPT r1 (flat v1a)" "v1b \<in> CPT r2 (flat v1b)" |
1214 (* SEQ *) |
1229 unfolding CPT_def by(auto elim: CPrf.cases) |
1215 apply(auto simp add: CPT_def)[1] |
1230 have "\<forall>v2 \<in> PT r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a" |
1216 apply(erule CPrf.cases) |
1231 proof |
1217 apply(simp_all) |
1232 fix v2 |
1218 apply(rule Posix.intros) |
1233 assume "v2 \<in> PT r1 (flat v1a)" |
1219 apply(drule_tac x="flat v1a" in meta_spec) |
1234 with eqs(2,4) have "Seq v2 v1b \<in> PT (SEQ r1 r2) s" |
1220 apply(drule_tac x="v1a" in meta_spec) |
1235 by (simp add: CPT_def PT_def Prf.intros(1) Prf_CPrf) |
1221 apply(drule meta_mp) |
1236 with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" |
1222 apply(simp) |
1237 using eqs by (simp add: PT_def) |
1223 apply(drule meta_mp) |
1238 then show "\<not> v2 :\<sqsubset>val v1a" |
1224 apply(auto)[1] |
1239 using PosOrd_SeqI1 by blast |
1225 apply(auto simp add: PT_def)[1] |
1240 qed |
1226 apply(drule_tac x="Seq v2a v2" in spec) |
1241 then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp |
1227 apply(simp) |
1242 moreover |
1228 apply(drule mp) |
1243 have "\<forall>v2 \<in> PT r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b" |
1229 apply (simp add: Prf.intros(1) Prf_CPrf) |
1244 proof |
1230 using val_ord_SeqI1 apply fastforce |
1245 fix v2 |
1231 apply(assumption) |
1246 assume "v2 \<in> PT r2 (flat v1b)" |
1232 apply(rotate_tac 1) |
1247 with eqs(2,3,4) have "Seq v1a v2 \<in> PT (SEQ r1 r2) s" |
1233 apply(drule_tac x="flat v2" in meta_spec) |
1248 by (simp add: CPT_def PT_def Prf.intros Prf_CPrf) |
1234 apply(drule_tac x="v2" in meta_spec) |
1249 with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" |
1235 apply(simp) |
1250 using eqs by (simp add: PT_def) |
1236 apply(auto)[1] |
1251 then show "\<not> v2 :\<sqsubset>val v1b" |
1237 apply(drule meta_mp) |
1252 using PosOrd_SeqI2 by auto |
1238 apply(auto)[1] |
1253 qed |
1239 apply(auto simp add: PT_def)[1] |
1254 then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp |
1240 apply(drule_tac x="Seq v1a v2a" in spec) |
1255 moreover |
1241 apply(simp) |
1256 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
1242 apply(drule mp) |
1257 proof |
1243 apply (simp add: Prf.intros(1) Prf_CPrf) |
1258 assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" |
1244 apply (meson val_ord_SeqI2) |
1259 then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast |
1245 apply(assumption) |
1260 then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2" |
1246 (* SEQ side condition *) |
1261 using L_flat_Prf2 by blast |
1247 apply(auto simp add: PT_def) |
1262 then have "Seq vA vB \<in> PT (SEQ r1 r2) s" unfolding eqs using q1 |
1248 apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a") |
1263 by (auto simp add: PT_def intro: Prf.intros) |
1249 prefer 2 |
1264 with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto |
1250 apply (meson L_flat_Prf2) |
1265 then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto |
1251 apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a") |
1266 then show "False" |
1252 prefer 2 |
1267 using PosOrd_shorterI by blast |
1253 apply (meson L_flat_Prf2) |
1268 qed |
1254 apply(clarify) |
1269 ultimately |
1255 apply(drule_tac x="Seq vA vB" in spec) |
1270 show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs |
1256 apply(simp) |
1271 by (rule Posix.intros) |
1257 apply(drule mp) |
1272 next |
1258 apply (simp add: Prf.intros(1)) |
1273 case (STAR r s v1) |
1259 apply(subst (asm) (3) val_ord_ex_def) |
1274 have IH: "\<And>s v1. \<lbrakk>v1 \<in> CPT r s; \<forall>v2\<in>PT r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact |
1260 apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SeqI1 val_ord_ex_def val_ord_shorterI) |
1275 have as1: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact |
1261 (* STAR *) |
1276 have as2: "v1 \<in> CPT (STAR r) s" by fact |
1262 apply(auto simp add: CPT_def)[1] |
1277 then obtain |
1263 apply(erule CPrf.cases) |
1278 vs where eqs: |
1264 apply(simp_all)[6] |
1279 "v1 = Stars vs" "s = flat (Stars vs)" |
1265 using Posix_STAR2 apply blast |
1280 "\<forall>v \<in> set vs. v \<in> CPT r (flat v)" |
1266 apply(clarify) |
1281 unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars) |
1267 apply(rule val_ord_Posix_Stars) |
1282 have "Stars vs \<in> CPT (STAR r) (flat (Stars vs))" |
1268 apply(auto simp add: CPT_def)[1] |
1283 using as2 unfolding eqs . |
1269 apply (simp add: CPrf.intros(7)) |
1284 moreover |
1270 apply(auto)[1] |
1285 have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v" |
1271 apply(drule_tac x="flat v" in meta_spec) |
1286 proof |
1272 apply(drule_tac x="v" in meta_spec) |
1287 fix v |
1273 apply(simp) |
1288 assume a: "v \<in> set vs" |
1274 apply(drule meta_mp) |
1289 then obtain pre post where e: "vs = pre @ [v] @ post" |
1275 apply(auto)[1] |
1290 by (metis append_Cons append_Nil in_set_conv_decomp_first) |
1276 apply(drule_tac x="Stars (v2#vs)" in spec) |
1291 then have q: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" |
1277 apply(simp) |
1292 using as1 unfolding eqs by simp |
1278 apply(drule mp) |
1293 have "\<forall>v2\<in>PT r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs |
1279 using Prf.intros(7) Prf_CPrf apply blast |
1294 proof (rule ballI, rule notI) |
1280 apply(simp add: val_ord_StarsI) |
1295 fix v2 |
1281 apply(assumption) |
1296 assume w: "v2 :\<sqsubset>val v" |
1282 apply(drule_tac x="flat va" in meta_spec) |
1297 assume "v2 \<in> PT r (flat v)" |
1283 apply(drule_tac x="va" in meta_spec) |
1298 then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s" |
1284 apply(simp) |
1299 using as2 unfolding e eqs |
1285 apply(drule meta_mp) |
1300 apply(auto simp add: CPT_def PT_def intro!: Prf_Stars)[1] |
1286 using CPrf_stars apply blast |
1301 using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast |
1287 apply(drule meta_mp) |
1302 by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2)) |
1288 apply(auto)[1] |
1303 then have "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)" |
1289 apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post") |
1304 using q by simp |
1290 prefer 2 |
1305 with w show "False" |
1291 apply (metis append_Cons append_Nil in_set_conv_decomp_first) |
1306 using PT_def \<open>v2 \<in> PT r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq |
1292 apply(clarify) |
1307 PosOrd_StarsI PosOrd_Stars_appendI by auto |
1293 apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec) |
1308 qed |
1294 apply(simp) |
1309 with IH |
1295 apply(drule mp) |
1310 show "flat v \<in> r \<rightarrow> v" using a as2 unfolding eqs |
1296 apply(rule Prf.intros) |
1311 using eqs(3) by blast |
1297 apply (simp add: Prf_CPrf) |
1312 qed |
1298 apply(rule Prf_Stars_append) |
1313 moreover |
1299 apply(drule CPrf_Stars_appendE) |
1314 have "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" |
1300 apply(auto simp add: Prf_CPrf)[1] |
1315 proof |
1301 apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD) |
1316 assume "\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs" |
1302 apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)") |
1317 then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)" |
1303 apply(subst (asm) val_ord_Stars_append_eq) |
1318 "Stars vs2 :\<sqsubset>val Stars vs" |
1304 apply(simp) |
1319 unfolding PT_def |
1305 apply(subst (asm) val_ord_Stars_append_eq) |
1320 apply(auto elim: Prf.cases) |
1306 apply(simp) |
1321 apply(erule Prf.cases) |
1307 prefer 2 |
1322 apply(auto intro: Prf.intros) |
1308 apply(simp) |
1323 apply(drule_tac x="[]" in meta_spec) |
1309 prefer 2 |
1324 apply(simp) |
1310 apply(simp) |
1325 apply(drule meta_mp) |
1311 apply (simp add: val_ord_StarsI) |
1326 apply(auto intro: Prf.intros) |
1312 apply(auto simp add: PT_def) |
1327 apply(drule_tac x="(v#vsa)" in meta_spec) |
1313 done |
1328 apply(auto intro: Prf.intros) |
|
1329 done |
|
1330 then show "False" using as1 unfolding eqs |
|
1331 apply - |
|
1332 apply(drule_tac x="Stars vs2" in bspec) |
|
1333 apply(auto simp add: PT_def) |
|
1334 done |
|
1335 qed |
|
1336 ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
|
1337 by (rule PosOrd_Posix_Stars) |
|
1338 then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs . |
|
1339 qed |
1314 |
1340 |
1315 unused_thms |
1341 unused_thms |
1316 |
1342 |
1317 end |
1343 end |