1 (*  Title:      HOL/Library/List_Prefix.thy

     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

     3 *)

     4 

     5 header {* List prefixes and postfixes *}

     6 

     7 theory List_Prefix

     8 imports List Main

     9 begin

    10 

    11 subsection {* Prefix order on lists *}

    12 

    13 instantiation list :: (type) "{order, bot}"

    14 begin

    15 

    16 definition

    17   prefix_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"

    18 

    19 definition

    20   strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"

    21 

    22 definition

    23   "bot = []"

    24 

    25 instance proof

    26 qed (auto simp add: prefix_def strict_prefix_def bot_list_def)

    27 

    28 end

    29 

    30 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"

    31   unfolding prefix_def by blast

    32 

    33 lemma prefixE [elim?]:

    34   assumes "xs \<le> ys"

    35   obtains zs where "ys = xs @ zs"

    36   using assms unfolding prefix_def by blast

    37 

    38 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"

    39   unfolding strict_prefix_def prefix_def by blast

    40 

    41 lemma strict_prefixE' [elim?]:

    42   assumes "xs < ys"

    43   obtains z zs where "ys = xs @ z # zs"

    44 proof -

    45   from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"

    46     unfolding strict_prefix_def prefix_def by blast

    47   with that show ?thesis by (auto simp add: neq_Nil_conv)

    48 qed

    49 

    50 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"

    51   unfolding strict_prefix_def by blast

    52 

    53 lemma strict_prefixE [elim?]:

    54   fixes xs ys :: "'a list"

    55   assumes "xs < ys"

    56   obtains "xs \<le> ys" and "xs \<noteq> ys"

    57   using assms unfolding strict_prefix_def by blast

    58 

    59 

    60 subsection {* Basic properties of prefixes *}

    61 

    62 theorem Nil_prefix [iff]: "[] \<le> xs"

    63   by (simp add: prefix_def)

    64 

    65 theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"

    66   by (induct xs) (simp_all add: prefix_def)

    67 

    68 lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"

    69 proof

    70   assume "xs \<le> ys @ [y]"

    71   then obtain zs where zs: "ys @ [y] = xs @ zs" ..

    72   show "xs = ys @ [y] \<or> xs \<le> ys"

    73     by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)

    74 next

    75   assume "xs = ys @ [y] \<or> xs \<le> ys"

    76   then show "xs \<le> ys @ [y]"

    77     by (metis order_eq_iff order_trans prefixI)

    78 qed

    79 

    80 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"

    81   by (auto simp add: prefix_def)

    82 

    83 lemma less_eq_list_code [code]:

    84   "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"

    85   "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"

    86   "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"

    87   by simp_all

    88 

    89 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"

    90   by (induct xs) simp_all

    91 

    92 lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"

    93   by (metis append_Nil2 append_self_conv order_eq_iff prefixI)

    94 

    95 lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"

    96   by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)

    97 

    98 lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"

    99   by (auto simp add: prefix_def)

   100 

   101 theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"

   102   by (cases xs) (auto simp add: prefix_def)

   103 

   104 theorem prefix_append:

   105   "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"

   106   apply (induct zs rule: rev_induct)

   107    apply force

   108   apply (simp del: append_assoc add: append_assoc [symmetric])

   109   apply (metis append_eq_appendI)

   110   done

   111 

   112 lemma append_one_prefix:

   113   "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"

   114   unfolding prefix_def

   115   by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj

   116     eq_Nil_appendI nth_drop')

   117 

   118 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"

   119   by (auto simp add: prefix_def)

   120 

   121 lemma prefix_same_cases:

   122   "(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"

   123   unfolding prefix_def by (metis append_eq_append_conv2)

   124 

   125 lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"

   126   by (auto simp add: prefix_def)

   127 

   128 lemma take_is_prefix: "take n xs \<le> xs"

   129   unfolding prefix_def by (metis append_take_drop_id)

   130 

   131 lemma map_prefixI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"

   132   by (auto simp: prefix_def)

   133 

   134 lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"

   135   by (auto simp: strict_prefix_def prefix_def)

   136 

   137 lemma strict_prefix_simps [simp, code]:

   138   "xs < [] \<longleftrightarrow> False"

   139   "[] < x # xs \<longleftrightarrow> True"

   140   "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"

   141   by (simp_all add: strict_prefix_def cong: conj_cong)

   142 

   143 lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"

   144   apply (induct n arbitrary: xs ys)

   145    apply (case_tac ys, simp_all)[1]

   146   apply (metis order_less_trans strict_prefixI take_is_prefix)

   147   done

   148 

   149 lemma not_prefix_cases:

   150   assumes pfx: "\<not> ps \<le> ls"

   151   obtains

   152     (c1) "ps \<noteq> []" and "ls = []"

   153   | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs"

   154   | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"

   155 proof (cases ps)

   156   case Nil then show ?thesis using pfx by simp

   157 next

   158   case (Cons a as)

   159   note c = `ps = a#as`

   160   show ?thesis

   161   proof (cases ls)

   162     case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)

   163   next

   164     case (Cons x xs)

   165     show ?thesis

   166     proof (cases "x = a")

   167       case True

   168       have "\<not> as \<le> xs" using pfx c Cons True by simp

   169       with c Cons True show ?thesis by (rule c2)

   170     next

   171       case False

   172       with c Cons show ?thesis by (rule c3)

   173     qed

   174   qed

   175 qed

   176 

   177 lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:

   178   assumes np: "\<not> ps \<le> ls"

   179     and base: "\<And>x xs. P (x#xs) []"

   180     and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"

   181     and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"

   182   shows "P ps ls" using np

   183 proof (induct ls arbitrary: ps)

   184   case Nil then show ?case

   185     by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)

   186 next

   187   case (Cons y ys)

   188   then have npfx: "\<not> ps \<le> (y # ys)" by simp

   189   then obtain x xs where pv: "ps = x # xs"

   190     by (rule not_prefix_cases) auto

   191   show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2)

   192 qed

   193 

   194 

   195 subsection {* Parallel lists *}

   196 

   197 definition

   198   parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50) where

   199   "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"

   200 

   201 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"

   202   unfolding parallel_def by blast

   203 

   204 lemma parallelE [elim]:

   205   assumes "xs \<parallel> ys"

   206   obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"

   207   using assms unfolding parallel_def by blast

   208 

   209 theorem prefix_cases:

   210   obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"

   211   unfolding parallel_def strict_prefix_def by blast

   212 

   213 theorem parallel_decomp:

   214   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"

   215 proof (induct xs rule: rev_induct)

   216   case Nil

   217   then have False by auto

   218   then show ?case ..

   219 next

   220   case (snoc x xs)

   221   show ?case

   222   proof (rule prefix_cases)

   223     assume le: "xs \<le> ys"

   224     then obtain ys' where ys: "ys = xs @ ys'" ..

   225     show ?thesis

   226     proof (cases ys')

   227       assume "ys' = []"

   228       then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)

   229     next

   230       fix c cs assume ys': "ys' = c # cs"

   231       then show ?thesis

   232         by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI

   233           same_prefix_prefix snoc.prems ys)

   234     qed

   235   next

   236     assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)

   237     with snoc have False by blast

   238     then show ?thesis ..

   239   next

   240     assume "xs \<parallel> ys"

   241     with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"

   242       and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"

   243       by blast

   244     from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp

   245     with neq ys show ?thesis by blast

   246   qed

   247 qed

   248 

   249 lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"

   250   apply (rule parallelI)

   251     apply (erule parallelE, erule conjE,

   252       induct rule: not_prefix_induct, simp+)+

   253   done

   254 

   255 lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"

   256   by (simp add: parallel_append)

   257 

   258 lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"

   259   unfolding parallel_def by auto

   260 

   261 

   262 subsection {* Postfix order on lists *}

   263 

   264 definition

   265   postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50) where

   266   "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"

   267 

   268 lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys"

   269   unfolding postfix_def by blast

   270 

   271 lemma postfixE [elim?]:

   272   assumes "xs >>= ys"

   273   obtains zs where "xs = zs @ ys"

   274   using assms unfolding postfix_def by blast

   275 

   276 lemma postfix_refl [iff]: "xs >>= xs"

   277   by (auto simp add: postfix_def)

   278 lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs"

   279   by (auto simp add: postfix_def)

   280 lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys"

   281   by (auto simp add: postfix_def)

   282 

   283 lemma Nil_postfix [iff]: "xs >>= []"

   284   by (simp add: postfix_def)

   285 lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])"

   286   by (auto simp add: postfix_def)

   287 

   288 lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys"

   289   by (auto simp add: postfix_def)

   290 lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys"

   291   by (auto simp add: postfix_def)

   292 

   293 lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"

   294   by (auto simp add: postfix_def)

   295 lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys"

   296   by (auto simp add: postfix_def)

   297 

   298 lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs"

   299 proof -

   300   assume "xs >>= ys"

   301   then obtain zs where "xs = zs @ ys" ..

   302   then show ?thesis by (induct zs) auto

   303 qed

   304 

   305 lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys"

   306 proof -

   307   assume "x#xs >>= y#ys"

   308   then obtain zs where "x#xs = zs @ y#ys" ..

   309   then show ?thesis

   310     by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)

   311 qed

   312 

   313 lemma postfix_to_prefix [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"

   314 proof

   315   assume "xs >>= ys"

   316   then obtain zs where "xs = zs @ ys" ..

   317   then have "rev xs = rev ys @ rev zs" by simp

   318   then show "rev ys <= rev xs" ..

   319 next

   320   assume "rev ys <= rev xs"

   321   then obtain zs where "rev xs = rev ys @ zs" ..

   322   then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp

   323   then have "xs = rev zs @ ys" by simp

   324   then show "xs >>= ys" ..

   325 qed

   326 

   327 lemma distinct_postfix: "distinct xs \<Longrightarrow> xs >>= ys \<Longrightarrow> distinct ys"

   328   by (clarsimp elim!: postfixE)

   329 

   330 lemma postfix_map: "xs >>= ys \<Longrightarrow> map f xs >>= map f ys"

   331   by (auto elim!: postfixE intro: postfixI)

   332 

   333 lemma postfix_drop: "as >>= drop n as"

   334   unfolding postfix_def

   335   apply (rule exI [where x = "take n as"])

   336   apply simp

   337   done

   338 

   339 lemma postfix_take: "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"

   340   by (clarsimp elim!: postfixE)

   341 

   342 lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"

   343   by blast

   344 

   345 lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x"

   346   by blast

   347 

   348 lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"

   349   unfolding parallel_def by simp

   350 

   351 lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"

   352   unfolding parallel_def by simp

   353 

   354 lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"

   355   by auto

   356 

   357 lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"

   358   by (metis Cons_prefix_Cons parallelE parallelI)

   359 

   360 lemma not_equal_is_parallel:

   361   assumes neq: "xs \<noteq> ys"

   362     and len: "length xs = length ys"

   363   shows "xs \<parallel> ys"

   364   using len neq

   365 proof (induct rule: list_induct2)

   366   case Nil

   367   then show ?case by simp

   368 next

   369   case (Cons a as b bs)

   370   have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact

   371   show ?case

   372   proof (cases "a = b")

   373     case True

   374     then have "as \<noteq> bs" using Cons by simp

   375     then show ?thesis by (rule Cons_parallelI2 [OF True ih])

   376   next

   377     case False

   378     then show ?thesis by (rule Cons_parallelI1)

   379   qed

   380 qed

   381 

   382 end