(* Title: HOL/Wellfounded.thy Author: Tobias Nipkow Author: Lawrence C Paulson Author: Konrad Slind Author: Alexander Krauss Author: Andrei Popescu, TU Muenchen *) section ‹Well-founded Recursion› theory Wellfounded imports Transitive_Closure begin subsection ‹Basic Definitions› definition wf :: "('a × 'a) set ⇒ bool" where "wf r ⟷ (∀P. (∀x. (∀y. (y, x) ∈ r ⟶ P y) ⟶ P x) ⟶ (∀x. P x))" definition wfP :: "('a ⇒ 'a ⇒ bool) ⇒ bool" where "wfP r ⟷ wf {(x, y). r x y}" lemma wfP_wf_eq [pred_set_conv]: "wfP (λx y. (x, y) ∈ r) = wf r" by (simp add: wfP_def) lemma wfUNIVI: "(⋀P x. (∀x. (∀y. (y, x) ∈ r ⟶ P y) ⟶ P x) ⟹ P x) ⟹ wf r" unfolding wf_def by blast lemmas wfPUNIVI = wfUNIVI [to_pred] text ‹Restriction to domain ‹A› and range ‹B›. If ‹r› is well-founded over their intersection, then ‹wf r›.› lemma wfI: assumes "r ⊆ A × B" and "⋀x P. ⟦∀x. (∀y. (y, x) ∈ r ⟶ P y) ⟶ P x; x ∈ A; x ∈ B⟧ ⟹ P x" shows "wf r" using assms unfolding wf_def by blast lemma wf_induct: assumes "wf r" and "⋀x. ∀y. (y, x) ∈ r ⟶ P y ⟹ P x" shows "P a" using assms unfolding wf_def by blast lemmas wfP_induct = wf_induct [to_pred] lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] lemma wf_not_sym: "wf r ⟹ (a, x) ∈ r ⟹ (x, a) ∉ r" by (induct a arbitrary: x set: wf) blast lemma wf_asym: assumes "wf r" "(a, x) ∈ r" obtains "(x, a) ∉ r" by (drule wf_not_sym[OF assms]) lemma wf_not_refl [simp]: "wf r ⟹ (a, a) ∉ r" by (blast elim: wf_asym) lemma wf_irrefl: assumes "wf r" obtains "(a, a) ∉ r" by (drule wf_not_refl[OF assms]) lemma wf_wellorderI: assumes wf: "wf {(x::'a::ord, y). x < y}" and lin: "OFCLASS('a::ord, linorder_class)" shows "OFCLASS('a::ord, wellorder_class)" using lin apply (rule wellorder_class.intro) apply (rule class.wellorder_axioms.intro) apply (rule wf_induct_rule [OF wf]) apply simp done lemma (in wellorder) wf: "wf {(x, y). x < y}" unfolding wf_def by (blast intro: less_induct) subsection ‹Basic Results› text ‹Point-free characterization of well-foundedness› lemma wfE_pf: assumes wf: "wf R" and a: "A ⊆ R `` A" shows "A = {}" proof - from wf have "x ∉ A" for x proof induct fix x assume "⋀y. (y, x) ∈ R ⟹ y ∉ A" then have "x ∉ R `` A" by blast with a show "x ∉ A" by blast qed then show ?thesis by auto qed lemma wfI_pf: assumes a: "⋀A. A ⊆ R `` A ⟹ A = {}" shows "wf R" proof (rule wfUNIVI) fix P :: "'a ⇒ bool" and x let ?A = "{x. ¬ P x}" assume "∀x. (∀y. (y, x) ∈ R ⟶ P y) ⟶ P x" then have "?A ⊆ R `` ?A" by blast with a show "P x" by blast qed subsubsection ‹Minimal-element characterization of well-foundedness› lemma wfE_min: assumes wf: "wf R" and Q: "x ∈ Q" obtains z where "z ∈ Q" "⋀y. (y, z) ∈ R ⟹ y ∉ Q" using Q wfE_pf[OF wf, of Q] by blast lemma wfE_min': "wf R ⟹ Q ≠ {} ⟹ (⋀z. z ∈ Q ⟹ (⋀y. (y, z) ∈ R ⟹ y ∉ Q) ⟹ thesis) ⟹ thesis" using wfE_min[of R _ Q] by blast lemma wfI_min: assumes a: "⋀x Q. x ∈ Q ⟹ ∃z∈Q. ∀y. (y, z) ∈ R ⟶ y ∉ Q" shows "wf R" proof (rule wfI_pf) fix A assume b: "A ⊆ R `` A" have False if "x ∈ A" for x using a[OF that] b by blast then show "A = {}" by blast qed lemma wf_eq_minimal: "wf r ⟷ (∀Q x. x ∈ Q ⟶ (∃z∈Q. ∀y. (y, z) ∈ r ⟶ y ∉ Q))" apply (rule iffI) apply (blast intro: elim!: wfE_min) by (rule wfI_min) auto lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] subsubsection ‹Well-foundedness of transitive closure› lemma wf_trancl: assumes "wf r" shows "wf (r⇧^{+})" proof - have "P x" if induct_step: "⋀x. (⋀y. (y, x) ∈ r⇧^{+}⟹ P y) ⟹ P x" for P x proof (rule induct_step) show "P y" if "(y, x) ∈ r⇧^{+}" for y using ‹wf r› and that proof (induct x arbitrary: y) case (less x) note hyp = ‹⋀x' y'. (x', x) ∈ r ⟹ (y', x') ∈ r⇧^{+}⟹ P y'› from ‹(y, x) ∈ r⇧^{+}› show "P y" proof cases case base show "P y" proof (rule induct_step) fix y' assume "(y', y) ∈ r⇧^{+}" with ‹(y, x) ∈ r› show "P y'" by (rule hyp [of y y']) qed next case step then obtain x' where "(x', x) ∈ r" and "(y, x') ∈ r⇧^{+}" by simp then show "P y" by (rule hyp [of x' y]) qed qed qed then show ?thesis unfolding wf_def by blast qed lemmas wfP_trancl = wf_trancl [to_pred] lemma wf_converse_trancl: "wf (r¯) ⟹ wf ((r⇧^{+})¯)" apply (subst trancl_converse [symmetric]) apply (erule wf_trancl) done text ‹Well-foundedness of subsets› lemma wf_subset: "wf r ⟹ p ⊆ r ⟹ wf p" by (simp add: wf_eq_minimal) fast lemmas wfP_subset = wf_subset [to_pred] text ‹Well-foundedness of the empty relation› lemma wf_empty [iff]: "wf {}" by (simp add: wf_def) lemma wfP_empty [iff]: "wfP (λx y. False)" proof - have "wfP bot" by (fact wf_empty[to_pred bot_empty_eq2]) then show ?thesis by (simp add: bot_fun_def) qed lemma wf_Int1: "wf r ⟹ wf (r ∩ r')" by (erule wf_subset) (rule Int_lower1) lemma wf_Int2: "wf r ⟹ wf (r' ∩ r)" by (erule wf_subset) (rule Int_lower2) text ‹Exponentiation.› lemma wf_exp: assumes "wf (R ^^ n)" shows "wf R" proof (rule wfI_pf) fix A assume "A ⊆ R `` A" then have "A ⊆ (R ^^ n) `` A" by (induct n) force+ with ‹wf (R ^^ n)› show "A = {}" by (rule wfE_pf) qed text ‹Well-foundedness of ‹insert›.› lemma wf_insert [iff]: "wf (insert (y,x) r) ⟷ wf r ∧ (x,y) ∉ r⇧^{*}" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (blast elim: wf_trancl [THEN wf_irrefl] intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN subsetD]) next assume R: ?rhs then have R': "Q ≠ {} ⟹ (∃z∈Q. ∀y. (y, z) ∈ r ⟶ y ∉ Q)" for Q by (auto simp: wf_eq_minimal) show ?lhs unfolding wf_eq_minimal proof clarify fix Q :: "'a set" and q assume "q ∈ Q" then obtain a where "a ∈ Q" and a: "⋀y. (y, a) ∈ r ⟹ y ∉ Q" using R by (auto simp: wf_eq_minimal) show "∃z∈Q. ∀y'. (y', z) ∈ insert (y, x) r ⟶ y' ∉ Q" proof (cases "a=x") case True show ?thesis proof (cases "y ∈ Q") case True then obtain z where "z ∈ Q" "(z, y) ∈ r⇧^{*}" "⋀z'. (z', z) ∈ r ⟶ z' ∈ Q ⟶ (z', y) ∉ r⇧^{*}" using R' [of "{z ∈ Q. (z,y) ∈ r⇧^{*}}"] by auto with R show ?thesis by (rule_tac x="z" in bexI) (blast intro: rtrancl_trans) next case False then show ?thesis using a ‹a ∈ Q› by blast qed next case False with a ‹a ∈ Q› show ?thesis by blast qed qed qed subsubsection ‹Well-foundedness of image› lemma wf_map_prod_image_Dom_Ran: fixes r:: "('a × 'a) set" and f:: "'a ⇒ 'b" assumes wf_r: "wf r" and inj: "⋀ a a'. a ∈ Domain r ⟹ a' ∈ Range r ⟹ f a = f a' ⟹ a = a'" shows "wf (map_prod f f ` r)" proof (unfold wf_eq_minimal, clarify) fix B :: "'b set" and b::"'b" assume "b ∈ B" define A where "A = f -` B ∩ Domain r" show "∃z∈B. ∀y. (y, z) ∈ map_prod f f ` r ⟶ y ∉ B" proof (cases "A = {}") case False then obtain a0 where "a0 ∈ A" and "∀a. (a, a0) ∈ r ⟶ a ∉ A" using wfE_min[OF wf_r] by auto thus ?thesis using inj unfolding A_def by (intro bexI[of _ "f a0"]) auto qed (insert ‹b ∈ B›, unfold A_def, auto) qed lemma wf_map_prod_image: "wf r ⟹ inj f ⟹ wf (map_prod f f ` r)" by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD) subsection ‹Well-Foundedness Results for Unions› lemma wf_union_compatible: assumes "wf R" "wf S" assumes "R O S ⊆ R" shows "wf (R ∪ S)" proof (rule wfI_min) fix x :: 'a and Q let ?Q' = "{x ∈ Q. ∀y. (y, x) ∈ R ⟶ y ∉ Q}" assume "x ∈ Q" obtain a where "a ∈ ?Q'" by (rule wfE_min [OF ‹wf R› ‹x ∈ Q›]) blast with ‹wf S› obtain z where "z ∈ ?Q'" and zmin: "⋀y. (y, z) ∈ S ⟹ y ∉ ?Q'" by (erule wfE_min) have "y ∉ Q" if "(y, z) ∈ S" for y proof from that have "y ∉ ?Q'" by (rule zmin) assume "y ∈ Q" with ‹y ∉ ?Q'› obtain w where "(w, y) ∈ R" and "w ∈ Q" by auto from ‹(w, y) ∈ R› ‹(y, z) ∈ S› have "(w, z) ∈ R O S" by (rule relcompI) with ‹R O S ⊆ R› have "(w, z) ∈ R" .. with ‹z ∈ ?Q'› have "w ∉ Q" by blast with ‹w ∈ Q› show False by contradiction qed with ‹z ∈ ?Q'› show "∃z∈Q. ∀y. (y, z) ∈ R ∪ S ⟶ y ∉ Q" by blast qed text ‹Well-foundedness of indexed union with disjoint domains and ranges.› lemma wf_UN: assumes r: "⋀i. i ∈ I ⟹ wf (r i)" and disj: "⋀i j. ⟦i ∈ I; j ∈ I; r i ≠ r j⟧ ⟹ Domain (r i) ∩ Range (r j) = {}" shows "wf (⋃i∈I. r i)" unfolding wf_eq_minimal proof clarify fix A and a :: "'b" assume "a ∈ A" show "∃z∈A. ∀y. (y, z) ∈ UNION I r ⟶ y ∉ A" proof (cases "∃i∈I. ∃a∈A. ∃b∈A. (b, a) ∈ r i") case True then obtain i b c where ibc: "i ∈ I" "b ∈ A" "c ∈ A" "(c,b) ∈ r i" by blast have ri: "⋀Q. Q ≠ {} ⟹ ∃z∈Q. ∀y. (y, z) ∈ r i ⟶ y ∉ Q" using r [OF ‹i ∈ I›] unfolding wf_eq_minimal by auto show ?thesis using ri [of "{a. a ∈ A ∧ (∃b∈A. (b, a) ∈ r i) }"] ibc disj by blast next case False with ‹a ∈ A› show ?thesis by blast qed qed lemma wfP_SUP: "∀i. wfP (r i) ⟹ ∀i j. r i ≠ r j ⟶ inf (Domainp (r i)) (Rangep (r j)) = bot ⟹ wfP (SUPREMUM UNIV r)" by (rule wf_UN[to_pred]) simp_all lemma wf_Union: assumes "∀r∈R. wf r" and "∀r∈R. ∀s∈R. r ≠ s ⟶ Domain r ∩ Range s = {}" shows "wf (⋃R)" using assms wf_UN[of R "λi. i"] by simp text ‹ Intuition: We find an ‹R ∪ S›-min element of a nonempty subset ‹A› by case distinction. ▸ There is a step ‹a ─R→ b› with ‹a, b ∈ A›. Pick an ‹R›-min element ‹z› of the (nonempty) set ‹{a∈A | ∃b∈A. a ─R→ b}›. By definition, there is ‹z' ∈ A› s.t. ‹z ─R→ z'›. Because ‹z› is ‹R›-min in the subset, ‹z'› must be ‹R›-min in ‹A›. Because ‹z'› has an ‹R›-predecessor, it cannot have an ‹S›-successor and is thus ‹S›-min in ‹A› as well. ▸ There is no such step. Pick an ‹S›-min element of ‹A›. In this case it must be an ‹R›-min element of ‹A› as well. › lemma wf_Un: "wf r ⟹ wf s ⟹ Domain r ∩ Range s = {} ⟹ wf (r ∪ s)" using wf_union_compatible[of s r] by (auto simp: Un_ac) lemma wf_union_merge: "wf (R ∪ S) = wf (R O R ∪ S O R ∪ S)" (is "wf ?A = wf ?B") proof assume "wf ?A" with wf_trancl have wfT: "wf (?A⇧^{+})" . moreover have "?B ⊆ ?A⇧^{+}" by (subst trancl_unfold, subst trancl_unfold) blast ultimately show "wf ?B" by (rule wf_subset) next assume "wf ?B" show "wf ?A" proof (rule wfI_min) fix Q :: "'a set" and x assume "x ∈ Q" with ‹wf ?B› obtain z where "z ∈ Q" and "⋀y. (y, z) ∈ ?B ⟹ y ∉ Q" by (erule wfE_min) then have 1: "⋀y. (y, z) ∈ R O R ⟹ y ∉ Q" and 2: "⋀y. (y, z) ∈ S O R ⟹ y ∉ Q" and 3: "⋀y. (y, z) ∈ S ⟹ y ∉ Q" by auto show "∃z∈Q. ∀y. (y, z) ∈ ?A ⟶ y ∉ Q" proof (cases "∀y. (y, z) ∈ R ⟶ y ∉ Q") case True with ‹z ∈ Q› 3 show ?thesis by blast next case False then obtain z' where "z'∈Q" "(z', z) ∈ R" by blast have "∀y. (y, z') ∈ ?A ⟶ y ∉ Q" proof (intro allI impI) fix y assume "(y, z') ∈ ?A" then show "y ∉ Q" proof assume "(y, z') ∈ R" then have "(y, z) ∈ R O R" using ‹(z', z) ∈ R› .. with 1 show "y ∉ Q" . next assume "(y, z') ∈ S" then have "(y, z) ∈ S O R" using ‹(z', z) ∈ R› .. with 2 show "y ∉ Q" . qed qed with ‹z' ∈ Q› show ?thesis .. qed qed qed lemma wf_comp_self: "wf R ⟷ wf (R O R)" ― ‹special case› by (rule wf_union_merge [where S = "{}", simplified]) subsection ‹Well-Foundedness of Composition› text ‹Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]› lemma qc_wf_relto_iff: assumes "R O S ⊆ (R ∪ S)⇧^{*}O R" ― ‹R quasi-commutes over S› shows "wf (S⇧^{*}O R O S⇧^{*}) ⟷ wf R" (is "wf ?S ⟷ _") proof show "wf R" if "wf ?S" proof - have "R ⊆ ?S" by auto with wf_subset [of ?S] that show "wf R" by auto qed next show "wf ?S" if "wf R" proof (rule wfI_pf) fix A assume A: "A ⊆ ?S `` A" let ?X = "(R ∪ S)⇧^{*}`` A" have *: "R O (R ∪ S)⇧^{*}⊆ (R ∪ S)⇧^{*}O R" proof - have "(x, z) ∈ (R ∪ S)⇧^{*}O R" if "(y, z) ∈ (R ∪ S)⇧^{*}" and "(x, y) ∈ R" for x y z using that proof (induct y z) case rtrancl_refl then show ?case by auto next case (rtrancl_into_rtrancl a b c) then have "(x, c) ∈ ((R ∪ S)⇧^{*}O (R ∪ S)⇧^{*}) O R" using assms by blast then show ?case by simp qed then show ?thesis by auto qed then have "R O S⇧^{*}⊆ (R ∪ S)⇧^{*}O R" using rtrancl_Un_subset by blast then have "?S ⊆ (R ∪ S)⇧^{*}O (R ∪ S)⇧^{*}O R" by (simp add: relcomp_mono rtrancl_mono) also have "… = (R ∪ S)⇧^{*}O R" by (simp add: O_assoc[symmetric]) finally have "?S O (R ∪ S)⇧^{*}⊆ (R ∪ S)⇧^{*}O R O (R ∪ S)⇧^{*}" by (simp add: O_assoc[symmetric] relcomp_mono) also have "… ⊆ (R ∪ S)⇧^{*}O (R ∪ S)⇧^{*}O R" using * by (simp add: relcomp_mono) finally have "?S O (R ∪ S)⇧^{*}⊆ (R ∪ S)⇧^{*}O R" by (simp add: O_assoc[symmetric]) then have "(?S O (R ∪ S)⇧^{*}) `` A ⊆ ((R ∪ S)⇧^{*}O R) `` A" by (simp add: Image_mono) moreover have "?X ⊆ (?S O (R ∪ S)⇧^{*}) `` A" using A by (auto simp: relcomp_Image) ultimately have "?X ⊆ R `` ?X" by (auto simp: relcomp_Image) then have "?X = {}" using ‹wf R› by (simp add: wfE_pf) moreover have "A ⊆ ?X" by auto ultimately show "A = {}" by simp qed qed corollary wf_relcomp_compatible: assumes "wf R" and "R O S ⊆ S O R" shows "wf (S O R)" proof - have "R O S ⊆ (R ∪ S)⇧^{*}O R" using assms by blast then have "wf (S⇧^{*}O R O S⇧^{*})" by (simp add: assms qc_wf_relto_iff) then show ?thesis by (rule Wellfounded.wf_subset) blast qed subsection ‹Acyclic relations› lemma wf_acyclic: "wf r ⟹ acyclic r" by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl]) lemmas wfP_acyclicP = wf_acyclic [to_pred] subsubsection ‹Wellfoundedness of finite acyclic relations› lemma finite_acyclic_wf: assumes "finite r" "acyclic r" shows "wf r" using assms proof (induction r rule: finite_induct) case (insert x r) then show ?case by (cases x) simp qed simp lemma finite_acyclic_wf_converse: "finite r ⟹ acyclic r ⟹ wf (r¯)" apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) apply (erule acyclic_converse [THEN iffD2]) done text ‹ Observe that the converse of an irreflexive, transitive, and finite relation is again well-founded. Thus, we may employ it for well-founded induction. › lemma wf_converse: assumes "irrefl r" and "trans r" and "finite r" shows "wf (r¯)" proof - have "acyclic r" using ‹irrefl r› and ‹trans r› by (simp add: irrefl_def acyclic_irrefl) with ‹finite r› show ?thesis by (rule finite_acyclic_wf_converse) qed lemma wf_iff_acyclic_if_finite: "finite r ⟹ wf r = acyclic r" by (blast intro: finite_acyclic_wf wf_acyclic) subsection ‹@{typ nat} is well-founded› lemma less_nat_rel: "(<) = (λm n. n = Suc m)⇧^{+}⇧^{+}" proof (rule ext, rule ext, rule iffI) fix n m :: nat show "(λm n. n = Suc m)⇧^{+}⇧^{+}m n" if "m < n" using that proof (induct n) case 0 then show ?case by auto next case (Suc n) then show ?case by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) qed show "m < n" if "(λm n. n = Suc m)⇧^{+}⇧^{+}m n" using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less) qed definition pred_nat :: "(nat × nat) set" where "pred_nat = {(m, n). n = Suc m}" definition less_than :: "(nat × nat) set" where "less_than = pred_nat⇧^{+}" lemma less_eq: "(m, n) ∈ pred_nat⇧^{+}⟷ m < n" unfolding less_nat_rel pred_nat_def trancl_def by simp lemma pred_nat_trancl_eq_le: "(m, n) ∈ pred_nat⇧^{*}⟷ m ≤ n" unfolding less_eq rtrancl_eq_or_trancl by auto lemma wf_pred_nat: "wf pred_nat" apply (unfold wf_def pred_nat_def) apply clarify apply (induct_tac x) apply blast+ done lemma wf_less_than [iff]: "wf less_than" by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) lemma trans_less_than [iff]: "trans less_than" by (simp add: less_than_def) lemma less_than_iff [iff]: "((x,y) ∈ less_than) = (x<y)" by (simp add: less_than_def less_eq) lemma wf_less: "wf {(x, y::nat). x < y}" by (rule Wellfounded.wellorder_class.wf) subsection ‹Accessible Part› text ‹ Inductive definition of the accessible part ‹acc r› of a relation; see also @{cite "paulin-tlca"}. › inductive_set acc :: "('a × 'a) set ⇒ 'a set" for r :: "('a × 'a) set" where accI: "(⋀y. (y, x) ∈ r ⟹ y ∈ acc r) ⟹ x ∈ acc r" abbreviation termip :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" where "termip r ≡ accp (r¯¯)" abbreviation termi :: "('a × 'a) set ⇒ 'a set" where "termi r ≡ acc (r¯)" lemmas accpI = accp.accI lemma accp_eq_acc [code]: "accp r = (λx. x ∈ Wellfounded.acc {(x, y). r x y})" by (simp add: acc_def) text ‹Induction rules› theorem accp_induct: assumes major: "accp r a" assumes hyp: "⋀x. accp r x ⟹ ∀y. r y x ⟶ P y ⟹ P x" shows "P a" apply (rule major [THEN accp.induct]) apply (rule hyp) apply (rule accp.accI) apply auto done lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] theorem accp_downward: "accp r b ⟹ r a b ⟹ accp r a" by (cases rule: accp.cases) lemma not_accp_down: assumes na: "¬ accp R x" obtains z where "R z x" and "¬ accp R z" proof - assume a: "⋀z. R z x ⟹ ¬ accp R z ⟹ thesis" show thesis proof (cases "∀z. R z x ⟶ accp R z") case True then have "⋀z. R z x ⟹ accp R z" by auto then have "accp R x" by (rule accp.accI) with na show thesis .. next case False then obtain z where "R z x" and "¬ accp R z" by auto with a show thesis . qed qed lemma accp_downwards_aux: "r⇧^{*}⇧^{*}b a ⟹ accp r a ⟶ accp r b" by (erule rtranclp_induct) (blast dest: accp_downward)+ theorem accp_downwards: "accp r a ⟹ r⇧^{*}⇧^{*}b a ⟹ accp r b" by (blast dest: accp_downwards_aux) theorem accp_wfPI: "∀x. accp r x ⟹ wfP r" apply (rule wfPUNIVI) apply (rule_tac P = P in accp_induct) apply blast+ done theorem accp_wfPD: "wfP r ⟹ accp r x" apply (erule wfP_induct_rule) apply (rule accp.accI) apply blast done theorem wfP_accp_iff: "wfP r = (∀x. accp r x)" by (blast intro: accp_wfPI dest: accp_wfPD) text ‹Smaller relations have bigger accessible parts:› lemma accp_subset: assumes "R1 ≤ R2" shows "accp R2 ≤ accp R1" proof (rule predicate1I) fix x assume "accp R2 x" then show "accp R1 x" proof (induct x) fix x assume "⋀y. R2 y x ⟹ accp R1 y" with assms show "accp R1 x" by (blast intro: accp.accI) qed qed text ‹This is a generalized induction theorem that works on subsets of the accessible part.› lemma accp_subset_induct: assumes subset: "D ≤ accp R" and dcl: "⋀x z. D x ⟹ R z x ⟹ D z" and "D x" and istep: "⋀x. D x ⟹ (⋀z. R z x ⟹ P z) ⟹ P x" shows "P x" proof - from subset and ‹D x› have "accp R x" .. then show "P x" using ‹D x› proof (induct x) fix x assume "D x" and "⋀y. R y x ⟹ D y ⟹ P y" with dcl and istep show "P x" by blast qed qed text ‹Set versions of the above theorems› lemmas acc_induct = accp_induct [to_set] lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] lemmas acc_downward = accp_downward [to_set] lemmas not_acc_down = not_accp_down [to_set] lemmas acc_downwards_aux = accp_downwards_aux [to_set] lemmas acc_downwards = accp_downwards [to_set] lemmas acc_wfI = accp_wfPI [to_set] lemmas acc_wfD = accp_wfPD [to_set] lemmas wf_acc_iff = wfP_accp_iff [to_set] lemmas acc_subset = accp_subset [to_set] lemmas acc_subset_induct = accp_subset_induct [to_set] subsection ‹Tools for building wellfounded relations› text ‹Inverse Image› lemma wf_inv_image [simp,intro!]: "wf r ⟹ wf (inv_image r f)" for f :: "'a ⇒ 'b" apply (simp add: inv_image_def wf_eq_minimal) apply clarify apply (subgoal_tac "∃w::'b. w ∈ {w. ∃x::'a. x ∈ Q ∧ f x = w}") prefer 2 apply (blast del: allE) apply (erule allE) apply (erule (1) notE impE) apply blast done text ‹Measure functions into @{typ nat}› definition measure :: "('a ⇒ nat) ⇒ ('a × 'a) set" where "measure = inv_image less_than" lemma in_measure[simp, code_unfold]: "(x, y) ∈ measure f ⟷ f x < f y" by (simp add:measure_def) lemma wf_measure [iff]: "wf (measure f)" unfolding measure_def by (rule wf_less_than [THEN wf_inv_image]) lemma wf_if_measure: "(⋀x. P x ⟹ f(g x) < f x) ⟹ wf {(y,x). P x ∧ y = g x}" for f :: "'a ⇒ nat" using wf_measure[of f] unfolding measure_def inv_image_def less_than_def less_eq by (rule wf_subset) auto subsubsection ‹Lexicographic combinations› definition lex_prod :: "('a ×'a) set ⇒ ('b × 'b) set ⇒ (('a × 'b) × ('a × 'b)) set" (infixr "<*lex*>" 80) where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') ∈ ra ∨ a = a' ∧ (b, b') ∈ rb}" lemma wf_lex_prod [intro!]: "wf ra ⟹ wf rb ⟹ wf (ra <*lex*> rb)" unfolding wf_def lex_prod_def apply (rule allI) apply (rule impI) apply (simp only: split_paired_All) apply (drule spec) apply (erule mp) apply (rule allI) apply (rule impI) apply (drule spec) apply (erule mp) apply blast done lemma in_lex_prod[simp]: "((a, b), (a', b')) ∈ r <*lex*> s ⟷ (a, a') ∈ r ∨ a = a' ∧ (b, b') ∈ s" by (auto simp:lex_prod_def) text ‹‹<*lex*>› preserves transitivity› lemma trans_lex_prod [intro!]: "trans R1 ⟹ trans R2 ⟹ trans (R1 <*lex*> R2)" unfolding trans_def lex_prod_def by blast text ‹lexicographic combinations with measure functions› definition mlex_prod :: "('a ⇒ nat) ⇒ ('a × 'a) set ⇒ ('a × 'a) set" (infixr "<*mlex*>" 80) where "f <*mlex*> R = inv_image (less_than <*lex*> R) (λx. (f x, x))" lemma wf_mlex: "wf R ⟹ wf (f <*mlex*> R)" and mlex_less: "f x < f y ⟹ (x, y) ∈ f <*mlex*> R" and mlex_leq: "f x ≤ f y ⟹ (x, y) ∈ R ⟹ (x, y) ∈ f <*mlex*> R" and mlex_iff: "(x, y) ∈ f <*mlex*> R ⟷ f x < f y ∨ f x = f y ∧ (x, y) ∈ R" by (auto simp: mlex_prod_def) text ‹Proper subset relation on finite sets.› definition finite_psubset :: "('a set × 'a set) set" where "finite_psubset = {(A, B). A ⊂ B ∧ finite B}" lemma wf_finite_psubset[simp]: "wf finite_psubset" apply (unfold finite_psubset_def) apply (rule wf_measure [THEN wf_subset]) apply (simp add: measure_def inv_image_def less_than_def less_eq) apply (fast elim!: psubset_card_mono) done lemma trans_finite_psubset: "trans finite_psubset" by (auto simp: finite_psubset_def less_le trans_def) lemma in_finite_psubset[simp]: "(A, B) ∈ finite_psubset ⟷ A ⊂ B ∧ finite B" unfolding finite_psubset_def by auto text ‹max- and min-extension of order to finite sets› inductive_set max_ext :: "('a × 'a) set ⇒ ('a set × 'a set) set" for R :: "('a × 'a) set" where max_extI[intro]: "finite X ⟹ finite Y ⟹ Y ≠ {} ⟹ (⋀x. x ∈ X ⟹ ∃y∈Y. (x, y) ∈ R) ⟹ (X, Y) ∈ max_ext R" lemma max_ext_wf: assumes wf: "wf r" shows "wf (max_ext r)" proof (rule acc_wfI, intro allI) show "M ∈ acc (max_ext r)" (is "_ ∈ ?W") for M proof (induct M rule: infinite_finite_induct) case empty show ?case by (rule accI) (auto elim: max_ext.cases) next case (insert a M) from wf ‹M ∈ ?W› ‹finite M› show "insert a M ∈ ?W" proof (induct arbitrary: M) fix M a assume "M ∈ ?W" assume [intro]: "finite M" assume hyp: "⋀b M. (b, a) ∈ r ⟹ M ∈ ?W ⟹ finite M ⟹ insert b M ∈ ?W" have add_less: "M ∈ ?W ⟹ (⋀y. y ∈ N ⟹ (y, a) ∈ r) ⟹ N ∪ M ∈ ?W" if "finite N" "finite M" for N M :: "'a set" using that by (induct N arbitrary: M) (auto simp: hyp) show "insert a M ∈ ?W" proof (rule accI) fix N assume Nless: "(N, insert a M) ∈ max_ext r" then have *: "⋀x. x ∈ N ⟹ (x, a) ∈ r ∨ (∃y ∈ M. (x, y) ∈ r)" by (auto elim!: max_ext.cases) let ?N1 = "{n ∈ N. (n, a) ∈ r}" let ?N2 = "{n ∈ N. (n, a) ∉ r}" have N: "?N1 ∪ ?N2 = N" by (rule set_eqI) auto from Nless have "finite N" by (auto elim: max_ext.cases) then have finites: "finite ?N1" "finite ?N2" by auto have "?N2 ∈ ?W" proof (cases "M = {}") case [simp]: True have Mw: "{} ∈ ?W" by (rule accI) (auto elim: max_ext.cases) from * have "?N2 = {}" by auto with Mw show "?N2 ∈ ?W" by (simp only:) next case False from * finites have N2: "(?N2, M) ∈ max_ext r" by (rule_tac max_extI[OF _ _ ‹M ≠ {}›]) auto with ‹M ∈ ?W› show "?N2 ∈ ?W" by (rule acc_downward) qed with finites have "?N1 ∪ ?N2 ∈ ?W" by (rule add_less) simp then show "N ∈ ?W" by (simp only: N) qed qed next case infinite show ?case by (rule accI) (auto elim: max_ext.cases simp: infinite) qed qed lemma max_ext_additive: "(A, B) ∈ max_ext R ⟹ (C, D) ∈ max_ext R ⟹ (A ∪ C, B ∪ D) ∈ max_ext R" by (force elim!: max_ext.cases) definition min_ext :: "('a × 'a) set ⇒ ('a set × 'a set) set" where "min_ext r = {(X, Y) | X Y. X ≠ {} ∧ (∀y ∈ Y. (∃x ∈ X. (x, y) ∈ r))}" lemma min_ext_wf: assumes "wf r" shows "wf (min_ext r)" proof (rule wfI_min) show "∃m ∈ Q. (∀n. (n, m) ∈ min_ext r ⟶ n ∉ Q)" if nonempty: "x ∈ Q" for Q :: "'a set set" and x proof (cases "Q = {{}}") case True then show ?thesis by (simp add: min_ext_def) next case False with nonempty obtain e x where "x ∈ Q" "e ∈ x" by force then have eU: "e ∈ ⋃Q" by auto with ‹wf r› obtain z where z: "z ∈ ⋃Q" "⋀y. (y, z) ∈ r ⟹ y ∉ ⋃Q" by (erule wfE_min) from z obtain m where "m ∈ Q" "z ∈ m" by auto from ‹m ∈ Q› show ?thesis proof (intro rev_bexI allI impI) fix n assume smaller: "(n, m) ∈ min_ext r" with ‹z ∈ m› obtain y where "y ∈ n" "(y, z) ∈ r" by (auto simp: min_ext_def) with z(2) show "n ∉ Q" by auto qed qed qed subsubsection ‹Bounded increase must terminate› lemma wf_bounded_measure: fixes ub :: "'a ⇒ nat" and f :: "'a ⇒ nat" assumes "⋀a b. (b, a) ∈ r ⟹ ub b ≤ ub a ∧ ub a ≥ f b ∧ f b > f a" shows "wf r" by (rule wf_subset[OF wf_measure[of "λa. ub a - f a"]]) (auto dest: assms) lemma wf_bounded_set: fixes ub :: "'a ⇒ 'b set" and f :: "'a ⇒ 'b set" assumes "⋀a b. (b,a) ∈ r ⟹ finite (ub a) ∧ ub b ⊆ ub a ∧ ub a ⊇ f b ∧ f b ⊃ f a" shows "wf r" apply (rule wf_bounded_measure[of r "λa. card (ub a)" "λa. card (f a)"]) apply (drule assms) apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) done lemma finite_subset_wf: assumes "finite A" shows "wf {(X, Y). X ⊂ Y ∧ Y ⊆ A}" by (rule wf_subset[OF wf_finite_psubset[unfolded finite_psubset_def]]) (auto intro: finite_subset[OF _ assms]) hide_const (open) acc accp end