haftmann@26735: (*  Title:      HOL/Library/Sublist_Order.thy
haftmann@26735:     Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
nipkow@33431:                 Florian Haftmann, Tobias Nipkow, TU Muenchen
haftmann@26735: *)
haftmann@26735: 
haftmann@26735: header {* Sublist Ordering *}
haftmann@26735: 
haftmann@26735: theory Sublist_Order
Christian@49088: imports Sublist
haftmann@26735: begin
haftmann@26735: 
haftmann@26735: text {*
haftmann@26735:   This theory defines sublist ordering on lists.
haftmann@26735:   A list @{text ys} is a sublist of a list @{text xs},
haftmann@26735:   iff one obtains @{text ys} by erasing some elements from @{text xs}.
haftmann@26735: *}
haftmann@26735: 
haftmann@26735: subsection {* Definitions and basic lemmas *}
haftmann@26735: 
nipkow@33431: instantiation list :: (type) ord
haftmann@26735: begin
haftmann@26735: 
Christian@49084: definition
Christian@50516:   "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
haftmann@26735: 
haftmann@26735: definition
Christian@49084:   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
haftmann@26735: 
Christian@49085: instance ..
nipkow@33431: 
nipkow@33431: end
nipkow@33431: 
Christian@49085: instance list :: (type) order
Christian@49085: proof
haftmann@26735:   fix xs ys :: "'a list"
haftmann@27682:   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
haftmann@26735: next
haftmann@26735:   fix xs :: "'a list"
Christian@49085:   show "xs \<le> xs" by (simp add: less_eq_list_def)
haftmann@26735: next
haftmann@26735:   fix xs ys :: "'a list"
Christian@49085:   assume "xs <= ys" and "ys <= xs"
Christian@50516:   thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
haftmann@26735: next
haftmann@26735:   fix xs ys zs :: "'a list"
Christian@49085:   assume "xs <= ys" and "ys <= zs"
Christian@50516:   thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
haftmann@26735: qed
haftmann@26735: 
Christian@49093: lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
Christian@57497:   list_emb.induct [of "op =", folded less_eq_list_def]
Christian@57497: lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
Christian@50516: lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
Christian@50516: lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
Christian@50516: lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
Christian@57497: lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
Christian@49093: 
nipkow@33431: lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
Christian@57497:   by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
haftmann@26735: 
nipkow@33431: lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
Christian@57497:   by (metis less_eq_list_def list_emb_Nil order_less_le)
nipkow@33431: 
Christian@49085: lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
Christian@57497:   by (metis list_emb_Nil less_eq_list_def less_list_def)
nipkow@33431: 
nipkow@33431: lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
Christian@49085:   by (unfold less_le less_eq_list_def) (auto)
haftmann@26735: 
nipkow@33431: lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
Christian@50516:   by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
nipkow@33431: 
nipkow@33431: lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
Christian@50516:   by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
nipkow@33431: 
nipkow@33431: lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
Christian@50516:   by (metis less_list_def less_eq_list_def sublisteq_append')
nipkow@33431: 
nipkow@33431: lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
Christian@49085:   by (unfold less_le less_eq_list_def) auto
haftmann@26735: 
haftmann@26735: end