src/HOL/Library/Subseq_Order.thy
author wenzelm
Mon, 26 Jun 2023 23:20:32 +0200 (19 months ago)
changeset 78209 50c5be88ad59
parent 75648 aa0403e5535f
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 65869
diff changeset
     1
(*  Title:      HOL/Library/Subseq_Order.thy
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
     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
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
     4
    Author:     Tobias Nipkow, TU Muenchen
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     5
*)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     6
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 65869
diff changeset
     7
section \<open>Subsequence Ordering\<close>
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     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
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    11
begin
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    12
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    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
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    15
  list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    16
\<close>
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    17
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    18
subsection \<open>Definitions and basic lemmas\<close>
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    19
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    20
instantiation list :: (type) ord
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    21
begin
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    22
75648
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    23
definition less_eq_list
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    24
  where \<open>xs \<le> ys \<longleftrightarrow> subseq xs ys\<close> for xs ys :: \<open>'a list\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    25
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    26
definition less_list
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    27
  where \<open>xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs\<close> for xs ys :: \<open>'a list\<close>
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    28
49085
4eef5c2ff5ad introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents: 49084
diff changeset
    29
instance ..
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    30
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    31
end
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    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
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    35
  fix xs ys zs :: "'a list"
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    36
  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    37
    unfolding less_list_def ..
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    38
  show "xs \<le> xs"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    39
    by (simp add: less_eq_list_def)
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    40
  show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
73411
1f1366966296 avoid name clash
haftmann
parents: 67399
diff changeset
    41
    using that unfolding less_eq_list_def
1f1366966296 avoid name clash
haftmann
parents: 67399
diff changeset
    42
    by (rule subseq_order.antisym)
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    43
  show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
73411
1f1366966296 avoid name clash
haftmann
parents: 67399
diff changeset
    44
    using that unfolding less_eq_list_def
1f1366966296 avoid name clash
haftmann
parents: 67399
diff changeset
    45
    by (rule subseq_order.order_trans)
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    46
qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    47
49093
fdc301f592c4 forgot to add lemmas
Christian Sternagel
parents: 49088
diff changeset
    48
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 65956
diff changeset
    49
  list_emb.induct [of "(=)", folded less_eq_list_def]
75648
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    50
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    51
lemma less_eq_list_empty [code]:
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    52
  \<open>[] \<le> xs \<longleftrightarrow> True\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    53
  by (simp add: less_eq_list_def)
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    54
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    55
lemma less_eq_list_below_empty [code]:
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    56
  \<open>x # xs \<le> [] \<longleftrightarrow> False\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    57
  by (simp add: less_eq_list_def)
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    58
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    59
lemma le_list_Cons2_iff [simp, code]:
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    60
  \<open>x # xs \<le> y # ys \<longleftrightarrow> (if x = y then xs \<le> ys else x # xs \<le> ys)\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    61
  by (simp add: less_eq_list_def)
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    62
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    63
lemma less_list_empty [simp]:
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    64
  \<open>[] < xs \<longleftrightarrow> xs \<noteq> []\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    65
  by (metis less_eq_list_def list_emb_Nil order_less_le)
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    66
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    67
lemma less_list_empty_Cons [code]:
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    68
  \<open>[] < x # xs \<longleftrightarrow> True\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    69
  by simp_all
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    70
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    71
lemma less_list_below_empty [simp, code]:
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    72
  \<open>xs < [] \<longleftrightarrow> False\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    73
  by (metis list_emb_Nil less_eq_list_def less_list_def)
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    74
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    75
lemma less_list_Cons2_iff [code]:
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    76
  \<open>x # xs < y # ys \<longleftrightarrow> (if x = y then xs < ys else x # xs \<le> ys)\<close>
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    77
  by (simp add: less_le)
aa0403e5535f more complete set of code equations
haftmann
parents: 73411
diff changeset
    78
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 65956
diff changeset
    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
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 65956
diff changeset
    82
lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def]
49093
fdc301f592c4 forgot to add lemmas
Christian Sternagel
parents: 49088
diff changeset
    83
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    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
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    86
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    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
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    89
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    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
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    92
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    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
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61585
diff changeset
    95
      self_append_conv2 less_eq_list_def)
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    96
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    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
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    99
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   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
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   102
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   103
end