Theory Open_Induction.Restricted_Predicates

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Binary Predicates Restricted to Elements of a Given Set›

theory Restricted_Predicates
imports Main
begin

text ‹
  A subset ‹C› of ‹A› is a \emph{chain} on ‹A› (w.r.t.\ ‹P›)
  iff for all pairs of elements of ‹C›, one is less than or equal
  to the other one.
›
abbreviation "chain_on P C A ≡ pred_on.chain A P C"
lemmas chain_on_def = pred_on.chain_def

lemma chain_on_subset:
  "A ⊆ B ⟹ chain_on P C A ⟹ chain_on P C B"
by (force simp: chain_on_def)

lemma chain_on_imp_subset:
  "chain_on P C A ⟹ C ⊆ A"
by (simp add: chain_on_def)

lemma subchain_on:
  assumes "C ⊆ D" and "chain_on P D A"
  shows "chain_on P C A"
using assms by (auto simp: chain_on_def)

definition restrict_to :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ ('a ⇒ 'a ⇒ bool)" where
  "restrict_to P A = (λx y. x ∈ A ∧ y ∈ A ∧ P x y)"

abbreviation "strict P ≡ λx y. P x y ∧ ¬ (P y x)"

abbreviation "incomparable P ≡ λx y. ¬ P x y ∧ ¬ P y x"

abbreviation "antichain_on P f A ≡ ∀(i::nat) j. f i ∈ A ∧ (i < j ⟶ incomparable P (f i) (f j))"

lemma strict_reflclp_conv [simp]:
  "strict (P⇧=⇧=) = strict P" by auto

lemma reflp_on_reflclp_simp [simp]:
  assumes "reflp_on A P" and "a ∈ A" and "b ∈ A"
  shows "P⇧=⇧= a b = P a b"
  using assms by (auto simp: reflp_on_def)

lemmas reflp_on_converse_simp = reflp_on_conversp
lemmas irreflp_on_converse_simp = irreflp_on_converse
lemmas transp_on_converse_simp = transp_on_conversep

lemma transp_on_strict:
  "transp_on A P ⟹ transp_on A (strict P)"
  unfolding transp_on_def by blast

definition wfp_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where
  "wfp_on P A ⟷ ¬ (∃f. ∀i. f i ∈ A ∧ P (f (Suc i)) (f i))"

definition inductive_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
  "inductive_on P A ⟷ (∀Q. (∀y∈A. (∀x∈A. P x y ⟶ Q x) ⟶ Q y) ⟶ (∀x∈A. Q x))"

lemma inductive_onI [Pure.intro]:
  assumes "⋀Q x. ⟦x ∈ A; (⋀y. ⟦y ∈ A; ⋀x. ⟦x ∈ A; P x y⟧ ⟹ Q x⟧ ⟹ Q y)⟧ ⟹  Q x"
  shows "inductive_on P A"
  using assms unfolding inductive_on_def by metis

text ‹
  If @{term P} is well-founded on @{term A} then every non-empty subset @{term Q} of @{term A} has a
  minimal element @{term z} w.r.t. @{term P}, i.e., all elements that are @{term P}-smaller than
  @{term z} are not in @{term Q}.
›
lemma wfp_on_imp_minimal:
  assumes "wfp_on P A"
  shows "∀Q x. x ∈ Q ∧ Q ⊆ A ⟶ (∃z∈Q. ∀y. P y z ⟶ y ∉ Q)"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain Q x where *: "x ∈ Q" "Q ⊆ A"
    and "∀z. ∃y. z ∈ Q ⟶ P y z ∧ y ∈ Q" by metis
  from choice [OF this(3)] obtain f
    where **: "∀x∈Q. P (f x) x ∧ f x ∈ Q" by blast
  let ?S = "λi. (f ^^ i) x"
  have ***: "∀i. ?S i ∈ Q"
  proof
    fix i show "?S i ∈ Q" by (induct i) (auto simp: * **)
  qed
  then have "∀i. ?S i ∈ A" using * by blast
  moreover have "∀i. P (?S (Suc i)) (?S i)"
  proof
    fix i show "P (?S (Suc i)) (?S i)"
      by (induct i) (auto simp: * ** ***)
  qed
  ultimately have "∀i. ?S i ∈ A ∧ P (?S (Suc i)) (?S i)" by blast
  with assms(1) show False
    unfolding wfp_on_def by fast
qed

