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 |
|
5117
|
13 |
Goalw [square_def] "square R S T U ==> square S R U T";
|
2897
|
14 |
by (Blast_tac 1);
|
1278
|
15 |
qed "square_sym";
|
|
16 |
|
5069
|
17 |
Goalw [square_def]
|
5117
|
18 |
"[| square R S T U; T <= T' |] ==> square R S T' U";
|
2897
|
19 |
by (Blast_tac 1);
|
1431
|
20 |
qed "square_subset";
|
|
21 |
|
5069
|
22 |
Goalw [square_def]
|
5117
|
23 |
"[| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
|
2897
|
24 |
by (Blast_tac 1);
|
1278
|
25 |
qed "square_reflcl";
|
|
26 |
|
5069
|
27 |
Goalw [square_def]
|
5117
|
28 |
"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);
|
4089
|
32 |
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
|
1278
|
33 |
qed "square_rtrancl";
|
|
34 |
|
5069
|
35 |
Goalw [commute_def]
|
5117
|
36 |
"square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
|
4089
|
37 |
by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl]
|
4474
|
38 |
addEs [r_into_rtrancl]
|
|
39 |
addss simpset()) 1);
|
1278
|
40 |
qed "square_rtrancl_reflcl_commute";
|
|
41 |
|
|
42 |
(*** commute ***)
|
|
43 |
|
5117
|
44 |
Goalw [commute_def] "commute R S ==> commute S R";
|
4089
|
45 |
by (blast_tac (claset() addIs [square_sym]) 1);
|
1278
|
46 |
qed "commute_sym";
|
|
47 |
|
5117
|
48 |
Goalw [commute_def] "commute R S ==> commute (R^*) (S^*)";
|
4089
|
49 |
by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1);
|
1278
|
50 |
qed "commute_rtrancl";
|
|
51 |
|
5069
|
52 |
Goalw [commute_def,square_def]
|
5117
|
53 |
"[| 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 |
|
5069
|
59 |
Goalw [diamond_def]
|
5117
|
60 |
"[| 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 |
|
5117
|
64 |
Goalw [diamond_def] "diamond R ==> confluent (R)";
|
1465
|
65 |
by (etac commute_rtrancl 1);
|
1278
|
66 |
qed "diamond_confluent";
|
|
67 |
|
5069
|
68 |
Goalw [diamond_def]
|
5117
|
69 |
"square R R (R^=) (R^=) ==> confluent R";
|
4089
|
70 |
by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
|
4474
|
71 |
addEs [square_subset]) 1);
|
1431
|
72 |
qed "square_reflcl_confluent";
|
|
73 |
|
5069
|
74 |
Goal
|
5117
|
75 |
"[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent(R Un S)";
|
2031
|
76 |
by (rtac (rtrancl_Un_rtrancl RS subst) 1);
|
4089
|
77 |
by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1);
|
1278
|
78 |
qed "confluent_Un";
|
|
79 |
|
5117
|
80 |
Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
|
8984
|
81 |
by (force_tac (claset() addIs [diamond_confluent]
|
|
82 |
addDs [rtrancl_subset RS sym], simpset()) 1);
|
1278
|
83 |
qed "diamond_to_confluence";
|
|
84 |
|
|
85 |
(*** Church_Rosser ***)
|
|
86 |
|
5069
|
87 |
Goalw [square_def,commute_def,diamond_def,Church_Rosser_def]
|
1278
|
88 |
"Church_Rosser(R) = confluent(R)";
|
2897
|
89 |
by (safe_tac HOL_cs);
|
|
90 |
by (blast_tac (HOL_cs addIs
|
1278
|
91 |
[Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
|
4746
|
92 |
rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
|
1465
|
93 |
by (etac rtrancl_induct 1);
|
2897
|
94 |
by (Blast_tac 1);
|
4474
|
95 |
by (blast_tac (claset() delrules [rtrancl_refl]
|
|
96 |
addIs [r_into_rtrancl, rtrancl_trans]) 1);
|
1278
|
97 |
qed "Church_Rosser_confluent";
|