1(*  Title:      ZF/ex/Commutation.thy
2    Author:     Tobias Nipkow & Sidi Ould Ehmety
3    Copyright   1995  TU Muenchen
4
5Commutation theory for proving the Church Rosser theorem.
6*)
7
8theory Commutation imports ZF begin
9
10definition
11  square  :: "[i, i, i, i] => o" where
12  "square(r,s,t,u) ==
13    (\<forall>a b. <a,b> \<in> r \<longrightarrow> (\<forall>c. <a, c> \<in> s \<longrightarrow> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
14
15definition
16  commute :: "[i, i] => o" where
17  "commute(r,s) == square(r,s,s,r)"
18
19definition
20  diamond :: "i=>o" where
21  "diamond(r)   == commute(r, r)"
22
23definition
24  strip :: "i=>o" where
25  "strip(r) == commute(r^*, r)"
26
27definition
28  Church_Rosser :: "i => o" where
29  "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r \<union> converse(r))^* \<longrightarrow>
30                        (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
31
32definition
33  confluent :: "i=>o" where
34  "confluent(r) == diamond(r^*)"
35
36
37lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)"
38  unfolding square_def by blast
39
40lemma square_subset: "[| square(r,s,t,u); t \<subseteq> t' |] ==> square(r,s,t',u)"
41  unfolding square_def by blast
42
43
44lemma square_rtrancl:
45  "square(r,s,s,t) ==> field(s)<=field(t) ==> square(r^*,s,s,t^*)"
46apply (unfold square_def, clarify)
47apply (erule rtrancl_induct)
48apply (blast intro: rtrancl_refl)
49apply (blast intro: rtrancl_into_rtrancl)
50done
51
52(* A special case of square_rtrancl_on *)
53lemma diamond_strip:
54  "diamond(r) ==> strip(r)"
55apply (unfold diamond_def commute_def strip_def)
56apply (rule square_rtrancl, simp_all)
57done
58
59(*** commute ***)
60
61lemma commute_sym: "commute(r,s) ==> commute(s,r)"
62  unfolding commute_def by (blast intro: square_sym)
63
64lemma commute_rtrancl:
65  "commute(r,s) ==> field(r)=field(s) ==> commute(r^*,s^*)"
66apply (unfold commute_def)
67apply (rule square_rtrancl)
68apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
69apply (simp_all add: rtrancl_field)
70done
71
72
73lemma confluentD: "confluent(r) ==> diamond(r^*)"
74by (simp add: confluent_def)
75
76lemma strip_confluent: "strip(r) ==> confluent(r)"
77apply (unfold strip_def confluent_def diamond_def)
78apply (drule commute_rtrancl)
79apply (simp_all add: rtrancl_field)
80done
81
82lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r \<union> s, t)"
83  unfolding commute_def square_def by blast
84
85lemma diamond_Un:
86     "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r \<union> s)"
87  unfolding diamond_def by (blast intro: commute_Un commute_sym)
88
89lemma diamond_confluent:
90    "diamond(r) ==> confluent(r)"
91apply (unfold diamond_def confluent_def)
92apply (erule commute_rtrancl, simp)
93done
94
95lemma confluent_Un:
96 "[| confluent(r); confluent(s); commute(r^*, s^*);
97     relation(r); relation(s) |] ==> confluent(r \<union> s)"
98apply (unfold confluent_def)
99apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
100apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
101done
102
103
104lemma diamond_to_confluence:
105     "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)"
106apply (drule rtrancl_subset [symmetric], assumption)
107apply (simp_all add: confluent_def)
108apply (blast intro: diamond_confluent [THEN confluentD])
109done
110
111
112(*** Church_Rosser ***)
113
114lemma Church_Rosser1:
115     "Church_Rosser(r) ==> confluent(r)"
116apply (unfold confluent_def Church_Rosser_def square_def
117              commute_def diamond_def, auto)
118apply (drule converseI)
119apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
120apply (drule_tac x = b in spec)
121apply (drule_tac x1 = c in spec [THEN mp])
122apply (rule_tac b = a in rtrancl_trans)
123apply (blast intro: rtrancl_mono [THEN subsetD])+
124done
125
126
127lemma Church_Rosser2:
128     "confluent(r) ==> Church_Rosser(r)"
129apply (unfold confluent_def Church_Rosser_def square_def
130              commute_def diamond_def, auto)
131apply (frule fieldI1)
132apply (simp add: rtrancl_field)
133apply (erule rtrancl_induct, auto)
134apply (blast intro: rtrancl_refl)
135apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+
136done
137
138
139lemma Church_Rosser: "Church_Rosser(r) \<longleftrightarrow> confluent(r)"
140  by (blast intro: Church_Rosser1 Church_Rosser2)
141
142end
143