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";
