Theory Function_Relators

✐‹creator "Kevin Kappelmann"›
subsection ‹Relators›
theory Function_Relators
  imports
    Binary_Relation_Functions
    Functions_Base
    Predicates_Lattice
    ML_Unification.ML_Unification_HOL_Setup
    ML_Unification.Unify_Resolve_Tactics
begin

paragraph ‹Summary›
text ‹Introduces the concept of function relators. The slogan of function
relators is "related functions map related inputs to related outputs".›

consts Dep_Fun_Rel :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
consts Fun_Rel :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"

open_bundle Dep_Fun_Rel_syntax
begin
notation "Fun_Rel" (infixr ‹⇛› 50)
syntax
  "_Dep_Fun_Rel_rel" :: "idt ⇒ idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
    (‹'(_/ _/ ∷/ _') ⇛ (_)› [51, 51, 50, 50] 50)
  "_Dep_Fun_Rel_rel_if" :: "idt ⇒ idt ⇒ 'a ⇒ bool ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
    (‹'(_/ _/ ∷/ _/ |/ _') ⇛ (_)› [51, 51, 50, 50, 50] 50)
  "_Dep_Fun_Rel_pred" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
    (‹'(_/ :/ _') ⇛ (_)› [51, 50, 50] 50)
  "_Dep_Fun_Rel_pred_if" :: "idt ⇒ 'a ⇒ bool ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
    (‹'(_/ :/ _/ |/ _') ⇛ (_)› [51, 50, 50, 50] 50)
end
syntax_consts
  "_Dep_Fun_Rel_rel" "_Dep_Fun_Rel_rel_if" "_Dep_Fun_Rel_pred" "_Dep_Fun_Rel_pred_if" ⇌ Dep_Fun_Rel
translations
  "(x y ∷ R) ⇛ S" ⇌ "CONST Dep_Fun_Rel R (λx y. S)"
  "(x y ∷ R | B) ⇛ S" ⇌ "CONST Dep_Fun_Rel R (λx y. CONST rel_if B S)"
  "(x : P) ⇛ R" ⇌ "CONST Dep_Fun_Rel P (λx. R)"
  "(x : P | B) ⇛ R" ⇌ "CONST Dep_Fun_Rel P (λx. CONST rel_if B R)"

definition "Dep_Fun_Rel_rel R S f g ≡ ∀x y. R x y ⟶ S x y (f x) (g y)"
adhoc_overloading Dep_Fun_Rel Dep_Fun_Rel_rel

definition "Fun_Rel_rel (R :: 'a ⇒ 'b ⇒ bool) (S :: 'c ⇒ 'd ⇒ bool) ≡
  ((_ _ ∷ R) ⇛ S) :: ('a ⇒ 'c) ⇒ ('b ⇒ 'd) ⇒ bool"
adhoc_overloading Fun_Rel Fun_Rel_rel

definition "Dep_Fun_Rel_pred P R f g ≡ ∀x. P x ⟶ R x (f x) (g x)"
adhoc_overloading Dep_Fun_Rel Dep_Fun_Rel_pred

