9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Prefix order on lists *} |
12 subsection {* Prefix order on lists *} |
13 |
13 |
14 definition prefixeq :: "'a list => 'a list => bool" where |
14 definition prefixeq :: "'a list => 'a list => bool" |
15 "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)" |
15 where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)" |
16 |
16 |
17 definition prefix :: "'a list => 'a list => bool" where |
17 definition prefix :: "'a list => 'a list => bool" |
18 "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys" |
18 where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys" |
19 |
19 |
20 interpretation prefix_order: order prefixeq prefix |
20 interpretation prefix_order: order prefixeq prefix |
21 by default (auto simp: prefixeq_def prefix_def) |
21 by default (auto simp: prefixeq_def prefix_def) |
22 |
22 |
23 interpretation prefix_bot: bot prefixeq prefix Nil |
23 interpretation prefix_bot: bot prefixeq prefix Nil |
188 qed |
189 qed |
189 |
190 |
190 |
191 |
191 subsection {* Parallel lists *} |
192 subsection {* Parallel lists *} |
192 |
193 |
193 definition |
194 definition parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) |
194 parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where |
195 where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)" |
195 "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)" |
|
196 |
196 |
197 lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys" |
197 lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys" |
198 unfolding parallel_def by blast |
198 unfolding parallel_def by blast |
199 |
199 |
200 lemma parallelE [elim]: |
200 lemma parallelE [elim]: |
227 then show ?thesis |
227 then show ?thesis |
228 by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixeqI |
228 by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixeqI |
229 same_prefixeq_prefixeq snoc.prems ys) |
229 same_prefixeq_prefixeq snoc.prems ys) |
230 qed |
230 qed |
231 next |
231 next |
232 assume "prefix ys xs" then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def) |
232 assume "prefix ys xs" |
|
233 then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def) |
233 with snoc have False by blast |
234 with snoc have False by blast |
234 then show ?thesis .. |
235 then show ?thesis .. |
235 next |
236 next |
236 assume "xs \<parallel> ys" |
237 assume "xs \<parallel> ys" |
237 with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" |
238 with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" |
255 unfolding parallel_def by auto |
256 unfolding parallel_def by auto |
256 |
257 |
257 |
258 |
258 subsection {* Suffix order on lists *} |
259 subsection {* Suffix order on lists *} |
259 |
260 |
260 definition |
261 definition suffixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
261 suffixeq :: "'a list => 'a list => bool" where |
262 where "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)" |
262 "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)" |
263 |
263 |
264 definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
264 definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
265 where "suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])" |
265 "suffix xs ys \<equiv> \<exists>us. ys = us @ xs \<and> us \<noteq> []" |
|
266 |
266 |
267 lemma suffix_imp_suffixeq: |
267 lemma suffix_imp_suffixeq: |
268 "suffix xs ys \<Longrightarrow> suffixeq xs ys" |
268 "suffix xs ys \<Longrightarrow> suffixeq xs ys" |
269 by (auto simp: suffixeq_def suffix_def) |
269 by (auto simp: suffixeq_def suffix_def) |
270 |
270 |
295 lemma Nil_suffixeq [iff]: "suffixeq [] xs" |
295 lemma Nil_suffixeq [iff]: "suffixeq [] xs" |
296 by (simp add: suffixeq_def) |
296 by (simp add: suffixeq_def) |
297 lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])" |
297 lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])" |
298 by (auto simp add: suffixeq_def) |
298 by (auto simp add: suffixeq_def) |
299 |
299 |
300 lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y#ys)" |
300 lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y # ys)" |
301 by (auto simp add: suffixeq_def) |
301 by (auto simp add: suffixeq_def) |
302 lemma suffixeq_ConsD: "suffixeq (x#xs) ys \<Longrightarrow> suffixeq xs ys" |
302 lemma suffixeq_ConsD: "suffixeq (x # xs) ys \<Longrightarrow> suffixeq xs ys" |
303 by (auto simp add: suffixeq_def) |
303 by (auto simp add: suffixeq_def) |
304 |
304 |
305 lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)" |
305 lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)" |
306 by (auto simp add: suffixeq_def) |
306 by (auto simp add: suffixeq_def) |
307 lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys" |
307 lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys" |
311 "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffix_def) |
311 "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffix_def) |
312 |
312 |
313 lemma suffixeq_set_subset: |
313 lemma suffixeq_set_subset: |
314 "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffixeq_def) |
314 "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffixeq_def) |
315 |
315 |
316 lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys" |
316 lemma suffixeq_ConsD2: "suffixeq (x # xs) (y # ys) \<Longrightarrow> suffixeq xs ys" |
317 proof - |
317 proof - |
318 assume "suffixeq (x#xs) (y#ys)" |
318 assume "suffixeq (x # xs) (y # ys)" |
319 then obtain zs where "y#ys = zs @ x#xs" .. |
319 then obtain zs where "y # ys = zs @ x # xs" .. |
320 then show ?thesis |
320 then show ?thesis |
321 by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI) |
321 by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI) |
322 qed |
322 qed |
323 |
323 |
324 lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> prefixeq (rev xs) (rev ys)" |
324 lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> prefixeq (rev xs) (rev ys)" |
346 apply (rule exI [where x = "take n as"]) |
346 apply (rule exI [where x = "take n as"]) |
347 apply simp |
347 apply simp |
348 done |
348 done |
349 |
349 |
350 lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs" |
350 lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs" |
351 by (clarsimp elim!: suffixeqE) |
351 by (auto elim!: suffixeqE) |
352 |
352 |
353 lemma suffixeq_suffix_reflclp_conv: |
353 lemma suffixeq_suffix_reflclp_conv: "suffixeq = suffix\<^sup>=\<^sup>=" |
354 "suffixeq = suffix\<^sup>=\<^sup>=" |
|
355 proof (intro ext iffI) |
354 proof (intro ext iffI) |
356 fix xs ys :: "'a list" |
355 fix xs ys :: "'a list" |
357 assume "suffixeq xs ys" |
356 assume "suffixeq xs ys" |
358 show "suffix\<^sup>=\<^sup>= xs ys" |
357 show "suffix\<^sup>=\<^sup>= xs ys" |
359 proof |
358 proof |
360 assume "xs \<noteq> ys" |
359 assume "xs \<noteq> ys" |
361 with `suffixeq xs ys` show "suffix xs ys" by (auto simp: suffixeq_def suffix_def) |
360 with `suffixeq xs ys` show "suffix xs ys" |
|
361 by (auto simp: suffixeq_def suffix_def) |
362 qed |
362 qed |
363 next |
363 next |
364 fix xs ys :: "'a list" |
364 fix xs ys :: "'a list" |
365 assume "suffix\<^sup>=\<^sup>= xs ys" |
365 assume "suffix\<^sup>=\<^sup>= xs ys" |
366 thus "suffixeq xs ys" |
366 then show "suffixeq xs ys" |
367 proof |
367 proof |
368 assume "suffix xs ys" thus "suffixeq xs ys" by (rule suffix_imp_suffixeq) |
368 assume "suffix xs ys" then show "suffixeq xs ys" |
369 next |
369 by (rule suffix_imp_suffixeq) |
370 assume "xs = ys" thus "suffixeq xs ys" by (auto simp: suffixeq_def) |
370 next |
|
371 assume "xs = ys" then show "suffixeq xs ys" |
|
372 by (auto simp: suffixeq_def) |
371 qed |
373 qed |
372 qed |
374 qed |
373 |
375 |
374 lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y" |
376 lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y" |
375 by blast |
377 by blast |
409 case False |
411 case False |
410 then show ?thesis by (rule Cons_parallelI1) |
412 then show ?thesis by (rule Cons_parallelI1) |
411 qed |
413 qed |
412 qed |
414 qed |
413 |
415 |
414 lemma suffix_reflclp_conv: |
416 lemma suffix_reflclp_conv: "suffix\<^sup>=\<^sup>= = suffixeq" |
415 "suffix\<^sup>=\<^sup>= = suffixeq" |
|
416 by (intro ext) (auto simp: suffixeq_def suffix_def) |
417 by (intro ext) (auto simp: suffixeq_def suffix_def) |
417 |
418 |
418 lemma suffix_lists: |
419 lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A" |
419 "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A" |
|
420 unfolding suffix_def by auto |
420 unfolding suffix_def by auto |
421 |
421 |
422 |
422 |
423 subsection {* Embedding on lists *} |
423 subsection {* Embedding on lists *} |
424 |
424 |
425 inductive |
425 inductive emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
426 emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
427 for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
426 for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
428 where |
427 where |
429 emb_Nil [intro, simp]: "emb P [] ys" |
428 emb_Nil [intro, simp]: "emb P [] ys" |
430 | emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)" |
429 | emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)" |
431 | emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> emb P (x#xs) (y#ys)" |
430 | emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> emb P (x#xs) (y#ys)" |
432 |
431 |
433 lemma emb_Nil2 [simp]: |
432 lemma emb_Nil2 [simp]: |
434 assumes "emb P xs []" shows "xs = []" |
433 assumes "emb P xs []" shows "xs = []" |
435 using assms by (cases rule: emb.cases) auto |
434 using assms by (cases rule: emb.cases) auto |
436 |
435 |
437 lemma emb_Cons_Nil [simp]: |
436 lemma emb_Cons_Nil [simp]: "emb P (x#xs) [] = False" |
438 "emb P (x#xs) [] = False" |
|
439 proof - |
437 proof - |
440 { assume "emb P (x#xs) []" |
438 { assume "emb P (x#xs) []" |
441 from emb_Nil2 [OF this] have False by simp |
439 from emb_Nil2 [OF this] have False by simp |
442 } moreover { |
440 } moreover { |
443 assume False |
441 assume False |
444 hence "emb P (x#xs) []" by simp |
442 then have "emb P (x#xs) []" by simp |
445 } ultimately show ?thesis by blast |
443 } ultimately show ?thesis by blast |
446 qed |
444 qed |
447 |
445 |
448 lemma emb_append2 [intro]: |
446 lemma emb_append2 [intro]: "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)" |
449 "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)" |
|
450 by (induct zs) auto |
447 by (induct zs) auto |
451 |
448 |
452 lemma emb_prefix [intro]: |
449 lemma emb_prefix [intro]: |
453 assumes "emb P xs ys" shows "emb P xs (ys @ zs)" |
450 assumes "emb P xs ys" shows "emb P xs (ys @ zs)" |
454 using assms |
451 using assms |
456 |
453 |
457 lemma emb_ConsD: |
454 lemma emb_ConsD: |
458 assumes "emb P (x#xs) ys" |
455 assumes "emb P (x#xs) ys" |
459 shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs" |
456 shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs" |
460 using assms |
457 using assms |
461 proof (induct x\<equiv>"x#xs" y\<equiv>"ys" arbitrary: x xs ys) |
458 proof (induct x \<equiv> "x # xs" ys arbitrary: x xs) |
462 case emb_Cons thus ?case by (metis append_Cons) |
459 case emb_Cons |
|
460 then show ?case by (metis append_Cons) |
463 next |
461 next |
464 case (emb_Cons2 x y xs ys) |
462 case (emb_Cons2 x y xs ys) |
465 thus ?case by (cases xs) (auto, blast+) |
463 then show ?case by (cases xs) (auto, blast+) |
466 qed |
464 qed |
467 |
465 |
468 lemma emb_appendD: |
466 lemma emb_appendD: |
469 assumes "emb P (xs @ ys) zs" |
467 assumes "emb P (xs @ ys) zs" |
470 shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs" |
468 shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs" |
471 using assms |
469 using assms |
472 proof (induction xs arbitrary: ys zs) |
470 proof (induction xs arbitrary: ys zs) |
473 case Nil thus ?case by auto |
471 case Nil then show ?case by auto |
474 next |
472 next |
475 case (Cons x xs) |
473 case (Cons x xs) |
476 then obtain us v vs where "zs = us @ v # vs" |
474 then obtain us v vs where "zs = us @ v # vs" |
477 and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD) |
475 and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD) |
478 with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2) |
476 with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2) |
490 |
488 |
491 lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys" |
489 lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys" |
492 by (induct rule: emb.induct) auto |
490 by (induct rule: emb.induct) auto |
493 |
491 |
494 (*FIXME: move*) |
492 (*FIXME: move*) |
495 definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where |
493 definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" |
496 "transp_on P A \<equiv> \<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c" |
494 where "transp_on P A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c)" |
497 lemma transp_onI [Pure.intro]: |
495 lemma transp_onI [Pure.intro]: |
498 "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A" |
496 "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A" |
499 unfolding transp_on_def by blast |
497 unfolding transp_on_def by blast |
500 |
498 |
501 lemma transp_on_emb: |
499 lemma transp_on_emb: |
503 shows "transp_on (emb P) (lists A)" |
501 shows "transp_on (emb P) (lists A)" |
504 proof |
502 proof |
505 fix xs ys zs |
503 fix xs ys zs |
506 assume "emb P xs ys" and "emb P ys zs" |
504 assume "emb P xs ys" and "emb P ys zs" |
507 and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A" |
505 and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A" |
508 thus "emb P xs zs" |
506 then show "emb P xs zs" |
509 proof (induction arbitrary: zs) |
507 proof (induction arbitrary: zs) |
510 case emb_Nil show ?case by blast |
508 case emb_Nil show ?case by blast |
511 next |
509 next |
512 case (emb_Cons xs ys y) |
510 case (emb_Cons xs ys y) |
513 from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs |
511 from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs |
514 where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast |
512 where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast |
515 hence "emb P ys (v#vs)" by blast |
513 then have "emb P ys (v#vs)" by blast |
516 hence "emb P ys zs" unfolding zs by (rule emb_append2) |
514 then have "emb P ys zs" unfolding zs by (rule emb_append2) |
517 from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp |
515 from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp |
518 next |
516 next |
519 case (emb_Cons2 x y xs ys) |
517 case (emb_Cons2 x y xs ys) |
520 from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs |
518 from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs |
521 where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast |
519 where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast |
526 moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all |
524 moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all |
527 ultimately show ?thesis using `P x y` and `P y v` and assms |
525 ultimately show ?thesis using `P x y` and `P y v` and assms |
528 unfolding transp_on_def by blast |
526 unfolding transp_on_def by blast |
529 qed |
527 qed |
530 ultimately have "emb P (x#xs) (v#vs)" by blast |
528 ultimately have "emb P (x#xs) (v#vs)" by blast |
531 thus ?case unfolding zs by (rule emb_append2) |
529 then show ?case unfolding zs by (rule emb_append2) |
532 qed |
530 qed |
533 qed |
531 qed |
534 |
532 |
535 |
533 |
536 subsection {* Sublists (special case of embedding) *} |
534 subsection {* Sublists (special case of embedding) *} |
537 |
535 |
538 abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
536 abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
539 "sub xs ys \<equiv> emb (op =) xs ys" |
537 where "sub xs ys \<equiv> emb (op =) xs ys" |
540 |
538 |
541 lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto |
539 lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto |
542 |
540 |
543 lemma sub_same_length: |
541 lemma sub_same_length: |
544 assumes "sub xs ys" and "length xs = length ys" shows "xs = ys" |
542 assumes "sub xs ys" and "length xs = length ys" shows "xs = ys" |
599 lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []" |
599 lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []" |
600 by (auto dest: emb_length) |
600 by (auto dest: emb_length) |
601 |
601 |
602 lemma emb_append_mono: |
602 lemma emb_append_mono: |
603 "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs@ys) (xs'@ys')" |
603 "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs@ys) (xs'@ys')" |
604 apply (induct rule: emb.induct) |
604 apply (induct rule: emb.induct) |
605 apply (metis eq_Nil_appendI emb_append2) |
605 apply (metis eq_Nil_appendI emb_append2) |
606 apply (metis append_Cons emb_Cons) |
606 apply (metis append_Cons emb_Cons) |
607 by (metis append_Cons emb_Cons2) |
607 apply (metis append_Cons emb_Cons2) |
|
608 done |
608 |
609 |
609 |
610 |
610 subsection {* Appending elements *} |
611 subsection {* Appending elements *} |
611 |
612 |
612 lemma sub_append [simp]: |
613 lemma sub_append [simp]: |
613 "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r") |
614 "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r") |
614 proof |
615 proof |
615 { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'" |
616 { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'" |
616 hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys" |
617 then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys" |
617 proof (induct arbitrary: xs ys zs) |
618 proof (induct arbitrary: xs ys zs) |
618 case emb_Nil show ?case by simp |
619 case emb_Nil show ?case by simp |
619 next |
620 next |
620 case (emb_Cons xs' ys' x) |
621 case (emb_Cons xs' ys' x) |
621 { assume "ys=[]" hence ?case using emb_Cons(1) by auto } |
622 { assume "ys=[]" then have ?case using emb_Cons(1) by auto } |
622 moreover |
623 moreover |
623 { fix us assume "ys = x#us" |
624 { fix us assume "ys = x#us" |
624 hence ?case using emb_Cons(2) by(simp add: emb.emb_Cons) } |
625 then have ?case using emb_Cons(2) by(simp add: emb.emb_Cons) } |
625 ultimately show ?case by (auto simp:Cons_eq_append_conv) |
626 ultimately show ?case by (auto simp:Cons_eq_append_conv) |
626 next |
627 next |
627 case (emb_Cons2 x y xs' ys') |
628 case (emb_Cons2 x y xs' ys') |
628 { assume "xs=[]" hence ?case using emb_Cons2(1) by auto } |
629 { assume "xs=[]" then have ?case using emb_Cons2(1) by auto } |
629 moreover |
630 moreover |
630 { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using emb_Cons2 by auto} |
631 { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using emb_Cons2 by auto} |
631 moreover |
632 moreover |
632 { fix us assume "xs=x#us" "ys=[]" hence ?case using emb_Cons2(2) by bestsimp } |
633 { fix us assume "xs=x#us" "ys=[]" then have ?case using emb_Cons2(2) by bestsimp } |
633 ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv) |
634 ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv) |
634 qed } |
635 qed } |
635 moreover assume ?l |
636 moreover assume ?l |
636 ultimately show ?r by blast |
637 ultimately show ?r by blast |
637 next |
638 next |
638 assume ?r thus ?l by (metis emb_append_mono sub_refl) |
639 assume ?r then show ?l by (metis emb_append_mono sub_refl) |
639 qed |
640 qed |
640 |
641 |
641 lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)" |
642 lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)" |
642 by (induct zs) auto |
643 by (induct zs) auto |
643 |
644 |
656 |
657 |
657 lemma sub_filter [simp]: |
658 lemma sub_filter [simp]: |
658 assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)" |
659 assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)" |
659 using assms by (induct) auto |
660 using assms by (induct) auto |
660 |
661 |
661 lemma "sub xs ys \<longleftrightarrow> (\<exists> N. xs = sublist ys N)" (is "?L = ?R") |
662 lemma "sub xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R") |
662 proof |
663 proof |
663 assume ?L |
664 assume ?L |
664 thus ?R |
665 then show ?R |
665 proof (induct) |
666 proof (induct) |
666 case emb_Nil show ?case by (metis sublist_empty) |
667 case emb_Nil show ?case by (metis sublist_empty) |
667 next |
668 next |
668 case (emb_Cons xs ys x) |
669 case (emb_Cons xs ys x) |
669 then obtain N where "xs = sublist ys N" by blast |
670 then obtain N where "xs = sublist ys N" by blast |
670 hence "xs = sublist (x#ys) (Suc ` N)" |
671 then have "xs = sublist (x#ys) (Suc ` N)" |
671 by (clarsimp simp add:sublist_Cons inj_image_mem_iff) |
672 by (clarsimp simp add:sublist_Cons inj_image_mem_iff) |
672 thus ?case by blast |
673 then show ?case by blast |
673 next |
674 next |
674 case (emb_Cons2 x y xs ys) |
675 case (emb_Cons2 x y xs ys) |
675 then obtain N where "xs = sublist ys N" by blast |
676 then obtain N where "xs = sublist ys N" by blast |
676 hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" |
677 then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" |
677 by (clarsimp simp add:sublist_Cons inj_image_mem_iff) |
678 by (clarsimp simp add:sublist_Cons inj_image_mem_iff) |
678 thus ?case unfolding `x = y` by blast |
679 then show ?case unfolding `x = y` by blast |
679 qed |
680 qed |
680 next |
681 next |
681 assume ?R |
682 assume ?R |
682 then obtain N where "xs = sublist ys N" .. |
683 then obtain N where "xs = sublist ys N" .. |
683 moreover have "sub (sublist ys N) ys" |
684 moreover have "sub (sublist ys N) ys" |
684 proof (induct ys arbitrary:N) |
685 proof (induct ys arbitrary: N) |
685 case Nil show ?case by simp |
686 case Nil show ?case by simp |
686 next |
687 next |
687 case Cons thus ?case by (auto simp: sublist_Cons) |
688 case Cons then show ?case by (auto simp: sublist_Cons) |
688 qed |
689 qed |
689 ultimately show ?L by simp |
690 ultimately show ?L by simp |
690 qed |
691 qed |
691 |
692 |
692 end |
693 end |