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