--- a/src/HOL/Lex/RegExp.thy Thu Jan 17 15:06:36 2002 +0100
+++ b/src/HOL/Lex/RegExp.thy Thu Jan 17 19:32:22 2002 +0100
@@ -10,7 +10,7 @@
datatype 'a rexp = Empty
| Atom 'a
- | Union ('a rexp) ('a rexp)
+ | Or ('a rexp) ('a rexp)
| Conc ('a rexp) ('a rexp)
| Star ('a rexp)
@@ -18,7 +18,7 @@
primrec
"lang Empty = {}"
"lang (Atom a) = {[a]}"
-"lang (Union el er) = (lang el) Un (lang er)"
+"lang (Or el er) = (lang el) Un (lang er)"
"lang (Conc el er) = RegSet.conc (lang el) (lang er)"
"lang (Star e) = RegSet.star(lang e)"
--- a/src/HOL/Lex/RegExp2NA.ML Thu Jan 17 15:06:36 2002 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML Thu Jan 17 19:32:22 2002 +0100
@@ -45,71 +45,71 @@
(******************************************************)
-(* union *)
+(* or *)
(******************************************************)
(***** True/False ueber fin anheben *****)
-Goalw [union_def]
- "!L R. fin (union L R) (True#p) = fin L p";
+Goalw [or_def]
+ "!L R. fin (or L R) (True#p) = fin L p";
by (Simp_tac 1);
-qed_spec_mp "fin_union_True";
+qed_spec_mp "fin_or_True";
-Goalw [union_def]
- "!L R. fin (union L R) (False#p) = fin R p";
+Goalw [or_def]
+ "!L R. fin (or L R) (False#p) = fin R p";
by (Simp_tac 1);
-qed_spec_mp "fin_union_False";
+qed_spec_mp "fin_or_False";
-AddIffs [fin_union_True,fin_union_False];
+AddIffs [fin_or_True,fin_or_False];
(***** True/False ueber step anheben *****)
-Goalw [union_def,step_def]
-"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
+Goalw [or_def,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_union";
+qed_spec_mp "True_in_step_or";
-Goalw [union_def,step_def]
-"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
+Goalw [or_def,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_union";
+qed_spec_mp "False_in_step_or";
-AddIffs [True_in_step_union,False_in_step_union];
+AddIffs [True_in_step_or,False_in_step_or];
(***** True/False ueber steps anheben *****)
Goal
- "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
+ "!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_union";
+qed_spec_mp "lift_True_over_steps_or";
Goal
- "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
+ "!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_union";
+qed_spec_mp "lift_False_over_steps_or";
-AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
+AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
(** From the start **)
-Goalw [union_def,step_def]
- "!L R. (start(union L R),q) : step(union L R) a = \
+Goalw [or_def,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_union";
-AddIffs [start_step_union];
+qed_spec_mp "start_step_or";
+AddIffs [start_step_or];
Goal
- "(start(union L R), q) : steps (union L R) w = \
-\ ( (w = [] & q = start(union L R)) | \
+ "(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);
@@ -117,23 +117,23 @@
by (Blast_tac 1);
by (Asm_simp_tac 1);
by (Blast_tac 1);
-qed "steps_union";
+qed "steps_or";
-Goalw [union_def]
- "!L R. fin (union L R) (start(union L R)) = \
+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_union";
-AddIffs [fin_start_union];
+qed_spec_mp "fin_start_or";
+AddIffs [fin_start_or];
Goal
- "accepts (union L R) w = (accepts L w | accepts R w)";
-by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
+ "accepts (or L R) w = (accepts L w | accepts R w)";
+by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_or]) 1);
(* get rid of case_tac: *)
by (case_tac "w = []" 1);
by (Auto_tac);
-qed "accepts_union";
-AddIffs [accepts_union];
+qed "accepts_or";
+AddIffs [accepts_or];
(******************************************************)
(* conc *)
--- a/src/HOL/Lex/RegExp2NA.thy Thu Jan 17 15:06:36 2002 +0100
+++ b/src/HOL/Lex/RegExp2NA.thy Thu Jan 17 19:32:22 2002 +0100
@@ -20,8 +20,8 @@
%b s. if s=[True] & b=a then {[False]} else {},
%s. s=[False])"
- union :: 'a bitsNA => 'a bitsNA => 'a bitsNA
-"union == %(ql,dl,fl)(qr,dr,fr).
+ or :: 'a bitsNA => 'a bitsNA => 'a bitsNA
+"or == %(ql,dl,fl)(qr,dr,fr).
([],
%a s. case s of
[] => (True ## dl a ql) Un (False ## dr a qr)
@@ -47,14 +47,14 @@
"plus == %(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f)"
star :: 'a bitsNA => 'a bitsNA
-"star A == union epsilon (plus A)"
+"star A == or epsilon (plus A)"
consts rexp2na :: 'a rexp => 'a bitsNA
primrec
"rexp2na Empty = ([], %a s. {}, %s. False)"
"rexp2na(Atom a) = atom a"
-"rexp2na(Union r s) = union (rexp2na r) (rexp2na s)"
-"rexp2na(Conc r s) = conc (rexp2na r) (rexp2na s)"
-"rexp2na(Star r) = star (rexp2na r)"
+"rexp2na(Or r s) = or (rexp2na r) (rexp2na s)"
+"rexp2na(Conc r s) = conc (rexp2na r) (rexp2na s)"
+"rexp2na(Star r) = star (rexp2na r)"
end
--- a/src/HOL/Lex/RegExp2NAe.ML Thu Jan 17 15:06:36 2002 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML Thu Jan 17 19:32:22 2002 +0100
@@ -50,43 +50,43 @@
(******************************************************)
-(* union *)
+(* or *)
(******************************************************)
(***** True/False ueber fin anheben *****)
-Goalw [union_def]
- "!L R. fin (union L R) (True#p) = fin L p";
+Goalw [or_def]
+ "!L R. fin (or L R) (True#p) = fin L p";
by (Simp_tac 1);
-qed_spec_mp "fin_union_True";
+qed_spec_mp "fin_or_True";
-Goalw [union_def]
- "!L R. fin (union L R) (False#p) = fin R p";
+Goalw [or_def]
+ "!L R. fin (or L R) (False#p) = fin R p";
by (Simp_tac 1);
-qed_spec_mp "fin_union_False";
+qed_spec_mp "fin_or_False";
-AddIffs [fin_union_True,fin_union_False];
+AddIffs [fin_or_True,fin_or_False];
(***** True/False ueber step anheben *****)
-Goalw [union_def,step_def]
-"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
+Goalw [or_def,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_union";
+qed_spec_mp "True_in_step_or";
-Goalw [union_def,step_def]
-"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
+Goalw [or_def,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_union";
+qed_spec_mp "False_in_step_or";
-AddIffs [True_in_step_union,False_in_step_union];
+AddIffs [True_in_step_or,False_in_step_or];
(***** True/False ueber epsclosure anheben *****)
Goal
- "(tp,tq) : (eps(union L R))^* ==> \
+ "(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);
@@ -96,7 +96,7 @@
val lemma1a = result();
Goal
- "(tp,tq) : (eps(union L R))^* ==> \
+ "(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);
@@ -106,48 +106,48 @@
val lemma1b = result();
Goal
- "(p,q) : (eps L)^* ==> (True#p, True#q) : (eps(union L R))^*";
+ "(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(union L R))^*";
+ "(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(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
+ "(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_union";
+qed "True_epsclosure_or";
Goal
- "(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
+ "(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_union";
+qed "False_epsclosure_or";
-AddIffs [True_epsclosure_union,False_epsclosure_union];
+AddIffs [True_epsclosure_or,False_epsclosure_or];
(***** True/False ueber steps anheben *****)
Goal
- "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
+ "!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_union";
+qed_spec_mp "lift_True_over_steps_or";
Goal
- "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
+ "!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_union";
+qed_spec_mp "lift_False_over_steps_or";
-AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
+AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
(***** Epsilonhuelle des Startzustands *****)
@@ -169,26 +169,26 @@
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];
+val epsclosure_start_step_or =
+ read_instantiate [("p","start(or L R)")] in_unfold_rtrancl2;
+AddIffs [epsclosure_start_step_or];
-Goalw [union_def,step_def]
- "!L R. (start(union L R),q) : eps(union L R) = \
+Goalw [or_def,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_union";
-AddIffs [start_eps_union];
+qed_spec_mp "start_eps_or";
+AddIffs [start_eps_or];
-Goalw [union_def,step_def]
- "!L R. (start(union L R),q) ~: step (union L R) (Some a)";
+Goalw [or_def,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_union_Some";
-AddIffs [not_start_step_union_Some];
+qed_spec_mp "not_start_step_or_Some";
+AddIffs [not_start_step_or_Some];
Goal
- "(start(union L R), q) : steps (union L R) w = \
-\ ( (w = [] & q = start(union L R)) | \
+ "(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);
@@ -196,23 +196,23 @@
by (Blast_tac 1);
by (Asm_simp_tac 1);
by (Blast_tac 1);
-qed "steps_union";
+qed "steps_or";
-Goalw [union_def]
- "!L R. ~ fin (union L R) (start(union L R))";
+Goalw [or_def]
+ "!L R. ~ fin (or L R) (start(or L R))";
by (Simp_tac 1);
-qed_spec_mp "start_union_not_final";
-AddIffs [start_union_not_final];
+qed_spec_mp "start_or_not_final";
+AddIffs [start_or_not_final];
Goalw [accepts_def]
- "accepts (union L R) w = (accepts L w | accepts R w)";
-by (simp_tac (simpset() addsimps [steps_union]) 1);
+ "accepts (or L R) w = (accepts L w | accepts R w)";
+by (simp_tac (simpset() addsimps [steps_or]) 1);
by Auto_tac;
-qed "accepts_union";
+qed "accepts_or";
(******************************************************)
-(* conc *)
+(* conc *)
(******************************************************)
(** True/False in fin **)
@@ -624,7 +624,7 @@
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_or]) 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";
--- a/src/HOL/Lex/RegExp2NAe.thy Thu Jan 17 15:06:36 2002 +0100
+++ b/src/HOL/Lex/RegExp2NAe.thy Thu Jan 17 19:32:22 2002 +0100
@@ -20,8 +20,8 @@
%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).
+ or :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
+"or == %(ql,dl,fl)(qr,dr,fr).
([],
%a s. case s of
[] => if a=None then {True#ql,False#qr} else {}
@@ -53,8 +53,8 @@
primrec
"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)"
+"rexp2nae(Or r s) = or (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Conc r s) = conc (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Star r) = star (rexp2nae r)"
end
--- a/src/HOL/Lex/Scanner.thy Thu Jan 17 15:06:36 2002 +0100
+++ b/src/HOL/Lex/Scanner.thy Thu Jan 17 19:32:22 2002 +0100
@@ -4,4 +4,36 @@
Copyright 1998 TUM
*)
-Scanner = Automata + RegExp2NA + RegExp2NAe
+theory Scanner = Automata + RegExp2NA + RegExp2NAe:
+
+theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)"
+by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na)
+
+theorem "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"
+by (simp add: NAe_DA_equiv accepts_rexp2nae)
+
+(* Testing code generation: *)
+
+types_code
+ set ("_ list")
+
+consts_code
+ "{}" ("[]")
+ "insert" ("(_ ins _)")
+ "op :" ("(_ mem _)")
+ "op Un" ("(_ union _)")
+ "image" ("map")
+ "UNION" ("(fn A => fn f => flat(map f A))")
+ "Bex" ("(fn A => fn f => exists f A)")
+
+generate_code
+ test = "let r0 = Atom(0::nat);
+ r1 = Atom(1::nat);
+ re = Conc (Star(Or(Conc r1 r1)r0))
+ (Star(Or(Conc r0 r0)r1));
+ N = rexp2na re;
+ D = na2da N
+ in (NA.accepts N [0,1,1,0,0,1], DA.accepts D [0,1,1,0,0,1])"
+ML test
+
+end