reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
authortraytel
Wed Feb 19 10:30:21 2014 +0100 (2014-02-19)
changeset 55579207538943038
parent 55578 32774e40afb0
child 55580 d12a13713cb4
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
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/Library/Prefix_Order.thy	Wed Feb 19 10:21:02 2014 +0100
     1.2 +++ b/src/HOL/Library/Prefix_Order.thy	Wed Feb 19 10:30:21 2014 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Prefix order on lists as order class instance *}
     1.5  
     1.6  theory Prefix_Order
     1.7 -imports List_Prefix
     1.8 +imports Sublist
     1.9  begin
    1.10  
    1.11  instantiation list :: (type) order
     2.1 --- a/src/HOL/Library/Sublist.thy	Wed Feb 19 10:21:02 2014 +0100
     2.2 +++ b/src/HOL/Library/Sublist.thy	Wed Feb 19 10:30:21 2014 +0100
     2.3 @@ -3,12 +3,198 @@
     2.4      Author:     Christian Sternagel, JAIST
     2.5  *)
     2.6  
     2.7 -header {* Parallel lists, list suffixes, and homeomorphic embedding *}
     2.8 +header {* List prefixes, suffixes, and homeomorphic embedding *}
     2.9  
    2.10  theory Sublist
    2.11  imports Main
    2.12  begin
    2.13  
    2.14 +subsection {* Prefix order on lists *}
    2.15 +
    2.16 +definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.17 +  where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    2.18 +
    2.19 +definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.20 +  where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    2.21 +
    2.22 +interpretation prefix_order: order prefixeq prefix
    2.23 +  by default (auto simp: prefixeq_def prefix_def)
    2.24 +
    2.25 +interpretation prefix_bot: order_bot Nil prefixeq prefix
    2.26 +  by default (simp add: prefixeq_def)
    2.27 +
    2.28 +lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
    2.29 +  unfolding prefixeq_def by blast
    2.30 +
    2.31 +lemma prefixeqE [elim?]:
    2.32 +  assumes "prefixeq xs ys"
    2.33 +  obtains zs where "ys = xs @ zs"
    2.34 +  using assms unfolding prefixeq_def by blast
    2.35 +
    2.36 +lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
    2.37 +  unfolding prefix_def prefixeq_def by blast
    2.38 +
    2.39 +lemma prefixE' [elim?]:
    2.40 +  assumes "prefix xs ys"
    2.41 +  obtains z zs where "ys = xs @ z # zs"
    2.42 +proof -
    2.43 +  from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    2.44 +    unfolding prefix_def prefixeq_def by blast
    2.45 +  with that show ?thesis by (auto simp add: neq_Nil_conv)
    2.46 +qed
    2.47 +
    2.48 +lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
    2.49 +  unfolding prefix_def by blast
    2.50 +
    2.51 +lemma prefixE [elim?]:
    2.52 +  fixes xs ys :: "'a list"
    2.53 +  assumes "prefix xs ys"
    2.54 +  obtains "prefixeq xs ys" and "xs \<noteq> ys"
    2.55 +  using assms unfolding prefix_def by blast
    2.56 +
    2.57 +
    2.58 +subsection {* Basic properties of prefixes *}
    2.59 +
    2.60 +theorem Nil_prefixeq [iff]: "prefixeq [] xs"
    2.61 +  by (simp add: prefixeq_def)
    2.62 +
    2.63 +theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])"
    2.64 +  by (induct xs) (simp_all add: prefixeq_def)
    2.65 +
    2.66 +lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
    2.67 +proof
    2.68 +  assume "prefixeq xs (ys @ [y])"
    2.69 +  then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    2.70 +  show "xs = ys @ [y] \<or> prefixeq xs ys"
    2.71 +    by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
    2.72 +next
    2.73 +  assume "xs = ys @ [y] \<or> prefixeq xs ys"
    2.74 +  then show "prefixeq xs (ys @ [y])"
    2.75 +    by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI)
    2.76 +qed
    2.77 +
    2.78 +lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \<and> prefixeq xs ys)"
    2.79 +  by (auto simp add: prefixeq_def)
    2.80 +
    2.81 +lemma prefixeq_code [code]:
    2.82 +  "prefixeq [] xs \<longleftrightarrow> True"
    2.83 +  "prefixeq (x # xs) [] \<longleftrightarrow> False"
    2.84 +  "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefixeq xs ys"
    2.85 +  by simp_all
    2.86 +
    2.87 +lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs"
    2.88 +  by (induct xs) simp_all
    2.89 +
    2.90 +lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
    2.91 +  by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
    2.92 +
    2.93 +lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
    2.94 +  by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
    2.95 +
    2.96 +lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
    2.97 +  by (auto simp add: prefixeq_def)
    2.98 +
    2.99 +theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
   2.100 +  by (cases xs) (auto simp add: prefixeq_def)
   2.101 +
   2.102 +theorem prefixeq_append:
   2.103 +  "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefixeq us zs))"
   2.104 +  apply (induct zs rule: rev_induct)
   2.105 +   apply force
   2.106 +  apply (simp del: append_assoc add: append_assoc [symmetric])
   2.107 +  apply (metis append_eq_appendI)
   2.108 +  done
   2.109 +
   2.110 +lemma append_one_prefixeq:
   2.111 +  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
   2.112 +  proof (unfold prefixeq_def)
   2.113 +    assume a1: "\<exists>zs. ys = xs @ zs"
   2.114 +    then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
   2.115 +    assume a2: "length xs < length ys"
   2.116 +    have f1: "\<And>v. ([]\<Colon>'a list) @ v = v" using append_Nil2 by simp
   2.117 +    have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
   2.118 +    hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
   2.119 +    thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
   2.120 +  qed
   2.121 +
   2.122 +theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
   2.123 +  by (auto simp add: prefixeq_def)
   2.124 +
   2.125 +lemma prefixeq_same_cases:
   2.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"
   2.127 +  unfolding prefixeq_def by (force simp: append_eq_append_conv2)
   2.128 +
   2.129 +lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   2.130 +  by (auto simp add: prefixeq_def)
   2.131 +
   2.132 +lemma take_is_prefixeq: "prefixeq (take n xs) xs"
   2.133 +  unfolding prefixeq_def by (metis append_take_drop_id)
   2.134 +
   2.135 +lemma map_prefixeqI: "prefixeq xs ys \<Longrightarrow> prefixeq (map f xs) (map f ys)"
   2.136 +  by (auto simp: prefixeq_def)
   2.137 +
   2.138 +lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
   2.139 +  by (auto simp: prefix_def prefixeq_def)
   2.140 +
   2.141 +lemma prefix_simps [simp, code]:
   2.142 +  "prefix xs [] \<longleftrightarrow> False"
   2.143 +  "prefix [] (x # xs) \<longleftrightarrow> True"
   2.144 +  "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
   2.145 +  by (simp_all add: prefix_def cong: conj_cong)
   2.146 +
   2.147 +lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   2.148 +  apply (induct n arbitrary: xs ys)
   2.149 +   apply (case_tac ys, simp_all)[1]
   2.150 +  apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   2.151 +  done
   2.152 +
   2.153 +lemma not_prefixeq_cases:
   2.154 +  assumes pfx: "\<not> prefixeq ps ls"
   2.155 +  obtains
   2.156 +    (c1) "ps \<noteq> []" and "ls = []"
   2.157 +  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
   2.158 +  | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
   2.159 +proof (cases ps)
   2.160 +  case Nil
   2.161 +  then show ?thesis using pfx by simp
   2.162 +next
   2.163 +  case (Cons a as)
   2.164 +  note c = `ps = a#as`
   2.165 +  show ?thesis
   2.166 +  proof (cases ls)
   2.167 +    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
   2.168 +  next
   2.169 +    case (Cons x xs)
   2.170 +    show ?thesis
   2.171 +    proof (cases "x = a")
   2.172 +      case True
   2.173 +      have "\<not> prefixeq as xs" using pfx c Cons True by simp
   2.174 +      with c Cons True show ?thesis by (rule c2)
   2.175 +    next
   2.176 +      case False
   2.177 +      with c Cons show ?thesis by (rule c3)
   2.178 +    qed
   2.179 +  qed
   2.180 +qed
   2.181 +
   2.182 +lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
   2.183 +  assumes np: "\<not> prefixeq ps ls"
   2.184 +    and base: "\<And>x xs. P (x#xs) []"
   2.185 +    and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
   2.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)"
   2.187 +  shows "P ps ls" using np
   2.188 +proof (induct ls arbitrary: ps)
   2.189 +  case Nil then show ?case
   2.190 +    by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
   2.191 +next
   2.192 +  case (Cons y ys)
   2.193 +  then have npfx: "\<not> prefixeq ps (y # ys)" by simp
   2.194 +  then obtain x xs where pv: "ps = x # xs"
   2.195 +    by (rule not_prefixeq_cases) auto
   2.196 +  show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
   2.197 +qed
   2.198 +
   2.199 +
   2.200  subsection {* Parallel lists *}
   2.201  
   2.202  definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
     3.1 --- a/src/HOL/List_Prefix.thy	Wed Feb 19 10:21:02 2014 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,197 +0,0 @@
     3.4 -(*  Title:      HOL/List_Prefix.thy
     3.5 -    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3.6 -    Author:     Christian Sternagel, JAIST
     3.7 -*)
     3.8 -
     3.9 -header {* Parallel lists, list suffixes, and homeomorphic embedding *}
    3.10 -
    3.11 -theory List_Prefix
    3.12 -imports List
    3.13 -begin
    3.14 -
    3.15 -subsection {* Prefix order on lists *}
    3.16 -
    3.17 -definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    3.18 -  where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    3.19 -
    3.20 -definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    3.21 -  where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    3.22 -
    3.23 -interpretation prefix_order: order prefixeq prefix
    3.24 -  by default (auto simp: prefixeq_def prefix_def)
    3.25 -
    3.26 -interpretation prefix_bot: order_bot Nil prefixeq prefix
    3.27 -  by default (simp add: prefixeq_def)
    3.28 -
    3.29 -lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
    3.30 -  unfolding prefixeq_def by blast
    3.31 -
    3.32 -lemma prefixeqE [elim?]:
    3.33 -  assumes "prefixeq xs ys"
    3.34 -  obtains zs where "ys = xs @ zs"
    3.35 -  using assms unfolding prefixeq_def by blast
    3.36 -
    3.37 -lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
    3.38 -  unfolding prefix_def prefixeq_def by blast
    3.39 -
    3.40 -lemma prefixE' [elim?]:
    3.41 -  assumes "prefix xs ys"
    3.42 -  obtains z zs where "ys = xs @ z # zs"
    3.43 -proof -
    3.44 -  from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    3.45 -    unfolding prefix_def prefixeq_def by blast
    3.46 -  with that show ?thesis by (auto simp add: neq_Nil_conv)
    3.47 -qed
    3.48 -
    3.49 -lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
    3.50 -  unfolding prefix_def by blast
    3.51 -
    3.52 -lemma prefixE [elim?]:
    3.53 -  fixes xs ys :: "'a list"
    3.54 -  assumes "prefix xs ys"
    3.55 -  obtains "prefixeq xs ys" and "xs \<noteq> ys"
    3.56 -  using assms unfolding prefix_def by blast
    3.57 -
    3.58 -
    3.59 -subsection {* Basic properties of prefixes *}
    3.60 -
    3.61 -theorem Nil_prefixeq [iff]: "prefixeq [] xs"
    3.62 -  by (simp add: prefixeq_def)
    3.63 -
    3.64 -theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])"
    3.65 -  by (induct xs) (simp_all add: prefixeq_def)
    3.66 -
    3.67 -lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
    3.68 -proof
    3.69 -  assume "prefixeq xs (ys @ [y])"
    3.70 -  then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    3.71 -  show "xs = ys @ [y] \<or> prefixeq xs ys"
    3.72 -    by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
    3.73 -next
    3.74 -  assume "xs = ys @ [y] \<or> prefixeq xs ys"
    3.75 -  then show "prefixeq xs (ys @ [y])"
    3.76 -    by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI)
    3.77 -qed
    3.78 -
    3.79 -lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \<and> prefixeq xs ys)"
    3.80 -  by (auto simp add: prefixeq_def)
    3.81 -
    3.82 -lemma prefixeq_code [code]:
    3.83 -  "prefixeq [] xs \<longleftrightarrow> True"
    3.84 -  "prefixeq (x # xs) [] \<longleftrightarrow> False"
    3.85 -  "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefixeq xs ys"
    3.86 -  by simp_all
    3.87 -
    3.88 -lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs"
    3.89 -  by (induct xs) simp_all
    3.90 -
    3.91 -lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
    3.92 -  by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
    3.93 -
    3.94 -lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
    3.95 -  by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
    3.96 -
    3.97 -lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
    3.98 -  by (auto simp add: prefixeq_def)
    3.99 -
   3.100 -theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
   3.101 -  by (cases xs) (auto simp add: prefixeq_def)
   3.102 -
   3.103 -theorem prefixeq_append:
   3.104 -  "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefixeq us zs))"
   3.105 -  apply (induct zs rule: rev_induct)
   3.106 -   apply force
   3.107 -  apply (simp del: append_assoc add: append_assoc [symmetric])
   3.108 -  apply (metis append_eq_appendI)
   3.109 -  done
   3.110 -
   3.111 -lemma append_one_prefixeq:
   3.112 -  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
   3.113 -  proof (unfold prefixeq_def)
   3.114 -    assume a1: "\<exists>zs. ys = xs @ zs"
   3.115 -    then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
   3.116 -    assume a2: "length xs < length ys"
   3.117 -    have f1: "\<And>v. ([]\<Colon>'a list) @ v = v" using append_Nil2 by simp
   3.118 -    have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
   3.119 -    hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
   3.120 -    thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
   3.121 -  qed
   3.122 -
   3.123 -theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
   3.124 -  by (auto simp add: prefixeq_def)
   3.125 -
   3.126 -lemma prefixeq_same_cases:
   3.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"
   3.128 -  unfolding prefixeq_def by (force simp: append_eq_append_conv2)
   3.129 -
   3.130 -lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   3.131 -  by (auto simp add: prefixeq_def)
   3.132 -
   3.133 -lemma take_is_prefixeq: "prefixeq (take n xs) xs"
   3.134 -  unfolding prefixeq_def by (metis append_take_drop_id)
   3.135 -
   3.136 -lemma map_prefixeqI: "prefixeq xs ys \<Longrightarrow> prefixeq (map f xs) (map f ys)"
   3.137 -  by (auto simp: prefixeq_def)
   3.138 -
   3.139 -lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
   3.140 -  by (auto simp: prefix_def prefixeq_def)
   3.141 -
   3.142 -lemma prefix_simps [simp, code]:
   3.143 -  "prefix xs [] \<longleftrightarrow> False"
   3.144 -  "prefix [] (x # xs) \<longleftrightarrow> True"
   3.145 -  "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
   3.146 -  by (simp_all add: prefix_def cong: conj_cong)
   3.147 -
   3.148 -lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   3.149 -  apply (induct n arbitrary: xs ys)
   3.150 -   apply (case_tac ys, simp_all)[1]
   3.151 -  apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   3.152 -  done
   3.153 -
   3.154 -lemma not_prefixeq_cases:
   3.155 -  assumes pfx: "\<not> prefixeq ps ls"
   3.156 -  obtains
   3.157 -    (c1) "ps \<noteq> []" and "ls = []"
   3.158 -  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
   3.159 -  | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
   3.160 -proof (cases ps)
   3.161 -  case Nil
   3.162 -  then show ?thesis using pfx by simp
   3.163 -next
   3.164 -  case (Cons a as)
   3.165 -  note c = `ps = a#as`
   3.166 -  show ?thesis
   3.167 -  proof (cases ls)
   3.168 -    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
   3.169 -  next
   3.170 -    case (Cons x xs)
   3.171 -    show ?thesis
   3.172 -    proof (cases "x = a")
   3.173 -      case True
   3.174 -      have "\<not> prefixeq as xs" using pfx c Cons True by simp
   3.175 -      with c Cons True show ?thesis by (rule c2)
   3.176 -    next
   3.177 -      case False
   3.178 -      with c Cons show ?thesis by (rule c3)
   3.179 -    qed
   3.180 -  qed
   3.181 -qed
   3.182 -
   3.183 -lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
   3.184 -  assumes np: "\<not> prefixeq ps ls"
   3.185 -    and base: "\<And>x xs. P (x#xs) []"
   3.186 -    and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
   3.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)"
   3.188 -  shows "P ps ls" using np
   3.189 -proof (induct ls arbitrary: ps)
   3.190 -  case Nil then show ?case
   3.191 -    by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
   3.192 -next
   3.193 -  case (Cons y ys)
   3.194 -  then have npfx: "\<not> prefixeq ps (y # ys)" by simp
   3.195 -  then obtain x xs where pv: "ps = x # xs"
   3.196 -    by (rule not_prefixeq_cases) auto
   3.197 -  show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
   3.198 -qed
   3.199 -
   3.200 -end
     4.1 --- a/src/HOL/Main.thy	Wed Feb 19 10:21:02 2014 +0100
     4.2 +++ b/src/HOL/Main.thy	Wed Feb 19 10:30:21 2014 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  header {* Main HOL *}
     4.5  
     4.6  theory Main
     4.7 -imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_GFP
     4.8 +imports Predicate_Compile Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
     4.9  begin
    4.10  
    4.11  text {*
    4.12 @@ -32,7 +32,7 @@
    4.13    czero cinfinite cfinite csum cone ctwo Csum cprod cexp
    4.14    image2 image2p vimage2p Gr Grp collect fsts snds setl setr
    4.15    convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
    4.16 -  prefCl PrefCl Succ Shift shift proj
    4.17 +  Succ Shift shift proj
    4.18  
    4.19  no_syntax (xsymbols)
    4.20    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)