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 "~~/src/Provers/trancl.ML" 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 "r\<^sup>*"} 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 "r\<^sup>+"}\<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 686lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set] 687 688lemmas transitive_closure_trans [trans] = 689 r_r_into_trancl trancl_trans rtrancl_trans 690 trancl.trancl_into_trancl trancl_into_trancl2 691 rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 692 rtrancl_trancl_trancl trancl_rtrancl_trancl 693 694lemmas transitive_closurep_trans' [trans] = 695 tranclp_trans rtranclp_trans 696 tranclp.trancl_into_trancl tranclp_into_tranclp2 697 rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp 698 rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp 699 700declare trancl_into_rtrancl [elim] 701 702 703subsection \<open>The power operation on relations\<close> 704 705text \<open>\<open>R ^^ n = R O \<dots> O R\<close>, the n-fold composition of \<open>R\<close>\<close> 706 707overloading 708 relpow \<equiv> "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 709 relpowp \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" 710begin 711 712primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 713 where 714 "relpow 0 R = Id" 715 | "relpow (Suc n) R = (R ^^ n) O R" 716 717primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" 718 where 719 "relpowp 0 R = HOL.eq" 720 | "relpowp (Suc n) R = (R ^^ n) OO R" 721 722end 723 724lemma relpowp_relpow_eq [pred_set_conv]: 725 "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)" for R :: "'a rel" 726 by (induct n) (simp_all add: relcompp_relcomp_eq) 727 728text \<open>For code generation:\<close> 729 730definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 731 where relpow_code_def [code_abbrev]: "relpow = compow" 732 733definition relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" 734 where relpowp_code_def [code_abbrev]: "relpowp = compow" 735 736lemma [code]: 737 "relpow (Suc n) R = (relpow n R) O R" 738 "relpow 0 R = Id" 739 by (simp_all add: relpow_code_def) 740 741lemma [code]: 742 "relpowp (Suc n) R = (R ^^ n) OO R" 743 "relpowp 0 R = HOL.eq" 744 by (simp_all add: relpowp_code_def) 745 746hide_const (open) relpow 747hide_const (open) relpowp 748 749lemma relpow_1 [simp]: "R ^^ 1 = R" 750 for R :: "('a \<times> 'a) set" 751 by simp 752 753lemma relpowp_1 [simp]: "P ^^ 1 = P" 754 for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 755 by (fact relpow_1 [to_pred]) 756 757lemma relpow_0_I: "(x, x) \<in> R ^^ 0" 758 by simp 759 760lemma relpowp_0_I: "(P ^^ 0) x x" 761 by (fact relpow_0_I [to_pred]) 762 763lemma relpow_Suc_I: "(x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n" 764 by auto 765 766lemma relpowp_Suc_I: "(P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> (P ^^ Suc n) x z" 767 by (fact relpow_Suc_I [to_pred]) 768 769lemma relpow_Suc_I2: "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n" 770 by (induct n arbitrary: z) (simp, fastforce) 771 772lemma relpowp_Suc_I2: "P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> (P ^^ Suc n) x z" 773 by (fact relpow_Suc_I2 [to_pred]) 774 775lemma relpow_0_E: "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" 776 by simp 777 778lemma relpowp_0_E: "(P ^^ 0) x y \<Longrightarrow> (x = y \<Longrightarrow> Q) \<Longrightarrow> Q" 779 by (fact relpow_0_E [to_pred]) 780 781lemma 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" 782 by auto 783 784lemma relpowp_Suc_E: "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. (P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q" 785 by (fact relpow_Suc_E [to_pred]) 786 787lemma relpow_E: 788 "(x, z) \<in> R ^^ n \<Longrightarrow> 789 (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow> 790 (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P" 791 by (cases n) auto 792 793lemma relpowp_E: 794 "(P ^^ n) x z \<Longrightarrow> 795 (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow> 796 (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q" 797 by (fact relpow_E [to_pred]) 798 799lemma relpow_Suc_D2: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)" 800 by (induct n arbitrary: x z) 801 (blast intro: relpow_0_I relpow_Suc_I elim: relpow_0_E relpow_Suc_E)+ 802 803lemma relpowp_Suc_D2: "(P ^^ Suc n) x z \<Longrightarrow> \<exists>y. P x y \<and> (P ^^ n) y z" 804 by (fact relpow_Suc_D2 [to_pred]) 805 806lemma 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" 807 by (blast dest: relpow_Suc_D2) 808 809lemma relpowp_Suc_E2: "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> Q) \<Longrightarrow> Q" 810 by (fact relpow_Suc_E2 [to_pred]) 811 812lemma 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)" 813 by (induct n) (simp_all, blast) 814 815lemma 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)" 816 by (fact relpow_Suc_D2' [to_pred]) 817 818lemma relpow_E2: 819 assumes "(x, z) \<in> R ^^ n" "n = 0 \<Longrightarrow> x = z \<Longrightarrow> P" 820 "\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P" 821 shows "P" 822proof (cases n) 823 case 0 824 with assms show ?thesis 825 by simp 826next 827 case (Suc m) 828 with assms relpow_Suc_D2' [of m R] show ?thesis 829 by force 830qed 831 832lemma relpowp_E2: 833 "(P ^^ n) x z \<Longrightarrow> 834 (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow> 835 (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) \<Longrightarrow> Q" 836 by (fact relpow_E2 [to_pred]) 837 838lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n" 839 by (induct n) auto 840 841lemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n" 842 by (fact relpow_add [to_pred]) 843 844lemma relpow_commute: "R O R ^^ n = R ^^ n O R" 845 by (induct n) (simp_all add: O_assoc [symmetric]) 846 847lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P" 848 by (fact relpow_commute [to_pred]) 849 850lemma relpow_empty: "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}" 851 by (cases n) auto 852 853lemma relpowp_bot: "0 < n \<Longrightarrow> (\<bottom> :: 'a \<Rightarrow> 'a \<Rightarrow> bool) ^^ n = \<bottom>" 854 by (fact relpow_empty [to_pred]) 855 856lemma rtrancl_imp_UN_relpow: 857 assumes "p \<in> R\<^sup>*" 858 shows "p \<in> (\<Union>n. R ^^ n)" 859proof (cases p) 860 case (Pair x y) 861 with assms have "(x, y) \<in> R\<^sup>*" by simp 862 then have "(x, y) \<in> (\<Union>n. R ^^ n)" 863 proof induct 864 case base 865 show ?case by (blast intro: relpow_0_I) 866 next 867 case step 868 then show ?case by (blast intro: relpow_Suc_I) 869 qed 870 with Pair show ?thesis by simp 871qed 872 873lemma rtranclp_imp_Sup_relpowp: 874 assumes "(P\<^sup>*\<^sup>*) x y" 875 shows "(\<Squnion>n. P ^^ n) x y" 876 using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp 877 878lemma relpow_imp_rtrancl: 879 assumes "p \<in> R ^^ n" 880 shows "p \<in> R\<^sup>*" 881proof (cases p) 882 case (Pair x y) 883 with assms have "(x, y) \<in> R ^^ n" by simp 884 then have "(x, y) \<in> R\<^sup>*" 885 proof (induct n arbitrary: x y) 886 case 0 887 then show ?case by simp 888 next 889 case Suc 890 then show ?case 891 by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl) 892 qed 893 with Pair show ?thesis by simp 894qed 895 896lemma relpowp_imp_rtranclp: "(P ^^ n) x y \<Longrightarrow> (P\<^sup>*\<^sup>*) x y" 897 using relpow_imp_rtrancl [of "(x, y)", to_pred] by simp 898 899lemma rtrancl_is_UN_relpow: "R\<^sup>* = (\<Union>n. R ^^ n)" 900 by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl) 901 902lemma rtranclp_is_Sup_relpowp: "P\<^sup>*\<^sup>* = (\<Squnion>n. P ^^ n)" 903 using rtrancl_is_UN_relpow [to_pred, of P] by auto 904 905lemma rtrancl_power: "p \<in> R\<^sup>* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)" 906 by (simp add: rtrancl_is_UN_relpow) 907 908lemma rtranclp_power: "(P\<^sup>*\<^sup>*) x y \<longleftrightarrow> (\<exists>n. (P ^^ n) x y)" 909 by (simp add: rtranclp_is_Sup_relpowp) 910 911lemma trancl_power: "p \<in> R\<^sup>+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)" 912proof - 913 have "((a, b) \<in> R\<^sup>+) = (\<exists>n>0. (a, b) \<in> R ^^ n)" for a b 914 proof safe 915 show "(a, b) \<in> R\<^sup>+ \<Longrightarrow> \<exists>n>0. (a, b) \<in> R ^^ n" 916 apply (drule tranclD2) 917 apply (fastforce simp: rtrancl_is_UN_relpow relcomp_unfold) 918 done 919 show "(a, b) \<in> R\<^sup>+" if "n > 0" "(a, b) \<in> R ^^ n" for n 920 proof (cases n) 921 case (Suc m) 922 with that show ?thesis 923 by (auto simp: dest: relpow_imp_rtrancl rtrancl_into_trancl1) 924 qed (use that in auto) 925 qed 926 then show ?thesis 927 by (cases p) auto 928qed 929 930lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)" 931 using trancl_power [to_pred, of P "(x, y)"] by simp 932 933lemma rtrancl_imp_relpow: "p \<in> R\<^sup>* \<Longrightarrow> \<exists>n. p \<in> R ^^ n" 934 by (auto dest: rtrancl_imp_UN_relpow) 935 936lemma rtranclp_imp_relpowp: "(P\<^sup>*\<^sup>*) x y \<Longrightarrow> \<exists>n. (P ^^ n) x y" 937 by (auto dest: rtranclp_imp_Sup_relpowp) 938 939text \<open>By Sternagel/Thiemann:\<close> 940lemma 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))" 941proof (induct n arbitrary: b) 942 case 0 943 show ?case by auto 944next 945 case (Suc n) 946 show ?case 947 proof (simp add: relcomp_unfold Suc) 948 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> 949 (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))" 950 (is "?l = ?r") 951 proof 952 assume ?l 953 then obtain c f 954 where 1: "f 0 = a" "f n = c" "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R" "(c,b) \<in> R" 955 by auto 956 let ?g = "\<lambda> m. if m = Suc n then b else f m" 957 show ?r by (rule exI[of _ ?g]) (simp add: 1) 958 next 959 assume ?r 960 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" 961 by auto 962 show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto) 963 qed 964 qed 965qed 966 967lemma 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))))" 968 by (fact relpow_fun_conv [to_pred]) 969 970lemma relpow_finite_bounded1: 971 fixes R :: "('a \<times> 'a) set" 972 assumes "finite R" and "k > 0" 973 shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" 974 (is "_ \<subseteq> ?r") 975proof - 976 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 977 proof (induct k arbitrary: b) 978 case 0 979 then have "R \<noteq> {}" by auto 980 with card_0_eq[OF \<open>finite R\<close>] have "card R \<ge> Suc 0" by auto 981 then show ?case using 0 by force 982 next 983 case (Suc k) 984 then obtain a' where "(a, a') \<in> R^^(Suc k)" and "(a', b) \<in> R" 985 by auto 986 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" 987 by auto 988 have "(a, b) \<in> R^^(Suc n)" 989 using \<open>(a, a') \<in> R^^n\<close> and \<open>(a', b)\<in> R\<close> by auto 990 from \<open>n \<le> card R\<close> consider "n < card R" | "n = card R" by force 991 then show ?case 992 proof cases 993 case 1 994 then show ?thesis 995 using \<open>(a, b) \<in> R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast 996 next 997 case 2 998 from \<open>(a, b) \<in> R ^^ (Suc n)\<close> [unfolded relpow_fun_conv] 999 obtain f where "f 0 = a" and "f (Suc n) = b" 1000 and steps: "\<And>i. i \<le> n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto 1001 let ?p = "\<lambda>i. (f i, f(Suc i))" 1002 let ?N = "{i. i \<le> n}" 1003 have "?p ` ?N \<subseteq> R" 1004 using steps by auto 1005 from card_mono[OF assms(1) this] have "card (?p ` ?N) \<le> card R" . 1006 also have "\<dots> < card ?N" 1007 using \<open>n = card R\<close> by simp 1008 finally have "\<not> inj_on ?p ?N" 1009 by (rule pigeonhole) 1010 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" 1011 by (auto simp: inj_on_def) 1012 let ?i = "min i j" 1013 let ?j = "max i j" 1014 have i: "?i \<le> n" and j: "?j \<le> n" and pij: "?p ?i = ?p ?j" and ij: "?i < ?j" 1015 using i j ij pij unfolding min_def max_def by auto 1016 from i j pij ij obtain i j where i: "i \<le> n" and j: "j \<le> n" and ij: "i < j" 1017 and pij: "?p i = ?p j" 1018 by blast 1019 let ?g = "\<lambda>l. if l \<le> i then f l else f (l + (j - i))" 1020 let ?n = "Suc (n - (j - i))" 1021 have abl: "(a, b) \<in> R ^^ ?n" 1022 unfolding relpow_fun_conv 1023 proof (rule exI[of _ ?g], intro conjI impI allI) 1024 show "?g ?n = b" 1025 using \<open>f(Suc n) = b\<close> j ij by auto 1026 next 1027 fix k 1028 assume "k < ?n" 1029 show "(?g k, ?g (Suc k)) \<in> R" 1030 proof (cases "k < i") 1031 case True 1032 with i have "k \<le> n" 1033 by auto 1034 from steps[OF this] show ?thesis 1035 using True by simp 1036 next 1037 case False 1038 then have "i \<le> k" by auto 1039 show ?thesis 1040 proof (cases "k = i") 1041 case True 1042 then show ?thesis 1043 using ij pij steps[OF i] by simp 1044 next 1045 case False 1046 with \<open>i \<le> k\<close> have "i < k" by auto 1047 then have small: "k + (j - i) \<le> n" 1048 using \<open>k<?n\<close> by arith 1049 show ?thesis 1050 using steps[OF small] \<open>i<k\<close> by auto 1051 qed 1052 qed 1053 qed (simp add: \<open>f 0 = a\<close>) 1054 moreover have "?n \<le> n" 1055 using i j ij by arith 1056 ultimately show ?thesis 1057 using \<open>n = card R\<close> by blast 1058 qed 1059 qed 1060 then show ?thesis 1061 using gr0_implies_Suc[OF \<open>k > 0\<close>] by auto 1062qed 1063 1064lemma relpow_finite_bounded: 1065 fixes R :: "('a \<times> 'a) set" 1066 assumes "finite R" 1067 shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)" 1068 apply (cases k, force) 1069 apply (use relpow_finite_bounded1[OF assms, of k] in auto) 1070 done 1071 1072lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)" 1073 by (fastforce simp: rtrancl_power dest: relpow_finite_bounded) 1074 1075lemma trancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>+ = (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" 1076 apply (auto simp: trancl_power) 1077 apply (auto dest: relpow_finite_bounded1) 1078 done 1079 1080lemma finite_relcomp[simp,intro]: 1081 assumes "finite R" and "finite S" 1082 shows "finite (R O S)" 1083proof- 1084 have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})" 1085 by (force simp: split_def image_constant_conv split: if_splits) 1086 then show ?thesis 1087 using assms by clarsimp 1088qed 1089 1090lemma finite_relpow [simp, intro]: 1091 fixes R :: "('a \<times> 'a) set" 1092 assumes "finite R" 1093 shows "n > 0 \<Longrightarrow> finite (R^^n)" 1094proof (induct n) 1095 case 0 1096 then show ?case by simp 1097next 1098 case (Suc n) 1099 then show ?case by (cases n) (use assms in simp_all) 1100qed 1101 1102lemma single_valued_relpow: 1103 fixes R :: "('a \<times> 'a) set" 1104 shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)" 1105proof (induct n arbitrary: R) 1106 case 0 1107 then show ?case by simp 1108next 1109 case (Suc n) 1110 show ?case 1111 by (rule single_valuedI) 1112 (use Suc in \<open>fast dest: single_valuedD elim: relpow_Suc_E\<close>) 1113qed 1114 1115 1116subsection \<open>Bounded transitive closure\<close> 1117 1118definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 1119 where "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)" 1120 1121lemma ntrancl_Zero [simp, code]: "ntrancl 0 R = R" 1122proof 1123 show "R \<subseteq> ntrancl 0 R" 1124 unfolding ntrancl_def by fastforce 1125 have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" for i 1126 by auto 1127 then show "ntrancl 0 R \<le> R" 1128 unfolding ntrancl_def by auto 1129qed 1130 1131lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)" 1132proof 1133 have "(a, b) \<in> ntrancl n R O (Id \<union> R)" if "(a, b) \<in> ntrancl (Suc n) R" for a b 1134 proof - 1135 from that obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i" 1136 unfolding ntrancl_def by auto 1137 show ?thesis 1138 proof (cases "i = 1") 1139 case True 1140 from this \<open>(a, b) \<in> R ^^ i\<close> show ?thesis 1141 by (auto simp: ntrancl_def) 1142 next 1143 case False 1144 with \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j" 1145 by (cases i) auto 1146 with \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2: "(c, b) \<in> R" 1147 by auto 1148 from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R" 1149 by (fastforce simp: ntrancl_def) 1150 with c2 show ?thesis by fastforce 1151 qed 1152 qed 1153 then show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)" 1154 by auto 1155 show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R" 1156 by (fastforce simp: ntrancl_def) 1157qed 1158 1159lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \<union> r' O r)" 1160 by (auto simp: Let_def) 1161 1162lemma finite_trancl_ntranl: "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R" 1163 by (cases "card R") (auto simp: trancl_finite_eq_relpow relpow_empty ntrancl_def) 1164 1165 1166subsection \<open>Acyclic relations\<close> 1167 1168definition acyclic :: "('a \<times> 'a) set \<Rightarrow> bool" 1169 where "acyclic r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r\<^sup>+)" 1170 1171abbreviation acyclicP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 1172 where "acyclicP r \<equiv> acyclic {(x, y). r x y}" 1173 1174lemma acyclic_irrefl [code]: "acyclic r \<longleftrightarrow> irrefl (r\<^sup>+)" 1175 by (simp add: acyclic_def irrefl_def) 1176 1177lemma acyclicI: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> acyclic r" 1178 by (simp add: acyclic_def) 1179 1180lemma (in order) acyclicI_order: 1181 assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a" 1182 shows "acyclic r" 1183proof - 1184 have "f b < f a" if "(a, b) \<in> r\<^sup>+" for a b 1185 using that by induct (auto intro: * less_trans) 1186 then show ?thesis 1187 by (auto intro!: acyclicI) 1188qed 1189 1190lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \<longleftrightarrow> acyclic r \<and> (x, y) \<notin> r\<^sup>*" 1191 by (simp add: acyclic_def trancl_insert) (blast intro: rtrancl_trans) 1192 1193lemma acyclic_converse [iff]: "acyclic (r\<inverse>) \<longleftrightarrow> acyclic r" 1194 by (simp add: acyclic_def trancl_converse) 1195 1196lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] 1197 1198lemma acyclic_impl_antisym_rtrancl: "acyclic r \<Longrightarrow> antisym (r\<^sup>*)" 1199 by (simp add: acyclic_def antisym_def) 1200 (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) 1201 1202(* Other direction: 1203acyclic = no loops 1204antisym = only self loops 1205Goalw [acyclic_def,antisym_def] "antisym( r\<^sup>* ) \<Longrightarrow> acyclic(r - Id) 1206\<Longrightarrow> antisym( r\<^sup>* ) = acyclic(r - Id)"; 1207*) 1208 1209lemma acyclic_subset: "acyclic s \<Longrightarrow> r \<subseteq> s \<Longrightarrow> acyclic r" 1210 unfolding acyclic_def by (blast intro: trancl_mono) 1211 1212 1213subsection \<open>Setup of transitivity reasoner\<close> 1214 1215ML \<open> 1216structure Trancl_Tac = Trancl_Tac 1217( 1218 val r_into_trancl = @{thm trancl.r_into_trancl}; 1219 val trancl_trans = @{thm trancl_trans}; 1220 val rtrancl_refl = @{thm rtrancl.rtrancl_refl}; 1221 val r_into_rtrancl = @{thm r_into_rtrancl}; 1222 val trancl_into_rtrancl = @{thm trancl_into_rtrancl}; 1223 val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl}; 1224 val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; 1225 val rtrancl_trans = @{thm rtrancl_trans}; 1226 1227 fun decomp (@{const Trueprop} $ t) = 1228 let 1229 fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel) = 1230 let 1231 fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*") 1232 | decr (Const (@{const_name trancl}, _ ) $ r) = (r,"r+") 1233 | decr r = (r,"r"); 1234 val (rel,r) = decr (Envir.beta_eta_contract rel); 1235 in SOME (a,b,rel,r) end 1236 | dec _ = NONE 1237 in dec t end 1238 | decomp _ = NONE; 1239); 1240 1241structure Tranclp_Tac = Trancl_Tac 1242( 1243 val r_into_trancl = @{thm tranclp.r_into_trancl}; 1244 val trancl_trans = @{thm tranclp_trans}; 1245 val rtrancl_refl = @{thm rtranclp.rtrancl_refl}; 1246 val r_into_rtrancl = @{thm r_into_rtranclp}; 1247 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; 1248 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; 1249 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; 1250 val rtrancl_trans = @{thm rtranclp_trans}; 1251 1252 fun decomp (@{const Trueprop} $ t) = 1253 let 1254 fun dec (rel $ a $ b) = 1255 let 1256 fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*") 1257 | decr (Const (@{const_name tranclp}, _ ) $ r) = (r,"r+") 1258 | decr r = (r,"r"); 1259 val (rel,r) = decr rel; 1260 in SOME (a, b, rel, r) end 1261 | dec _ = NONE 1262 in dec t end 1263 | decomp _ = NONE; 1264); 1265\<close> 1266 1267setup \<open> 1268 map_theory_simpset (fn ctxt => ctxt 1269 addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac) 1270 addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac) 1271 addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac) 1272 addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac)) 1273\<close> 1274 1275 1276text \<open>Optional methods.\<close> 1277 1278method_setup trancl = 1279 \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\<close> 1280 \<open>simple transitivity reasoner\<close> 1281method_setup rtrancl = 1282 \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\<close> 1283 \<open>simple transitivity reasoner\<close> 1284method_setup tranclp = 1285 \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\<close> 1286 \<open>simple transitivity reasoner (predicate version)\<close> 1287method_setup rtranclp = 1288 \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\<close> 1289 \<open>simple transitivity reasoner (predicate version)\<close> 1290 1291end 1292