19 AddSEs par_beta_cases; |
19 AddSEs par_beta_cases; |
20 |
20 |
21 (*** beta <= par_beta <= beta^* ***) |
21 (*** beta <= par_beta <= beta^* ***) |
22 |
22 |
23 goal ParRed.thy "(Var n => t) = (t = Var n)"; |
23 goal ParRed.thy "(Var n => t) = (t = Var n)"; |
24 by (Fast_tac 1); |
24 by (Blast_tac 1); |
25 qed "par_beta_varL"; |
25 qed "par_beta_varL"; |
26 Addsimps [par_beta_varL]; |
26 Addsimps [par_beta_varL]; |
27 |
27 |
28 goal ParRed.thy "t => t"; |
28 goal ParRed.thy "t => t"; |
29 by (dB.induct_tac "t" 1); |
29 by (dB.induct_tac "t" 1); |
34 |
34 |
35 goal ParRed.thy "beta <= par_beta"; |
35 goal ParRed.thy "beta <= par_beta"; |
36 by (rtac subsetI 1); |
36 by (rtac subsetI 1); |
37 by (split_all_tac 1); |
37 by (split_all_tac 1); |
38 by (etac beta.induct 1); |
38 by (etac beta.induct 1); |
39 by (ALLGOALS(fast_tac (!claset addSIs [par_beta_refl]))); |
39 by (ALLGOALS(blast_tac (!claset addSIs [par_beta_refl]))); |
40 qed "beta_subset_par_beta"; |
40 qed "beta_subset_par_beta"; |
41 |
41 |
42 goal ParRed.thy "par_beta <= beta^*"; |
42 goal ParRed.thy "par_beta <= beta^*"; |
43 by (rtac subsetI 1); |
43 by (rtac subsetI 1); |
44 by (split_all_tac 1); |
44 by (split_all_tac 1); |
70 (*** Confluence (directly) ***) |
70 (*** Confluence (directly) ***) |
71 |
71 |
72 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
72 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
73 by (rtac (impI RS allI RS allI) 1); |
73 by (rtac (impI RS allI RS allI) 1); |
74 by (etac par_beta.induct 1); |
74 by (etac par_beta.induct 1); |
75 by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst]))); |
75 by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7)); |
76 qed "diamond_par_beta"; |
76 qed "diamond_par_beta"; |
77 |
77 |
78 |
78 |
79 (*** cd ***) |
79 (*** cd ***) |
80 |
80 |
81 goal ParRed.thy "!t. s => t --> t => cd s"; |
81 goal ParRed.thy "!t. s => t --> t => cd s"; |
82 by (dB.induct_tac "s" 1); |
82 by (dB.induct_tac "s" 1); |
83 by (Simp_tac 1); |
83 by (Simp_tac 1); |
84 by (etac rev_mp 1); |
84 by (etac rev_mp 1); |
85 by (dB.induct_tac "dB1" 1); |
85 by (dB.induct_tac "dB1" 1); |
86 by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset)))); |
86 by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] |
|
87 unsafe_addss (!simpset)))); |
87 qed_spec_mp "par_beta_cd"; |
88 qed_spec_mp "par_beta_cd"; |
88 |
89 |
89 (*** Confluence (via cd) ***) |
90 (*** Confluence (via cd) ***) |
90 |
91 |
91 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
92 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
92 by (fast_tac (HOL_cs addIs [par_beta_cd]) 1); |
93 by (blast_tac (HOL_cs addIs [par_beta_cd]) 1); |
93 qed "diamond_par_beta2"; |
94 qed "diamond_par_beta2"; |
94 |
95 |
95 goal ParRed.thy "confluent(beta)"; |
96 goal ParRed.thy "confluent(beta)"; |
96 by (fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence, |
97 by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence, |
97 par_beta_subset_beta,beta_subset_par_beta]) 1); |
98 par_beta_subset_beta, beta_subset_par_beta]) 1); |
98 qed"beta_confluent"; |
99 qed"beta_confluent"; |