src/HOL/Library/Sublist_Order.thy
author haftmann
Mon, 07 Jul 2008 08:47:17 +0200
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 27682 25aceefd4786
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Sublist_Order.thy
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     2
    ID:         $Id$
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     3
    Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     4
                Florian Haftmann, TU München
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     5
*)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     6
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     7
header {* Sublist Ordering *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     8
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     9
theory Sublist_Order
27487
c8a6ce181805 absolute imports of HOL/*.thy theories
haftmann
parents: 27368
diff changeset
    10
imports Plain "~~/src/HOL/List"
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    11
begin
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    12
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    13
text {*
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    14
  This theory defines sublist ordering on lists.
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    15
  A list @{text ys} is a sublist of a list @{text xs},
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    16
  iff one obtains @{text ys} by erasing some elements from @{text xs}.
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    17
*}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    18
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    19
subsection {* Definitions and basic lemmas *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    20
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    21
instantiation list :: (type) order
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    22
begin
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    23
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    24
inductive less_eq_list where
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    25
  empty [simp, intro!]: "[] \<le> xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    26
  | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    27
  | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    28
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    29
lemmas ileq_empty = empty
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    30
lemmas ileq_drop = drop
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    31
lemmas ileq_take = take
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    32
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    33
lemma ileq_cases [cases set, case_names empty drop take]:
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    34
  assumes "xs \<le> ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    35
    and "xs = [] \<Longrightarrow> P"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    36
    and "\<And>z zs. ys = z # zs \<Longrightarrow> xs \<le> zs \<Longrightarrow> P"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    37
    and "\<And>x zs ws. xs = x # zs \<Longrightarrow> ys = x # ws \<Longrightarrow> zs \<le> ws \<Longrightarrow> P"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    38
  shows P
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    39
  using assms by (blast elim: less_eq_list.cases)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    40
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    41
lemma ileq_induct [induct set, case_names empty drop take]:
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    42
  assumes "xs \<le> ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    43
    and "\<And>zs. P [] zs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    44
    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow>  P ws zs \<Longrightarrow> P ws (z # zs)"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    45
    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow> P ws zs \<Longrightarrow> P (z # ws) (z # zs)"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    46
  shows "P xs ys" 
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    47
  using assms by (induct rule: less_eq_list.induct) blast+
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    48
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    49
definition
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    50
  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    51
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    52
lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    53
  by (induct rule: ileq_induct) auto
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    54
lemma ileq_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    55
  by (auto dest: ileq_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    56
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    57
instance proof
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    58
  fix xs ys :: "'a list"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    59
  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys" unfolding less_list_def ..
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    60
next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    61
  fix xs :: "'a list"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    62
  show "xs \<le> xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    63
next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    64
  fix xs ys :: "'a list"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    65
  (* TODO: Is there a simpler proof ? *)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    66
  { fix n
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    67
    have "!!l l'. \<lbrakk>l\<le>l'; l'\<le>l; n=length l + length l'\<rbrakk> \<Longrightarrow> l=l'"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    68
    proof (induct n rule: nat_less_induct)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    69
      case (1 n l l') from "1.prems"(1) show ?case proof (cases rule: ileq_cases)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    70
        case empty with "1.prems"(2) show ?thesis by auto 
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    71
      next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    72
        case (drop a l2') with "1.prems"(2) have "length l'\<le>length l" "length l \<le> length l2'" "1+length l2' = length l'" by (auto dest: ileq_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    73
        hence False by simp thus ?thesis ..
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    74
      next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    75
        case (take a l1' l2') hence LEN': "length l1' + length l2' < length l + length l'" by simp
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    76
        from "1.prems" have LEN: "length l' = length l" by (auto dest!: ileq_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    77
        from "1.prems"(2) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    78
          case empty' with take LEN show ?thesis by simp 
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    79
        next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    80
          case (drop' ah l2h) with take LEN have "length l1' \<le> length l2h" "1+length l2h = length l2'" "length l2' = length l1'" by (auto dest: ileq_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    81
          hence False by simp thus ?thesis ..
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    82
        next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    83
          case (take' ah l1h l2h)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    84
          with take have 2: "ah=a" "l1h=l2'" "l2h=l1'" "l1' \<le> l2'" "l2' \<le> l1'" by auto
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    85
          with LEN' "1.hyps" "1.prems"(3) have "l1'=l2'" by blast
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    86
          with take 2 show ?thesis by simp
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    87
        qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    88
      qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    89
    qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    90
  }
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    91
  moreover assume "xs \<le> ys" "ys \<le> xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    92
  ultimately show "xs = ys" by blast
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    93
next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    94
  fix xs ys zs :: "'a list"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    95
  {
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    96
    fix n
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    97
    have "!!x y z. \<lbrakk>x \<le> y; y \<le> z; n=length x + length y + length z\<rbrakk> \<Longrightarrow> x \<le> z" 
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    98
    proof (induct rule: nat_less_induct[case_names I])
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    99
      case (I n x y z)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   100
      from I.prems(2) show ?case proof (cases rule: ileq_cases)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   101
        case empty with I.prems(1) show ?thesis by auto
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   102
      next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   103
        case (drop a z') hence "length x + length y + length z' < length x + length y + length z" by simp
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   104
        with I.hyps I.prems(3,1) drop(2) have "x\<le>z'" by blast
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   105
        with drop(1) show ?thesis by (auto intro: ileq_drop)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   106
      next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   107
        case (take a y' z') from I.prems(1) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   108
          case empty' thus ?thesis by auto
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   109
        next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   110
          case (drop' ah y'h) with take have "x\<le>y'" "y'\<le>z'" "length x + length y' + length z' < length x + length y + length z" by auto
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   111
          with I.hyps I.prems(3) have "x\<le>z'" by (blast)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   112
          with take(2) show ?thesis  by (auto intro: ileq_drop)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   113
        next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   114
          case (take' ah x' y'h) with take have 2: "x=a#x'" "x'\<le>y'" "y'\<le>z'" "length x' + length y' + length z' < length x + length y + length z" by auto
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   115
          with I.hyps I.prems(3) have "x'\<le>z'" by blast
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   116
          with 2 take(2) show ?thesis by (auto intro: ileq_take)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   117
        qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   118
      qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   119
    qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   120
  }
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   121
  moreover assume "xs \<le> ys" "ys \<le> zs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   122
  ultimately show "xs \<le> zs" by blast
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   123
qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   124
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   125
end
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   126
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   127
lemmas ileq_intros = ileq_empty ileq_drop ileq_take
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   128
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   129
lemma ileq_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   130
  by (induct zs) (auto intro: ileq_drop)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   131
lemma ileq_take_many: "xs \<le> ys \<Longrightarrow> zs @ xs \<le> zs @ ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   132
  by (induct zs) (auto intro: ileq_take)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   133
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   134
lemma ileq_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   135
  by (induct rule: ileq_induct) (auto dest: ileq_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   136
lemma ileq_same_append [simp]: "x # xs \<le> xs \<longleftrightarrow> False"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   137
  by (auto dest: ileq_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   138
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   139
lemma ilt_length [intro]:
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   140
  assumes "xs < ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   141
  shows "length xs < length ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   142
proof -
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   143
  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_list_def)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   144
  moreover with ileq_length have "length xs \<le> length ys" by auto
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   145
  ultimately show ?thesis by (auto intro: ileq_same_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   146
qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   147
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   148
lemma ilt_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   149
  by (unfold less_list_def, auto)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   150
lemma ilt_emptyI: "xs \<noteq> [] \<Longrightarrow> [] < xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   151
  by (unfold less_list_def, auto)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   152
lemma ilt_emptyD: "[] < xs \<Longrightarrow> xs \<noteq> []"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   153
  by (unfold less_list_def, auto)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   154
lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   155
  by (auto dest: ilt_length)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   156
lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   157
  by (unfold less_list_def) (auto intro: ileq_intros)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   158
lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   159
  by (unfold less_list_def) (auto intro: ileq_intros)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   160
lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   161
  by (induct zs) (auto intro: ilt_drop)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   162
lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   163
  by (induct zs) (auto intro: ilt_take)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   164
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   165
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   166
subsection {* Appending elements *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   167
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   168
lemma ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   169
  by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   170
lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   171
  by (unfold less_list_def) (auto dest: ileq_rev_take)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   172
lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   173
  by (induct rule: ileq_induct) (auto intro: ileq_intros)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   174
lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   175
  by (induct zs rule: rev_induct) (auto dest: ileq_rev_drop)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   176
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   177
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   178
subsection {* Relation to standard list operations *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   179
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   180
lemma ileq_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   181
  by (induct rule: ileq_induct) (auto intro: ileq_intros)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   182
lemma ileq_filter_left[simp]: "filter f xs \<le> xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   183
  by (induct xs) (auto intro: ileq_intros)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   184
lemma ileq_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   185
  by (induct rule: ileq_induct) (auto intro: ileq_intros) 
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   186
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   187
end