src/HOL/Lex/RegExp2NA.ML
changeset 12792 b344226f924c
parent 12487 bbd564190c9b
child 13145 59bc43b51aa2
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Thu Jan 17 15:06:36 2002 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Thu Jan 17 19:32:22 2002 +0100
     1.3 @@ -45,71 +45,71 @@
     1.4  
     1.5  
     1.6  (******************************************************)
     1.7 -(*                      union                         *)
     1.8 +(*                      or                            *)
     1.9  (******************************************************)
    1.10  
    1.11  (***** True/False ueber fin anheben *****)
    1.12  
    1.13 -Goalw [union_def] 
    1.14 - "!L R. fin (union L R) (True#p) = fin L p";
    1.15 +Goalw [or_def] 
    1.16 + "!L R. fin (or L R) (True#p) = fin L p";
    1.17  by (Simp_tac 1);
    1.18 -qed_spec_mp "fin_union_True";
    1.19 +qed_spec_mp "fin_or_True";
    1.20  
    1.21 -Goalw [union_def] 
    1.22 - "!L R. fin (union L R) (False#p) = fin R p";
    1.23 +Goalw [or_def] 
    1.24 + "!L R. fin (or L R) (False#p) = fin R p";
    1.25  by (Simp_tac 1);
    1.26 -qed_spec_mp "fin_union_False";
    1.27 +qed_spec_mp "fin_or_False";
    1.28  
    1.29 -AddIffs [fin_union_True,fin_union_False];
    1.30 +AddIffs [fin_or_True,fin_or_False];
    1.31  
    1.32  (***** True/False ueber step anheben *****)
    1.33  
    1.34 -Goalw [union_def,step_def]
    1.35 -"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    1.36 +Goalw [or_def,step_def]
    1.37 +"!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)";
    1.38  by (Simp_tac 1);
    1.39  by (Blast_tac 1);
    1.40 -qed_spec_mp "True_in_step_union";
    1.41 +qed_spec_mp "True_in_step_or";
    1.42  
    1.43 -Goalw [union_def,step_def]
    1.44 -"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    1.45 +Goalw [or_def,step_def]
    1.46 +"!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)";
    1.47  by (Simp_tac 1);
    1.48  by (Blast_tac 1);
    1.49 -qed_spec_mp "False_in_step_union";
    1.50 +qed_spec_mp "False_in_step_or";
    1.51  
    1.52 -AddIffs [True_in_step_union,False_in_step_union];
    1.53 +AddIffs [True_in_step_or,False_in_step_or];
    1.54  
    1.55  
    1.56  (***** True/False ueber steps anheben *****)
    1.57  
    1.58  Goal
    1.59 - "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
    1.60 + "!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)";
    1.61  by (induct_tac "w" 1);
    1.62  by (ALLGOALS Force_tac);
    1.63 -qed_spec_mp "lift_True_over_steps_union";
    1.64 +qed_spec_mp "lift_True_over_steps_or";
    1.65  
    1.66  Goal 
    1.67 - "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
    1.68 + "!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)";
    1.69  by (induct_tac "w" 1);
    1.70  by (ALLGOALS Force_tac);
    1.71 -qed_spec_mp "lift_False_over_steps_union";
    1.72 +qed_spec_mp "lift_False_over_steps_or";
    1.73  
    1.74 -AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
    1.75 +AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
    1.76  
    1.77  
    1.78  (** From the start  **)
    1.79  
    1.80 -Goalw [union_def,step_def]
    1.81 - "!L R. (start(union L R),q) : step(union L R) a = \
    1.82 +Goalw [or_def,step_def]
    1.83 + "!L R. (start(or L R),q) : step(or L R) a = \
    1.84  \       (? p. (q = True#p & (start L,p) : step L a) | \
    1.85  \             (q = False#p & (start R,p) : step R a))";
    1.86  by (Simp_tac 1);
    1.87  by (Blast_tac 1);
    1.88 -qed_spec_mp "start_step_union";
    1.89 -AddIffs [start_step_union];
    1.90 +qed_spec_mp "start_step_or";
    1.91 +AddIffs [start_step_or];
    1.92  
    1.93  Goal
    1.94 - "(start(union L R), q) : steps (union L R) w = \
    1.95 -\ ( (w = [] & q = start(union L R)) | \
    1.96 + "(start(or L R), q) : steps (or L R) w = \
    1.97 +\ ( (w = [] & q = start(or L R)) | \
    1.98  \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
    1.99  \                     q = False # p & (start R,p) : steps R w)))";
   1.100  by (case_tac "w" 1);
   1.101 @@ -117,23 +117,23 @@
   1.102   by (Blast_tac 1);
   1.103  by (Asm_simp_tac 1);
   1.104  by (Blast_tac 1);
   1.105 -qed "steps_union";
   1.106 +qed "steps_or";
   1.107  
   1.108 -Goalw [union_def]
   1.109 - "!L R. fin (union L R) (start(union L R)) = \
   1.110 +Goalw [or_def]
   1.111 + "!L R. fin (or L R) (start(or L R)) = \
   1.112  \       (fin L (start L) | fin R (start R))";
   1.113  by (Simp_tac 1);
   1.114 -qed_spec_mp "fin_start_union";
   1.115 -AddIffs [fin_start_union];
   1.116 +qed_spec_mp "fin_start_or";
   1.117 +AddIffs [fin_start_or];
   1.118  
   1.119  Goal
   1.120 - "accepts (union L R) w = (accepts L w | accepts R w)";
   1.121 -by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
   1.122 + "accepts (or L R) w = (accepts L w | accepts R w)";
   1.123 +by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_or]) 1);
   1.124  (* get rid of case_tac: *)
   1.125  by (case_tac "w = []" 1);
   1.126  by (Auto_tac);
   1.127 -qed "accepts_union";
   1.128 -AddIffs [accepts_union];
   1.129 +qed "accepts_or";
   1.130 +AddIffs [accepts_or];
   1.131  
   1.132  (******************************************************)
   1.133  (*                      conc                        *)