src/HOL/Library/Sublist_Order.thy
changeset 33431 af516ed40e72
parent 30738 0842e906300c
child 33499 30e6e070bdb6
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Tue Nov 03 10:36:20 2009 +0100
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Wed Nov 04 09:18:03 2009 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Library/Sublist_Order.thy
     1.5      Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
     1.6 -                Florian Haftmann, TU Muenchen
     1.7 +                Florian Haftmann, Tobias Nipkow, TU Muenchen
     1.8  *)
     1.9  
    1.10  header {* Sublist Ordering *}
    1.11 @@ -17,7 +17,7 @@
    1.12  
    1.13  subsection {* Definitions and basic lemmas *}
    1.14  
    1.15 -instantiation list :: (type) order
    1.16 +instantiation list :: (type) ord
    1.17  begin
    1.18  
    1.19  inductive less_eq_list where
    1.20 @@ -25,162 +25,237 @@
    1.21    | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
    1.22    | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
    1.23  
    1.24 -lemmas ileq_empty = empty
    1.25 -lemmas ileq_drop = drop
    1.26 -lemmas ileq_take = take
    1.27 -
    1.28 -lemma ileq_cases [cases set, case_names empty drop take]:
    1.29 -  assumes "xs \<le> ys"
    1.30 -    and "xs = [] \<Longrightarrow> P"
    1.31 -    and "\<And>z zs. ys = z # zs \<Longrightarrow> xs \<le> zs \<Longrightarrow> P"
    1.32 -    and "\<And>x zs ws. xs = x # zs \<Longrightarrow> ys = x # ws \<Longrightarrow> zs \<le> ws \<Longrightarrow> P"
    1.33 -  shows P
    1.34 -  using assms by (blast elim: less_eq_list.cases)
    1.35 -
    1.36 -lemma ileq_induct [induct set, case_names empty drop take]:
    1.37 -  assumes "xs \<le> ys"
    1.38 -    and "\<And>zs. P [] zs"
    1.39 -    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow>  P ws zs \<Longrightarrow> P ws (z # zs)"
    1.40 -    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow> P ws zs \<Longrightarrow> P (z # ws) (z # zs)"
    1.41 -  shows "P xs ys" 
    1.42 -  using assms by (induct rule: less_eq_list.induct) blast+
    1.43 -
    1.44  definition
    1.45    [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    1.46  
    1.47 -lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    1.48 -  by (induct rule: ileq_induct) auto
    1.49 -lemma ileq_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
    1.50 -  by (auto dest: ileq_length)
    1.51 +instance proof qed
    1.52 +
    1.53 +end
    1.54 +
    1.55 +lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    1.56 +by (induct rule: less_eq_list.induct) auto
    1.57 +
    1.58 +lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
    1.59 +by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
    1.60 +
    1.61 +lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
    1.62 +by (metis le_list_length linorder_not_less)
    1.63 +
    1.64 +lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
    1.65 +by (auto dest: le_list_length)
    1.66 +
    1.67 +lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
    1.68 +by (induct zs) (auto intro: drop)
    1.69 +
    1.70 +lemma [code]: "[] <= xs \<longleftrightarrow> True"
    1.71 +by(metis less_eq_list.empty)
    1.72 +
    1.73 +lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
    1.74 +by simp
    1.75 +
    1.76 +lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
    1.77 +proof-
    1.78 +  { fix xs' ys'
    1.79 +    assume "xs' <= ys"
    1.80 +    hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
    1.81 +    proof induct
    1.82 +      case empty thus ?case by simp
    1.83 +    next
    1.84 +      case drop thus ?case by (metis less_eq_list.drop)
    1.85 +    next
    1.86 +      case take thus ?case by (simp add: drop)
    1.87 +    qed }
    1.88 +  from this[OF assms] show ?thesis by simp
    1.89 +qed
    1.90 +
    1.91 +lemma le_list_drop_Cons2:
    1.92 +assumes "x#xs <= x#ys" shows "xs <= ys"
    1.93 +using assms
    1.94 +proof cases
    1.95 +  case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
    1.96 +qed simp_all
    1.97 +
    1.98 +lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
    1.99 +shows "x ~= y \<Longrightarrow> x # xs <= ys"
   1.100 +using assms proof cases qed auto
   1.101 +
   1.102 +lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
   1.103 +  (if x=y then xs <= ys else (x#xs) <= ys)"
   1.104 +by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
   1.105 +
   1.106 +lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"
   1.107 +by (induct zs) (auto intro: take)
   1.108 +
   1.109 +lemma le_list_Cons_EX:
   1.110 +  assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
   1.111 +proof-
   1.112 +  { fix xys zs :: "'a list" assume "xys <= zs"
   1.113 +    hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
   1.114 +    proof induct
   1.115 +      case empty show ?case by simp
   1.116 +    next
   1.117 +      case take thus ?case by (metis list.inject self_append_conv2)
   1.118 +    next
   1.119 +      case drop thus ?case by (metis append_eq_Cons_conv)
   1.120 +    qed
   1.121 +  } with assms show ?thesis by blast
   1.122 +qed
   1.123 +
   1.124 +instantiation list :: (type) order
   1.125 +begin
   1.126  
   1.127  instance proof
   1.128    fix xs ys :: "'a list"
   1.129    show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
   1.130  next
   1.131    fix xs :: "'a list"
   1.132 -  show "xs \<le> xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take)
   1.133 +  show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
   1.134  next
   1.135    fix xs ys :: "'a list"
   1.136 -  (* TODO: Is there a simpler proof ? *)
   1.137 -  { fix n
   1.138 -    have "!!l l'. \<lbrakk>l\<le>l'; l'\<le>l; n=length l + length l'\<rbrakk> \<Longrightarrow> l=l'"
   1.139 -    proof (induct n rule: nat_less_induct)
   1.140 -      case (1 n l l') from "1.prems"(1) show ?case proof (cases rule: ileq_cases)
   1.141 -        case empty with "1.prems"(2) show ?thesis by auto 
   1.142 -      next
   1.143 -        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)
   1.144 -        hence False by simp thus ?thesis ..
   1.145 -      next
   1.146 -        case (take a l1' l2') hence LEN': "length l1' + length l2' < length l + length l'" by simp
   1.147 -        from "1.prems" have LEN: "length l' = length l" by (auto dest!: ileq_length)
   1.148 -        from "1.prems"(2) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
   1.149 -          case empty' with take LEN show ?thesis by simp 
   1.150 -        next
   1.151 -          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)
   1.152 -          hence False by simp thus ?thesis ..
   1.153 -        next
   1.154 -          case (take' ah l1h l2h)
   1.155 -          with take have 2: "ah=a" "l1h=l2'" "l2h=l1'" "l1' \<le> l2'" "l2' \<le> l1'" by auto
   1.156 -          with LEN' "1.hyps" "1.prems"(3) have "l1'=l2'" by blast
   1.157 -          with take 2 show ?thesis by simp
   1.158 -        qed
   1.159 -      qed
   1.160 -    qed
   1.161 -  }
   1.162 -  moreover assume "xs \<le> ys" "ys \<le> xs"
   1.163 +  assume "xs <= ys"
   1.164 +  hence "ys <= xs \<longrightarrow> xs = ys"
   1.165 +  proof induct
   1.166 +    case empty show ?case by simp
   1.167 +  next
   1.168 +    case take thus ?case by simp
   1.169 +  next
   1.170 +    case drop thus ?case
   1.171 +      by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
   1.172 +  qed
   1.173 +  moreover assume "ys <= xs"
   1.174    ultimately show "xs = ys" by blast
   1.175  next
   1.176    fix xs ys zs :: "'a list"
   1.177 -  {
   1.178 -    fix n
   1.179 -    have "!!x y z. \<lbrakk>x \<le> y; y \<le> z; n=length x + length y + length z\<rbrakk> \<Longrightarrow> x \<le> z" 
   1.180 -    proof (induct rule: nat_less_induct[case_names I])
   1.181 -      case (I n x y z)
   1.182 -      from I.prems(2) show ?case proof (cases rule: ileq_cases)
   1.183 -        case empty with I.prems(1) show ?thesis by auto
   1.184 -      next
   1.185 -        case (drop a z') hence "length x + length y + length z' < length x + length y + length z" by simp
   1.186 -        with I.hyps I.prems(3,1) drop(2) have "x\<le>z'" by blast
   1.187 -        with drop(1) show ?thesis by (auto intro: ileq_drop)
   1.188 -      next
   1.189 -        case (take a y' z') from I.prems(1) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
   1.190 -          case empty' thus ?thesis by auto
   1.191 -        next
   1.192 -          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
   1.193 -          with I.hyps I.prems(3) have "x\<le>z'" by (blast)
   1.194 -          with take(2) show ?thesis  by (auto intro: ileq_drop)
   1.195 -        next
   1.196 -          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
   1.197 -          with I.hyps I.prems(3) have "x'\<le>z'" by blast
   1.198 -          with 2 take(2) show ?thesis by (auto intro: ileq_take)
   1.199 -        qed
   1.200 -      qed
   1.201 +  assume "xs <= ys"
   1.202 +  hence "ys <= zs \<longrightarrow> xs <= zs"
   1.203 +  proof (induct arbitrary:zs)
   1.204 +    case empty show ?case by simp
   1.205 +  next
   1.206 +    case (take xs ys x) show ?case
   1.207 +    proof
   1.208 +      assume "x # ys <= zs"
   1.209 +      with take show "x # xs <= zs"
   1.210 +        by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))
   1.211      qed
   1.212 -  }
   1.213 -  moreover assume "xs \<le> ys" "ys \<le> zs"
   1.214 -  ultimately show "xs \<le> zs" by blast
   1.215 +  next
   1.216 +    case drop thus ?case by (metis le_list_drop_Cons)
   1.217 +  qed
   1.218 +  moreover assume "ys <= zs"
   1.219 +  ultimately show "xs <= zs" by blast
   1.220  qed
   1.221  
   1.222  end
   1.223  
   1.224 -lemmas ileq_intros = ileq_empty ileq_drop ileq_take
   1.225 +lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
   1.226 +by (auto dest: le_list_length)
   1.227  
   1.228 -lemma ileq_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
   1.229 -  by (induct zs) (auto intro: ileq_drop)
   1.230 -lemma ileq_take_many: "xs \<le> ys \<Longrightarrow> zs @ xs \<le> zs @ ys"
   1.231 -  by (induct zs) (auto intro: ileq_take)
   1.232 +lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
   1.233 +apply (induct rule:less_eq_list.induct)
   1.234 +  apply (metis eq_Nil_appendI le_list_drop_many)
   1.235 + apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
   1.236 +apply simp
   1.237 +done
   1.238  
   1.239 -lemma ileq_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
   1.240 -  by (induct rule: ileq_induct) (auto dest: ileq_length)
   1.241 -lemma ileq_same_append [simp]: "x # xs \<le> xs \<longleftrightarrow> False"
   1.242 -  by (auto dest: ileq_length)
   1.243 +lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   1.244 +by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
   1.245  
   1.246 -lemma ilt_length [intro]:
   1.247 -  assumes "xs < ys"
   1.248 -  shows "length xs < length ys"
   1.249 -proof -
   1.250 -  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_le)
   1.251 -  moreover with ileq_length have "length xs \<le> length ys" by auto
   1.252 -  ultimately show ?thesis by (auto intro: ileq_same_length)
   1.253 -qed
   1.254 +lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   1.255 +by (metis empty order_less_le)
   1.256 +
   1.257 +lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
   1.258 +by (metis empty less_list_def)
   1.259 +
   1.260 +lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   1.261 +by (unfold less_le) (auto intro: less_eq_list.drop)
   1.262  
   1.263 -lemma ilt_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   1.264 -  by (unfold less_list_def, auto)
   1.265 -lemma ilt_emptyI: "xs \<noteq> [] \<Longrightarrow> [] < xs"
   1.266 -  by (unfold less_list_def, auto)
   1.267 -lemma ilt_emptyD: "[] < xs \<Longrightarrow> xs \<noteq> []"
   1.268 -  by (unfold less_list_def, auto)
   1.269 -lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False"
   1.270 -  by (auto dest: ilt_length)
   1.271 -lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   1.272 -  by (unfold less_le) (auto intro: ileq_intros)
   1.273 -lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys"
   1.274 -  by (unfold less_le) (auto intro: ileq_intros)
   1.275 -lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   1.276 -  by (induct zs) (auto intro: ilt_drop)
   1.277 -lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys"
   1.278 -  by (induct zs) (auto intro: ilt_take)
   1.279 +lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
   1.280 +by (metis le_list_Cons2_iff less_list_def)
   1.281 +
   1.282 +lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   1.283 +by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
   1.284 +
   1.285 +lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
   1.286 +by (metis le_list_take_many_iff less_list_def)
   1.287  
   1.288  
   1.289  subsection {* Appending elements *}
   1.290  
   1.291 -lemma ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]"
   1.292 -  by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many)
   1.293 -lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]"
   1.294 -  by (unfold less_le) (auto dest: ileq_rev_take)
   1.295 -lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]"
   1.296 -  by (induct rule: ileq_induct) (auto intro: ileq_intros)
   1.297 -lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
   1.298 -  by (induct zs rule: rev_induct) (auto dest: ileq_rev_drop)
   1.299 +lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
   1.300 +proof
   1.301 +  { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
   1.302 +    hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
   1.303 +    proof (induct arbitrary: xs ys zs)
   1.304 +      case empty show ?case by simp
   1.305 +    next
   1.306 +      case (drop xs' ys' x)
   1.307 +      { assume "ys=[]" hence ?case using drop(1) by auto }
   1.308 +      moreover
   1.309 +      { fix us assume "ys = x#us"
   1.310 +        hence ?case using drop(2) by(simp add: less_eq_list.drop) }
   1.311 +      ultimately show ?case by (auto simp:Cons_eq_append_conv)
   1.312 +    next
   1.313 +      case (take xs' ys' x)
   1.314 +      { assume "xs=[]" hence ?case using take(1) by auto }
   1.315 +      moreover
   1.316 +      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}
   1.317 +      moreover
   1.318 +      { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
   1.319 +      ultimately show ?case by (auto simp:Cons_eq_append_conv)
   1.320 +    qed }
   1.321 +  moreover assume ?L
   1.322 +  ultimately show ?R by blast
   1.323 +next
   1.324 +  assume ?R thus ?L by(metis le_list_append_mono order_refl)
   1.325 +qed
   1.326 +
   1.327 +lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   1.328 +by (unfold less_le) auto
   1.329 +
   1.330 +lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
   1.331 +by (metis append_Nil2 empty le_list_append_mono)
   1.332  
   1.333  
   1.334  subsection {* Relation to standard list operations *}
   1.335  
   1.336 -lemma ileq_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   1.337 -  by (induct rule: ileq_induct) (auto intro: ileq_intros)
   1.338 -lemma ileq_filter_left[simp]: "filter f xs \<le> xs"
   1.339 -  by (induct xs) (auto intro: ileq_intros)
   1.340 -lemma ileq_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
   1.341 -  by (induct rule: ileq_induct) (auto intro: ileq_intros) 
   1.342 +lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   1.343 +by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
   1.344 +
   1.345 +lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
   1.346 +by (induct xs) (auto intro: less_eq_list.drop)
   1.347 +
   1.348 +lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
   1.349 +by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
   1.350 +
   1.351 +
   1.352 +lemma "xs <= ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
   1.353 +proof
   1.354 +  assume ?L
   1.355 +  thus ?R
   1.356 +  proof induct
   1.357 +    case empty show ?case by (metis sublist_empty)
   1.358 +  next
   1.359 +    case (drop xs ys x)
   1.360 +    then obtain N where "xs = sublist ys N" by blast
   1.361 +    hence "xs = sublist (x#ys) (Suc ` N)"
   1.362 +      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.363 +    thus ?case by blast
   1.364 +  next
   1.365 +    case (take xs ys x)
   1.366 +    then obtain N where "xs = sublist ys N" by blast
   1.367 +    hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   1.368 +      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.369 +    thus ?case by blast
   1.370 +  qed
   1.371 +next
   1.372 +  assume ?R
   1.373 +  then obtain N where "xs = sublist ys N" ..
   1.374 +  moreover have "sublist ys N <= ys"
   1.375 +  proof (induct ys arbitrary:N)
   1.376 +    case Nil show ?case by simp
   1.377 +  next
   1.378 +    case Cons thus ?case by (auto simp add:sublist_Cons drop)
   1.379 +  qed
   1.380 +  ultimately show ?L by simp
   1.381 +qed
   1.382  
   1.383  end