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@21305: using prems 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@21305: using prems 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: 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@21305: using prems 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: 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@21305: using prems 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: 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