author | paulson |
Fri, 04 Apr 1997 12:21:28 +0200 | |
changeset 2897 | 27dc4862751b |
parent 2057 | 4d7a4b25a11f |
child 2922 | 580647a879cf |
permissions | -rw-r--r-- |
1278 | 1 |
(* Title: HOL/Lambda/Commutation.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
6 |
Basic commutation lemmas. |
|
7 |
*) |
|
8 |
||
9 |
open Commutation; |
|
10 |
||
11 |
(*** square ***) |
|
12 |
||
13 |
goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T"; |
|
2897 | 14 |
by (Blast_tac 1); |
1278 | 15 |
qed "square_sym"; |
16 |
||
17 |
goalw Commutation.thy [square_def] |
|
1431 | 18 |
"!!R. [| square R S T U; T <= T' |] ==> square R S T' U"; |
2897 | 19 |
by (Blast_tac 1); |
1431 | 20 |
qed "square_subset"; |
21 |
||
22 |
goalw Commutation.thy [square_def] |
|
1278 | 23 |
"!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)"; |
2897 | 24 |
by (Blast_tac 1); |
1278 | 25 |
qed "square_reflcl"; |
26 |
||
27 |
goalw Commutation.thy [square_def] |
|
28 |
"!!R. square R S S T ==> square (R^*) S S (T^*)"; |
|
2031 | 29 |
by (strip_tac 1); |
1465 | 30 |
by (etac rtrancl_induct 1); |
2897 | 31 |
by (Blast_tac 1); |
32 |
by (blast_tac (!claset addIs [rtrancl_into_rtrancl]) 1); |
|
1278 | 33 |
qed "square_rtrancl"; |
34 |
||
35 |
goalw Commutation.thy [commute_def] |
|
36 |
"!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)"; |
|
2031 | 37 |
by (fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl] |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1641
diff
changeset
|
38 |
addEs [r_into_rtrancl] |
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1641
diff
changeset
|
39 |
addss !simpset) 1); |
1278 | 40 |
qed "square_rtrancl_reflcl_commute"; |
41 |
||
42 |
(*** commute ***) |
|
43 |
||
44 |
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R"; |
|
2897 | 45 |
by (blast_tac (!claset addIs [square_sym]) 1); |
1278 | 46 |
qed "commute_sym"; |
47 |
||
48 |
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)"; |
|
2897 | 49 |
by (blast_tac (!claset addIs [square_rtrancl,square_sym]) 1); |
1278 | 50 |
qed "commute_rtrancl"; |
51 |
||
52 |
goalw Commutation.thy [commute_def,square_def] |
|
53 |
"!!R. [| commute R T; commute S T |] ==> commute (R Un S) T"; |
|
2897 | 54 |
by (Blast_tac 1); |
1278 | 55 |
qed "commute_Un"; |
56 |
||
57 |
(*** diamond, confluence and union ***) |
|
58 |
||
59 |
goalw Commutation.thy [diamond_def] |
|
60 |
"!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)"; |
|
2031 | 61 |
by (REPEAT(ares_tac [commute_Un,commute_sym] 1)); |
1278 | 62 |
qed "diamond_Un"; |
63 |
||
64 |
goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)"; |
|
1465 | 65 |
by (etac commute_rtrancl 1); |
1278 | 66 |
qed "diamond_confluent"; |
67 |
||
1431 | 68 |
goalw Commutation.thy [diamond_def] |
69 |
"!!R. square R R (R^=) (R^=) ==> confluent R"; |
|
2897 | 70 |
by (fast_tac (!claset addIs [square_rtrancl_reflcl_commute, r_into_rtrancl] |
71 |
addEs [square_subset]) 1); |
|
1431 | 72 |
qed "square_reflcl_confluent"; |
73 |
||
1278 | 74 |
goal Commutation.thy |
75 |
"!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \ |
|
76 |
\ ==> confluent(R Un S)"; |
|
2031 | 77 |
by (rtac (rtrancl_Un_rtrancl RS subst) 1); |
2897 | 78 |
by (blast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1); |
1278 | 79 |
qed "confluent_Un"; |
80 |
||
81 |
goal Commutation.thy |
|
82 |
"!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)"; |
|
2031 | 83 |
by (fast_tac (!claset addIs [diamond_confluent] |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1641
diff
changeset
|
84 |
addDs [rtrancl_subset RS sym] addss !simpset) 1); |
1278 | 85 |
qed "diamond_to_confluence"; |
86 |
||
87 |
(*** Church_Rosser ***) |
|
88 |
||
89 |
goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def] |
|
90 |
"Church_Rosser(R) = confluent(R)"; |
|
2897 | 91 |
by (safe_tac HOL_cs); |
92 |
by (blast_tac (HOL_cs addIs |
|
1278 | 93 |
[Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans, |
94 |
rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1); |
|
1465 | 95 |
by (etac rtrancl_induct 1); |
2897 | 96 |
by (Blast_tac 1); |
2031 | 97 |
by (slow_best_tac (!claset addIs [r_into_rtrancl] |
1302 | 98 |
addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1); |
1278 | 99 |
qed "Church_Rosser_confluent"; |