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