# Theory Open_Induction.Restricted_Predicates

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

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"

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"

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"

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"

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

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
`