Theory Function_Relators

✐‹creator "Kevin Kappelmann"›
subsection ‹Relators›
theory Function_Relators
  imports
    Predicate_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_rel :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
consts Dep_Fun_Rel_pred :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"
consts Fun_Rel :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"

nonterminal dep_rel_restrict and Dep_Fun_Rel_rel_pttrn and Dep_Fun_Rel_pred_pttrn
open_bundle Dep_Fun_Rel_syntax
begin
notation "Fun_Rel" (infixr ‹⇛› 50)
syntax
  "_dep_rel_restrict_if" :: "'a ⇒ dep_rel_restrict" (‹(|/ _)›)
  "_Dep_Fun_Rel_rel" :: "Dep_Fun_Rel_rel_pttrn ⇒ 'a ⇒ bool" (‹(_ ⇛/ _)› [0, 10] 50)
  "_Dep_Fun_Rel_rel_standard" :: "idt ⇒ idt ⇒ 'a ⇒ Dep_Fun_Rel_rel_pttrn" (‹('(_ _ ∷ _'))›)
  "_Dep_Fun_Rel_rel_restrict" :: "idt ⇒ idt ⇒ 'a ⇒ dep_rel_restrict  ⇒ Dep_Fun_Rel_rel_pttrn" (‹('(_ _ ∷ _ _'))›)
  "_Dep_Fun_Rel_pred" :: "Dep_Fun_Rel_pred_pttrn ⇒ 'a ⇒ bool" (‹(_ ⇛/ _)› [0, 10] 50)
  "_Dep_Fun_Rel_pred_standard" :: "idt ⇒ 'a ⇒ Dep_Fun_Rel_pred_pttrn" (‹('(_ : _'))›)
  "_Dep_Fun_Rel_pred_restrict" :: "idt ⇒ 'a ⇒ dep_rel_restrict  ⇒ Dep_Fun_Rel_pred_pttrn" (‹('(_ : _ _'))›)
syntax_consts
  "_dep_rel_restrict_if" ⇌ rel_if
  and "_Dep_Fun_Rel_rel" "_Dep_Fun_Rel_rel_standard" "_Dep_Fun_Rel_rel_restrict" ⇌ Dep_Fun_Rel_rel
  and "_Dep_Fun_Rel_pred" "_Dep_Fun_Rel_pred_standard" "_Dep_Fun_Rel_pred_restrict" ⇌ Dep_Fun_Rel_pred
translations
  "(x y ∷ R | P) ⇛ S" ⇌ "CONST Dep_Fun_Rel_rel R (λx y. CONST rel_if P S)"
  "(x y ∷ R) ⇛ S" ⇌ "CONST Dep_Fun_Rel_rel R (λx y. S)"
  "(x : P | Q) ⇛ R" ⇌ "CONST Dep_Fun_Rel_pred P (λx. CONST rel_if Q R)"
  "(x : P) ⇛ R" ⇌ "CONST Dep_Fun_Rel_pred P (λx. R)"
end

definition "Dep_Fun_Rel_rel_rel R S f g ≡ ∀x y. R x y ⟶ S x y (f x) (g y)"
adhoc_overloading Dep_Fun_Rel_rel ⇌ Dep_Fun_Rel_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_pred P R f g ≡ ∀x. P x ⟶ R x (f x) (g x)"
adhoc_overloading Dep_Fun_Rel_pred ⇌ Dep_Fun_Rel_pred_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 "⋀x y. S' x y ≡ 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 "⋀x. R' x ≡ 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_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_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_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_rel_collect_eq_Dep_Fun_Rel_rel_if [simp]:
  "((x y ∷ ⦇x y ∷ R | P x y⦈) ⇛ S x y) = ((x y ∷ R | P x y) ⇛ S x y)"
  by fastforce

lemma Fun_Rel_rel_collect_eq_Dep_Fun_Rel_rel_if [simp]:
  "(⦇x y ∷ R | P x y⦈ ⇛ S) = ((x y ∷ R | P x y) ⇛ S)"
  by fastforce

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_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_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_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 Dep_Fun_Rel_pred_collect_eq_Dep_Fun_Rel_rel_if [simp]:
  "((x : ⦇x : P | Q x⦈) ⇛ R x) = ((x : P | Q x) ⇛ R x)"
  by fastforce

lemma Fun_Rel_pred_collect_eq_Dep_Fun_Rel_rel_if [simp]:
  "(⦇x : P | Q x⦈ ⇛ R) = ((x : P | Q x) ⇛ R)"
  by fastforce

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

lemma Dep_Fun_Rel_pred_rel_inv_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 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⇙)"
  using assms Dep_Fun_Rel_restrict_left_restrict_left_eq[where ?R="R¯" and ?S="λy x. (S x y)¯"]
  by simp

end