37 by (unfold square_def, blast) |
37 by (unfold square_def, blast) |
38 |
38 |
39 |
39 |
40 lemma square_rtrancl [rule_format]: |
40 lemma square_rtrancl [rule_format]: |
41 "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)" |
41 "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)" |
42 apply (unfold square_def) |
42 apply (unfold square_def, clarify) |
43 apply clarify |
|
44 apply (erule rtrancl_induct) |
43 apply (erule rtrancl_induct) |
45 apply (blast intro: rtrancl_refl) |
44 apply (blast intro: rtrancl_refl) |
46 apply (blast intro: rtrancl_into_rtrancl) |
45 apply (blast intro: rtrancl_into_rtrancl) |
47 done |
46 done |
48 |
47 |
49 (* A special case of square_rtrancl_on *) |
48 (* A special case of square_rtrancl_on *) |
50 lemma diamond_strip: |
49 lemma diamond_strip: |
51 "diamond(r) ==> strip(r)" |
50 "diamond(r) ==> strip(r)" |
52 apply (unfold diamond_def commute_def strip_def) |
51 apply (unfold diamond_def commute_def strip_def) |
53 apply (rule square_rtrancl) |
52 apply (rule square_rtrancl, simp_all) |
54 apply simp_all |
|
55 done |
53 done |
56 |
54 |
57 (*** commute ***) |
55 (*** commute ***) |
58 |
56 |
59 lemma commute_sym: |
57 lemma commute_sym: |
60 "commute(r,s) ==> commute(s,r)" |
58 "commute(r,s) ==> commute(s,r)" |
61 by (unfold commute_def, blast intro: square_sym) |
59 by (unfold commute_def, blast intro: square_sym) |
62 |
60 |
63 lemma commute_rtrancl [rule_format]: |
61 lemma commute_rtrancl [rule_format]: |
64 "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)" |
62 "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)" |
65 apply (unfold commute_def) |
63 apply (unfold commute_def, clarify) |
66 apply clarify |
|
67 apply (rule square_rtrancl) |
64 apply (rule square_rtrancl) |
68 apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) |
65 apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) |
69 apply (simp_all add: rtrancl_field) |
66 apply (simp_all add: rtrancl_field) |
70 done |
67 done |
71 |
68 |
87 by (unfold diamond_def, blast intro: commute_Un commute_sym) |
84 by (unfold diamond_def, blast intro: commute_Un commute_sym) |
88 |
85 |
89 lemma diamond_confluent: |
86 lemma diamond_confluent: |
90 "diamond(r) ==> confluent(r)" |
87 "diamond(r) ==> confluent(r)" |
91 apply (unfold diamond_def confluent_def) |
88 apply (unfold diamond_def confluent_def) |
92 apply (erule commute_rtrancl) |
89 apply (erule commute_rtrancl, simp) |
93 apply simp |
|
94 done |
90 done |
95 |
91 |
96 lemma confluent_Un: |
92 lemma confluent_Un: |
97 "[| confluent(r); confluent(s); commute(r^*, s^*); |
93 "[| confluent(r); confluent(s); commute(r^*, s^*); |
98 relation(r); relation(s) |] ==> confluent(r Un s)" |
94 relation(r); relation(s) |] ==> confluent(r Un s)" |
99 apply (unfold confluent_def) |
95 apply (unfold confluent_def) |
100 apply (rule rtrancl_Un_rtrancl [THEN subst]) |
96 apply (rule rtrancl_Un_rtrancl [THEN subst], auto) |
101 apply auto |
|
102 apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD]) |
97 apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD]) |
103 done |
98 done |
104 |
99 |
105 |
100 |
106 lemma diamond_to_confluence: |
101 lemma diamond_to_confluence: |
107 "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)" |
102 "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)" |
108 apply (drule rtrancl_subset [symmetric]) |
103 apply (drule rtrancl_subset [symmetric], assumption) |
109 apply assumption |
|
110 apply (simp_all add: confluent_def) |
104 apply (simp_all add: confluent_def) |
111 apply (blast intro: diamond_confluent [THEN confluentD]) |
105 apply (blast intro: diamond_confluent [THEN confluentD]) |
112 done |
106 done |
113 |
107 |
114 |
108 |
115 (*** Church_Rosser ***) |
109 (*** Church_Rosser ***) |
116 |
110 |
117 lemma Church_Rosser1: |
111 lemma Church_Rosser1: |
118 "Church_Rosser(r) ==> confluent(r)" |
112 "Church_Rosser(r) ==> confluent(r)" |
119 apply (unfold confluent_def Church_Rosser_def square_def |
113 apply (unfold confluent_def Church_Rosser_def square_def |
120 commute_def diamond_def) |
114 commute_def diamond_def, auto) |
121 apply auto |
|
122 apply (drule converseI) |
115 apply (drule converseI) |
123 apply (simp (no_asm_use) add: rtrancl_converse [symmetric]) |
116 apply (simp (no_asm_use) add: rtrancl_converse [symmetric]) |
124 apply (drule_tac x = "b" in spec) |
117 apply (drule_tac x = b in spec) |
125 apply (drule_tac x1 = "c" in spec [THEN mp]) |
118 apply (drule_tac x1 = c in spec [THEN mp]) |
126 apply (rule_tac b = "a" in rtrancl_trans) |
119 apply (rule_tac b = a in rtrancl_trans) |
127 apply (blast intro: rtrancl_mono [THEN subsetD])+ |
120 apply (blast intro: rtrancl_mono [THEN subsetD])+ |
128 done |
121 done |
129 |
122 |
130 |
123 |
131 lemma Church_Rosser2: |
124 lemma Church_Rosser2: |
132 "confluent(r) ==> Church_Rosser(r)" |
125 "confluent(r) ==> Church_Rosser(r)" |
133 apply (unfold confluent_def Church_Rosser_def square_def |
126 apply (unfold confluent_def Church_Rosser_def square_def |
134 commute_def diamond_def) |
127 commute_def diamond_def, auto) |
135 apply auto |
|
136 apply (frule fieldI1) |
128 apply (frule fieldI1) |
137 apply (simp add: rtrancl_field) |
129 apply (simp add: rtrancl_field) |
138 apply (erule rtrancl_induct) |
130 apply (erule rtrancl_induct, auto) |
139 apply auto |
|
140 apply (blast intro: rtrancl_refl) |
131 apply (blast intro: rtrancl_refl) |
141 apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+ |
132 apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+ |
142 done |
133 done |
143 |
134 |
144 |
135 |