Added code generation to Scanner.thy
authornipkow
Thu Jan 17 19:32:22 2002 +0100 (2002-01-17)
changeset 12792b344226f924c
parent 12791 ccc0f45ad2c4
child 12793 e99d4a6cba8b
Added code generation to Scanner.thy
Renamed Union -> Or, union -> or
src/HOL/Lex/RegExp.thy
src/HOL/Lex/RegExp2NA.ML
src/HOL/Lex/RegExp2NA.thy
src/HOL/Lex/RegExp2NAe.ML
src/HOL/Lex/RegExp2NAe.thy
src/HOL/Lex/Scanner.thy
     1.1 --- a/src/HOL/Lex/RegExp.thy	Thu Jan 17 15:06:36 2002 +0100
     1.2 +++ b/src/HOL/Lex/RegExp.thy	Thu Jan 17 19:32:22 2002 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  datatype 'a rexp = Empty
     1.6                   | Atom 'a
     1.7 -                 | Union ('a rexp) ('a rexp)
     1.8 +                 | Or   ('a rexp) ('a rexp)
     1.9                   | Conc ('a rexp) ('a rexp)
    1.10                   | Star ('a rexp)
    1.11  
    1.12 @@ -18,7 +18,7 @@
    1.13  primrec
    1.14  "lang Empty = {}"
    1.15  "lang (Atom a) = {[a]}"
    1.16 -"lang (Union el er) = (lang el) Un (lang er)"
    1.17 +"lang (Or el er) = (lang el) Un (lang er)"
    1.18  "lang (Conc el er) = RegSet.conc (lang el) (lang er)"
    1.19  "lang (Star e) = RegSet.star(lang e)"
    1.20  
     2.1 --- a/src/HOL/Lex/RegExp2NA.ML	Thu Jan 17 15:06:36 2002 +0100
     2.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Thu Jan 17 19:32:22 2002 +0100
     2.3 @@ -45,71 +45,71 @@
     2.4  
     2.5  
     2.6  (******************************************************)
     2.7 -(*                      union                         *)
     2.8 +(*                      or                            *)
     2.9  (******************************************************)
    2.10  
    2.11  (***** True/False ueber fin anheben *****)
    2.12  
    2.13 -Goalw [union_def] 
    2.14 - "!L R. fin (union L R) (True#p) = fin L p";
    2.15 +Goalw [or_def] 
    2.16 + "!L R. fin (or L R) (True#p) = fin L p";
    2.17  by (Simp_tac 1);
    2.18 -qed_spec_mp "fin_union_True";
    2.19 +qed_spec_mp "fin_or_True";
    2.20  
    2.21 -Goalw [union_def] 
    2.22 - "!L R. fin (union L R) (False#p) = fin R p";
    2.23 +Goalw [or_def] 
    2.24 + "!L R. fin (or L R) (False#p) = fin R p";
    2.25  by (Simp_tac 1);
    2.26 -qed_spec_mp "fin_union_False";
    2.27 +qed_spec_mp "fin_or_False";
    2.28  
    2.29 -AddIffs [fin_union_True,fin_union_False];
    2.30 +AddIffs [fin_or_True,fin_or_False];
    2.31  
    2.32  (***** True/False ueber step anheben *****)
    2.33  
    2.34 -Goalw [union_def,step_def]
    2.35 -"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    2.36 +Goalw [or_def,step_def]
    2.37 +"!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)";
    2.38  by (Simp_tac 1);
    2.39  by (Blast_tac 1);
    2.40 -qed_spec_mp "True_in_step_union";
    2.41 +qed_spec_mp "True_in_step_or";
    2.42  
    2.43 -Goalw [union_def,step_def]
    2.44 -"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    2.45 +Goalw [or_def,step_def]
    2.46 +"!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)";
    2.47  by (Simp_tac 1);
    2.48  by (Blast_tac 1);
    2.49 -qed_spec_mp "False_in_step_union";
    2.50 +qed_spec_mp "False_in_step_or";
    2.51  
    2.52 -AddIffs [True_in_step_union,False_in_step_union];
    2.53 +AddIffs [True_in_step_or,False_in_step_or];
    2.54  
    2.55  
    2.56  (***** True/False ueber steps anheben *****)
    2.57  
    2.58  Goal
    2.59 - "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
    2.60 + "!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)";
    2.61  by (induct_tac "w" 1);
    2.62  by (ALLGOALS Force_tac);
    2.63 -qed_spec_mp "lift_True_over_steps_union";
    2.64 +qed_spec_mp "lift_True_over_steps_or";
    2.65  
    2.66  Goal 
    2.67 - "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
    2.68 + "!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)";
    2.69  by (induct_tac "w" 1);
    2.70  by (ALLGOALS Force_tac);
    2.71 -qed_spec_mp "lift_False_over_steps_union";
    2.72 +qed_spec_mp "lift_False_over_steps_or";
    2.73  
    2.74 -AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
    2.75 +AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
    2.76  
    2.77  
    2.78  (** From the start  **)
    2.79  
    2.80 -Goalw [union_def,step_def]
    2.81 - "!L R. (start(union L R),q) : step(union L R) a = \
    2.82 +Goalw [or_def,step_def]
    2.83 + "!L R. (start(or L R),q) : step(or L R) a = \
    2.84  \       (? p. (q = True#p & (start L,p) : step L a) | \
    2.85  \             (q = False#p & (start R,p) : step R a))";
    2.86  by (Simp_tac 1);
    2.87  by (Blast_tac 1);
    2.88 -qed_spec_mp "start_step_union";
    2.89 -AddIffs [start_step_union];
    2.90 +qed_spec_mp "start_step_or";
    2.91 +AddIffs [start_step_or];
    2.92  
    2.93  Goal
    2.94 - "(start(union L R), q) : steps (union L R) w = \
    2.95 -\ ( (w = [] & q = start(union L R)) | \
    2.96 + "(start(or L R), q) : steps (or L R) w = \
    2.97 +\ ( (w = [] & q = start(or L R)) | \
    2.98  \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
    2.99  \                     q = False # p & (start R,p) : steps R w)))";
   2.100  by (case_tac "w" 1);
   2.101 @@ -117,23 +117,23 @@
   2.102   by (Blast_tac 1);
   2.103  by (Asm_simp_tac 1);
   2.104  by (Blast_tac 1);
   2.105 -qed "steps_union";
   2.106 +qed "steps_or";
   2.107  
   2.108 -Goalw [union_def]
   2.109 - "!L R. fin (union L R) (start(union L R)) = \
   2.110 +Goalw [or_def]
   2.111 + "!L R. fin (or L R) (start(or L R)) = \
   2.112  \       (fin L (start L) | fin R (start R))";
   2.113  by (Simp_tac 1);
   2.114 -qed_spec_mp "fin_start_union";
   2.115 -AddIffs [fin_start_union];
   2.116 +qed_spec_mp "fin_start_or";
   2.117 +AddIffs [fin_start_or];
   2.118  
   2.119  Goal
   2.120 - "accepts (union L R) w = (accepts L w | accepts R w)";
   2.121 -by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
   2.122 + "accepts (or L R) w = (accepts L w | accepts R w)";
   2.123 +by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_or]) 1);
   2.124  (* get rid of case_tac: *)
   2.125  by (case_tac "w = []" 1);
   2.126  by (Auto_tac);
   2.127 -qed "accepts_union";
   2.128 -AddIffs [accepts_union];
   2.129 +qed "accepts_or";
   2.130 +AddIffs [accepts_or];
   2.131  
   2.132  (******************************************************)
   2.133  (*                      conc                        *)
     3.1 --- a/src/HOL/Lex/RegExp2NA.thy	Thu Jan 17 15:06:36 2002 +0100
     3.2 +++ b/src/HOL/Lex/RegExp2NA.thy	Thu Jan 17 19:32:22 2002 +0100
     3.3 @@ -20,8 +20,8 @@
     3.4              %b s. if s=[True] & b=a then {[False]} else {},
     3.5              %s. s=[False])"
     3.6  
     3.7 - union :: 'a bitsNA => 'a bitsNA => 'a bitsNA
     3.8 -"union == %(ql,dl,fl)(qr,dr,fr).
     3.9 + or :: 'a bitsNA => 'a bitsNA => 'a bitsNA
    3.10 +"or == %(ql,dl,fl)(qr,dr,fr).
    3.11     ([],
    3.12      %a s. case s of
    3.13              [] => (True ## dl a ql) Un (False ## dr a qr)
    3.14 @@ -47,14 +47,14 @@
    3.15  "plus == %(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f)"
    3.16  
    3.17   star :: 'a bitsNA => 'a bitsNA
    3.18 -"star A == union epsilon (plus A)"
    3.19 +"star A == or epsilon (plus A)"
    3.20  
    3.21  consts rexp2na :: 'a rexp => 'a bitsNA
    3.22  primrec
    3.23  "rexp2na Empty      = ([], %a s. {}, %s. False)"
    3.24  "rexp2na(Atom a)    = atom a"
    3.25 -"rexp2na(Union r s) = union (rexp2na r) (rexp2na s)"
    3.26 -"rexp2na(Conc r s)  = conc  (rexp2na r) (rexp2na s)"
    3.27 -"rexp2na(Star r)    = star  (rexp2na r)"
    3.28 +"rexp2na(Or r s)    = or   (rexp2na r) (rexp2na s)"
    3.29 +"rexp2na(Conc r s)  = conc (rexp2na r) (rexp2na s)"
    3.30 +"rexp2na(Star r)    = star (rexp2na r)"
    3.31  
    3.32  end
     4.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Thu Jan 17 15:06:36 2002 +0100
     4.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Jan 17 19:32:22 2002 +0100
     4.3 @@ -50,43 +50,43 @@
     4.4  
     4.5  
     4.6  (******************************************************)
     4.7 -(*                      union                         *)
     4.8 +(*                      or                            *)
     4.9  (******************************************************)
    4.10  
    4.11  (***** True/False ueber fin anheben *****)
    4.12  
    4.13 -Goalw [union_def] 
    4.14 - "!L R. fin (union L R) (True#p) = fin L p";
    4.15 +Goalw [or_def] 
    4.16 + "!L R. fin (or L R) (True#p) = fin L p";
    4.17  by (Simp_tac 1);
    4.18 -qed_spec_mp "fin_union_True";
    4.19 +qed_spec_mp "fin_or_True";
    4.20  
    4.21 -Goalw [union_def] 
    4.22 - "!L R. fin (union L R) (False#p) = fin R p";
    4.23 +Goalw [or_def] 
    4.24 + "!L R. fin (or L R) (False#p) = fin R p";
    4.25  by (Simp_tac 1);
    4.26 -qed_spec_mp "fin_union_False";
    4.27 +qed_spec_mp "fin_or_False";
    4.28  
    4.29 -AddIffs [fin_union_True,fin_union_False];
    4.30 +AddIffs [fin_or_True,fin_or_False];
    4.31  
    4.32  (***** True/False ueber step anheben *****)
    4.33  
    4.34 -Goalw [union_def,step_def]
    4.35 -"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    4.36 +Goalw [or_def,step_def]
    4.37 +"!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)";
    4.38  by (Simp_tac 1);
    4.39  by (Blast_tac 1);
    4.40 -qed_spec_mp "True_in_step_union";
    4.41 +qed_spec_mp "True_in_step_or";
    4.42  
    4.43 -Goalw [union_def,step_def]
    4.44 -"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    4.45 +Goalw [or_def,step_def]
    4.46 +"!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)";
    4.47  by (Simp_tac 1);
    4.48  by (Blast_tac 1);
    4.49 -qed_spec_mp "False_in_step_union";
    4.50 +qed_spec_mp "False_in_step_or";
    4.51  
    4.52 -AddIffs [True_in_step_union,False_in_step_union];
    4.53 +AddIffs [True_in_step_or,False_in_step_or];
    4.54  
    4.55  (***** True/False ueber epsclosure anheben *****)
    4.56  
    4.57  Goal
    4.58 - "(tp,tq) : (eps(union L R))^* ==> \
    4.59 + "(tp,tq) : (eps(or L R))^* ==> \
    4.60  \ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
    4.61  by (etac rtrancl_induct 1);
    4.62   by (Blast_tac 1);
    4.63 @@ -96,7 +96,7 @@
    4.64  val lemma1a = result();
    4.65  
    4.66  Goal
    4.67 - "(tp,tq) : (eps(union L R))^* ==> \
    4.68 + "(tp,tq) : (eps(or L R))^* ==> \
    4.69  \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
    4.70  by (etac rtrancl_induct 1);
    4.71   by (Blast_tac 1);
    4.72 @@ -106,48 +106,48 @@
    4.73  val lemma1b = result();
    4.74  
    4.75  Goal
    4.76 - "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
    4.77 + "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(or L R))^*";
    4.78  by (etac rtrancl_induct 1);
    4.79   by (Blast_tac 1);
    4.80  by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
    4.81  val lemma2a = result();
    4.82  
    4.83  Goal
    4.84 - "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
    4.85 + "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(or L R))^*";
    4.86  by (etac rtrancl_induct 1);
    4.87   by (Blast_tac 1);
    4.88  by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
    4.89  val lemma2b = result();
    4.90  
    4.91  Goal
    4.92 - "(True#p,q) : (eps(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
    4.93 + "(True#p,q) : (eps(or L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
    4.94  by (blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
    4.95 -qed "True_epsclosure_union";
    4.96 +qed "True_epsclosure_or";
    4.97  
    4.98  Goal
    4.99 - "(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
   4.100 + "(False#p,q) : (eps(or L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
   4.101  by (blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
   4.102 -qed "False_epsclosure_union";
   4.103 +qed "False_epsclosure_or";
   4.104  
   4.105 -AddIffs [True_epsclosure_union,False_epsclosure_union];
   4.106 +AddIffs [True_epsclosure_or,False_epsclosure_or];
   4.107  
   4.108  (***** True/False ueber steps anheben *****)
   4.109  
   4.110  Goal
   4.111 - "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
   4.112 + "!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)";
   4.113  by (induct_tac "w" 1);
   4.114   by Auto_tac;
   4.115  by (Force_tac 1);
   4.116 -qed_spec_mp "lift_True_over_steps_union";
   4.117 +qed_spec_mp "lift_True_over_steps_or";
   4.118  
   4.119  Goal 
   4.120 - "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
   4.121 + "!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)";
   4.122  by (induct_tac "w" 1);
   4.123   by Auto_tac;
   4.124  by (Force_tac 1);
   4.125 -qed_spec_mp "lift_False_over_steps_union";
   4.126 +qed_spec_mp "lift_False_over_steps_or";
   4.127  
   4.128 -AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
   4.129 +AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
   4.130  
   4.131  
   4.132  (***** Epsilonhuelle des Startzustands  *****)
   4.133 @@ -169,26 +169,26 @@
   4.134  by (Blast_tac 1);
   4.135  qed "in_unfold_rtrancl2";
   4.136  
   4.137 -val epsclosure_start_step_union =
   4.138 -  read_instantiate [("p","start(union L R)")] in_unfold_rtrancl2;
   4.139 -AddIffs [epsclosure_start_step_union];
   4.140 +val epsclosure_start_step_or =
   4.141 +  read_instantiate [("p","start(or L R)")] in_unfold_rtrancl2;
   4.142 +AddIffs [epsclosure_start_step_or];
   4.143  
   4.144 -Goalw [union_def,step_def]
   4.145 - "!L R. (start(union L R),q) : eps(union L R) = \
   4.146 +Goalw [or_def,step_def]
   4.147 + "!L R. (start(or L R),q) : eps(or L R) = \
   4.148  \       (q = True#start L | q = False#start R)";
   4.149  by (Simp_tac 1);
   4.150 -qed_spec_mp "start_eps_union";
   4.151 -AddIffs [start_eps_union];
   4.152 +qed_spec_mp "start_eps_or";
   4.153 +AddIffs [start_eps_or];
   4.154  
   4.155 -Goalw [union_def,step_def]
   4.156 - "!L R. (start(union L R),q) ~: step (union L R) (Some a)";
   4.157 +Goalw [or_def,step_def]
   4.158 + "!L R. (start(or L R),q) ~: step (or L R) (Some a)";
   4.159  by (Simp_tac 1);
   4.160 -qed_spec_mp "not_start_step_union_Some";
   4.161 -AddIffs [not_start_step_union_Some];
   4.162 +qed_spec_mp "not_start_step_or_Some";
   4.163 +AddIffs [not_start_step_or_Some];
   4.164  
   4.165  Goal
   4.166 - "(start(union L R), q) : steps (union L R) w = \
   4.167 -\ ( (w = [] & q = start(union L R)) | \
   4.168 + "(start(or L R), q) : steps (or L R) w = \
   4.169 +\ ( (w = [] & q = start(or L R)) | \
   4.170  \   (? p.  q = True  # p & (start L,p) : steps L w | \
   4.171  \          q = False # p & (start R,p) : steps R w) )";
   4.172  by (case_tac "w" 1);
   4.173 @@ -196,23 +196,23 @@
   4.174   by (Blast_tac 1);
   4.175  by (Asm_simp_tac 1);
   4.176  by (Blast_tac 1);
   4.177 -qed "steps_union";
   4.178 +qed "steps_or";
   4.179  
   4.180 -Goalw [union_def]
   4.181 - "!L R. ~ fin (union L R) (start(union L R))";
   4.182 +Goalw [or_def]
   4.183 + "!L R. ~ fin (or L R) (start(or L R))";
   4.184  by (Simp_tac 1);
   4.185 -qed_spec_mp "start_union_not_final";
   4.186 -AddIffs [start_union_not_final];
   4.187 +qed_spec_mp "start_or_not_final";
   4.188 +AddIffs [start_or_not_final];
   4.189  
   4.190  Goalw [accepts_def]
   4.191 - "accepts (union L R) w = (accepts L w | accepts R w)";
   4.192 -by (simp_tac (simpset() addsimps [steps_union]) 1);
   4.193 + "accepts (or L R) w = (accepts L w | accepts R w)";
   4.194 +by (simp_tac (simpset() addsimps [steps_or]) 1);
   4.195  by Auto_tac;
   4.196 -qed "accepts_union";
   4.197 +qed "accepts_or";
   4.198  
   4.199  
   4.200  (******************************************************)
   4.201 -(*                      conc                        *)
   4.202 +(*                      conc                          *)
   4.203  (******************************************************)
   4.204  
   4.205  (** True/False in fin **)
   4.206 @@ -624,7 +624,7 @@
   4.207  by (induct_tac "r" 1);
   4.208      by (simp_tac (simpset() addsimps [accepts_def]) 1);
   4.209     by (simp_tac(simpset() addsimps [accepts_atom]) 1);
   4.210 -  by (asm_simp_tac (simpset() addsimps [accepts_union]) 1);
   4.211 +  by (asm_simp_tac (simpset() addsimps [accepts_or]) 1);
   4.212   by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   4.213  by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   4.214  qed "accepts_rexp2nae";
     5.1 --- a/src/HOL/Lex/RegExp2NAe.thy	Thu Jan 17 15:06:36 2002 +0100
     5.2 +++ b/src/HOL/Lex/RegExp2NAe.thy	Thu Jan 17 19:32:22 2002 +0100
     5.3 @@ -20,8 +20,8 @@
     5.4              %b s. if s=[True] & b=Some a then {[False]} else {},
     5.5              %s. s=[False])"
     5.6  
     5.7 - union :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
     5.8 -"union == %(ql,dl,fl)(qr,dr,fr).
     5.9 + or :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
    5.10 +"or == %(ql,dl,fl)(qr,dr,fr).
    5.11     ([],
    5.12      %a s. case s of
    5.13              [] => if a=None then {True#ql,False#qr} else {}
    5.14 @@ -53,8 +53,8 @@
    5.15  primrec
    5.16  "rexp2nae Empty      = ([], %a s. {}, %s. False)"
    5.17  "rexp2nae(Atom a)    = atom a"
    5.18 -"rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
    5.19 -"rexp2nae(Conc r s)  = conc  (rexp2nae r) (rexp2nae s)"
    5.20 -"rexp2nae(Star r)    = star  (rexp2nae r)"
    5.21 +"rexp2nae(Or r s)    = or   (rexp2nae r) (rexp2nae s)"
    5.22 +"rexp2nae(Conc r s)  = conc (rexp2nae r) (rexp2nae s)"
    5.23 +"rexp2nae(Star r)    = star (rexp2nae r)"
    5.24  
    5.25  end
     6.1 --- a/src/HOL/Lex/Scanner.thy	Thu Jan 17 15:06:36 2002 +0100
     6.2 +++ b/src/HOL/Lex/Scanner.thy	Thu Jan 17 19:32:22 2002 +0100
     6.3 @@ -4,4 +4,36 @@
     6.4      Copyright   1998 TUM
     6.5  *)
     6.6  
     6.7 -Scanner = Automata + RegExp2NA + RegExp2NAe
     6.8 +theory Scanner = Automata + RegExp2NA + RegExp2NAe:
     6.9 +
    6.10 +theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)"
    6.11 +by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na)
    6.12 +
    6.13 +theorem  "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"
    6.14 +by (simp add: NAe_DA_equiv accepts_rexp2nae)
    6.15 +
    6.16 +(* Testing code generation: *)
    6.17 +
    6.18 +types_code
    6.19 +  set ("_ list")
    6.20 +
    6.21 +consts_code
    6.22 +  "{}"     ("[]")
    6.23 +  "insert" ("(_ ins _)")
    6.24 +  "op :"   ("(_ mem _)")
    6.25 +  "op Un"  ("(_ union _)")
    6.26 +  "image"  ("map")
    6.27 +  "UNION"  ("(fn A => fn f => flat(map f A))")
    6.28 +  "Bex"    ("(fn A => fn f => exists f A)")
    6.29 +
    6.30 +generate_code
    6.31 +  test = "let r0 = Atom(0::nat);
    6.32 +              r1 = Atom(1::nat);
    6.33 +              re = Conc (Star(Or(Conc r1 r1)r0))
    6.34 +                        (Star(Or(Conc r0 r0)r1));
    6.35 +              N = rexp2na re;
    6.36 +              D = na2da N
    6.37 +          in (NA.accepts N [0,1,1,0,0,1], DA.accepts D [0,1,1,0,0,1])"
    6.38 +ML test
    6.39 +
    6.40 +end