# HG changeset patch
# User nipkow
# Date 893688416 -7200
# Node ID bc11b5b06f87c72763b75c84ac24547c7432b4ab
# Parent  dae4d63a1318f6498e6a76d28c29af1c7d902a57
Added conversion of reg.expr. to automata.
Renamed expand_const -> split_const.

diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/Auto.ML
--- a/src/HOL/Lex/Auto.ML	Mon Apr 27 16:45:27 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      HOL/Lex/Auto.ML
-    ID:         $Id$
-    Author:     Richard Mayr & Tobias Nipkow
-    Copyright   1995 TUM
-*)
-
-goalw Auto.thy [nexts_def] "nexts A st [] = st";
-by (Simp_tac 1);
-qed"nexts_Nil";
-
-goalw Auto.thy [nexts_def] "nexts A st (x#xs) = nexts A (next A st x) xs";
-by (Simp_tac 1);
-qed"nexts_Cons";
-
-Addsimps [nexts_Nil,nexts_Cons];
-
-goalw Auto.thy [acc_prefix_def] "~acc_prefix A st []";
-by (Simp_tac 1);
-qed"acc_prefix_Nil";
-Addsimps [acc_prefix_Nil];
-
-goalw Auto.thy [acc_prefix_def]
- "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
-by (simp_tac (simpset() addsimps [prefix_Cons]) 1);
-by Safe_tac;
-  by (Asm_full_simp_tac 1);
-  by (case_tac "zs=[]" 1);
-   by (hyp_subst_tac 1);
-   by (Asm_full_simp_tac 1);
-  by (Fast_tac 1);
- by (res_inst_tac [("x","[x]")] exI 1);
- by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by (res_inst_tac [("x","x#us")] exI 1);
-by (Asm_simp_tac 1);
-qed"acc_prefix_Cons";
-Addsimps [acc_prefix_Cons];
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/Auto.thy
--- a/src/HOL/Lex/Auto.thy	Mon Apr 27 16:45:27 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Title:      HOL/Lex/Auto.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1995 TUM
-
-Automata expressed as triples of
-  1. a start state,
-  2. a transition function and
-  3. a test for final states.
-
-NOTE: this functional representation is suitable for all kinds of automata,
-      not just finite ones!
-*)
-
-Auto = Prefix +
-
-types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
-
-constdefs
-
-  start :: ('a, 'b)auto => 'b
-  "start(A) == fst(A)"
-
-  next  :: ('a, 'b)auto => ('b => 'a => 'b)
-  "next(A) == fst(snd(A))"
-
-  fin   :: ('a, 'b)auto => ('b => bool)
-  "fin(A) == snd(snd(A))"
-
-  nexts :: ('a, 'b)auto => 'b => 'a list => 'b
-  "nexts(A) == foldl(next(A))"
-
-  accepts :: ('a,'b) auto => 'a list => bool
-  "accepts A == (%xs. fin A (nexts A (start A) xs))"
-
-  acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
-  "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
-
-end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -8,23 +8,42 @@
 
 Delsimps (ex_simps @ all_simps);
 
-open AutoChopper;
-
 infix repeat_RS;
 fun th1 repeat_RS th2 = ((th1 RS th2) repeat_RS th2) handle _ => th1;
 
 Addsimps [Let_def];
 
-goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
+goalw thy [acc_prefix_def] "~acc_prefix A [] s";
+by (Simp_tac 1);
+qed"acc_prefix_Nil";
+Addsimps [acc_prefix_Nil];
+
+goalw thy [acc_prefix_def]
+ "acc_prefix A (x#xs) s = (fin A (next A x s) | acc_prefix A xs (next A x s))";
+by (simp_tac (simpset() addsimps [prefix_Cons]) 1);
+by Safe_tac;
+  by (Asm_full_simp_tac 1);
+  by (case_tac "zs=[]" 1);
+   by (hyp_subst_tac 1);
+   by (Asm_full_simp_tac 1);
+  by (Fast_tac 1);
+ by (res_inst_tac [("x","[x]")] exI 1);
+ by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+by (res_inst_tac [("x","x#us")] exI 1);
+by (Asm_simp_tac 1);
+qed"acc_prefix_Cons";
+Addsimps [acc_prefix_Cons];
+
+goal thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 val accept_not_Nil = result() repeat_RS spec;
 Addsimps [accept_not_Nil];
 
-goal AutoChopper.thy
+goal thy
 "!st us. acc xs st [] us ([],ys) A = ([], zs) --> \
-\        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
+\        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))";
 by (list.induct_tac "xs" 1);
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (Simp_tac 1);
@@ -48,10 +67,10 @@
 val ex_special = result();
 
 
-goal AutoChopper.thy
+goal thy
 "! r erk l rst st ys yss zs::'a list. \
 \    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
