author | wenzelm |
Mon, 26 Jun 2023 23:20:32 +0200 (19 months ago) | |
changeset 78209 | 50c5be88ad59 |
parent 75648 | aa0403e5535f |
permissions | -rw-r--r-- |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
1 |
(* Title: HOL/Library/Subseq_Order.thy |
63465 | 2 |
Author: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de> |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
63465 | 4 |
Author: Tobias Nipkow, TU Muenchen |
26735 | 5 |
*) |
6 |
||
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
7 |
section \<open>Subsequence Ordering\<close> |
26735 | 8 |
|
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
9 |
theory Subseq_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> |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
14 |
This theory defines subsequence ordering on lists. A list \<open>ys\<close> is a subsequence of a |
63465 | 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 |
||
75648 | 23 |
definition less_eq_list |
24 |
where \<open>xs \<le> ys \<longleftrightarrow> subseq xs ys\<close> for xs ys :: \<open>'a list\<close> |
|
25 |
||
26 |
definition less_list |
|
27 |
where \<open>xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs\<close> for xs ys :: \<open>'a list\<close> |
|
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 zs :: "'a list" |
63465 | 36 |
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
37 |
unfolding less_list_def .. |
|
38 |
show "xs \<le> xs" |
|
39 |
by (simp add: less_eq_list_def) |
|
40 |
show "xs = ys" if "xs \<le> ys" and "ys \<le> xs" |
|
73411 | 41 |
using that unfolding less_eq_list_def |
42 |
by (rule subseq_order.antisym) |
|
63465 | 43 |
show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" |
73411 | 44 |
using that unfolding less_eq_list_def |
45 |
by (rule subseq_order.order_trans) |
|
26735 | 46 |
qed |
47 |
||
49093 | 48 |
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = |
67399 | 49 |
list_emb.induct [of "(=)", folded less_eq_list_def] |
75648 | 50 |
|
51 |
lemma less_eq_list_empty [code]: |
|
52 |
\<open>[] \<le> xs \<longleftrightarrow> True\<close> |
|
53 |
by (simp add: less_eq_list_def) |
|
54 |
||
55 |
lemma less_eq_list_below_empty [code]: |
|
56 |
\<open>x # xs \<le> [] \<longleftrightarrow> False\<close> |
|
57 |
by (simp add: less_eq_list_def) |
|
58 |
||
59 |
lemma le_list_Cons2_iff [simp, code]: |
|
60 |
\<open>x # xs \<le> y # ys \<longleftrightarrow> (if x = y then xs \<le> ys else x # xs \<le> ys)\<close> |
|
61 |
by (simp add: less_eq_list_def) |
|
62 |
||
63 |
lemma less_list_empty [simp]: |
|
64 |
\<open>[] < xs \<longleftrightarrow> xs \<noteq> []\<close> |
|
65 |
by (metis less_eq_list_def list_emb_Nil order_less_le) |
|
66 |
||
67 |
lemma less_list_empty_Cons [code]: |
|
68 |
\<open>[] < x # xs \<longleftrightarrow> True\<close> |
|
69 |
by simp_all |
|
70 |
||
71 |
lemma less_list_below_empty [simp, code]: |
|
72 |
\<open>xs < [] \<longleftrightarrow> False\<close> |
|
73 |
by (metis list_emb_Nil less_eq_list_def less_list_def) |
|
74 |
||
75 |
lemma less_list_Cons2_iff [code]: |
|
76 |
\<open>x # xs < y # ys \<longleftrightarrow> (if x = y then xs < ys else x # xs \<le> ys)\<close> |
|
77 |
by (simp add: less_le) |
|
78 |
||
67399 | 79 |
lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "(=)", folded less_eq_list_def] |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
80 |
lemmas le_list_map = subseq_map [folded less_eq_list_def] |
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
81 |
lemmas le_list_filter = subseq_filter [folded less_eq_list_def] |
67399 | 82 |
lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def] |
49093 | 83 |
|
33431 | 84 |
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
85 |
by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def) |
26735 | 86 |
|
33431 | 87 |
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
|
88 |
by (unfold less_le less_eq_list_def) (auto) |
26735 | 89 |
|
33431 | 90 |
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
91 |
by (metis subseq_Cons2_iff less_list_def less_eq_list_def) |
33431 | 92 |
|
93 |
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
|
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
94 |
by (metis subseq_append_le_same_iff subseq_drop_many order_less_le |
63465 | 95 |
self_append_conv2 less_eq_list_def) |
33431 | 96 |
|
97 |
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
|
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65869
diff
changeset
|
98 |
by (metis less_list_def less_eq_list_def subseq_append') |
33431 | 99 |
|
100 |
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
|
101 |
by (unfold less_le less_eq_list_def) auto |
26735 | 102 |
|
103 |
end |