src/HOL/Library/Sublist.thy
changeset 63173 3413b1cf30cd
parent 63155 ea8540c71581
child 63649 e690d6f2185b
     1.1 --- a/src/HOL/Library/Sublist.thy	Fri May 27 23:58:24 2016 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Sun May 29 14:10:48 2016 +0200
     1.3 @@ -127,6 +127,10 @@
     1.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"
     1.5    unfolding prefix_def by (force simp: append_eq_append_conv2)
     1.6  
     1.7 +lemma prefix_length_prefix:
     1.8 +  "prefix ps xs \<Longrightarrow> prefix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> prefix ps qs"
     1.9 +by (auto simp: prefix_def) (metis append_Nil2 append_eq_append_conv_if)
    1.10 +
    1.11  lemma set_mono_prefix: "prefix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
    1.12    by (auto simp add: prefix_def)
    1.13  
    1.14 @@ -226,6 +230,128 @@
    1.15  by (cases ys rule: rev_cases) auto
    1.16  
    1.17  
    1.18 +subsection \<open>Longest Common Prefix\<close>
    1.19 +
    1.20 +definition Longest_common_prefix :: "'a list set \<Rightarrow> 'a list" where
    1.21 +"Longest_common_prefix L = (GREATEST ps WRT length. \<forall>xs \<in> L. prefix ps xs)"
    1.22 +
    1.23 +lemma Longest_common_prefix_ex: "L \<noteq> {} \<Longrightarrow>
    1.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)"
    1.25 +  (is "_ \<Longrightarrow> \<exists>ps. ?P L ps")
    1.26 +proof(induction "LEAST n. \<exists>xs \<in>L. n = length xs" arbitrary: L)
    1.27 +  case 0
    1.28 +  have "[] : L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close>
    1.29 +    by auto
    1.30 +  hence "?P L []" by(auto)
    1.31 +  thus ?case ..
    1.32 +next
    1.33 +  case (Suc n)
    1.34 +  let ?EX = "\<lambda>n. \<exists>xs\<in>L. n = length xs"
    1.35 +  obtain x xs where xxs: "x#xs \<in> L" "size xs = n" using Suc.prems Suc.hyps(2)
    1.36 +    by(metis LeastI_ex[of ?EX] Suc_length_conv ex_in_conv)
    1.37 +  hence "[] \<notin> L" using Suc.hyps(2) by auto
    1.38 +  show ?case
    1.39 +  proof (cases "\<forall>xs \<in> L. \<exists>ys. xs = x#ys")
    1.40 +    case True
    1.41 +    let ?L = "{ys. x#ys \<in> L}"
    1.42 +    have 1: "(LEAST n. \<exists>xs \<in> ?L. n = length xs) = n"
    1.43 +      using xxs Suc.prems Suc.hyps(2) Least_le[of "?EX"]
    1.44 +      by - (rule Least_equality, fastforce+)
    1.45 +    have 2: "?L \<noteq> {}" using \<open>x # xs \<in> L\<close> by auto
    1.46 +    from Suc.hyps(1)[OF 1[symmetric] 2] obtain ps where IH: "?P ?L ps" ..
    1.47 +    { fix qs
    1.48 +      assume "\<forall>qs. (\<forall>xa. x # xa \<in> L \<longrightarrow> prefix qs xa) \<longrightarrow> length qs \<le> length ps"
    1.49 +      and "\<forall>xs\<in>L. prefix qs xs"
    1.50 +      hence "length (tl qs) \<le> length ps"
    1.51 +        by (metis Cons_prefix_Cons hd_Cons_tl list.sel(2) Nil_prefix) 
    1.52 +      hence "length qs \<le> Suc (length ps)" by auto
    1.53 +    }
    1.54 +    hence "?P L (x#ps)" using True IH by auto
    1.55 +    thus ?thesis ..
    1.56 +  next
    1.57 +    case False
    1.58 +    then obtain y ys where yys: "x\<noteq>y" "y#ys \<in> L" using \<open>[] \<notin> L\<close>
    1.59 +      by (auto) (metis list.exhaust)
    1.60 +    have "\<forall>qs. (\<forall>xs\<in>L. prefix qs xs) \<longrightarrow> qs = []" using yys \<open>x#xs \<in> L\<close>
    1.61 +      by auto (metis Cons_prefix_Cons prefix_Cons)
    1.62 +    hence "?P L []" by auto
    1.63 +    thus ?thesis ..
    1.64 +  qed
    1.65 +qed
    1.66 +
    1.67 +lemma Longest_common_prefix_unique: "L \<noteq> {} \<Longrightarrow>
    1.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)"
    1.69 +by(rule ex_ex1I[OF Longest_common_prefix_ex];
    1.70 +   meson equals0I prefix_length_prefix prefix_order.antisym)
    1.71 +
    1.72 +lemma Longest_common_prefix_eq:
    1.73 + "\<lbrakk> L \<noteq> {};  \<forall>xs \<in> L. prefix ps xs;
    1.74 +    \<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk>
    1.75 +  \<Longrightarrow> Longest_common_prefix L = ps"
    1.76 +unfolding Longest_common_prefix_def GreatestM_def
    1.77 +by(rule some1_equality[OF Longest_common_prefix_unique]) auto
    1.78 +
    1.79 +lemma Longest_common_prefix_prefix:
    1.80 +  "xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs"
    1.81 +unfolding Longest_common_prefix_def GreatestM_def
    1.82 +by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
    1.83 +
    1.84 +lemma Longest_common_prefix_longest:
    1.85 +  "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)"
    1.86 +unfolding Longest_common_prefix_def GreatestM_def
    1.87 +by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
    1.88 +
    1.89 +lemma Longest_common_prefix_max_prefix:
    1.90 +  "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> prefix ps (Longest_common_prefix L)"
    1.91 +by(metis Longest_common_prefix_prefix Longest_common_prefix_longest
    1.92 +     prefix_length_prefix ex_in_conv)
    1.93 +
    1.94 +lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []"
    1.95 +using Longest_common_prefix_prefix prefix_Nil by blast
    1.96 +
    1.97 +lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow>
    1.98 +  Longest_common_prefix (op # x ` L) = x # Longest_common_prefix L"
    1.99 +apply(rule Longest_common_prefix_eq)
   1.100 +  apply(simp)
   1.101 + apply (simp add: Longest_common_prefix_prefix)
   1.102 +apply simp
   1.103 +by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2)
   1.104 +     Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc)
   1.105 +
   1.106 +lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L"  "\<forall>xs\<in>L. hd xs = x"
   1.107 +shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}"
   1.108 +proof -
   1.109 +  have "L = op # x ` {ys. x#ys \<in> L}" using assms(2,3)
   1.110 +    by (auto simp: image_def)(metis hd_Cons_tl)
   1.111 +  thus ?thesis
   1.112 +    by (metis Longest_common_prefix_image_Cons image_is_empty assms(1))
   1.113 +qed
   1.114 +
   1.115 +lemma Longest_common_prefix_eq_Nil:
   1.116 +  "\<lbrakk>x#ys \<in> L; y#zs \<in> L; x \<noteq> y \<rbrakk> \<Longrightarrow> Longest_common_prefix L = []"
   1.117 +by (metis Longest_common_prefix_prefix list.inject prefix_Cons)
   1.118 +
   1.119 +
   1.120 +fun longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.121 +"longest_common_prefix (x#xs) (y#ys) =
   1.122 +  (if x=y then x # longest_common_prefix xs ys else [])" |
   1.123 +"longest_common_prefix _ _ = []"
   1.124 +
   1.125 +lemma longest_common_prefix_prefix1:
   1.126 +  "prefix (longest_common_prefix xs ys) xs"
   1.127 +by(induction xs ys rule: longest_common_prefix.induct) auto
   1.128 +
   1.129 +lemma longest_common_prefix_prefix2:
   1.130 +  "prefix (longest_common_prefix xs ys) ys"
   1.131 +by(induction xs ys rule: longest_common_prefix.induct) auto
   1.132 +
   1.133 +lemma longest_common_prefix_max_prefix:
   1.134 +  "\<lbrakk> prefix ps xs; prefix ps ys \<rbrakk>
   1.135 +   \<Longrightarrow> prefix ps (longest_common_prefix xs ys)"
   1.136 +by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct)
   1.137 +  (auto simp: prefix_Cons)
   1.138 +
   1.139 +
   1.140  subsection \<open>Parallel lists\<close>
   1.141  
   1.142  definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)