lemma minimal_imp_inductive_on:
  assumes "∀Q x. x ∈ Q ∧ Q ⊆ A ⟶ (∃z∈Q. ∀y. P y z ⟶ y ∉ Q)"
  shows "inductive_on P A"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain Q x
    where *: "∀y∈A. (∀x∈A. P x y ⟶ Q x) ⟶ Q y"
    and **: "x ∈ A" "¬ Q x"
    by (auto simp: inductive_on_def)
  let ?Q = "{x∈A. ¬ Q x}"
  from ** have "x ∈ ?Q" by auto
  moreover have "?Q ⊆ A" by auto
  ultimately obtain z where "z ∈ ?Q"
    and min: "∀y. P y z ⟶ y ∉ ?Q"
    using assms [THEN spec [of _ ?Q], THEN spec [of _ x]] by blast
  from ‹z ∈ ?Q› have "z ∈ A" and "¬ Q z" by auto
  with * obtain y where "y ∈ A" and "P y z" and "¬ Q y" by auto
  then have "y ∈ ?Q" by auto
  with ‹P y z› and min show False by auto
qed

lemmas wfp_on_imp_inductive_on =
  wfp_on_imp_minimal [THEN minimal_imp_inductive_on]

lemma inductive_on_induct [consumes 2, case_names less, induct pred: inductive_on]:
  assumes "inductive_on P A" and "x ∈ A"
    and "⋀y. ⟦ y ∈ A; ⋀x. ⟦ x ∈ A; P x y ⟧ ⟹ Q x ⟧ ⟹ Q y"
  shows "Q x"
  using assms unfolding inductive_on_def by metis

lemma inductive_on_imp_wfp_on:
  assumes "inductive_on P A"
  shows "wfp_on P A"
proof -
  let ?Q = "λx. ¬ (∃f. f 0 = x ∧ (∀i. f i ∈ A ∧ P (f (Suc i)) (f i)))"
  { fix x assume "x ∈ A"
    with assms have "?Q x"
    proof (induct rule: inductive_on_induct)
      fix y assume "y ∈ A" and IH: "⋀x. x ∈ A ⟹ P x y ⟹ ?Q x"
      show "?Q y"
      proof (rule ccontr)
        assume "¬ ?Q y"
        then obtain f where *: "f 0 = y"
          "∀i. f i ∈ A ∧ P (f (Suc i)) (f i)" by auto
        then have "P (f (Suc 0)) (f 0)" and "f (Suc 0) ∈ A" by auto
        with IH and * have "?Q (f (Suc 0))" by auto
        with * show False by auto
      qed
    qed }
  then show ?thesis unfolding wfp_on_def by blast
qed

definition qo_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
  "qo_on P A ⟷ reflp_on A P ∧ transp_on A P"

definition po_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
  "po_on P A ⟷ (irreflp_on A P ∧ transp_on A P)"

lemma po_onI [Pure.intro]:
  "⟦irreflp_on A P; transp_on A P⟧ ⟹ po_on P A"
  by (auto simp: po_on_def)

lemma po_on_converse_simp [simp]:
  "po_on P¯¯ A ⟷ po_on P A"
  by (simp add: po_on_def)

lemma po_on_imp_qo_on:
  "po_on P A ⟹ qo_on (P⇧=⇧=) A"
  unfolding po_on_def qo_on_def
  by (metis reflp_on_reflclp transp_on_reflclp)

lemma po_on_imp_irreflp_on:
  "po_on P A ⟹ irreflp_on A P"
  by (auto simp: po_on_def)

lemma po_on_imp_transp_on:
  "po_on P A ⟹ transp_on A P"
  by (auto simp: po_on_def)

lemma po_on_subset:
  assumes "A ⊆ B" and "po_on P B"
  shows "po_on P A"
  using transp_on_subset and irreflp_on_subset and assms
  unfolding po_on_def by blast

lemma transp_on_irreflp_on_imp_antisymp_on:
  assumes "transp_on A P" and "irreflp_on A P"
  shows "antisymp_on A (P⇧=⇧=)"
proof (rule antisymp_onI)
  fix a b assume "a ∈ A"
    and "b ∈ A" and "P⇧=⇧= a b" and "P⇧=⇧= b a"
  show "a = b"
  proof (rule ccontr)
    assume "a ≠ b"
    with ‹P⇧=⇧= a b› and ‹P⇧=⇧= b a› have "P a b" and "P b a" by auto
    with ‹transp_on A P› and ‹a ∈ A› and ‹b ∈ A› have "P a a" unfolding transp_on_def by blast
    with ‹irreflp_on A P› and ‹a ∈ A› show False unfolding irreflp_on_def by blast
  qed
