# HG changeset patch
# User nipkow
# Date 903344457 -7200
# Node ID 028e00595280765f9e48277187b814845e7bbc8d
# Parent  504b129e05022153a6cb8b594c727a08b7971f0e
Direct translation RegExp -> NA!

diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/Automata.ML
--- a/src/HOL/Lex/Automata.ML	Mon Aug 17 11:00:27 1998 +0200
+++ b/src/HOL/Lex/Automata.ML	Mon Aug 17 11:00:57 1998 +0200
@@ -4,7 +4,7 @@
     Copyright   1998 TUM
 *)
 
-(*** Equivalence of NA and DA --- redundant ***)
+(*** Equivalence of NA and DA ***)
 
 Goalw [na2da_def]
  "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/NA.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/NA.ML	Mon Aug 17 11:00:57 1998 +0200
@@ -0,0 +1,29 @@
+(*  Title:      HOL/Lex/NA.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+Goal
+ "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 "(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];
+
+Goal
+ "!p. delta A w p = {q. (p,q) : steps A w}";
+by(induct_tac "w" 1);
+by(auto_tac (claset(), simpset() addsimps [step_def]));
+qed_spec_mp "delta_conv_steps";
+
+Goalw [accepts_def]
+ "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
+by(simp_tac (simpset() addsimps [delta_conv_steps]) 1);
+qed "accepts_conv_steps";
diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/NA.thy
--- a/src/HOL/Lex/NA.thy	Mon Aug 17 11:00:27 1998 +0200
+++ b/src/HOL/Lex/NA.thy	Mon Aug 17 11:00:57 1998 +0200
@@ -19,4 +19,13 @@
  accepts ::   ('a,'s)na => 'a list => bool
 "accepts A w == ? q : delta A w (start A). fin A q"
 
+constdefs
+ step :: "('a,'s)na => 'a => ('s * 's)set"
+"step A a == {(p,q) . q : next A a p}"
+
+consts steps :: "('a,'s)na => 'a list => ('s * 's)set"
+primrec
+"steps A [] = id"
+"steps A (a#w) = steps A w  O  step A a"
+
 end
diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Mon Aug 17 11:00:27 1998 +0200
+++ b/src/HOL/Lex/ROOT.ML	Mon Aug 17 11:00:57 1998 +0200
@@ -14,5 +14,6 @@
    Or via ML-bound names of axioms that are overwritten?
 *)
 use_thy"RegSet_of_nat_DA";
+use_thy"RegExp2NA";
 use_thy"RegExp2NAe";
 use_thy"Scanner";
diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/RegExp2NA.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegExp2NA.ML	Mon Aug 17 11:00:57 1998 +0200
@@ -0,0 +1,463 @@
+(*  Title:      HOL/Lex/RegExp2NA.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+(******************************************************)
+(*                       atom                         *)
+(******************************************************)
+
+Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
+by(Simp_tac 1);
+qed "fin_atom";
+
+Goalw [atom_def] "start (atom a) = [True]";
+by(Simp_tac 1);
+qed "start_atom";
+
+Goalw [atom_def,step_def]
+ "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
+by(Simp_tac 1);
+qed "in_step_atom_Some";
+Addsimps [in_step_atom_Some];
+
+Goal
+ "([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
+ "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
+by (induct_tac "w" 1);
+ by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
+by(asm_full_simp_tac (simpset()
+     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
+qed "start_fin_in_steps_atom";
+
+Goal
+ "accepts (atom a) w = (w = [a])";
+by(simp_tac(simpset() addsimps
+       [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
+qed "accepts_atom";
+
+
+(******************************************************)
+(*                      union                         *)
+(******************************************************)
+
+(***** True/False ueber fin anheben *****)
+
+Goalw [union_def] 
+ "!L R. fin (union L R) (True#p) = fin L p";
+by (Simp_tac 1);
+qed_spec_mp "fin_union_True";
+
+Goalw [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 [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 [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 steps anheben *****)
+
+Goal
+ "!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(ALLGOALS Fast_tac);
+qed_spec_mp "lift_True_over_steps_union";
+
+Goal 
+ "!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(ALLGOALS Fast_tac);
+qed_spec_mp "lift_False_over_steps_union";
+
+AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
+
+
+(** From the start  **)
+
+Goalw [union_def,step_def]
+ "!L R. (start(union L R),q) : step(union L R) a = \
+\       (? p. (q = True#p & (start L,p) : step L a) | \
+\             (q = False#p & (start R,p) : step R a))";
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "start_step_union";
+AddIffs [start_step_union];
+
+Goal
+ "(start(union L R), q) : steps (union L R) w = \
+\ ( (w = [] & q = start(union L R)) | \
+\   (w ~= [] & (? 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);
+ by(Blast_tac 1);
+by (Asm_simp_tac 1);
+by(Blast_tac 1);
+qed "steps_union";
+
+Goalw [union_def]
+ "!L R. fin (union L R) (start(union L R)) = \
+\       (fin L (start L) | fin R (start R))";
+by(Simp_tac 1);
+qed_spec_mp "fin_start_union";
+AddIffs [fin_start_union];
+
+Goal
+ "accepts (union L R) w = (accepts L w | accepts R w)";
+by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
+(* get rid of case_tac: *)
+by(case_tac "w = []" 1);
+by(Auto_tac);
+qed "accepts_union";
+AddIffs [accepts_union];
+
+(******************************************************)
+(*                      conc                        *)
+(******************************************************)
+
+(** True/False in fin **)
+
+Goalw [conc_def]
+ "!L R. fin (conc L R) (True#p) = (fin L p & fin R (start R))";
+by (Simp_tac 1);
+qed_spec_mp "fin_conc_True";
+
+Goalw [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 [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 & (? r. q=False#r & (start R,r) : step R a)))";
+by (Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "True_step_conc";
+
+Goalw [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 steps **)
+
+Goal
+ "!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(Fast_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 steps **)
+
+Goal
+ "!!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 1);
+by (Simp_tac 1);
+by(Blast_tac 1);
+qed_spec_mp "True_True_steps_concI";
+
+Goal
+ "!L R. (True#p,False#q) : step (conc L R) a = \
+\       (fin L p & (start R,q) : step R a)";
+by(Simp_tac 1);
+qed "True_False_step_conc";
+AddIffs [True_False_step_conc];
+
+Goal
+ "!p. (True#p,q) : steps (conc L R) w --> \
+\     ((? r. (p,r) : steps L w & q = True#r)  | \
+\  (? u a v. w = u@a#v & \
+\            (? r. (p,r) : steps L u & fin L r & \
+\            (? s. (start R,s) : step R a & \
+\            (? t. (s,t) : steps R v & q = False#t)))))";
+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);
+ 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);
+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
+ "(True#p,q) : steps (conc L R) w = \
+\ ((? r. (p,r) : steps L w & q = True#r)  | \
+\  (? u a v. w = u@a#v & \
+\            (? r. (p,r) : steps L u & fin L r & \
+\            (? s. (start R,s) : step R a & \
+\            (? t. (s,t) : steps R v & q = False#t)))))";
+by(fast_tac (claset() addDs [True_steps_concD]
+     addIs [True_True_steps_concI] addss simpset()) 1);
+qed "True_steps_conc";
+
+(** starting from the start **)
+
+Goalw [conc_def]
+  "!L R. start(conc L R) = True#start L";
+by(Simp_tac 1);
+qed_spec_mp "start_conc";
+
+Goalw [conc_def]
+ "!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | \
+\                          (? s. p = False#s & fin R s))";
+by (simp_tac (simpset() addsplits [list.split]) 1);
+by (Blast_tac 1);
+qed_spec_mp "final_conc";
+
+Goal
+ "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
+by (simp_tac (simpset() addsimps
+     [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
+br iffI 1;
+ by (Clarify_tac 1);
+ be disjE 1;
+  by (Clarify_tac 1);
+  be disjE 1;
+   by(res_inst_tac [("x","w")] exI 1);
+   by(Simp_tac 1);
+   by(Blast_tac 1);
+  by(Blast_tac 1);
+ be disjE 1;
+  by(Blast_tac 1);
+ by (Clarify_tac 1);
+ by(res_inst_tac [("x","u")] exI 1);
+ by(Simp_tac 1);
+ by(Blast_tac 1);
+by (Clarify_tac 1);
+by(exhaust_tac "v" 1);
+ by(Asm_full_simp_tac 1);
+ by(Blast_tac 1);
+by(Asm_full_simp_tac 1);
+by(Blast_tac 1);
+qed "accepts_conc";
+
+(******************************************************)
+(*                     epsilon                        *)
+(******************************************************)
+
+Goalw [epsilon_def,step_def] "step epsilon a = {}";
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed "step_epsilon";
+Addsimps [step_epsilon];
+
+Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
+by(induct_tac "w" 1);
+by(Auto_tac);
+qed "steps_epsilon";
+
+Goal "accepts epsilon w = (w = [])";
+by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
+by(simp_tac (simpset() addsimps [epsilon_def]) 1);
+qed "accepts_epsilon";
+AddIffs [accepts_epsilon];
+
+(******************************************************)
+(*                       plus                         *)
+(******************************************************)
+
+Goalw [plus_def] "!A. start (plus A) = start A";
+by(Simp_tac 1);
+qed_spec_mp "start_plus";
+Addsimps [start_plus];
+
+Goalw [plus_def] "!A. fin (plus A) = fin A";
+by(Simp_tac 1);
+qed_spec_mp "fin_plus";
+AddIffs [fin_plus];
+
+Goalw [plus_def,step_def]
+  "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
+by(Simp_tac 1);
+qed_spec_mp "step_plusI";
+
+Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
+by(induct_tac "w" 1);
+ by(Simp_tac 1);
+by(Simp_tac 1);
+by(blast_tac (claset() addIs [step_plusI]) 1);
+qed_spec_mp "steps_plusI";
+
+Goalw [plus_def,step_def]
+ "!A. (p,r): step (plus A) a = \
+\     ( (p,r): step A a | fin A p & (start A,r) : step A a )";
+by(Simp_tac 1);
+qed_spec_mp "step_plus_conv";
+AddIffs [step_plus_conv];
+
+Goal
+ "[| (start A,q) : steps A u; u ~= []; fin A p |] \
+\ ==> (p,q) : steps (plus A) u";
+by(exhaust_tac "u" 1);
+ by(Blast_tac 1);
+by(Asm_full_simp_tac 1);
+by(blast_tac (claset() addIs [steps_plusI]) 1);
+qed "fin_steps_plusI";
+
+(* reverse list induction! Complicates matters for conc? *)
+Goal
+ "!r. (start A,r) : steps (plus A) w --> \
+\     (? us v. w = concat us @ v & \
+\              (!u:set us. u ~= [] & accepts A u) & \
+\              (start A,r) : steps A v)";
+by(rev_induct_tac "w" 1);
+ by (Simp_tac 1);
+ by(res_inst_tac [("x","[]")] exI 1);
+ by (Simp_tac 1);
+by (Simp_tac 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(Asm_simp_tac 1);
+ by(Blast_tac 1);
+by(exhaust_tac "v" 1);
+ by(res_inst_tac [("x","us")] exI 1);
+ by(Asm_full_simp_tac 1);
+by(res_inst_tac [("x","us@[v]")] exI 1);
+by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by(Blast_tac 1);
+qed_spec_mp "start_steps_plusD";
+
+Goal
+ "!r. (start A,r) : steps (plus A) w --> \
+\     (? us v. w = concat us @ v & \
+\              (!u:set us. accepts A u) & \
+\              (start A,r) : steps A v)";
+by(rev_induct_tac "w" 1);
+ by (Simp_tac 1);
+ by(res_inst_tac [("x","[]")] exI 1);
+ by (Simp_tac 1);
+by (Simp_tac 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(Asm_simp_tac 1);
+ by(Blast_tac 1);
+by(res_inst_tac [("x","us@[v]")] exI 1);
+by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by(Blast_tac 1);
+qed_spec_mp "start_steps_plusD";
+
+Goal
+ "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
+by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by(rev_induct_tac "us" 1);
+ by(Simp_tac 1);
+by(rename_tac "u us" 1);
+by(Simp_tac 1);
+by (Clarify_tac 1);
+by(case_tac "us = []" 1);
+ by(Asm_full_simp_tac 1);
+ by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by (Clarify_tac 1);
+by(case_tac "u = []" 1);
+ by(Asm_full_simp_tac 1);
+ by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by(Asm_full_simp_tac 1);
+by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+qed_spec_mp "steps_star_cycle";
+
+Goal
+ "accepts (plus A) w = \
+\ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
+br iffI 1;
+ by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+ by (Clarify_tac 1);
+ bd start_steps_plusD 1;
+ by (Clarify_tac 1);
+ by(res_inst_tac [("x","us@[v]")] exI 1);
+ by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [steps_star_cycle]) 1);
+qed "accepts_plus";
+AddIffs [accepts_plus];
+
+(******************************************************)
+(*                       star                         *)
+(******************************************************)
+
+Goalw [star_def]
+"accepts (star A) w = \
+\ (? us. (!u : set us. accepts A u) & w = concat us)";
+br iffI 1;
+ by (Clarify_tac 1);
+ be disjE 1;
+  by(res_inst_tac [("x","[]")] exI 1);
+  by(Simp_tac 1);
+  by(Blast_tac 1);
+ by(Blast_tac 1);
+by(Auto_tac);
+qed "accepts_star";
+
+(***** Correctness of r2n *****)
+
+Goal
+ "!w. accepts (rexp2na r) w = (w : lang r)";
+by(induct_tac "r" 1);
+    by(simp_tac (simpset() addsimps [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);
+qed_spec_mp "accepts_rexp2na";
diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/RegExp2NA.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegExp2NA.thy	Mon Aug 17 11:00:57 1998 +0200
@@ -0,0 +1,60 @@
+(*  Title:      HOL/Lex/RegExp2NA.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Conversion of regular expressions *directly*
+into nondeterministic automata *without* epsilon transitions
+*)
+
+RegExp2NA = NA + RegExp +
+
+types 'a bitsNA = ('a,bool list)na
+
+syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
+translations "x ## S" == "op # x `` S"
+
+constdefs
+ atom  :: 'a => 'a bitsNA
+"atom a == ([True],
+            %b s. if s=[True] & b=a then {[False]} else {},
+            %s. s=[False])"
+
+ union :: 'a bitsNA => 'a bitsNA => 'a bitsNA
+"union == %(ql,dl,fl)(qr,dr,fr).
+   ([],
+    %a s. case s of
+            [] => (True ## dl a ql) Un (False ## dr a qr)
+          | left#s => if left then True ## dl a s
+                              else False ## dr a s,
+    %s. case s of [] => (fl ql | fr qr)
+                | left#s => if left then fl s else fr s)"
+
+ conc :: 'a bitsNA => 'a bitsNA => 'a bitsNA
+"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 then False ## dr a qr else {})
+                              else False ## dr a s,
+    %s. case s of [] => False | left#s => left & fl s & fr qr | ~left & fr s)"
+
+ epsilon :: 'a bitsNA
+"epsilon == ([],%a s. {}, %s. s=[])"
+
+ plus :: 'a bitsNA => 'a bitsNA
+"plus == %(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f)"
+
+ star :: 'a bitsNA => 'a bitsNA
+"star A == union epsilon (plus A)"
+
+consts rexp2na :: 'a rexp => 'a bitsNA
+primrec
+"rexp2na Empty      = ([], %a s. {}, %s. False)"
+"rexp2na(Atom a)    = atom a"
+"rexp2na(Union r s) = union (rexp2na r) (rexp2na s)"
+"rexp2na(Conc r s)  = conc  (rexp2na r) (rexp2na s)"
+"rexp2na(Star r)    = star  (rexp2na r)"
+
+end
diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/Scanner.ML
--- a/src/HOL/Lex/Scanner.ML	Mon Aug 17 11:00:27 1998 +0200
+++ b/src/HOL/Lex/Scanner.ML	Mon Aug 17 11:00:57 1998 +0200
@@ -5,6 +5,11 @@
 *)
 
 Goal
+ "DA.accepts (na2da(rexp2na r)) w = (w : lang r)";
+by (simp_tac (simpset() addsimps [NA_DA_equiv RS sym,accepts_rexp2na]) 1);
+qed "accepts_na2da_rexp2na";
+
+Goal
  "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
 by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
 qed "accepts_nae2da_rexp2nae";
diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/Scanner.thy
--- a/src/HOL/Lex/Scanner.thy	Mon Aug 17 11:00:27 1998 +0200
+++ b/src/HOL/Lex/Scanner.thy	Mon Aug 17 11:00:57 1998 +0200
@@ -4,4 +4,4 @@
     Copyright   1998 TUM
 *)
 
-Scanner = Automata + RegExp2NAe
+Scanner = Automata + RegExp2NA + RegExp2NAe