--- a/Theories/Prefix_subtract.thy	Tue May 31 20:32:49 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-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