src/HOL/Library/Sublist.thy
changeset 49078 398e8fddabb0
parent 45236 ac4a2a66707d
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Aug 29 10:27:56 2012 +0900
     1.2 +++ b/src/HOL/Library/Sublist.thy	Wed Aug 29 10:35:05 2012 +0900
     1.3 @@ -14,71 +14,71 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  prefix_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
     1.8 +  prefixeq_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
     1.9  
    1.10  definition
    1.11 -  strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    1.12 +  prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    1.13  
    1.14  definition
    1.15    "bot = []"
    1.16  
    1.17  instance proof
    1.18 -qed (auto simp add: prefix_def strict_prefix_def bot_list_def)
    1.19 +qed (auto simp add: prefixeq_def prefix_def bot_list_def)
    1.20  
    1.21  end
    1.22  
    1.23 -lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
    1.24 -  unfolding prefix_def by blast
    1.25 +lemma prefixeqI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
    1.26 +  unfolding prefixeq_def by blast
    1.27  
    1.28 -lemma prefixE [elim?]:
    1.29 +lemma prefixeqE [elim?]:
    1.30    assumes "xs \<le> ys"
    1.31    obtains zs where "ys = xs @ zs"
    1.32 -  using assms unfolding prefix_def by blast
    1.33 +  using assms unfolding prefixeq_def by blast
    1.34  
    1.35 -lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    1.36 -  unfolding strict_prefix_def prefix_def by blast
    1.37 +lemma prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    1.38 +  unfolding prefix_def prefixeq_def by blast
    1.39  
    1.40 -lemma strict_prefixE' [elim?]:
    1.41 +lemma prefixE' [elim?]:
    1.42    assumes "xs < ys"
    1.43    obtains z zs where "ys = xs @ z # zs"
    1.44  proof -
    1.45    from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.46 -    unfolding strict_prefix_def prefix_def by blast
    1.47 +    unfolding prefix_def prefixeq_def by blast
    1.48    with that show ?thesis by (auto simp add: neq_Nil_conv)
    1.49  qed
    1.50  
    1.51 -lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    1.52 -  unfolding strict_prefix_def by blast
    1.53 +lemma prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    1.54 +  unfolding prefix_def by blast
    1.55  
    1.56 -lemma strict_prefixE [elim?]:
    1.57 +lemma prefixE [elim?]:
    1.58    fixes xs ys :: "'a list"
    1.59    assumes "xs < ys"
    1.60    obtains "xs \<le> ys" and "xs \<noteq> ys"
    1.61 -  using assms unfolding strict_prefix_def by blast
    1.62 +  using assms unfolding prefix_def by blast
    1.63  
    1.64  
    1.65  subsection {* Basic properties of prefixes *}
    1.66  
    1.67 -theorem Nil_prefix [iff]: "[] \<le> xs"
    1.68 -  by (simp add: prefix_def)
    1.69 +theorem Nil_prefixeq [iff]: "[] \<le> xs"
    1.70 +  by (simp add: prefixeq_def)
    1.71  
    1.72 -theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
    1.73 -  by (induct xs) (simp_all add: prefix_def)
    1.74 +theorem prefixeq_Nil [simp]: "(xs \<le> []) = (xs = [])"
    1.75 +  by (induct xs) (simp_all add: prefixeq_def)
    1.76  
    1.77 -lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
    1.78 +lemma prefixeq_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
    1.79  proof
    1.80    assume "xs \<le> ys @ [y]"
    1.81    then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    1.82    show "xs = ys @ [y] \<or> xs \<le> ys"
    1.83 -    by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)
    1.84 +    by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
    1.85  next
    1.86    assume "xs = ys @ [y] \<or> xs \<le> ys"
    1.87    then show "xs \<le> ys @ [y]"
    1.88 -    by (metis order_eq_iff order_trans prefixI)
    1.89 +    by (metis order_eq_iff order_trans prefixeqI)
    1.90  qed
    1.91  
    1.92 -lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    1.93 -  by (auto simp add: prefix_def)
    1.94 +lemma Cons_prefixeq_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    1.95 +  by (auto simp add: prefixeq_def)
    1.96  
    1.97  lemma less_eq_list_code [code]:
    1.98    "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
    1.99 @@ -86,22 +86,22 @@
   1.100    "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   1.101    by simp_all
   1.102  
   1.103 -lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
   1.104 +lemma same_prefixeq_prefixeq [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
   1.105    by (induct xs) simp_all
   1.106  
   1.107 -lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
   1.108 -  by (metis append_Nil2 append_self_conv order_eq_iff prefixI)
   1.109 +lemma same_prefixeq_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
   1.110 +  by (metis append_Nil2 append_self_conv order_eq_iff prefixeqI)
   1.111  
   1.112 -lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
   1.113 -  by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)
   1.114 +lemma prefixeq_prefixeq [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
   1.115 +  by (metis order_le_less_trans prefixeqI prefixE prefixI)
   1.116  
   1.117 -lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
   1.118 -  by (auto simp add: prefix_def)
   1.119 +lemma append_prefixeqD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
   1.120 +  by (auto simp add: prefixeq_def)
   1.121  
   1.122 -theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
   1.123 -  by (cases xs) (auto simp add: prefix_def)
   1.124 +theorem prefixeq_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
   1.125 +  by (cases xs) (auto simp add: prefixeq_def)
   1.126  
   1.127 -theorem prefix_append:
   1.128 +theorem prefixeq_append:
   1.129    "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
   1.130    apply (induct zs rule: rev_induct)
   1.131     apply force
   1.132 @@ -109,44 +109,44 @@
   1.133    apply (metis append_eq_appendI)
   1.134    done
   1.135  
   1.136 -lemma append_one_prefix:
   1.137 +lemma append_one_prefixeq:
   1.138    "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
   1.139 -  unfolding prefix_def
   1.140 +  unfolding prefixeq_def
   1.141    by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
   1.142      eq_Nil_appendI nth_drop')
   1.143  
   1.144 -theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   1.145 -  by (auto simp add: prefix_def)
   1.146 +theorem prefixeq_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   1.147 +  by (auto simp add: prefixeq_def)
   1.148  
   1.149 -lemma prefix_same_cases:
   1.150 +lemma prefixeq_same_cases:
   1.151    "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
   1.152 -  unfolding prefix_def by (metis append_eq_append_conv2)
   1.153 +  unfolding prefixeq_def by (metis append_eq_append_conv2)
   1.154  
   1.155 -lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
   1.156 -  by (auto simp add: prefix_def)
   1.157 +lemma set_mono_prefixeq: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
   1.158 +  by (auto simp add: prefixeq_def)
   1.159  
   1.160 -lemma take_is_prefix: "take n xs \<le> xs"
   1.161 -  unfolding prefix_def by (metis append_take_drop_id)
   1.162 +lemma take_is_prefixeq: "take n xs \<le> xs"
   1.163 +  unfolding prefixeq_def by (metis append_take_drop_id)
   1.164  
   1.165 -lemma map_prefixI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   1.166 -  by (auto simp: prefix_def)
   1.167 +lemma map_prefixeqI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   1.168 +  by (auto simp: prefixeq_def)
   1.169  
   1.170 -lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
   1.171 -  by (auto simp: strict_prefix_def prefix_def)
   1.172 +lemma prefixeq_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
   1.173 +  by (auto simp: prefix_def prefixeq_def)
   1.174  
   1.175 -lemma strict_prefix_simps [simp, code]:
   1.176 +lemma prefix_simps [simp, code]:
   1.177    "xs < [] \<longleftrightarrow> False"
   1.178    "[] < x # xs \<longleftrightarrow> True"
   1.179    "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
   1.180 -  by (simp_all add: strict_prefix_def cong: conj_cong)
   1.181 +  by (simp_all add: prefix_def cong: conj_cong)
   1.182  
   1.183 -lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
   1.184 +lemma take_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
   1.185    apply (induct n arbitrary: xs ys)
   1.186     apply (case_tac ys, simp_all)[1]
   1.187 -  apply (metis order_less_trans strict_prefixI take_is_prefix)
   1.188 +  apply (metis order_less_trans prefixI take_is_prefixeq)
   1.189    done
   1.190  
   1.191 -lemma not_prefix_cases:
   1.192 +lemma not_prefixeq_cases:
   1.193    assumes pfx: "\<not> ps \<le> ls"
   1.194    obtains
   1.195      (c1) "ps \<noteq> []" and "ls = []"
   1.196 @@ -159,7 +159,7 @@
   1.197    note c = `ps = a#as`
   1.198    show ?thesis
   1.199    proof (cases ls)
   1.200 -    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)
   1.201 +    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
   1.202    next
   1.203      case (Cons x xs)
   1.204      show ?thesis
   1.205 @@ -174,7 +174,7 @@
   1.206    qed
   1.207  qed
   1.208  
   1.209 -lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:
   1.210 +lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
   1.211    assumes np: "\<not> ps \<le> ls"
   1.212      and base: "\<And>x xs. P (x#xs) []"
   1.213      and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
   1.214 @@ -182,13 +182,13 @@
   1.215    shows "P ps ls" using np
   1.216  proof (induct ls arbitrary: ps)
   1.217    case Nil then show ?case
   1.218 -    by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
   1.219 +    by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
   1.220  next
   1.221    case (Cons y ys)
   1.222    then have npfx: "\<not> ps \<le> (y # ys)" by simp
   1.223    then obtain x xs where pv: "ps = x # xs"
   1.224 -    by (rule not_prefix_cases) auto
   1.225 -  show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2)
   1.226 +    by (rule not_prefixeq_cases) auto
   1.227 +  show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
   1.228  qed
   1.229  
   1.230  
   1.231 @@ -206,9 +206,9 @@
   1.232    obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   1.233    using assms unfolding parallel_def by blast
   1.234  
   1.235 -theorem prefix_cases:
   1.236 +theorem prefixeq_cases:
   1.237    obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
   1.238 -  unfolding parallel_def strict_prefix_def by blast
   1.239 +  unfolding parallel_def prefix_def by blast
   1.240  
   1.241  theorem parallel_decomp:
   1.242    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
   1.243 @@ -219,21 +219,21 @@
   1.244  next
   1.245    case (snoc x xs)
   1.246    show ?case
   1.247 -  proof (rule prefix_cases)
   1.248 +  proof (rule prefixeq_cases)
   1.249      assume le: "xs \<le> ys"
   1.250      then obtain ys' where ys: "ys = xs @ ys'" ..
   1.251      show ?thesis
   1.252      proof (cases ys')
   1.253        assume "ys' = []"
   1.254 -      then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
   1.255 +      then show ?thesis by (metis append_Nil2 parallelE prefixeqI snoc.prems ys)
   1.256      next
   1.257        fix c cs assume ys': "ys' = c # cs"
   1.258        then show ?thesis
   1.259 -        by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI
   1.260 -          same_prefix_prefix snoc.prems ys)
   1.261 +        by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixeqI
   1.262 +          same_prefixeq_prefixeq snoc.prems ys)
   1.263      qed
   1.264    next
   1.265 -    assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
   1.266 +    assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: prefix_def)
   1.267      with snoc have False by blast
   1.268      then show ?thesis ..
   1.269    next
   1.270 @@ -249,7 +249,7 @@
   1.271  lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
   1.272    apply (rule parallelI)
   1.273      apply (erule parallelE, erule conjE,
   1.274 -      induct rule: not_prefix_induct, simp+)+
   1.275 +      induct rule: not_prefixeq_induct, simp+)+
   1.276    done
   1.277  
   1.278  lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
   1.279 @@ -310,7 +310,7 @@
   1.280      by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
   1.281  qed
   1.282  
   1.283 -lemma postfix_to_prefix [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
   1.284 +lemma postfix_to_prefixeq [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
   1.285  proof
   1.286    assume "xs >>= ys"
   1.287    then obtain zs where "xs = zs @ ys" ..
   1.288 @@ -355,7 +355,7 @@
   1.289    by auto
   1.290  
   1.291  lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
   1.292 -  by (metis Cons_prefix_Cons parallelE parallelI)
   1.293 +  by (metis Cons_prefixeq_Cons parallelE parallelI)
   1.294  
   1.295  lemma not_equal_is_parallel:
   1.296    assumes neq: "xs \<noteq> ys"