wenzelm@10330: (* Title: HOL/Library/List_Prefix.thy wenzelm@10330: ID: $Id$ wenzelm@10330: Author: Tobias Nipkow and Markus Wenzel, TU Muenchen wenzelm@10330: *) wenzelm@10330: wenzelm@14706: header {* List prefixes and postfixes *} wenzelm@10330: nipkow@15131: theory List_Prefix nipkow@15140: imports Main nipkow@15131: begin wenzelm@10330: wenzelm@10330: subsection {* Prefix order on lists *} wenzelm@10330: wenzelm@12338: instance list :: (type) ord .. wenzelm@10330: wenzelm@10330: defs (overloaded) wenzelm@10389: prefix_def: "xs \ ys == \zs. ys = xs @ zs" wenzelm@10389: strict_prefix_def: "xs < ys == xs \ ys \ xs \ (ys::'a list)" wenzelm@10330: wenzelm@12338: instance list :: (type) order wenzelm@10389: by intro_classes (auto simp add: prefix_def strict_prefix_def) wenzelm@10330: wenzelm@10389: lemma prefixI [intro?]: "ys = xs @ zs ==> xs \ ys" wenzelm@18730: unfolding prefix_def by blast wenzelm@10330: wenzelm@21305: lemma prefixE [elim?]: wenzelm@21305: assumes "xs \ ys" wenzelm@21305: obtains zs where "ys = xs @ zs" wenzelm@23394: using assms unfolding prefix_def by blast wenzelm@10330: wenzelm@10870: lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" wenzelm@18730: unfolding strict_prefix_def prefix_def by blast wenzelm@10870: wenzelm@10870: lemma strict_prefixE' [elim?]: wenzelm@21305: assumes "xs < ys" wenzelm@21305: obtains z zs where "ys = xs @ z # zs" wenzelm@10870: proof - wenzelm@21305: from `xs < ys` obtain us where "ys = xs @ us" and "xs \ ys" wenzelm@18730: unfolding strict_prefix_def prefix_def by blast wenzelm@21305: with that show ?thesis by (auto simp add: neq_Nil_conv) wenzelm@10870: qed wenzelm@10870: wenzelm@10389: lemma strict_prefixI [intro?]: "xs \ ys ==> xs \ ys ==> xs < (ys::'a list)" wenzelm@18730: unfolding strict_prefix_def by blast wenzelm@10330: wenzelm@10389: lemma strict_prefixE [elim?]: wenzelm@21305: fixes xs ys :: "'a list" wenzelm@21305: assumes "xs < ys" wenzelm@21305: obtains "xs \ ys" and "xs \ ys" wenzelm@23394: using assms unfolding strict_prefix_def by blast wenzelm@10330: wenzelm@10330: wenzelm@10389: subsection {* Basic properties of prefixes *} wenzelm@10330: wenzelm@10330: theorem Nil_prefix [iff]: "[] \ xs" wenzelm@10389: by (simp add: prefix_def) wenzelm@10330: wenzelm@10330: theorem prefix_Nil [simp]: "(xs \ []) = (xs = [])" wenzelm@10389: by (induct xs) (simp_all add: prefix_def) wenzelm@10330: wenzelm@10330: lemma prefix_snoc [simp]: "(xs \ ys @ [y]) = (xs = ys @ [y] \ xs \ ys)" wenzelm@10389: proof wenzelm@10389: assume "xs \ ys @ [y]" wenzelm@10389: then obtain zs where zs: "ys @ [y] = xs @ zs" .. wenzelm@10389: show "xs = ys @ [y] \ xs \ ys" wenzelm@10389: proof (cases zs rule: rev_cases) wenzelm@10389: assume "zs = []" wenzelm@10389: with zs have "xs = ys @ [y]" by simp wenzelm@23254: then show ?thesis .. wenzelm@10389: next wenzelm@10389: fix z zs' assume "zs = zs' @ [z]" wenzelm@10389: with zs have "ys = xs @ zs'" by simp wenzelm@23254: then have "xs \ ys" .. wenzelm@23254: then show ?thesis .. wenzelm@10389: qed wenzelm@10389: next wenzelm@10389: assume "xs = ys @ [y] \ xs \ ys" wenzelm@23254: then show "xs \ ys @ [y]" wenzelm@10389: proof wenzelm@10389: assume "xs = ys @ [y]" wenzelm@23254: then show ?thesis by simp wenzelm@10389: next wenzelm@10389: assume "xs \ ys" wenzelm@10389: then obtain zs where "ys = xs @ zs" .. wenzelm@23254: then have "ys @ [y] = xs @ (zs @ [y])" by simp wenzelm@23254: then show ?thesis .. wenzelm@10389: qed wenzelm@10389: qed wenzelm@10330: wenzelm@10330: lemma Cons_prefix_Cons [simp]: "(x # xs \ y # ys) = (x = y \ xs \ ys)" wenzelm@10389: by (auto simp add: prefix_def) wenzelm@10330: wenzelm@10330: lemma same_prefix_prefix [simp]: "(xs @ ys \ xs @ zs) = (ys \ zs)" wenzelm@10389: by (induct xs) simp_all wenzelm@10330: wenzelm@10389: lemma same_prefix_nil [iff]: "(xs @ ys \ xs) = (ys = [])" wenzelm@10389: proof - wenzelm@10389: have "(xs @ ys \ xs @ []) = (ys \ [])" by (rule same_prefix_prefix) wenzelm@23254: then show ?thesis by simp wenzelm@10389: qed wenzelm@10330: wenzelm@10330: lemma prefix_prefix [simp]: "xs \ ys ==> xs \ ys @ zs" wenzelm@10389: proof - wenzelm@10389: assume "xs \ ys" wenzelm@10389: then obtain us where "ys = xs @ us" .. wenzelm@23254: then have "ys @ zs = xs @ (us @ zs)" by simp wenzelm@23254: then show ?thesis .. wenzelm@10389: qed wenzelm@10330: nipkow@14300: lemma append_prefixD: "xs @ ys \ zs \ xs \ zs" wenzelm@17201: by (auto simp add: prefix_def) nipkow@14300: wenzelm@10330: theorem prefix_Cons: "(xs \ y # ys) = (xs = [] \ (\zs. xs = y # zs \ zs \ ys))" wenzelm@10389: by (cases xs) (auto simp add: prefix_def) wenzelm@10330: wenzelm@10330: theorem prefix_append: wenzelm@10330: "(xs \ ys @ zs) = (xs \ ys \ (\us. xs = ys @ us \ us \ zs))" wenzelm@10330: apply (induct zs rule: rev_induct) wenzelm@10330: apply force wenzelm@10330: apply (simp del: append_assoc add: append_assoc [symmetric]) wenzelm@10330: apply simp wenzelm@10330: apply blast wenzelm@10330: done wenzelm@10330: wenzelm@10330: lemma append_one_prefix: wenzelm@10330: "xs \ ys ==> length xs < length ys ==> xs @ [ys ! length xs] \ ys" wenzelm@10330: apply (unfold prefix_def) wenzelm@10330: apply (auto simp add: nth_append) wenzelm@10389: apply (case_tac zs) wenzelm@10330: apply auto wenzelm@10330: done wenzelm@10330: wenzelm@10330: theorem prefix_length_le: "xs \ ys ==> length xs \ length ys" wenzelm@10389: by (auto simp add: prefix_def) wenzelm@10330: nipkow@14300: lemma prefix_same_cases: wenzelm@17201: "(xs\<^isub>1::'a list) \ ys \ xs\<^isub>2 \ ys \ xs\<^isub>1 \ xs\<^isub>2 \ xs\<^isub>2 \ xs\<^isub>1" wenzelm@17201: apply (simp add: prefix_def) wenzelm@17201: apply (erule exE)+ wenzelm@17201: apply (simp add: append_eq_append_conv_if split: if_splits) wenzelm@17201: apply (rule disjI2) wenzelm@17201: apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI) wenzelm@17201: apply clarify wenzelm@17201: apply (drule sym) wenzelm@17201: apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1]) wenzelm@17201: apply simp wenzelm@17201: apply (rule disjI1) wenzelm@17201: apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI) wenzelm@17201: apply clarify wenzelm@17201: apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2]) wenzelm@17201: apply simp wenzelm@17201: done nipkow@14300: nipkow@14300: lemma set_mono_prefix: wenzelm@17201: "xs \ ys \ set xs \ set ys" wenzelm@17201: by (auto simp add: prefix_def) nipkow@14300: kleing@25299: lemma take_is_prefix: kleing@25299: "take n xs \ xs" kleing@25299: apply (simp add: prefix_def) kleing@25299: apply (rule_tac x="drop n xs" in exI) kleing@25299: apply simp kleing@25299: done kleing@25299: kleing@25322: lemma map_prefixI: kleing@25322: "xs \ ys \ map f xs \ map f ys" kleing@25322: by (clarsimp simp: prefix_def) kleing@25322: kleing@25299: lemma prefix_length_less: kleing@25299: "xs < ys \ length xs < length ys" kleing@25299: apply (clarsimp simp: strict_prefix_def) kleing@25299: apply (frule prefix_length_le) kleing@25299: apply (rule ccontr, simp) kleing@25299: apply (clarsimp simp: prefix_def) kleing@25299: done kleing@25299: kleing@25299: lemma strict_prefix_simps [simp]: kleing@25299: "xs < [] = False" kleing@25299: "[] < (x # xs) = True" kleing@25299: "(x # xs) < (y # ys) = (x = y \ xs < ys)" kleing@25299: by (simp_all add: strict_prefix_def cong: conj_cong) kleing@25299: kleing@25299: lemma take_strict_prefix: kleing@25299: "xs < ys \ take n xs < ys" kleing@25299: apply (induct n arbitrary: xs ys) kleing@25299: apply (case_tac ys, simp_all)[1] kleing@25299: apply (case_tac xs, simp) kleing@25299: apply (case_tac ys, simp_all) kleing@25299: done kleing@25299: kleing@25299: lemma not_prefix_cases: kleing@25299: assumes pfx: "\ ps \ ls" kleing@25299: and c1: "\ ps \ []; ls = [] \ \ R" kleing@25299: and c2: "\a as x xs. \ ps = a#as; ls = x#xs; x = a; \ as \ xs\ \ R" kleing@25299: and c3: "\a as x xs. \ ps = a#as; ls = x#xs; x \ a\ \ R" kleing@25299: shows "R" kleing@25299: proof (cases ps) kleing@25299: case Nil thus ?thesis using pfx by simp kleing@25299: next kleing@25299: case (Cons a as) kleing@25299: kleing@25299: hence c: "ps = a#as" . kleing@25299: kleing@25299: show ?thesis kleing@25299: proof (cases ls) kleing@25299: case Nil thus ?thesis kleing@25299: by (intro c1, simp add: Cons) kleing@25299: next kleing@25299: case (Cons x xs) kleing@25299: show ?thesis kleing@25299: proof (cases "x = a") kleing@25299: case True kleing@25299: show ?thesis kleing@25299: proof (intro c2) kleing@25299: show "\ as \ xs" using pfx c Cons True kleing@25299: by simp kleing@25299: qed kleing@25299: next kleing@25299: case False kleing@25299: show ?thesis by (rule c3) kleing@25299: qed kleing@25299: qed kleing@25299: qed kleing@25299: kleing@25299: lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: kleing@25299: assumes np: "\ ps \ ls" kleing@25299: and base: "\x xs. P (x#xs) []" kleing@25299: and r1: "\x xs y ys. x \ y \ P (x#xs) (y#ys)" kleing@25299: and r2: "\x xs y ys. \ x = y; \ xs \ ys; P xs ys \ \ P (x#xs) (y#ys)" kleing@25299: shows "P ps ls" kleing@25299: using np kleing@25299: proof (induct ls arbitrary: ps) kleing@25299: case Nil thus ?case kleing@25299: by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) kleing@25299: next kleing@25299: case (Cons y ys) kleing@25299: hence npfx: "\ ps \ (y # ys)" by simp kleing@25299: then obtain x xs where pv: "ps = x # xs" kleing@25299: by (rule not_prefix_cases) auto kleing@25299: kleing@25299: from Cons kleing@25299: have ih: "\ps. \ps \ ys \ P ps ys" by simp kleing@25299: kleing@25299: show ?case using npfx kleing@25299: by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih) kleing@25299: qed nipkow@14300: wenzelm@10389: subsection {* Parallel lists *} wenzelm@10389: wenzelm@19086: definition wenzelm@21404: parallel :: "'a list => 'a list => bool" (infixl "\" 50) where wenzelm@19086: "(xs \ ys) = (\ xs \ ys \ \ ys \ xs)" wenzelm@10389: wenzelm@10389: lemma parallelI [intro]: "\ xs \ ys ==> \ ys \ xs ==> xs \ ys" wenzelm@18730: unfolding parallel_def by blast wenzelm@10330: wenzelm@10389: lemma parallelE [elim]: wenzelm@21305: assumes "xs \ ys" wenzelm@21305: obtains "\ xs \ ys \ \ ys \ xs" wenzelm@23394: using assms unfolding parallel_def by blast wenzelm@10330: wenzelm@10389: theorem prefix_cases: wenzelm@21305: obtains "xs \ ys" | "ys < xs" | "xs \ ys" wenzelm@18730: unfolding parallel_def strict_prefix_def by blast wenzelm@10330: wenzelm@10389: theorem parallel_decomp: wenzelm@10389: "xs \ ys ==> \as b bs c cs. b \ c \ xs = as @ b # bs \ ys = as @ c # cs" wenzelm@10408: proof (induct xs rule: rev_induct) wenzelm@11987: case Nil wenzelm@23254: then have False by auto wenzelm@23254: then show ?case .. wenzelm@10408: next wenzelm@11987: case (snoc x xs) wenzelm@11987: show ?case wenzelm@10408: proof (rule prefix_cases) wenzelm@10408: assume le: "xs \ ys" wenzelm@10408: then obtain ys' where ys: "ys = xs @ ys'" .. wenzelm@10408: show ?thesis wenzelm@10408: proof (cases ys') wenzelm@10408: assume "ys' = []" with ys have "xs = ys" by simp wenzelm@11987: with snoc have "[x] \ []" by auto wenzelm@23254: then have False by blast wenzelm@23254: then show ?thesis .. wenzelm@10389: next wenzelm@10408: fix c cs assume ys': "ys' = c # cs" wenzelm@11987: with snoc ys have "xs @ [x] \ xs @ c # cs" by (simp only:) wenzelm@23254: then have "x \ c" by auto wenzelm@10408: moreover have "xs @ [x] = xs @ x # []" by simp wenzelm@10408: moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) wenzelm@10408: ultimately show ?thesis by blast wenzelm@10389: qed wenzelm@10408: next wenzelm@23254: assume "ys < xs" then have "ys \ xs @ [x]" by (simp add: strict_prefix_def) wenzelm@11987: with snoc have False by blast wenzelm@23254: then show ?thesis .. wenzelm@10408: next wenzelm@10408: assume "xs \ ys" wenzelm@11987: with snoc obtain as b bs c cs where neq: "(b::'a) \ c" wenzelm@10408: and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" wenzelm@10408: by blast wenzelm@10408: from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp wenzelm@10408: with neq ys show ?thesis by blast wenzelm@10389: qed wenzelm@10389: qed wenzelm@10330: kleing@25299: lemma parallel_append: kleing@25299: "a \ b \ a @ c \ b @ d" kleing@25299: by (rule parallelI) kleing@25299: (erule parallelE, erule conjE, kleing@25299: induct rule: not_prefix_induct, simp+)+ kleing@25299: kleing@25299: lemma parallel_appendI: kleing@25299: "\ xs \ ys; x = xs @ xs' ; y = ys @ ys' \ \ x \ y" kleing@25299: by simp (rule parallel_append) kleing@25299: kleing@25299: lemma parallel_commute: kleing@25299: "(a \ b) = (b \ a)" kleing@25299: unfolding parallel_def by auto oheimb@14538: oheimb@14538: subsection {* Postfix order on lists *} wenzelm@17201: wenzelm@19086: definition wenzelm@21404: postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where wenzelm@19086: "(xs >>= ys) = (\zs. xs = zs @ ys)" oheimb@14538: wenzelm@21305: lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" wenzelm@21305: unfolding postfix_def by blast wenzelm@21305: wenzelm@21305: lemma postfixE [elim?]: wenzelm@21305: assumes "xs >>= ys" wenzelm@21305: obtains zs where "xs = zs @ ys" wenzelm@23394: using assms unfolding postfix_def by blast wenzelm@21305: wenzelm@21305: lemma postfix_refl [iff]: "xs >>= xs" wenzelm@14706: by (auto simp add: postfix_def) wenzelm@17201: lemma postfix_trans: "\xs >>= ys; ys >>= zs\ \ xs >>= zs" wenzelm@14706: by (auto simp add: postfix_def) wenzelm@17201: lemma postfix_antisym: "\xs >>= ys; ys >>= xs\ \ xs = ys" wenzelm@14706: by (auto simp add: postfix_def) oheimb@14538: wenzelm@17201: lemma Nil_postfix [iff]: "xs >>= []" wenzelm@14706: by (simp add: postfix_def) wenzelm@17201: lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" wenzelm@21305: by (auto simp add: postfix_def) oheimb@14538: wenzelm@17201: lemma postfix_ConsI: "xs >>= ys \ x#xs >>= ys" wenzelm@14706: by (auto simp add: postfix_def) wenzelm@17201: lemma postfix_ConsD: "xs >>= y#ys \ xs >>= ys" wenzelm@14706: by (auto simp add: postfix_def) oheimb@14538: wenzelm@17201: lemma postfix_appendI: "xs >>= ys \ zs @ xs >>= ys" wenzelm@14706: by (auto simp add: postfix_def) wenzelm@17201: lemma postfix_appendD: "xs >>= zs @ ys \ xs >>= ys" wenzelm@21305: by (auto simp add: postfix_def) oheimb@14538: wenzelm@21305: lemma postfix_is_subset: "xs >>= ys ==> set ys \ set xs" wenzelm@21305: proof - wenzelm@21305: assume "xs >>= ys" wenzelm@21305: then obtain zs where "xs = zs @ ys" .. wenzelm@21305: then show ?thesis by (induct zs) auto wenzelm@21305: qed oheimb@14538: wenzelm@21305: lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" wenzelm@21305: proof - wenzelm@21305: assume "x#xs >>= y#ys" wenzelm@21305: then obtain zs where "x#xs = zs @ y#ys" .. wenzelm@21305: then show ?thesis wenzelm@21305: by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) wenzelm@21305: qed oheimb@14538: wenzelm@21305: lemma postfix_to_prefix: "xs >>= ys \ rev ys \ rev xs" wenzelm@21305: proof wenzelm@21305: assume "xs >>= ys" wenzelm@21305: then obtain zs where "xs = zs @ ys" .. wenzelm@21305: then have "rev xs = rev ys @ rev zs" by simp wenzelm@21305: then show "rev ys <= rev xs" .. wenzelm@21305: next wenzelm@21305: assume "rev ys <= rev xs" wenzelm@21305: then obtain zs where "rev xs = rev ys @ zs" .. wenzelm@21305: then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp wenzelm@21305: then have "xs = rev zs @ ys" by simp wenzelm@21305: then show "xs >>= ys" .. wenzelm@21305: qed wenzelm@17201: kleing@25299: lemma distinct_postfix: kleing@25299: assumes dx: "distinct xs" kleing@25299: and pf: "xs >>= ys" kleing@25299: shows "distinct ys" kleing@25299: using dx pf by (clarsimp elim!: postfixE) kleing@25299: kleing@25299: lemma postfix_map: kleing@25299: assumes pf: "xs >>= ys" kleing@25299: shows "map f xs >>= map f ys" kleing@25299: using pf by (auto elim!: postfixE intro: postfixI) kleing@25299: kleing@25299: lemma postfix_drop: kleing@25299: "as >>= drop n as" kleing@25299: unfolding postfix_def kleing@25299: by (rule exI [where x = "take n as"]) simp kleing@25299: kleing@25299: lemma postfix_take: kleing@25299: "xs >>= ys \ xs = take (length xs - length ys) xs @ ys" kleing@25299: by (clarsimp elim!: postfixE) kleing@25299: kleing@25299: lemma parallelD1: kleing@25299: "x \ y \ \ x \ y" by blast kleing@25299: kleing@25299: lemma parallelD2: kleing@25299: "x \ y \ \ y \ x" by blast kleing@25299: kleing@25299: lemma parallel_Nil1 [simp]: "\ x \ []" kleing@25299: unfolding parallel_def by simp kleing@25299: kleing@25299: lemma parallel_Nil2 [simp]: "\ [] \ x" kleing@25299: unfolding parallel_def by simp kleing@25299: kleing@25299: lemma Cons_parallelI1: kleing@25299: "a \ b \ a # as \ b # bs" by auto kleing@25299: kleing@25299: lemma Cons_parallelI2: kleing@25299: "\ a = b; as \ bs \ \ a # as \ b # bs" kleing@25299: apply simp kleing@25299: apply (rule parallelI) kleing@25299: apply simp kleing@25299: apply (erule parallelD1) kleing@25299: apply simp kleing@25299: apply (erule parallelD2) kleing@25299: done kleing@25299: kleing@25299: lemma not_equal_is_parallel: kleing@25299: assumes neq: "xs \ ys" kleing@25299: and len: "length xs = length ys" kleing@25299: shows "xs \ ys" kleing@25299: using len neq kleing@25299: proof (induct rule: list_induct2) kleing@25299: case 1 thus ?case by simp kleing@25299: next kleing@25299: case (2 a as b bs) kleing@25299: kleing@25299: have ih: "as \ bs \ as \ bs" . kleing@25299: kleing@25299: show ?case kleing@25299: proof (cases "a = b") kleing@25299: case True kleing@25299: hence "as \ bs" using 2 by simp kleing@25299: kleing@25299: thus ?thesis by (rule Cons_parallelI2 [OF True ih]) kleing@25299: next kleing@25299: case False kleing@25299: thus ?thesis by (rule Cons_parallelI1) kleing@25299: qed kleing@25299: qed haftmann@22178: haftmann@22178: subsection {* Exeuctable code *} haftmann@22178: haftmann@22178: lemma less_eq_code [code func]: haftmann@22178: "([]\'a\{eq, ord} list) \ xs \ True" haftmann@22178: "(x\'a\{eq, ord}) # xs \ [] \ False" haftmann@22178: "(x\'a\{eq, ord}) # xs \ y # ys \ x = y \ xs \ ys" haftmann@22178: by simp_all haftmann@22178: haftmann@22178: lemma less_code [code func]: haftmann@22178: "xs < ([]\'a\{eq, ord} list) \ False" haftmann@22178: "[] < (x\'a\{eq, ord})# xs \ True" haftmann@22178: "(x\'a\{eq, ord}) # xs < y # ys \ x = y \ xs < ys" haftmann@22178: unfolding strict_prefix_def by auto haftmann@22178: haftmann@22178: lemmas [code func] = postfix_to_prefix haftmann@22178: wenzelm@10330: end