author | Christian Sternagel |
Wed, 29 Aug 2012 16:25:35 +0900 | |
changeset 49085 | 4eef5c2ff5ad |
parent 49084 | e3973567ed4f |
child 49088 | 5cd8b4426a57 |
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 |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
9 |
imports |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
10 |
Main |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
11 |
Sublist |
26735 | 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 |
||
33431 | 22 |
instantiation list :: (type) ord |
26735 | 23 |
begin |
24 |
||
49084
e3973567ed4f
base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
Christian Sternagel
parents:
37765
diff
changeset
|
25 |
definition |
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
26 |
"(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys" |
26735 | 27 |
|
28 |
definition |
|
49084
e3973567ed4f
base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
Christian Sternagel
parents:
37765
diff
changeset
|
29 |
"(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
26735 | 30 |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
31 |
instance .. |
33431 | 32 |
|
33 |
end |
|
34 |
||
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
35 |
instance list :: (type) order |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
36 |
proof |
26735 | 37 |
fix xs ys :: "'a list" |
27682 | 38 |
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. |
26735 | 39 |
next |
40 |
fix xs :: "'a list" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
41 |
show "xs \<le> xs" by (simp add: less_eq_list_def) |
26735 | 42 |
next |
43 |
fix xs ys :: "'a list" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
44 |
assume "xs <= ys" and "ys <= xs" |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
45 |
thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym) |
26735 | 46 |
next |
47 |
fix xs ys zs :: "'a list" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
48 |
assume "xs <= ys" and "ys <= zs" |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
49 |
thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans) |
26735 | 50 |
qed |
51 |
||
33431 | 52 |
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
53 |
by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def) |
26735 | 54 |
|
33431 | 55 |
lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
56 |
by (metis less_eq_list_def emb_Nil order_less_le) |
33431 | 57 |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
58 |
lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False" |
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
59 |
by (metis emb_Nil less_eq_list_def less_list_def) |
33431 | 60 |
|
61 |
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
|
62 |
by (unfold less_le less_eq_list_def) (auto) |
26735 | 63 |
|
33431 | 64 |
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
65 |
by (metis sub_Cons2_iff less_list_def less_eq_list_def) |
33431 | 66 |
|
67 |
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
68 |
by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def) |
33431 | 69 |
|
70 |
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
|
49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset
|
71 |
by (metis less_list_def less_eq_list_def sub_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 |