# HG changeset patch # User nipkow # Date 1011292342 -3600 # Node ID b344226f924c717129dc2410a6e42f9c792bcc06 # Parent ccc0f45ad2c438430377fe3ab020206e3326eb9c Added code generation to Scanner.thy Renamed Union -> Or, union -> or diff -r ccc0f45ad2c4 -r b344226f924c src/HOL/Lex/RegExp.thy --- 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)" diff -r ccc0f45ad2c4 -r b344226f924c src/HOL/Lex/RegExp2NA.ML --- 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 *) diff -r ccc0f45ad2c4 -r b344226f924c src/HOL/Lex/RegExp2NA.thy --- 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 diff -r ccc0f45ad2c4 -r b344226f924c src/HOL/Lex/RegExp2NAe.ML --- 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"; diff -r ccc0f45ad2c4 -r b344226f924c src/HOL/Lex/RegExp2NAe.thy --- 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 diff -r ccc0f45ad2c4 -r b344226f924c src/HOL/Lex/Scanner.thy --- 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