Theory RelUtils
theory RelUtils
imports Main "HOL.Transitive_Closure"
begin
definition reflexive where
"reflexive R ≡ ∀x. R x x"
definition TC where
"TC R a b ≡ (∀P. (∀x y. R x y ⟶ P x y) ∧ (∀x y z. P x y ∧ P y z ⟶ P x z) ⟶ P a b)"
lemma TC_equiv_tranclp: "TC R a b ⟷ (R⇧+⇧+ a b)"
proof -
{
have "TC R a b ⟹ (R⇧+⇧+ a b)"
unfolding TC_def
using tranclp.r_into_trancl tranclp_trans
by metis
}
moreover
{
have "(R⇧+⇧+ a b) ⟹ TC R a b" proof(induction rule: tranclp.induct)
case (r_into_trancl a b)
then show ?case by(subst TC_def; auto)
next
case (trancl_into_trancl a b c)
then show ?case unfolding TC_def by blast
qed
}
ultimately show ?thesis
by fast
qed
lemma TC_IMP_NOT_TC_CONJ_1:
fixes R P and x y
assumes "¬(R⇧+⇧+ x y)"
shows "¬((λx y. R x y ∧ P x y)⇧+⇧+ x y)"
proof -
from assms(1) have 1: "¬TC R x y"
using TC_equiv_tranclp
by fast
{
assume P: "¬TC R x y"
then obtain P where a: "(∀x y. R x y ⟶ P x y) ∧ (∀x y z. P x y ∧ P y z ⟶ P x z) ⟶ ¬P x y"
unfolding TC_def
by blast
{
assume P_1: "(∀x y. R x y ⟶ P x y)" "(∀x y z. P x y ∧ P y z ⟶ P x z)"
then have "(∀x y. R x y ∧ P x y ⟶ P x y)" "(∀x y z. P x y ∧ P y z ⟶ P x z)"
by blast+
moreover from a and P_1 have "¬P x y"
by blast
then have "∃P. (∀x y. R x y ∧ P x y ⟶ P x y) ∧ (∀x y z. P x y ∧ P y z ⟶ P x z) ⟶ ¬P x y"
by blast
}
then have "∃P.
(∀x y. R x y ∧ P x y ⟶ P x y) ∧ (∀x y z. P x y ∧ P y z ⟶ P x z) ⟶ ¬P x y"
by blast
}
note 2 = this
{
from 1 2 have "∃P.
(∀x y. R x y ∧ P x y ⟶ P x y) ∧ (∀x y z. P x y ∧ P y z ⟶ P x z) ⟶ ¬P x y"
by blast
then have "¬TC (λx y. R x y ∧ P x y) x y"
unfolding TC_def
by (metis assms tranclp.r_into_trancl tranclp_trans)
then have "¬(λx y. R x y ∧ P x y)⇧+⇧+ x y"
using TC_equiv_tranclp
by fast
}
then show ?thesis
by blast
qed
lemma TC_IMP_NOT_TC_CONJ:
fixes R R' P x y
assumes "∀x y. P x y ⟶ R' x y ⟶ R x y" "¬R⇧+⇧+ x y"
shows "¬(λx y. R' x y ∧ P x y)⇧+⇧+ x y"
proof -
from assms(2)
have 1: "¬(λx y. R x y ∧ P x y)⇧+⇧+ x y"
using TC_IMP_NOT_TC_CONJ_1[where P="λx y. P x y"]
by blast
{
{
from 1 have "¬TC (λx y. R x y ∧ P x y) x y"
using TC_equiv_tranclp
by fast
then have "∃Pa.
(∀x y. R x y ∧ P x y ⟶ Pa x y) ∧ (∀x y z. Pa x y ∧ Pa y z ⟶ Pa x z)
⟶ ¬Pa x y"
unfolding TC_def
by blast
}
then obtain Pa where a:
"(∀x y. R x y ∧ P x y ⟶ Pa x y) ∧ (∀x y z. Pa x y ∧ Pa y z ⟶ Pa x z) ⟶ ¬Pa x y"
by blast
then have "¬(∀Pa. (∀x y. R' x y ∧ P x y ⟶ Pa x y) ∧ (∀x y z. Pa x y ∧ Pa y z ⟶ Pa x z) ⟶ Pa x y)"
by (metis assms(1) assms(2) tranclp.r_into_trancl tranclp_trans)
then have "¬TC (λx y. R' x y ∧ P x y) x y"
unfolding TC_def
by blast
}
then show ?thesis
using TC_equiv_tranclp
by fast
qed
lemma TC_INDUCT:
fixes R :: "'a ⇒ 'a ⇒ bool" and P
assumes "(∀x y. R x y ⟶ P x y)" "(∀x y z. P x y ∧ P y z ⟶ P x z)"
shows "∀u v. (TC R) u v ⟶ P u v"
using assms
unfolding TC_def
by metis
lemma REFL_IMP_3_CONJ_1:
fixes R P x y
assumes "((λx y. R x y ∧ P x y)⇧+⇧+ x y)"
shows "R⇧+⇧+ x y"
using assms
proof -
show ?thesis
using assms TC_IMP_NOT_TC_CONJ_1
by fast
qed
lemma REFL_IMP_3_CONJ:
fixes R'
assumes "reflexive R'"
shows "(∀P x y.
(R'⇧+⇧+ x y) ⟶ ( ((λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x y) ∨ (∃z. ¬P z ∧ R'⇧+⇧+ x z ∧ R'⇧+⇧+ z y)))"
proof -
{
fix P
{
have "∀x y. R' x y ⟶ (λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x y ∨ (∃z. ¬ P z ∧ R'⇧+⇧+ x z ∧ R'⇧+⇧+ z y)"
proof (auto)
fix x y
assume P: "R' x y" "∀z. R'⇧+⇧+ x z ⟶ P z ∨ ¬ R'⇧+⇧+ z y"
then show "(λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x y"
proof -
have a: "⋀a. ¬ R' x a ∨ ¬ R' a y ∨ P a"
using P(2)
by blast
have "reflexive R'"
by (meson assms)
then show ?thesis
using a P(1)
by (simp add: reflexive_def tranclp.r_into_trancl)
qed
qed
}
moreover {
have "∀x y z. ((λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x y ∨ (∃z. ¬ P z ∧ R'⇧+⇧+ x z ∧ R'⇧+⇧+ z y)) ∧
((λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ y z ∨ (∃za. ¬ P za ∧ R'⇧+⇧+ y za ∧ R'⇧+⇧+ za z)) ⟶
(λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x z ∨ (∃za. ¬ P za ∧ R'⇧+⇧+ x za ∧ R'⇧+⇧+ za z)"
proof (auto)
fix x y z za
assume P: "∀za. R'⇧+⇧+ x za ⟶ P za ∨ ¬ R'⇧+⇧+ za z" "(λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x y"
"¬ P za" "R'⇧+⇧+ y za" "R'⇧+⇧+ za z"
then show "(λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x z"
using P
by (meson P rtranclp_tranclp_tranclp TC_IMP_NOT_TC_CONJ_1 tranclp_into_rtranclp)
next
fix x y z za
assume P: "∀za. R'⇧+⇧+ x za ⟶ P za ∨ ¬ R'⇧+⇧+ za z" "¬ P za" "R'⇧+⇧+ x za" "R'⇧+⇧+ za y"
"(λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ y z"
then show "(λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x z"
by (meson P TC_IMP_NOT_TC_CONJ_1 tranclp_trans)
qed
}
ultimately have "∀u v.
TC R' u v
⟶ (λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ u v ∨ (∃z. ¬ P z ∧ R'⇧+⇧+ u z ∧ R'⇧+⇧+ z v)"
using TC_INDUCT[where R="R'" and
P="λx y. ( ((λx y. R' x y ∧ P x ∧ P y)⇧+⇧+ x y) ∨ (∃z. ¬P z ∧ R'⇧+⇧+ x z ∧ R'⇧+⇧+ z y))"]
by fast
}
then show ?thesis
by (simp add: TC_equiv_tranclp)
qed
lemma REFL_TC_CONJ:
fixes R R' :: "'a ⇒ 'a ⇒ bool" and P x y
assumes "reflexive R'" "∀x y. P x ∧ P y ⟶ (R' x y ⟶ R x y)" "¬(R⇧+⇧+ x y)"
shows "(¬(R'⇧+⇧+ x y) ∨ (∃z. ¬P z ∧ (R')⇧+⇧+ x z ∧ (R')⇧+⇧+ z y))"
using assms
proof (cases "¬R'⇧+⇧+ x y")
next
case False
then show ?thesis using assms
TC_IMP_NOT_TC_CONJ[where P="λx y. P x ∧ P y"]
REFL_IMP_3_CONJ[of R']
by blast
qed blast
lemma TC_CASES1_NEQ:
fixes R x z
assumes "R⇧+⇧+ x z"
shows "R x z ∨ (∃y :: 'a. ¬(x = y) ∧ ¬(y = z) ∧ R x y ∧ R⇧+⇧+ y z)"
proof -
{
fix u v
have "∀x y. R x y ⟶ R x y ∨ (∃ya. x ≠ ya ∧ ya ≠ y ∧ R x ya ∧ R⇧+⇧+ ya y)"
by meson
moreover have "∀x y z.
(R x y ∨ (∃ya. x ≠ ya ∧ ya ≠ y ∧ R x ya ∧ R⇧+⇧+ ya y))
∧ (R y z ∨ (∃ya. y ≠ ya ∧ ya ≠ z ∧ R y ya ∧ R⇧+⇧+ ya z))
⟶ R x z ∨ (∃y. x ≠ y ∧ y ≠ z ∧ R x y ∧ R⇧+⇧+ y z)"
by (metis tranclp.r_into_trancl tranclp_trans)
ultimately have "TC R u v ⟶ R u v ∨ (∃y. u ≠ y ∧ y ≠ v ∧ R u y ∧ R⇧+⇧+ y v)"
using TC_INDUCT[where P="λx z. R x z ∨ (∃y :: 'a. ¬(x = y) ∧ ¬(y = z) ∧ R x y ∧ R⇧+⇧+ y z)"]
by blast
}
then show ?thesis
using assms TC_equiv_tranclp
by (simp add: TC_equiv_tranclp)
qed
end