factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
authorblanchet
Wed Nov 20 18:58:00 2013 +0100 (2013-11-20)
changeset 54538ba7392b52a7c
parent 54537 f37354a894a3
child 54539 bbab2ebda234
factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy
src/HOL/Library/Prefix_Order.thy
src/HOL/Library/Sublist.thy
src/HOL/List_Prefix.thy
src/HOL/Main.thy
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Wed Nov 20 18:32:25 2013 +0100
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Wed Nov 20 18:58:00 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_GFP
     1.7 -imports BNF_FP_Base Equiv_Relations_More "~~/src/HOL/Library/Sublist"
     1.8 +imports BNF_FP_Base Equiv_Relations_More
     1.9  keywords
    1.10    "codatatype" :: thy_decl and
    1.11    "primcorecursive" :: thy_goal and
     2.1 --- a/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy	Wed Nov 20 18:32:25 2013 +0100
     2.2 +++ b/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy	Wed Nov 20 18:58:00 2013 +0100
     2.3 @@ -12,7 +12,6 @@
     2.4  begin
     2.5  
     2.6  no_notation plus_class.plus (infixl "+" 65)
     2.7 -no_notation Sublist.parallel (infixl "\<parallel>" 50)
     2.8  
     2.9  consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
    2.10  
    2.11 @@ -145,4 +144,4 @@
    2.12    thus ?thesis by blast
    2.13  qed
    2.14  
    2.15 -end
    2.16 \ No newline at end of file
    2.17 +end
     3.1 --- a/src/HOL/Library/Prefix_Order.thy	Wed Nov 20 18:32:25 2013 +0100
     3.2 +++ b/src/HOL/Library/Prefix_Order.thy	Wed Nov 20 18:58:00 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Prefix order on lists as order class instance *}
     3.5  
     3.6  theory Prefix_Order
     3.7 -imports Sublist
     3.8 +imports List_Prefix
     3.9  begin
    3.10  
    3.11  instantiation list :: (type) order
     4.1 --- a/src/HOL/Library/Sublist.thy	Wed Nov 20 18:32:25 2013 +0100
     4.2 +++ b/src/HOL/Library/Sublist.thy	Wed Nov 20 18:58:00 2013 +0100
     4.3 @@ -3,198 +3,12 @@
     4.4      Author:     Christian Sternagel, JAIST
     4.5  *)
     4.6  
     4.7 -header {* List prefixes, suffixes, and homeomorphic embedding *}
     4.8 +header {* Parallel lists, list suffixes, and homeomorphic embedding *}
     4.9  
    4.10  theory Sublist
    4.11  imports Main
    4.12  begin
    4.13  
    4.14 -subsection {* Prefix order on lists *}
    4.15 -
    4.16 -definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    4.17 -  where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    4.18 -
    4.19 -definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    4.20 -  where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    4.21 -
    4.22 -interpretation prefix_order: order prefixeq prefix
    4.23 -  by default (auto simp: prefixeq_def prefix_def)
    4.24 -
    4.25 -interpretation prefix_bot: order_bot Nil prefixeq prefix
    4.26 -  by default (simp add: prefixeq_def)
    4.27 -
    4.28 -lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
    4.29 -  unfolding prefixeq_def by blast
    4.30 -
    4.31 -lemma prefixeqE [elim?]:
    4.32 -  assumes "prefixeq xs ys"
    4.33 -  obtains zs where "ys = xs @ zs"
    4.34 -  using assms unfolding prefixeq_def by blast
    4.35 -
    4.36 -lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
    4.37 -  unfolding prefix_def prefixeq_def by blast
    4.38 -
    4.39 -lemma prefixE' [elim?]:
    4.40 -  assumes "prefix xs ys"
    4.41 -  obtains z zs where "ys = xs @ z # zs"
    4.42 -proof -
    4.43 -  from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    4.44 -    unfolding prefix_def prefixeq_def by blast
    4.45 -  with that show ?thesis by (auto simp add: neq_Nil_conv)
    4.46 -qed
    4.47 -
    4.48 -lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
    4.49 -  unfolding prefix_def by blast
    4.50 -
    4.51 -lemma prefixE [elim?]:
    4.52 -  fixes xs ys :: "'a list"
    4.53 -  assumes "prefix xs ys"
    4.54 -  obtains "prefixeq xs ys" and "xs \<noteq> ys"
    4.55 -  using assms unfolding prefix_def by blast
    4.56 -
    4.57 -
    4.58 -subsection {* Basic properties of prefixes *}
    4.59 -
    4.60 -theorem Nil_prefixeq [iff]: "prefixeq [] xs"
    4.61 -  by (simp add: prefixeq_def)
    4.62 -
    4.63 -theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])"
    4.64 -  by (induct xs) (simp_all add: prefixeq_def)
    4.65 -
    4.66 -lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
    4.67 -proof
    4.68 -  assume "prefixeq xs (ys @ [y])"
    4.69 -  then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    4.70 -  show "xs = ys @ [y] \<or> prefixeq xs ys"
    4.71 -    by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
    4.72 -next
    4.73 -  assume "xs = ys @ [y] \<or> prefixeq xs ys"
    4.74 -  then show "prefixeq xs (ys @ [y])"
    4.75 -    by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI)
    4.76 -qed
    4.77 -
    4.78 -lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \<and> prefixeq xs ys)"
    4.79 -  by (auto simp add: prefixeq_def)
    4.80 -
    4.81 -lemma prefixeq_code [code]:
    4.82 -  "prefixeq [] xs \<longleftrightarrow> True"
    4.83 -  "prefixeq (x # xs) [] \<longleftrightarrow> False"
    4.84 -  "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefixeq xs ys"
    4.85 -  by simp_all
    4.86 -
    4.87 -lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs"
    4.88 -  by (induct xs) simp_all
    4.89 -
    4.90 -lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
    4.91 -  by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
    4.92 -
    4.93 -lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
    4.94 -  by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
    4.95 -
    4.96 -lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
    4.97 -  by (auto simp add: prefixeq_def)
    4.98 -
    4.99 -theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
   4.100 -  by (cases xs) (auto simp add: prefixeq_def)
   4.101 -
   4.102 -theorem prefixeq_append:
   4.103 -  "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefixeq us zs))"
   4.104 -  apply (induct zs rule: rev_induct)
   4.105 -   apply force
   4.106 -  apply (simp del: append_assoc add: append_assoc [symmetric])
   4.107 -  apply (metis append_eq_appendI)
   4.108 -  done
   4.109 -
   4.110 -lemma append_one_prefixeq:
   4.111 -  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
   4.112 -  proof (unfold prefixeq_def)
   4.113 -    assume a1: "\<exists>zs. ys = xs @ zs"
   4.114 -    then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
   4.115 -    assume a2: "length xs < length ys"
   4.116 -    have f1: "\<And>v. ([]\<Colon>'a list) @ v = v" using append_Nil2 by simp
   4.117 -    have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
   4.118 -    hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
   4.119 -    thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
   4.120 -  qed
   4.121 -
   4.122 -theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
   4.123 -  by (auto simp add: prefixeq_def)
   4.124 -
   4.125 -lemma prefixeq_same_cases:
   4.126 -  "prefixeq (xs\<^sub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^sub>2 ys \<Longrightarrow> prefixeq xs\<^sub>1 xs\<^sub>2 \<or> prefixeq xs\<^sub>2 xs\<^sub>1"
   4.127 -  unfolding prefixeq_def by (force simp: append_eq_append_conv2)
   4.128 -
   4.129 -lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   4.130 -  by (auto simp add: prefixeq_def)
   4.131 -
   4.132 -lemma take_is_prefixeq: "prefixeq (take n xs) xs"
   4.133 -  unfolding prefixeq_def by (metis append_take_drop_id)
   4.134 -
   4.135 -lemma map_prefixeqI: "prefixeq xs ys \<Longrightarrow> prefixeq (map f xs) (map f ys)"
   4.136 -  by (auto simp: prefixeq_def)
   4.137 -
   4.138 -lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
   4.139 -  by (auto simp: prefix_def prefixeq_def)
   4.140 -
   4.141 -lemma prefix_simps [simp, code]:
   4.142 -  "prefix xs [] \<longleftrightarrow> False"
   4.143 -  "prefix [] (x # xs) \<longleftrightarrow> True"
   4.144 -  "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
   4.145 -  by (simp_all add: prefix_def cong: conj_cong)
   4.146 -
   4.147 -lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   4.148 -  apply (induct n arbitrary: xs ys)
   4.149 -   apply (case_tac ys, simp_all)[1]
   4.150 -  apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   4.151 -  done
   4.152 -
   4.153 -lemma not_prefixeq_cases:
   4.154 -  assumes pfx: "\<not> prefixeq ps ls"
   4.155 -  obtains
   4.156 -    (c1) "ps \<noteq> []" and "ls = []"
   4.157 -  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
   4.158 -  | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
   4.159 -proof (cases ps)
   4.160 -  case Nil
   4.161 -  then show ?thesis using pfx by simp
   4.162 -next
   4.163 -  case (Cons a as)
   4.164 -  note c = `ps = a#as`
   4.165 -  show ?thesis
   4.166 -  proof (cases ls)
   4.167 -    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
   4.168 -  next
   4.169 -    case (Cons x xs)
   4.170 -    show ?thesis
   4.171 -    proof (cases "x = a")
   4.172 -      case True
   4.173 -      have "\<not> prefixeq as xs" using pfx c Cons True by simp
   4.174 -      with c Cons True show ?thesis by (rule c2)
   4.175 -    next
   4.176 -      case False
   4.177 -      with c Cons show ?thesis by (rule c3)
   4.178 -    qed
   4.179 -  qed
   4.180 -qed
   4.181 -
   4.182 -lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
   4.183 -  assumes np: "\<not> prefixeq ps ls"
   4.184 -    and base: "\<And>x xs. P (x#xs) []"
   4.185 -    and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
   4.186 -    and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefixeq xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
   4.187 -  shows "P ps ls" using np
   4.188 -proof (induct ls arbitrary: ps)
   4.189 -  case Nil then show ?case
   4.190 -    by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
   4.191 -next
   4.192 -  case (Cons y ys)
   4.193 -  then have npfx: "\<not> prefixeq ps (y # ys)" by simp
   4.194 -  then obtain x xs where pv: "ps = x # xs"
   4.195 -    by (rule not_prefixeq_cases) auto
   4.196 -  show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
   4.197 -qed
   4.198 -
   4.199 -
   4.200  subsection {* Parallel lists *}
   4.201  
   4.202  definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/List_Prefix.thy	Wed Nov 20 18:58:00 2013 +0100
     5.3 @@ -0,0 +1,197 @@
     5.4 +(*  Title:      HOL/List_Prefix.thy
     5.5 +    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     5.6 +    Author:     Christian Sternagel, JAIST
     5.7 +*)
     5.8 +
     5.9 +header {* Parallel lists, list suffixes, and homeomorphic embedding *}
    5.10 +
    5.11 +theory List_Prefix
    5.12 +imports List
    5.13 +begin
    5.14 +
    5.15 +subsection {* Prefix order on lists *}
    5.16 +
    5.17 +definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    5.18 +  where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    5.19 +
    5.20 +definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    5.21 +  where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    5.22 +
    5.23 +interpretation prefix_order: order prefixeq prefix
    5.24 +  by default (auto simp: prefixeq_def prefix_def)
    5.25 +
    5.26 +interpretation prefix_bot: order_bot Nil prefixeq prefix
    5.27 +  by default (simp add: prefixeq_def)
    5.28 +
    5.29 +lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
    5.30 +  unfolding prefixeq_def by blast
    5.31 +
    5.32 +lemma prefixeqE [elim?]:
    5.33 +  assumes "prefixeq xs ys"
    5.34 +  obtains zs where "ys = xs @ zs"
    5.35 +  using assms unfolding prefixeq_def by blast
    5.36 +
    5.37 +lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
    5.38 +  unfolding prefix_def prefixeq_def by blast
    5.39 +
    5.40 +lemma prefixE' [elim?]:
    5.41 +  assumes "prefix xs ys"
    5.42 +  obtains z zs where "ys = xs @ z # zs"
    5.43 +proof -
    5.44 +  from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    5.45 +    unfolding prefix_def prefixeq_def by blast
    5.46 +  with that show ?thesis by (auto simp add: neq_Nil_conv)
    5.47 +qed
    5.48 +
    5.49 +lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
    5.50 +  unfolding prefix_def by blast
    5.51 +
    5.52 +lemma prefixE [elim?]:
    5.53 +  fixes xs ys :: "'a list"
    5.54 +  assumes "prefix xs ys"
    5.55 +  obtains "prefixeq xs ys" and "xs \<noteq> ys"
    5.56 +  using assms unfolding prefix_def by blast
    5.57 +
    5.58 +
    5.59 +subsection {* Basic properties of prefixes *}
    5.60 +
    5.61 +theorem Nil_prefixeq [iff]: "prefixeq [] xs"
    5.62 +  by (simp add: prefixeq_def)
    5.63 +
    5.64 +theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])"
    5.65 +  by (induct xs) (simp_all add: prefixeq_def)
    5.66 +
    5.67 +lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
    5.68 +proof
    5.69 +  assume "prefixeq xs (ys @ [y])"
    5.70 +  then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    5.71 +  show "xs = ys @ [y] \<or> prefixeq xs ys"
    5.72 +    by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
    5.73 +next
    5.74 +  assume "xs = ys @ [y] \<or> prefixeq xs ys"
    5.75 +  then show "prefixeq xs (ys @ [y])"
    5.76 +    by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI)
    5.77 +qed
    5.78 +
    5.79 +lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \<and> prefixeq xs ys)"
    5.80 +  by (auto simp add: prefixeq_def)
    5.81 +
    5.82 +lemma prefixeq_code [code]:
    5.83 +  "prefixeq [] xs \<longleftrightarrow> True"
    5.84 +  "prefixeq (x # xs) [] \<longleftrightarrow> False"
    5.85 +  "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefixeq xs ys"
    5.86 +  by simp_all
    5.87 +
    5.88 +lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs"
    5.89 +  by (induct xs) simp_all
    5.90 +
    5.91 +lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
    5.92 +  by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
    5.93 +
    5.94 +lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
    5.95 +  by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
    5.96 +
    5.97 +lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
    5.98 +  by (auto simp add: prefixeq_def)
    5.99 +
   5.100 +theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
   5.101 +  by (cases xs) (auto simp add: prefixeq_def)
   5.102 +
   5.103 +theorem prefixeq_append:
   5.104 +  "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefixeq us zs))"
   5.105 +  apply (induct zs rule: rev_induct)
   5.106 +   apply force
   5.107 +  apply (simp del: append_assoc add: append_assoc [symmetric])
   5.108 +  apply (metis append_eq_appendI)
   5.109 +  done
   5.110 +
   5.111 +lemma append_one_prefixeq:
   5.112 +  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
   5.113 +  proof (unfold prefixeq_def)
   5.114 +    assume a1: "\<exists>zs. ys = xs @ zs"
   5.115 +    then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
   5.116 +    assume a2: "length xs < length ys"
   5.117 +    have f1: "\<And>v. ([]\<Colon>'a list) @ v = v" using append_Nil2 by simp
   5.118 +    have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
   5.119 +    hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
   5.120 +    thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
   5.121 +  qed
   5.122 +
   5.123 +theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
   5.124 +  by (auto simp add: prefixeq_def)
   5.125 +
   5.126 +lemma prefixeq_same_cases:
   5.127 +  "prefixeq (xs\<^sub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^sub>2 ys \<Longrightarrow> prefixeq xs\<^sub>1 xs\<^sub>2 \<or> prefixeq xs\<^sub>2 xs\<^sub>1"
   5.128 +  unfolding prefixeq_def by (force simp: append_eq_append_conv2)
   5.129 +
   5.130 +lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   5.131 +  by (auto simp add: prefixeq_def)
   5.132 +
   5.133 +lemma take_is_prefixeq: "prefixeq (take n xs) xs"
   5.134 +  unfolding prefixeq_def by (metis append_take_drop_id)
   5.135 +
   5.136 +lemma map_prefixeqI: "prefixeq xs ys \<Longrightarrow> prefixeq (map f xs) (map f ys)"
   5.137 +  by (auto simp: prefixeq_def)
   5.138 +
   5.139 +lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
   5.140 +  by (auto simp: prefix_def prefixeq_def)
   5.141 +
   5.142 +lemma prefix_simps [simp, code]:
   5.143 +  "prefix xs [] \<longleftrightarrow> False"
   5.144 +  "prefix [] (x # xs) \<longleftrightarrow> True"
   5.145 +  "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
   5.146 +  by (simp_all add: prefix_def cong: conj_cong)
   5.147 +
   5.148 +lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   5.149 +  apply (induct n arbitrary: xs ys)
   5.150 +   apply (case_tac ys, simp_all)[1]
   5.151 +  apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   5.152 +  done
   5.153 +
   5.154 +lemma not_prefixeq_cases:
   5.155 +  assumes pfx: "\<not> prefixeq ps ls"
   5.156 +  obtains
   5.157 +    (c1) "ps \<noteq> []" and "ls = []"
   5.158 +  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
   5.159 +  | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
   5.160 +proof (cases ps)
   5.161 +  case Nil
   5.162 +  then show ?thesis using pfx by simp
   5.163 +next
   5.164 +  case (Cons a as)
   5.165 +  note c = `ps = a#as`
   5.166 +  show ?thesis
   5.167 +  proof (cases ls)
   5.168 +    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
   5.169 +  next
   5.170 +    case (Cons x xs)
   5.171 +    show ?thesis
   5.172 +    proof (cases "x = a")
   5.173 +      case True
   5.174 +      have "\<not> prefixeq as xs" using pfx c Cons True by simp
   5.175 +      with c Cons True show ?thesis by (rule c2)
   5.176 +    next
   5.177 +      case False
   5.178 +      with c Cons show ?thesis by (rule c3)
   5.179 +    qed
   5.180 +  qed
   5.181 +qed
   5.182 +
   5.183 +lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
   5.184 +  assumes np: "\<not> prefixeq ps ls"
   5.185 +    and base: "\<And>x xs. P (x#xs) []"
   5.186 +    and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
   5.187 +    and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefixeq xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
   5.188 +  shows "P ps ls" using np
   5.189 +proof (induct ls arbitrary: ps)
   5.190 +  case Nil then show ?case
   5.191 +    by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
   5.192 +next
   5.193 +  case (Cons y ys)
   5.194 +  then have npfx: "\<not> prefixeq ps (y # ys)" by simp
   5.195 +  then obtain x xs where pv: "ps = x # xs"
   5.196 +    by (rule not_prefixeq_cases) auto
   5.197 +  show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
   5.198 +qed
   5.199 +
   5.200 +end
     6.1 --- a/src/HOL/Main.thy	Wed Nov 20 18:32:25 2013 +0100
     6.2 +++ b/src/HOL/Main.thy	Wed Nov 20 18:58:00 2013 +0100
     6.3 @@ -1,7 +1,7 @@
     6.4  header {* Main HOL *}
     6.5  
     6.6  theory Main
     6.7 -imports Predicate_Compile Nitpick Extraction Lifting_Sum
     6.8 +imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix
     6.9  begin
    6.10  
    6.11  text {*