--- a/NEWS Fri May 27 23:58:24 2016 +0200
+++ b/NEWS Sun May 29 14:10:48 2016 +0200
@@ -227,10 +227,11 @@
for polynomials over factorial rings. INCOMPATIBILITY.
* Library/Sublist.thy: added function "prefixes" and renamed
- prefixeq -> prefix
- prefix -> strict_prefix
- suffixeq -> suffix
- suffix -> strict_suffix
+ prefixeq -> prefix
+ prefix -> strict_prefix
+ suffixeq -> suffix
+ suffix -> strict_suffix
+ Added theory of longest common prefixes.
* Dropped various legacy fact bindings, whose replacements are often
of a more general type also:
--- a/src/HOL/Library/Sublist.thy Fri May 27 23:58:24 2016 +0200
+++ b/src/HOL/Library/Sublist.thy Sun May 29 14:10:48 2016 +0200
@@ -127,6 +127,10 @@
"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"
unfolding prefix_def by (force simp: append_eq_append_conv2)
+lemma prefix_length_prefix:
+ "prefix ps xs \<Longrightarrow> prefix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> prefix ps qs"
+by (auto simp: prefix_def) (metis append_Nil2 append_eq_append_conv_if)
+
lemma set_mono_prefix: "prefix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
by (auto simp add: prefix_def)
@@ -226,6 +230,128 @@
by (cases ys rule: rev_cases) auto
+subsection \<open>Longest Common Prefix\<close>
+
+definition Longest_common_prefix :: "'a list set \<Rightarrow> 'a list" where
+"Longest_common_prefix L = (GREATEST ps WRT length. \<forall>xs \<in> L. prefix ps xs)"
+
+lemma Longest_common_prefix_ex: "L \<noteq> {} \<Longrightarrow>
+ \<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)"
+ (is "_ \<Longrightarrow> \<exists>ps. ?P L ps")
+proof(induction "LEAST n. \<exists>xs \<in>L. n = length xs" arbitrary: L)
+ case 0
+ have "[] : L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close>
+ by auto
+ hence "?P L []" by(auto)
+ thus ?case ..
+next
+ case (Suc n)
+ let ?EX = "\<lambda>n. \<exists>xs\<in>L. n = length xs"
+ obtain x xs where xxs: "x#xs \<in> L" "size xs = n" using Suc.prems Suc.hyps(2)
+ by(metis LeastI_ex[of ?EX] Suc_length_conv ex_in_conv)
+ hence "[] \<notin> L" using Suc.hyps(2) by auto
+ show ?case
+ proof (cases "\<forall>xs \<in> L. \<exists>ys. xs = x#ys")
+ case True
+ let ?L = "{ys. x#ys \<in> L}"
+ have 1: "(LEAST n. \<exists>xs \<in> ?L. n = length xs) = n"
+ using xxs Suc.prems Suc.hyps(2) Least_le[of "?EX"]
+ by - (rule Least_equality, fastforce+)
+ have 2: "?L \<noteq> {}" using \<open>x # xs \<in> L\<close> by auto
+ from Suc.hyps(1)[OF 1[symmetric] 2] obtain ps where IH: "?P ?L ps" ..
+ { fix qs
+ assume "\<forall>qs. (\<forall>xa. x # xa \<in> L \<longrightarrow> prefix qs xa) \<longrightarrow> length qs \<le> length ps"
+ and "\<forall>xs\<in>L. prefix qs xs"
+ hence "length (tl qs) \<le> length ps"
+ by (metis Cons_prefix_Cons hd_Cons_tl list.sel(2) Nil_prefix)
+ hence "length qs \<le> Suc (length ps)" by auto
+ }
+ hence "?P L (x#ps)" using True IH by auto
+ thus ?thesis ..
+ next
+ case False
+ then obtain y ys where yys: "x\<noteq>y" "y#ys \<in> L" using \<open>[] \<notin> L\<close>
+ by (auto) (metis list.exhaust)
+ have "\<forall>qs. (\<forall>xs\<in>L. prefix qs xs) \<longrightarrow> qs = []" using yys \<open>x#xs \<in> L\<close>
+ by auto (metis Cons_prefix_Cons prefix_Cons)
+ hence "?P L []" by auto
+ thus ?thesis ..
+ qed
+qed
+
+lemma Longest_common_prefix_unique: "L \<noteq> {} \<Longrightarrow>
+ \<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)"
+by(rule ex_ex1I[OF Longest_common_prefix_ex];
+ meson equals0I prefix_length_prefix prefix_order.antisym)
+
+lemma Longest_common_prefix_eq:
+ "\<lbrakk> L \<noteq> {}; \<forall>xs \<in> L. prefix ps xs;
+ \<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk>
+ \<Longrightarrow> Longest_common_prefix L = ps"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule some1_equality[OF Longest_common_prefix_unique]) auto
+
+lemma Longest_common_prefix_prefix:
+ "xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+
+lemma Longest_common_prefix_longest:
+ "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+
+lemma Longest_common_prefix_max_prefix:
+ "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> prefix ps (Longest_common_prefix L)"
+by(metis Longest_common_prefix_prefix Longest_common_prefix_longest
+ prefix_length_prefix ex_in_conv)
+
+lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []"
+using Longest_common_prefix_prefix prefix_Nil by blast
+
+lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow>
+ Longest_common_prefix (op # x ` L) = x # Longest_common_prefix L"
+apply(rule Longest_common_prefix_eq)
+ apply(simp)
+ apply (simp add: Longest_common_prefix_prefix)
+apply simp
+by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2)
+ Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc)
+
+lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L" "\<forall>xs\<in>L. hd xs = x"
+shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}"
+proof -
+ have "L = op # x ` {ys. x#ys \<in> L}" using assms(2,3)
+ by (auto simp: image_def)(metis hd_Cons_tl)
+ thus ?thesis
+ by (metis Longest_common_prefix_image_Cons image_is_empty assms(1))
+qed
+
+lemma Longest_common_prefix_eq_Nil:
+ "\<lbrakk>x#ys \<in> L; y#zs \<in> L; x \<noteq> y \<rbrakk> \<Longrightarrow> Longest_common_prefix L = []"
+by (metis Longest_common_prefix_prefix list.inject prefix_Cons)
+
+
+fun longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"longest_common_prefix (x#xs) (y#ys) =
+ (if x=y then x # longest_common_prefix xs ys else [])" |
+"longest_common_prefix _ _ = []"
+
+lemma longest_common_prefix_prefix1:
+ "prefix (longest_common_prefix xs ys) xs"
+by(induction xs ys rule: longest_common_prefix.induct) auto
+
+lemma longest_common_prefix_prefix2:
+ "prefix (longest_common_prefix xs ys) ys"
+by(induction xs ys rule: longest_common_prefix.induct) auto
+
+lemma longest_common_prefix_max_prefix:
+ "\<lbrakk> prefix ps xs; prefix ps ys \<rbrakk>
+ \<Longrightarrow> prefix ps (longest_common_prefix xs ys)"
+by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct)
+ (auto simp: prefix_Cons)
+
+
subsection \<open>Parallel lists\<close>
definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<parallel>" 50)
--- a/src/HOL/List.thy Fri May 27 23:58:24 2016 +0200
+++ b/src/HOL/List.thy Sun May 29 14:10:48 2016 +0200
@@ -1002,6 +1002,12 @@
(ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
by(cases ys) auto
+lemma longest_common_prefix:
+ "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys'
+ \<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')"
+by (induct xs ys rule: list_induct2')
+ (blast, blast, blast,
+ metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
@@ -1961,6 +1967,12 @@
"xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] & butlast ys = xs & last ys = x)"
by fastforce
+corollary longest_common_suffix:
+ "\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
+ \<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> last ys')"
+using longest_common_prefix[of "rev xs" "rev ys"]
+unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
+
subsubsection \<open>@{const take} and @{const drop}\<close>