qed

lemma po_on_imp_antisymp_on:
  assumes "po_on P A"
  shows "antisymp_on A P"
using transp_on_irreflp_on_imp_antisymp_on [of A P] and assms by (auto simp: po_on_def)

lemma strict_reflclp [simp]:
  assumes "x ∈ A" and "y ∈ A"
    and "transp_on A P" and "irreflp_on A P"
  shows "strict (P⇧=⇧=) x y = P x y"
  using assms unfolding transp_on_def irreflp_on_def
  by blast

lemma qo_on_imp_reflp_on:
  "qo_on P A ⟹ reflp_on A P"
  by (auto simp: qo_on_def)

lemma qo_on_imp_transp_on:
  "qo_on P A ⟹ transp_on A P"
  by (auto simp: qo_on_def)

lemma qo_on_subset:
  "A ⊆ B ⟹ qo_on P B ⟹ qo_on P A"
  unfolding qo_on_def
  using reflp_on_subset
    and transp_on_subset by blast

text ‹
  Quasi-orders are instances of the @{class preorder} class.
›
lemma qo_on_UNIV_conv:
  "qo_on P UNIV ⟷ class.preorder P (strict P)" (is "?lhs = ?rhs")
proof
  assume "?lhs" then show "?rhs"
    unfolding qo_on_def class.preorder_def
    using qo_on_imp_reflp_on [of P UNIV]
      and qo_on_imp_transp_on [of P UNIV]
    by (auto simp: reflp_on_def) (unfold transp_on_def, blast)
next
  assume "?rhs" then show "?lhs"
    unfolding class.preorder_def
    by (auto simp: qo_on_def reflp_on_def transp_on_def)
qed

lemma wfp_on_iff_inductive_on:
  "wfp_on P A ⟷ inductive_on P A"
  by (blast intro: inductive_on_imp_wfp_on wfp_on_imp_inductive_on)

lemma wfp_on_iff_minimal:
  "wfp_on P A ⟷ (∀Q x.
     x ∈ Q ∧ Q ⊆ A ⟶
     (∃z∈Q. ∀y. P y z ⟶ y ∉ Q))"
  using wfp_on_imp_minimal [of P A]
    and minimal_imp_inductive_on [of A P]
    and inductive_on_imp_wfp_on [of P A]
    by blast

text ‹
  Every non-empty well-founded set @{term A} has a minimal element, i.e., an element that is not
  greater than any other element.
›
lemma wfp_on_imp_has_min_elt:
  assumes "wfp_on P A" and "A ≠ {}"
  shows "∃x∈A. ∀y∈A. ¬ P y x"
  using assms unfolding wfp_on_iff_minimal by force

lemma wfp_on_induct [consumes 2, case_names less, induct pred: wfp_on]:
  assumes "wfp_on P A" and "x ∈ A"
    and "⋀y. ⟦ y ∈ A; ⋀x. ⟦ x ∈ A; P x y ⟧ ⟹ Q x ⟧ ⟹ Q y"
  shows "Q x"
  using assms and inductive_on_induct [of P A x]
  unfolding wfp_on_iff_inductive_on by blast

lemma wfp_on_UNIV [simp]:
  "wfp_on P UNIV ⟷ wfP P"
  unfolding wfp_on_iff_inductive_on inductive_on_def wfP_def wf_def by force


subsection ‹Measures on Sets (Instead of Full Types)›

definition
  inv_image_betw ::
    "('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ ('a ⇒ 'a ⇒ bool)"
where
  "inv_image_betw P f A B = (λx y. x ∈ A ∧ y ∈ A ∧ f x ∈ B ∧ f y ∈ B ∧ P (f x) (f y))"

definition
  measure_on :: "('a ⇒ nat) ⇒ 'a set ⇒ 'a ⇒ 'a ⇒ bool"
where
  "measure_on f A = inv_image_betw (<) f A UNIV"

lemma in_inv_image_betw [simp]:
  "inv_image_betw P f A B x y ⟷ x ∈ A ∧ y ∈ A ∧ f x ∈ B ∧ f y ∈ B ∧ P (f x) (f y)"
  by (auto simp: inv_image_betw_def)

lemma in_measure_on [simp, code_unfold]:
  "measure_on f A x y ⟷ x ∈ A ∧ y ∈ A ∧ f x < f y"
  by (simp add: measure_on_def)

