1(*  Title:      HOL/Proofs/Lambda/Commutation.thy
2    Author:     Tobias Nipkow
3    Copyright   1995  TU Muenchen
4*)
5
6section \<open>Abstract commutation and confluence notions\<close>
7
8theory Commutation
9imports Main
10begin
11
12declare [[syntax_ambiguity_warning = false]]
13
14
15subsection \<open>Basic definitions\<close>
16
17definition
18  square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
19  "square R S T U =
20    (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
21
22definition
23  commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
24  "commute R S = square R S S R"
25
26definition
27  diamond :: "('a => 'a => bool) => bool" where
28  "diamond R = commute R R"
29
30definition
31  Church_Rosser :: "('a => 'a => bool) => bool" where
32  "Church_Rosser R =
33    (\<forall>x y. (sup R (R\<inverse>\<inverse>))\<^sup>*\<^sup>* x y \<longrightarrow> (\<exists>z. R\<^sup>*\<^sup>* x z \<and> R\<^sup>*\<^sup>* y z))"
34
35abbreviation
36  confluent :: "('a => 'a => bool) => bool" where
37  "confluent R == diamond (R\<^sup>*\<^sup>*)"
38
39
40subsection \<open>Basic lemmas\<close>
41
42subsubsection \<open>\<open>square\<close>\<close>
43
44lemma square_sym: "square R S T U ==> square S R U T"
45  apply (unfold square_def)
46  apply blast
47  done
48
49lemma square_subset:
50    "[| square R S T U; T \<le> T' |] ==> square R S T' U"
51  apply (unfold square_def)
52  apply (blast dest: predicate2D)
53  done
54
55lemma square_reflcl:
56    "[| square R S T (R\<^sup>=\<^sup>=); S \<le> T |] ==> square (R\<^sup>=\<^sup>=) S T (R\<^sup>=\<^sup>=)"
57  apply (unfold square_def)
58  apply (blast dest: predicate2D)
59  done
60
61lemma square_rtrancl:
62    "square R S S T ==> square (R\<^sup>*\<^sup>*) S S (T\<^sup>*\<^sup>*)"
63  apply (unfold square_def)
64  apply (intro strip)
65  apply (erule rtranclp_induct)
66   apply blast
67  apply (blast intro: rtranclp.rtrancl_into_rtrancl)
68  done
69
70lemma square_rtrancl_reflcl_commute:
71    "square R S (S\<^sup>*\<^sup>*) (R\<^sup>=\<^sup>=) ==> commute (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*)"
72  apply (unfold commute_def)
73  apply (fastforce dest: square_reflcl square_sym [THEN square_rtrancl])
74  done
75
76
77subsubsection \<open>\<open>commute\<close>\<close>
78
79lemma commute_sym: "commute R S ==> commute S R"
80  apply (unfold commute_def)
81  apply (blast intro: square_sym)
82  done
83
84lemma commute_rtrancl: "commute R S ==> commute (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*)"
85  apply (unfold commute_def)
86  apply (blast intro: square_rtrancl square_sym)
87  done
88
89lemma commute_Un:
90    "[| commute R T; commute S T |] ==> commute (sup R S) T"
91  apply (unfold commute_def square_def)
92  apply blast
93  done
94
95
96subsubsection \<open>\<open>diamond\<close>, \<open>confluence\<close>, and \<open>union\<close>\<close>
97
98lemma diamond_Un:
99    "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
100  apply (unfold diamond_def)
101  apply (blast intro: commute_Un commute_sym) 
102  done
103
104lemma diamond_confluent: "diamond R ==> confluent R"
105  apply (unfold diamond_def)
106  apply (erule commute_rtrancl)
107  done
108
109lemma square_reflcl_confluent:
110    "square R R (R\<^sup>=\<^sup>=) (R\<^sup>=\<^sup>=) ==> confluent R"
111  apply (unfold diamond_def)
112  apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
113  done
114
115lemma confluent_Un:
116    "[| confluent R; confluent S; commute (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*) |] ==> confluent (sup R S)"
117  apply (rule rtranclp_sup_rtranclp [THEN subst])
118  apply (blast dest: diamond_Un intro: diamond_confluent)
119  done
120
121lemma diamond_to_confluence:
122    "[| diamond R; T \<le> R; R \<le> T\<^sup>*\<^sup>* |] ==> confluent T"
123  apply (force intro: diamond_confluent
124    dest: rtranclp_subset [symmetric])
125  done
126
127
128subsection \<open>Church-Rosser\<close>
129
130lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
131  apply (unfold square_def commute_def diamond_def Church_Rosser_def)
132  apply (tactic \<open>safe_tac (put_claset HOL_cs \<^context>)\<close>)
133   apply (tactic \<open>
134     blast_tac (put_claset HOL_cs \<^context> addIs
135       [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
136        @{thm rtranclp_converseI}, @{thm conversepI},
137        @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1\<close>)
138  apply (erule rtranclp_induct)
139   apply blast
140  apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
141  done
142
143
144subsection \<open>Newman's lemma\<close>
145
146text \<open>Proof by Stefan Berghofer\<close>
147
148theorem newman:
149  assumes wf: "wfP (R\<inverse>\<inverse>)"
150  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
151    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
152  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
153    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
154  using wf
155proof induct
156  case (less x b c)
157  have xc: "R\<^sup>*\<^sup>* x c" by fact
158  have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
159  proof (rule converse_rtranclpE)
160    assume "x = b"
161    with xc have "R\<^sup>*\<^sup>* b c" by simp
162    thus ?thesis by iprover
163  next
164    fix y
165    assume xy: "R x y"
166    assume yb: "R\<^sup>*\<^sup>* y b"
167    from xc show ?thesis
168    proof (rule converse_rtranclpE)
169      assume "x = c"
170      with xb have "R\<^sup>*\<^sup>* c b" by simp
171      thus ?thesis by iprover
172    next
173      fix y'
174      assume y'c: "R\<^sup>*\<^sup>* y' c"
175      assume xy': "R x y'"
176      with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
177      then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
178      from xy have "R\<inverse>\<inverse> y x" ..
179      from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
180      then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
181      from xy' have "R\<inverse>\<inverse> y' x" ..
182      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans)
183      moreover note y'c
184      ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
185      then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
186      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans)
187      with cw show ?thesis by iprover
188    qed
189  qed
190qed
191
192text \<open>
193  Alternative version.  Partly automated by Tobias
194  Nipkow. Takes 2 minutes (2002).
195
196  This is the maximal amount of automation possible using \<open>blast\<close>.
197\<close>
198
199theorem newman':
200  assumes wf: "wfP (R\<inverse>\<inverse>)"
201  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
202    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
203  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
204    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
205  using wf
206proof induct
207  case (less x b c)
208  note IH = \<open>\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
209                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d\<close>
210  have xc: "R\<^sup>*\<^sup>* x c" by fact
211  have xb: "R\<^sup>*\<^sup>* x b" by fact
212  thus ?case
213  proof (rule converse_rtranclpE)
214    assume "x = b"
215    with xc have "R\<^sup>*\<^sup>* b c" by simp
216    thus ?thesis by iprover
217  next
218    fix y
219    assume xy: "R x y"
220    assume yb: "R\<^sup>*\<^sup>* y b"
221    from xc show ?thesis
222    proof (rule converse_rtranclpE)
223      assume "x = c"
224      with xb have "R\<^sup>*\<^sup>* c b" by simp
225      thus ?thesis by iprover
226    next
227      fix y'
228      assume y'c: "R\<^sup>*\<^sup>* y' c"
229      assume xy': "R x y'"
230      with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
231        by (blast dest: lc)
232      from yb u y'c show ?thesis
233        by (blast del: rtranclp.rtrancl_refl
234            intro: rtranclp_trans
235            dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
236    qed
237  qed
238qed
239
240text \<open>
241  Using the coherent logic prover, the proof of the induction step
242  is completely automatic.
243\<close>
244
245lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
246  by simp
247
248theorem newman'':
249  assumes wf: "wfP (R\<inverse>\<inverse>)"
250  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
251    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
252  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
253    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
254  using wf
255proof induct
256  case (less x b c)
257  note IH = \<open>\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
258                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d\<close>
259  show ?case
260    by (coherent
261      \<open>R\<^sup>*\<^sup>* x c\<close> \<open>R\<^sup>*\<^sup>* x b\<close>
262      refl [where 'a='a] sym
263      eq_imp_rtranclp
264      r_into_rtranclp [of R]
265      rtranclp_trans
266      lc IH [OF conversepI]
267      converse_rtranclpE)
268qed
269
270end
271