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 \<le> ys == \<exists>zs. ys = xs @ zs"
wenzelm@10389:   strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (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 \<le> ys"
wenzelm@18730:   unfolding prefix_def by blast
wenzelm@10330: 
wenzelm@10389: lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
wenzelm@18730:   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@17201:   assumes lt: "xs < ys"
wenzelm@17201:     and r: "!!z zs. ys = xs @ z # zs ==> C"
wenzelm@17201:   shows C
wenzelm@10870: proof -
wenzelm@17201:   from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys"
wenzelm@18730:     unfolding strict_prefix_def prefix_def by blast
wenzelm@10870:   with r show ?thesis by (auto simp add: neq_Nil_conv)
wenzelm@10870: qed
wenzelm@10870: 
wenzelm@10389: lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
wenzelm@18730:   unfolding strict_prefix_def by blast
wenzelm@10330: 
wenzelm@10389: lemma strict_prefixE [elim?]:
wenzelm@10389:     "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
wenzelm@18730:   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]: "[] \<le> xs"
wenzelm@10389:   by (simp add: prefix_def)
wenzelm@10330: 
wenzelm@10330: theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
wenzelm@10389:   by (induct xs) (simp_all add: prefix_def)
wenzelm@10330: 
wenzelm@10330: lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
wenzelm@10389: proof
wenzelm@10389:   assume "xs \<le> ys @ [y]"
wenzelm@10389:   then obtain zs where zs: "ys @ [y] = xs @ zs" ..
wenzelm@10389:   show "xs = ys @ [y] \<or> xs \<le> ys"
wenzelm@10389:   proof (cases zs rule: rev_cases)
wenzelm@10389:     assume "zs = []"
wenzelm@10389:     with zs have "xs = ys @ [y]" by simp
wenzelm@10389:     thus ?thesis ..
wenzelm@10389:   next
wenzelm@10389:     fix z zs' assume "zs = zs' @ [z]"
wenzelm@10389:     with zs have "ys = xs @ zs'" by simp
wenzelm@10389:     hence "xs \<le> ys" ..
wenzelm@10389:     thus ?thesis ..
wenzelm@10389:   qed
wenzelm@10389: next
wenzelm@10389:   assume "xs = ys @ [y] \<or> xs \<le> ys"
wenzelm@10389:   thus "xs \<le> ys @ [y]"
wenzelm@10389:   proof
wenzelm@10389:     assume "xs = ys @ [y]"
wenzelm@10389:     thus ?thesis by simp
wenzelm@10389:   next
wenzelm@10389:     assume "xs \<le> ys"
wenzelm@10389:     then obtain zs where "ys = xs @ zs" ..
wenzelm@10389:     hence "ys @ [y] = xs @ (zs @ [y])" by simp
wenzelm@10389:     thus ?thesis ..
wenzelm@10389:   qed
wenzelm@10389: qed
wenzelm@10330: 
wenzelm@10330: lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
wenzelm@10389:   by (auto simp add: prefix_def)
wenzelm@10330: 
wenzelm@10330: lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
wenzelm@10389:   by (induct xs) simp_all
wenzelm@10330: 
wenzelm@10389: lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
wenzelm@10389: proof -
wenzelm@10389:   have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix)
wenzelm@10389:   thus ?thesis by simp
wenzelm@10389: qed
wenzelm@10330: 
wenzelm@10330: lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
wenzelm@10389: proof -
wenzelm@10389:   assume "xs \<le> ys"
wenzelm@10389:   then obtain us where "ys = xs @ us" ..
wenzelm@10389:   hence "ys @ zs = xs @ (us @ zs)" by simp
wenzelm@10389:   thus ?thesis ..
wenzelm@10389: qed
wenzelm@10330: 
nipkow@14300: lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
wenzelm@17201:   by (auto simp add: prefix_def)
nipkow@14300: 
wenzelm@10330: theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
wenzelm@10389:   by (cases xs) (auto simp add: prefix_def)
wenzelm@10330: 
wenzelm@10330: theorem prefix_append:
wenzelm@10330:     "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> 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 \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> 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 \<le> ys ==> length xs \<le> 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) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> 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 \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
wenzelm@17201:   by (auto simp add: prefix_def)
nipkow@14300: 
nipkow@14300: 
wenzelm@10389: subsection {* Parallel lists *}
wenzelm@10389: 
wenzelm@10389: constdefs
wenzelm@10389:   parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
wenzelm@10389:   "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
wenzelm@10389: 
wenzelm@10389: lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
wenzelm@18730:   unfolding parallel_def by blast
wenzelm@10330: 
wenzelm@10389: lemma parallelE [elim]:
wenzelm@10389:     "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
wenzelm@18730:   unfolding parallel_def by blast
wenzelm@10330: 
wenzelm@10389: theorem prefix_cases:
wenzelm@10389:   "(xs \<le> ys ==> C) ==>
wenzelm@10512:     (ys < xs ==> C) ==>
wenzelm@10389:     (xs \<parallel> ys ==> C) ==> C"
wenzelm@18730:   unfolding parallel_def strict_prefix_def by blast
wenzelm@10330: 
wenzelm@10389: theorem parallel_decomp:
wenzelm@10389:   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
wenzelm@10408: proof (induct xs rule: rev_induct)
wenzelm@11987:   case Nil
wenzelm@11987:   hence False by auto
wenzelm@11987:   thus ?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 \<le> 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] \<parallel> []" by auto
wenzelm@10408:       hence False by blast
wenzelm@10389:       thus ?thesis ..
wenzelm@10389:     next
wenzelm@10408:       fix c cs assume ys': "ys' = c # cs"
wenzelm@11987:       with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
wenzelm@10408:       hence "x \<noteq> 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@10512:     assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
wenzelm@11987:     with snoc have False by blast
wenzelm@10408:     thus ?thesis ..
wenzelm@10408:   next
wenzelm@10408:     assume "xs \<parallel> ys"
wenzelm@11987:     with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> 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: 
oheimb@14538: constdefs
wenzelm@17201:   postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
wenzelm@17201:   "xs >>= ys == \<exists>zs. xs = zs @ ys"
oheimb@14538: 
wenzelm@17201: lemma postfix_refl [simp, intro!]: "xs >>= xs"
wenzelm@14706:   by (auto simp add: postfix_def)
wenzelm@17201: lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs"
wenzelm@14706:   by (auto simp add: postfix_def)
wenzelm@17201: lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> 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@14706:   by (auto simp add:postfix_def)
oheimb@14538: 
wenzelm@17201: lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys"
wenzelm@14706:   by (auto simp add: postfix_def)
wenzelm@17201: lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys"
wenzelm@14706:   by (auto simp add: postfix_def)
oheimb@14538: 
wenzelm@17201: lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"
wenzelm@14706:   by (auto simp add: postfix_def)
wenzelm@17201: lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys"
wenzelm@14706:   by(auto simp add: postfix_def)
oheimb@14538: 
oheimb@14538: lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
wenzelm@18258:   by (induct zs) auto
wenzelm@17201: lemma postfix_is_subset: "xs >>= ys \<Longrightarrow> set ys \<subseteq> set xs"
wenzelm@14706:   by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
oheimb@14538: 
wenzelm@18258: lemma postfix_ConsD2_lemma: "x#xs = zs @ y#ys \<Longrightarrow> xs >>= ys"
wenzelm@18258:   by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
wenzelm@17201: lemma postfix_ConsD2: "x#xs >>= y#ys \<Longrightarrow> xs >>= ys"
wenzelm@14706:   by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
oheimb@14538: 
wenzelm@17201: lemma postfix2prefix: "(xs >>= ys) = (rev ys <= rev xs)"
wenzelm@14706:   apply (unfold prefix_def postfix_def, safe)
wenzelm@17201:    apply (rule_tac x = "rev zs" in exI, simp)
wenzelm@14706:   apply (rule_tac x = "rev zs" in exI)
wenzelm@14706:   apply (rule rev_is_rev_conv [THEN iffD1], simp)
wenzelm@14706:   done
wenzelm@17201: 
wenzelm@10330: end