author | wenzelm |
Wed, 08 Mar 2017 10:50:59 +0100 | |
changeset 65151 | a7394aa4d21c |
parent 63465 | d7610beb98bc |
child 65869 | a6ed757b8585 |
permissions | -rw-r--r-- |
26735 | 1 |
(* Title: HOL/Library/Sublist_Order.thy |
63465 | 2 |
Author: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de> |
3 |
Author: Florian Haftmann, , TU Muenchen |
|
4 |
Author: Tobias Nipkow, TU Muenchen |
|
26735 | 5 |
*) |
6 |
||
60500 | 7 |
section \<open>Sublist Ordering\<close> |
26735 | 8 |
|
9 |
theory Sublist_Order |
|
49088
5cd8b4426a57
Main is implicitly imported via Sublist
Christian Sternagel
parents:
49085
diff
changeset
|
10 |
imports Sublist |
26735 | 11 |
begin |
12 |
||
60500 | 13 |
text \<open> |
63465 | 14 |
This theory defines sublist ordering on lists. A list \<open>ys\<close> is a sublist of a |
15 |
list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>. |
|
60500 | 16 |
\<close> |
26735 | 17 |
|
60500 | 18 |
subsection \<open>Definitions and basic lemmas\<close> |
26735 | 19 |
|
33431 | 20 |
instantiation list :: (type) ord |
26735 | 21 |
begin |
22 |
||
63465 | 23 |
definition "xs \<le> ys \<longleftrightarrow> sublisteq xs ys" for xs ys :: "'a list" |
24 |
definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list" |
|
26735 | 25 |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
26 |
instance .. |
33431 | 27 |
|
28 |
end |
|
29 |
||
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
30 |
instance list :: (type) order |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
31 |
proof |
26735 | 32 |
fix xs ys zs :: "'a list" |
63465 | 33 |
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
34 |
unfolding less_list_def .. |
|
35 |
show "xs \<le> xs" |
|
36 |
by (simp add: less_eq_list_def) |
|
37 |
show "xs = ys" if "xs \<le> ys" and "ys \<le> xs" |
|
38 |
using that unfolding less_eq_list_def by (rule sublisteq_antisym) |
|
39 |
show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" |
|
40 |
using that unfolding less_eq_list_def by (rule sublisteq_trans) |
|
26735 | 41 |
qed |
42 |
||
49093 | 43 |
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = |
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset
|
44 |
list_emb.induct [of "op =", folded less_eq_list_def] |
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset
|
45 |
lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def] |
50516 | 46 |
lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def] |
47 |
lemmas le_list_map = sublisteq_map [folded less_eq_list_def] |
|
48 |
lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def] |
|
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset
|
49 |
lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def] |
49093 | 50 |
|
33431 | 51 |
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset
|
52 |
by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def) |
26735 | 53 |
|
33431 | 54 |
lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset
|
55 |
by (metis less_eq_list_def list_emb_Nil order_less_le) |
33431 | 56 |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
57 |
lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False" |
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset
|
58 |
by (metis list_emb_Nil less_eq_list_def less_list_def) |
33431 | 59 |
|
60 |
lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
61 |
by (unfold less_le less_eq_list_def) (auto) |
26735 | 62 |
|
33431 | 63 |
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
50516 | 64 |
by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def) |
33431 | 65 |
|
66 |
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
|
63465 | 67 |
by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le |
68 |
self_append_conv2 less_eq_list_def) |
|
33431 | 69 |
|
70 |
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
|
50516 | 71 |
by (metis less_list_def less_eq_list_def sublisteq_append') |
33431 | 72 |
|
73 |
lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
74 |
by (unfold less_le less_eq_list_def) auto |
26735 | 75 |
|
76 |
end |