# HG changeset patch
# User nipkow
# Date 894645209 -7200
# Node ID 0eb6730de30f0866d30d8ea4d9a7a5dc533f3251
# Parent  0537ee95d00402d2f1d394d8840d965f7d698df7
Reshuffeling, renaming and a few simple corollaries.

diff -r 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/Automata.ML
--- a/src/HOL/Lex/Automata.ML	Fri May 08 15:45:01 1998 +0200
+++ b/src/HOL/Lex/Automata.ML	Fri May 08 18:33:29 1998 +0200
@@ -7,7 +7,7 @@
 (*** Equivalence of NA and DA --- redundant ***)
 
 goalw thy [na2da_def]
- "!Q. DA.delta (na2da A) w Q = lift(NA.delta A w) Q";
+ "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
 by(induct_tac "w" 1);
  by(ALLGOALS Asm_simp_tac);
  by(ALLGOALS Blast_tac);
@@ -35,7 +35,7 @@
 val lemma = result();
 
 goalw thy [NAe.accepts_def,DA.accepts_def]
-  "NAe.accepts A w = DA.accepts (nae2da A) w";
+  "DA.accepts (nae2da A) w = NAe.accepts A w";
 by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
 by(simp_tac (simpset() addsimps [nae2da_def]) 1);
 by(Blast_tac 1);
diff -r 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/Automata.thy
--- a/src/HOL/Lex/Automata.thy	Fri May 08 15:45:01 1998 +0200
+++ b/src/HOL/Lex/Automata.thy	Fri May 08 18:33:29 1998 +0200
@@ -10,11 +10,11 @@
 
 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)"
+"na2da A == ({start A}, %a Q. Union(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),
+              %a Q. Union(next A (Some a) `` ((eps A)^* ^^ Q)),
               %Q. ? p: (eps A)^* ^^ Q. fin A p)"
 
 end
diff -r 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/NA.thy
--- a/src/HOL/Lex/NA.thy	Fri May 08 15:45:01 1998 +0200
+++ b/src/HOL/Lex/NA.thy	Fri May 08 18:33:29 1998 +0200
@@ -10,13 +10,10 @@
 
 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)"
+"delta A (a#w) p = Union(delta A w `` next A a p)"
 
 constdefs
  accepts ::   ('a,'s)na => 'a list => bool
diff -r 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/NAe_of_RegExp.ML
--- a/src/HOL/Lex/NAe_of_RegExp.ML	Fri May 08 15:45:01 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,663 +0,0 @@
-(*  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 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/NAe_of_RegExp.thy
--- a/src/HOL/Lex/NAe_of_RegExp.thy	Fri May 08 15:45:01 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  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 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Fri May 08 15:45:01 1998 +0200
+++ b/src/HOL/Lex/ROOT.ML	Fri May 08 18:33:29 1998 +0200
@@ -9,10 +9,10 @@
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
 use_thy"AutoMaxChop";
-(* Do no swap the next 2.
+(* Do not swap the next two use_thy's.
    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";
+use_thy"RegExp2NAe";
+use_thy"Scanner";
diff -r 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/RegExp2NAe.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegExp2NAe.ML	Fri May 08 18:33:29 1998 +0200
@@ -0,0 +1,671 @@
+(*  Title:      HOL/Lex/RegExp2NAe.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";
+
+goal thy
+ "accepts (atom a) w = (w = [a])";
+by(simp_tac(simpset() addsimps
+       [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
+qed "accepts_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 "accepts_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";
+
+goal thy
+ "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
+by (simp_tac (simpset() addsimps
+     [accepts_def,True_steps_conc,final_conc,start_conc]) 1);
+by(Blast_tac 1);
+qed "accepts_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. accepts (rexp2nae r) w = (w : lang r)";
+by(induct_tac "r" 1);
+    by(simp_tac (simpset() addsimps [accepts_def]) 1);
+   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
+  by(asm_simp_tac (simpset() addsimps [accepts_union]) 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 "accepts_rexp2nae";
diff -r 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/RegExp2NAe.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegExp2NAe.thy	Fri May 08 18:33:29 1998 +0200
@@ -0,0 +1,60 @@
+(*  Title:      HOL/Lex/RegExp2NAe.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Conversion of regular expressions
+into nondeterministic automata with epsilon transitions
+*)
+
+RegExp2NAe = NAe + RegExp +
+
+types 'a bitsNAe = ('a,bool list)nae
+
+syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
+translations "x ## S" == "op # x `` S"
+
+constdefs
+ atom  :: 'a => 'a bitsNAe
+"atom a == ([True],
+            %b s. if s=[True] & b=Some a then {[False]} else {},
+            %s. s=[False])"
+
+ union :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
+"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 bitsNAe => 'a bitsNAe => 'a bitsNAe
+"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 bitsNAe => 'a bitsNAe
+"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 rexp2nae :: 'a rexp => 'a bitsNAe
+primrec rexp2nae rexp
+"rexp2nae Empty      = ([], %a s. {}, %s. False)"
+"rexp2nae(Atom a)    = atom a"
+"rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Conc r s)  = conc  (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Star r)    = star  (rexp2nae r)"
+
+end
diff -r 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/Scanner.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Scanner.ML	Fri May 08 18:33:29 1998 +0200
@@ -0,0 +1,10 @@
+(*  Title:      HOL/Lex/Scanner.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+goal thy
+ "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 0537ee95d004 -r 0eb6730de30f src/HOL/Lex/Scanner.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Scanner.thy	Fri May 08 18:33:29 1998 +0200
@@ -0,0 +1,7 @@
+(*  Title:      HOL/Lex/Scanner.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+Scanner = Automata + RegExp2NAe