|
1 (* Title: HOL/Lambda/Commutation.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Sidi Ould Ehmety |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 Commutation theory for proving the Church Rosser theorem |
|
7 ported from Isabelle/HOL by Sidi Ould Ehmety |
|
8 *) |
|
9 |
|
10 Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)"; |
|
11 by (Blast_tac 1); |
|
12 qed "square_sym"; |
|
13 |
|
14 |
|
15 Goalw [square_def] "[| square(r,s,t,u); t <= t' |] ==> square(r,s,t',u)"; |
|
16 by (Blast_tac 1); |
|
17 qed "square_subset"; |
|
18 |
|
19 |
|
20 Goalw [square_def] |
|
21 "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)"; |
|
22 by (Clarify_tac 1); |
|
23 by (etac rtrancl_induct 1); |
|
24 by (blast_tac (claset() addIs [rtrancl_refl]) 1); |
|
25 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1); |
|
26 qed_spec_mp "square_rtrancl"; |
|
27 |
|
28 (* A special case of square_rtrancl_on *) |
|
29 Goalw [diamond_def, commute_def, strip_def] |
|
30 "diamond(r) ==> strip(r)"; |
|
31 by (resolve_tac [square_rtrancl] 1); |
|
32 by (ALLGOALS(Asm_simp_tac)); |
|
33 qed "diamond_strip"; |
|
34 |
|
35 (*** commute ***) |
|
36 |
|
37 Goalw [commute_def] |
|
38 "commute(r,s) ==> commute(s,r)"; |
|
39 by (blast_tac (claset() addIs [square_sym]) 1); |
|
40 qed "commute_sym"; |
|
41 |
|
42 Goalw [commute_def] |
|
43 "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)"; |
|
44 by (Clarify_tac 1); |
|
45 by (rtac square_rtrancl 1); |
|
46 by (rtac square_sym 2); |
|
47 by (rtac square_rtrancl 2); |
|
48 by (rtac square_sym 3); |
|
49 by (ALLGOALS(asm_simp_tac |
|
50 (simpset() addsimps [rtrancl_field]))); |
|
51 qed_spec_mp "commute_rtrancl"; |
|
52 |
|
53 |
|
54 Goalw [strip_def,confluent_def, diamond_def] |
|
55 "strip(r) ==> confluent(r)"; |
|
56 by (dtac commute_rtrancl 1); |
|
57 by (ALLGOALS(asm_full_simp_tac (simpset() |
|
58 addsimps [rtrancl_field]))); |
|
59 qed "strip_confluent"; |
|
60 |
|
61 |
|
62 Goalw [commute_def,square_def] |
|
63 "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"; |
|
64 by (Blast_tac 1); |
|
65 qed "commute_Un"; |
|
66 |
|
67 |
|
68 Goalw [diamond_def] |
|
69 "[| diamond(r); diamond(s); commute(r, s) |] \ |
|
70 \ ==> diamond(r Un s)"; |
|
71 by (REPEAT(ares_tac [commute_Un,commute_sym] 1)); |
|
72 qed "diamond_Un"; |
|
73 |
|
74 |
|
75 Goalw [diamond_def,confluent_def] |
|
76 "diamond(r) ==> confluent(r)"; |
|
77 by (etac commute_rtrancl 1); |
|
78 by (Simp_tac 1); |
|
79 qed "diamond_confluent"; |
|
80 |
|
81 |
|
82 Goalw [confluent_def] |
|
83 "[| confluent(r); confluent(s); commute(r^*, s^*); \ |
|
84 \ r<=Sigma(A,B); s<=Sigma(C,D) |] ==> confluent(r Un s)"; |
|
85 by (rtac (rtrancl_Un_rtrancl RS subst) 1); |
|
86 by (blast_tac (claset() addDs [diamond_Un] |
|
87 addIs [rewrite_rule [confluent_def] diamond_confluent]) 3); |
|
88 by Auto_tac; |
|
89 qed "confluent_Un"; |
|
90 |
|
91 |
|
92 Goal |
|
93 "[| diamond(r); s<=r; r<= s^* |] ==> confluent(s)"; |
|
94 by (dresolve_tac [rtrancl_subset RS sym] 1); |
|
95 by (assume_tac 1); |
|
96 by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def]))); |
|
97 by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1); |
|
98 by (Asm_simp_tac 1); |
|
99 qed "diamond_to_confluence"; |
|
100 |
|
101 (*** Church_Rosser ***) |
|
102 |
|
103 Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def] |
|
104 "Church_Rosser(r) ==> confluent(r)"; |
|
105 by Auto_tac; |
|
106 by (dtac converseI 1); |
|
107 by (full_simp_tac (simpset() |
|
108 addsimps [rtrancl_converse RS sym]) 1); |
|
109 by (dres_inst_tac [("x", "b")] spec 1); |
|
110 by (dres_inst_tac [("x1", "c")] (spec RS mp) 1); |
|
111 by (res_inst_tac [("b", "a")] rtrancl_trans 1); |
|
112 by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1)); |
|
113 qed "Church_Rosser1"; |
|
114 |
|
115 |
|
116 Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def] |
|
117 "confluent(r) ==> Church_Rosser(r)"; |
|
118 by Auto_tac; |
|
119 by (forward_tac [fieldI1] 1); |
|
120 by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1); |
|
121 by (etac rtrancl_induct 1); |
|
122 by (ALLGOALS(Clarify_tac)); |
|
123 by (blast_tac (claset() addIs [rtrancl_refl]) 1); |
|
124 by (blast_tac (claset() delrules [rtrancl_refl] |
|
125 addIs [r_into_rtrancl, rtrancl_trans]) 1); |
|
126 qed "Church_Rosser2"; |
|
127 |
|
128 |
|
129 Goal "Church_Rosser(r) <-> confluent(r)"; |
|
130 by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1); |
|
131 qed "Church_Rosser"; |