src/HOL/Library/Sublist.thy
changeset 49083 01081bca31b6
parent 45236 ac4a2a66707d
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Aug 29 11:05:44 2012 +0900
     1.2 +++ b/src/HOL/Library/Sublist.thy	Wed Aug 29 12:23:14 2012 +0900
     1.3 @@ -10,99 +10,94 @@
     1.4  
     1.5  subsection {* Prefix order on lists *}
     1.6  
     1.7 -instantiation list :: (type) "{order, bot}"
     1.8 -begin
     1.9 +definition prefixeq :: "'a list => 'a list => bool" where
    1.10 +  "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    1.11  
    1.12 -definition
    1.13 -  prefixeq_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    1.14 -
    1.15 -definition
    1.16 -  prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    1.17 +definition prefix :: "'a list => 'a list => bool" where
    1.18 +  "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    1.19  
    1.20 -definition
    1.21 -  "bot = []"
    1.22 +interpretation prefix_order: order prefixeq prefix
    1.23 +  by default (auto simp: prefixeq_def prefix_def)
    1.24  
    1.25 -instance proof
    1.26 -qed (auto simp add: prefixeq_def prefix_def bot_list_def)
    1.27 +interpretation prefix_bot: bot prefixeq prefix Nil
    1.28 +  by default (simp add: prefixeq_def)
    1.29  
    1.30 -end
    1.31 -
    1.32 -lemma prefixeqI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
    1.33 +lemma prefixeqI [intro?]: "ys = xs @ zs ==> prefixeq xs ys"
    1.34    unfolding prefixeq_def by blast
    1.35  
    1.36  lemma prefixeqE [elim?]:
    1.37 -  assumes "xs \<le> ys"
    1.38 +  assumes "prefixeq xs ys"
    1.39    obtains zs where "ys = xs @ zs"
    1.40    using assms unfolding prefixeq_def by blast
    1.41  
    1.42 -lemma prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    1.43 +lemma prefixI' [intro?]: "ys = xs @ z # zs ==> prefix xs ys"
    1.44    unfolding prefix_def prefixeq_def by blast
    1.45  
    1.46  lemma prefixE' [elim?]:
    1.47 -  assumes "xs < ys"
    1.48 +  assumes "prefix xs ys"
    1.49    obtains z zs where "ys = xs @ z # zs"
    1.50  proof -
    1.51 -  from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.52 +  from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.53      unfolding prefix_def prefixeq_def by blast
    1.54    with that show ?thesis by (auto simp add: neq_Nil_conv)
    1.55  qed
    1.56  
    1.57 -lemma prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    1.58 +lemma prefixI [intro?]: "prefixeq xs ys ==> xs \<noteq> ys ==> prefix xs ys"
    1.59    unfolding prefix_def by blast
    1.60  
    1.61  lemma prefixE [elim?]:
    1.62    fixes xs ys :: "'a list"
    1.63 -  assumes "xs < ys"
    1.64 -  obtains "xs \<le> ys" and "xs \<noteq> ys"
    1.65 +  assumes "prefix xs ys"
    1.66 +  obtains "prefixeq xs ys" and "xs \<noteq> ys"
    1.67    using assms unfolding prefix_def by blast
    1.68  
    1.69  
    1.70  subsection {* Basic properties of prefixes *}
    1.71  
    1.72 -theorem Nil_prefixeq [iff]: "[] \<le> xs"
    1.73 +theorem Nil_prefixeq [iff]: "prefixeq [] xs"
    1.74    by (simp add: prefixeq_def)
    1.75  
    1.76 -theorem prefixeq_Nil [simp]: "(xs \<le> []) = (xs = [])"
    1.77 +theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])"
    1.78    by (induct xs) (simp_all add: prefixeq_def)
    1.79  
    1.80 -lemma prefixeq_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
    1.81 +lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
    1.82  proof
    1.83 -  assume "xs \<le> ys @ [y]"
    1.84 +  assume "prefixeq xs (ys @ [y])"
    1.85    then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    1.86 -  show "xs = ys @ [y] \<or> xs \<le> ys"
    1.87 +  show "xs = ys @ [y] \<or> prefixeq xs ys"
    1.88      by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
    1.89  next
    1.90 -  assume "xs = ys @ [y] \<or> xs \<le> ys"
    1.91 -  then show "xs \<le> ys @ [y]"
    1.92 -    by (metis order_eq_iff order_trans prefixeqI)
    1.93 +  assume "xs = ys @ [y] \<or> prefixeq xs ys"
    1.94 +  then show "prefixeq xs (ys @ [y])"
    1.95 +    by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI)
    1.96  qed
    1.97  
    1.98 -lemma Cons_prefixeq_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    1.99 +lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \<and> prefixeq xs ys)"
   1.100    by (auto simp add: prefixeq_def)
   1.101  
   1.102 -lemma less_eq_list_code [code]:
   1.103 -  "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
   1.104 -  "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
   1.105 -  "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   1.106 +lemma prefixeq_code [code]:
   1.107 +  "prefixeq [] xs \<longleftrightarrow> True"
   1.108 +  "prefixeq (x # xs) [] \<longleftrightarrow> False"
   1.109 +  "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefixeq xs ys"
   1.110    by simp_all
   1.111  
   1.112 -lemma same_prefixeq_prefixeq [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
   1.113 +lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs"
   1.114    by (induct xs) simp_all
   1.115  
   1.116 -lemma same_prefixeq_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
   1.117 -  by (metis append_Nil2 append_self_conv order_eq_iff prefixeqI)
   1.118 +lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
   1.119 +  by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
   1.120  
   1.121 -lemma prefixeq_prefixeq [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
   1.122 -  by (metis order_le_less_trans prefixeqI prefixE prefixI)
   1.123 +lemma prefixeq_prefixeq [simp]: "prefixeq xs ys ==> prefixeq xs (ys @ zs)"
   1.124 +  by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
   1.125  
   1.126 -lemma append_prefixeqD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
   1.127 +lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
   1.128    by (auto simp add: prefixeq_def)
   1.129  
   1.130 -theorem prefixeq_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
   1.131 +theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
   1.132    by (cases xs) (auto simp add: prefixeq_def)
   1.133  
   1.134  theorem prefixeq_append:
   1.135 -  "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
   1.136 +  "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefixeq us zs))"
   1.137    apply (induct zs rule: rev_induct)
   1.138     apply force
   1.139    apply (simp del: append_assoc add: append_assoc [symmetric])
   1.140 @@ -110,47 +105,47 @@
   1.141    done
   1.142  
   1.143  lemma append_one_prefixeq:
   1.144 -  "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
   1.145 +  "prefixeq xs ys ==> length xs < length ys ==> prefixeq (xs @ [ys ! length xs]) ys"
   1.146    unfolding prefixeq_def
   1.147    by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
   1.148      eq_Nil_appendI nth_drop')
   1.149  
   1.150 -theorem prefixeq_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   1.151 +theorem prefixeq_length_le: "prefixeq xs ys ==> length xs \<le> length ys"
   1.152    by (auto simp add: prefixeq_def)
   1.153  
   1.154  lemma prefixeq_same_cases:
   1.155 -  "(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.156 +  "prefixeq (xs\<^isub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^isub>2 ys \<Longrightarrow> prefixeq xs\<^isub>1 xs\<^isub>2 \<or> prefixeq xs\<^isub>2 xs\<^isub>1"
   1.157    unfolding prefixeq_def by (metis append_eq_append_conv2)
   1.158  
   1.159 -lemma set_mono_prefixeq: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
   1.160 +lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   1.161    by (auto simp add: prefixeq_def)
   1.162  
   1.163 -lemma take_is_prefixeq: "take n xs \<le> xs"
   1.164 +lemma take_is_prefixeq: "prefixeq (take n xs) xs"
   1.165    unfolding prefixeq_def by (metis append_take_drop_id)
   1.166  
   1.167 -lemma map_prefixeqI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   1.168 +lemma map_prefixeqI: "prefixeq xs ys \<Longrightarrow> prefixeq (map f xs) (map f ys)"
   1.169    by (auto simp: prefixeq_def)
   1.170  
   1.171 -lemma prefixeq_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
   1.172 +lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
   1.173    by (auto simp: prefix_def prefixeq_def)
   1.174  
   1.175  lemma prefix_simps [simp, code]:
   1.176 -  "xs < [] \<longleftrightarrow> False"
   1.177 -  "[] < x # xs \<longleftrightarrow> True"
   1.178 -  "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
   1.179 +  "prefix xs [] \<longleftrightarrow> False"
   1.180 +  "prefix [] (x # xs) \<longleftrightarrow> True"
   1.181 +  "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
   1.182    by (simp_all add: prefix_def cong: conj_cong)
   1.183  
   1.184 -lemma take_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
   1.185 +lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   1.186    apply (induct n arbitrary: xs ys)
   1.187     apply (case_tac ys, simp_all)[1]
   1.188 -  apply (metis order_less_trans prefixI take_is_prefixeq)
   1.189 +  apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   1.190    done
   1.191  
   1.192  lemma not_prefixeq_cases:
   1.193 -  assumes pfx: "\<not> ps \<le> ls"
   1.194 +  assumes pfx: "\<not> prefixeq ps ls"
   1.195    obtains
   1.196      (c1) "ps \<noteq> []" and "ls = []"
   1.197 -  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs"
   1.198 +  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
   1.199    | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
   1.200  proof (cases ps)
   1.201    case Nil then show ?thesis using pfx by simp
   1.202 @@ -165,7 +160,7 @@
   1.203      show ?thesis
   1.204      proof (cases "x = a")
   1.205        case True
   1.206 -      have "\<not> as \<le> xs" using pfx c Cons True by simp
   1.207 +      have "\<not> prefixeq as xs" using pfx c Cons True by simp
   1.208        with c Cons True show ?thesis by (rule c2)
   1.209      next
   1.210        case False
   1.211 @@ -175,17 +170,17 @@
   1.212  qed
   1.213  
   1.214  lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
   1.215 -  assumes np: "\<not> ps \<le> ls"
   1.216 +  assumes np: "\<not> prefixeq ps ls"
   1.217      and base: "\<And>x xs. P (x#xs) []"
   1.218      and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
   1.219 -    and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
   1.220 +    and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefixeq xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
   1.221    shows "P ps ls" using np
   1.222  proof (induct ls arbitrary: ps)
   1.223    case Nil then show ?case
   1.224      by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
   1.225  next
   1.226    case (Cons y ys)
   1.227 -  then have npfx: "\<not> ps \<le> (y # ys)" by simp
   1.228 +  then have npfx: "\<not> prefixeq ps (y # ys)" by simp
   1.229    then obtain x xs where pv: "ps = x # xs"
   1.230      by (rule not_prefixeq_cases) auto
   1.231    show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
   1.232 @@ -196,18 +191,18 @@
   1.233  
   1.234  definition
   1.235    parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50) where
   1.236 -  "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
   1.237 +  "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
   1.238  
   1.239 -lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
   1.240 +lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys"
   1.241    unfolding parallel_def by blast
   1.242  
   1.243  lemma parallelE [elim]:
   1.244    assumes "xs \<parallel> ys"
   1.245 -  obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   1.246 +  obtains "\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs"
   1.247    using assms unfolding parallel_def by blast
   1.248  
   1.249  theorem prefixeq_cases:
   1.250 -  obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
   1.251 +  obtains "prefixeq xs ys" | "prefix ys xs" | "xs \<parallel> ys"
   1.252    unfolding parallel_def prefix_def by blast
   1.253  
   1.254  theorem parallel_decomp:
   1.255 @@ -220,7 +215,7 @@
   1.256    case (snoc x xs)
   1.257    show ?case
   1.258    proof (rule prefixeq_cases)
   1.259 -    assume le: "xs \<le> ys"
   1.260 +    assume le: "prefixeq xs ys"
   1.261      then obtain ys' where ys: "ys = xs @ ys'" ..
   1.262      show ?thesis
   1.263      proof (cases ys')
   1.264 @@ -233,7 +228,7 @@
   1.265            same_prefixeq_prefixeq snoc.prems ys)
   1.266      qed
   1.267    next
   1.268 -    assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: prefix_def)
   1.269 +    assume "prefix ys xs" then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def)
   1.270      with snoc have False by blast
   1.271      then show ?thesis ..
   1.272    next
   1.273 @@ -325,14 +320,14 @@
   1.274      by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI)
   1.275  qed
   1.276  
   1.277 -lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> rev xs \<le> rev ys"
   1.278 +lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> prefixeq (rev xs) (rev ys)"
   1.279  proof
   1.280    assume "suffixeq xs ys"
   1.281    then obtain zs where "ys = zs @ xs" ..
   1.282    then have "rev ys = rev xs @ rev zs" by simp
   1.283 -  then show "rev xs <= rev ys" ..
   1.284 +  then show "prefixeq (rev xs) (rev ys)" ..
   1.285  next
   1.286 -  assume "rev xs <= rev ys"
   1.287 +  assume "prefixeq (rev xs) (rev ys)"
   1.288    then obtain zs where "rev ys = rev xs @ zs" ..
   1.289    then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp
   1.290    then have "ys = rev zs @ xs" by simp
   1.291 @@ -375,10 +370,10 @@
   1.292    qed
   1.293  qed
   1.294  
   1.295 -lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"
   1.296 +lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y"
   1.297    by blast
   1.298  
   1.299 -lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x"
   1.300 +lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefixeq y x"
   1.301    by blast
   1.302  
   1.303  lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
   1.304 @@ -481,4 +476,7 @@
   1.305    shows "emb P xs zs"
   1.306    using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
   1.307  
   1.308 +lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys"
   1.309 +  by (induct rule: emb.induct) auto
   1.310 +
   1.311  end