-\    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
+\    ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)";
 by (list.induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (Asm_simp_tac 1);
@@ -67,10 +86,10 @@
 val step2_a = (result() repeat_RS spec) RS mp;
 
 
-goal AutoChopper.thy
+goal thy
  "! st erk r l rest ys yss zs.\
 \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
-\     (if acc_prefix A st xs \
+\     (if acc_prefix A xs st \
 \      then ys ~= [] \
 \      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
 by (Simp_tac 1);
@@ -82,7 +101,7 @@
 by (rename_tac "vss lrst" 1);  
 by (Asm_simp_tac 1);
 by (strip_tac 1);
-by (case_tac "acc_prefix A (next A st a) list" 1);
+by (case_tac "acc_prefix A list (next A a st)" 1);
  by (Asm_simp_tac 1);
 by (subgoal_tac "r @ [a] ~= []" 1);
  by (Fast_tac 1);
@@ -90,11 +109,11 @@
 val step2_b = (result() repeat_RS spec) RS mp;
 
 
-goal AutoChopper.thy  
+goal thy  
  "! st erk r l rest ys yss zs. \
 \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
-\     (if acc_prefix A st xs                   \
-\      then ? g. ys=r@g & fin A (nexts A st g)  \
+\     (if acc_prefix A xs st                   \
+\      then ? g. ys=r@g & fin A (delta A g st)  \
 \      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
 by (Simp_tac 1);
 by (list.induct_tac "xs" 1);
@@ -106,7 +125,7 @@
  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
  by (rename_tac "vss lrst" 1);  
  by (Asm_simp_tac 1);
- by (case_tac "acc_prefix A (next A st a) list" 1);
+ by (case_tac "acc_prefix A list (next A a st)" 1);
   by (strip_tac 1);
   by (res_inst_tac [("f","%k. a#k")] ex_special 1);
   by (Simp_tac 1);
@@ -129,10 +148,10 @@
 val step2_c = (result() repeat_RS spec) RS mp;
 
 
-goal AutoChopper.thy
+goal thy
  "! st erk r l rest ys yss zs. \
 \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
-\     (if acc_prefix A st xs       \
+\     (if acc_prefix A xs st       \
 \      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
 \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
 by (Simp_tac 1);
@@ -144,7 +163,7 @@
 by (rename_tac "vss lrst" 1);  
 by (Asm_simp_tac 1);
 by (strip_tac 1);
-by (case_tac "acc_prefix A (next A st a) list" 1);
+by (case_tac "acc_prefix A list (next A a st)" 1);
  by (Asm_simp_tac 1);
 by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
  by (Asm_simp_tac 2);
@@ -168,11 +187,11 @@
 val step2_d = (result() repeat_RS spec) RS mp;
 
 Delsimps [split_paired_All];
-goal AutoChopper.thy 
+goal thy 
 "! st erk r p ys yss zs. \
 \  acc xs st erk r p A = (ys#yss, zs) --> \
-\  (if acc_prefix A st xs  \
-\   then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
+\  (if acc_prefix A xs st  \
+\   then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (delta A as st))\
 \   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
 by (Simp_tac 1);
 by (list.induct_tac "xs" 1);
@@ -180,13 +199,13 @@
  by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
-by (case_tac "acc_prefix A (next A st a) list" 1);
+by (case_tac "acc_prefix A list (next A a st)" 1);
  by (rtac conjI 1);
   by (strip_tac 1);
   by (res_inst_tac [("f","%k. a#k")] ex_special 1);
   by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
    by (Simp_tac 1);
-  by (res_inst_tac [("P","%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
+  by (res_inst_tac [("P","%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (delta A as (next A a st)))")] exE 1);
    by (asm_simp_tac HOL_ss 1);
   by (res_inst_tac [("x","x")] exI 1);
   by (Asm_simp_tac 1);
@@ -197,7 +216,7 @@
  by (res_inst_tac [("f","%k. a#k")] ex_special 1);
  by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
   by (Simp_tac 1);
- by (res_inst_tac [("P","%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
+ by (res_inst_tac [("P","%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (delta A as (next A a st)))")] exE 1);
   by (asm_simp_tac HOL_ss 1);
  by (res_inst_tac [("x","x")] exI 1);
  by (Asm_simp_tac 1);
@@ -219,8 +238,8 @@
 val step2_e = (result() repeat_RS spec) RS mp;
 Addsimps[split_paired_All];
 
-goalw AutoChopper.thy [accepts_def, is_auto_chopper_def, auto_chopper_def,
-                       Chopper.is_longest_prefix_chopper_def]
+goalw thy [accepts_def, is_auto_chopper_def, auto_chopper_def,
+           Chopper.is_longest_prefix_chopper_def]
  "is_auto_chopper(auto_chopper)";
 by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
  by (rtac mp 1);
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -16,28 +16,33 @@
 A more efficient version is defined in AutoChopper1.
 *)
 
-AutoChopper = Auto + Chopper +
+AutoChopper = Prefix + DA + Chopper +
+
+constdefs
+ is_auto_chopper :: (('a,'s)da => 'a chopper) => bool
+"is_auto_chopper(chopperf) ==
+    !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
 
 consts
-  is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
-  auto_chopper :: ('a,'b)auto => 'a chopper
-  acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
+  acc :: "['a list, 's, 'a list, 'a list, 'a list list*'a list, ('a,'s)da]
           => 'a list list * 'a list"
-
-defs
-  is_auto_chopper_def "is_auto_chopper(chopperf) ==
-                       !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
-
-  auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
-
 primrec acc List.list
   "acc [] st ys zs chopsr A =
               (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
-  "acc(x#xs) st ys zs chopsr A =
-            (let s0 = start(A); nxt = next(A); fin = fin(A)
-             in if fin(nxt st x)
-                then acc xs (nxt st x) (zs@[x]) (zs@[x])
-                         (acc xs s0 [] [] ([],xs) A) A
-                else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
+  "acc(x#xs) s ys zs chopsr A =
+            (let t = next A x s
+             in if fin A t
+                then acc xs t (zs@[x]) (zs@[x])
+                         (acc xs (start A) [] [] ([],xs) A) A
+                else acc xs t ys (zs@[x]) chopsr A)"
+
+constdefs
+ auto_chopper :: ('a,'s)da => 'a chopper
+"auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
+
+(* acc_prefix is an auxiliary notion for the proof *)
+constdefs
+ acc_prefix :: ('a,'s)da => 'a list => 's => bool
+"acc_prefix A xs s == ? us. us <= xs & us~=[] & fin A (delta A us s)"
 
 end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/AutoChopper1.thy
--- a/src/HOL/Lex/AutoChopper1.thy	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/AutoChopper1.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -17,10 +17,10 @@
 No proofs yet.
 *)
 
-AutoChopper1 = Auto + Chopper + WF_Rel +
+AutoChopper1 = DA + Chopper + WF_Rel +
 
 consts
-  acc :: "(('a,'b)auto * 'a list * 'b * 'a list list * 'a list * 'a list)
+  acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
           => 'a list list * 'a list"
 recdef acc "inv_image (less_than ** less_than)
               (%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
@@ -29,7 +29,7 @@
 "acc(A,[],s,xss,zs,[]) = (xss, zs)"
 "acc(A,[],s,xss,zs,x#xs) = acc(A,zs,start A, xss @ [x#xs],[],[])"
 "acc(A,y#ys,s,xss,zs,xs) =
-  (let s' = next A s y;
+  (let s' = next A y s;
       zs' = (if fin A s' then [] else zs@[y]);
       xs' = (if fin A s' then xs@zs@[y] else xs)
    in acc(A,ys,s',xss,zs',xs'))"
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/AutoMaxChop.ML
--- a/src/HOL/Lex/AutoMaxChop.ML	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -4,29 +4,22 @@
     Copyright   1998 TUM
 *)
 
-goal thy "!q ys. nexts A q (xs@ys) = nexts A (nexts A q xs) ys";
-by(induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "nexts_append";
-Addsimps [nexts_append];
-
-goal thy "nexts A q (xs@[y]) = next A (nexts A q xs) y";
+goal thy "delta A (xs@[y]) q = next A y (delta A xs q)";
 by(Simp_tac 1);
-qed "nexts_snoc";
-Addsimps [nexts_append];
+qed "delta_snoc";
 
 goal thy
- "!q ps res. auto_split A (nexts A q ps) ps xs res = \
-\            maxsplit (%ys. fin A (nexts A q ys)) ps xs res";
+ "!q ps res. auto_split A (delta A ps q) ps xs res = \
+\            maxsplit (%ys. fin A (delta A ys q)) ps xs res";
 by(induct_tac "xs" 1);
 by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [nexts_snoc RS sym]
-                           delsimps [nexts_append]) 1);
+by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
+                           delsimps [delta_append]) 1);
 qed_spec_mp "auto_split_lemma";
 
 goalw thy [accepts_def]
  "auto_split A (start A) [] xs res = maxsplit (accepts A) [] xs res";
-by(stac ((read_instantiate [("st","start A")] nexts_Nil) RS sym) 1);
+by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
 by(stac auto_split_lemma 1);
 by(Simp_tac 1);
 qed_spec_mp "auto_split_is_maxsplit";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/AutoMaxChop.thy
--- a/src/HOL/Lex/AutoMaxChop.thy	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -4,17 +4,17 @@
     Copyright   1998 TUM
 *)
 
-AutoMaxChop = Auto + MaxChop +
+AutoMaxChop = DA + MaxChop +
 
 consts
- auto_split :: "('a,'s)auto => 's => 'a list => 'a list => 'a list * 'a list
+ auto_split :: "('a,'s)da => 's => 'a list => 'a list => 'a list * 'a list
                 => 'a list * 'a list"
 primrec auto_split list
 "auto_split A q ps []     res = (if fin A q then (ps,[]) else res)"
-"auto_split A q ps (x#xs) res = auto_split A (next A q x) (ps@[x]) xs
+"auto_split A q ps (x#xs) res = auto_split A (next A x q) (ps@[x]) xs
                                      (if fin A q then (ps,x#xs) else res)"
 
 constdefs
- auto_chop :: "('a,'s)auto => 'a chopper"
+ auto_chop :: "('a,'s)da => 'a chopper"
 "auto_chop A == chop (%xs. auto_split A (start A) [] xs ([],xs))"
 end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/AutoProj.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoProj.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOL/Lex/AutoProj.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+goalw thy [start_def] "start(q,d,f) = q";
+by(Simp_tac 1);
+qed "start_conv";
+
+goalw thy [next_def] "next(q,d,f) = d";
+by(Simp_tac 1);
+qed "next_conv";
+
+goalw thy [fin_def] "fin(q,d,f) = f";
+by(Simp_tac 1);
+qed "fin_conv";
+
+Addsimps [start_conv,next_conv,fin_conv];
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/AutoProj.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoProj.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/Lex/AutoProj.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Is there an optimal order of arguments for `next'?
+Currently we can have laws like `delta A (a#w) = delta A w o delta A a'
+Otherwise we could have `acceps A == fin A o delta A (start A)'
+and use foldl instead of foldl2.
+*)
+
+AutoProj = Prod +
+
+constdefs
+ start :: "'a * 'b * 'c => 'a"
+"start A == fst A"
+ next :: "'a * 'b * 'c => 'b"
+"next A == fst(snd(A))"
+ fin :: "'a * 'b * 'c => 'c"
+"fin A == snd(snd(A))"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/Automata.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Automata.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,43 @@
+(*  Title:      HOL/Lex/Automata.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+(*** Equivalence of NA and DA --- redundant ***)
+
+goalw thy [na2da_def]
+ "!Q. DA.delta (na2da A) w Q = lift(NA.delta A w) Q";
+by(induct_tac "w" 1);
+ by(ALLGOALS Asm_simp_tac);
+ by(ALLGOALS Blast_tac);
+qed_spec_mp "DA_delta_is_lift_NA_delta";
+
+goalw thy [DA.accepts_def,NA.accepts_def]
+  "NA.accepts A w = DA.accepts (na2da A) w";
+by(simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
+by(simp_tac (simpset() addsimps [na2da_def]) 1);
+qed "NA_DA_equiv";
+
+(*** Direct equivalence of NAe and DA ***)
+
+goalw thy [nae2da_def]
+ "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = lift(NAe.delta A w) Q";
+by(induct_tac "w" 1);
+ by(ALLGOALS Asm_simp_tac);
+ by(Blast_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "espclosure_DA_delta_is_lift_NAe_delta";
+
+goalw thy [nae2da_def]
+ "fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
+by(Simp_tac 1);
+val lemma = result();
+
+goalw thy [NAe.accepts_def,DA.accepts_def]
+  "NAe.accepts A w = DA.accepts (nae2da A) w";
+by(simp_tac (simpset() addsimps [lemma,steps_equiv_delta,
+     espclosure_DA_delta_is_lift_NAe_delta]) 1);
+by(simp_tac (simpset() addsimps [nae2da_def]) 1);
+by(Blast_tac 1);
+qed "NAe_DA_equiv";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/Automata.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Automata.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Lex/Automata.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Conversions between different kinds of automata
+*)
+
+Automata = DA + NAe +
+
+constdefs
+ na2da :: ('a,'s)na => ('a,'s set)da
+"na2da A == ({start A}, %a Q. lift(next A a) Q, %Q. ? q:Q. fin A q)"
+
+ nae2da :: ('a,'s)nae => ('a,'s set)da
+"nae2da A == ({start A},
+              %a Q. lift (next A (Some a)) ((eps A)^* ^^ Q),
+              %Q. ? p: (eps A)^* ^^ Q. fin A p)"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/DA.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/DA.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,31 @@
+(*  Title:      HOL/Lex/DA.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+goalw thy [foldl2_def] "foldl2 f [] a = a";
+by(Simp_tac 1);
+qed "foldl2_Nil";
+
+goalw thy [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)";
+by(Simp_tac 1);
+qed "foldl2_Cons";
+
+Addsimps [foldl2_Nil,foldl2_Cons];
+
+goalw thy [delta_def] "delta A [] s = s";
+by(Simp_tac 1);
+qed "delta_Nil";
+
+goalw thy [delta_def] "delta A (a#w) s = delta A w (next A a s)";
+by(Simp_tac 1);
+qed "delta_Cons";
+
+Addsimps [delta_Nil,delta_Cons];
+
+goal thy "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)";
+by(induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "delta_append";
+Addsimps [delta_append];
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/DA.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/DA.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Lex/DA.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Deterministic automata
+*)
+
+DA = List + AutoProj +
+
+types ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)"
+
+constdefs
+ foldl2 :: ('a => 'b => 'b) => 'a list => 'b => 'b
+"foldl2 f xs a == foldl (%a b. f b a) a xs"
+
+ delta :: ('a,'s)da => 'a list => 's => 's
+"delta A == foldl2 (next A)"
+
+ accepts ::  ('a,'s)da => 'a list => bool
+"accepts A == %w. fin A (delta A w (start A))"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -23,7 +23,7 @@
 \                      else let (xss,zs) = chop splitf post \
 \                             in (pre#xss,zs))";
 by(asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
-by(simp_tac (simpset() addsimps [Let_def] addsplits [expand_split]) 1);
+by(simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
 qed "chop_rule";
 
 goalw thy [is_maxsplitter_def,reducing_def]
@@ -34,11 +34,11 @@
 goal thy "!!P. is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
 by(res_inst_tac [("xs","xs")] length_induct 1);
-by(asm_simp_tac (simpset() delsplits [expand_if]
+by(asm_simp_tac (simpset() delsplits [split_if]
                            addsimps [chop_rule,is_maxsplitter_reducing]
                            addcongs [if_weak_cong]) 1);
 by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
-                                addsplits [expand_split]) 1);
+                                addsplits [split_split]) 1);
 qed_spec_mp "chop_concat";
 
 goal thy "!!P. is_maxsplitter P splitf ==> \
@@ -47,9 +47,9 @@
 by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
                            addcongs [if_weak_cong]) 1);
 by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
-                                addsplits [expand_split]) 1);
+                                addsplits [split_split]) 1);
 by(simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
-                       addsplits [expand_split]) 1);
+                       addsplits [split_split]) 1);
 be thin_rl 1;
 by(strip_tac 1);
 br ballI 1;
@@ -69,7 +69,7 @@
  be rev_mp 1;
  by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
  by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
-                        addsplits [expand_split]) 1);
+                        addsplits [split_split]) 1);
  by(Clarify_tac 1);
  br conjI 1;
   by(Clarify_tac 1);
@@ -81,7 +81,7 @@
  ba 1;
 by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
  by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
-                        addsplits [expand_split]) 1);
+                        addsplits [split_split]) 1);
 by(Clarify_tac 1);
 br conjI 1;
  by(Clarify_tac 1);
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/MaxPrefix.ML
--- a/src/HOL/Lex/MaxPrefix.ML	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -4,13 +4,13 @@
     Copyright   1998 TUM
 *)
 
-Delsplits [expand_if];
+Delsplits [split_if];
 goalw thy [is_maxpref_def] "!(ps::'a list) res. \
 \ (maxsplit P ps qs res = (xs,ys)) = \
 \ (if (? us. us <= qs & P(ps@us)) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \
 \  else (xs,ys)=res)";
 by(induct_tac "qs" 1);
- by(simp_tac (simpset() addsplits [expand_if]) 1);
+ by(simp_tac (simpset() addsplits [split_if]) 1);
  by(Blast_tac 1);
 by(Asm_simp_tac 1);
 be thin_rl 1;
@@ -47,7 +47,7 @@
 by(Asm_simp_tac 1);
 by(fast_tac (claset() addss simpset()) 1);
 qed_spec_mp "maxsplit_lemma";
-Addsplits [expand_if];
+Addsplits [split_if];
 
 goalw thy [is_maxpref_def]
  "!!P. ~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/NA.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/NA.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/Lex/NA.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Nondeterministic automata
+*)
+
+NA = List + AutoProj +
+
+types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
+
+syntax lift :: ('a => 'b set) => 'a set => 'b set
+translations "lift f A" == "Union(f `` A)"
+
+consts delta :: "('a,'s)na => 'a list => 's => 's set"
+primrec delta list
+"delta A []    p = {p}"
+"delta A (a#w) p = lift (delta A w) (next A a p)"
+
+constdefs
+ accepts ::   ('a,'s)na => 'a list => bool
+"accepts A w == ? q : delta A w (start A). fin A q"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/NAe.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/NAe.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,52 @@
+(*  Title:      HOL/Lex/NAe.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+goal thy
+ "steps A w O (eps A)^* = steps A w";
+by (exhaust_tac "w" 1);
+by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
+qed_spec_mp "steps_epsclosure";
+Addsimps [steps_epsclosure];
+
+goal thy
+ "!! A. [| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
+by(rtac (steps_epsclosure RS equalityE) 1);
+by(Blast_tac 1);
+qed "in_steps_epsclosure";
+
+goal thy "(eps A)^* O steps A w = steps A w";
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [O_assoc RS sym]) 1);
+qed "epsclosure_steps";
+
+goal thy
+ "!!A. [| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
+by(rtac (epsclosure_steps RS equalityE) 1);
+by(Blast_tac 1);
+qed "in_epsclosure_steps";
+
+goal thy
+ "steps A (v@w) = steps A w  O  steps A v";
+by (induct_tac "v" 1);
+by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
+qed "steps_append";
+Addsimps [steps_append];
+
+goal thy "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
+by(rtac (steps_append RS equalityE) 1);
+by(Blast_tac 1);
+qed "in_steps_append";
+AddIffs [in_steps_append];
+
+(** Equivalence of steps and delta **)
+(* Use "(? x : f `` A. P x) = (? a:A. P(f x))" ?? *)
+goal thy "!p. (p,q) : steps A w = (q : delta A w p)";
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
+by(Blast_tac 1);
+qed_spec_mp "steps_equiv_delta";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/NAe.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/NAe.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,34 @@
+(*  Title:      HOL/Lex/NAe.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Nondeterministic automata with epsilon transitions
+*)
+
+NAe = List + Option + NA +
+
+types ('a,'s)nae = ('a option,'s)na
+
+constdefs
+ step :: "('a,'s)nae => 'a option => ('s * 's)set"
+"step A a == {(p,q) . q : next A a p}"
+
+syntax eps :: "('a,'s)nae => ('s * 's)set"
+translations "eps A" == "step A None"
+
+consts steps :: "('a,'s)nae => 'a list =>   ('s * 's)set"
+primrec steps list
+"steps A [] = (eps A)^*"
+"steps A (a#w) = steps A w  O  step A (Some a)  O  (eps A)^*"
+
+consts delta :: "('a,'s)nae => 'a list => 's => 's set"
+primrec delta list
+"delta A [] s = (eps A)^* ^^ {s}"
+"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
+
+constdefs
+ accepts :: ('a,'s)nae => 'a list => bool
+"accepts A w == ? q. (start A,q) : steps A w & fin A q"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/NAe_of_RegExp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/NAe_of_RegExp.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,663 @@
+(*  Title:      HOL/Lex/NAe_of_RegExp.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+(******************************************************)
+(*                       atom                         *)
+(******************************************************)
+
+goalw thy [atom_def] "(fin (atom a) q) = (q = [False])";
+by(Simp_tac 1);
+qed "fin_atom";
+
+goalw thy [atom_def] "start (atom a) = [True]";
+by(Simp_tac 1);
+qed "start_atom";
+
+(* Use {x. False} = {}? *)
+
+goalw thy [atom_def,step_def]
+ "eps(atom a) = {}";
+by(Simp_tac 1);
+by (Blast_tac 1);
+qed "eps_atom";
+Addsimps [eps_atom];
+
+goalw thy [atom_def,step_def]
+ "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
+by(Simp_tac 1);
+qed "in_step_atom_Some";
+Addsimps [in_step_atom_Some];
+
+goal thy
+ "([False],[False]) : steps (atom a) w = (w = [])";
+by (induct_tac "w" 1);
+ by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
+qed "False_False_in_steps_atom";
+
+goal thy
+ "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
+by (induct_tac "w" 1);
+ by(asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
+by(asm_full_simp_tac (simpset()
+     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
+qed "start_fin_in_steps_atom";
+
+(******************************************************)
+(*                      union                         *)
+(******************************************************)
+
+(***** True/False ueber fin anheben *****)
+
+goalw thy [union_def] 
+ "!L R. fin (union L R) (True#p) = fin L p";
+by (Simp_tac 1);
+qed_spec_mp "fin_union_True";
+
+goalw thy [union_def] 
+ "!L R. fin (union L R) (False#p) = fin R p";
+by (Simp_tac 1);
+qed_spec_mp "fin_union_False";
+
+AddIffs [fin_union_True,fin_union_False];
+
+(***** True/False ueber step anheben *****)
+
+goalw thy [union_def,step_def]
+"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
+by (Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "True_in_step_union";
+
+goalw thy [union_def,step_def]
+"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
+by (Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "False_in_step_union";
+
+AddIffs [True_in_step_union,False_in_step_union];
+
+(***** True/False ueber epsclosure anheben *****)
+
+goal thy
+ "!!d. (tp,tq) : (eps(union L R))^* ==> \
+\ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
+be rtrancl_induct 1;
+ by(Blast_tac 1);
+by(Clarify_tac 1);
+by(Asm_full_simp_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma1a = result();
+
+goal thy
+ "!!d. (tp,tq) : (eps(union L R))^* ==> \
+\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
+be rtrancl_induct 1;
+ by(Blast_tac 1);
+by(Clarify_tac 1);
+by(Asm_full_simp_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma1b = result();
+
+goal thy
+ "!!p. (p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
+be rtrancl_induct 1;
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma2a = result();
+
+goal thy
+ "!!p. (p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
+be rtrancl_induct 1;
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma2b = result();
+
+goal thy
+ "(True#p,q) : (eps(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
+by(blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
+qed "True_epsclosure_union";
+
+goal thy
+ "(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
+by(blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
+qed "False_epsclosure_union";
+
+AddIffs [True_epsclosure_union,False_epsclosure_union];
+
+(***** True/False ueber steps anheben *****)
+
+goal thy
+ "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
+by (induct_tac "w" 1);
+by (ALLGOALS Asm_simp_tac);
+(* Blast_tac produces PROOF FAILED for depth 8 *)
+by(Fast_tac 1);
+qed_spec_mp "lift_True_over_steps_union";
+
+goal thy 
+ "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
+by (induct_tac "w" 1);
+by (ALLGOALS Asm_simp_tac);
+(* Blast_tac produces PROOF FAILED for depth 8 *)
+by(Fast_tac 1);
+qed_spec_mp "lift_False_over_steps_union";
+
+AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
+
+
+(***** Epsilonhuelle des Startzustands  *****)
+
+goal thy
+ "R^* = id Un (R^* O R)";
+by(rtac set_ext 1);
+by(split_all_tac 1);
+by(rtac iffI 1);
+ be rtrancl_induct 1;
+  by(Blast_tac 1);
+ by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+qed "unfold_rtrancl2";
+
+goal thy
+ "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))";
+by(rtac (unfold_rtrancl2 RS equalityE) 1);
+by(Blast_tac 1);
+qed "in_unfold_rtrancl2";
+
+val epsclosure_start_step_union =
+  read_instantiate [("p","start(union L R)")] in_unfold_rtrancl2;
+AddIffs [epsclosure_start_step_union];
+
+goalw thy [union_def,step_def]
+ "!L R. (start(union L R),q) : eps(union L R) = \
+\       (q = True#start L | q = False#start R)";
+by(Simp_tac 1);
+qed_spec_mp "start_eps_union";
+AddIffs [start_eps_union];
+
+goalw thy [union_def,step_def]
+ "!L R. (start(union L R),q) ~: step (union L R) (Some a)";
+by(Simp_tac 1);
+qed_spec_mp "not_start_step_union_Some";
+AddIffs [not_start_step_union_Some];
+
+goal thy
+ "(start(union L R), q) : steps (union L R) w = \
+\ ( (w = [] & q = start(union L R)) | \
+\   (? p.  q = True  # p & (start L,p) : steps L w | \
+\          q = False # p & (start R,p) : steps R w) )";
+by (exhaust_tac "w" 1);
+ by (Asm_simp_tac 1);
+ (* Blast_tac produces PROOF FAILED! *)
+ by(Fast_tac 1);
+by (Asm_simp_tac 1);
+(* The goal is now completely dual to the first one.
+   Fast/Best_tac don't return. Blast_tac produces PROOF FAILED!
+   The lemmas used in the explicit proof are part of the claset already!
+*)
+br iffI 1;
+ by(Blast_tac 1);
+by(Clarify_tac 1);
+be disjE 1;
+ by(Blast_tac 1);
+by(Clarify_tac 1);
+br compI 1;
+br compI 1;
+br (epsclosure_start_step_union RS iffD2) 1;
+br disjI2 1;
+br exI 1;
+br conjI 1;
+br (start_eps_union RS iffD2) 1;
+br disjI2 1;
+br refl 1;
+by(Clarify_tac 1);
+br exI 1;
+br conjI 1;
+br refl 1;
+ba 1;
+by(Clarify_tac 1);
+br exI 1;
+br conjI 1;
+br refl 1;
+ba 1;
+by(Clarify_tac 1);
+br exI 1;
+br conjI 1;
+br refl 1;
+ba 1;
+qed "steps_union";
+
+goalw thy [union_def]
+ "!L R. ~ fin (union L R) (start(union L R))";
+by(Simp_tac 1);
+qed_spec_mp "start_union_not_final";
+AddIffs [start_union_not_final];
+
+goalw thy [accepts_def]
+ "accepts (union L R) w = (accepts L w | accepts R w)";
+by (simp_tac (simpset() addsimps [steps_union]) 1);
+auto();
+qed "final_union";
+
+
+(******************************************************)
+(*                      conc                        *)
+(******************************************************)
+
+(** True/False in fin **)
+
+goalw thy [conc_def]
+ "!L R. fin (conc L R) (True#p) = False";
+by (Simp_tac 1);
+qed_spec_mp "fin_conc_True";
+
+goalw thy [conc_def] 
+ "!L R. fin (conc L R) (False#p) = fin R p";
+by (Simp_tac 1);
+qed "fin_conc_False";
+
+AddIffs [fin_conc_True,fin_conc_False];
+
+(** True/False in step **)
+
+goalw thy [conc_def,step_def]
+ "!L R. (True#p,q) : step (conc L R) a = \
+\       ((? r. q=True#r & (p,r): step L a) | \
+\        (fin L p & a=None & q=False#start R))";
+by (Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "True_step_conc";
+
+goalw thy [conc_def,step_def]
+ "!L R. (False#p,q) : step (conc L R) a = \
+\       (? r. q = False#r & (p,r) : step R a)";
+by (Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "False_step_conc";
+
+AddIffs [True_step_conc, False_step_conc];
+
+(** False in epsclosure **)
+
+goal thy
+ "!!d. (tp,tq) : (eps(conc L R))^* ==> \
+\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
+by(etac rtrancl_induct 1);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+qed "lemma1b";
+
+goal thy
+ "!!p. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
+by(etac rtrancl_induct 1);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma2b = result();
+
+goal thy
+ "((False # p, q) : (eps (conc L R))^*) = \
+\ (? r. q = False # r & (p, r) : (eps R)^*)";
+by (rtac iffI 1);
+ by(blast_tac (claset() addDs [lemma1b]) 1);
+by(blast_tac (claset() addDs [lemma2b]) 1);
+qed "False_epsclosure_conc";
+AddIffs [False_epsclosure_conc];
+
+(** False in steps **)
+
+goal thy
+ "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+(* Blast_tac produces PROOF FAILED for depth 8 *)
+by(Fast_tac 1);
+qed_spec_mp "False_steps_conc";
+AddIffs [False_steps_conc];
+
+(** True in epsclosure **)
+
+goal thy
+ "!!L R. (p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
+be rtrancl_induct 1;
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+qed "True_True_eps_concI";
+
+goal thy
+ "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
+by(induct_tac "w" 1);
+ by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
+by (Simp_tac 1);
+by(blast_tac (claset() addIs [True_True_eps_concI]) 1);
+qed_spec_mp "True_True_steps_concI";
+
+goal thy
+ "!!d. (tp,tq) : (eps(conc L R))^* ==> \
+\ !p. tp = True#p --> \
+\ (? q. tq = True#q & (p,q) : (eps L)^*) | \
+\ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
+by(etac rtrancl_induct 1);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma1a = result();
+
+goal thy
+ "!!p. (p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
+by(etac rtrancl_induct 1);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma2a = result();
+
+goalw thy [conc_def,step_def]
+ "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
+by(split_all_tac 1);
+by (Asm_full_simp_tac 1);
+val lemma = result();
+
+goal thy
+ "!!L R. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
+by(etac rtrancl_induct 1);
+ by(Blast_tac 1);
+by (dtac lemma 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma2b = result();
+
+goalw thy [conc_def,step_def]
+ "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
+by(split_all_tac 1);
+by(Asm_full_simp_tac 1);
+qed "True_False_eps_concI";
+
+goal thy
+ "((True#p,q) : (eps(conc L R))^*) = \
+\ ((? r. (p,r) : (eps L)^* & q = True#r) | \
+\  (? r. (p,r) : (eps L)^* & fin L r & \
+\        (? s. (start R, s) : (eps R)^* & q = False#s)))";
+by(rtac iffI 1);
+ by(blast_tac (claset() addDs [lemma1a]) 1);
+be disjE 1;
+ by(blast_tac (claset() addIs [lemma2a]) 1);
+by(Clarify_tac 1);
+br (rtrancl_trans) 1;
+be lemma2a 1;
+br (rtrancl_into_rtrancl2) 1;
+be True_False_eps_concI 1;
+be lemma2b 1;
+qed "True_epsclosure_conc";
+AddIffs [True_epsclosure_conc];
+
+(** True in steps **)
+
+goal thy
+ "!p. (True#p,q) : steps (conc L R) w --> \
+\     ((? r. (p,r) : steps L w & q = True#r)  | \
+\      (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
+\              (? s. (start R,s) : steps R v & q = False#s))))";
+by(induct_tac "w" 1);
+ by(Simp_tac 1);
+by(Simp_tac 1);
+by(clarify_tac (claset() delrules [disjCI]) 1);
+ be disjE 1;
+ by(clarify_tac (claset() delrules [disjCI]) 1);
+ be disjE 1;
+  by(clarify_tac (claset() delrules [disjCI]) 1);
+  by(etac allE 1 THEN mp_tac 1);
+  be disjE 1;
+   by (Blast_tac 1);
+  br disjI2 1;
+  by (Clarify_tac 1);
+  by(Simp_tac 1);
+  by(res_inst_tac[("x","a#u")] exI 1);
+  by(Simp_tac 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
+br disjI2 1;
+by (Clarify_tac 1);
+by(Simp_tac 1);
+by(res_inst_tac[("x","[]")] exI 1);
+by(Simp_tac 1);
+by (Blast_tac 1);
+qed_spec_mp "True_steps_concD";
+
+goal thy
+ "(True#p,q) : steps (conc L R) w = \
+\ ((? r. (p,r) : steps L w & q = True#r)  | \
+\  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
+\          (? s. (start R,s) : steps R v & q = False#s))))";
+by(blast_tac (claset() addDs [True_steps_concD]
+     addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
+qed "True_steps_conc";
+
+(** starting from the start **)
+
+goalw thy [conc_def]
+  "!L R. start(conc L R) = True#start L";
+by(Simp_tac 1);
+qed_spec_mp "start_conc";
+
+goalw thy [conc_def]
+ "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
+by (simp_tac (simpset() addsplits [split_list_case]) 1);
+qed_spec_mp "final_conc";
+
+
+(******************************************************)
+(*                       star                         *)
+(******************************************************)
+
+goalw thy [star_def,step_def]
+ "!A. (True#p,q) : eps(star A) = \
+\     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "True_in_eps_star";
+AddIffs [True_in_eps_star];
+
+goalw thy [star_def,step_def]
+  "!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
+by(Simp_tac 1);
+qed_spec_mp "True_True_step_starI";
+
+goal thy
+  "!!A. (p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
+be rtrancl_induct 1;
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
+qed_spec_mp "True_True_eps_starI";
+
+goalw thy [star_def,step_def]
+ "!A. fin A p --> (True#p,True#start A) : eps(star A)";
+by(Simp_tac 1);
+qed_spec_mp "True_start_eps_starI";
+
+goal thy
+ "!!dummy. (tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> \
+\ (? r. ((p,r) : (eps A)^* | \
+\        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
+\       s = True#r))";
+be rtrancl_induct 1;
+ by(Simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+val lemma = result();
+
+goal thy
+ "((True#p,s) : (eps(star A))^*) = \
+\ (? r. ((p,r) : (eps A)^* | \
+\        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
+\       s = True#r)";
+br iffI 1;
+ bd lemma 1;
+ by(Blast_tac 1);
+(* Why can't blast_tac do the rest? *)
+by (Clarify_tac 1);
+be disjE 1;
+be True_True_eps_starI 1;
+by (Clarify_tac 1);
+br rtrancl_trans 1;
+be True_True_eps_starI 1;
+br rtrancl_trans 1;
+br r_into_rtrancl 1;
+be True_start_eps_starI 1;
+be True_True_eps_starI 1;
+qed "True_eps_star";
+AddIffs [True_eps_star];
+
+(** True in step Some **)
+
+goalw thy [star_def,step_def]
+ "!A. (True#p,r): step (star A) (Some a) = \
+\     (? q. (p,q): step A (Some a) & r=True#q)";
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "True_step_star";
+AddIffs [True_step_star];
+
+
+(** True in steps **)
+
+(* reverse list induction! Complicates matters for conc? *)
+goal thy
+ "!rr. (True#start A,rr) : steps (star A) w --> \
+\ (? us v. w = concat us @ v & \
+\             (!u:set us. accepts A u) & \
+\             (? r. (start A,r) : steps A v & rr = True#r))";
+by(res_inst_tac [("xs","w")] snoc_induct 1);
+ by (Asm_full_simp_tac 1);
+ by (Clarify_tac 1);
+ by(res_inst_tac [("x","[]")] exI 1);
+ be disjE 1;
+  by (Asm_simp_tac 1);
+ by (Clarify_tac 1);
+ by (Asm_simp_tac 1);
+by(simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+by (Clarify_tac 1);
+by(etac allE 1 THEN mp_tac 1);
+by (Clarify_tac 1);
+be disjE 1;
+ by(res_inst_tac [("x","us")] exI 1);
+ by(res_inst_tac [("x","v@[x]")] exI 1);
+ by(asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+ by(Blast_tac 1);
+by (Clarify_tac 1);
+by(res_inst_tac [("x","us@[v@[x]]")] exI 1);
+by(res_inst_tac [("x","[]")] exI 1);
+by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by(Blast_tac 1);
+qed_spec_mp "True_start_steps_starD";
+
+goal thy "!p. (p,q) : steps A w --> (True#p,True#q) : steps (star A) w";
+by(induct_tac "w" 1);
+ by(Simp_tac 1);
+by(Simp_tac 1);
+by(blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
+qed_spec_mp "True_True_steps_starI";
+
+goalw thy [accepts_def]
+ "(!u : set us. accepts A u) --> \
+\ (True#start A,True#start A) : steps (star A) (concat us)";
+by(induct_tac "us" 1);
+ by(Simp_tac 1);
+by(Simp_tac 1);
+by(blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
+qed_spec_mp "steps_star_cycle";
+
+(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
+goal thy
+ "(True#start A,rr) : steps (star A) w = \
+\ (? us v. w = concat us @ v & \
+\             (!u:set us. accepts A u) & \
+\             (? r. (start A,r) : steps A v & rr = True#r))";
+br iffI 1;
+ be True_start_steps_starD 1;
+by (Clarify_tac 1);
+by(Asm_simp_tac 1);
+by(blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
+qed "True_start_steps_star";
+
+(** the start state **)
+
+goalw thy [star_def,step_def]
+  "!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
+by(Simp_tac 1);
+qed_spec_mp "start_step_star";
+AddIffs [start_step_star];
+
+val epsclosure_start_step_star =
+  read_instantiate [("p","start(star A)")] in_unfold_rtrancl2;
+
+goal thy
+ "(start(star A),r) : steps (star A) w = \
+\ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
+br iffI 1;
+ by(exhaust_tac "w" 1);
+  by(asm_full_simp_tac (simpset() addsimps
+    [epsclosure_start_step_star]) 1);
+ by(Asm_full_simp_tac 1);
+ by (Clarify_tac 1);
+ by(asm_full_simp_tac (simpset() addsimps
+    [epsclosure_start_step_star]) 1);
+ by(Blast_tac 1);
+be disjE 1;
+ by(Asm_simp_tac 1);
+by(blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
+qed "start_steps_star";
+
+goalw thy [star_def] "!A. fin (star A) (True#p) = fin A p";
+by(Simp_tac 1);
+qed_spec_mp "fin_star_True";
+AddIffs [fin_star_True];
+
+goalw thy [star_def] "!A. fin (star A) (start(star A))";
+by(Simp_tac 1);
+qed_spec_mp "fin_star_start";
+AddIffs [fin_star_start];
+
+(* too complex! Simpler if loop back to start(star A)? *)
+goalw thy [accepts_def]
+ "accepts (star A) w = \
+\ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
+by(simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
+br iffI 1;
+ by (Clarify_tac 1);
+ be disjE 1;
+  by (Clarify_tac 1);
+  by(Simp_tac 1);
+  by(res_inst_tac [("x","[]")] exI 1);
+  by(Simp_tac 1);
+ by (Clarify_tac 1);
+ by(res_inst_tac [("x","us@[v]")] exI 1);
+ by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+ by(Blast_tac 1);
+by (Clarify_tac 1);
+by(res_inst_tac [("xs","us")] snoc_exhaust 1);
+ by(Asm_simp_tac 1);
+ by(Blast_tac 1);
+by (Clarify_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by(Blast_tac 1);
+qed "accepts_star";
+
+
+(***** Correctness of r2n *****)
+
+goal thy
+ "!w. w:(lang r) = accepts (r2n r) w";
+by(induct_tac "r" 1);
+    by(simp_tac (simpset() addsimps [accepts_def]) 1);
+   by(simp_tac(simpset() addsimps
+       [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
+  (* 3. Fall: Union *)
+  by (asm_simp_tac (simpset() addsimps [final_union]) 1);
+  (* 4. Fall: Concat *)
+ by (asm_simp_tac (simpset() addsimps
+     [accepts_def,True_steps_conc,final_conc,start_conc,RegSet.conc_def]) 1);
+ by(Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [in_star,accepts_star]) 1);
+qed "Rexp_Automata";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/NAe_of_RegExp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/NAe_of_RegExp.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,60 @@
+(*  Title:      HOL/Lex/NAe_of_RegExp.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Conversion of regular expressions
+into nondeterministic automata with epsilon transitions
+*)
+
+NAe_of_RegExp = NAe + RegExp +
+
+types 'a r2nae = ('a,bool list)nae
+
+syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
+translations "x ## S" == "op # x `` S"
+
+constdefs
+ atom  :: 'a => 'a r2nae
+"atom a == ([True],
+            %b s. if s=[True] & b=Some a then {[False]} else {},
+            %s. s=[False])"
+
+ union :: 'a r2nae => 'a r2nae => 'a r2nae
+"union == %(ql,dl,fl)(qr,dr,fr).
+   ([],
+    %a s. case s of
+            [] => if a=None then {True#ql,False#qr} else {}
+          | left#s => if left then True ## dl a s
+                              else False ## dr a s,
+    %s. case s of [] => False | left#s => if left then fl s else fr s)"
+
+ conc :: 'a r2nae => 'a r2nae => 'a r2nae
+"conc == %(ql,dl,fl)(qr,dr,fr).
+   (True#ql,
+    %a s. case s of
+            [] => {}
+          | left#s => if left then (True ## dl a s) Un
+                                   (if fl s & a=None then {False#qr} else {})
+                              else False ## dr a s,
+    %s. case s of [] => False | left#s => ~left & fr s)"
+
+ star :: 'a r2nae => 'a r2nae
+"star == %(q,d,f).
+   ([],
+    %a s. case s of
+            [] => if a=None then {True#q} else {}
+          | left#s => if left then (True ## d a s) Un
+                                   (if f s & a=None then {True#q} else {})
+                              else {},
+    %s. case s of [] => True | left#s => left & f s)"
+
+consts r2n :: 'a rexp => 'a r2nae
+primrec r2n rexp
+"r2n Empty = ([], %a s. {}, %s. False)"
+"r2n(Atom a) = atom a"
+"r2n(Union el er) = union(r2n el)(r2n er)"
+"r2n(Conc el er) = conc(r2n el)(r2n er)"
+"r2n(Star e) = star(r2n e)"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/ROOT.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Lex/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1995 TUM
+    Copyright   1998 TUM
 *)
 
 HOL_build_completed;    (*Make examples fail if HOL did*)
@@ -9,4 +9,10 @@
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
 use_thy"AutoMaxChop";
-use_thy"Regset_of_auto";
+(* Do no swap the next 2.
+   There is some interference, probably via claset() or simpset().
+   Or via ML-bound names of axioms that are overwritten?
+*)
+use_thy"RegSet_of_nat_DA";
+use_thy"NAe_of_RegExp";
+use_thy"Automata";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/RegExp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegExp.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/Lex/RegExp.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Regular expressions
+*)
+
+RegExp = RegSet +
+
+datatype 'a rexp = Empty
+                 | Atom 'a
+                 | Union ('a rexp) ('a rexp)
+                 | Conc ('a rexp) ('a rexp)
+                 | Star ('a rexp)
+
+consts lang :: 'a rexp => 'a list set
+primrec lang rexp
+lang_Emp  "lang Empty = {}"
+lang_Atom "lang (Atom a) = {[a]}"
+lang_Un   "lang (Union el er) = (lang el) Un (lang er)"
+lang_Conc "lang (Conc el er) = RegSet.conc (lang el) (lang er)"
+lang_Star "lang (Star e) = RegSet.star(lang e)"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/RegSet.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegSet.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,27 @@
+(*  Title:      HOL/Lex/RegSet.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+AddIffs [star.NilI];
+Addsimps [star.ConsI];
+AddIs [star.ConsI];
+
+goal thy "(!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 thy
+ "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
+br iffI 1;
+ be 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 dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/RegSet.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegSet.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Lex/RegSet.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Regular sets
+*)
+
+RegSet = List +
+
+constdefs
+ 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
+inductive "star A"
+intrs
+  NilI   "[] : star A"
+  ConsI  "[| a:A; as : star A |] ==> a@as : star A"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/RegSet_of_nat_DA.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,215 @@
+(*  Title:      HOL/Lex/RegSet_of_nat_DA.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
+AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
+Addsimps [image_eqI];
+
+(* Lists *)
+
+goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "butlast_empty";
+AddIffs [butlast_empty];
+
+goal thy "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 (rotate_tac ~1 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 thy "!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 (rtac conjI 1);
+ by (Blast_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 thy "!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 thy "!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 thy "!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 thy "(!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 thy "!i. (trace d i xs = []) = (xs = [])";
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "trace_is_Nil";
+Addsimps [trace_is_Nil];
+
+goal thy "(trace d i xs = n#ns) = \
+\         (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)";
+by (exhaust_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 thy "!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 thy
+ "(!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 Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
+by (etac nat_neqE 1);
+by (ALLGOALS trans_tac);
+val lemma = result();
+
+
+goal thy
+ "!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 [split_list_case]) 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
+      "(!n:set(butlast(trace d k xsb)). n < Suc k) & deltas d xsb k = k" 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 "k : 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 (Asm_simp_tac 2);
+by (EVERY[dtac bspec 1, atac 2]);
+by (Asm_simp_tac 1);
+qed_spec_mp "regset_spec";
+
+goalw thy [bounded_def]
+ "!!d. 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 thy "!!d. [| 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 thy [bounded_def]
+ "!!d. 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 thy [regset_of_DA_def]
+ "!!d. [| 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,accepts_def,delta_def]) 1);
+qed "regset_DA_equiv";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/RegSet_of_nat_DA.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegSet_of_nat_DA.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,48 @@
+(*  Title:      HOL/Lex/RegSet_of_nat_DA.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Conversion of deterministic automata into regular sets.
+
+To generate a regual expression, the alphabet must be finite.
+regexp needs to be supplied with an 'a list for a unique order
+
+add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r)
+atoms d i j as = foldl (add_Atom d i j) Empty as
+
+regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as)
+                        else atoms d i j as
+*)
+
+RegSet_of_nat_DA = RegSet + DA +
+
+types 'a nat_next = "'a => nat => nat"
+
+syntax deltas :: 'a nat_next => 'a list => nat => nat
+translations "deltas" == "foldl2"
+
+consts trace :: 'a nat_next => nat => 'a list => nat list
+primrec trace list
+"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
+primrec regset nat
+"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
+                          else {[a] | a. d a i = j})"
+"regset d i j (Suc k) = regset d i j k Un
+                        conc (regset d i k k)
+                             (conc (star(regset d k k k))
+                                   (regset d k j k))"
+
+constdefs
+ 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)"
+
+end
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/Regset_of_auto.ML
--- a/src/HOL/Lex/Regset_of_auto.ML	Mon Apr 27 16:45:27 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,217 +0,0 @@
-Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
-AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
-Addsimps [image_eqI];
-
-AddIffs [star.NilI];
-Addsimps [star.ConsI];
-AddIs [star.ConsI];
-
-(* Lists *)
-
-(*
-(* could go into List. Needs WF_Rel as ancestor. *)
-(* Induction over the length of a list: *)
-val prems = goal thy
- "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
-by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
-     wf_induct 1);
-by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
-by (eresolve_tac prems 1);
-qed "list_length_induct";
-*)
-
-goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
-by (exhaust_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "butlast_empty";
-AddIffs [butlast_empty];
-
-goal thy "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 (rotate_tac ~1 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 *)
-
-goal thy "(!xs: set xss. xs:A) --> concat xss : star A";
-by (induct_tac "xss" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed_spec_mp "concat_in_star";
-
-(* The main lemma:
-   how to decompose a trace into a prefix, a list of loops and a suffix.
-*)
-goal thy "!i. k : set(trace A i xs) --> (? pref mids suf. \
-\ xs = pref @ concat mids @ suf & \
-\ deltas A pref i = k & (!n:set(butlast(trace A i pref)). n ~= k) & \
-\ (!mid:set mids. (deltas A mid k = k) & \
-\                 (!n:set(butlast(trace A k mid)). n ~= k)) & \
-\ (!n:set(butlast(trace A 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 "A 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 A (A 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 (rtac conjI 1);
- by (Blast_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 thy "!i. length(trace A i xs) = length xs";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "length_trace";
-Addsimps [length_trace];
-
-goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "deltas_append";
-Addsimps [deltas_append];
-
-goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "trace_append";
-Addsimps [trace_append];
-
-goal thy "(!xs: set xss. deltas A xs i = i) --> \
-\         trace A i (concat xss) = concat (map (trace A i) xss)";
-by (induct_tac "xss" 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "trace_concat";
-Addsimps [trace_concat];
-
-goal thy "!i. (trace A i xs = []) = (xs = [])";
-by (exhaust_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "trace_is_Nil";
-Addsimps [trace_is_Nil];
-
-goal thy "(trace A i xs = n#ns) = \
-\         (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)";
-by (exhaust_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 thy "!i. set(trace A i xs) = \
-\ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A 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 thy
- "(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k";
-by (induct_tac "mids" 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "deltas_concat";
-Addsimps [deltas_concat];
-
-goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
-by (etac nat_neqE 1);
-by (ALLGOALS trans_tac);
-val lemma = result();
-
-
-goal thy
- "!i j xs. xs : regset_of A i j k = \
-\          ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
-by (induct_tac "k" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [split_list_case]) 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
-      "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 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 "k : set(butlast(trace A 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 (Asm_simp_tac 2);
-by (EVERY[dtac bspec 1, atac 2]);
-by (Asm_simp_tac 1);
-qed_spec_mp "regset_of_spec";
-
-goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \
-\         !i. i < k --> (!n:set(trace A i xs). n < k)";
-by (induct_tac "xs" 1);
- by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
-qed_spec_mp "trace_below";
-
-goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \
-\         regset_of A i j k = {xs. deltas A xs i = j}";
-by (rtac set_ext 1);
-by (simp_tac (simpset() addsimps [regset_of_spec]) 1);
-by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
-qed "regset_of_below";
diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/Regset_of_auto.thy
--- a/src/HOL/Lex/Regset_of_auto.thy	Mon Apr 27 16:45:27 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*
-Conversion of automata into regular sets.
-use_thy"Auto";
-*)
-
-Regset_of_auto = List +
-
-(* autos *)
-
-types 'a auto = "'a => nat => nat"
-
-consts deltas :: 'a auto => 'a list => nat => nat
-primrec deltas list
-"deltas A [] i = i"
-"deltas A (x#xs) i = deltas A xs (A x i)"
-
-consts trace :: 'a auto => nat => 'a list => nat list
-primrec trace list
-"trace A i [] = []"
-"trace A i (x#xs) = A x i # trace A (A x i) xs"
-
-(* regular sets *)
-
-constdefs 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
-inductive "star A"
-intrs
-  NilI   "[] : star A"
-  ConsI  "[| a:A; as : star A |] ==> a@as : star A"
-
-(* conversion a la Warshall *)
-
-consts regset_of :: 'a auto => nat => nat => nat => 'a list set
-primrec regset_of nat
-"regset_of A i j 0 = (if i=j then insert [] {[a] | a. A a i = j}
-                             else {[a] | a. A a i = j})"
-"regset_of A i j (Suc k) = regset_of A i j k Un
-                           conc (regset_of A i k k)
-                          (conc (star(regset_of A k k k))
-                                (regset_of A k j k))"
-
-end