src/HOL/Library/Sublist_Order.thy
changeset 49084 e3973567ed4f
parent 37765 26bdfb7b680b
child 49085 4eef5c2ff5ad
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 12:23:14 2012 +0900
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 12:24:26 2012 +0900
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Sublist Ordering *}
     1.5  
     1.6  theory Sublist_Order
     1.7 -imports Main
     1.8 +imports Main Sublist
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -20,23 +20,35 @@
    1.13  instantiation list :: (type) ord
    1.14  begin
    1.15  
    1.16 -inductive less_eq_list where
    1.17 -  empty [simp, intro!]: "[] \<le> xs"
    1.18 -  | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
    1.19 -  | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
    1.20 +definition
    1.21 +  "(xs :: 'a list) \<le> ys \<longleftrightarrow> emb (op =) xs ys"
    1.22  
    1.23  definition
    1.24 -  "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    1.25 +  "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    1.26  
    1.27  instance proof qed
    1.28  
    1.29  end
    1.30  
    1.31 +lemma empty [simp, intro!]: "[] \<le> xs" by (auto simp: less_eq_list_def)
    1.32 +
    1.33 +lemma drop: "xs \<le> ys \<Longrightarrow> xs \<le> (y # ys)"
    1.34 +  by (unfold less_eq_list_def) blast
    1.35 +
    1.36 +lemma take: "xs \<le> ys \<Longrightarrow> (x#xs) \<le> (x#ys)"
    1.37 +  by (unfold less_eq_list_def) blast
    1.38 +
    1.39 +lemmas le_list_induct [consumes 1, case_names empty drop take] =
    1.40 +  emb.induct [of "op =", folded less_eq_list_def]
    1.41 +
    1.42 +lemmas le_list_cases [consumes 1, case_names empty drop take] =
    1.43 +  emb.cases [of "op =", folded less_eq_list_def]
    1.44 +
    1.45  lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    1.46 -by (induct rule: less_eq_list.induct) auto
    1.47 +  by (induct rule: le_list_induct) auto
    1.48  
    1.49  lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
    1.50 -by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
    1.51 +  by (induct rule: le_list_induct) (auto dest: le_list_length)
    1.52  
    1.53  lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
    1.54  by (metis le_list_length linorder_not_less)
    1.55 @@ -45,10 +57,10 @@
    1.56  by (auto dest: le_list_length)
    1.57  
    1.58  lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
    1.59 -by (induct zs) (auto intro: drop)
    1.60 +by (induct zs) (auto simp: less_eq_list_def)
    1.61  
    1.62  lemma [code]: "[] <= xs \<longleftrightarrow> True"
    1.63 -by(metis less_eq_list.empty)
    1.64 +by (simp add: less_eq_list_def)
    1.65  
    1.66  lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
    1.67  by simp
    1.68 @@ -58,11 +70,13 @@
    1.69    { fix xs' ys'
    1.70      assume "xs' <= ys"
    1.71      hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
    1.72 -    proof induct
    1.73 +    proof (induct rule: le_list_induct)
    1.74        case empty thus ?case by simp
    1.75      next
    1.76 -      case drop thus ?case by (metis less_eq_list.drop)
    1.77 +      note drop' = drop
    1.78 +      case drop thus ?case by (metis drop')
    1.79      next
    1.80 +      note t = take
    1.81        case take thus ?case by (simp add: drop)
    1.82      qed }
    1.83    from this[OF assms] show ?thesis by simp
    1.84 @@ -71,13 +85,13 @@
    1.85  lemma le_list_drop_Cons2:
    1.86  assumes "x#xs <= x#ys" shows "xs <= ys"
    1.87  using assms
    1.88 -proof cases
    1.89 +proof (cases rule: le_list_cases)
    1.90    case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
    1.91  qed simp_all
    1.92  
    1.93  lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
    1.94  shows "x ~= y \<Longrightarrow> x # xs <= ys"
    1.95 -using assms proof cases qed auto
    1.96 +using assms by (cases rule: le_list_cases) auto
    1.97  
    1.98  lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
    1.99    (if x=y then xs <= ys else (x#xs) <= ys)"
   1.100 @@ -91,7 +105,7 @@
   1.101  proof-
   1.102    { fix xys zs :: "'a list" assume "xys <= zs"
   1.103      hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
   1.104 -    proof induct
   1.105 +    proof (induct rule: le_list_induct)
   1.106        case empty show ?case by simp
   1.107      next
   1.108        case take thus ?case by (metis list.inject self_append_conv2)
   1.109 @@ -109,12 +123,12 @@
   1.110    show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
   1.111  next
   1.112    fix xs :: "'a list"
   1.113 -  show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
   1.114 +  show "xs \<le> xs" by (induct xs) (auto intro!: drop)
   1.115  next
   1.116    fix xs ys :: "'a list"
   1.117    assume "xs <= ys"
   1.118    hence "ys <= xs \<longrightarrow> xs = ys"
   1.119 -  proof induct
   1.120 +  proof (induct rule: le_list_induct)
   1.121      case empty show ?case by simp
   1.122    next
   1.123      case take thus ?case by simp
   1.124 @@ -128,14 +142,15 @@
   1.125    fix xs ys zs :: "'a list"
   1.126    assume "xs <= ys"
   1.127    hence "ys <= zs \<longrightarrow> xs <= zs"
   1.128 -  proof (induct arbitrary:zs)
   1.129 +  proof (induct arbitrary:zs rule: le_list_induct)
   1.130      case empty show ?case by simp
   1.131    next
   1.132 -    case (take xs ys x) show ?case
   1.133 +    note take' = take
   1.134 +    case (take x y xs ys) show ?case
   1.135      proof
   1.136 -      assume "x # ys <= zs"
   1.137 +      assume "y # ys <= zs"
   1.138        with take show "x # xs <= zs"
   1.139 -        by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))
   1.140 +        by(metis le_list_Cons_EX le_list_drop_many take')
   1.141      qed
   1.142    next
   1.143      case drop thus ?case by (metis le_list_drop_Cons)
   1.144 @@ -150,7 +165,7 @@
   1.145  by (auto dest: le_list_length)
   1.146  
   1.147  lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
   1.148 -apply (induct rule:less_eq_list.induct)
   1.149 +apply (induct rule: le_list_induct)
   1.150    apply (metis eq_Nil_appendI le_list_drop_many)
   1.151   apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
   1.152  apply simp
   1.153 @@ -166,7 +181,7 @@
   1.154  by (metis empty less_list_def)
   1.155  
   1.156  lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   1.157 -by (unfold less_le) (auto intro: less_eq_list.drop)
   1.158 +by (unfold less_le) (auto intro: drop)
   1.159  
   1.160  lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
   1.161  by (metis le_list_Cons2_iff less_list_def)
   1.162 @@ -184,23 +199,24 @@
   1.163  proof
   1.164    { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
   1.165      hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
   1.166 -    proof (induct arbitrary: xs ys zs)
   1.167 +    proof (induct arbitrary: xs ys zs rule: le_list_induct)
   1.168        case empty show ?case by simp
   1.169      next
   1.170 +      note drop' = drop
   1.171        case (drop xs' ys' x)
   1.172        { assume "ys=[]" hence ?case using drop(1) by auto }
   1.173        moreover
   1.174        { fix us assume "ys = x#us"
   1.175 -        hence ?case using drop(2) by(simp add: less_eq_list.drop) }
   1.176 +        hence ?case using drop(2) by(simp add: drop') }
   1.177        ultimately show ?case by (auto simp:Cons_eq_append_conv)
   1.178      next
   1.179 -      case (take xs' ys' x)
   1.180 +      case (take x y xs' ys')
   1.181        { assume "xs=[]" hence ?case using take(1) by auto }
   1.182        moreover
   1.183 -      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}
   1.184 +      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take by auto}
   1.185        moreover
   1.186        { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
   1.187 -      ultimately show ?case by (auto simp:Cons_eq_append_conv)
   1.188 +      ultimately show ?case using `x = y` by (auto simp:Cons_eq_append_conv)
   1.189      qed }
   1.190    moreover assume ?L
   1.191    ultimately show ?R by blast
   1.192 @@ -218,19 +234,19 @@
   1.193  subsection {* Relation to standard list operations *}
   1.194  
   1.195  lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   1.196 -by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
   1.197 +by (induct rule: le_list_induct) (auto intro: drop)
   1.198  
   1.199  lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
   1.200 -by (induct xs) (auto intro: less_eq_list.drop)
   1.201 +by (induct xs) (auto intro: drop)
   1.202  
   1.203  lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
   1.204 -by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
   1.205 +by (induct rule: le_list_induct) (auto intro: drop)
   1.206  
   1.207  lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
   1.208  proof
   1.209    assume ?L
   1.210    thus ?R
   1.211 -  proof induct
   1.212 +  proof (induct rule: le_list_induct)
   1.213      case empty show ?case by (metis sublist_empty)
   1.214    next
   1.215      case (drop xs ys x)
   1.216 @@ -239,11 +255,11 @@
   1.217        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.218      thus ?case by blast
   1.219    next
   1.220 -    case (take xs ys x)
   1.221 +    case (take x y xs ys)
   1.222      then obtain N where "xs = sublist ys N" by blast
   1.223      hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   1.224        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.225 -    thus ?case by blast
   1.226 +    thus ?case unfolding `x = y` by blast
   1.227    qed
   1.228  next
   1.229    assume ?R