# HG changeset patch
# User nipkow
# Date 1078411718 -3600
# Node ID ade3d26e0caf7c658917970a73e0a43ae03ef8c5
# Parent  5cb24165a2e1f021e0b94ce1fb0a10782ba86f45
ML -> Isar

diff -r 5cb24165a2e1 -r ade3d26e0caf src/HOL/Lex/AutoMaxChop.ML
--- a/src/HOL/Lex/AutoMaxChop.ML	Thu Mar 04 12:06:07 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      HOL/Lex/AutoMaxChop.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Goal "delta A (xs@[y]) q = next A y (delta A xs q)";
-by (Simp_tac 1);
-qed "delta_snoc";
-
-Goal
- "!q ps res. auto_split A (delta A ps q) res ps xs = \
-\            maxsplit (%ys. fin A (delta A ys q)) res ps xs";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
-                           delsimps [thm"delta_append"]) 1);
-qed_spec_mp "auto_split_lemma";
-
-Goalw [thm"accepts_def"]
- "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
-by (stac ((read_instantiate [("s","start A")] (thm"delta_Nil")) RS sym) 1);
-by (stac auto_split_lemma 1);
-by (Simp_tac 1);
-qed_spec_mp "auto_split_is_maxsplit";
-
-Goal
- "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
-by (simp_tac (simpset() addsimps
-        [auto_split_is_maxsplit,thm"is_maxsplitter_maxsplit"]) 1);
-qed "is_maxsplitter_auto_split";
-
-Goalw [thm"auto_chop_def"]
- "is_maxchopper (accepts A) (auto_chop A)";
-by (rtac (thm"is_maxchopper_chop") 1);
-by (rtac is_maxsplitter_auto_split 1);
-qed "is_maxchopper_auto_chop";
diff -r 5cb24165a2e1 -r ade3d26e0caf 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
diff -r 5cb24165a2e1 -r ade3d26e0caf src/HOL/Lex/RegExp2NA.ML
--- a/src/HOL/Lex/RegExp2NA.ML	Thu Mar 04 12:06:07 2004 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML	Thu Mar 04 15:48:38 2004 +0100
@@ -424,6 +424,6 @@
     by (simp_tac (simpset() addsimps [thm"accepts_conv_steps"]) 1);
    by (simp_tac(simpset() addsimps [accepts_atom]) 1);
   by (Asm_simp_tac 1);
- by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
-by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
+ by (asm_simp_tac (simpset() addsimps [accepts_conc,thm"RegSet.conc_def"]) 1);
+by (asm_simp_tac (simpset() addsimps [accepts_star,thm"in_star"]) 1);
 qed_spec_mp "accepts_rexp2na";
diff -r 5cb24165a2e1 -r ade3d26e0caf src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Thu Mar 04 12:06:07 2004 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Mar 04 15:48:38 2004 +0100
@@ -625,6 +625,6 @@
     by (simp_tac (simpset() addsimps [thm"accepts_def"]) 1);
    by (simp_tac(simpset() addsimps [accepts_atom]) 1);
   by (asm_simp_tac (simpset() addsimps [accepts_or]) 1);
- by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
-by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
+ by (asm_simp_tac (simpset() addsimps [accepts_conc,thm"RegSet.conc_def"]) 1);
+by (asm_simp_tac (simpset() addsimps [accepts_star,thm"in_star"]) 1);
 qed "accepts_rexp2nae";
diff -r 5cb24165a2e1 -r ade3d26e0caf src/HOL/Lex/RegSet.ML
--- a/src/HOL/Lex/RegSet.ML	Thu Mar 04 12:06:07 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      HOL/Lex/RegSet.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-AddIffs [star.NilI];
-Addsimps [star.ConsI];
-AddIs [star.ConsI];
-
-Goal "(!xs: set xss. xs:S) --> concat xss : star S";
-by (induct_tac "xss" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed_spec_mp "concat_in_star";
-
-Goal
- "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
-by (rtac iffI 1);
- by (etac star.induct 1);
-  by (res_inst_tac [("x","[]")] exI 1);
-  by (Simp_tac 1);
- by (Clarify_tac 1);
- by (res_inst_tac [("x","a#us")] exI 1);
- by (Asm_simp_tac 1);
-by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [concat_in_star]) 1);
-qed "in_star";
diff -r 5cb24165a2e1 -r ade3d26e0caf src/HOL/Lex/RegSet.thy
--- a/src/HOL/Lex/RegSet.thy	Thu Mar 04 12:06:07 2004 +0100
+++ b/src/HOL/Lex/RegSet.thy	Thu Mar 04 15:48:38 2004 +0100
@@ -6,16 +6,32 @@
 Regular sets
 *)
 
