src/HOL/Library/Sublist_Order.thy
author Christian Sternagel
Wed Aug 29 16:25:35 2012 +0900 (2012-08-29)
changeset 49085 4eef5c2ff5ad
parent 49084 e3973567ed4f
child 49088 5cd8b4426a57
permissions -rw-r--r--
introduced "sub" as abbreviation for "emb (op =)";
Sublist_Order is now based on Sublist.sub;
simplified and moved most lemmas on sub from Sublist_Order to Sublist;
Sublist_Order merely contains ord and order instances for sub plus some lemmas on the strict part of the order
     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
    10   Main
    11   Sublist
    12 begin
    13 
    14 text {*
    15   This theory defines sublist ordering on lists.
    16   A list @{text ys} is a sublist of a list @{text xs},
    17   iff one obtains @{text ys} by erasing some elements from @{text xs}.
    18 *}
    19 
    20 subsection {* Definitions and basic lemmas *}
    21 
    22 instantiation list :: (type) ord
    23 begin
    24 
    25 definition
    26   "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
    27 
    28 definition
    29   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    30 
    31 instance ..
    32 
    33 end
    34 
    35 instance list :: (type) order
    36 proof
    37   fix xs ys :: "'a list"
    38   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
    39 next
    40   fix xs :: "'a list"
    41   show "xs \<le> xs" by (simp add: less_eq_list_def)
    42 next
    43   fix xs ys :: "'a list"
    44   assume "xs <= ys" and "ys <= xs"
    45   thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
    46 next
    47   fix xs ys zs :: "'a list"
    48   assume "xs <= ys" and "ys <= zs"
    49   thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
    50 qed
    51 
    52 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    53   by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
    54 
    55 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
    56   by (metis less_eq_list_def emb_Nil order_less_le)
    57 
    58 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
    59   by (metis emb_Nil less_eq_list_def less_list_def)
    60 
    61 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    62   by (unfold less_le less_eq_list_def) (auto)
    63 
    64 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
    65   by (metis sub_Cons2_iff less_list_def less_eq_list_def)
    66 
    67 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
    68   by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
    69 
    70 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
    71   by (metis less_list_def less_eq_list_def sub_append')
    72 
    73 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
    74   by (unfold less_le less_eq_list_def) auto
    75 
    76 end