lemma wfp_on_inv_image_betw [simp, intro!]:
  assumes "wfp_on P B"
  shows "wfp_on (inv_image_betw P f A B) A" (is "wfp_on ?P A")
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain g where "∀i. g i ∈ A ∧ ?P (g (Suc i)) (g i)" by (auto simp: wfp_on_def)
  with assms show False by (auto simp: wfp_on_def)
qed

lemma wfp_less:
  "wfp_on (<) (UNIV :: nat set)"
  using wf_less by (auto simp: wfP_def)

lemma wfp_on_measure_on [iff]:
  "wfp_on (measure_on f A) A"
  unfolding measure_on_def
  by (rule wfp_less [THEN wfp_on_inv_image_betw])

lemma wfp_on_mono:
  "A ⊆ B ⟹ (⋀x y. x ∈ A ⟹ y ∈ A ⟹ P x y ⟹ Q x y) ⟹ wfp_on Q B ⟹ wfp_on P A"
  unfolding wfp_on_def by (metis subsetD)

lemma wfp_on_subset:
  "A ⊆ B ⟹ wfp_on P B ⟹ wfp_on P A"
  using wfp_on_mono by blast

lemma restrict_to_iff [iff]:
  "restrict_to P A x y ⟷ x ∈ A ∧ y ∈ A ∧ P x y"
  by (simp add: restrict_to_def)

lemma wfp_on_restrict_to [simp]:
  "wfp_on (restrict_to P A) A = wfp_on P A"
  by (auto simp: wfp_on_def)

lemma irreflp_on_strict [simp, intro]:
  "irreflp_on A (strict P)"
  by (auto simp: irreflp_on_def)

lemma transp_on_map':
  assumes "transp_on B Q"
    and "g ` A ⊆ B"
    and "h ` A ⊆ B"
    and "⋀x. x ∈ A ⟹ Q⇧=⇧= (h x) (g x)"
  shows "transp_on A (λx y. Q (g x) (h y))"
  using assms unfolding transp_on_def
  by auto (metis imageI subsetD)

lemma transp_on_map:
  assumes "transp_on B Q"
    and "h ` A ⊆ B"
  shows "transp_on A (λx y. Q (h x) (h y))"
  using transp_on_map' [of B Q h A h, simplified, OF assms] by blast

lemma irreflp_on_map:
  assumes "irreflp_on B Q"
    and "h ` A ⊆ B"
  shows "irreflp_on A (λx y. Q (h x) (h y))"
  using assms unfolding irreflp_on_def by auto

lemma po_on_map:
  assumes "po_on Q B"
    and "h ` A ⊆ B"
  shows "po_on (λx y. Q (h x) (h y)) A"
  using assms and transp_on_map and irreflp_on_map
  unfolding po_on_def by auto

lemma chain_transp_on_less:
  assumes "∀i. f i ∈ A ∧ P (f i) (f (Suc i))" and "transp_on A P" and "i < j"
  shows "P (f i) (f j)"
using ‹i < j›
proof (induct j)
  case 0 then show ?case by simp
next
  case (Suc j)
  show ?case
  proof (cases "i = j")
    case True
    with Suc show ?thesis using assms(1) by simp
  next
    case False
    with Suc have "P (f i) (f j)" by force
    moreover from assms have "P (f j) (f (Suc j))" by auto
    ultimately show ?thesis using assms(1, 2) unfolding transp_on_def by blast
  qed
qed

lemma wfp_on_imp_irreflp_on:
  assumes "wfp_on P A"
  shows "irreflp_on A P"
proof (rule irreflp_onI)
  fix x
  assume "x ∈ A"
  show "¬ P x x"
  proof
    let ?f = "λ_. x"
    assume "P x x"
    then have "∀i. P (?f (Suc i)) (?f i)" by blast
    with ‹x ∈ A› have "¬ wfp_on P A" by (auto simp: wfp_on_def)
    with assms show False by contradiction
  qed
qed

inductive
  accessible_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a ⇒ bool"
  for P and A
where
  accessible_onI [Pure.intro]:
    "⟦x ∈ A; ⋀y. ⟦y ∈ A; P y x⟧ ⟹ accessible_on P A y⟧ ⟹ accessible_on P A x"

lemma accessible_on_imp_mem:
  assumes "accessible_on P A a"
  shows "a ∈ A"
  using assms by (induct) auto