-RegSet = Main +
+theory RegSet = Main:
 
 constdefs
- conc :: 'a list set => 'a list set => 'a list set
+ conc :: "'a list set => 'a list set => 'a list set"
 "conc A B == {xs@ys | xs ys. xs:A & ys:B}"
 
-consts star :: 'a list set => 'a list set
+consts star :: "'a list set => 'a list set"
 inductive "star A"
-intrs
-  NilI   "[] : star A"
-  ConsI  "[| a:A; as : star A |] ==> a@as : star A"
+intros
+  NilI[iff]:   "[] : star A"
+  ConsI[intro,simp]:  "[| a:A; as : star A |] ==> a@as : star A"
+
+lemma concat_in_star: "!xs: set xss. xs:S ==> concat xss : star S"
+by (induct "xss") simp_all
+
+lemma in_star:
+ "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))"
+apply (rule iffI)
+ apply (erule star.induct)
+  apply (rule_tac x = "[]" in exI)
+  apply simp
+ apply clarify
+ apply (rule_tac x = "a#us" in exI)
+ apply simp
+apply clarify
+apply (simp add: concat_in_star)
+done
 
 end
diff -r 5cb24165a2e1 -r ade3d26e0caf src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Mar 04 12:06:07 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,208 +0,0 @@
-(*  Title:      HOL/Lex/RegSet_of_nat_DA.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Addsimps [in_set_butlast_appendI, less_SucI];
-AddIs    [in_set_butlast_appendI];
-Addsimps [image_eqI];
-
-(* Lists *)
-
-Goal "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
-by (case_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "butlast_empty";
-AddIffs [butlast_empty];
-
-Goal "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
-by (induct_tac "xss" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps) 1);
-by (rtac conjI 1);
- by (Clarify_tac 1);
- by (rtac conjI 1);
-  by (Blast_tac 1);
- by (Clarify_tac 1);
- by (subgoal_tac "xs=[]" 1);
-  by (Asm_full_simp_tac 1);
- by (Blast_tac 1);
-by (blast_tac (claset() addDs [in_set_butlastD]) 1);
-qed_spec_mp "in_set_butlast_concatI";
-
-(* Regular sets *)
-
-(* The main lemma:
-   how to decompose a trace into a prefix, a list of loops and a suffix.
-*)
-Goal "!i. k : set(trace d i xs) --> (? pref mids suf. \
-\ xs = pref @ concat mids @ suf & \
-\ deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) & \
-\ (!mid:set mids. (deltas d mid k = k) & \
-\                 (!n:set(butlast(trace d k mid)). n ~= k)) & \
-\ (!n:set(butlast(trace d k suf)). n ~= k))";
-by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (rename_tac "a as" 1);
-by (rtac allI 1);
-by (case_tac "d a i = k" 1);
- by (strip_tac 1);
- by (res_inst_tac[("x","[a]")]exI 1);
- by (Asm_full_simp_tac 1);
- by (case_tac "k : set(trace d (d a i) as)" 1);
-  by (etac allE 1);
-  by (etac impE 1);
-   by (assume_tac 1);
-  by (REPEAT(etac exE 1));
-  by (res_inst_tac[("x","pref#mids")]exI 1);
-  by (res_inst_tac[("x","suf")]exI 1);
-  by (Asm_full_simp_tac 1);
- by (res_inst_tac[("x","[]")]exI 1);
- by (res_inst_tac[("x","as")]exI 1);
- by (Asm_full_simp_tac 1);
- by (blast_tac (claset() addDs [in_set_butlastD]) 1);
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (etac allE 1);
-by (etac impE 1);
- by (assume_tac 1);
-by (REPEAT(etac exE 1));
-by (res_inst_tac[("x","a#pref")]exI 1);
-by (res_inst_tac[("x","mids")]exI 1);
-by (res_inst_tac[("x","suf")]exI 1);
-by (Asm_simp_tac 1);
-qed_spec_mp "decompose";
-
-Goal "!i. length(trace d i xs) = length xs";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "length_trace";
-Addsimps [length_trace];
-
-Goal "!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "deltas_append";
-Addsimps [deltas_append];
-
-Goal "!i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "trace_append";
-Addsimps [trace_append];
-
-Goal "(!xs: set xss. deltas d xs i = i) --> \
-\         trace d i (concat xss) = concat (map (trace d i) xss)";
-by (induct_tac "xss" 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "trace_concat";
-Addsimps [trace_concat];
-
-Goal "!i. (trace d i xs = []) = (xs = [])";
-by (case_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "trace_is_Nil";
-Addsimps [trace_is_Nil];
-
-Goal "(trace d i xs = n#ns) = \
-\         (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)";
-by (case_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed_spec_mp "trace_is_Cons_conv";
-Addsimps [trace_is_Cons_conv];
-
-Goal "!i. set(trace d i xs) = \
-\ (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))";
-by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [insert_commute]) 1);
-qed "set_trace_conv";
-
-Goal
- "(!mid:set mids. deltas d mid k = k) --> deltas d (concat mids) k = k";
-by (induct_tac "mids" 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "deltas_concat";
-Addsimps [deltas_concat];
-
-Goal "[| n < Suc k; n ~= k |] ==> n < k";
-by (arith_tac 1);
-val lemma = result();
-
-Goal
- "!i j xs. xs : regset d i j k = \
-\          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
-by (induct_tac "k" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [thm"list.split"]) 1);
-by (strip_tac 1);
-by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
-by (rtac iffI 1);
- by (etac disjE 1);
-  by (Asm_simp_tac 1);
- by (REPEAT(eresolve_tac[exE,conjE] 1));
- by (Asm_full_simp_tac 1);
- by (subgoal_tac
-      "(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n" 1);
-  by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
- by (etac star.induct 1);
-  by (Simp_tac 1);
- by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
-by (case_tac "n : set(butlast(trace d i xs))" 1);
- by (rtac disjI1 2);
- by (blast_tac (claset() addIs [lemma]) 2);
-by (rtac disjI2 1);
-by (dtac (in_set_butlastD RS decompose) 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("x","pref")] exI 1);
-by (Asm_full_simp_tac 1);
-by (rtac conjI 1);
- by (rtac ballI 1);
- by (rtac lemma 1);
-  by (Asm_simp_tac 2);
- by (EVERY[dtac bspec 1, atac 2]);
- by (Asm_simp_tac 1);
-by (res_inst_tac [("x","concat mids")] exI 1);
-by (Simp_tac 1);
-by (rtac conjI 1);
- by (rtac concat_in_star 1);
- by (Asm_simp_tac 1);
- by (rtac ballI 1);
- by (rtac ballI 1);
- by (rtac lemma 1);
-  by (Asm_simp_tac 2);
- by (EVERY[dtac bspec 1, atac 2]);
- by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
-by (rtac ballI 1);
-by (rtac lemma 1);
- by (Auto_tac);
-qed_spec_mp "regset_spec";
-
-Goalw [bounded_def]
- "bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)";
-by (induct_tac "xs" 1);
- by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
-qed_spec_mp "trace_below";
-
-Goal "[| bounded d k; i < k; j < k |] ==> \
-\     regset d i j k = {xs. deltas d xs i = j}";
-by (rtac set_ext 1);
-by (simp_tac (simpset() addsimps [regset_spec]) 1);
-by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
-qed "regset_below";
-
-Goalw [bounded_def]
- "bounded d k ==> !i. i < k --> deltas d w i < k";
-by (induct_tac "w" 1);
- by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
-qed_spec_mp "deltas_below";
-
-Goalw [regset_of_DA_def]
- "[| bounded (next A) k; start A < k; j < k |] ==> \
-\ w : regset_of_DA A k = accepts A w";
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps
- [regset_below,deltas_below,thm"accepts_def",thm"delta_def"]) 1);
-qed "regset_DA_equiv";
diff -r 5cb24165a2e1 -r ade3d26e0caf src/HOL/Lex/RegSet_of_nat_DA.thy
--- a/src/HOL/Lex/RegSet_of_nat_DA.thy	Thu Mar 04 12:06:07 2004 +0100
+++ b/src/HOL/Lex/RegSet_of_nat_DA.thy	Thu Mar 04 15:48:38 2004 +0100
@@ -15,21 +15,21 @@
                         else atoms d i j as
 *)
 
