theory Prefix_subtract+
−
  imports Main "~~/src/HOL/Library/List_Prefix"+
−
begin+
−
+
−
+
−
section {* A small theory of prefix subtraction *}+
−
+
−
text {*+
−
  The notion of @{text "prefix_subtract"} makes +
−
  the second direction of the Myhill-Nerode theorem +
−
  more readable.+
−
*}+
−
+
−
instantiation list :: (type) minus+
−
begin+
−
+
−
fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" +
−
where+
−
  "minus_list []     xs     = []" +
−
| "minus_list (x#xs) []     = x#xs" +
−
| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"+
−
+
−
instance by default+
−
+
−
end+
−
+
−
lemma [simp]: "x - [] = x"+
−
by (induct x) (auto)+
−
+
−
lemma [simp]: "(x @ y) - x = y"+
−
by (induct x) (auto)+
−
+
−
lemma [simp]: "x - x = []"+
−
by (induct x) (auto)+
−
+
−
lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "+
−
by (induct x) (auto)+
−
+
−
lemma diff_prefix:+
−
  "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"+
−
by (auto elim: prefixE)+
−
+
−
lemma diff_diff_append: +
−
  "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"+
−
apply (clarsimp simp:strict_prefix_def)+
−
by (drule diff_prefix, auto elim:prefixE)+
−
+
−
lemma append_eq_cases:+
−
  assumes a: "x @ y = m @ n"+
−
  shows "x \<le> m \<or> m \<le> x"+
−
unfolding prefix_def using a+
−
by (auto simp add: append_eq_append_conv2)+
−
+
−
lemma append_eq_dest:+
−
  assumes a: "x @ y = m @ n" +
−
  shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"+
−
using append_eq_cases[OF a] a+
−
by (auto elim: prefixE)+
−
+
−
end+
−