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