--- a/Prefix_subtract.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Prefix_subtract.thy	Wed May 18 19:54:43 2011 +0000
@@ -1,59 +1,60 @@
 theory Prefix_subtract
-  imports Main 
-          "~~/src/HOL/Library/List_Prefix"
+  imports Main "~~/src/HOL/Library/List_Prefix"
 begin
 
+
 section {* A small theory of prefix subtraction *}
 
 text {*
-  The notion of @{text "prefix_subtract"} is need to make proofs more readable.
-  *}
+  The notion of @{text "prefix_subtract"} makes 
+  the second direction of the Myhill-Nerode theorem 
+  more readable.
+*}
+
+instantiation list :: (type) minus
+begin
 
-fun prefix_subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)
+fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
 where
-  "prefix_subtract []     xs     = []" 
-| "prefix_subtract (x#xs) []     = x#xs" 
-| "prefix_subtract (x#xs) (y#ys) = (if x = y then prefix_subtract xs ys else (x#xs))"
+  "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"
-apply (induct x)
-by (case_tac y, simp+)
+by (induct x) (auto)
 
 lemma [simp]: "x - x = []"
-by (induct x, auto)
-
-lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "
-by (induct x, auto)
-
-lemma [simp]: "x - [] = x"
-by (induct x, auto)
+by (induct x) (auto)
 
-lemma [simp]: "(x - y = []) \<Longrightarrow> (x \<le> y)"
-proof-   
-  have "\<exists>xa. x = xa @ (x - y) \<and> xa \<le> y"
-    apply (rule prefix_subtract.induct[of _ x y], simp+)
-    by (clarsimp, rule_tac x = "y # xa" in exI, simp+)
-  thus "(x - y = []) \<Longrightarrow> (x \<le> y)" by simp
-qed
+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)
+by (auto elim: prefixE)
 
-lemma diff_diff_appd: 
+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 app_eq_cases[rule_format]:
-  "\<forall> x . x @ y = m @ n \<longrightarrow> (x \<le> m \<or> m \<le> x)"
-apply (induct y, simp)
-apply (clarify, drule_tac x = "x @ [a]" in spec)
-by (clarsimp, auto simp:prefix_def)
+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 app_eq_dest:
-  "x @ y = m @ n \<Longrightarrow> 
-               (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
-by (frule_tac app_eq_cases, auto elim:prefixE)
+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