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 apply (rule wellorder_class.intro [OF lin]) 72 apply (simp add: wellorder_class.intro class.wellorder_axioms.intro wf_induct_rule [OF wf]) 73 done 74 75lemma (in wellorder) wf: "wf {(x, y). x < y}" 76 unfolding wf_def by (blast intro: less_induct) 77 78 79subsection \<open>Basic Results\<close> 80 81text \<open>Point-free characterization of well-foundedness\<close> 82 83lemma wfE_pf: 84 assumes wf: "wf R" 85 and a: "A \<subseteq> R `` A" 86 shows "A = {}" 87proof - 88 from wf have "x \<notin> A" for x 89 proof induct 90 fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A" 91 then have "x \<notin> R `` A" by blast 92 with a show "x \<notin> A" by blast 93 qed 94 then show ?thesis by auto 95qed 96 97lemma wfI_pf: 98 assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}" 99 shows "wf R" 100proof (rule wfUNIVI) 101 fix P :: "'a \<Rightarrow> bool" and x 102 let ?A = "{x. \<not> P x}" 103 assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x" 104 then have "?A \<subseteq> R `` ?A" by blast 105 with a show "P x" by blast 106qed 107 108 109subsubsection \<open>Minimal-element characterization of well-foundedness\<close> 110 111lemma wfE_min: 112 assumes wf: "wf R" and Q: "x \<in> Q" 113 obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q" 114 using Q wfE_pf[OF wf, of Q] by blast 115 116lemma wfE_min': 117 "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" 118 using wfE_min[of R _ Q] by blast 119 120lemma wfI_min: 121 assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q" 122 shows "wf R" 123proof (rule wfI_pf) 124 fix A 125 assume b: "A \<subseteq> R `` A" 126 have False if "x \<in> A" for x 127 using a[OF that] b by blast 128 then show "A = {}" by blast 129qed 130 131lemma 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))" 132 apply (rule iffI) 133 apply (blast intro: elim!: wfE_min) 134 by (rule wfI_min) auto 135 136lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] 137 138 139subsubsection \<open>Well-foundedness of transitive closure\<close> 140 141lemma wf_trancl: 142 assumes "wf r" 143 shows "wf (r\<^sup>+)" 144proof - 145 have "P x" if induct_step: "\<And>x. (\<And>y. (y, x) \<in> r\<^sup>+ \<Longrightarrow> P y) \<Longrightarrow> P x" for P x 146 proof (rule induct_step) 147 show "P y" if "(y, x) \<in> r\<^sup>+" for y 148 using \<open>wf r\<close> and that 149 proof (induct x arbitrary: y) 150 case (less x) 151 note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close> 152 from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y" 153 proof cases 154 case base 155 show "P y" 156 proof (rule induct_step) 157 fix y' 158 assume "(y', y) \<in> r\<^sup>+" 159 with \<open>(y, x) \<in> r\<close> show "P y'" 160 by (rule hyp [of y y']) 161 qed 162 next 163 case step 164 then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+" 165 by simp 166 then show "P y" by (rule hyp [of x' y]) 167 qed 168 qed 169 qed 170 then show ?thesis unfolding wf_def by blast 171qed 172 173lemmas wfP_trancl = wf_trancl [to_pred] 174 175lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)" 176 apply (subst trancl_converse [symmetric]) 177 apply (erule wf_trancl) 178 done 179 180text \<open>Well-foundedness of subsets\<close> 181 182lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p" 183 by (simp add: wf_eq_minimal) fast 184 185lemmas wfP_subset = wf_subset [to_pred] 186 187text \<open>Well-foundedness of the empty relation\<close> 188 189lemma wf_empty [iff]: "wf {}" 190 by (simp add: wf_def) 191 192lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)" 193proof - 194 have "wfP bot" 195 by (fact wf_empty[to_pred bot_empty_eq2]) 196 then show ?thesis 197 by (simp add: bot_fun_def) 198qed 199 200lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')" 201 by (erule wf_subset) (rule Int_lower1) 202 203lemma wf_Int2: "wf r \<Longrightarrow> wf (r' \<inter> r)" 204 by (erule wf_subset) (rule Int_lower2) 205 206text \<open>Exponentiation.\<close> 207lemma wf_exp: 208 assumes "wf (R ^^ n)" 209 shows "wf R" 210proof (rule wfI_pf) 211 fix A assume "A \<subseteq> R `` A" 212 then have "A \<subseteq> (R ^^ n) `` A" 213 by (induct n) force+ 214 with \<open>wf (R ^^ n)\<close> show "A = {}" 215 by (rule wfE_pf) 216qed 217 218text \<open>Well-foundedness of \<open>insert\<close>.\<close> 219lemma wf_insert [iff]: "wf (insert (y,x) r) \<longleftrightarrow> wf r \<and> (x,y) \<notin> r\<^sup>*" (is "?lhs = ?rhs") 220proof 221 assume ?lhs then show ?rhs 222 by (blast elim: wf_trancl [THEN wf_irrefl] 223 intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN subsetD]) 224next 225 assume R: ?rhs 226 then have R': "Q \<noteq> {} \<Longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" for Q 227 by (auto simp: wf_eq_minimal) 228 show ?lhs 229 unfolding wf_eq_minimal 230 proof clarify 231 fix Q :: "'a set" and q 232 assume "q \<in> Q" 233 then obtain a where "a \<in> Q" and a: "\<And>y. (y, a) \<in> r \<Longrightarrow> y \<notin> Q" 234 using R by (auto simp: wf_eq_minimal) 235 show "\<exists>z\<in>Q. \<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q" 236 proof (cases "a=x") 237 case True 238 show ?thesis 239 proof (cases "y \<in> Q") 240 case True 241 then obtain z where "z \<in> Q" "(z, y) \<in> r\<^sup>*" 242 "\<And>z'. (z', z) \<in> r \<longrightarrow> z' \<in> Q \<longrightarrow> (z', y) \<notin> r\<^sup>*" 243 using R' [of "{z \<in> Q. (z,y) \<in> r\<^sup>*}"] by auto 244 with R show ?thesis 245 by (rule_tac x="z" in bexI) (blast intro: rtrancl_trans) 246 next 247 case False 248 then show ?thesis 249 using a \<open>a \<in> Q\<close> by blast 250 qed 251 next 252 case False 253 with a \<open>a \<in> Q\<close> show ?thesis 254 by blast 255 qed 256 qed 257qed 258 259 260subsubsection \<open>Well-foundedness of image\<close> 261 262lemma wf_map_prod_image_Dom_Ran: 263 fixes r:: "('a \<times> 'a) set" 264 and f:: "'a \<Rightarrow> 'b" 265 assumes wf_r: "wf r" 266 and inj: "\<And> a a'. a \<in> Domain r \<Longrightarrow> a' \<in> Range r \<Longrightarrow> f a = f a' \<Longrightarrow> a = a'" 267 shows "wf (map_prod f f ` r)" 268proof (unfold wf_eq_minimal, clarify) 269 fix B :: "'b set" and b::"'b" 270 assume "b \<in> B" 271 define A where "A = f -` B \<inter> Domain r" 272 show "\<exists>z\<in>B. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> B" 273 proof (cases "A = {}") 274 case False 275 then obtain a0 where "a0 \<in> A" and "\<forall>a. (a, a0) \<in> r \<longrightarrow> a \<notin> A" 276 using wfE_min[OF wf_r] by auto 277 thus ?thesis 278 using inj unfolding A_def 279 by (intro bexI[of _ "f a0"]) auto 280 qed (insert \<open>b \<in> B\<close>, unfold A_def, auto) 281qed 282 283lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)" 284by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD) 285 286 287subsection \<open>Well-Foundedness Results for Unions\<close> 288 289lemma wf_union_compatible: 290 assumes "wf R" "wf S" 291 assumes "R O S \<subseteq> R" 292 shows "wf (R \<union> S)" 293proof (rule wfI_min) 294 fix x :: 'a and Q 295 let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}" 296 assume "x \<in> Q" 297 obtain a where "a \<in> ?Q'" 298 by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast 299 with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" 300 by (erule wfE_min) 301 have "y \<notin> Q" if "(y, z) \<in> S" for y 302 proof 303 from that have "y \<notin> ?Q'" by (rule zmin) 304 assume "y \<in> Q" 305 with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto 306 from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI) 307 with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" .. 308 with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast 309 with \<open>w \<in> Q\<close> show False by contradiction 310 qed 311 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 312qed 313 314 315text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close> 316 317lemma wf_UN: 318 assumes r: "\<And>i. i \<in> I \<Longrightarrow> wf (r i)" 319 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) = {}" 320 shows "wf (\<Union>i\<in>I. r i)" 321 unfolding wf_eq_minimal 322proof clarify 323 fix A and a :: "'b" 324 assume "a \<in> A" 325 show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> \<Union>(r ` I) \<longrightarrow> y \<notin> A" 326 proof (cases "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i") 327 case True 328 then obtain i b c where ibc: "i \<in> I" "b \<in> A" "c \<in> A" "(c,b) \<in> r i" 329 by blast 330 have ri: "\<And>Q. Q \<noteq> {} \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r i \<longrightarrow> y \<notin> Q" 331 using r [OF \<open>i \<in> I\<close>] unfolding wf_eq_minimal by auto 332 show ?thesis 333 using ri [of "{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }"] ibc disj 334 by blast 335 next 336 case False 337 with \<open>a \<in> A\<close> show ?thesis 338 by blast 339 qed 340qed 341 342lemma wfP_SUP: 343 "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow> 344 wfP (\<Squnion>(range r))" 345 by (rule wf_UN[to_pred]) simp_all 346 347lemma wf_Union: 348 assumes "\<forall>r\<in>R. wf r" 349 and "\<forall>r\<in>R. \<forall>s\<in>R. r \<noteq> s \<longrightarrow> Domain r \<inter> Range s = {}" 350 shows "wf (\<Union>R)" 351 using assms wf_UN[of R "\<lambda>i. i"] by simp 352 353text \<open> 354 Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction. 355 \<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>. 356 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>. 357 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 358 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 359 have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well. 360 \<^enum> There is no such step. 361 Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min 362 element of \<open>A\<close> as well. 363\<close> 364lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)" 365 using wf_union_compatible[of s r] 366 by (auto simp: Un_ac) 367 368lemma wf_union_merge: "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" 369 (is "wf ?A = wf ?B") 370proof 371 assume "wf ?A" 372 with wf_trancl have wfT: "wf (?A\<^sup>+)" . 373 moreover have "?B \<subseteq> ?A\<^sup>+" 374 by (subst trancl_unfold, subst trancl_unfold) blast 375 ultimately show "wf ?B" by (rule wf_subset) 376next 377 assume "wf ?B" 378 show "wf ?A" 379 proof (rule wfI_min) 380 fix Q :: "'a set" and x 381 assume "x \<in> Q" 382 with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 383 by (erule wfE_min) 384 then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" 385 and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" 386 and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" 387 by auto 388 show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" 389 proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") 390 case True 391 with \<open>z \<in> Q\<close> 3 show ?thesis by blast 392 next 393 case False 394 then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast 395 have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" 396 proof (intro allI impI) 397 fix y assume "(y, z') \<in> ?A" 398 then show "y \<notin> Q" 399 proof 400 assume "(y, z') \<in> R" 401 then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> .. 402 with 1 show "y \<notin> Q" . 403 next 404 assume "(y, z') \<in> S" 405 then have "(y, z) \<in> S O R" using \<open>(z', z) \<in> R\<close> .. 406 with 2 show "y \<notin> Q" . 407 qed 408 qed 409 with \<open>z' \<in> Q\<close> show ?thesis .. 410 qed 411 qed 412qed 413 414lemma wf_comp_self: "wf R \<longleftrightarrow> wf (R O R)" \<comment> \<open>special case\<close> 415 by (rule wf_union_merge [where S = "{}", simplified]) 416 417 418subsection \<open>Well-Foundedness of Composition\<close> 419 420text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close> 421 422lemma qc_wf_relto_iff: 423 assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close> 424 shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" 425 (is "wf ?S \<longleftrightarrow> _") 426proof 427 show "wf R" if "wf ?S" 428 proof - 429 have "R \<subseteq> ?S" by auto 430 with wf_subset [of ?S] that show "wf R" 431 by auto 432 qed 433next 434 show "wf ?S" if "wf R" 435 proof (rule wfI_pf) 436 fix A 437 assume A: "A \<subseteq> ?S `` A" 438 let ?X = "(R \<union> S)\<^sup>* `` A" 439 have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" 440 proof - 441 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 442 using that 443 proof (induct y z) 444 case rtrancl_refl 445 then show ?case by auto 446 next 447 case (rtrancl_into_rtrancl a b c) 448 then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" 449 using assms by blast 450 then show ?case by simp 451 qed 452 then show ?thesis by auto 453 qed 454 then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" 455 using rtrancl_Un_subset by blast 456 then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" 457 by (simp add: relcomp_mono rtrancl_mono) 458 also have "\<dots> = (R \<union> S)\<^sup>* O R" 459 by (simp add: O_assoc[symmetric]) 460 finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" 461 by (simp add: O_assoc[symmetric] relcomp_mono) 462 also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" 463 using * by (simp add: relcomp_mono) 464 finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" 465 by (simp add: O_assoc[symmetric]) 466 then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" 467 by (simp add: Image_mono) 468 moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" 469 using A by (auto simp: relcomp_Image) 470 ultimately have "?X \<subseteq> R `` ?X" 471 by (auto simp: relcomp_Image) 472 then have "?X = {}" 473 using \<open>wf R\<close> by (simp add: wfE_pf) 474 moreover have "A \<subseteq> ?X" by auto 475 ultimately show "A = {}" by simp 476 qed 477qed 478 479corollary wf_relcomp_compatible: 480 assumes "wf R" and "R O S \<subseteq> S O R" 481 shows "wf (S O R)" 482proof - 483 have "R O S \<subseteq> (R \<union> S)\<^sup>* O R" 484 using assms by blast 485 then have "wf (S\<^sup>* O R O S\<^sup>*)" 486 by (simp add: assms qc_wf_relto_iff) 487 then show ?thesis 488 by (rule Wellfounded.wf_subset) blast 489qed 490 491 492subsection \<open>Acyclic relations\<close> 493 494lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r" 495 by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl]) 496 497lemmas wfP_acyclicP = wf_acyclic [to_pred] 498 499 500subsubsection \<open>Wellfoundedness of finite acyclic relations\<close> 501 502lemma finite_acyclic_wf: 503 assumes "finite r" "acyclic r" shows "wf r" 504 using assms 505proof (induction r rule: finite_induct) 506 case (insert x r) 507 then show ?case 508 by (cases x) simp 509qed simp 510 511lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)" 512 apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) 513 apply (erule acyclic_converse [THEN iffD2]) 514 done 515 516text \<open> 517 Observe that the converse of an irreflexive, transitive, 518 and finite relation is again well-founded. Thus, we may 519 employ it for well-founded induction. 520\<close> 521lemma wf_converse: 522 assumes "irrefl r" and "trans r" and "finite r" 523 shows "wf (r\<inverse>)" 524proof - 525 have "acyclic r" 526 using \<open>irrefl r\<close> and \<open>trans r\<close> 527 by (simp add: irrefl_def acyclic_irrefl) 528 with \<open>finite r\<close> show ?thesis 529 by (rule finite_acyclic_wf_converse) 530qed 531 532lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r" 533 by (blast intro: finite_acyclic_wf wf_acyclic) 534 535 536subsection \<open>\<^typ>\<open>nat\<close> is well-founded\<close> 537 538lemma less_nat_rel: "(<) = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+" 539proof (rule ext, rule ext, rule iffI) 540 fix n m :: nat 541 show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n" 542 using that 543 proof (induct n) 544 case 0 545 then show ?case by auto 546 next 547 case (Suc n) 548 then show ?case 549 by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) 550 qed 551 show "m < n" if "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" 552 using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less) 553qed 554 555definition pred_nat :: "(nat \<times> nat) set" 556 where "pred_nat = {(m, n). n = Suc m}" 557 558definition less_than :: "(nat \<times> nat) set" 559 where "less_than = pred_nat\<^sup>+" 560 561lemma less_eq: "(m, n) \<in> pred_nat\<^sup>+ \<longleftrightarrow> m < n" 562 unfolding less_nat_rel pred_nat_def trancl_def by simp 563 564lemma pred_nat_trancl_eq_le: "(m, n) \<in> pred_nat\<^sup>* \<longleftrightarrow> m \<le> n" 565 unfolding less_eq rtrancl_eq_or_trancl by auto 566 567lemma wf_pred_nat: "wf pred_nat" 568 apply (unfold wf_def pred_nat_def) 569 apply clarify 570 apply (induct_tac x) 571 apply blast+ 572 done 573 574lemma wf_less_than [iff]: "wf less_than" 575 by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) 576 577lemma trans_less_than [iff]: "trans less_than" 578 by (simp add: less_than_def) 579 580lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)" 581 by (simp add: less_than_def less_eq) 582 583lemma total_less_than: "total less_than" 584 using total_on_def by force 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!]: 728 fixes f :: "'a \<Rightarrow> 'b" 729 assumes "wf r" 730 shows "wf (inv_image r f)" 731proof (clarsimp simp: inv_image_def wf_eq_minimal) 732 fix P and x::'a 733 assume "x \<in> P" 734 then obtain w where w: "w \<in> {w. \<exists>x::'a. x \<in> P \<and> f x = w}" 735 by auto 736 have *: "\<And>Q u. u \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" 737 using assms by (auto simp add: wf_eq_minimal) 738 show "\<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P" 739 using * [OF w] by auto 740qed 741 742text \<open>Measure functions into \<^typ>\<open>nat\<close>\<close> 743 744definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set" 745 where "measure = inv_image less_than" 746 747lemma in_measure[simp, code_unfold]: "(x, y) \<in> measure f \<longleftrightarrow> f x < f y" 748 by (simp add:measure_def) 749 750lemma wf_measure [iff]: "wf (measure f)" 751 unfolding measure_def by (rule wf_less_than [THEN wf_inv_image]) 752 753lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}" 754 for f :: "'a \<Rightarrow> nat" 755 using wf_measure[of f] unfolding measure_def inv_image_def less_than_def less_eq 756 by (rule wf_subset) auto 757 758 759subsubsection \<open>Lexicographic combinations\<close> 760 761definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" 762 (infixr "<*lex*>" 80) 763 where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}" 764 765lemma 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" 766 by (auto simp:lex_prod_def) 767 768lemma wf_lex_prod [intro!]: 769 assumes "wf ra" "wf rb" 770 shows "wf (ra <*lex*> rb)" 771proof (rule wfI) 772 fix z :: "'a \<times> 'b" and P 773 assume * [rule_format]: "\<forall>u. (\<forall>v. (v, u) \<in> ra <*lex*> rb \<longrightarrow> P v) \<longrightarrow> P u" 774 obtain x y where zeq: "z = (x,y)" 775 by fastforce 776 have "P(x,y)" using \<open>wf ra\<close> 777 proof (induction x arbitrary: y rule: wf_induct_rule) 778 case (less x) 779 note lessx = less 780 show ?case using \<open>wf rb\<close> less 781 proof (induction y rule: wf_induct_rule) 782 case (less y) 783 show ?case 784 by (force intro: * less.IH lessx) 785 qed 786 qed 787 then show "P z" 788 by (simp add: zeq) 789qed auto 790 791text \<open>\<open><*lex*>\<close> preserves transitivity\<close> 792lemma trans_lex_prod [simp,intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)" 793 unfolding trans_def lex_prod_def by blast 794 795lemma total_on_lex_prod [simp]: "total_on A r \<Longrightarrow> total_on B s \<Longrightarrow> total_on (A \<times> B) (r <*lex*> s)" 796 by (auto simp: total_on_def) 797 798lemma total_lex_prod [simp]: "total r \<Longrightarrow> total s \<Longrightarrow> total (r <*lex*> s)" 799 by (auto simp: total_on_def) 800 801text \<open>lexicographic combinations with measure functions\<close> 802 803definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80) 804 where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))" 805 806lemma 807 wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" and 808 mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and 809 mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and 810 mlex_iff: "(x, y) \<in> f <*mlex*> R \<longleftrightarrow> f x < f y \<or> f x = f y \<and> (x, y) \<in> R" 811 by (auto simp: mlex_prod_def) 812 813text \<open>Proper subset relation on finite sets.\<close> 814definition finite_psubset :: "('a set \<times> 'a set) set" 815 where "finite_psubset = {(A, B). A \<subset> B \<and> finite B}" 816 817lemma wf_finite_psubset[simp]: "wf finite_psubset" 818 apply (unfold finite_psubset_def) 819 apply (rule wf_measure [THEN wf_subset]) 820 apply (simp add: measure_def inv_image_def less_than_def less_eq) 821 apply (fast elim!: psubset_card_mono) 822 done 823 824lemma trans_finite_psubset: "trans finite_psubset" 825 by (auto simp: finite_psubset_def less_le trans_def) 826 827lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B" 828 unfolding finite_psubset_def by auto 829 830text \<open>max- and min-extension of order to finite sets\<close> 831 832inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 833 for R :: "('a \<times> 'a) set" 834 where max_extI[intro]: 835 "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" 836 837lemma max_ext_wf: 838 assumes wf: "wf r" 839 shows "wf (max_ext r)" 840proof (rule acc_wfI, intro allI) 841 show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") for M 842 proof (induct M rule: infinite_finite_induct) 843 case empty 844 show ?case 845 by (rule accI) (auto elim: max_ext.cases) 846 next 847 case (insert a M) 848 from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W" 849 proof (induct arbitrary: M) 850 fix M a 851 assume "M \<in> ?W" 852 assume [intro]: "finite M" 853 assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W" 854 have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W" 855 if "finite N" "finite M" for N M :: "'a set" 856 using that by (induct N arbitrary: M) (auto simp: hyp) 857 show "insert a M \<in> ?W" 858 proof (rule accI) 859 fix N 860 assume Nless: "(N, insert a M) \<in> max_ext r" 861 then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)" 862 by (auto elim!: max_ext.cases) 863 864 let ?N1 = "{n \<in> N. (n, a) \<in> r}" 865 let ?N2 = "{n \<in> N. (n, a) \<notin> r}" 866 have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto 867 from Nless have "finite N" by (auto elim: max_ext.cases) 868 then have finites: "finite ?N1" "finite ?N2" by auto 869 870 have "?N2 \<in> ?W" 871 proof (cases "M = {}") 872 case [simp]: True 873 have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases) 874 from * have "?N2 = {}" by auto 875 with Mw show "?N2 \<in> ?W" by (simp only:) 876 next 877 case False 878 from * finites have N2: "(?N2, M) \<in> max_ext r" 879 by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto 880 with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward) 881 qed 882 with finites have "?N1 \<union> ?N2 \<in> ?W" 883 by (rule add_less) simp 884 then show "N \<in> ?W" by (simp only: N) 885 qed 886 qed 887 next 888 case infinite 889 show ?case 890 by (rule accI) (auto elim: max_ext.cases simp: infinite) 891 qed 892qed 893 894lemma 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" 895 by (force elim!: max_ext.cases) 896 897definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 898 where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}" 899 900lemma min_ext_wf: 901 assumes "wf r" 902 shows "wf (min_ext r)" 903proof (rule wfI_min) 904 show "\<exists>m \<in> Q. (\<forall>n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q" 905 for Q :: "'a set set" and x 906 proof (cases "Q = {{}}") 907 case True 908 then show ?thesis by (simp add: min_ext_def) 909 next 910 case False 911 with nonempty obtain e x where "x \<in> Q" "e \<in> x" by force 912 then have eU: "e \<in> \<Union>Q" by auto 913 with \<open>wf r\<close> 914 obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" 915 by (erule wfE_min) 916 from z obtain m where "m \<in> Q" "z \<in> m" by auto 917 from \<open>m \<in> Q\<close> show ?thesis 918 proof (intro rev_bexI allI impI) 919 fix n 920 assume smaller: "(n, m) \<in> min_ext r" 921 with \<open>z \<in> m\<close> obtain y where "y \<in> n" "(y, z) \<in> r" 922 by (auto simp: min_ext_def) 923 with z(2) show "n \<notin> Q" by auto 924 qed 925 qed 926qed 927 928 929subsubsection \<open>Bounded increase must terminate\<close> 930 931lemma wf_bounded_measure: 932 fixes ub :: "'a \<Rightarrow> nat" 933 and f :: "'a \<Rightarrow> nat" 934 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" 935 shows "wf r" 936 by (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]]) (auto dest: assms) 937 938lemma wf_bounded_set: 939 fixes ub :: "'a \<Rightarrow> 'b set" 940 and f :: "'a \<Rightarrow> 'b set" 941 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" 942 shows "wf r" 943 apply (rule wf_bounded_measure[of r "\<lambda>a. card (ub a)" "\<lambda>a. card (f a)"]) 944 apply (drule assms) 945 apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) 946 done 947 948lemma finite_subset_wf: 949 assumes "finite A" 950 shows "wf {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}" 951 by (rule wf_subset[OF wf_finite_psubset[unfolded finite_psubset_def]]) 952 (auto intro: finite_subset[OF _ assms]) 953 954hide_const (open) acc accp 955 956end 957