definition "Fun_Rel_pred (P :: 'a ⇒ bool) (R :: 'b ⇒ 'c ⇒ bool) ≡
  ((_ : P) ⇛ R) :: ('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ bool"
adhoc_overloading Fun_Rel Fun_Rel_pred

lemma Fun_Rel_rel_eq_Dep_Fun_Rel_rel:
  "((R :: 'a ⇒ 'b ⇒ bool) ⇛ (S :: 'c ⇒ 'd ⇒ bool)) = ((_ _ ∷ R) ⇛ S)"
  unfolding Fun_Rel_rel_def by simp

lemma Fun_Rel_rel_eq_Dep_Fun_Rel_rel_uhint [uhint]:
  assumes "R ≡ R'"
  and "S' ≡ (λ(_ :: 'a) (_ :: 'b). S)"
  shows "((R :: 'a ⇒ 'b ⇒ bool) ⇛ (S :: 'c ⇒ 'd ⇒ bool)) = ((x y ∷ R') ⇛ S' x y)"
  using assms by (simp add: Fun_Rel_rel_eq_Dep_Fun_Rel_rel)

lemma Fun_Rel_rel_iff_Dep_Fun_Rel_rel:
  "((R :: 'a ⇒ 'b ⇒ bool) ⇛ (S :: 'c ⇒ 'd ⇒ bool)) f g ⟷ ((_ _ ∷ R) ⇛ S) f g"
  by (simp add: Fun_Rel_rel_eq_Dep_Fun_Rel_rel)

lemma Fun_Rel_pred_eq_Dep_Fun_Rel_pred:
  "((P :: 'a ⇒ bool) ⇛ (R :: 'b ⇒ 'c ⇒ bool)) = ((_ : P) ⇛ R)"
  unfolding Fun_Rel_pred_def by simp

lemma Fun_Rel_pred_eq_Dep_Fun_Rel_pred_uhint [uhint]:
  assumes "P ≡ P'"
  and "R' ≡ (λ(_ :: 'a). R)"
  shows "((P :: 'a ⇒ bool) ⇛ (R :: 'b ⇒ 'c ⇒ bool)) = ((x : P') ⇛ R' x)"
  using assms by (simp add: Fun_Rel_pred_eq_Dep_Fun_Rel_pred)

lemma Fun_Rel_pred_iff_Dep_Fun_Rel_pred:
  "((P :: 'a ⇒ bool) ⇛ (R :: 'b ⇒ 'c ⇒ bool)) f g ⟷ ((_ : P) ⇛ R) (f :: 'a ⇒ 'b) (g :: 'a ⇒ 'c)"
  by (simp add: Fun_Rel_pred_eq_Dep_Fun_Rel_pred)

lemma Dep_Fun_Rel_relI [intro]:
  assumes "⋀x y. R x y ⟹ S x y (f x) (g y)"
  shows "((x y ∷ R) ⇛ S x y) f g"
  unfolding Dep_Fun_Rel_rel_def using assms by blast

lemma Dep_Fun_Rel_relD [dest]:
  assumes "((x y ∷ R) ⇛ S x y) f g"
  and "R x y"
  shows "S x y (f x) (g y)"
  using assms unfolding Dep_Fun_Rel_rel_def by blast

lemma Dep_Fun_Rel_relE:
  assumes "((x y ∷ R) ⇛ S x y) f g"
  obtains "⋀x y. R x y ⟹ S x y (f x) (g y)"
  using assms unfolding Dep_Fun_Rel_rel_def by blast

lemma Dep_Fun_Rel_rel_cong [cong]:
  assumes "R = R'"
  and "⋀x y. R' x y ⟹ S x y = S' x y"
  shows "((x y ∷ R) ⇛ S x y) = ((x y ∷ R') ⇛ S' x y)"
  using assms by force

lemma Fun_Rel_relI [intro]:
  assumes "⋀x y. R x y ⟹ S (f x) (g y)"
  shows "(R ⇛ S) f g"
  using assms by (urule Dep_Fun_Rel_relI)

lemma Fun_Rel_relD [dest]:
  assumes "(R ⇛ S) f g"
  and "R x y"
  shows "S (f x) (g y)"
  using assms by (urule Dep_Fun_Rel_relD)

lemma Fun_Rel_relE:
  assumes "((x y ∷ R) ⇛ S x y) f g"
  obtains "⋀x y. R x y ⟹ S x y (f x) (g y)"
  using assms by (urule (e) Dep_Fun_Rel_relE)

lemma Dep_Fun_Rel_predI [intro]:
  assumes "⋀x. P x ⟹ R x (f x) (g x)"
  shows "((x : P) ⇛ R x) f g"
  unfolding Dep_Fun_Rel_pred_def using assms by blast

lemma Dep_Fun_Rel_predD [dest]:
  assumes "((x : P) ⇛ R x) f g"
  and "P x"
  shows "R x (f x) (g x)"
  using assms unfolding Dep_Fun_Rel_pred_def by blast

lemma Dep_Fun_Rel_predE:
  assumes "((x : P) ⇛ R x) f g"
  obtains "⋀x. P x ⟹ R x (f x) (g x)"
  using assms unfolding Dep_Fun_Rel_pred_def by blast

lemma Dep_Fun_Rel_pred_cong [cong]:
  assumes "P = P'"
  and "⋀x. P' x ⟹ R x = R' x"
  shows "((x : P) ⇛ R x) = ((x : P') ⇛ R' x)"
  using assms by force

lemma Fun_Rel_predI [intro]:
  assumes "⋀x. P x ⟹ R (f x) (g x)"
  shows "(P ⇛ R) f g"
  using assms by (urule Dep_Fun_Rel_predI)

lemma Fun_Rel_predD [dest]:
  assumes "(P ⇛ R) f g"
  and "P x"
  shows "R (f x) (g x)"
  using assms by (urule Dep_Fun_Rel_predD)

lemma Fun_Rel_predE:
  assumes "(P ⇛ R) f g"
  obtains "⋀x. P x ⟹ R (f x) (g x)"
  using assms by (urule (e) Dep_Fun_Rel_predE)

lemma rel_inv_Dep_Fun_Rel_rel_eq [simp]:
  fixes R :: "'a ⇒ 'b ⇒ bool" and S :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
  shows "((x y ∷ R) ⇛ S x y)¯ = ((y x ∷ R¯) ⇛ (S x y)¯)"
  by (intro ext) auto

lemma rel_inv_rel_inv_Dep_Fun_Rel_rel_iff_Dep_Fun_Rel_rel [iff]:
  "((x y ∷ R¯) ⇛ (S x y)¯) f g ⟷ ((x y ∷ R) ⇛ (S y x)) g f"
  by (simp flip: rel_inv_Dep_Fun_Rel_rel_eq)

lemma rel_inv_Dep_Fun_Rel_pred_eq [simp]:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
  shows "((x : P) ⇛ R x)¯ = ((x : P) ⇛ (R x)¯)"
  by (intro ext) auto

lemma rel_inv_Dep_Fun_Rel_pred_iff_Dep_Fun_Rel_pred [iff]:
  "((x : P) ⇛ (R x)¯) f g ⟷ ((x : P) ⇛ (R x)) g f"
  by (simp flip: rel_inv_Dep_Fun_Rel_pred_eq)

lemma Dep_Fun_Rel_pred_eq_Dep_Fun_Rel_rel:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
  shows "((x : P) ⇛ R x) = ((x (_ :: 'a) ∷ (((⊓) P) ∘ (=))) ⇛ R x)"
  by (intro ext) (auto intro!: Dep_Fun_Rel_predI Dep_Fun_Rel_relI)

lemma Fun_Rel_eq_eq_eq [simp]: "((=) ⇛ (=)) = (=)"
  by (intro ext) auto


paragraph ‹Composition›

lemma Dep_Fun_Rel_rel_compI:
  assumes "((x y ∷ R) ⇛ S x y) f g"
  and "⋀x y. R x y ⟹ ((x' y' ∷ T x y) ⇛ U x y x' y') f' g'"
  and "⋀x y. R x y ⟹ S x y (f x) (g y) ⟹ T x y (f x) (g y)"
  shows "((x y ∷ R) ⇛ U x y (f x) (g y)) (f' ∘ f) (g' ∘ g)"
  using assms by (intro Dep_Fun_Rel_relI) (auto 6 0)

corollary Dep_Fun_Rel_rel_compI':
  assumes "((x y ∷ R) ⇛ S x y) f g"
  and "⋀x y. R x y ⟹ ((x' y' ∷ S x y) ⇛ T x y x' y') f' g'"
  shows "((x y ∷ R) ⇛ T x y (f x) (g y)) (f' ∘ f) (g' ∘ g)"
  using assms by (intro Dep_Fun_Rel_rel_compI)

lemma Dep_Fun_Rel_pred_comp_Dep_Fun_Rel_rel_compI:
  assumes "((x : P) ⇛ R x) f g"
  and "⋀x. P x ⟹ ((x' y' ∷ S x) ⇛ T x x' y') f' g'"
  and "⋀x. P x ⟹ R x (f x) (g x) ⟹ S x (f x) (g x)"
  shows "((x : P) ⇛ T x (f x) (g x)) (f' ∘ f) (g' ∘ g)"
  using assms by (intro Dep_Fun_Rel_predI) (auto 6 0)

corollary Dep_Fun_Rel_pred_comp_Dep_Fun_Rel_rel_compI':
  assumes "((x : P) ⇛ R x) f g"
  and "⋀x. P x ⟹ ((x' y' ∷ R x) ⇛ S x x' y') f' g'"
  shows "((x : P) ⇛ S x (f x) (g x)) (f' ∘ f) (g' ∘ g)"
  using assms by (intro Dep_Fun_Rel_pred_comp_Dep_Fun_Rel_rel_compI)


paragraph ‹Restrictions›

lemma Dep_Fun_Rel_restrict_left_restrict_left_eq:
  assumes "⋀f x y. Q f ⟹ R x y ⟹ P x y (f x)"
  shows "((x y ∷ R) ⇛ (S x y)↾⇘P x y⇙)↾⇘Q⇙ = ((x y ∷ R) ⇛ S x y)↾⇘Q⇙"
  using assms by (intro ext iffI rel_restrict_leftI Dep_Fun_Rel_relI)
  (auto dest!: Dep_Fun_Rel_relD)

lemma Dep_Fun_Rel_restrict_right_restrict_right_eq:
  assumes "⋀f x y. Q f ⟹ R x y ⟹ P x y (f y)"
  shows "((x y ∷ R) ⇛ (S x y)↿⇘P x y⇙)↿⇘Q⇙ = (((x y ∷ R) ⇛ S x y)↿⇘Q⇙)"
  unfolding rel_restrict_right_eq
  using assms
    Dep_Fun_Rel_restrict_left_restrict_left_eq[where ?R="R¯" and ?S="λy x. (S x y)¯"]
  by simp


end