lemma accessible_on_induct [consumes 1, induct pred: accessible_on]:
  assumes *: "accessible_on P A a"
    and IH: "⋀x. ⟦accessible_on P A x; ⋀y. ⟦y ∈ A; P y x⟧ ⟹ Q y⟧ ⟹ Q x"
  shows "Q a"
  by (rule * [THEN accessible_on.induct]) (auto intro: IH accessible_onI)

lemma accessible_on_downward:
  "accessible_on P A b ⟹ a ∈ A ⟹ P a b ⟹ accessible_on P A a"
  by (cases rule: accessible_on.cases) fast

lemma accessible_on_restrict_to_downwards:
  assumes "(restrict_to P A)⇧+⇧+ a b" and "accessible_on P A b"
  shows "accessible_on P A a"
  using assms by (induct) (auto dest: accessible_on_imp_mem accessible_on_downward)

lemma accessible_on_imp_inductive_on:
  assumes "∀x∈A. accessible_on P A x"
  shows "inductive_on P A"
proof
  fix Q x
  assume "x ∈ A"
    and *: "⋀y. ⟦y ∈ A; ⋀x. ⟦x ∈ A; P x y⟧ ⟹ Q x⟧ ⟹ Q y"
  with assms have "accessible_on P A x" by auto
  then show "Q x"
  proof (induct)
    case (1 z)
    then have "z ∈ A" by (blast dest: accessible_on_imp_mem)
    show ?case by (rule *) fact+
  qed
qed

lemmas accessible_on_imp_wfp_on = accessible_on_imp_inductive_on [THEN inductive_on_imp_wfp_on]

lemma wfp_on_tranclp_imp_wfp_on:
  assumes "wfp_on (P⇧+⇧+) A"
  shows "wfp_on P A"
  by (rule ccontr) (insert assms, auto simp: wfp_on_def)

lemma inductive_on_imp_accessible_on:
  assumes "inductive_on P A"
  shows "∀x∈A. accessible_on P A x"
proof
  fix x
  assume "x ∈ A"
  with assms show "accessible_on P A x"
    by (induct) (auto intro: accessible_onI)
qed

lemma inductive_on_accessible_on_conv:
  "inductive_on P A ⟷ (∀x∈A. accessible_on P A x)"
  using inductive_on_imp_accessible_on
    and accessible_on_imp_inductive_on
    by blast

lemmas wfp_on_imp_accessible_on =
  wfp_on_imp_inductive_on [THEN inductive_on_imp_accessible_on]

lemma wfp_on_accessible_on_iff:
  "wfp_on P A ⟷ (∀x∈A. accessible_on P A x)"
  by (blast dest: wfp_on_imp_accessible_on accessible_on_imp_wfp_on)

lemma accessible_on_tranclp:
  assumes "accessible_on P A x"
  shows "accessible_on ((restrict_to P A)⇧+⇧+) A x"
    (is "accessible_on ?P A x")
  using assms
proof (induct)
  case (1 x)
  then have "x ∈ A" by (blast dest: accessible_on_imp_mem)
  then show ?case
  proof (rule accessible_onI)
    fix y
    assume "y ∈ A"
    assume "?P y x"
    then show "accessible_on ?P A y"
    proof (cases)
      assume "restrict_to P A y x"
      with 1 and ‹y ∈ A› show ?thesis by blast
    next
      fix z
      assume "?P y z" and "restrict_to P A z x"
      with 1 have "accessible_on ?P A z" by (auto simp: restrict_to_def)
      from accessible_on_downward [OF this ‹y ∈ A› ‹?P y z›]
        show ?thesis .
    qed
  qed
qed

lemma wfp_on_restrict_to_tranclp:
  assumes "wfp_on P A"
  shows "wfp_on ((restrict_to P A)⇧+⇧+) A"
  using wfp_on_imp_accessible_on [OF assms]
    and accessible_on_tranclp [of P A]
    and accessible_on_imp_wfp_on [of A "(restrict_to P A)⇧+⇧+"]
    by blast

lemma wfp_on_restrict_to_tranclp':
  assumes "wfp_on (restrict_to P A)⇧+⇧+ A"
  shows "wfp_on P A"
  by (rule ccontr) (insert assms, auto simp: wfp_on_def)

lemma wfp_on_restrict_to_tranclp_wfp_on_conv:
  "wfp_on (restrict_to P A)⇧+⇧+ A ⟷ wfp_on P A"
  using wfp_on_restrict_to_tranclp [of P A]
    and wfp_on_restrict_to_tranclp' [of P A]
    by blast

