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