src/HOL/Library/Sublist_Order.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 57497 4106a2bc066a child 58881 b9556a055632 permissions -rw-r--r--
simpler proof
```     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 Sublist
```
```    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 definition
```
```    24   "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
```
```    25
```
```    26 definition
```
```    27   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
```
```    28
```
```    29 instance ..
```
```    30
```
```    31 end
```
```    32
```
```    33 instance list :: (type) order
```
```    34 proof
```
```    35   fix xs ys :: "'a list"
```
```    36   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def ..
```
```    37 next
```
```    38   fix xs :: "'a list"
```
```    39   show "xs \<le> xs" by (simp add: less_eq_list_def)
```
```    40 next
```
```    41   fix xs ys :: "'a list"
```
```    42   assume "xs <= ys" and "ys <= xs"
```
```    43   thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
```
```    44 next
```
```    45   fix xs ys zs :: "'a list"
```
```    46   assume "xs <= ys" and "ys <= zs"
```
```    47   thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
```
```    48 qed
```
```    49
```
```    50 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
```
```    51   list_emb.induct [of "op =", folded less_eq_list_def]
```
```    52 lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
```
```    53 lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
```
```    54 lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
```
```    55 lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
```
```    56 lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
```
```    57
```
```    58 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
```
```    59   by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
```
```    60
```
```    61 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
```
```    62   by (metis less_eq_list_def list_emb_Nil order_less_le)
```
```    63
```
```    64 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
```
```    65   by (metis list_emb_Nil less_eq_list_def less_list_def)
```
```    66
```
```    67 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
```
```    68   by (unfold less_le less_eq_list_def) (auto)
```
```    69
```
```    70 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
```
```    71   by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
```
```    72
```
```    73 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
```
```    74   by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
```
```    75
```
```    76 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
```
```    77   by (metis less_list_def less_eq_list_def sublisteq_append')
```
```    78
```
```    79 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
```
```    80   by (unfold less_le less_eq_list_def) auto
```
```    81
```
```    82 end
```