added subtheory of longest common prefix
authornipkow
Sun May 29 14:10:48 2016 +0200 (2016-05-29)
changeset 631733413b1cf30cd
parent 63172 d4f459eb7ed0
child 63174 57c0d60e491c
added subtheory of longest common prefix
NEWS
src/HOL/Library/Sublist.thy
src/HOL/List.thy
     1.1 --- a/NEWS	Fri May 27 23:58:24 2016 +0200
     1.2 +++ b/NEWS	Sun May 29 14:10:48 2016 +0200
     1.3 @@ -227,10 +227,11 @@
     1.4  for polynomials over factorial rings.  INCOMPATIBILITY.
     1.5  
     1.6  * Library/Sublist.thy: added function "prefixes" and renamed
     1.7 - prefixeq -> prefix
     1.8 - prefix -> strict_prefix
     1.9 - suffixeq -> suffix
    1.10 - suffix -> strict_suffix
    1.11 +  prefixeq -> prefix
    1.12 +  prefix -> strict_prefix
    1.13 +  suffixeq -> suffix
    1.14 +  suffix -> strict_suffix
    1.15 +  Added theory of longest common prefixes.
    1.16  
    1.17  * Dropped various legacy fact bindings, whose replacements are often
    1.18  of a more general type also:
     2.1 --- a/src/HOL/Library/Sublist.thy	Fri May 27 23:58:24 2016 +0200
     2.2 +++ b/src/HOL/Library/Sublist.thy	Sun May 29 14:10:48 2016 +0200
     2.3 @@ -127,6 +127,10 @@
     2.4    "prefix (xs\<^sub>1::'a list) ys \<Longrightarrow> prefix xs\<^sub>2 ys \<Longrightarrow> prefix xs\<^sub>1 xs\<^sub>2 \<or> prefix xs\<^sub>2 xs\<^sub>1"
     2.5    unfolding prefix_def by (force simp: append_eq_append_conv2)
     2.6  
     2.7 +lemma prefix_length_prefix:
     2.8 +  "prefix ps xs \<Longrightarrow> prefix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> prefix ps qs"
     2.9 +by (auto simp: prefix_def) (metis append_Nil2 append_eq_append_conv_if)
    2.10 +
    2.11  lemma set_mono_prefix: "prefix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
    2.12    by (auto simp add: prefix_def)
    2.13  
    2.14 @@ -226,6 +230,128 @@
    2.15  by (cases ys rule: rev_cases) auto
    2.16  
    2.17  
    2.18 +subsection \<open>Longest Common Prefix\<close>
    2.19 +
    2.20 +definition Longest_common_prefix :: "'a list set \<Rightarrow> 'a list" where
    2.21 +"Longest_common_prefix L = (GREATEST ps WRT length. \<forall>xs \<in> L. prefix ps xs)"
    2.22 +
    2.23 +lemma Longest_common_prefix_ex: "L \<noteq> {} \<Longrightarrow>
    2.24 +  \<exists>ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
    2.25 +  (is "_ \<Longrightarrow> \<exists>ps. ?P L ps")
    2.26 +proof(induction "LEAST n. \<exists>xs \<in>L. n = length xs" arbitrary: L)
    2.27 +  case 0
    2.28 +  have "[] : L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close>
    2.29 +    by auto
    2.30 +  hence "?P L []" by(auto)
    2.31 +  thus ?case ..
    2.32 +next
    2.33 +  case (Suc n)
    2.34 +  let ?EX = "\<lambda>n. \<exists>xs\<in>L. n = length xs"
    2.35 +  obtain x xs where xxs: "x#xs \<in> L" "size xs = n" using Suc.prems Suc.hyps(2)
    2.36 +    by(metis LeastI_ex[of ?EX] Suc_length_conv ex_in_conv)
    2.37 +  hence "[] \<notin> L" using Suc.hyps(2) by auto
    2.38 +  show ?case
    2.39 +  proof (cases "\<forall>xs \<in> L. \<exists>ys. xs = x#ys")
    2.40 +    case True
    2.41 +    let ?L = "{ys. x#ys \<in> L}"
    2.42 +    have 1: "(LEAST n. \<exists>xs \<in> ?L. n = length xs) = n"
    2.43 +      using xxs Suc.prems Suc.hyps(2) Least_le[of "?EX"]
    2.44 +      by - (rule Least_equality, fastforce+)
    2.45 +    have 2: "?L \<noteq> {}" using \<open>x # xs \<in> L\<close> by auto
    2.46 +    from Suc.hyps(1)[OF 1[symmetric] 2] obtain ps where IH: "?P ?L ps" ..
    2.47 +    { fix qs
    2.48 +      assume "\<forall>qs. (\<forall>xa. x # xa \<in> L \<longrightarrow> prefix qs xa) \<longrightarrow> length qs \<le> length ps"
    2.49 +      and "\<forall>xs\<in>L. prefix qs xs"
    2.50 +      hence "length (tl qs) \<le> length ps"
    2.51 +        by (metis Cons_prefix_Cons hd_Cons_tl list.sel(2) Nil_prefix) 
    2.52 +      hence "length qs \<le> Suc (length ps)" by auto
    2.53 +    }
    2.54 +    hence "?P L (x#ps)" using True IH by auto
    2.55 +    thus ?thesis ..
    2.56 +  next
    2.57 +    case False
    2.58 +    then obtain y ys where yys: "x\<noteq>y" "y#ys \<in> L" using \<open>[] \<notin> L\<close>
    2.59 +      by (auto) (metis list.exhaust)
    2.60 +    have "\<forall>qs. (\<forall>xs\<in>L. prefix qs xs) \<longrightarrow> qs = []" using yys \<open>x#xs \<in> L\<close>
    2.61 +      by auto (metis Cons_prefix_Cons prefix_Cons)
    2.62 +    hence "?P L []" by auto
    2.63 +    thus ?thesis ..
    2.64 +  qed
    2.65 +qed
    2.66 +
    2.67 +lemma Longest_common_prefix_unique: "L \<noteq> {} \<Longrightarrow>
    2.68 +  \<exists>! ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
    2.69 +by(rule ex_ex1I[OF Longest_common_prefix_ex];
    2.70 +   meson equals0I prefix_length_prefix prefix_order.antisym)
    2.71 +
    2.72 +lemma Longest_common_prefix_eq:
    2.73 + "\<lbrakk> L \<noteq> {};  \<forall>xs \<in> L. prefix ps xs;
    2.74 +    \<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk>
    2.75 +  \<Longrightarrow> Longest_common_prefix L = ps"
    2.76 +unfolding Longest_common_prefix_def GreatestM_def
    2.77 +by(rule some1_equality[OF Longest_common_prefix_unique]) auto
    2.78 +
    2.79 +lemma Longest_common_prefix_prefix:
    2.80 +  "xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs"
    2.81 +unfolding Longest_common_prefix_def GreatestM_def
    2.82 +by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
    2.83 +
    2.84 +lemma Longest_common_prefix_longest:
    2.85 +  "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)"
    2.86 +unfolding Longest_common_prefix_def GreatestM_def
    2.87 +by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
    2.88 +
    2.89 +lemma Longest_common_prefix_max_prefix:
    2.90 +  "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> prefix ps (Longest_common_prefix L)"
    2.91 +by(metis Longest_common_prefix_prefix Longest_common_prefix_longest
    2.92 +     prefix_length_prefix ex_in_conv)
    2.93 +
    2.94 +lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []"
    2.95 +using Longest_common_prefix_prefix prefix_Nil by blast
    2.96 +
    2.97 +lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow>
    2.98 +  Longest_common_prefix (op # x ` L) = x # Longest_common_prefix L"
    2.99 +apply(rule Longest_common_prefix_eq)
   2.100 +  apply(simp)
   2.101 + apply (simp add: Longest_common_prefix_prefix)
   2.102 +apply simp
   2.103 +by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2)
   2.104 +     Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc)
   2.105 +
   2.106 +lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L"  "\<forall>xs\<in>L. hd xs = x"
   2.107 +shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}"
   2.108 +proof -
   2.109 +  have "L = op # x ` {ys. x#ys \<in> L}" using assms(2,3)
   2.110 +    by (auto simp: image_def)(metis hd_Cons_tl)
   2.111 +  thus ?thesis
   2.112 +    by (metis Longest_common_prefix_image_Cons image_is_empty assms(1))
   2.113 +qed
   2.114 +
   2.115 +lemma Longest_common_prefix_eq_Nil:
   2.116 +  "\<lbrakk>x#ys \<in> L; y#zs \<in> L; x \<noteq> y \<rbrakk> \<Longrightarrow> Longest_common_prefix L = []"
   2.117 +by (metis Longest_common_prefix_prefix list.inject prefix_Cons)
   2.118 +
   2.119 +
   2.120 +fun longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   2.121 +"longest_common_prefix (x#xs) (y#ys) =
   2.122 +  (if x=y then x # longest_common_prefix xs ys else [])" |
   2.123 +"longest_common_prefix _ _ = []"
   2.124 +
   2.125 +lemma longest_common_prefix_prefix1:
   2.126 +  "prefix (longest_common_prefix xs ys) xs"
   2.127 +by(induction xs ys rule: longest_common_prefix.induct) auto
   2.128 +
   2.129 +lemma longest_common_prefix_prefix2:
   2.130 +  "prefix (longest_common_prefix xs ys) ys"
   2.131 +by(induction xs ys rule: longest_common_prefix.induct) auto
   2.132 +
   2.133 +lemma longest_common_prefix_max_prefix:
   2.134 +  "\<lbrakk> prefix ps xs; prefix ps ys \<rbrakk>
   2.135 +   \<Longrightarrow> prefix ps (longest_common_prefix xs ys)"
   2.136 +by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct)
   2.137 +  (auto simp: prefix_Cons)
   2.138 +
   2.139 +
   2.140  subsection \<open>Parallel lists\<close>
   2.141  
   2.142  definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
     3.1 --- a/src/HOL/List.thy	Fri May 27 23:58:24 2016 +0200
     3.2 +++ b/src/HOL/List.thy	Sun May 29 14:10:48 2016 +0200
     3.3 @@ -1002,6 +1002,12 @@
     3.4   (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
     3.5  by(cases ys) auto
     3.6  
     3.7 +lemma longest_common_prefix:
     3.8 +  "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys'
     3.9 +       \<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')"
    3.10 +by (induct xs ys rule: list_induct2')
    3.11 +   (blast, blast, blast,
    3.12 +    metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
    3.13  
    3.14  text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
    3.15  
    3.16 @@ -1961,6 +1967,12 @@
    3.17    "xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] & butlast ys = xs & last ys = x)"
    3.18  by fastforce
    3.19  
    3.20 +corollary longest_common_suffix:
    3.21 +  "\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
    3.22 +       \<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> last ys')"
    3.23 +using longest_common_prefix[of "rev xs" "rev ys"]
    3.24 +unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
    3.25 +
    3.26  
    3.27  subsubsection \<open>@{const take} and @{const drop}\<close>
    3.28