wenzelm@10330: (* Title: HOL/Library/List_Prefix.thy 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 haftmann@30663: imports List Main nipkow@15131: begin wenzelm@10330: wenzelm@10330: subsection {* Prefix order on lists *} wenzelm@10330: haftmann@37474: instantiation list :: (type) "{order, bot}" haftmann@25764: begin haftmann@25764: haftmann@25764: definition haftmann@37474: prefix_def: "xs \ ys \ (\zs. ys = xs @ zs)" wenzelm@10330: haftmann@25764: definition haftmann@37474: strict_prefix_def: "xs < ys \ xs \ ys \ xs \ (ys::'a list)" wenzelm@10330: haftmann@37474: definition haftmann@37474: "bot = []" haftmann@37474: haftmann@37474: instance proof haftmann@37474: qed (auto simp add: prefix_def strict_prefix_def bot_list_def) wenzelm@10330: haftmann@25764: end haftmann@25764: 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" nipkow@25564: by (metis append_Nil2 butlast_append butlast_snoc prefixI zs) wenzelm@10389: next wenzelm@10389: assume "xs = ys @ [y] \ xs \ ys" wenzelm@23254: then show "xs \ ys @ [y]" bulwahn@45236: by (metis order_eq_iff order_trans prefixI) 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: haftmann@37474: lemma less_eq_list_code [code]: haftmann@38857: "([]\'a\{equal, ord} list) \ xs \ True" haftmann@38857: "(x\'a\{equal, ord}) # xs \ [] \ False" haftmann@38857: "(x\'a\{equal, ord}) # xs \ y # ys \ x = y \ xs \ ys" haftmann@37474: by simp_all haftmann@37474: 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@25692: by (metis append_Nil2 append_self_conv order_eq_iff prefixI) nipkow@25665: wenzelm@10330: lemma prefix_prefix [simp]: "xs \ ys ==> xs \ ys @ zs" wenzelm@25692: by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI) nipkow@25665: 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: nipkow@25564: "(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]) nipkow@25564: apply (metis append_eq_appendI) wenzelm@10330: done wenzelm@10330: wenzelm@10330: lemma append_one_prefix: nipkow@25564: "xs \ ys ==> length xs < length ys ==> xs @ [ys ! length xs] \ ys" wenzelm@25692: unfolding prefix_def wenzelm@25692: by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj wenzelm@25692: eq_Nil_appendI nth_drop') nipkow@25665: 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: nipkow@25564: "(xs\<^isub>1::'a list) \ ys \ xs\<^isub>2 \ ys \ xs\<^isub>1 \ xs\<^isub>2 \ xs\<^isub>2 \ xs\<^isub>1" wenzelm@25692: unfolding prefix_def by (metis append_eq_append_conv2) nipkow@25665: nipkow@25564: lemma set_mono_prefix: "xs \ ys \ set xs \ set ys" wenzelm@25692: by (auto simp add: prefix_def) nipkow@14300: nipkow@25564: lemma take_is_prefix: "take n xs \ xs" wenzelm@25692: unfolding prefix_def by (metis append_take_drop_id) nipkow@25665: wenzelm@25692: lemma map_prefixI: "xs \ ys \ map f xs \ map f ys" wenzelm@25692: by (auto simp: prefix_def) kleing@25322: wenzelm@25692: lemma prefix_length_less: "xs < ys \ length xs < length ys" wenzelm@25692: by (auto simp: strict_prefix_def prefix_def) nipkow@25665: haftmann@37474: lemma strict_prefix_simps [simp, code]: haftmann@37474: "xs < [] \ False" haftmann@37474: "[] < x # xs \ True" haftmann@37474: "x # xs < y # ys \ x = y \ xs < ys" wenzelm@25692: by (simp_all add: strict_prefix_def cong: conj_cong) kleing@25299: nipkow@25564: lemma take_strict_prefix: "xs < ys \ take n xs < ys" wenzelm@25692: apply (induct n arbitrary: xs ys) wenzelm@25692: apply (case_tac ys, simp_all)[1] wenzelm@25692: apply (metis order_less_trans strict_prefixI take_is_prefix) wenzelm@25692: done kleing@25299: wenzelm@25355: lemma not_prefix_cases: kleing@25299: assumes pfx: "\ ps \ ls" wenzelm@25356: obtains wenzelm@25356: (c1) "ps \ []" and "ls = []" wenzelm@25356: | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\ as \ xs" wenzelm@25356: | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \ a" kleing@25299: proof (cases ps) wenzelm@25692: case Nil then show ?thesis using pfx by simp kleing@25299: next kleing@25299: case (Cons a as) wenzelm@25692: note c = `ps = a#as` kleing@25299: show ?thesis kleing@25299: proof (cases ls) wenzelm@25692: case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil) kleing@25299: next kleing@25299: case (Cons x xs) kleing@25299: show ?thesis kleing@25299: proof (cases "x = a") wenzelm@25355: case True wenzelm@25355: have "\ as \ xs" using pfx c Cons True by simp wenzelm@25355: with c Cons True show ?thesis by (rule c2) wenzelm@25355: next wenzelm@25355: case False wenzelm@25355: with c Cons 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" wenzelm@25356: and base: "\x xs. P (x#xs) []" wenzelm@25356: and r1: "\x xs y ys. x \ y \ P (x#xs) (y#ys)" wenzelm@25356: and r2: "\x xs y ys. \ x = y; \ xs \ ys; P xs ys \ \ P (x#xs) (y#ys)" wenzelm@25356: shows "P ps ls" using np kleing@25299: proof (induct ls arbitrary: ps) wenzelm@25355: case Nil then show ?case kleing@25299: by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) kleing@25299: next wenzelm@25355: case (Cons y ys) wenzelm@25355: then have npfx: "\ ps \ (y # ys)" by simp wenzelm@25355: then obtain x xs where pv: "ps = x # xs" kleing@25299: by (rule not_prefix_cases) auto nipkow@25564: show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2) kleing@25299: qed nipkow@14300: wenzelm@25356: 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@25692: unfolding parallel_def by blast wenzelm@10330: wenzelm@10389: lemma parallelE [elim]: wenzelm@25692: assumes "xs \ ys" wenzelm@25692: obtains "\ xs \ ys \ \ ys \ xs" wenzelm@25692: using assms unfolding parallel_def by blast wenzelm@10330: wenzelm@10389: theorem prefix_cases: wenzelm@25692: obtains "xs \ ys" | "ys < xs" | "xs \ ys" wenzelm@25692: 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') nipkow@25564: assume "ys' = []" wenzelm@25692: then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys) wenzelm@10389: next wenzelm@10408: fix c cs assume ys': "ys' = c # cs" wenzelm@25692: then show ?thesis wenzelm@25692: by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI wenzelm@25692: same_prefix_prefix snoc.prems ys) 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: nipkow@25564: lemma parallel_append: "a \ b \ a @ c \ b @ d" wenzelm@25692: apply (rule parallelI) wenzelm@25692: apply (erule parallelE, erule conjE, wenzelm@25692: induct rule: not_prefix_induct, simp+)+ wenzelm@25692: done kleing@25299: wenzelm@25692: lemma parallel_appendI: "xs \ ys \ x = xs @ xs' \ y = ys @ ys' \ x \ y" wenzelm@25692: by (simp add: parallel_append) kleing@25299: wenzelm@25692: lemma parallel_commute: "a \ b \ b \ a" wenzelm@25692: unfolding parallel_def by auto oheimb@14538: wenzelm@25356: 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@25692: unfolding postfix_def by blast wenzelm@21305: wenzelm@21305: lemma postfixE [elim?]: wenzelm@25692: assumes "xs >>= ys" wenzelm@25692: obtains zs where "xs = zs @ ys" wenzelm@25692: 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: haftmann@37474: lemma postfix_to_prefix [code]: "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: nipkow@25564: lemma distinct_postfix: "distinct xs \ xs >>= ys \ distinct ys" wenzelm@25692: by (clarsimp elim!: postfixE) kleing@25299: nipkow@25564: lemma postfix_map: "xs >>= ys \ map f xs >>= map f ys" wenzelm@25692: by (auto elim!: postfixE intro: postfixI) kleing@25299: wenzelm@25356: lemma postfix_drop: "as >>= drop n as" wenzelm@25692: unfolding postfix_def wenzelm@25692: apply (rule exI [where x = "take n as"]) wenzelm@25692: apply simp wenzelm@25692: done kleing@25299: nipkow@25564: lemma postfix_take: "xs >>= ys \ xs = take (length xs - length ys) xs @ ys" wenzelm@25692: by (clarsimp elim!: postfixE) kleing@25299: wenzelm@25356: lemma parallelD1: "x \ y \ \ x \ y" wenzelm@25692: by blast kleing@25299: wenzelm@25356: lemma parallelD2: "x \ y \ \ y \ x" wenzelm@25692: by blast wenzelm@25355: wenzelm@25355: lemma parallel_Nil1 [simp]: "\ x \ []" wenzelm@25692: unfolding parallel_def by simp wenzelm@25355: kleing@25299: lemma parallel_Nil2 [simp]: "\ [] \ x" wenzelm@25692: unfolding parallel_def by simp kleing@25299: nipkow@25564: lemma Cons_parallelI1: "a \ b \ a # as \ b # bs" wenzelm@25692: by auto kleing@25299: nipkow@25564: lemma Cons_parallelI2: "\ a = b; as \ bs \ \ a # as \ b # bs" wenzelm@25692: by (metis Cons_prefix_Cons parallelE parallelI) nipkow@25665: kleing@25299: lemma not_equal_is_parallel: kleing@25299: assumes neq: "xs \ ys" wenzelm@25356: and len: "length xs = length ys" wenzelm@25356: shows "xs \ ys" kleing@25299: using len neq wenzelm@25355: proof (induct rule: list_induct2) haftmann@26445: case Nil wenzelm@25356: then show ?case by simp kleing@25299: next haftmann@26445: case (Cons a as b bs) wenzelm@25355: have ih: "as \ bs \ as \ bs" by fact kleing@25299: show ?case kleing@25299: proof (cases "a = b") wenzelm@25355: case True haftmann@26445: then have "as \ bs" using Cons by simp wenzelm@25355: then show ?thesis by (rule Cons_parallelI2 [OF True ih]) kleing@25299: next kleing@25299: case False wenzelm@25355: then show ?thesis by (rule Cons_parallelI1) kleing@25299: qed kleing@25299: qed haftmann@22178: wenzelm@10330: end