8 |
8 |
9 open Commutation; |
9 open Commutation; |
10 |
10 |
11 (*** square ***) |
11 (*** square ***) |
12 |
12 |
13 Goalw [square_def] "!!R. square R S T U ==> square S R U T"; |
13 Goalw [square_def] "square R S T U ==> square S R U T"; |
14 by (Blast_tac 1); |
14 by (Blast_tac 1); |
15 qed "square_sym"; |
15 qed "square_sym"; |
16 |
16 |
17 Goalw [square_def] |
17 Goalw [square_def] |
18 "!!R. [| square R S T U; T <= T' |] ==> square R S T' U"; |
18 "[| square R S T U; T <= T' |] ==> square R S T' U"; |
19 by (Blast_tac 1); |
19 by (Blast_tac 1); |
20 qed "square_subset"; |
20 qed "square_subset"; |
21 |
21 |
22 Goalw [square_def] |
22 Goalw [square_def] |
23 "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)"; |
23 "[| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)"; |
24 by (Blast_tac 1); |
24 by (Blast_tac 1); |
25 qed "square_reflcl"; |
25 qed "square_reflcl"; |
26 |
26 |
27 Goalw [square_def] |
27 Goalw [square_def] |
28 "!!R. square R S S T ==> square (R^*) S S (T^*)"; |
28 "square R S S T ==> square (R^*) S S (T^*)"; |
29 by (strip_tac 1); |
29 by (strip_tac 1); |
30 by (etac rtrancl_induct 1); |
30 by (etac rtrancl_induct 1); |
31 by (Blast_tac 1); |
31 by (Blast_tac 1); |
32 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1); |
32 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1); |
33 qed "square_rtrancl"; |
33 qed "square_rtrancl"; |
34 |
34 |
35 Goalw [commute_def] |
35 Goalw [commute_def] |
36 "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)"; |
36 "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"; |
37 by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl] |
37 by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl] |
38 addEs [r_into_rtrancl] |
38 addEs [r_into_rtrancl] |
39 addss simpset()) 1); |
39 addss simpset()) 1); |
40 qed "square_rtrancl_reflcl_commute"; |
40 qed "square_rtrancl_reflcl_commute"; |
41 |
41 |
42 (*** commute ***) |
42 (*** commute ***) |
43 |
43 |
44 Goalw [commute_def] "!!R. commute R S ==> commute S R"; |
44 Goalw [commute_def] "commute R S ==> commute S R"; |
45 by (blast_tac (claset() addIs [square_sym]) 1); |
45 by (blast_tac (claset() addIs [square_sym]) 1); |
46 qed "commute_sym"; |
46 qed "commute_sym"; |
47 |
47 |
48 Goalw [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)"; |
48 Goalw [commute_def] "commute R S ==> commute (R^*) (S^*)"; |
49 by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1); |
49 by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1); |
50 qed "commute_rtrancl"; |
50 qed "commute_rtrancl"; |
51 |
51 |
52 Goalw [commute_def,square_def] |
52 Goalw [commute_def,square_def] |
53 "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T"; |
53 "[| commute R T; commute S T |] ==> commute (R Un S) T"; |
54 by (Blast_tac 1); |
54 by (Blast_tac 1); |
55 qed "commute_Un"; |
55 qed "commute_Un"; |
56 |
56 |
57 (*** diamond, confluence and union ***) |
57 (*** diamond, confluence and union ***) |
58 |
58 |
59 Goalw [diamond_def] |
59 Goalw [diamond_def] |
60 "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)"; |
60 "[| diamond R; diamond S; commute R S |] ==> diamond (R Un S)"; |
61 by (REPEAT(ares_tac [commute_Un,commute_sym] 1)); |
61 by (REPEAT(ares_tac [commute_Un,commute_sym] 1)); |
62 qed "diamond_Un"; |
62 qed "diamond_Un"; |
63 |
63 |
64 Goalw [diamond_def] "!!R. diamond R ==> confluent (R)"; |
64 Goalw [diamond_def] "diamond R ==> confluent (R)"; |
65 by (etac commute_rtrancl 1); |
65 by (etac commute_rtrancl 1); |
66 qed "diamond_confluent"; |
66 qed "diamond_confluent"; |
67 |
67 |
68 Goalw [diamond_def] |
68 Goalw [diamond_def] |
69 "!!R. square R R (R^=) (R^=) ==> confluent R"; |
69 "square R R (R^=) (R^=) ==> confluent R"; |
70 by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl] |
70 by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl] |
71 addEs [square_subset]) 1); |
71 addEs [square_subset]) 1); |
72 qed "square_reflcl_confluent"; |
72 qed "square_reflcl_confluent"; |
73 |
73 |
74 Goal |
74 Goal |
75 "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \ |
75 "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent(R Un S)"; |
76 \ ==> confluent(R Un S)"; |
|
77 by (rtac (rtrancl_Un_rtrancl RS subst) 1); |
76 by (rtac (rtrancl_Un_rtrancl RS subst) 1); |
78 by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1); |
77 by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1); |
79 qed "confluent_Un"; |
78 qed "confluent_Un"; |
80 |
79 |
81 Goal |
80 Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)"; |
82 "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)"; |
|
83 by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] |
81 by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] |
84 addss simpset()) 1); |
82 addss simpset()) 1); |
85 qed "diamond_to_confluence"; |
83 qed "diamond_to_confluence"; |
86 |
84 |
87 (*** Church_Rosser ***) |
85 (*** Church_Rosser ***) |