-RegSet_of_nat_DA = RegSet + DA +
+theory RegSet_of_nat_DA = RegSet + DA:
 
 types 'a nat_next = "'a => nat => nat"
 
-syntax deltas :: 'a nat_next => 'a list => nat => nat
+syntax deltas :: "'a nat_next => 'a list => nat => nat"
 translations "deltas" == "foldl2"
 
-consts trace :: 'a nat_next => nat => 'a list => nat list
+consts trace :: "'a nat_next => nat => 'a list => nat list"
 primrec
 "trace d i [] = []"
 "trace d i (x#xs) = d x i # trace d (d x i) xs"
 
 (* conversion a la Warshall *)
 
-consts regset :: 'a nat_next => nat => nat => nat => 'a list set
+consts regset :: "'a nat_next => nat => nat => nat => 'a list set"
 primrec
 "regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
                           else {[a] | a. d a i = j})"
@@ -39,10 +39,198 @@
                                    (regset d k j k))"
 
 constdefs
- regset_of_DA :: ('a,nat)da => nat => 'a list set
+ regset_of_DA :: "('a,nat)da => nat => 'a list set"
 "regset_of_DA A k == UN j:{j. j<k & fin A j}. regset (next A) (start A) j k"
 
  bounded :: "'a => nat => bool"
 "bounded d k == !n. n < k --> (!x. d x n < k)"
 
+declare
+  in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp]
+
+(* Lists *)
+
+lemma butlast_empty[iff]:
+  "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"
+by (case_tac "xs") simp_all
+
+lemma in_set_butlast_concatI:
+ "x:set(butlast xs) ==> xs:set xss ==> x:set(butlast(concat xss))"
+apply (induct "xss")
+ apply simp
+apply (simp add: butlast_append del: ball_simps)
+apply (rule conjI)
+ apply (clarify)
+ apply (erule disjE)
+  apply (blast)
+ apply (subgoal_tac "xs=[]")
+  apply simp
+ apply (blast)
+apply (blast dest: in_set_butlastD)
+done
+
+(* Regular sets *)
+
+(* The main lemma:
+   how to decompose a trace into a prefix, a list of loops and a suffix.
+*)
+lemma decompose[rule_format]:
+ "!i. k : set(trace d i xs) --> (EX pref mids suf.
+  xs = pref @ concat mids @ suf &
+  deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) &
+  (!mid:set mids. (deltas d mid k = k) &
+                  (!n:set(butlast(trace d k mid)). n ~= k)) &
+  (!n:set(butlast(trace d k suf)). n ~= k))"
+apply (induct "xs")
+ apply (simp)
+apply (rename_tac a as)
+apply (intro strip)
+apply (case_tac "d a i = k")
+ apply (rule_tac x = "[a]" in exI)
+ apply simp
+ apply (case_tac "k : set(trace d (d a i) as)")
+  apply (erule allE)
+  apply (erule impE)
+   apply (assumption)
+  apply (erule exE)+
+  apply (rule_tac x = "pref#mids" in exI)
+  apply (rule_tac x = "suf" in exI)
+  apply simp
+ apply (rule_tac x = "[]" in exI)
+ apply (rule_tac x = "as" in exI)
+ apply simp
+ apply (blast dest: in_set_butlastD)
+apply simp
+apply (erule allE)
+apply (erule impE)
+ apply (assumption)
+apply (erule exE)+
+apply (rule_tac x = "a#pref" in exI)
+apply (rule_tac x = "mids" in exI)
+apply (rule_tac x = "suf" in exI)
+apply simp
+done
+
+lemma length_trace[simp]: "!!i. length(trace d i xs) = length xs"
+by (induct "xs") simp_all
+
+lemma deltas_append[simp]:
+  "!!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"
+by (induct "xs") simp_all
+
+lemma trace_append[simp]:
+  "!!i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"
+by (induct "xs") simp_all
+
+lemma trace_concat[simp]:
+ "(!xs: set xss. deltas d xs i = i) ==>
+  trace d i (concat xss) = concat (map (trace d i) xss)"
+by (induct "xss") simp_all
+
+lemma trace_is_Nil[simp]: "!!i. (trace d i xs = []) = (xs = [])"
+by (case_tac "xs") simp_all
+
+lemma trace_is_Cons_conv[simp]:
+ "(trace d i xs = n#ns) =
+  (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)"
+apply (case_tac "xs")
+apply simp_all
+apply (blast)
+done
+
+lemma set_trace_conv:
+ "!!i. set(trace d i xs) =
+  (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"
+apply (induct "xs")
+ apply (simp)
+apply (simp add: insert_commute)
+done
+
+lemma deltas_concat[simp]:
+ "(!mid:set mids. deltas d mid k = k) ==> deltas d (concat mids) k = k"
+by (induct mids) simp_all
+
+lemma lem: "[| n < Suc k; n ~= k |] ==> n < k"
+by arith
+
+lemma regset_spec:
+ "!!i j xs. xs : regset d i j k =
+        ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)"
+apply (induct k)
+ apply(simp split: list.split)
+ apply(fastsimp)
+apply (simp add: conc_def)
+apply (rule iffI)
+ apply (erule disjE)
+  apply simp
+ apply (erule exE conjE)+
+ apply simp
+ apply (subgoal_tac
+      "(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n")
+  apply (simp add: set_trace_conv butlast_append ball_Un)
+ apply (erule star.induct)
+  apply (simp)
+ apply (simp add: set_trace_conv butlast_append ball_Un)
+apply (case_tac "n : set(butlast(trace d i xs))")
+ prefer 2 apply (rule disjI1)
+ apply (blast intro:lem)
+apply (rule disjI2)
+apply (drule in_set_butlastD[THEN decompose])
+apply (clarify)
+apply (rule_tac x = "pref" in exI)
+apply simp
+apply (rule conjI)
+ apply (rule ballI)
+ apply (rule lem)
+  prefer 2 apply simp
+ apply (drule bspec) prefer 2 apply assumption
+ apply simp
+apply (rule_tac x = "concat mids" in exI)
+apply (simp)
+apply (rule conjI)
+ apply (rule concat_in_star)
+ apply simp
+ apply (rule ballI)
+ apply (rule ballI)
+ apply (rule lem)
+  prefer 2 apply simp
+ apply (drule bspec) prefer 2 apply assumption
+ apply (simp add: image_eqI in_set_butlast_concatI)
+apply (rule ballI)
+apply (rule lem)
+ apply auto
+done
+
+lemma trace_below:
+ "bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)"
+apply (unfold bounded_def)
+apply (induct "xs")
+ apply simp
+apply (simp (no_asm))
+apply (blast)
+done
+
+lemma regset_below:
+ "[| bounded d k; i < k; j < k |] ==>
+  regset d i j k = {xs. deltas d xs i = j}"
+apply (rule set_ext)
+apply (simp add: regset_spec)
+apply (blast dest: trace_below in_set_butlastD)
+done
+
+lemma deltas_below:
+ "!!i. bounded d k ==> i < k ==> deltas d w i < k"
+apply (unfold bounded_def)
+apply (induct "w")
+ apply simp_all
+done
+
+lemma regset_DA_equiv:
+ "[| bounded (next A) k; start A < k; j < k |] ==> \
+\ w : regset_of_DA A k = accepts A w"
+apply(unfold regset_of_DA_def)
+apply (simp cong: conj_cong
+            add: regset_below deltas_below accepts_def delta_def)
+done
+
 end