1(* Title: HOL/Transitive_Closure.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4*) 5 6section \<open>Reflexive and Transitive closure of a relation\<close> 7 8theory Transitive_Closure 9 imports Relation 10 abbrevs "^*" = "\<^sup>*" "\<^sup>*\<^sup>*" 11 and "^+" = "\<^sup>+" "\<^sup>+\<^sup>+" 12 and "^=" = "\<^sup>=" "\<^sup>=\<^sup>=" 13begin 14 15ML_file \<open>~~/src/Provers/trancl.ML\<close> 16 17text \<open> 18 \<open>rtrancl\<close> is reflexive/transitive closure, 19 \<open>trancl\<close> is transitive closure, 20 \<open>reflcl\<close> is reflexive closure. 21 22 These postfix operators have \<^emph>\<open>maximum priority\<close>, forcing their 23 operands to be atomic. 24\<close> 25 26context notes [[inductive_internals]] 27begin 28 29inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999) 30 for r :: "('a \<times> 'a) set" 31 where 32 rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*" 33 | rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*" 34 35inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999) 36 for r :: "('a \<times> 'a) set" 37 where 38 r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+" 39 | trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+" 40 41notation 42 rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and 43 tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) 44 45declare 46 rtrancl_def [nitpick_unfold del] 47 rtranclp_def [nitpick_unfold del] 48 trancl_def [nitpick_unfold del] 49 tranclp_def [nitpick_unfold del] 50 51end 52 53abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999) 54 where "r\<^sup>= \<equiv> r \<union> Id" 55 56abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_\<^sup>=\<^sup>=)" [1000] 1000) 57 where "r\<^sup>=\<^sup>= \<equiv> sup r (=)" 58 59notation (ASCII) 60 rtrancl ("(_^*)" [1000] 999) and 61 trancl ("(_^+)" [1000] 999) and 62 reflcl ("(_^=)" [1000] 999) and 63 rtranclp ("(_^**)" [1000] 1000) and 64 tranclp ("(_^++)" [1000] 1000) and 65 reflclp ("(_^==)" [1000] 1000) 66 67 68subsection \<open>Reflexive closure\<close> 69 70lemma refl_reflcl[simp]: "refl (r\<^sup>=)" 71 by (simp add: refl_on_def) 72 73lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r" 74 by (simp add: antisym_def) 75 76lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)" 77 unfolding trans_def by blast 78 79lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>=" 80 by blast 81 82 83subsection \<open>Reflexive-transitive closure\<close> 84 85lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) (=)) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" 86 by (auto simp: fun_eq_iff) 87 88lemma r_into_rtrancl [intro]: "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>*" 89 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> 90 apply (simp only: split_tupled_all) 91 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) 92 done 93 94lemma r_into_rtranclp [intro]: "r x y \<Longrightarrow> r\<^sup>*\<^sup>* x y" 95 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> 96 by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl]) 97 98lemma rtranclp_mono: "r \<le> s \<Longrightarrow> r\<^sup>*\<^sup>* \<le> s\<^sup>*\<^sup>*" 99 \<comment> \<open>monotonicity of \<open>rtrancl\<close>\<close> 100 apply (rule predicate2I) 101 apply (erule rtranclp.induct) 102 apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+) 103 done 104 105lemma mono_rtranclp[mono]: "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x\<^sup>*\<^sup>* a b \<longrightarrow> y\<^sup>*\<^sup>* a b" 106 using rtranclp_mono[of x y] by auto 107 108lemmas rtrancl_mono = rtranclp_mono [to_set] 109 110theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]: 111 assumes a: "r\<^sup>*\<^sup>* a b" 112 and cases: "P a" "\<And>y z. r\<^sup>*\<^sup>* a y \<Longrightarrow> r y z \<Longrightarrow> P y \<Longrightarrow> P z" 113 shows "P b" 114 using a by (induct x\<equiv>a b) (rule cases)+ 115 116lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set] 117 118lemmas rtranclp_induct2 = 119 rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step] 120 121lemmas rtrancl_induct2 = 122 rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names refl step] 123 124lemma refl_rtrancl: "refl (r\<^sup>*)" 125 unfolding refl_on_def by fast 126 127text \<open>Transitivity of transitive closure.\<close> 128lemma trans_rtrancl: "trans (r\<^sup>*)" 129proof (rule transI) 130 fix x y z 131 assume "(x, y) \<in> r\<^sup>*" 132 assume "(y, z) \<in> r\<^sup>*" 133 then show "(x, z) \<in> r\<^sup>*" 134 proof induct 135 case base 136 show "(x, y) \<in> r\<^sup>*" by fact 137 next 138 case (step u v) 139 from \<open>(x, u) \<in> r\<^sup>*\<close> and \<open>(u, v) \<in> r\<close> 140 show "(x, v) \<in> r\<^sup>*" .. 141 qed 142qed 143 144lemmas rtrancl_trans = trans_rtrancl [THEN transD] 145 146lemma rtranclp_trans: 147 assumes "r\<^sup>*\<^sup>* x y" 148 and "r\<^sup>*\<^sup>* y z" 149 shows "r\<^sup>*\<^sup>* x z" 150 using assms(2,1) by induct iprover+ 151 152lemma rtranclE [cases set: rtrancl]: 153 fixes a b :: 'a 154 assumes major: "(a, b) \<in> r\<^sup>*" 155 obtains 156 (base) "a = b" 157 | (step) y where "(a, y) \<in> r\<^sup>*" and "(y, b) \<in> r" 158 \<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close> 159proof - 160 have "a = b \<or> (\<exists>y. (a, y) \<in> r\<^sup>* \<and> (y, b) \<in> r)" 161 by (rule major [THEN rtrancl_induct]) blast+ 162 then show ?thesis 163 by (auto intro: base step) 164qed 165 166lemma rtrancl_Int_subset: "Id \<subseteq> s \<Longrightarrow> (r\<^sup>* \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>* \<subseteq> s" 167 apply clarify 168 apply (erule rtrancl_induct, auto) 169 done 170 171lemma converse_rtranclp_into_rtranclp: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" 172 by (rule rtranclp_trans) iprover+ 173 174lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] 175 176text \<open>\<^medskip> More \<^term>\<open>r\<^sup>*\<close> equations and inclusions.\<close> 177 178lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" 179 apply (auto intro!: order_antisym) 180 apply (erule rtranclp_induct) 181 apply (rule rtranclp.rtrancl_refl) 182 apply (blast intro: rtranclp_trans) 183 done 184 185lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set] 186 187lemma rtrancl_idemp_self_comp [simp]: "R\<^sup>* O R\<^sup>* = R\<^sup>*" 188 apply (rule set_eqI) 189 apply (simp only: split_tupled_all) 190 apply (blast intro: rtrancl_trans) 191 done 192 193lemma rtrancl_subset_rtrancl: "r \<subseteq> s\<^sup>* \<Longrightarrow> r\<^sup>* \<subseteq> s\<^sup>*" 194by (drule rtrancl_mono, simp) 195 196lemma rtranclp_subset: "R \<le> S \<Longrightarrow> S \<le> R\<^sup>*\<^sup>* \<Longrightarrow> S\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" 197 apply (drule rtranclp_mono) 198 apply (drule rtranclp_mono, simp) 199 done 200 201lemmas rtrancl_subset = rtranclp_subset [to_set] 202 203lemma rtranclp_sup_rtranclp: "(sup (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*))\<^sup>*\<^sup>* = (sup R S)\<^sup>*\<^sup>*" 204 by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D]) 205 206lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set] 207 208lemma rtranclp_reflclp [simp]: "(R\<^sup>=\<^sup>=)\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" 209 by (blast intro!: rtranclp_subset) 210 211lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set] 212 213lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*" 214 by (rule rtrancl_subset [symmetric]) auto 215 216lemma rtranclp_r_diff_Id: "(inf r (\<noteq>))\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" 217 by (rule rtranclp_subset [symmetric]) auto 218 219theorem rtranclp_converseD: 220 assumes "(r\<inverse>\<inverse>)\<^sup>*\<^sup>* x y" 221 shows "r\<^sup>*\<^sup>* y x" 222 using assms by induct (iprover intro: rtranclp_trans dest!: conversepD)+ 223 224lemmas rtrancl_converseD = rtranclp_converseD [to_set] 225 226theorem rtranclp_converseI: 227 assumes "r\<^sup>*\<^sup>* y x" 228 shows "(r\<inverse>\<inverse>)\<^sup>*\<^sup>* x y" 229 using assms by induct (iprover intro: rtranclp_trans conversepI)+ 230 231lemmas rtrancl_converseI = rtranclp_converseI [to_set] 232 233lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" 234 by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) 235 236lemma sym_rtrancl: "sym r \<Longrightarrow> sym (r\<^sup>*)" 237 by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) 238 239theorem converse_rtranclp_induct [consumes 1, case_names base step]: 240 assumes major: "r\<^sup>*\<^sup>* a b" 241 and cases: "P b" "\<And>y z. r y z \<Longrightarrow> r\<^sup>*\<^sup>* z b \<Longrightarrow> P z \<Longrightarrow> P y" 242 shows "P a" 243 using rtranclp_converseI [OF major] 244 by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+ 245 246lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set] 247 248lemmas converse_rtranclp_induct2 = 249 converse_rtranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names refl step] 250 251lemmas converse_rtrancl_induct2 = 252 converse_rtrancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete), 253 consumes 1, case_names refl step] 254 255lemma converse_rtranclpE [consumes 1, case_names base step]: 256 assumes major: "r\<^sup>*\<^sup>* x z" 257 and cases: "x = z \<Longrightarrow> P" "\<And>y. r x y \<Longrightarrow> r\<^sup>*\<^sup>* y z \<Longrightarrow> P" 258 shows P 259proof - 260 have "x = z \<or> (\<exists>y. r x y \<and> r\<^sup>*\<^sup>* y z)" 261 by (rule_tac major [THEN converse_rtranclp_induct]) iprover+ 262 then show ?thesis 263 by (auto intro: cases) 264qed 265 266lemmas converse_rtranclE = converse_rtranclpE [to_set] 267 268lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule] 269 270lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] 271 272lemma r_comp_rtrancl_eq: "r O r\<^sup>* = r\<^sup>* O r" 273 by (blast elim: rtranclE converse_rtranclE 274 intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) 275 276lemma rtrancl_unfold: "r\<^sup>* = Id \<union> r\<^sup>* O r" 277 by (auto intro: rtrancl_into_rtrancl elim: rtranclE) 278 279lemma rtrancl_Un_separatorE: 280 "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (a, x) \<in> P\<^sup>* \<longrightarrow> (x, y) \<in> Q \<longrightarrow> x = y \<Longrightarrow> (a, b) \<in> P\<^sup>*" 281proof (induct rule: rtrancl.induct) 282 case rtrancl_refl 283 then show ?case by blast 284next 285 case rtrancl_into_rtrancl 286 then show ?case by (blast intro: rtrancl_trans) 287qed 288 289lemma rtrancl_Un_separator_converseE: 290 "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (x, b) \<in> P\<^sup>* \<longrightarrow> (y, x) \<in> Q \<longrightarrow> y = x \<Longrightarrow> (a, b) \<in> P\<^sup>*" 291proof (induct rule: converse_rtrancl_induct) 292 case base 293 then show ?case by blast 294next 295 case step 296 then show ?case by (blast intro: rtrancl_trans) 297qed 298 299lemma Image_closed_trancl: 300 assumes "r `` X \<subseteq> X" 301 shows "r\<^sup>* `` X = X" 302proof - 303 from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" 304 by auto 305 have "x \<in> X" if 1: "(y, x) \<in> r\<^sup>*" and 2: "y \<in> X" for x y 306 proof - 307 from 1 show "x \<in> X" 308 proof induct 309 case base 310 show ?case by (fact 2) 311 next 312 case step 313 with ** show ?case by auto 314 qed 315 qed 316 then show ?thesis by auto 317qed 318 319 320subsection \<open>Transitive closure\<close> 321 322lemma trancl_mono: "\<And>p. p \<in> r\<^sup>+ \<Longrightarrow> r \<subseteq> s \<Longrightarrow> p \<in> s\<^sup>+" 323 apply (simp add: split_tupled_all) 324 apply (erule trancl.induct) 325 apply (iprover dest: subsetD)+ 326 done 327 328lemma r_into_trancl': "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>+" 329 by (simp only: split_tupled_all) (erule r_into_trancl) 330 331text \<open>\<^medskip> Conversions between \<open>trancl\<close> and \<open>rtrancl\<close>.\<close> 332 333lemma tranclp_into_rtranclp: "r\<^sup>+\<^sup>+ a b \<Longrightarrow> r\<^sup>*\<^sup>* a b" 334 by (erule tranclp.induct) iprover+ 335 336lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set] 337 338lemma rtranclp_into_tranclp1: 339 assumes "r\<^sup>*\<^sup>* a b" 340 shows "r b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" 341 using assms by (induct arbitrary: c) iprover+ 342 343lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set] 344 345lemma rtranclp_into_tranclp2: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" 346 \<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close> 347 apply (erule rtranclp.cases, iprover) 348 apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1]) 349 apply (simp | rule r_into_rtranclp)+ 350 done 351 352lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set] 353 354text \<open>Nice induction rule for \<open>trancl\<close>\<close> 355lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]: 356 assumes a: "r\<^sup>+\<^sup>+ a b" 357 and cases: "\<And>y. r a y \<Longrightarrow> P y" "\<And>y z. r\<^sup>+\<^sup>+ a y \<Longrightarrow> r y z \<Longrightarrow> P y \<Longrightarrow> P z" 358 shows "P b" 359 using a by (induct x\<equiv>a b) (iprover intro: cases)+ 360 361lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set] 362 363lemmas tranclp_induct2 = 364 tranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names base step] 365 366lemmas trancl_induct2 = 367 trancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete), 368 consumes 1, case_names base step] 369 370lemma tranclp_trans_induct: 371 assumes major: "r\<^sup>+\<^sup>+ x y" 372 and cases: "\<And>x y. r x y \<Longrightarrow> P x y" "\<And>x y z. r\<^sup>+\<^sup>+ x y \<Longrightarrow> P x y \<Longrightarrow> r\<^sup>+\<^sup>+ y z \<Longrightarrow> P y z \<Longrightarrow> P x z" 373 shows "P x y" 374 \<comment> \<open>Another induction rule for trancl, incorporating transitivity\<close> 375 by (iprover intro: major [THEN tranclp_induct] cases) 376 377lemmas trancl_trans_induct = tranclp_trans_induct [to_set] 378 379lemma tranclE [cases set: trancl]: 380 assumes "(a, b) \<in> r\<^sup>+" 381 obtains 382 (base) "(a, b) \<in> r" 383 | (step) c where "(a, c) \<in> r\<^sup>+" and "(c, b) \<in> r" 384 using assms by cases simp_all 385 386lemma trancl_Int_subset: "r \<subseteq> s \<Longrightarrow> (r\<^sup>+ \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>+ \<subseteq> s" 387 apply clarify 388 apply (erule trancl_induct, auto) 389 done 390 391lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r" 392 by (auto intro: trancl_into_trancl elim: tranclE) 393 394text \<open>Transitivity of \<^term>\<open>r\<^sup>+\<close>\<close> 395lemma trans_trancl [simp]: "trans (r\<^sup>+)" 396proof (rule transI) 397 fix x y z 398 assume "(x, y) \<in> r\<^sup>+" 399 assume "(y, z) \<in> r\<^sup>+" 400 then show "(x, z) \<in> r\<^sup>+" 401 proof induct 402 case (base u) 403 from \<open>(x, y) \<in> r\<^sup>+\<close> and \<open>(y, u) \<in> r\<close> 404 show "(x, u) \<in> r\<^sup>+" .. 405 next 406 case (step u v) 407 from \<open>(x, u) \<in> r\<^sup>+\<close> and \<open>(u, v) \<in> r\<close> 408 show "(x, v) \<in> r\<^sup>+" .. 409 qed 410qed 411 412lemmas trancl_trans = trans_trancl [THEN transD] 413 414lemma tranclp_trans: 415 assumes "r\<^sup>+\<^sup>+ x y" 416 and "r\<^sup>+\<^sup>+ y z" 417 shows "r\<^sup>+\<^sup>+ x z" 418 using assms(2,1) by induct iprover+ 419 420lemma trancl_id [simp]: "trans r \<Longrightarrow> r\<^sup>+ = r" 421 apply auto 422 apply (erule trancl_induct, assumption) 423 apply (unfold trans_def, blast) 424 done 425 426lemma rtranclp_tranclp_tranclp: 427 assumes "r\<^sup>*\<^sup>* x y" 428 shows "\<And>z. r\<^sup>+\<^sup>+ y z \<Longrightarrow> r\<^sup>+\<^sup>+ x z" 429 using assms by induct (iprover intro: tranclp_trans)+ 430 431lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set] 432 433lemma tranclp_into_tranclp2: "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" 434 by (erule tranclp_trans [OF tranclp.r_into_trancl]) 435 436lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set] 437 438lemma tranclp_converseI: "(r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y \<Longrightarrow> (r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y" 439 apply (drule conversepD) 440 apply (erule tranclp_induct) 441 apply (iprover intro: conversepI tranclp_trans)+ 442 done 443 444lemmas trancl_converseI = tranclp_converseI [to_set] 445 446lemma tranclp_converseD: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y \<Longrightarrow> (r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y" 447 apply (rule conversepI) 448 apply (erule tranclp_induct) 449 apply (iprover dest: conversepD intro: tranclp_trans)+ 450 done 451 452lemmas trancl_converseD = tranclp_converseD [to_set] 453 454lemma tranclp_converse: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ = (r\<^sup>+\<^sup>+)\<inverse>\<inverse>" 455 by (fastforce simp add: fun_eq_iff intro!: tranclp_converseI dest!: tranclp_converseD) 456 457lemmas trancl_converse = tranclp_converse [to_set] 458 459lemma sym_trancl: "sym r \<Longrightarrow> sym (r\<^sup>+)" 460 by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) 461 462lemma converse_tranclp_induct [consumes 1, case_names base step]: 463 assumes major: "r\<^sup>+\<^sup>+ a b" 464 and cases: "\<And>y. r y b \<Longrightarrow> P y" "\<And>y z. r y z \<Longrightarrow> r\<^sup>+\<^sup>+ z b \<Longrightarrow> P z \<Longrightarrow> P y" 465 shows "P a" 466 apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major]) 467 apply (blast intro: cases) 468 apply (blast intro: assms dest!: tranclp_converseD) 469 done 470 471lemmas converse_trancl_induct = converse_tranclp_induct [to_set] 472 473lemma tranclpD: "R\<^sup>+\<^sup>+ x y \<Longrightarrow> \<exists>z. R x z \<and> R\<^sup>*\<^sup>* z y" 474 apply (erule converse_tranclp_induct, auto) 475 apply (blast intro: rtranclp_trans) 476 done 477 478lemmas tranclD = tranclpD [to_set] 479 480lemma converse_tranclpE: 481 assumes major: "tranclp r x z" 482 and base: "r x z \<Longrightarrow> P" 483 and step: "\<And>y. r x y \<Longrightarrow> tranclp r y z \<Longrightarrow> P" 484 shows P 485proof - 486 from tranclpD [OF major] obtain y where "r x y" and "rtranclp r y z" 487 by iprover 488 from this(2) show P 489 proof (cases rule: rtranclp.cases) 490 case rtrancl_refl 491 with \<open>r x y\<close> base show P 492 by iprover 493 next 494 case rtrancl_into_rtrancl 495 from this have "tranclp r y z" 496 by (iprover intro: rtranclp_into_tranclp1) 497 with \<open>r x y\<close> step show P 498 by iprover 499 qed 500qed 501 502lemmas converse_tranclE = converse_tranclpE [to_set] 503 504lemma tranclD2: "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R" 505 by (blast elim: tranclE intro: trancl_into_rtrancl) 506 507lemma irrefl_tranclI: "r\<inverse> \<inter> r\<^sup>* = {} \<Longrightarrow> (x, x) \<notin> r\<^sup>+" 508 by (blast elim: tranclE dest: trancl_into_rtrancl) 509 510lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y" 511 by (blast dest: r_into_trancl) 512 513lemma trancl_subset_Sigma_aux: "(a, b) \<in> r\<^sup>* \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> a = b \<or> a \<in> A" 514 by (induct rule: rtrancl_induct) auto 515 516lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A \<Longrightarrow> r\<^sup>+ \<subseteq> A \<times> A" 517 apply (clarsimp simp:) 518 apply (erule tranclE) 519 apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ 520 done 521 522lemma reflclp_tranclp [simp]: "(r\<^sup>+\<^sup>+)\<^sup>=\<^sup>= = r\<^sup>*\<^sup>*" 523 apply (safe intro!: order_antisym) 524 apply (erule tranclp_into_rtranclp) 525 apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1) 526 done 527 528lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set] 529 530lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*" 531proof - 532 have "(a, b) \<in> (r\<^sup>=)\<^sup>+ \<Longrightarrow> (a, b) \<in> r\<^sup>*" for a b 533 by (force dest: trancl_into_rtrancl) 534 moreover have "(a, b) \<in> (r\<^sup>=)\<^sup>+" if "(a, b) \<in> r\<^sup>*" for a b 535 using that 536 proof (cases a b rule: rtranclE) 537 case step 538 show ?thesis 539 by (rule rtrancl_into_trancl1) (use step in auto) 540 qed auto 541 ultimately show ?thesis 542 by auto 543qed 544 545lemma rtrancl_trancl_reflcl [code]: "r\<^sup>* = (r\<^sup>+)\<^sup>=" 546 by simp 547 548lemma trancl_empty [simp]: "{}\<^sup>+ = {}" 549 by (auto elim: trancl_induct) 550 551lemma rtrancl_empty [simp]: "{}\<^sup>* = Id" 552 by (rule subst [OF reflcl_trancl]) simp 553 554lemma rtranclpD: "R\<^sup>*\<^sup>* a b \<Longrightarrow> a = b \<or> a \<noteq> b \<and> R\<^sup>+\<^sup>+ a b" 555 by (force simp: reflclp_tranclp [symmetric] simp del: reflclp_tranclp) 556 557lemmas rtranclD = rtranclpD [to_set] 558 559lemma rtrancl_eq_or_trancl: "(x,y) \<in> R\<^sup>* \<longleftrightarrow> x = y \<or> x \<noteq> y \<and> (x, y) \<in> R\<^sup>+" 560 by (fast elim: trancl_into_rtrancl dest: rtranclD) 561 562lemma trancl_unfold_right: "r\<^sup>+ = r\<^sup>* O r" 563 by (auto dest: tranclD2 intro: rtrancl_into_trancl1) 564 565lemma trancl_unfold_left: "r\<^sup>+ = r O r\<^sup>*" 566 by (auto dest: tranclD intro: rtrancl_into_trancl2) 567 568lemma trancl_insert: "(insert (y, x) r)\<^sup>+ = r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}" 569 \<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close> 570proof - 571 have "\<And>a b. (a, b) \<in> (insert (y, x) r)\<^sup>+ \<Longrightarrow> 572 (a, b) \<in> r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}" 573 by (erule trancl_induct) (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)+ 574 moreover have "r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*} \<subseteq> (insert (y, x) r)\<^sup>+" 575 by (blast intro: trancl_mono rtrancl_mono [THEN [2] rev_subsetD] 576 rtrancl_trancl_trancl rtrancl_into_trancl2) 577 ultimately show ?thesis 578 by auto 579qed 580 581lemma trancl_insert2: 582 "(insert (a, b) r)\<^sup>+ = r\<^sup>+ \<union> {(x, y). ((x, a) \<in> r\<^sup>+ \<or> x = a) \<and> ((b, y) \<in> r\<^sup>+ \<or> y = b)}" 583 by (auto simp: trancl_insert rtrancl_eq_or_trancl) 584 585lemma rtrancl_insert: "(insert (a,b) r)\<^sup>* = r\<^sup>* \<union> {(x, y). (x, a) \<in> r\<^sup>* \<and> (b, y) \<in> r\<^sup>*}" 586 using trancl_insert[of a b r] 587 by (simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast 588 589 590text \<open>Simplifying nested closures\<close> 591 592lemma rtrancl_trancl_absorb[simp]: "(R\<^sup>*)\<^sup>+ = R\<^sup>*" 593 by (simp add: trans_rtrancl) 594 595lemma trancl_rtrancl_absorb[simp]: "(R\<^sup>+)\<^sup>* = R\<^sup>*" 596 by (subst reflcl_trancl[symmetric]) simp 597 598lemma rtrancl_reflcl_absorb[simp]: "(R\<^sup>*)\<^sup>= = R\<^sup>*" 599 by auto 600 601 602text \<open>\<open>Domain\<close> and \<open>Range\<close>\<close> 603 604lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV" 605 by blast 606 607lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV" 608 by blast 609 610lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R \<union> S)\<^sup>*" 611 by (rule rtrancl_Un_rtrancl [THEN subst]) fast 612 613lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*" 614 by (blast intro: subsetD [OF rtrancl_Un_subset]) 615 616lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r" 617 by (unfold Domain_unfold) (blast dest: tranclD) 618 619lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r" 620 unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric]) 621 622lemma Not_Domain_rtrancl: 623 assumes "x \<notin> Domain R" shows "(x, y) \<in> R\<^sup>* \<longleftrightarrow> x = y" 624proof - 625have "(x, y) \<in> R\<^sup>* \<Longrightarrow> x = y" 626 by (erule rtrancl_induct) (use assms in auto) 627 then show ?thesis 628 by auto 629qed 630 631lemma trancl_subset_Field2: "r\<^sup>+ \<subseteq> Field r \<times> Field r" 632 apply clarify 633 apply (erule trancl_induct) 634 apply (auto simp: Field_def) 635 done 636 637lemma finite_trancl[simp]: "finite (r\<^sup>+) = finite r" 638proof 639 show "finite (r\<^sup>+) \<Longrightarrow> finite r" 640 by (blast intro: r_into_trancl' finite_subset) 641 show "finite r \<Longrightarrow> finite (r\<^sup>+)" 642 apply (rule trancl_subset_Field2 [THEN finite_subset]) 643 apply (auto simp: finite_Field) 644 done 645qed 646 647lemma finite_rtrancl_Image[simp]: assumes "finite R" "finite A" shows "finite (R\<^sup>* `` A)" 648proof (rule ccontr) 649 assume "infinite (R\<^sup>* `` A)" 650 with assms show False 651 by(simp add: rtrancl_trancl_reflcl Un_Image del: reflcl_trancl) 652qed 653 654text \<open>More about converse \<open>rtrancl\<close> and \<open>trancl\<close>, should 655 be merged with main body.\<close> 656 657lemma single_valued_confluent: 658 assumes "single_valued r" and xy: "(x, y) \<in> r\<^sup>*" and xz: "(x, z) \<in> r\<^sup>*" 659 shows "(y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*" 660 using xy 661proof (induction rule: rtrancl_induct) 662 case base 663 show ?case 664 by (simp add: assms) 665next 666 case (step y z) 667 with xz \<open>single_valued r\<close> show ?case 668 apply (auto simp: elim: converse_rtranclE dest: single_valuedD) 669 apply (blast intro: rtrancl_trans) 670 done 671qed 672 673lemma r_r_into_trancl: "(a, b) \<in> R \<Longrightarrow> (b, c) \<in> R \<Longrightarrow> (a, c) \<in> R\<^sup>+" 674 by (fast intro: trancl_trans) 675 676lemma trancl_into_trancl: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+" 677 by (induct rule: trancl_induct) (fast intro: r_r_into_trancl trancl_trans)+ 678 679lemma tranclp_rtranclp_tranclp: "r\<^sup>+\<^sup>+ a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" 680 apply (drule tranclpD) 681 apply (elim exE conjE) 682 apply (drule rtranclp_trans, assumption) 683 apply (drule (2) rtranclp_into_tranclp2) 684 done 685 686lemma rtranclp_conversep: "r\<inverse>\<inverse>\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*\<inverse>\<inverse>" 687 by(auto simp add: fun_eq_iff intro: rtranclp_converseI rtranclp_converseD) 688 689lemmas symp_rtranclp = sym_rtrancl[to_pred] 690 691lemmas symp_conv_conversep_eq = sym_conv_converse_eq[to_pred] 692 693lemmas rtranclp_tranclp_absorb [simp] = rtrancl_trancl_absorb[to_pred] 694lemmas tranclp_rtranclp_absorb [simp] = trancl_rtrancl_absorb[to_pred] 695lemmas rtranclp_reflclp_absorb [simp] = rtrancl_reflcl_absorb[to_pred] 696 697lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set] 698 699lemmas transitive_closure_trans [trans] = 700 r_r_into_trancl trancl_trans rtrancl_trans 701 trancl.trancl_into_trancl trancl_into_trancl2 702 rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 703 rtrancl_trancl_trancl trancl_rtrancl_trancl 704 705lemmas transitive_closurep_trans' [trans] = 706 tranclp_trans rtranclp_trans 707 tranclp.trancl_into_trancl tranclp_into_tranclp2 708 rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp 709 rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp 710 711declare trancl_into_rtrancl [elim] 712 713subsection \<open>Symmetric closure\<close> 714 715definition symclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 716where "symclp r x y \<longleftrightarrow> r x y \<or> r y x" 717 718lemma symclpI [simp, intro?]: 719 shows symclpI1: "r x y \<Longrightarrow> symclp r x y" 720 and symclpI2: "r y x \<Longrightarrow> symclp r x y" 721by(simp_all add: symclp_def) 722 723lemma symclpE [consumes 1, cases pred]: 724 assumes "symclp r x y" 725 obtains (base) "r x y" | (sym) "r y x" 726using assms by(auto simp add: symclp_def) 727 728lemma symclp_pointfree: "symclp r = sup r r\<inverse>\<inverse>" 729 by(auto simp add: symclp_def fun_eq_iff) 730 731lemma symclp_greater: "r \<le> symclp r" 732 by(simp add: symclp_pointfree) 733 734lemma symclp_conversep [simp]: "symclp r\<inverse>\<inverse> = symclp r" 735 by(simp add: symclp_pointfree sup.commute) 736 737lemma symp_symclp [simp]: "symp (symclp r)" 738 by(auto simp add: symp_def elim: symclpE intro: symclpI) 739 740lemma symp_symclp_eq: "symp r \<Longrightarrow> symclp r = r" 741 by(simp add: symclp_pointfree symp_conv_conversep_eq) 742 743lemma symp_rtranclp_symclp [simp]: "symp (symclp r)\<^sup>*\<^sup>*" 744 by(simp add: symp_rtranclp) 745 746lemma rtranclp_symclp_sym [sym]: "(symclp r)\<^sup>*\<^sup>* x y \<Longrightarrow> (symclp r)\<^sup>*\<^sup>* y x" 747 by(rule sympD[OF symp_rtranclp_symclp]) 748 749lemma symclp_idem [simp]: "symclp (symclp r) = symclp r" 750 by(simp add: symclp_pointfree sup_commute converse_join) 751 752lemma reflp_rtranclp [simp]: "reflp R\<^sup>*\<^sup>*" 753 using refl_rtrancl[to_pred, of R] reflp_refl_eq[of "{(x, y). R\<^sup>*\<^sup>* x y}"] by simp 754 755subsection \<open>The power operation on relations\<close> 756 757text \<open>\<open>R ^^ n = R O \<dots> O R\<close>, the n-fold composition of \<open>R\<close>\<close> 758 759overloading 760 relpow \<equiv> "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 761 relpowp \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" 762begin 763 764primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 765 where 766 "relpow 0 R = Id" 767 | "relpow (Suc n) R = (R ^^ n) O R" 768 769primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" 770 where 771 "relpowp 0 R = HOL.eq" 772 | "relpowp (Suc n) R = (R ^^ n) OO R" 773 774end 775 776lemma relpowp_relpow_eq [pred_set_conv]: 777 "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)" for R :: "'a rel" 778 by (induct n) (simp_all add: relcompp_relcomp_eq) 779 780text \<open>For code generation:\<close> 781 782definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 783 where relpow_code_def [code_abbrev]: "relpow = compow" 784 785definition relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" 786 where relpowp_code_def [code_abbrev]: "relpowp = compow" 787 788lemma [code]: 789 "relpow (Suc n) R = (relpow n R) O R" 790 "relpow 0 R = Id" 791 by (simp_all add: relpow_code_def) 792 793lemma [code]: 794 "relpowp (Suc n) R = (R ^^ n) OO R" 795 "relpowp 0 R = HOL.eq" 796 by (simp_all add: relpowp_code_def) 797 798hide_const (open) relpow 799hide_const (open) relpowp 800 801lemma relpow_1 [simp]: "R ^^ 1 = R" 802 for R :: "('a \<times> 'a) set" 803 by simp 804 805lemma relpowp_1 [simp]: "P ^^ 1 = P" 806 for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 807 by (fact relpow_1 [to_pred]) 808 809lemma relpow_0_I: "(x, x) \<in> R ^^ 0" 810 by simp 811 812lemma relpowp_0_I: "(P ^^ 0) x x" 813 by (fact relpow_0_I [to_pred]) 814 815lemma relpow_Suc_I: "(x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n" 816 by auto 817 818lemma relpowp_Suc_I: "(P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> (P ^^ Suc n) x z" 819 by (fact relpow_Suc_I [to_pred]) 820 821lemma relpow_Suc_I2: "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n" 822 by (induct n arbitrary: z) (simp, fastforce) 823 824lemma relpowp_Suc_I2: "P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> (P ^^ Suc n) x z" 825 by (fact relpow_Suc_I2 [to_pred]) 826 827lemma relpow_0_E: "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" 828 by simp 829 830lemma relpowp_0_E: "(P ^^ 0) x y \<Longrightarrow> (x = y \<Longrightarrow> Q) \<Longrightarrow> Q" 831 by (fact relpow_0_E [to_pred]) 832 833lemma relpow_Suc_E: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P" 834 by auto 835 836lemma relpowp_Suc_E: "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. (P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q" 837 by (fact relpow_Suc_E [to_pred]) 838 839lemma relpow_E: 840 "(x, z) \<in> R ^^ n \<Longrightarrow> 841 (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow> 842 (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P" 843 by (cases n) auto 844 845lemma relpowp_E: 846 "(P ^^ n) x z \<Longrightarrow> 847 (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow> 848 (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q" 849 by (fact relpow_E [to_pred]) 850 851lemma relpow_Suc_D2: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)" 852 by (induct n arbitrary: x z) 853 (blast intro: relpow_0_I relpow_Suc_I elim: relpow_0_E relpow_Suc_E)+ 854 855lemma relpowp_Suc_D2: "(P ^^ Suc n) x z \<Longrightarrow> \<exists>y. P x y \<and> (P ^^ n) y z" 856 by (fact relpow_Suc_D2 [to_pred]) 857 858lemma relpow_Suc_E2: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> P) \<Longrightarrow> P" 859 by (blast dest: relpow_Suc_D2) 860 861lemma relpowp_Suc_E2: "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> Q) \<Longrightarrow> Q" 862 by (fact relpow_Suc_E2 [to_pred]) 863 864lemma relpow_Suc_D2': "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)" 865 by (induct n) (simp_all, blast) 866 867lemma relpowp_Suc_D2': "\<forall>x y z. (P ^^ n) x y \<and> P y z \<longrightarrow> (\<exists>w. P x w \<and> (P ^^ n) w z)" 868 by (fact relpow_Suc_D2' [to_pred]) 869 870lemma relpow_E2: 871 assumes "(x, z) \<in> R ^^ n" "n = 0 \<Longrightarrow> x = z \<Longrightarrow> P" 872 "\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P" 873 shows "P" 874proof (cases n) 875 case 0 876 with assms show ?thesis 877 by simp 878next 879 case (Suc m) 880 with assms relpow_Suc_D2' [of m R] show ?thesis 881 by force 882qed 883 884lemma relpowp_E2: 885 "(P ^^ n) x z \<Longrightarrow> 886 (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow> 887 (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) \<Longrightarrow> Q" 888 by (fact relpow_E2 [to_pred]) 889 890lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n" 891 by (induct n) auto 892 893lemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n" 894 by (fact relpow_add [to_pred]) 895 896lemma relpow_commute: "R O R ^^ n = R ^^ n O R" 897 by (induct n) (simp_all add: O_assoc [symmetric]) 898 899lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P" 900 by (fact relpow_commute [to_pred]) 901 902lemma relpow_empty: "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}" 903 by (cases n) auto 904 905lemma relpowp_bot: "0 < n \<Longrightarrow> (\<bottom> :: 'a \<Rightarrow> 'a \<Rightarrow> bool) ^^ n = \<bottom>" 906 by (fact relpow_empty [to_pred]) 907 908lemma rtrancl_imp_UN_relpow: 909 assumes "p \<in> R\<^sup>*" 910 shows "p \<in> (\<Union>n. R ^^ n)" 911proof (cases p) 912 case (Pair x y) 913 with assms have "(x, y) \<in> R\<^sup>*" by simp 914 then have "(x, y) \<in> (\<Union>n. R ^^ n)" 915 proof induct 916 case base 917 show ?case by (blast intro: relpow_0_I) 918 next 919 case step 920 then show ?case by (blast intro: relpow_Suc_I) 921 qed 922 with Pair show ?thesis by simp 923qed 924 925lemma rtranclp_imp_Sup_relpowp: 926 assumes "(P\<^sup>*\<^sup>*) x y" 927 shows "(\<Squnion>n. P ^^ n) x y" 928 using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp 929 930lemma relpow_imp_rtrancl: 931 assumes "p \<in> R ^^ n" 932 shows "p \<in> R\<^sup>*" 933proof (cases p) 934 case (Pair x y) 935 with assms have "(x, y) \<in> R ^^ n" by simp 936 then have "(x, y) \<in> R\<^sup>*" 937 proof (induct n arbitrary: x y) 938 case 0 939 then show ?case by simp 940 next 941 case Suc 942 then show ?case 943 by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl) 944 qed 945 with Pair show ?thesis by simp 946qed 947 948lemma relpowp_imp_rtranclp: "(P ^^ n) x y \<Longrightarrow> (P\<^sup>*\<^sup>*) x y" 949 using relpow_imp_rtrancl [of "(x, y)", to_pred] by simp 950 951lemma rtrancl_is_UN_relpow: "R\<^sup>* = (\<Union>n. R ^^ n)" 952 by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl) 953 954lemma rtranclp_is_Sup_relpowp: "P\<^sup>*\<^sup>* = (\<Squnion>n. P ^^ n)" 955 using rtrancl_is_UN_relpow [to_pred, of P] by auto 956 957lemma rtrancl_power: "p \<in> R\<^sup>* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)" 958 by (simp add: rtrancl_is_UN_relpow) 959 960lemma rtranclp_power: "(P\<^sup>*\<^sup>*) x y \<longleftrightarrow> (\<exists>n. (P ^^ n) x y)" 961 by (simp add: rtranclp_is_Sup_relpowp) 962 963lemma trancl_power: "p \<in> R\<^sup>+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)" 964proof - 965 have "((a, b) \<in> R\<^sup>+) = (\<exists>n>0. (a, b) \<in> R ^^ n)" for a b 966 proof safe 967 show "(a, b) \<in> R\<^sup>+ \<Longrightarrow> \<exists>n>0. (a, b) \<in> R ^^ n" 968 apply (drule tranclD2) 969 apply (fastforce simp: rtrancl_is_UN_relpow relcomp_unfold) 970 done 971 show "(a, b) \<in> R\<^sup>+" if "n > 0" "(a, b) \<in> R ^^ n" for n 972 proof (cases n) 973 case (Suc m) 974 with that show ?thesis 975 by (auto simp: dest: relpow_imp_rtrancl rtrancl_into_trancl1) 976 qed (use that in auto) 977 qed 978 then show ?thesis 979 by (cases p) auto 980qed 981 982lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)" 983 using trancl_power [to_pred, of P "(x, y)"] by simp 984 985lemma rtrancl_imp_relpow: "p \<in> R\<^sup>* \<Longrightarrow> \<exists>n. p \<in> R ^^ n" 986 by (auto dest: rtrancl_imp_UN_relpow) 987 988lemma rtranclp_imp_relpowp: "(P\<^sup>*\<^sup>*) x y \<Longrightarrow> \<exists>n. (P ^^ n) x y" 989 by (auto dest: rtranclp_imp_Sup_relpowp) 990 991text \<open>By Sternagel/Thiemann:\<close> 992lemma relpow_fun_conv: "(a, b) \<in> R ^^ n \<longleftrightarrow> (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> R))" 993proof (induct n arbitrary: b) 994 case 0 995 show ?case by auto 996next 997 case (Suc n) 998 show ?case 999 proof (simp add: relcomp_unfold Suc) 1000 show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) \<longleftrightarrow> 1001 (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))" 1002 (is "?l = ?r") 1003 proof 1004 assume ?l 1005 then obtain c f 1006 where 1: "f 0 = a" "f n = c" "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R" "(c,b) \<in> R" 1007 by auto 1008 let ?g = "\<lambda> m. if m = Suc n then b else f m" 1009 show ?r by (rule exI[of _ ?g]) (simp add: 1) 1010 next 1011 assume ?r 1012 then obtain f where 1: "f 0 = a" "b = f (Suc n)" "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R" 1013 by auto 1014 show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto) 1015 qed 1016 qed 1017qed 1018 1019lemma relpowp_fun_conv: "(P ^^ n) x y \<longleftrightarrow> (\<exists>f. f 0 = x \<and> f n = y \<and> (\<forall>i<n. P (f i) (f (Suc i))))" 1020 by (fact relpow_fun_conv [to_pred]) 1021 1022lemma relpow_finite_bounded1: 1023 fixes R :: "('a \<times> 'a) set" 1024 assumes "finite R" and "k > 0" 1025 shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" 1026 (is "_ \<subseteq> ?r") 1027proof - 1028 have "(a, b) \<in> R^^(Suc k) \<Longrightarrow> \<exists>n. 0 < n \<and> n \<le> card R \<and> (a, b) \<in> R^^n" for a b k 1029 proof (induct k arbitrary: b) 1030 case 0 1031 then have "R \<noteq> {}" by auto 1032 with card_0_eq[OF \<open>finite R\<close>] have "card R \<ge> Suc 0" by auto 1033 then show ?case using 0 by force 1034 next 1035 case (Suc k) 1036 then obtain a' where "(a, a') \<in> R^^(Suc k)" and "(a', b) \<in> R" 1037 by auto 1038 from Suc(1)[OF \<open>(a, a') \<in> R^^(Suc k)\<close>] obtain n where "n \<le> card R" and "(a, a') \<in> R ^^ n" 1039 by auto 1040 have "(a, b) \<in> R^^(Suc n)" 1041 using \<open>(a, a') \<in> R^^n\<close> and \<open>(a', b)\<in> R\<close> by auto 1042 from \<open>n \<le> card R\<close> consider "n < card R" | "n = card R" by force 1043 then show ?case 1044 proof cases 1045 case 1 1046 then show ?thesis 1047 using \<open>(a, b) \<in> R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast 1048 next 1049 case 2 1050 from \<open>(a, b) \<in> R ^^ (Suc n)\<close> [unfolded relpow_fun_conv] 1051 obtain f where "f 0 = a" and "f (Suc n) = b" 1052 and steps: "\<And>i. i \<le> n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto 1053 let ?p = "\<lambda>i. (f i, f(Suc i))" 1054 let ?N = "{i. i \<le> n}" 1055 have "?p ` ?N \<subseteq> R" 1056 using steps by auto 1057 from card_mono[OF assms(1) this] have "card (?p ` ?N) \<le> card R" . 1058 also have "\<dots> < card ?N" 1059 using \<open>n = card R\<close> by simp 1060 finally have "\<not> inj_on ?p ?N" 1061 by (rule pigeonhole) 1062 then obtain i j where i: "i \<le> n" and j: "j \<le> n" and ij: "i \<noteq> j" and pij: "?p i = ?p j" 1063 by (auto simp: inj_on_def) 1064 let ?i = "min i j" 1065 let ?j = "max i j" 1066 have i: "?i \<le> n" and j: "?j \<le> n" and pij: "?p ?i = ?p ?j" and ij: "?i < ?j" 1067 using i j ij pij unfolding min_def max_def by auto 1068 from i j pij ij obtain i j where i: "i \<le> n" and j: "j \<le> n" and ij: "i < j" 1069 and pij: "?p i = ?p j" 1070 by blast 1071 let ?g = "\<lambda>l. if l \<le> i then f l else f (l + (j - i))" 1072 let ?n = "Suc (n - (j - i))" 1073 have abl: "(a, b) \<in> R ^^ ?n" 1074 unfolding relpow_fun_conv 1075 proof (rule exI[of _ ?g], intro conjI impI allI) 1076 show "?g ?n = b" 1077 using \<open>f(Suc n) = b\<close> j ij by auto 1078 next 1079 fix k 1080 assume "k < ?n" 1081 show "(?g k, ?g (Suc k)) \<in> R" 1082 proof (cases "k < i") 1083 case True 1084 with i have "k \<le> n" 1085 by auto 1086 from steps[OF this] show ?thesis 1087 using True by simp 1088 next 1089 case False 1090 then have "i \<le> k" by auto 1091 show ?thesis 1092 proof (cases "k = i") 1093 case True 1094 then show ?thesis 1095 using ij pij steps[OF i] by simp 1096 next 1097 case False 1098 with \<open>i \<le> k\<close> have "i < k" by auto 1099 then have small: "k + (j - i) \<le> n" 1100 using \<open>k<?n\<close> by arith 1101 show ?thesis 1102 using steps[OF small] \<open>i<k\<close> by auto 1103 qed 1104 qed 1105 qed (simp add: \<open>f 0 = a\<close>) 1106 moreover have "?n \<le> n" 1107 using i j ij by arith 1108 ultimately show ?thesis 1109 using \<open>n = card R\<close> by blast 1110 qed 1111 qed 1112 then show ?thesis 1113 using gr0_implies_Suc[OF \<open>k > 0\<close>] by auto 1114qed 1115 1116lemma relpow_finite_bounded: 1117 fixes R :: "('a \<times> 'a) set" 1118 assumes "finite R" 1119 shows "R^^k \<subseteq> (\<Union>n\<in>{n. n \<le> card R}. R^^n)" 1120 apply (cases k, force) 1121 apply (use relpow_finite_bounded1[OF assms, of k] in auto) 1122 done 1123 1124lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)" 1125 by (fastforce simp: rtrancl_power dest: relpow_finite_bounded) 1126 1127lemma trancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>+ = (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" 1128 apply (auto simp: trancl_power) 1129 apply (auto dest: relpow_finite_bounded1) 1130 done 1131 1132lemma finite_relcomp[simp,intro]: 1133 assumes "finite R" and "finite S" 1134 shows "finite (R O S)" 1135proof- 1136 have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})" 1137 by (force simp: split_def image_constant_conv split: if_splits) 1138 then show ?thesis 1139 using assms by clarsimp 1140qed 1141 1142lemma finite_relpow [simp, intro]: 1143 fixes R :: "('a \<times> 'a) set" 1144 assumes "finite R" 1145 shows "n > 0 \<Longrightarrow> finite (R^^n)" 1146proof (induct n) 1147 case 0 1148 then show ?case by simp 1149next 1150 case (Suc n) 1151 then show ?case by (cases n) (use assms in simp_all) 1152qed 1153 1154lemma single_valued_relpow: 1155 fixes R :: "('a \<times> 'a) set" 1156 shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)" 1157proof (induct n arbitrary: R) 1158 case 0 1159 then show ?case by simp 1160next 1161 case (Suc n) 1162 show ?case 1163 by (rule single_valuedI) 1164 (use Suc in \<open>fast dest: single_valuedD elim: relpow_Suc_E\<close>) 1165qed 1166 1167 1168subsection \<open>Bounded transitive closure\<close> 1169 1170definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 1171 where "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)" 1172 1173lemma ntrancl_Zero [simp, code]: "ntrancl 0 R = R" 1174proof 1175 show "R \<subseteq> ntrancl 0 R" 1176 unfolding ntrancl_def by fastforce 1177 have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" for i 1178 by auto 1179 then show "ntrancl 0 R \<le> R" 1180 unfolding ntrancl_def by auto 1181qed 1182 1183lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)" 1184proof 1185 have "(a, b) \<in> ntrancl n R O (Id \<union> R)" if "(a, b) \<in> ntrancl (Suc n) R" for a b 1186 proof - 1187 from that obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i" 1188 unfolding ntrancl_def by auto 1189 show ?thesis 1190 proof (cases "i = 1") 1191 case True 1192 from this \<open>(a, b) \<in> R ^^ i\<close> show ?thesis 1193 by (auto simp: ntrancl_def) 1194 next 1195 case False 1196 with \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j" 1197 by (cases i) auto 1198 with \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2: "(c, b) \<in> R" 1199 by auto 1200 from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R" 1201 by (fastforce simp: ntrancl_def) 1202 with c2 show ?thesis by fastforce 1203 qed 1204 qed 1205 then show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)" 1206 by auto 1207 show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R" 1208 by (fastforce simp: ntrancl_def) 1209qed 1210 1211lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \<union> r' O r)" 1212 by (auto simp: Let_def) 1213 1214lemma finite_trancl_ntranl: "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R" 1215 by (cases "card R") (auto simp: trancl_finite_eq_relpow relpow_empty ntrancl_def) 1216 1217 1218subsection \<open>Acyclic relations\<close> 1219 1220definition acyclic :: "('a \<times> 'a) set \<Rightarrow> bool" 1221 where "acyclic r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r\<^sup>+)" 1222 1223abbreviation acyclicP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 1224 where "acyclicP r \<equiv> acyclic {(x, y). r x y}" 1225 1226lemma acyclic_irrefl [code]: "acyclic r \<longleftrightarrow> irrefl (r\<^sup>+)" 1227 by (simp add: acyclic_def irrefl_def) 1228 1229lemma acyclicI: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> acyclic r" 1230 by (simp add: acyclic_def) 1231 1232lemma (in preorder) acyclicI_order: 1233 assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a" 1234 shows "acyclic r" 1235proof - 1236 have "f b < f a" if "(a, b) \<in> r\<^sup>+" for a b 1237 using that by induct (auto intro: * less_trans) 1238 then show ?thesis 1239 by (auto intro!: acyclicI) 1240qed 1241 1242lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \<longleftrightarrow> acyclic r \<and> (x, y) \<notin> r\<^sup>*" 1243 by (simp add: acyclic_def trancl_insert) (blast intro: rtrancl_trans) 1244 1245lemma acyclic_converse [iff]: "acyclic (r\<inverse>) \<longleftrightarrow> acyclic r" 1246 by (simp add: acyclic_def trancl_converse) 1247 1248lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] 1249 1250lemma acyclic_impl_antisym_rtrancl: "acyclic r \<Longrightarrow> antisym (r\<^sup>*)" 1251 by (simp add: acyclic_def antisym_def) 1252 (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) 1253 1254(* Other direction: 1255acyclic = no loops 1256antisym = only self loops 1257Goalw [acyclic_def,antisym_def] "antisym( r\<^sup>* ) \<Longrightarrow> acyclic(r - Id) 1258\<Longrightarrow> antisym( r\<^sup>* ) = acyclic(r - Id)"; 1259*) 1260 1261lemma acyclic_subset: "acyclic s \<Longrightarrow> r \<subseteq> s \<Longrightarrow> acyclic r" 1262 unfolding acyclic_def by (blast intro: trancl_mono) 1263 1264 1265subsection \<open>Setup of transitivity reasoner\<close> 1266 1267ML \<open> 1268structure Trancl_Tac = Trancl_Tac 1269( 1270 val r_into_trancl = @{thm trancl.r_into_trancl}; 1271 val trancl_trans = @{thm trancl_trans}; 1272 val rtrancl_refl = @{thm rtrancl.rtrancl_refl}; 1273 val r_into_rtrancl = @{thm r_into_rtrancl}; 1274 val trancl_into_rtrancl = @{thm trancl_into_rtrancl}; 1275 val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl}; 1276 val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; 1277 val rtrancl_trans = @{thm rtrancl_trans}; 1278 1279 fun decomp (\<^const>\<open>Trueprop\<close> $ t) = 1280 let 1281 fun dec (Const (\<^const_name>\<open>Set.member\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b) $ rel) = 1282 let 1283 fun decr (Const (\<^const_name>\<open>rtrancl\<close>, _ ) $ r) = (r,"r*") 1284 | decr (Const (\<^const_name>\<open>trancl\<close>, _ ) $ r) = (r,"r+") 1285 | decr r = (r,"r"); 1286 val (rel,r) = decr (Envir.beta_eta_contract rel); 1287 in SOME (a,b,rel,r) end 1288 | dec _ = NONE 1289 in dec t end 1290 | decomp _ = NONE; 1291); 1292 1293structure Tranclp_Tac = Trancl_Tac 1294( 1295 val r_into_trancl = @{thm tranclp.r_into_trancl}; 1296 val trancl_trans = @{thm tranclp_trans}; 1297 val rtrancl_refl = @{thm rtranclp.rtrancl_refl}; 1298 val r_into_rtrancl = @{thm r_into_rtranclp}; 1299 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; 1300 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; 1301 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; 1302 val rtrancl_trans = @{thm rtranclp_trans}; 1303 1304 fun decomp (\<^const>\<open>Trueprop\<close> $ t) = 1305 let 1306 fun dec (rel $ a $ b) = 1307 let 1308 fun decr (Const (\<^const_name>\<open>rtranclp\<close>, _ ) $ r) = (r,"r*") 1309 | decr (Const (\<^const_name>\<open>tranclp\<close>, _ ) $ r) = (r,"r+") 1310 | decr r = (r,"r"); 1311 val (rel,r) = decr rel; 1312 in SOME (a, b, rel, r) end 1313 | dec _ = NONE 1314 in dec t end 1315 | decomp _ = NONE; 1316); 1317\<close> 1318 1319setup \<open> 1320 map_theory_simpset (fn ctxt => ctxt 1321 addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac) 1322 addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac) 1323 addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac) 1324 addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac)) 1325\<close> 1326 1327lemma transp_rtranclp [simp]: "transp R\<^sup>*\<^sup>*" 1328 by(auto simp add: transp_def) 1329 1330text \<open>Optional methods.\<close> 1331 1332method_setup trancl = 1333 \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\<close> 1334 \<open>simple transitivity reasoner\<close> 1335method_setup rtrancl = 1336 \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\<close> 1337 \<open>simple transitivity reasoner\<close> 1338method_setup tranclp = 1339 \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\<close> 1340 \<open>simple transitivity reasoner (predicate version)\<close> 1341method_setup rtranclp = 1342 \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\<close> 1343 \<open>simple transitivity reasoner (predicate version)\<close> 1344 1345end 1346