lemma tranclp_idemp [simp]:
  "(P⇧+⇧+)⇧+⇧+ = P⇧+⇧+" (is "?l = ?r")
proof (intro ext)
  fix x y
  show "?l x y = ?r x y"
  proof
    assume "?l x y" then show "?r x y" by (induct) auto
  next
    assume "?r x y" then show "?l x y" by (induct) auto
  qed
qed

(*TODO: move the following 3 lemmas to Transitive_Closure?*)
lemma stepfun_imp_tranclp:
  assumes "f 0 = x" and "f (Suc n) = z"
    and "∀i≤n. P (f i) (f (Suc i))"
  shows "P⇧+⇧+ x z"
  using assms
  by (induct n arbitrary: x z)
     (auto intro: tranclp.trancl_into_trancl)

lemma tranclp_imp_stepfun:
  assumes "P⇧+⇧+ x z"
  shows "∃f n. f 0 = x ∧ f (Suc n) = z ∧ (∀i≤n. P (f i) (f (Suc i)))"
    (is "∃f n. ?P x z f n")
  using assms
proof (induct rule: tranclp_induct)
  case (base y)
  let ?f = "(λ_. y)(0 := x)"
  have "?f 0 = x" and "?f (Suc 0) = y" by auto
  moreover have "∀i≤0. P (?f i) (?f (Suc i))"
    using base by auto
  ultimately show ?case by blast
next
  case (step y z)
  then obtain f n where IH: "?P x y f n" by blast
  then have *: "∀i≤n. P (f i) (f (Suc i))"
    and [simp]: "f 0 = x" "f (Suc n) = y"
    by auto
  let ?n = "Suc n"
  let ?f = "f(Suc ?n := z)"
  have "?f 0 = x" and "?f (Suc ?n) = z" by auto
  moreover have "∀i≤?n. P (?f i) (?f (Suc i))"
    using ‹P y z› and * by auto
  ultimately show ?case by blast
qed

lemma tranclp_stepfun_conv:
  "P⇧+⇧+ x y ⟷ (∃f n. f 0 = x ∧ f (Suc n) = y ∧ (∀i≤n. P (f i) (f (Suc i))))"
  using tranclp_imp_stepfun and stepfun_imp_tranclp by metis


subsection ‹Facts About Predecessor Sets›

lemma qo_on_predecessor_subset_conv':
  assumes "qo_on P A" and "B ⊆ A" and "C ⊆ A"
  shows "{x∈A. ∃y∈B. P x y} ⊆ {x∈A. ∃y∈C. P x y} ⟷ (∀x∈B. ∃y∈C. P x y)"
  using assms
  by (auto simp: subset_eq qo_on_def reflp_on_def, unfold transp_on_def) metis+

lemma qo_on_predecessor_subset_conv:
  "⟦qo_on P A; x ∈ A; y ∈ A⟧ ⟹ {z∈A. P z x} ⊆ {z∈A. P z y} ⟷ P x y"
  using qo_on_predecessor_subset_conv' [of P A "{x}" "{y}"] by simp

lemma po_on_predecessors_eq_conv:
  assumes "po_on P A" and "x ∈ A" and "y ∈ A"
  shows "{z∈A. P⇧=⇧= z x} = {z∈A. P⇧=⇧= z y} ⟷ x = y"
  using assms(2-)
    and reflp_on_reflclp [of A P]
    and po_on_imp_antisymp_on [OF ‹po_on P A›]
    unfolding antisymp_on_def reflp_on_def
    by blast

lemma restrict_to_rtranclp:
  assumes "transp_on A P"
    and "x ∈ A" and "y ∈ A"
  shows "(restrict_to P A)⇧*⇧* x y ⟷ P⇧=⇧= x y"
proof -
  { assume "(restrict_to P A)⇧*⇧* x y"
    then have "P⇧=⇧= x y" using assms
      by (induct) (auto, unfold transp_on_def, blast) }
  with assms show ?thesis by auto
qed

lemma reflp_on_restrict_to_rtranclp:
  assumes "reflp_on A P" and "transp_on A P"
    and "x ∈ A" and "y ∈ A"
  shows "(restrict_to P A)⇧*⇧* x y ⟷ P x y"
  unfolding restrict_to_rtranclp [OF assms(2-)]
  unfolding reflp_on_reflclp_simp [OF assms(1, 3-)] ..

end