src/HOL/Lex/AutoMaxChop.thy

--- a/src/HOL/Lex/AutoMaxChop.thy	Thu Mar 04 12:06:07 2004 +0100
+++ b/src/HOL/Lex/AutoMaxChop.thy	Thu Mar 04 15:48:38 2004 +0100
@@ -16,4 +16,37 @@
 constdefs
  auto_chop :: "('a,'s)da => 'a chopper"
 "auto_chop A == chop (%xs. auto_split A (start A) ([],xs) [] xs)"
+
+
+lemma delta_snoc: "delta A (xs@[y]) q = next A y (delta A xs q)";
+by simp
+
+lemma auto_split_lemma:
+ "!!q ps res. auto_split A (delta A ps q) res ps xs =
+              maxsplit (%ys. fin A (delta A ys q)) res ps xs"
+apply (induct xs)
+ apply simp
+apply (simp add: delta_snoc[symmetric] del: delta_append)
+done
+
+lemma auto_split_is_maxsplit:
+ "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs"
+apply (unfold accepts_def)
+apply (subst delta_Nil[where s = "start A", symmetric])
+apply (subst auto_split_lemma)
+apply simp
+done
+
+lemma is_maxsplitter_auto_split:
+ "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)"
+by (simp add: auto_split_is_maxsplit is_maxsplitter_maxsplit)
+
+
+lemma is_maxchopper_auto_chop:
+ "is_maxchopper (accepts A) (auto_chop A)"
+apply (unfold auto_chop_def)
+apply (rule is_maxchopper_chop)
+apply (rule is_maxsplitter_auto_split)
+done
+
 end