# Theory Transitive_Closure_Ext

```(*  Title:       Safe OCL
Author:      Denis Nikiforov, March 2019
Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
*)
section ‹Transitive Closures›
theory Transitive_Closure_Ext
imports "HOL-Library.FuncSet"
begin

(*** Basic Properties *******************************************************)

subsection ‹Basic Properties›

text ‹
@{text "R⇧+⇧+"} is a transitive closure of a relation @{text R}.
@{text "R⇧*⇧*"} is a reflexive transitive closure of a relation @{text R}.›

text ‹
A function @{text f} is surjective on @{text "R⇧+⇧+"} iff for any
two elements in the range of @{text f}, related through @{text "R⇧+⇧+"},
all their intermediate elements belong to the range of @{text f}.›

abbreviation "surj_on_trancl R f ≡
(∀x y z. R⇧+⇧+ (f x) y ⟶ R y (f z) ⟶ y ∈ range f)"

text ‹
A function @{text f} is bijective on @{text "R⇧+⇧+"} iff
it is injective and surjective on @{text "R⇧+⇧+"}.›

abbreviation "bij_on_trancl R f ≡ inj f ∧ surj_on_trancl R f"

(*** Helper Lemmas **********************************************************)

subsection ‹Helper Lemmas›

lemma rtranclp_eq_rtranclp [iff]:
"(λx y. P x y ∨ x = y)⇧*⇧* = P⇧*⇧*"
proof (intro ext iffI)
fix x y
have "(λx y. P x y ∨ x = y)⇧*⇧* x y ⟶ P⇧=⇧=⇧*⇧* x y"
by (rule mono_rtranclp) simp
thus "(λx y. P x y ∨ x = y)⇧*⇧* x y ⟹ P⇧*⇧* x y"
by simp
show "P⇧*⇧* x y ⟹ (λx y. P x y ∨ x = y)⇧*⇧* x y"
by (metis (no_types, lifting) mono_rtranclp)
qed

lemma tranclp_eq_rtranclp [iff]:
"(λx y. P x y ∨ x = y)⇧+⇧+ = P⇧*⇧*"
proof (intro ext iffI)
fix x y
have "(λx y. P x y ∨ x = y)⇧*⇧* x y ⟶ P⇧=⇧=⇧*⇧* x y"
by (rule mono_rtranclp) simp
thus "(λx y. P x y ∨ x = y)⇧+⇧+ x y ⟹ P⇧*⇧* x y"
using tranclp_into_rtranclp by force
show "P⇧*⇧* x y ⟹ (λx y. P x y ∨ x = y)⇧+⇧+ x y"
by (metis (mono_tags, lifting) mono_rtranclp rtranclpD tranclp.r_into_trancl)
qed

lemma rtranclp_eq_rtranclp' [iff]:
"(λx y. P x y ∧ x ≠ y)⇧*⇧* = P⇧*⇧*"
proof (intro ext iffI)
fix x y
show "(λx y. P x y ∧ x ≠ y)⇧*⇧* x y ⟹ P⇧*⇧* x y"
by (metis (no_types, lifting) mono_rtranclp)
assume "P⇧*⇧* x y"
hence "(inf P (≠))⇧*⇧* x y"
also have "(inf P (≠))⇧*⇧* x y ⟶ (λx y. P x y ∧ x ≠ y)⇧*⇧* x y"
by (rule mono_rtranclp) simp
finally show "P⇧*⇧* x y ⟹ (λx y. P x y ∧ x ≠ y)⇧*⇧* x y" by simp
qed

lemma tranclp_tranclp_to_tranclp_r:
assumes "(⋀x y z. R⇧+⇧+ x y ⟹ R y z ⟹ P x ⟹ P z ⟹ P y)"
assumes "R⇧+⇧+ x y" and "R⇧+⇧+ y z"
assumes "P x" and "P z"
shows "P y"
proof -
have "(⋀x y z. R⇧+⇧+ x y ⟹ R y z ⟹ P x ⟹ P z ⟹ P y) ⟹
R⇧+⇧+ y z ⟹ R⇧+⇧+ x y ⟹ P x ⟶ P z ⟶ P y"
by (erule tranclp_induct, auto) (meson tranclp_trans)
thus ?thesis using assms by auto
qed

(*** Transitive Closure Preservation & Reflection ***************************)

subsection ‹Transitive Closure Preservation›

text ‹
A function @{text f} preserves @{text "R⇧+⇧+"} if it preserves @{text R}.›

text ‹
The proof was derived from the accepted answer on the website
Stack Overflow that is available at
@{url "https://stackoverflow.com/a/52573551/632199"}
and provided with the permission of the author of the answer.›

lemma preserve_tranclp:
assumes "⋀x y. R x y ⟹ S (f x) (f y)"
assumes "R⇧+⇧+ x y"
shows "S⇧+⇧+ (f x) (f y)"
proof -
define P where P: "P = (λx y. S⇧+⇧+ (f x) (f y))"
define r where r: "r = (λx y. S (f x) (f y))"
have "r⇧+⇧+ x y" by (insert assms r; erule tranclp_trans_induct; auto)
moreover have "⋀x y. r x y ⟹ P x y" unfolding P r by simp
moreover have "⋀x y z. r⇧+⇧+ x y ⟹ P x y ⟹ r⇧+⇧+ y z ⟹ P y z ⟹ P x z"
unfolding P by auto
ultimately have "P x y" by (rule tranclp_trans_induct)
with P show ?thesis by simp
qed

text ‹
A function @{text f} preserves @{text "R⇧*⇧*"} if it preserves @{text R}.›

lemma preserve_rtranclp:
"(⋀x y. R x y ⟹ S (f x) (f y)) ⟹
R⇧*⇧* x y ⟹ S⇧*⇧* (f x) (f y)"
unfolding Nitpick.rtranclp_unfold
by (metis preserve_tranclp)

text ‹
If one needs to prove that @{text "(f x)"} and @{text "(g y)"}
are related through @{text "S⇧*⇧*"} then one can use the previous
lemma and add a one more step from @{text "(f y)"} to @{text "(g y)"}.›

lemma preserve_rtranclp':
"(⋀x y. R x y ⟹ S (f x) (f y)) ⟹
(⋀y. S (f y) (g y)) ⟹
R⇧*⇧* x y ⟹ S⇧*⇧* (f x) (g y)"
by (metis preserve_rtranclp rtranclp.rtrancl_into_rtrancl)

lemma preserve_rtranclp'':
"(⋀x y. R x y ⟹ S (f x) (f y)) ⟹
(⋀y. S (f y) (g y)) ⟹
R⇧*⇧* x y ⟹ S⇧+⇧+ (f x) (g y)"
apply (rule_tac ?b="f y" in rtranclp_into_tranclp1, auto)
by (rule preserve_rtranclp, auto)

subsection ‹Transitive Closure Reflection›

text ‹
A function @{text f} reflects @{text "S⇧+⇧+"} if it reflects
@{text S} and is bijective on @{text "S⇧+⇧+"}.›

text ‹
The proof was derived from the accepted answer on the website
Stack Overflow that is available at
@{url "https://stackoverflow.com/a/52573551/632199"}
and provided with the permission of the author of the answer.›

lemma reflect_tranclp:
assumes refl_f: "⋀x y. S (f x) (f y) ⟹ R x y"
assumes bij_f: "bij_on_trancl S f"
assumes prem: "S⇧+⇧+ (f x) (f y)"
shows "R⇧+⇧+ x y"
proof -
define B where B: "B = range f"
define g where g: "g = the_inv_into UNIV f"
define gr where gr: "gr = restrict g B"
define P where P: "P = (λx y. x ∈ B ⟶ y ∈ B ⟶ R⇧+⇧+ (gr x) (gr y))"
from prem have major: "S⇧+⇧+ (f x) (f y)" by blast
from refl_f bij_f have cases_1: "⋀x y. S x y ⟹ P x y"
unfolding B P g gr
from refl_f bij_f
have "(⋀x y z. S⇧+⇧+ x y ⟹ S⇧+⇧+ y z ⟹ x ∈ B ⟹ z ∈ B ⟹ y ∈ B)"
unfolding B
by (rule_tac ?z="z" in tranclp_tranclp_to_tranclp_r, auto, blast)
with P have cases_2:
"⋀x y z. S⇧+⇧+ x y ⟹ P x y ⟹ S⇧+⇧+ y z ⟹ P y z ⟹ P x z"
unfolding B
by auto
from major cases_1 cases_2 have "P (f x) (f y)"
by (rule tranclp_trans_induct)
with bij_f show ?thesis unfolding P B g gr by (simp add: the_inv_f_f)
qed

text ‹
A function @{text f} reflects @{text "S⇧*⇧*"} if it reflects
@{text S} and is bijective on @{text "S⇧+⇧+"}.›

lemma reflect_rtranclp:
"(⋀x y. S (f x) (f y) ⟹ R x y) ⟹
bij_on_trancl S f ⟹
S⇧*⇧* (f x) (f y) ⟹ R⇧*⇧* x y"
unfolding Nitpick.rtranclp_unfold
by (metis (full_types) injD reflect_tranclp)

end
```