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