author | Christian Sternagel |
Thu, 13 Dec 2012 13:11:38 +0100 | |
changeset 50516 | ed6b40d15d1c |
parent 49093 | fdc301f592c4 |
child 57497 | 4106a2bc066a |
permissions | -rw-r--r-- |
26735 | 1 |
(* Title: HOL/Library/Sublist_Order.thy |
2 |
Authors: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de> |
|
33431 | 3 |
Florian Haftmann, Tobias Nipkow, TU Muenchen |
26735 | 4 |
*) |
5 |
||
6 |
header {* Sublist Ordering *} |
|
7 |
||
8 |
theory Sublist_Order |
|
49088
5cd8b4426a57
Main is implicitly imported via Sublist
Christian Sternagel
parents:
49085
diff
changeset
|
9 |
imports Sublist |
26735 | 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 |
||
33431 | 20 |
instantiation list :: (type) ord |
26735 | 21 |
begin |
22 |
||
49084
e3973567ed4f
base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
Christian Sternagel
parents:
37765
diff
changeset
|
23 |
definition |
50516 | 24 |
"(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys" |
26735 | 25 |
|
26 |
definition |
|
49084
e3973567ed4f
base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
Christian Sternagel
parents:
37765
diff
changeset
|
27 |
"(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
26735 | 28 |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
29 |
instance .. |
33431 | 30 |
|
31 |
end |
|
32 |
||
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
33 |
instance list :: (type) order |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
34 |
proof |
26735 | 35 |
fix xs ys :: "'a list" |
27682 | 36 |
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. |
26735 | 37 |
next |
38 |
fix xs :: "'a list" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
39 |
show "xs \<le> xs" by (simp add: less_eq_list_def) |
26735 | 40 |
next |
41 |
fix xs ys :: "'a list" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
42 |
assume "xs <= ys" and "ys <= xs" |
50516 | 43 |
thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym) |
26735 | 44 |
next |
45 |
fix xs ys zs :: "'a list" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
46 |
assume "xs <= ys" and "ys <= zs" |
50516 | 47 |
thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans) |
26735 | 48 |
qed |
49 |
||
49093 | 50 |
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = |
50516 | 51 |
list_hembeq.induct [of "op =", folded less_eq_list_def] |
52 |
lemmas less_eq_list_drop = list_hembeq.list_hembeq_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_hembeq_length [of "op =", folded less_eq_list_def] |
|
49093 | 57 |
|
33431 | 58 |
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
50516 | 59 |
by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def) |
26735 | 60 |
|
33431 | 61 |
lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
50516 | 62 |
by (metis less_eq_list_def list_hembeq_Nil order_less_le) |
33431 | 63 |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
64 |
lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False" |
50516 | 65 |
by (metis list_hembeq_Nil less_eq_list_def less_list_def) |
33431 | 66 |
|
67 |
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
|
68 |
by (unfold less_le less_eq_list_def) (auto) |
26735 | 69 |
|
33431 | 70 |
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
50516 | 71 |
by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def) |
33431 | 72 |
|
73 |
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
|
50516 | 74 |
by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def) |
33431 | 75 |
|
76 |
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
|
50516 | 77 |
by (metis less_list_def less_eq_list_def sublisteq_append') |
33431 | 78 |
|
79 |
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
|
80 |
by (unfold less_le less_eq_list_def) auto |
26735 | 81 |
|
82 |
end |