src/HOL/Library/Sublist_Order.thy
author Christian Sternagel
Wed Aug 29 12:23:14 2012 +0900 (2012-08-29)
changeset 49083 01081bca31b6
parent 37765 26bdfb7b680b
child 49084 e3973567ed4f
permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
     1 (*  Title:      HOL/Library/Sublist_Order.thy
     2     Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
     3                 Florian Haftmann, Tobias Nipkow, TU Muenchen
     4 *)
     5 
     6 header {* Sublist Ordering *}
     7 
     8 theory Sublist_Order
     9 imports Main
    10 begin
    11 
    12 text {*
    13   This theory defines sublist ordering on lists.
    14   A list @{text ys} is a sublist of a list @{text xs},
    15   iff one obtains @{text ys} by erasing some elements from @{text xs}.
    16 *}
    17 
    18 subsection {* Definitions and basic lemmas *}
    19 
    20 instantiation list :: (type) ord
    21 begin
    22 
    23 inductive less_eq_list where
    24   empty [simp, intro!]: "[] \<le> xs"
    25   | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
    26   | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
    27 
    28 definition
    29   "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    30 
    31 instance proof qed
    32 
    33 end
    34 
    35 lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    36 by (induct rule: less_eq_list.induct) auto
    37 
    38 lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
    39 by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
    40 
    41 lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
    42 by (metis le_list_length linorder_not_less)
    43 
    44 lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
    45 by (auto dest: le_list_length)
    46 
    47 lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
    48 by (induct zs) (auto intro: drop)
    49 
    50 lemma [code]: "[] <= xs \<longleftrightarrow> True"
    51 by(metis less_eq_list.empty)
    52 
    53 lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
    54 by simp
    55 
    56 lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
    57 proof-
    58   { fix xs' ys'
    59     assume "xs' <= ys"
    60     hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
    61     proof induct
    62       case empty thus ?case by simp
    63     next
    64       case drop thus ?case by (metis less_eq_list.drop)
    65     next
    66       case take thus ?case by (simp add: drop)
    67     qed }
    68   from this[OF assms] show ?thesis by simp
    69 qed
    70 
    71 lemma le_list_drop_Cons2:
    72 assumes "x#xs <= x#ys" shows "xs <= ys"
    73 using assms
    74 proof cases
    75   case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
    76 qed simp_all
    77 
    78 lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
    79 shows "x ~= y \<Longrightarrow> x # xs <= ys"
    80 using assms proof cases qed auto
    81 
    82 lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
    83   (if x=y then xs <= ys else (x#xs) <= ys)"
    84 by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
    85 
    86 lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"
    87 by (induct zs) (auto intro: take)
    88 
    89 lemma le_list_Cons_EX:
    90   assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
    91 proof-
    92   { fix xys zs :: "'a list" assume "xys <= zs"
    93     hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
    94     proof induct
    95       case empty show ?case by simp
    96     next
    97       case take thus ?case by (metis list.inject self_append_conv2)
    98     next
    99       case drop thus ?case by (metis append_eq_Cons_conv)
   100     qed
   101   } with assms show ?thesis by blast
   102 qed
   103 
   104 instantiation list :: (type) order
   105 begin
   106 
   107 instance proof
   108   fix xs ys :: "'a list"
   109   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
   110 next
   111   fix xs :: "'a list"
   112   show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
   113 next
   114   fix xs ys :: "'a list"
   115   assume "xs <= ys"
   116   hence "ys <= xs \<longrightarrow> xs = ys"
   117   proof induct
   118     case empty show ?case by simp
   119   next
   120     case take thus ?case by simp
   121   next
   122     case drop thus ?case
   123       by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
   124   qed
   125   moreover assume "ys <= xs"
   126   ultimately show "xs = ys" by blast
   127 next
   128   fix xs ys zs :: "'a list"
   129   assume "xs <= ys"
   130   hence "ys <= zs \<longrightarrow> xs <= zs"
   131   proof (induct arbitrary:zs)
   132     case empty show ?case by simp
   133   next
   134     case (take xs ys x) show ?case
   135     proof
   136       assume "x # ys <= zs"
   137       with take show "x # xs <= zs"
   138         by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))
   139     qed
   140   next
   141     case drop thus ?case by (metis le_list_drop_Cons)
   142   qed
   143   moreover assume "ys <= zs"
   144   ultimately show "xs <= zs" by blast
   145 qed
   146 
   147 end
   148 
   149 lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
   150 by (auto dest: le_list_length)
   151 
   152 lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
   153 apply (induct rule:less_eq_list.induct)
   154   apply (metis eq_Nil_appendI le_list_drop_many)
   155  apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
   156 apply simp
   157 done
   158 
   159 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   160 by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
   161 
   162 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   163 by (metis empty order_less_le)
   164 
   165 lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
   166 by (metis empty less_list_def)
   167 
   168 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   169 by (unfold less_le) (auto intro: less_eq_list.drop)
   170 
   171 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
   172 by (metis le_list_Cons2_iff less_list_def)
   173 
   174 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   175 by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
   176 
   177 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
   178 by (metis le_list_take_many_iff less_list_def)
   179 
   180 
   181 subsection {* Appending elements *}
   182 
   183 lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
   184 proof
   185   { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
   186     hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
   187     proof (induct arbitrary: xs ys zs)
   188       case empty show ?case by simp
   189     next
   190       case (drop xs' ys' x)
   191       { assume "ys=[]" hence ?case using drop(1) by auto }
   192       moreover
   193       { fix us assume "ys = x#us"
   194         hence ?case using drop(2) by(simp add: less_eq_list.drop) }
   195       ultimately show ?case by (auto simp:Cons_eq_append_conv)
   196     next
   197       case (take xs' ys' x)
   198       { assume "xs=[]" hence ?case using take(1) by auto }
   199       moreover
   200       { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}
   201       moreover
   202       { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
   203       ultimately show ?case by (auto simp:Cons_eq_append_conv)
   204     qed }
   205   moreover assume ?L
   206   ultimately show ?R by blast
   207 next
   208   assume ?R thus ?L by(metis le_list_append_mono order_refl)
   209 qed
   210 
   211 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   212 by (unfold less_le) auto
   213 
   214 lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
   215 by (metis append_Nil2 empty le_list_append_mono)
   216 
   217 
   218 subsection {* Relation to standard list operations *}
   219 
   220 lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   221 by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
   222 
   223 lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
   224 by (induct xs) (auto intro: less_eq_list.drop)
   225 
   226 lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
   227 by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
   228 
   229 lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
   230 proof
   231   assume ?L
   232   thus ?R
   233   proof induct
   234     case empty show ?case by (metis sublist_empty)
   235   next
   236     case (drop xs ys x)
   237     then obtain N where "xs = sublist ys N" by blast
   238     hence "xs = sublist (x#ys) (Suc ` N)"
   239       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   240     thus ?case by blast
   241   next
   242     case (take xs ys x)
   243     then obtain N where "xs = sublist ys N" by blast
   244     hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   245       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   246     thus ?case by blast
   247   qed
   248 next
   249   assume ?R
   250   then obtain N where "xs = sublist ys N" ..
   251   moreover have "sublist ys N <= ys"
   252   proof (induct ys arbitrary:N)
   253     case Nil show ?case by simp
   254   next
   255     case Cons thus ?case by (auto simp add:sublist_Cons drop)
   256   qed
   257   ultimately show ?L by simp
   258 qed
   259 
   260 end