# HG changeset patch
# User nipkow
# Date 1078597887 -3600
# Node ID 3d6ed7eedfc8546101b8d12205b00437a385fa7b
# Parent  0f626a71245636e416f97cb7273f37f7c9f04209
Conversion ML -> Isar

diff -r 0f626a712456 -r 3d6ed7eedfc8 src/HOL/Lex/RegExp2NA.ML
--- a/src/HOL/Lex/RegExp2NA.ML	Fri Mar 05 15:30:49 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,429 +0,0 @@
-(*  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,thm"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 [rel_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,rel_comp_def,start_atom]) 1);
-qed "start_fin_in_steps_atom";
-
-Goal
- "accepts (atom a) w = (w = [a])";
-by (simp_tac(simpset() addsimps
-       [thm"accepts_conv_steps",start_fin_in_steps_atom,fin_atom]) 1);
-qed "accepts_atom";
-
-
-(******************************************************)
-(*                      or                            *)
-(******************************************************)
-
-(***** True/False ueber fin anheben *****)
-
-Goalw [or_def] 
- "!L R. fin (or L R) (True#p) = fin L p";
-by (Simp_tac 1);
-qed_spec_mp "fin_or_True";
-
-Goalw [or_def] 
- "!L R. fin (or L R) (False#p) = fin R p";
-by (Simp_tac 1);
-qed_spec_mp "fin_or_False";
-
-AddIffs [fin_or_True,fin_or_False];
-
-(***** True/False ueber step anheben *****)
-
-Goalw [or_def,thm"step_def"]
-"!L R. (True#p,q) : step (or 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_or";
-
-Goalw [or_def,thm"step_def"]
-"!L R. (False#p,q) : step (or 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_or";
-
-AddIffs [True_in_step_or,False_in_step_or];
-
-
-(***** True/False ueber steps anheben *****)
-
-Goal
- "!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)";
-by (induct_tac "w" 1);
-by (ALLGOALS Force_tac);
-qed_spec_mp "lift_True_over_steps_or";
-
-Goal 
- "!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)";
-by (induct_tac "w" 1);
-by (ALLGOALS Force_tac);
-qed_spec_mp "lift_False_over_steps_or";
-
-AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
-
-
-(** From the start  **)
-
-Goalw [or_def,thm"step_def"]
- "!L R. (start(or L R),q) : step(or 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_or";
-AddIffs [start_step_or];
-
-Goal
- "(start(or L R), q) : steps (or L R) w = \
-\ ( (w = [] & q = start(or L R)) | \
-\   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
-\                     q = False # p & (start R,p) : steps R w)))";
-by (case_tac "w" 1);
- by (Asm_simp_tac 1);
- by (Blast_tac 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "steps_or";
-
-Goalw [or_def]
- "!L R. fin (or L R) (start(or L R)) = \
-\       (fin L (start L) | fin R (start R))";
-by (Simp_tac 1);
-qed_spec_mp "fin_start_or";
-AddIffs [fin_start_or];
-
-Goal
- "accepts (or L R) w = (accepts L w | accepts R w)";
-by (simp_tac (simpset() addsimps [thm"accepts_conv_steps",steps_or]) 1);
-(* get rid of case_tac: *)
-by (case_tac "w = []" 1);
-by (Auto_tac);
-qed "accepts_or";
-AddIffs [accepts_or];
-
-(******************************************************)
-(*                      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,thm"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,thm"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 (ALLGOALS Force_tac);
-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);
-by (etac disjE 1);
- by (clarify_tac (claset() delrules [disjCI]) 1);
- by (etac allE 1 THEN mp_tac 1);
- by (etac disjE 1);
-  by (Blast_tac 1);
- by (rtac 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 (rtac 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 (force_tac (claset() addDs [True_steps_concD]
-     addIs [True_True_steps_concI],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 [thm"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
-     [thm"accepts_conv_steps",True_steps_conc,final_conc,start_conc]) 1);
-by (rtac iffI 1);
- by (Clarify_tac 1);
- by (etac disjE 1);
-  by (Clarify_tac 1);
-  by (etac disjE 1);
-   by (res_inst_tac [("x","w")] exI 1);
-   by (Simp_tac 1);
-   by (Blast_tac 1);
-  by (Blast_tac 1);
- by (etac 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 (case_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,thm"step_def"] "step epsilon a = {}";
-by (Simp_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,thm"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,thm"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,thm"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 (case_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. accepts A u) & \
-\              (start A,r) : steps A v)";
-by (res_inst_tac [("xs","w")] rev_induct 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);
-by (etac 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 [thm"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 [thm"accepts_conv_steps"]) 1);
-by (res_inst_tac [("xs","us")] rev_induct 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))";
-by (rtac iffI 1);
- by (asm_full_simp_tac (simpset() addsimps [thm"accepts_conv_steps"]) 1);
- by (Clarify_tac 1);
- by (dtac start_steps_plusD 1);
- by (Clarify_tac 1);
- by (res_inst_tac [("x","us@[v]")] exI 1);
- by (asm_full_simp_tac (simpset() addsimps [thm"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)";
-by (rtac iffI 1);
- by (Clarify_tac 1);
- by (etac disjE 1);
-  by (res_inst_tac [("x","[]")] exI 1);
-  by (Simp_tac 1);
-  by (Blast_tac 1);
- by (Blast_tac 1);
-by (Force_tac 1);
-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 [thm"accepts_conv_steps"]) 1);
-   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
-  by (Asm_simp_tac 1);
- by (asm_simp_tac (simpset() addsimps [accepts_conc,thm"RegSet.conc_def"]) 1);
-by (asm_simp_tac (simpset() addsimps [accepts_star,thm"in_star"]) 1);
-qed_spec_mp "accepts_rexp2na";
diff -r 0f626a712456 -r 3d6ed7eedfc8 src/HOL/Lex/RegExp2NA.thy
--- a/src/HOL/Lex/RegExp2NA.thy	Fri Mar 05 15:30:49 2004 +0100
+++ b/src/HOL/Lex/RegExp2NA.thy	Sat Mar 06 19:31:27 2004 +0100
@@ -7,20 +7,20 @@
 into nondeterministic automata *without* epsilon transitions
 *)
 
-RegExp2NA = RegExp + NA +
+theory RegExp2NA = RegExp + NA:
 
-types 'a bitsNA = ('a,bool list)na
+types 'a bitsNA = "('a,bool list)na"
 
-syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
+syntax "##" :: "'a => 'a list set => 'a list set" (infixr 65)
 translations "x ## S" == "Cons x ` S"
 
 constdefs
- atom  :: 'a => 'a bitsNA
+ atom  :: "'a => 'a bitsNA"
 "atom a == ([True],
             %b s. if s=[True] & b=a then {[False]} else {},
             %s. s=[False])"
 
- or :: 'a bitsNA => 'a bitsNA => 'a bitsNA
+ or :: "'a bitsNA => 'a bitsNA => 'a bitsNA"
 "or == %(ql,dl,fl)(qr,dr,fr).
    ([],
     %a s. case s of
@@ -30,7 +30,7 @@
     %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 :: "'a bitsNA => 'a bitsNA => 'a bitsNA"
 "conc == %(ql,dl,fl)(qr,dr,fr).
    (True#ql,
     %a s. case s of
@@ -40,16 +40,16 @@
                               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 bitsNA"
 "epsilon == ([],%a s. {}, %s. s=[])"
 
- plus :: 'a bitsNA => 'a bitsNA
+ 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 bitsNA => 'a bitsNA"
 "star A == or epsilon (plus A)"
 
-consts rexp2na :: 'a rexp => 'a bitsNA
+consts rexp2na :: "'a rexp => 'a bitsNA"
 primrec
 "rexp2na Empty      = ([], %a s. {}, %s. False)"
 "rexp2na(Atom a)    = atom a"
@@ -57,4 +57,384 @@
 "rexp2na(Conc r s)  = conc (rexp2na r) (rexp2na s)"
 "rexp2na(Star r)    = star (rexp2na r)"
 
+declare split_paired_all[simp]
+
+(******************************************************)
+(*                       atom                         *)
+(******************************************************)
+
+lemma fin_atom: "(fin (atom a) q) = (q = [False])"
+by(simp add:atom_def)
+
+lemma start_atom: "start (atom a) = [True]"
+by(simp add:atom_def)
+
+lemma in_step_atom_Some[simp]:
+ "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)"
+by (simp add: atom_def step_def)
+
+lemma False_False_in_steps_atom:
+ "([False],[False]) : steps (atom a) w = (w = [])"
+apply (induct "w")
+ apply simp
+apply (simp add: rel_comp_def)
+done
+
+lemma start_fin_in_steps_atom:
+ "(start (atom a), [False]) : steps (atom a) w = (w = [a])"
+apply (induct "w")
+ apply (simp add: start_atom)
+apply (simp add: False_False_in_steps_atom rel_comp_def start_atom)
+done
+
+lemma accepts_atom:
+ "accepts (atom a) w = (w = [a])"
+by (simp add: accepts_conv_steps start_fin_in_steps_atom fin_atom)
+
+(******************************************************)
+(*                      or                            *)
+(******************************************************)
+
+(***** lift True/False over fin *****)
+
+lemma fin_or_True[iff]:
+ "!!L R. fin (or L R) (True#p) = fin L p"
+by(simp add:or_def)
+
+lemma fin_or_False[iff]:
+ "!!L R. fin (or L R) (False#p) = fin R p"
+by(simp add:or_def)
+
+(***** lift True/False over step *****)
+
+lemma True_in_step_or[iff]:
+"!!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)"
+apply (simp add:or_def step_def)
+apply blast
+done
+
+lemma False_in_step_or[iff]:
+"!!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)"
+apply (simp add:or_def step_def)
+apply blast
+done
+
+
+(***** lift True/False over steps *****)
+
+lemma lift_True_over_steps_or[iff]:
+ "!!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)"
+apply (induct "w")
+ apply force
+apply force
+done
+
+lemma lift_False_over_steps_or[iff]:
+ "!!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)"
+apply (induct "w")
+ apply force
+apply force
+done
+
+(** From the start  **)
+
+lemma start_step_or[iff]:
+ "!!L R. (start(or L R),q) : step(or L R) a = 
+         (? p. (q = True#p & (start L,p) : step L a) | 
+               (q = False#p & (start R,p) : step R a))"
+apply (simp add:or_def step_def)
+apply blast
+done
+
+lemma steps_or:
+ "(start(or L R), q) : steps (or L R) w = 
+  ( (w = [] & q = start(or L R)) | 
+    (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | 
+                      q = False # p & (start R,p) : steps R w)))"
+apply (case_tac "w")
+ apply (simp)
+ apply blast
+apply (simp)
+apply blast
+done
+
+lemma fin_start_or[iff]:
+ "!!L R. fin (or L R) (start(or L R)) = (fin L (start L) | fin R (start R))"
+by (simp add:or_def)
+
+lemma accepts_or[iff]:
+ "accepts (or L R) w = (accepts L w | accepts R w)"
+apply (simp add: accepts_conv_steps steps_or)
+(* get rid of case_tac: *)
+apply (case_tac "w = []")
+ apply auto
+done
+
+(******************************************************)
+(*                      conc                        *)
+(******************************************************)
+
+(** True/False in fin **)
+
+lemma fin_conc_True[iff]:
+ "!!L R. fin (conc L R) (True#p) = (fin L p & fin R (start R))"
+by(simp add:conc_def)
+
+lemma fin_conc_False[iff]:
+ "!!L R. fin (conc L R) (False#p) = fin R p"
+by(simp add:conc_def)
+
+
+(** True/False in step **)
+
+lemma True_step_conc[iff]:
+ "!!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)))"
+apply (simp add:conc_def step_def)
+apply blast
+done
+
+lemma False_step_conc[iff]:
+ "!!L R. (False#p,q) : step (conc L R) a = 
+       (? r. q = False#r & (p,r) : step R a)"
+apply (simp add:conc_def step_def)
+apply blast
+done
+
+(** False in steps **)
+
+lemma False_steps_conc[iff]:
+ "!!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)"
+apply (induct "w")
+ apply fastsimp
+apply force
+done
+
+(** True in steps **)
+
+lemma True_True_steps_concI:
+ "!!L R p. (p,q) : steps L w ==> (True#p,True#q) : steps (conc L R) w"
+apply (induct "w")
+ apply simp
+apply simp
+apply fast
+done
+
+lemma True_False_step_conc[iff]:
+ "!!L R. (True#p,False#q) : step (conc L R) a = 
+         (fin L p & (start R,q) : step R a)"
+by simp
+
+lemma True_steps_concD[rule_format]:
+ "!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)))))"
+apply (induct "w")
+ apply simp
+apply simp
+apply (clarify del:disjCI)
+apply (erule disjE)
+ apply (clarify del:disjCI)
+ apply (erule allE, erule impE, assumption)
+ apply (erule disjE)
+  apply blast
+ apply (rule disjI2)
+ apply (clarify)
+ apply simp
+ apply (rule_tac x = "a#u" in exI)
+ apply simp
+ apply blast
+apply (rule disjI2)
+apply (clarify)
+apply simp
+apply (rule_tac x = "[]" in exI)
+apply simp
+apply blast
+done
+
+lemma True_steps_conc:
+ "(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(force dest!: True_steps_concD intro!: True_True_steps_concI)
+
+(** starting from the start **)
+
+lemma start_conc:
+  "!!L R. start(conc L R) = True#start L"
+by (simp add:conc_def)
+
+lemma final_conc:
+ "!!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))"
+apply (simp add:conc_def split: list.split)
+apply blast
+done
+
+lemma accepts_conc:
+ "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)"
+apply (simp add: accepts_conv_steps True_steps_conc final_conc start_conc)
+apply (rule iffI)
+ apply (clarify)
+ apply (erule disjE)
+  apply (clarify)
+  apply (erule disjE)
+   apply (rule_tac x = "w" in exI)
+   apply simp
+   apply blast
+  apply blast
+ apply (erule disjE)
+  apply blast
+ apply (clarify)
+ apply (rule_tac x = "u" in exI)
+ apply simp
+ apply blast
+apply (clarify)
+apply (case_tac "v")
+ apply simp
+ apply blast
+apply simp
+apply blast
+done
+
+(******************************************************)
+(*                     epsilon                        *)
+(******************************************************)
+
+lemma step_epsilon[simp]: "step epsilon a = {}"
+by(simp add:epsilon_def step_def)
+
+lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] & p=q)"
+by (induct "w") auto
+
+lemma accepts_epsilon[iff]: "accepts epsilon w = (w = [])"
+apply (simp add: steps_epsilon accepts_conv_steps)
+apply (simp add: epsilon_def)
+done
+
+(******************************************************)
+(*                       plus                         *)
+(******************************************************)
+
+lemma start_plus[simp]: "!!A. start (plus A) = start A"
+by(simp add:plus_def)
+
+lemma fin_plus[iff]: "!!A. fin (plus A) = fin A"
+by(simp add:plus_def)
+
+lemma step_plusI:
+  "!!A. (p,q) : step A a ==> (p,q) : step (plus A) a"
+by(simp add:plus_def step_def)
+
+lemma steps_plusI: "!!p. (p,q) : steps A w ==> (p,q) : steps (plus A) w"
+apply (induct "w")
+ apply simp
+apply simp
+apply (blast intro: step_plusI)
+done
+
+lemma step_plus_conv[iff]:
+ "!!A. (p,r): step (plus A) a = 
+       ( (p,r): step A a | fin A p & (start A,r) : step A a )"
+by(simp add:plus_def step_def)
+
+lemma fin_steps_plusI:
+ "[| (start A,q) : steps A u; u ~= []; fin A p |] 
+ ==> (p,q) : steps (plus A) u"
+apply (case_tac "u")
+ apply blast
+apply simp
+apply (blast intro: steps_plusI)
+done
+
+(* reverse list induction! Complicates matters for conc? *)
+lemma start_steps_plusD[rule_format]:
+ "!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)"
+apply (induct w rule: rev_induct)
+ apply simp
+ apply (rule_tac x = "[]" in exI)
+ apply simp
+apply simp
+apply (clarify)
+apply (erule allE, erule impE, assumption)
+apply (clarify)
+apply (erule disjE)
+ apply (rule_tac x = "us" in exI)
+ apply (simp)
+ apply blast
+apply (rule_tac x = "us@[v]" in exI)
+apply (simp add: accepts_conv_steps)
+apply blast
+done
+
+lemma steps_star_cycle[rule_format]:
+ "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)"
+apply (simp add: accepts_conv_steps)
+apply (induct us rule: rev_induct)
+ apply simp
+apply (rename_tac u us)
+apply simp
+apply (clarify)
+apply (case_tac "us = []")
+ apply (simp)
+ apply (blast intro: steps_plusI fin_steps_plusI)
+apply (clarify)
+apply (case_tac "u = []")
+ apply (simp)
+ apply (blast intro: steps_plusI fin_steps_plusI)
+apply (blast intro: steps_plusI fin_steps_plusI)
+done
+
+lemma accepts_plus[iff]:
+ "accepts (plus A) w = 
+ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))"
+apply (rule iffI)
+ apply (simp add: accepts_conv_steps)
+ apply (clarify)
+ apply (drule start_steps_plusD)
+ apply (clarify)
+ apply (rule_tac x = "us@[v]" in exI)
+ apply (simp add: accepts_conv_steps)
+ apply blast
+apply (blast intro: steps_star_cycle)
+done
+
+(******************************************************)
+(*                       star                         *)
+(******************************************************)
+
+lemma accepts_star:
+ "accepts (star A) w = (? us. (!u : set us. accepts A u) & w = concat us)"
+apply(unfold star_def)
+apply (rule iffI)
+ apply (clarify)
+ apply (erule disjE)
+  apply (rule_tac x = "[]" in exI)
+  apply simp
+ apply blast
+apply force
+done
+
+(***** Correctness of r2n *****)
+
+lemma accepts_rexp2na:
+ "!!w. accepts (rexp2na r) w = (w : lang r)"
+apply (induct "r")
+    apply (simp add: accepts_conv_steps)
+   apply (simp add: accepts_atom)
+  apply (simp)
+ apply (simp add: accepts_conc RegSet.conc_def)
+apply (simp add: accepts_star in_star)
+done
+
 end
diff -r 0f626a712456 -r 3d6ed7eedfc8 src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Fri Mar 05 15:30:49 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,630 +0,0 @@
-(*  Title:      HOL/Lex/RegExp2NAe.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";
-
-(* Use {x. False} = {}? *)
-
-Goalw [atom_def,thm"step_def"]
- "eps(atom a) = {}";
-by (Simp_tac 1);
-qed "eps_atom";
-Addsimps [eps_atom];
-
-Goalw [atom_def,thm"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 "([False],[False]) : steps (atom a) w = (w = [])";
-by (induct_tac "w" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [rel_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,thm"rtrancl_empty"]) 1);
-by (asm_full_simp_tac (simpset()
-     addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1);
-qed "start_fin_in_steps_atom";
-
-Goal "accepts (atom a) w = (w = [a])";
-by (simp_tac(simpset() addsimps
-       [thm"accepts_def",start_fin_in_steps_atom,fin_atom]) 1);
-qed "accepts_atom";
-
-
-(******************************************************)
-(*                      or                            *)
-(******************************************************)
-
-(***** True/False ueber fin anheben *****)
-
-Goalw [or_def] 
- "!L R. fin (or L R) (True#p) = fin L p";
-by (Simp_tac 1);
-qed_spec_mp "fin_or_True";
-
-Goalw [or_def] 
- "!L R. fin (or L R) (False#p) = fin R p";
-by (Simp_tac 1);
-qed_spec_mp "fin_or_False";
-
-AddIffs [fin_or_True,fin_or_False];
-
-(***** True/False ueber step anheben *****)
-
-Goalw [or_def,thm"step_def"]
-"!L R. (True#p,q) : step (or 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_or";
-
-Goalw [or_def,thm"step_def"]
-"!L R. (False#p,q) : step (or 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_or";
-
-AddIffs [True_in_step_or,False_in_step_or];
-
-(***** True/False ueber epsclosure anheben *****)
-
-Goal
- "(tp,tq) : (eps(or L R))^* ==> \
-\ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
-by (etac 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
- "(tp,tq) : (eps(or L R))^* ==> \
-\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
-by (etac 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
- "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(or L R))^*";
-by (etac rtrancl_induct 1);
- by (Blast_tac 1);
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-val lemma2a = result();
-
-Goal
- "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(or L R))^*";
-by (etac rtrancl_induct 1);
- by (Blast_tac 1);
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-val lemma2b = result();
-
-Goal
- "(True#p,q) : (eps(or L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
-by (blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
-qed "True_epsclosure_or";
-
-Goal
- "(False#p,q) : (eps(or L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
-by (blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
-qed "False_epsclosure_or";
-
-AddIffs [True_epsclosure_or,False_epsclosure_or];
-
-(***** True/False ueber steps anheben *****)
-
-Goal
- "!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)";
-by (induct_tac "w" 1);
- by Auto_tac;
-by (Force_tac 1);
-qed_spec_mp "lift_True_over_steps_or";
-
-Goal 
- "!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)";
-by (induct_tac "w" 1);
- by Auto_tac;
-by (Force_tac 1);
-qed_spec_mp "lift_False_over_steps_or";
-
-AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
-
-
-(***** Epsilonhuelle des Startzustands  *****)
-
-Goal
- "R^* = Id Un (R^* O R)";
-by (rtac set_ext 1);
-by (split_all_tac 1);
-by (rtac iffI 1);
- by (etac rtrancl_induct 1);
-  by (Blast_tac 1);
- by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-by (blast_tac (claset() addIs [converse_rtrancl_into_rtrancl]) 1);
-qed "unfold_rtrancl2";
-
-Goal
- "(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_or =
-  read_instantiate [("p","start(or L R)")] in_unfold_rtrancl2;
-AddIffs [epsclosure_start_step_or];
-
-Goalw [or_def,thm"step_def"]
- "!L R. (start(or L R),q) : eps(or L R) = \
-\       (q = True#start L | q = False#start R)";
-by (Simp_tac 1);
-qed_spec_mp "start_eps_or";
-AddIffs [start_eps_or];
-
-Goalw [or_def,thm"step_def"]
- "!L R. (start(or L R),q) ~: step (or L R) (Some a)";
-by (Simp_tac 1);
-qed_spec_mp "not_start_step_or_Some";
-AddIffs [not_start_step_or_Some];
-
-Goal
- "(start(or L R), q) : steps (or L R) w = \
-\ ( (w = [] & q = start(or L R)) | \
-\   (? p.  q = True  # p & (start L,p) : steps L w | \
-\          q = False # p & (start R,p) : steps R w) )";
-by (case_tac "w" 1);
- by (Asm_simp_tac 1);
- by (Blast_tac 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "steps_or";
-
-Goalw [or_def]
- "!L R. ~ fin (or L R) (start(or L R))";
-by (Simp_tac 1);
-qed_spec_mp "start_or_not_final";
-AddIffs [start_or_not_final];
-
-Goalw [thm"accepts_def"]
- "accepts (or L R) w = (accepts L w | accepts R w)";
-by (simp_tac (simpset() addsimps [steps_or]) 1);
-by Auto_tac;
-qed "accepts_or";
-
-
-(******************************************************)
-(*                      conc                          *)
-(******************************************************)
-
-(** True/False in fin **)
-
-Goalw [conc_def]
- "!L R. fin (conc L R) (True#p) = False";
-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,thm"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 [conc_def,thm"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
- "(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
- "(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
- "((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
- "!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);
-by (Fast_tac 1);  (*MUCH faster than Blast_tac*)
-qed_spec_mp "False_steps_conc";
-AddIffs [False_steps_conc];
-
-(** True in epsclosure **)
-
-Goal
- "(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);
-qed "True_True_eps_concI";
-
-Goal
- "!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
- "(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
- "(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 [conc_def,thm"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
- "(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 [conc_def,thm"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
- "((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);
-by (etac disjE 1);
- by (blast_tac (claset() addIs [lemma2a]) 1);
-by (Clarify_tac 1);
-by (rtac (rtrancl_trans) 1);
-by (etac lemma2a 1);
-by (rtac converse_rtrancl_into_rtrancl 1);
-by (etac True_False_eps_concI 1);
-by (etac lemma2b 1);
-qed "True_epsclosure_conc";
-AddIffs [True_epsclosure_conc];
-
-(** True in steps **)
-
-Goal
- "!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);
- by (etac disjE 1);
- by (clarify_tac (claset() delrules [disjCI]) 1);
- by (etac disjE 1);
-  by (clarify_tac (claset() delrules [disjCI]) 1);
-  by (etac allE 1 THEN mp_tac 1);
-  by (etac disjE 1);
-   by (Blast_tac 1);
-  by (rtac 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);
-by (rtac 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 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,thm"in_steps_epsclosure"]) 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 = (? s. p = False#s & fin R s)";
-by (simp_tac (simpset() addsplits [thm"list.split"]) 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
-     [thm"accepts_def",True_steps_conc,final_conc,start_conc]) 1);
-by (Blast_tac 1);
-qed "accepts_conc";
-
-(******************************************************)
-(*                       star                         *)
-(******************************************************)
-
-Goalw [star_def,thm"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 [star_def,thm"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
-  "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
-by (etac 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 [star_def,thm"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
- "(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))";
-by (etac 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
- "((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)";
-by (rtac iffI 1);
- by (dtac lemma 1);
- by (Blast_tac 1);
-(* Why can't blast_tac do the rest? *)
-by (Clarify_tac 1);
-by (etac disjE 1);
-by (etac True_True_eps_starI 1);
-by (Clarify_tac 1);
-by (rtac rtrancl_trans 1);
-by (etac True_True_eps_starI 1);
-by (rtac rtrancl_trans 1);
-by (rtac r_into_rtrancl 1);
-by (etac True_start_eps_starI 1);
-by (etac True_True_eps_starI 1);
-qed "True_eps_star";
-AddIffs [True_eps_star];
-
-(** True in step Some **)
-
-Goalw [star_def,thm"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
- "!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")] rev_induct 1);
- by (Asm_full_simp_tac 1);
- by (Clarify_tac 1);
- by (res_inst_tac [("x","[]")] exI 1);
- by (etac disjE 1);
-  by (Asm_simp_tac 1);
- by (Clarify_tac 1);
- by (Asm_simp_tac 1);
-by (simp_tac (simpset() addsimps [O_assoc,thm"epsclosure_steps"]) 1);
-by (Clarify_tac 1);
-by (etac allE 1 THEN mp_tac 1);
-by (Clarify_tac 1);
-by (etac 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,thm"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 [thm"accepts_def"]) 1);
-by (Blast_tac 1);
-qed_spec_mp "True_start_steps_starD";
-
-Goal "!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 [thm"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,thm"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
- "(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 (rtac iffI 1);
- by (etac 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 [star_def,thm"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
- "(start(star A),r) : steps (star A) w = \
-\ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
-by (rtac iffI 1);
- by (case_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);
-by (etac disjE 1);
- by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [thm"in_steps_epsclosure"]) 1);
-qed "start_steps_star";
-
-Goalw [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 [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 [thm"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);
-by (rtac iffI 1);
- by (Clarify_tac 1);
- by (etac 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 [thm"accepts_def"]) 1);
- by (Blast_tac 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("xs","us")] rev_exhaust 1);
- by (Asm_simp_tac 1);
- by (Blast_tac 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [thm"accepts_def"]) 1);
-by (Blast_tac 1);
-qed "accepts_star";
-
-
-(***** Correctness of r2n *****)
-
-Goal
- "!w. accepts (rexp2nae r) w = (w : lang r)";
-by (induct_tac "r" 1);
-    by (simp_tac (simpset() addsimps [thm"accepts_def"]) 1);
-   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
-  by (asm_simp_tac (simpset() addsimps [accepts_or]) 1);
- by (asm_simp_tac (simpset() addsimps [accepts_conc,thm"RegSet.conc_def"]) 1);
-by (asm_simp_tac (simpset() addsimps [accepts_star,thm"in_star"]) 1);
-qed "accepts_rexp2nae";
diff -r 0f626a712456 -r 3d6ed7eedfc8 src/HOL/Lex/RegExp2NAe.thy
--- a/src/HOL/Lex/RegExp2NAe.thy	Fri Mar 05 15:30:49 2004 +0100
+++ b/src/HOL/Lex/RegExp2NAe.thy	Sat Mar 06 19:31:27 2004 +0100
@@ -7,20 +7,20 @@
 into nondeterministic automata with epsilon transitions
 *)
 
-RegExp2NAe = RegExp + NAe +
+theory RegExp2NAe = RegExp + NAe:
 
-types 'a bitsNAe = ('a,bool list)nae
+types 'a bitsNAe = "('a,bool list)nae"
 
-syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
+syntax "##" :: "'a => 'a list set => 'a list set" (infixr 65)
 translations "x ## S" == "Cons x ` S"
 
 constdefs
- atom  :: 'a => 'a bitsNAe
+ atom  :: "'a => 'a bitsNAe"
 "atom a == ([True],
             %b s. if s=[True] & b=Some a then {[False]} else {},
             %s. s=[False])"
 
- or :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
+ or :: "'a bitsNAe => 'a bitsNAe => 'a bitsNAe"
 "or == %(ql,dl,fl)(qr,dr,fr).
    ([],
     %a s. case s of
@@ -29,7 +29,7 @@
                               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 :: "'a bitsNAe => 'a bitsNAe => 'a bitsNAe"
 "conc == %(ql,dl,fl)(qr,dr,fr).
    (True#ql,
     %a s. case s of
@@ -39,7 +39,7 @@
                               else False ## dr a s,
     %s. case s of [] => False | left#s => ~left & fr s)"
 
- star :: 'a bitsNAe => 'a bitsNAe
+ star :: "'a bitsNAe => 'a bitsNAe"
 "star == %(q,d,f).
    ([],
     %a s. case s of
@@ -49,7 +49,7 @@
                               else {},
     %s. case s of [] => True | left#s => left & f s)"
 
-consts rexp2nae :: 'a rexp => 'a bitsNAe
+consts rexp2nae :: "'a rexp => 'a bitsNAe"
 primrec
 "rexp2nae Empty      = ([], %a s. {}, %s. False)"
 "rexp2nae(Atom a)    = atom a"
@@ -57,4 +57,566 @@
 "rexp2nae(Conc r s)  = conc (rexp2nae r) (rexp2nae s)"
 "rexp2nae(Star r)    = star (rexp2nae r)"
 
+declare split_paired_all[simp]
+
+(******************************************************)
+(*                       atom                         *)
+(******************************************************)
+
+lemma fin_atom: "(fin (atom a) q) = (q = [False])"
+by(simp add:atom_def)
+
+lemma start_atom: "start (atom a) = [True]"
+by(simp add:atom_def)
+
+(* Use {x. False} = {}? *)
+
+lemma eps_atom[simp]:
+ "eps(atom a) = {}"
+by (simp add:atom_def step_def)
+
+lemma in_step_atom_Some[simp]:
+ "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)"
+by (simp add:atom_def step_def)
+
+lemma False_False_in_steps_atom:
+  "([False],[False]) : steps (atom a) w = (w = [])"
+apply (induct "w")
+ apply (simp)
+apply (simp add: rel_comp_def)
+done
+
+lemma start_fin_in_steps_atom:
+  "(start (atom a), [False]) : steps (atom a) w = (w = [a])"
+apply (induct "w")
+ apply (simp add: start_atom rtrancl_empty)
+apply (simp add: False_False_in_steps_atom rel_comp_def start_atom)
+done
+
+lemma accepts_atom: "accepts (atom a) w = (w = [a])"
+by (simp add: accepts_def start_fin_in_steps_atom fin_atom)
+
+
+(******************************************************)
+(*                      or                            *)
+(******************************************************)
+
+(***** lift True/False over fin *****)
+
+lemma fin_or_True[iff]:
+ "!!L R. fin (or L R) (True#p) = fin L p"
+by(simp add:or_def)
+
+lemma fin_or_False[iff]:
+ "!!L R. fin (or L R) (False#p) = fin R p"
+by(simp add:or_def)
+
+(***** lift True/False over step *****)
+
+lemma True_in_step_or[iff]:
+"!!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)"
+apply (simp add:or_def step_def)
+apply blast
+done
+
+lemma False_in_step_or[iff]:
+"!!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)"
+apply (simp add:or_def step_def)
+apply blast
+done
+
+
+(***** lift True/False over epsclosure *****)
+
+lemma lemma1a:
+ "(tp,tq) : (eps(or L R))^* ==> 
+ (!!p. tp = True#p ==> ? q. (p,q) : (eps L)^* & tq = True#q)"
+apply (induct rule:rtrancl_induct)
+ apply (blast)
+apply (clarify)
+apply (simp)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma lemma1b:
+ "(tp,tq) : (eps(or L R))^* ==> 
+ (!!p. tp = False#p ==> ? q. (p,q) : (eps R)^* & tq = False#q)"
+apply (induct rule:rtrancl_induct)
+ apply (blast)
+apply (clarify)
+apply (simp)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma lemma2a:
+ "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(or L R))^*"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma lemma2b:
+ "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(or L R))^*"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma True_epsclosure_or[iff]:
+ "(True#p,q) : (eps(or L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)"
+by (blast dest: lemma1a lemma2a)
+
+lemma False_epsclosure_or[iff]:
+ "(False#p,q) : (eps(or L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)"
+by (blast dest: lemma1b lemma2b)
+
+(***** lift True/False over steps *****)
+
+lemma lift_True_over_steps_or[iff]:
+ "!!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)"
+apply (induct "w")
+ apply auto
+apply force
+done
+
+lemma lift_False_over_steps_or[iff]:
+ "!!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)"
+apply (induct "w")
+ apply auto
+apply (force)
+done
+
+(***** Epsilon closure of start state *****)
+
+lemma unfold_rtrancl2:
+ "R^* = Id Un (R^* O R)"
+apply (rule set_ext)
+apply (simp)
+apply (rule iffI)
+ apply (erule rtrancl_induct)
+  apply (blast)
+ apply (blast intro: rtrancl_into_rtrancl)
+apply (blast intro: converse_rtrancl_into_rtrancl)
+done
+
+lemma in_unfold_rtrancl2:
+ "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))"
+apply (rule unfold_rtrancl2[THEN equalityE])
+apply (blast)
+done
+
+lemmas [iff] = in_unfold_rtrancl2[where p = "start(or L R)", standard]
+
+lemma start_eps_or[iff]:
+ "!!L R. (start(or L R),q) : eps(or L R) = 
+       (q = True#start L | q = False#start R)"
+by (simp add:or_def step_def)
+
+lemma not_start_step_or_Some[iff]:
+ "!!L R. (start(or L R),q) ~: step (or L R) (Some a)"
+by (simp add:or_def step_def)
+
+lemma steps_or:
+ "(start(or L R), q) : steps (or L R) w = 
+ ( (w = [] & q = start(or L R)) | 
+   (? p.  q = True  # p & (start L,p) : steps L w | 
+          q = False # p & (start R,p) : steps R w) )"
+apply (case_tac "w")
+ apply (simp)
+ apply (blast)
+apply (simp)
+apply (blast)
+done
+
+lemma start_or_not_final[iff]:
+ "!!L R. ~ fin (or L R) (start(or L R))"
+by (simp add:or_def)
+
+lemma accepts_or:
+ "accepts (or L R) w = (accepts L w | accepts R w)"
+apply (simp add:accepts_def steps_or)
+ apply auto
+done
+
+
+(******************************************************)
+(*                      conc                          *)
+(******************************************************)
+
+(** True/False in fin **)
+
+lemma in_conc_True[iff]:
+ "!!L R. fin (conc L R) (True#p) = False"
+by (simp add:conc_def)
+
+lemma fin_conc_False[iff]:
+ "!!L R. fin (conc L R) (False#p) = fin R p"
+by (simp add:conc_def)
+
+(** True/False in step **)
+
+lemma True_step_conc[iff]:
+ "!!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 add:conc_def step_def) (blast)
+
+lemma False_step_conc[iff]:
+ "!!L R. (False#p,q) : step (conc L R) a = 
+       (? r. q = False#r & (p,r) : step R a)"
+by (simp add:conc_def step_def) (blast)
+
+(** False in epsclosure **)
+
+lemma lemma1b:
+ "(tp,tq) : (eps(conc L R))^* ==> 
+  (!!p. tp = False#p ==> ? q. (p,q) : (eps R)^* & tq = False#q)"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma lemma2b:
+ "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma False_epsclosure_conc[iff]:
+ "((False # p, q) : (eps (conc L R))^*) = 
+ (? r. q = False # r & (p, r) : (eps R)^*)"
+apply (rule iffI)
+ apply (blast dest: lemma1b)
+apply (blast dest: lemma2b)
+done
+
+(** False in steps **)
+
+lemma False_steps_conc[iff]:
+ "!!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)"
+apply (induct "w")
+ apply (simp)
+apply (simp)
+apply (fast)  (*MUCH faster than blast*)
+done
+
+(** True in epsclosure **)
+
+lemma True_True_eps_concI:
+ "(p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma True_True_steps_concI:
+ "!!p. (p,q) : steps L w ==> (True#p,True#q) : steps (conc L R) w"
+apply (induct "w")
+ apply (simp add: True_True_eps_concI)
+apply (simp)
+apply (blast intro: True_True_eps_concI)
+done
+
+lemma lemma1a:
+ "(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)^*))"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma lemma2a:
+ "(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma lem:
+ "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None"
+by(simp add: conc_def step_def)
+
+lemma lemma2b:
+ "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (drule lem)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma True_False_eps_concI:
+ "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)"
+by(simp add: conc_def step_def)
+
+lemma True_epsclosure_conc[iff]:
+ "((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)))"
+apply (rule iffI)
+ apply (blast dest: lemma1a)
+apply (erule disjE)
+ apply (blast intro: lemma2a)
+apply (clarify)
+apply (rule rtrancl_trans)
+apply (erule lemma2a)
+apply (rule converse_rtrancl_into_rtrancl)
+apply (erule True_False_eps_concI)
+apply (erule lemma2b)
+done
+
+(** True in steps **)
+
+lemma True_steps_concD[rule_format]:
+ "!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))))"
+apply (induct "w")
+ apply (simp)
+apply (simp)
+apply (clarify del: disjCI)
+ apply (erule disjE)
+ apply (clarify del: disjCI)
+ apply (erule disjE)
+  apply (clarify del: disjCI)
+  apply (erule allE, erule impE, assumption)
+  apply (erule disjE)
+   apply (blast)
+  apply (rule disjI2)
+  apply (clarify)
+  apply (simp)
+  apply (rule_tac x = "a#u" in exI)
+  apply (simp)
+  apply (blast)
+ apply (blast)
+apply (rule disjI2)
+apply (clarify)
+apply (simp)
+apply (rule_tac x = "[]" in exI)
+apply (simp)
+apply (blast)
+done
+
+lemma True_steps_conc:
+ "(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 dest: True_steps_concD
+    intro: True_True_steps_concI in_steps_epsclosure)
+
+(** starting from the start **)
+
+lemma start_conc:
+  "!!L R. start(conc L R) = True#start L"
+by (simp add: conc_def)
+
+lemma final_conc:
+ "!!L R. fin(conc L R) p = (? s. p = False#s & fin R s)"
+by (simp add:conc_def split: list.split)
+
+lemma accepts_conc:
+ "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)"
+apply (simp add: accepts_def True_steps_conc final_conc start_conc)
+apply (blast)
+done
+
+(******************************************************)
+(*                       star                         *)
+(******************************************************)
+
+lemma True_in_eps_star[iff]:
+ "!!A. (True#p,q) : eps(star A) = 
+     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )"
+by (simp add:star_def step_def) (blast)
+
+lemma True_True_step_starI:
+  "!!A. (p,q) : step A a ==> (True#p, True#q) : step (star A) a"
+by (simp add:star_def step_def)
+
+lemma True_True_eps_starI:
+  "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*"
+apply (induct rule: rtrancl_induct)
+ apply (blast)
+apply (blast intro: True_True_step_starI rtrancl_into_rtrancl)
+done
+
+lemma True_start_eps_starI:
+ "!!A. fin A p ==> (True#p,True#start A) : eps(star A)"
+by (simp add:star_def step_def)
+
+lemma lem:
+ "(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))"
+apply (induct rule: rtrancl_induct)
+ apply (simp)
+apply (clarify)
+apply (simp)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemma True_eps_star[iff]:
+ "((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)"
+apply (rule iffI)
+ apply (drule lem)
+ apply (blast)
+(* Why can't blast do the rest? *)
+apply (clarify)
+apply (erule disjE)
+apply (erule True_True_eps_starI)
+apply (clarify)
+apply (rule rtrancl_trans)
+apply (erule True_True_eps_starI)
+apply (rule rtrancl_trans)
+apply (rule r_into_rtrancl)
+apply (erule True_start_eps_starI)
+apply (erule True_True_eps_starI)
+done
+
+(** True in step Some **)
+
+lemma True_step_star[iff]:
+ "!!A. (True#p,r): step (star A) (Some a) = 
+     (? q. (p,q): step A (Some a) & r=True#q)"
+by (simp add:star_def step_def) (blast)
+
+
+(** True in steps **)
+
+(* reverse list induction! Complicates matters for conc? *)
+lemma True_start_steps_starD[rule_format]:
+ "!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))"
+apply (induct w rule: rev_induct)
+ apply (simp)
+ apply (clarify)
+ apply (rule_tac x = "[]" in exI)
+ apply (erule disjE)
+  apply (simp)
+ apply (clarify)
+ apply (simp)
+apply (simp add: O_assoc epsclosure_steps)
+apply (clarify)
+apply (erule allE, erule impE, assumption)
+apply (clarify)
+apply (erule disjE)
+ apply (rule_tac x = "us" in exI)
+ apply (rule_tac x = "v@[x]" in exI)
+ apply (simp add: O_assoc epsclosure_steps)
+ apply (blast)
+apply (clarify)
+apply (rule_tac x = "us@[v@[x]]" in exI)
+apply (rule_tac x = "[]" in exI)
+apply (simp add: accepts_def)
+apply (blast)
+done
+
+lemma True_True_steps_starI:
+  "!!p. (p,q) : steps A w ==> (True#p,True#q) : steps (star A) w"
+apply (induct "w")
+ apply (simp)
+apply (simp)
+apply (blast intro: True_True_eps_starI True_True_step_starI)
+done
+
+lemma steps_star_cycle:
+ "(!u : set us. accepts A u) ==> 
+ (True#start A,True#start A) : steps (star A) (concat us)"
+apply (induct "us")
+ apply (simp add:accepts_def)
+apply (simp add:accepts_def)
+by(blast intro: True_True_steps_starI True_start_eps_starI in_epsclosure_steps)
+
+(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
+lemma True_start_steps_star:
+ "(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))"
+apply (rule iffI)
+ apply (erule True_start_steps_starD)
+apply (clarify)
+apply (blast intro: steps_star_cycle True_True_steps_starI)
+done
+
+(** the start state **)
+
+lemma start_step_star[iff]:
+  "!!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)"
+by (simp add:star_def step_def)
+
+lemmas epsclosure_start_step_star =
+  in_unfold_rtrancl2[where p = "start(star A)", standard]
+
+lemma start_steps_star:
+ "(start(star A),r) : steps (star A) w = 
+ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)"
+apply (rule iffI)
+ apply (case_tac "w")
+  apply (simp add: epsclosure_start_step_star)
+ apply (simp)
+ apply (clarify)
+ apply (simp add: epsclosure_start_step_star)
+ apply (blast)
+apply (erule disjE)
+ apply (simp)
+apply (blast intro: in_steps_epsclosure)
+done
+
+lemma fin_star_True[iff]: "!!A. fin (star A) (True#p) = fin A p"
+by (simp add:star_def)
+
+lemma fin_star_start[iff]: "!!A. fin (star A) (start(star A))"
+by (simp add:star_def)
+
+(* too complex! Simpler if loop back to start(star A)? *)
+lemma accepts_star:
+ "accepts (star A) w = 
+ (? us. (!u : set(us). accepts A u) & (w = concat us) )"
+apply(unfold accepts_def)
+apply (simp add: start_steps_star True_start_steps_star)
+apply (rule iffI)
+ apply (clarify)
+ apply (erule disjE)
+  apply (clarify)
+  apply (simp)
+  apply (rule_tac x = "[]" in exI)
+  apply (simp)
+ apply (clarify)
+ apply (rule_tac x = "us@[v]" in exI)
+ apply (simp add: accepts_def)
+ apply (blast)
+apply (clarify)
+apply (rule_tac xs = "us" in rev_exhaust)
+ apply (simp)
+ apply (blast)
+apply (clarify)
+apply (simp add: accepts_def)
+apply (blast)
+done
+
+
+(***** Correctness of r2n *****)
+
+lemma accepts_rexp2nae:
+ "!!w. accepts (rexp2nae r) w = (w : lang r)"
+apply (induct "r")
+    apply (simp add: accepts_def)
+   apply (simp add: accepts_atom)
+  apply (simp add: accepts_or)
+ apply (simp add: accepts_conc RegSet.conc_def)
+apply (simp add: accepts_star in_star)
+done
+
 end