1(* Title: HOL/Wellfounded.thy 2 Author: Tobias Nipkow 3 Author: Lawrence C Paulson 4 Author: Konrad Slind 5 Author: Alexander Krauss 6 Author: Andrei Popescu, TU Muenchen 7*) 8 9section \<open>Well-founded Recursion\<close> 10 11theory Wellfounded 12 imports Transitive_Closure 13begin 14 15subsection \<open>Basic Definitions\<close> 16 17definition wf :: "('a \<times> 'a) set \<Rightarrow> bool" 18 where "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))" 19 20definition wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 21 where "wfP r \<longleftrightarrow> wf {(x, y). r x y}" 22 23lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r" 24 by (simp add: wfP_def) 25 26lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r" 27 unfolding wf_def by blast 28 29lemmas wfPUNIVI = wfUNIVI [to_pred] 30 31text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>. 32 If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close> 33lemma wfI: 34 assumes "r \<subseteq> A \<times> B" 35 and "\<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x; x \<in> A; x \<in> B\<rbrakk> \<Longrightarrow> P x" 36 shows "wf r" 37 using assms unfolding wf_def by blast 38 39lemma wf_induct: 40 assumes "wf r" 41 and "\<And>x. \<forall>y. (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x" 42 shows "P a" 43 using assms unfolding wf_def by blast 44 45lemmas wfP_induct = wf_induct [to_pred] 46 47lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] 48 49lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] 50 51lemma wf_not_sym: "wf r \<Longrightarrow> (a, x) \<in> r \<Longrightarrow> (x, a) \<notin> r" 52 by (induct a arbitrary: x set: wf) blast 53 54lemma wf_asym: 55 assumes "wf r" "(a, x) \<in> r" 56 obtains "(x, a) \<notin> r" 57 by (drule wf_not_sym[OF assms]) 58 59lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r" 60 by (blast elim: wf_asym) 61 62lemma wf_irrefl: 63 assumes "wf r" 64 obtains "(a, a) \<notin> r" 65 by (drule wf_not_refl[OF assms]) 66 67lemma wf_wellorderI: 68 assumes wf: "wf {(x::'a::ord, y). x < y}" 69 and lin: "OFCLASS('a::ord, linorder_class)" 70 shows "OFCLASS('a::ord, wellorder_class)" 71 using lin 72 apply (rule wellorder_class.intro) 73 apply (rule class.wellorder_axioms.intro) 74 apply (rule wf_induct_rule [OF wf]) 75 apply simp 76 done 77 78lemma (in wellorder) wf: "wf {(x, y). x < y}" 79 unfolding wf_def by (blast intro: less_induct) 80 81 82subsection \<open>Basic Results\<close> 83 84text \<open>Point-free characterization of well-foundedness\<close> 85 86lemma wfE_pf: 87 assumes wf: "wf R" 88 and a: "A \<subseteq> R `` A" 89 shows "A = {}" 90proof - 91 from wf have "x \<notin> A" for x 92 proof induct 93 fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A" 94 then have "x \<notin> R `` A" by blast 95 with a show "x \<notin> A" by blast 96 qed 97 then show ?thesis by auto 98qed 99 100lemma wfI_pf: 101 assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}" 102 shows "wf R" 103proof (rule wfUNIVI) 104 fix P :: "'a \<Rightarrow> bool" and x 105 let ?A = "{x. \<not> P x}" 106 assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x" 107 then have "?A \<subseteq> R `` ?A" by blast 108 with a show "P x" by blast 109qed 110 111 112subsubsection \<open>Minimal-element characterization of well-foundedness\<close> 113 114lemma wfE_min: 115 assumes wf: "wf R" and Q: "x \<in> Q" 116 obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q" 117 using Q wfE_pf[OF wf, of Q] by blast 118 119lemma wfE_min': 120 "wf R \<Longrightarrow> Q \<noteq> {} \<Longrightarrow> (\<And>z. z \<in> Q \<Longrightarrow> (\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q) \<Longrightarrow> thesis) \<Longrightarrow> thesis" 121 using wfE_min[of R _ Q] by blast 122 123lemma wfI_min: 124 assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q" 125 shows "wf R" 126proof (rule wfI_pf) 127 fix A 128 assume b: "A \<subseteq> R `` A" 129 have False if "x \<in> A" for x 130 using a[OF that] b by blast 131 then show "A = {}" by blast 132qed 133 134lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))" 135 apply (rule iffI) 136 apply (blast intro: elim!: wfE_min) 137 by (rule wfI_min) auto 138 139lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] 140 141 142subsubsection \<open>Well-foundedness of transitive closure\<close> 143 144lemma wf_trancl: 145 assumes "wf r" 146 shows "wf (r\<^sup>+)" 147proof - 148 have "P x" if induct_step: "\<And>x. (\<And>y. (y, x) \<in> r\<^sup>+ \<Longrightarrow> P y) \<Longrightarrow> P x" for P x 149 proof (rule induct_step) 150 show "P y" if "(y, x) \<in> r\<^sup>+" for y 151 using \<open>wf r\<close> and that 152 proof (induct x arbitrary: y) 153 case (less x) 154 note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close> 155 from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y" 156 proof cases 157 case base 158 show "P y" 159 proof (rule induct_step) 160 fix y' 161 assume "(y', y) \<in> r\<^sup>+" 162 with \<open>(y, x) \<in> r\<close> show "P y'" 163 by (rule hyp [of y y']) 164 qed 165 next 166 case step 167 then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+" 168 by simp 169 then show "P y" by (rule hyp [of x' y]) 170 qed 171 qed 172 qed 173 then show ?thesis unfolding wf_def by blast 174qed 175 176lemmas wfP_trancl = wf_trancl [to_pred] 177 178lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)" 179 apply (subst trancl_converse [symmetric]) 180 apply (erule wf_trancl) 181 done 182 183text \<open>Well-foundedness of subsets\<close> 184 185lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p" 186 by (simp add: wf_eq_minimal) fast 187 188lemmas wfP_subset = wf_subset [to_pred] 189 190text \<open>Well-foundedness of the empty relation\<close> 191 192lemma wf_empty [iff]: "wf {}" 193 by (simp add: wf_def) 194 195lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)" 196proof - 197 have "wfP bot" 198 by (fact wf_empty[to_pred bot_empty_eq2]) 199 then show ?thesis 200 by (simp add: bot_fun_def) 201qed 202 203lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')" 204 by (erule wf_subset) (rule Int_lower1) 205 206lemma wf_Int2: "wf r \<Longrightarrow> wf (r' \<inter> r)" 207 by (erule wf_subset) (rule Int_lower2) 208 209text \<open>Exponentiation.\<close> 210lemma wf_exp: 211 assumes "wf (R ^^ n)" 212 shows "wf R" 213proof (rule wfI_pf) 214 fix A assume "A \<subseteq> R `` A" 215 then have "A \<subseteq> (R ^^ n) `` A" 216 by (induct n) force+ 217 with \<open>wf (R ^^ n)\<close> show "A = {}" 218 by (rule wfE_pf) 219qed 220 221text \<open>Well-foundedness of \<open>insert\<close>.\<close> 222lemma wf_insert [iff]: "wf (insert (y,x) r) \<longleftrightarrow> wf r \<and> (x,y) \<notin> r\<^sup>*" (is "?lhs = ?rhs") 223proof 224 assume ?lhs then show ?rhs 225 by (blast elim: wf_trancl [THEN wf_irrefl] 226 intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN subsetD]) 227next 228 assume R: ?rhs 229 then have R': "Q \<noteq> {} \<Longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" for Q 230 by (auto simp: wf_eq_minimal) 231 show ?lhs 232 unfolding wf_eq_minimal 233 proof clarify 234 fix Q :: "'a set" and q 235 assume "q \<in> Q" 236 then obtain a where "a \<in> Q" and a: "\<And>y. (y, a) \<in> r \<Longrightarrow> y \<notin> Q" 237 using R by (auto simp: wf_eq_minimal) 238 show "\<exists>z\<in>Q. \<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q" 239 proof (cases "a=x") 240 case True 241 show ?thesis 242 proof (cases "y \<in> Q") 243 case True 244 then obtain z where "z \<in> Q" "(z, y) \<in> r\<^sup>*" 245 "\<And>z'. (z', z) \<in> r \<longrightarrow> z' \<in> Q \<longrightarrow> (z', y) \<notin> r\<^sup>*" 246 using R' [of "{z \<in> Q. (z,y) \<in> r\<^sup>*}"] by auto 247 with R show ?thesis 248 by (rule_tac x="z" in bexI) (blast intro: rtrancl_trans) 249 next 250 case False 251 then show ?thesis 252 using a \<open>a \<in> Q\<close> by blast 253 qed 254 next 255 case False 256 with a \<open>a \<in> Q\<close> show ?thesis 257 by blast 258 qed 259 qed 260qed 261 262 263subsubsection \<open>Well-foundedness of image\<close> 264 265lemma wf_map_prod_image_Dom_Ran: 266 fixes r:: "('a \<times> 'a) set" 267 and f:: "'a \<Rightarrow> 'b" 268 assumes wf_r: "wf r" 269 and inj: "\<And> a a'. a \<in> Domain r \<Longrightarrow> a' \<in> Range r \<Longrightarrow> f a = f a' \<Longrightarrow> a = a'" 270 shows "wf (map_prod f f ` r)" 271proof (unfold wf_eq_minimal, clarify) 272 fix B :: "'b set" and b::"'b" 273 assume "b \<in> B" 274 define A where "A = f -` B \<inter> Domain r" 275 show "\<exists>z\<in>B. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> B" 276 proof (cases "A = {}") 277 case False 278 then obtain a0 where "a0 \<in> A" and "\<forall>a. (a, a0) \<in> r \<longrightarrow> a \<notin> A" 279 using wfE_min[OF wf_r] by auto 280 thus ?thesis 281 using inj unfolding A_def 282 by (intro bexI[of _ "f a0"]) auto 283 qed (insert \<open>b \<in> B\<close>, unfold A_def, auto) 284qed 285 286lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)" 287by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD) 288 289 290subsection \<open>Well-Foundedness Results for Unions\<close> 291 292lemma wf_union_compatible: 293 assumes "wf R" "wf S" 294 assumes "R O S \<subseteq> R" 295 shows "wf (R \<union> S)" 296proof (rule wfI_min) 297 fix x :: 'a and Q 298 let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}" 299 assume "x \<in> Q" 300 obtain a where "a \<in> ?Q'" 301 by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast 302 with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" 303 by (erule wfE_min) 304 have "y \<notin> Q" if "(y, z) \<in> S" for y 305 proof 306 from that have "y \<notin> ?Q'" by (rule zmin) 307 assume "y \<in> Q" 308 with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto 309 from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI) 310 with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" .. 311 with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast 312 with \<open>w \<in> Q\<close> show False by contradiction 313 qed 314 with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast 315qed 316 317 318text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close> 319 320lemma wf_UN: 321 assumes r: "\<And>i. i \<in> I \<Longrightarrow> wf (r i)" 322 and disj: "\<And>i j. \<lbrakk>i \<in> I; j \<in> I; r i \<noteq> r j\<rbrakk> \<Longrightarrow> Domain (r i) \<inter> Range (r j) = {}" 323 shows "wf (\<Union>i\<in>I. r i)" 324 unfolding wf_eq_minimal 325proof clarify 326 fix A and a :: "'b" 327 assume "a \<in> A" 328 show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> UNION I r \<longrightarrow> y \<notin> A" 329 proof (cases "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i") 330 case True 331 then obtain i b c where ibc: "i \<in> I" "b \<in> A" "c \<in> A" "(c,b) \<in> r i" 332 by blast 333 have ri: "\<And>Q. Q \<noteq> {} \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r i \<longrightarrow> y \<notin> Q" 334 using r [OF \<open>i \<in> I\<close>] unfolding wf_eq_minimal by auto 335 show ?thesis 336 using ri [of "{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }"] ibc disj 337 by blast 338 next 339 case False 340 with \<open>a \<in> A\<close> show ?thesis 341 by blast 342 qed 343qed 344 345lemma wfP_SUP: 346 "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow> 347 wfP (SUPREMUM UNIV r)" 348 by (rule wf_UN[to_pred]) simp_all 349 350lemma wf_Union: 351 assumes "\<forall>r\<in>R. wf r" 352 and "\<forall>r\<in>R. \<forall>s\<in>R. r \<noteq> s \<longrightarrow> Domain r \<inter> Range s = {}" 353 shows "wf (\<Union>R)" 354 using assms wf_UN[of R "\<lambda>i. i"] by simp 355 356text \<open> 357 Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction. 358 \<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>. 359 Pick an \<open>R\<close>-min element \<open>z\<close> of the (nonempty) set \<open>{a\<in>A | \<exists>b\<in>A. a \<midarrow>R\<rightarrow> b}\<close>. 360 By definition, there is \<open>z' \<in> A\<close> s.t. \<open>z \<midarrow>R\<rightarrow> z'\<close>. Because \<open>z\<close> is \<open>R\<close>-min in the 361 subset, \<open>z'\<close> must be \<open>R\<close>-min in \<open>A\<close>. Because \<open>z'\<close> has an \<open>R\<close>-predecessor, it cannot 362 have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well. 363 \<^enum> There is no such step. 364 Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min 365 element of \<open>A\<close> as well. 366\<close> 367lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)" 368 using wf_union_compatible[of s r] 369 by (auto simp: Un_ac) 370 371lemma wf_union_merge: "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" 372 (is "wf ?A = wf ?B") 373proof 374 assume "wf ?A" 375 with wf_trancl have wfT: "wf (?A\<^sup>+)" . 376 moreover have "?B \<subseteq> ?A\<^sup>+" 377 by (subst trancl_unfold, subst trancl_unfold) blast 378 ultimately show "wf ?B" by (rule wf_subset) 379next 380 assume "wf ?B" 381 show "wf ?A" 382 proof (rule wfI_min) 383 fix Q :: "'a set" and x 384 assume "x \<in> Q" 385 with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 386 by (erule wfE_min) 387 then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" 388 and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" 389 and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" 390 by auto 391 show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" 392 proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") 393 case True 394 with \<open>z \<in> Q\<close> 3 show ?thesis by blast 395 next 396 case False 397 then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast 398 have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" 399 proof (intro allI impI) 400 fix y assume "(y, z') \<in> ?A" 401 then show "y \<notin> Q" 402 proof 403 assume "(y, z') \<in> R" 404 then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> .. 405 with 1 show "y \<notin> Q" . 406 next 407 assume "(y, z') \<in> S" 408 then have "(y, z) \<in> S O R" using \<open>(z', z) \<in> R\<close> .. 409 with 2 show "y \<notin> Q" . 410 qed 411 qed 412 with \<open>z' \<in> Q\<close> show ?thesis .. 413 qed 414 qed 415qed 416 417lemma wf_comp_self: "wf R \<longleftrightarrow> wf (R O R)" \<comment> \<open>special case\<close> 418 by (rule wf_union_merge [where S = "{}", simplified]) 419 420 421subsection \<open>Well-Foundedness of Composition\<close> 422 423text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close> 424 425lemma qc_wf_relto_iff: 426 assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close> 427 shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" 428 (is "wf ?S \<longleftrightarrow> _") 429proof 430 show "wf R" if "wf ?S" 431 proof - 432 have "R \<subseteq> ?S" by auto 433 with wf_subset [of ?S] that show "wf R" 434 by auto 435 qed 436next 437 show "wf ?S" if "wf R" 438 proof (rule wfI_pf) 439 fix A 440 assume A: "A \<subseteq> ?S `` A" 441 let ?X = "(R \<union> S)\<^sup>* `` A" 442 have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" 443 proof - 444 have "(x, z) \<in> (R \<union> S)\<^sup>* O R" if "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R" for x y z 445 using that 446 proof (induct y z) 447 case rtrancl_refl 448 then show ?case by auto 449 next 450 case (rtrancl_into_rtrancl a b c) 451 then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" 452 using assms by blast 453 then show ?case by simp 454 qed 455 then show ?thesis by auto 456 qed 457 then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" 458 using rtrancl_Un_subset by blast 459 then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" 460 by (simp add: relcomp_mono rtrancl_mono) 461 also have "\<dots> = (R \<union> S)\<^sup>* O R" 462 by (simp add: O_assoc[symmetric]) 463 finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" 464 by (simp add: O_assoc[symmetric] relcomp_mono) 465 also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" 466 using * by (simp add: relcomp_mono) 467 finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" 468 by (simp add: O_assoc[symmetric]) 469 then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" 470 by (simp add: Image_mono) 471 moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" 472 using A by (auto simp: relcomp_Image) 473 ultimately have "?X \<subseteq> R `` ?X" 474 by (auto simp: relcomp_Image) 475 then have "?X = {}" 476 using \<open>wf R\<close> by (simp add: wfE_pf) 477 moreover have "A \<subseteq> ?X" by auto 478 ultimately show "A = {}" by simp 479 qed 480qed 481 482corollary wf_relcomp_compatible: 483 assumes "wf R" and "R O S \<subseteq> S O R" 484 shows "wf (S O R)" 485proof - 486 have "R O S \<subseteq> (R \<union> S)\<^sup>* O R" 487 using assms by blast 488 then have "wf (S\<^sup>* O R O S\<^sup>*)" 489 by (simp add: assms qc_wf_relto_iff) 490 then show ?thesis 491 by (rule Wellfounded.wf_subset) blast 492qed 493 494 495subsection \<open>Acyclic relations\<close> 496 497lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r" 498 by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl]) 499 500lemmas wfP_acyclicP = wf_acyclic [to_pred] 501 502 503subsubsection \<open>Wellfoundedness of finite acyclic relations\<close> 504 505lemma finite_acyclic_wf: 506 assumes "finite r" "acyclic r" shows "wf r" 507 using assms 508proof (induction r rule: finite_induct) 509 case (insert x r) 510 then show ?case 511 by (cases x) simp 512qed simp 513 514lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)" 515 apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) 516 apply (erule acyclic_converse [THEN iffD2]) 517 done 518 519text \<open> 520 Observe that the converse of an irreflexive, transitive, 521 and finite relation is again well-founded. Thus, we may 522 employ it for well-founded induction. 523\<close> 524lemma wf_converse: 525 assumes "irrefl r" and "trans r" and "finite r" 526 shows "wf (r\<inverse>)" 527proof - 528 have "acyclic r" 529 using \<open>irrefl r\<close> and \<open>trans r\<close> 530 by (simp add: irrefl_def acyclic_irrefl) 531 with \<open>finite r\<close> show ?thesis 532 by (rule finite_acyclic_wf_converse) 533qed 534 535lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r" 536 by (blast intro: finite_acyclic_wf wf_acyclic) 537 538 539subsection \<open>@{typ nat} is well-founded\<close> 540 541lemma less_nat_rel: "(<) = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+" 542proof (rule ext, rule ext, rule iffI) 543 fix n m :: nat 544 show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n" 545 using that 546 proof (induct n) 547 case 0 548 then show ?case by auto 549 next 550 case (Suc n) 551 then show ?case 552 by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) 553 qed 554 show "m < n" if "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" 555 using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less) 556qed 557 558definition pred_nat :: "(nat \<times> nat) set" 559 where "pred_nat = {(m, n). n = Suc m}" 560 561definition less_than :: "(nat \<times> nat) set" 562 where "less_than = pred_nat\<^sup>+" 563 564lemma less_eq: "(m, n) \<in> pred_nat\<^sup>+ \<longleftrightarrow> m < n" 565 unfolding less_nat_rel pred_nat_def trancl_def by simp 566 567lemma pred_nat_trancl_eq_le: "(m, n) \<in> pred_nat\<^sup>* \<longleftrightarrow> m \<le> n" 568 unfolding less_eq rtrancl_eq_or_trancl by auto 569 570lemma wf_pred_nat: "wf pred_nat" 571 apply (unfold wf_def pred_nat_def) 572 apply clarify 573 apply (induct_tac x) 574 apply blast+ 575 done 576 577lemma wf_less_than [iff]: "wf less_than" 578 by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) 579 580lemma trans_less_than [iff]: "trans less_than" 581 by (simp add: less_than_def) 582 583lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)" 584 by (simp add: less_than_def less_eq) 585 586lemma wf_less: "wf {(x, y::nat). x < y}" 587 by (rule Wellfounded.wellorder_class.wf) 588 589 590subsection \<open>Accessible Part\<close> 591 592text \<open> 593 Inductive definition of the accessible part \<open>acc r\<close> of a 594 relation; see also @{cite "paulin-tlca"}. 595\<close> 596 597inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set" 598 where accI: "(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" 599 600abbreviation termip :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" 601 where "termip r \<equiv> accp (r\<inverse>\<inverse>)" 602 603abbreviation termi :: "('a \<times> 'a) set \<Rightarrow> 'a set" 604 where "termi r \<equiv> acc (r\<inverse>)" 605 606lemmas accpI = accp.accI 607 608lemma accp_eq_acc [code]: "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})" 609 by (simp add: acc_def) 610 611 612text \<open>Induction rules\<close> 613 614theorem accp_induct: 615 assumes major: "accp r a" 616 assumes hyp: "\<And>x. accp r x \<Longrightarrow> \<forall>y. r y x \<longrightarrow> P y \<Longrightarrow> P x" 617 shows "P a" 618 apply (rule major [THEN accp.induct]) 619 apply (rule hyp) 620 apply (rule accp.accI) 621 apply auto 622 done 623 624lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] 625 626theorem accp_downward: "accp r b \<Longrightarrow> r a b \<Longrightarrow> accp r a" 627 by (cases rule: accp.cases) 628 629lemma not_accp_down: 630 assumes na: "\<not> accp R x" 631 obtains z where "R z x" and "\<not> accp R z" 632proof - 633 assume a: "\<And>z. R z x \<Longrightarrow> \<not> accp R z \<Longrightarrow> thesis" 634 show thesis 635 proof (cases "\<forall>z. R z x \<longrightarrow> accp R z") 636 case True 637 then have "\<And>z. R z x \<Longrightarrow> accp R z" by auto 638 then have "accp R x" by (rule accp.accI) 639 with na show thesis .. 640 next 641 case False then obtain z where "R z x" and "\<not> accp R z" 642 by auto 643 with a show thesis . 644 qed 645qed 646 647lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b" 648 by (erule rtranclp_induct) (blast dest: accp_downward)+ 649 650theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b" 651 by (blast dest: accp_downwards_aux) 652 653theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r" 654 apply (rule wfPUNIVI) 655 apply (rule_tac P = P in accp_induct) 656 apply blast+ 657 done 658 659theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x" 660 apply (erule wfP_induct_rule) 661 apply (rule accp.accI) 662 apply blast 663 done 664 665theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)" 666 by (blast intro: accp_wfPI dest: accp_wfPD) 667 668 669text \<open>Smaller relations have bigger accessible parts:\<close> 670 671lemma accp_subset: 672 assumes "R1 \<le> R2" 673 shows "accp R2 \<le> accp R1" 674proof (rule predicate1I) 675 fix x 676 assume "accp R2 x" 677 then show "accp R1 x" 678 proof (induct x) 679 fix x 680 assume "\<And>y. R2 y x \<Longrightarrow> accp R1 y" 681 with assms show "accp R1 x" 682 by (blast intro: accp.accI) 683 qed 684qed 685 686 687text \<open>This is a generalized induction theorem that works on 688 subsets of the accessible part.\<close> 689 690lemma accp_subset_induct: 691 assumes subset: "D \<le> accp R" 692 and dcl: "\<And>x z. D x \<Longrightarrow> R z x \<Longrightarrow> D z" 693 and "D x" 694 and istep: "\<And>x. D x \<Longrightarrow> (\<And>z. R z x \<Longrightarrow> P z) \<Longrightarrow> P x" 695 shows "P x" 696proof - 697 from subset and \<open>D x\<close> 698 have "accp R x" .. 699 then show "P x" using \<open>D x\<close> 700 proof (induct x) 701 fix x 702 assume "D x" and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" 703 with dcl and istep show "P x" by blast 704 qed 705qed 706 707 708text \<open>Set versions of the above theorems\<close> 709 710lemmas acc_induct = accp_induct [to_set] 711lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] 712lemmas acc_downward = accp_downward [to_set] 713lemmas not_acc_down = not_accp_down [to_set] 714lemmas acc_downwards_aux = accp_downwards_aux [to_set] 715lemmas acc_downwards = accp_downwards [to_set] 716lemmas acc_wfI = accp_wfPI [to_set] 717lemmas acc_wfD = accp_wfPD [to_set] 718lemmas wf_acc_iff = wfP_accp_iff [to_set] 719lemmas acc_subset = accp_subset [to_set] 720lemmas acc_subset_induct = accp_subset_induct [to_set] 721 722 723subsection \<open>Tools for building wellfounded relations\<close> 724 725text \<open>Inverse Image\<close> 726 727lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)" 728 for f :: "'a \<Rightarrow> 'b" 729 apply (simp add: inv_image_def wf_eq_minimal) 730 apply clarify 731 apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}") 732 prefer 2 733 apply (blast del: allE) 734 apply (erule allE) 735 apply (erule (1) notE impE) 736 apply blast 737 done 738 739text \<open>Measure functions into @{typ nat}\<close> 740 741definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set" 742 where "measure = inv_image less_than" 743 744lemma in_measure[simp, code_unfold]: "(x, y) \<in> measure f \<longleftrightarrow> f x < f y" 745 by (simp add:measure_def) 746 747lemma wf_measure [iff]: "wf (measure f)" 748 unfolding measure_def by (rule wf_less_than [THEN wf_inv_image]) 749 750lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}" 751 for f :: "'a \<Rightarrow> nat" 752 using wf_measure[of f] unfolding measure_def inv_image_def less_than_def less_eq 753 by (rule wf_subset) auto 754 755 756subsubsection \<open>Lexicographic combinations\<close> 757 758definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" 759 (infixr "<*lex*>" 80) 760 where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}" 761 762lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)" 763 unfolding wf_def lex_prod_def 764 apply (rule allI) 765 apply (rule impI) 766 apply (simp only: split_paired_All) 767 apply (drule spec) 768 apply (erule mp) 769 apply (rule allI) 770 apply (rule impI) 771 apply (drule spec) 772 apply (erule mp) 773 apply blast 774 done 775 776lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s" 777 by (auto simp:lex_prod_def) 778 779text \<open>\<open><*lex*>\<close> preserves transitivity\<close> 780lemma trans_lex_prod [intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)" 781 unfolding trans_def lex_prod_def by blast 782 783 784text \<open>lexicographic combinations with measure functions\<close> 785 786definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80) 787 where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))" 788 789lemma 790 wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" and 791 mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and 792 mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and 793 mlex_iff: "(x, y) \<in> f <*mlex*> R \<longleftrightarrow> f x < f y \<or> f x = f y \<and> (x, y) \<in> R" 794 by (auto simp: mlex_prod_def) 795 796text \<open>Proper subset relation on finite sets.\<close> 797definition finite_psubset :: "('a set \<times> 'a set) set" 798 where "finite_psubset = {(A, B). A \<subset> B \<and> finite B}" 799 800lemma wf_finite_psubset[simp]: "wf finite_psubset" 801 apply (unfold finite_psubset_def) 802 apply (rule wf_measure [THEN wf_subset]) 803 apply (simp add: measure_def inv_image_def less_than_def less_eq) 804 apply (fast elim!: psubset_card_mono) 805 done 806 807lemma trans_finite_psubset: "trans finite_psubset" 808 by (auto simp: finite_psubset_def less_le trans_def) 809 810lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B" 811 unfolding finite_psubset_def by auto 812 813text \<open>max- and min-extension of order to finite sets\<close> 814 815inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 816 for R :: "('a \<times> 'a) set" 817 where max_extI[intro]: 818 "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R" 819 820lemma max_ext_wf: 821 assumes wf: "wf r" 822 shows "wf (max_ext r)" 823proof (rule acc_wfI, intro allI) 824 show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") for M 825 proof (induct M rule: infinite_finite_induct) 826 case empty 827 show ?case 828 by (rule accI) (auto elim: max_ext.cases) 829 next 830 case (insert a M) 831 from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W" 832 proof (induct arbitrary: M) 833 fix M a 834 assume "M \<in> ?W" 835 assume [intro]: "finite M" 836 assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W" 837 have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W" 838 if "finite N" "finite M" for N M :: "'a set" 839 using that by (induct N arbitrary: M) (auto simp: hyp) 840 show "insert a M \<in> ?W" 841 proof (rule accI) 842 fix N 843 assume Nless: "(N, insert a M) \<in> max_ext r" 844 then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)" 845 by (auto elim!: max_ext.cases) 846 847 let ?N1 = "{n \<in> N. (n, a) \<in> r}" 848 let ?N2 = "{n \<in> N. (n, a) \<notin> r}" 849 have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto 850 from Nless have "finite N" by (auto elim: max_ext.cases) 851 then have finites: "finite ?N1" "finite ?N2" by auto 852 853 have "?N2 \<in> ?W" 854 proof (cases "M = {}") 855 case [simp]: True 856 have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases) 857 from * have "?N2 = {}" by auto 858 with Mw show "?N2 \<in> ?W" by (simp only:) 859 next 860 case False 861 from * finites have N2: "(?N2, M) \<in> max_ext r" 862 by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto 863 with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward) 864 qed 865 with finites have "?N1 \<union> ?N2 \<in> ?W" 866 by (rule add_less) simp 867 then show "N \<in> ?W" by (simp only: N) 868 qed 869 qed 870 next 871 case infinite 872 show ?case 873 by (rule accI) (auto elim: max_ext.cases simp: infinite) 874 qed 875qed 876 877lemma max_ext_additive: "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> (A \<union> C, B \<union> D) \<in> max_ext R" 878 by (force elim!: max_ext.cases) 879 880definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 881 where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}" 882 883lemma min_ext_wf: 884 assumes "wf r" 885 shows "wf (min_ext r)" 886proof (rule wfI_min) 887 show "\<exists>m \<in> Q. (\<forall>n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q" 888 for Q :: "'a set set" and x 889 proof (cases "Q = {{}}") 890 case True 891 then show ?thesis by (simp add: min_ext_def) 892 next 893 case False 894 with nonempty obtain e x where "x \<in> Q" "e \<in> x" by force 895 then have eU: "e \<in> \<Union>Q" by auto 896 with \<open>wf r\<close> 897 obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" 898 by (erule wfE_min) 899 from z obtain m where "m \<in> Q" "z \<in> m" by auto 900 from \<open>m \<in> Q\<close> show ?thesis 901 proof (intro rev_bexI allI impI) 902 fix n 903 assume smaller: "(n, m) \<in> min_ext r" 904 with \<open>z \<in> m\<close> obtain y where "y \<in> n" "(y, z) \<in> r" 905 by (auto simp: min_ext_def) 906 with z(2) show "n \<notin> Q" by auto 907 qed 908 qed 909qed 910 911 912subsubsection \<open>Bounded increase must terminate\<close> 913 914lemma wf_bounded_measure: 915 fixes ub :: "'a \<Rightarrow> nat" 916 and f :: "'a \<Rightarrow> nat" 917 assumes "\<And>a b. (b, a) \<in> r \<Longrightarrow> ub b \<le> ub a \<and> ub a \<ge> f b \<and> f b > f a" 918 shows "wf r" 919 by (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]]) (auto dest: assms) 920 921lemma wf_bounded_set: 922 fixes ub :: "'a \<Rightarrow> 'b set" 923 and f :: "'a \<Rightarrow> 'b set" 924 assumes "\<And>a b. (b,a) \<in> r \<Longrightarrow> finite (ub a) \<and> ub b \<subseteq> ub a \<and> ub a \<supseteq> f b \<and> f b \<supset> f a" 925 shows "wf r" 926 apply (rule wf_bounded_measure[of r "\<lambda>a. card (ub a)" "\<lambda>a. card (f a)"]) 927 apply (drule assms) 928 apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) 929 done 930 931lemma finite_subset_wf: 932 assumes "finite A" 933 shows "wf {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}" 934 by (rule wf_subset[OF wf_finite_psubset[unfolded finite_psubset_def]]) 935 (auto intro: finite_subset[OF _ assms]) 936 937hide_const (open) acc accp 938 939end 940