src/HOL/Library/Sublist_Order.thy
 author haftmann Mon Jul 12 08:58:13 2010 +0200 (2010-07-12) changeset 37765 26bdfb7b680b parent 33499 30e6e070bdb6 child 49084 e3973567ed4f permissions -rw-r--r--
dropped superfluous [code del]s
```     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
```