|
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";
|
|
|
14 |
by(fast_tac HOL_cs 1);
|
|
|
15 |
qed "square_sym";
|
|
|
16 |
|
|
|
17 |
goalw Commutation.thy [square_def]
|
|
|
18 |
"!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
|
|
|
19 |
by(fast_tac rel_cs 1);
|
|
|
20 |
qed "square_reflcl";
|
|
|
21 |
|
|
|
22 |
goalw Commutation.thy [square_def]
|
|
|
23 |
"!!R. square R S S T ==> square (R^*) S S (T^*)";
|
|
|
24 |
by(strip_tac 1);
|
|
|
25 |
be rtrancl_induct 1;
|
|
|
26 |
by(fast_tac trancl_cs 1);
|
|
|
27 |
by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
|
|
|
28 |
qed "square_rtrancl";
|
|
|
29 |
|
|
|
30 |
goalw Commutation.thy [commute_def]
|
|
|
31 |
"!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
|
|
|
32 |
bd square_reflcl 1;
|
|
|
33 |
br subsetI 1;
|
|
1302
|
34 |
be r_into_rtrancl 1;
|
|
1278
|
35 |
bd square_sym 1;
|
|
|
36 |
bd square_rtrancl 1;
|
|
|
37 |
by(Asm_full_simp_tac 1);
|
|
|
38 |
bd square_sym 1;
|
|
|
39 |
bd square_rtrancl 1;
|
|
|
40 |
by(Asm_full_simp_tac 1);
|
|
|
41 |
qed "square_rtrancl_reflcl_commute";
|
|
|
42 |
|
|
|
43 |
(*** commute ***)
|
|
|
44 |
|
|
|
45 |
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R";
|
|
|
46 |
by(fast_tac (HOL_cs addIs [square_sym]) 1);
|
|
|
47 |
qed "commute_sym";
|
|
|
48 |
|
|
|
49 |
goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
|
|
|
50 |
by(fast_tac (HOL_cs addIs [square_rtrancl,square_sym]) 1);
|
|
|
51 |
qed "commute_rtrancl";
|
|
|
52 |
|
|
|
53 |
goalw Commutation.thy [commute_def,square_def]
|
|
|
54 |
"!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
|
|
|
55 |
by(fast_tac set_cs 1);
|
|
|
56 |
qed "commute_Un";
|
|
|
57 |
|
|
|
58 |
(*** diamond, confluence and union ***)
|
|
|
59 |
|
|
|
60 |
goalw Commutation.thy [diamond_def]
|
|
|
61 |
"!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
|
|
|
62 |
by(REPEAT(ares_tac [commute_Un,commute_sym] 1));
|
|
|
63 |
qed "diamond_Un";
|
|
|
64 |
|
|
|
65 |
goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)";
|
|
|
66 |
be commute_rtrancl 1;
|
|
|
67 |
qed "diamond_confluent";
|
|
|
68 |
|
|
|
69 |
goal Commutation.thy
|
|
|
70 |
"!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
|
|
|
71 |
\ ==> confluent(R Un S)";
|
|
|
72 |
br(trancl_Un_trancl RS subst) 1;
|
|
|
73 |
by(fast_tac (HOL_cs addDs [diamond_Un] addIs [diamond_confluent]) 1);
|
|
|
74 |
qed "confluent_Un";
|
|
|
75 |
|
|
|
76 |
goal Commutation.thy
|
|
|
77 |
"!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
|
|
|
78 |
by(fast_tac (HOL_cs addIs [diamond_confluent]
|
|
|
79 |
addDs [rtrancl_subset RS sym] addss HOL_ss) 1);
|
|
|
80 |
qed "diamond_to_confluence";
|
|
|
81 |
|
|
|
82 |
(*** Church_Rosser ***)
|
|
|
83 |
|
|
|
84 |
goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def]
|
|
|
85 |
"Church_Rosser(R) = confluent(R)";
|
|
|
86 |
br iffI 1;
|
|
|
87 |
by(fast_tac (HOL_cs addIs
|
|
|
88 |
[Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
|
|
|
89 |
rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
|
|
|
90 |
by(safe_tac HOL_cs);
|
|
|
91 |
be rtrancl_induct 1;
|
|
|
92 |
by(fast_tac trancl_cs 1);
|
|
1302
|
93 |
by(slow_tac (rel_cs addIs [r_into_rtrancl]
|
|
|
94 |
addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
|
|
1278
|
95 |
qed "Church_Rosser_confluent";
|