Theory Functions_Base

✐‹creator "Kevin Kappelmann"›
section ‹Functions›
subsection ‹Basic Functions›
theory Functions_Base
  imports
    Binary_Relation_Functions
begin

definition "id x ≡ x"

lemma id_eq_self [simp]: "id x = x"
  unfolding id_def ..

lemma rel_map_id_eq_self [simp]: "rel_map id R = R" by (intro ext) auto

consts comp :: "'a ⇒ 'b ⇒ 'c"

open_bundle comp_syntax
begin
notation comp (infixl ‹∘› 55)
end

definition "comp_fun f g x ≡ f (g x)"
adhoc_overloading comp ⇌ comp_fun

lemma comp_eq [simp]: "(f ∘ g) x = f (g x)"
  unfolding comp_fun_def ..

lemma id_comp_eq [simp]: "id ∘ f = f"
  by (rule ext) simp

lemma comp_id_eq [simp]: "f ∘ id = f"
  by (rule ext) simp

lemma bottom_comp_eq [simp]: "⊥ ∘ f = ⊥" by auto
lemma top_comp_eq [simp]: "⊤ ∘ f = ⊤" by auto


definition "dep_fun_map f g h x ≡ g x (f x) (h (f x))"

definition "fun_map f g h ≡ dep_fun_map f (λ_ _. g) h"

open_bundle dep_fun_map_syntax
begin
notation "fun_map" (infixr ‹↝› 40)
syntax
  "_dep_fun_map" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c" (‹('(_ : _') ↝/ _)› [41, 41, 40] 40)
syntax_consts "_dep_fun_map" ⇌ dep_fun_map
translations
  "(x : f) ↝ g" ⇌ "CONST dep_fun_map f (λx. g)"
end

lemma fun_map_eq_dep_fun_map: "(f ↝ g) = ((_ : f) ↝ (λ_. g))"
  unfolding fun_map_def by simp

lemma fun_map_eq_dep_fun_map_uhint [uhint]:
  assumes "f ≡ f'"
  and "g' ≡ λ_ _. g"
  shows "(f ↝ g) = ((x : f') ↝ g' x)"
  using assms by (simp add: fun_map_eq_dep_fun_map)

lemma dep_fun_map_eq [simp]: "((x : f) ↝ g x) h x = g x (f x) (h (f x))"
  unfolding dep_fun_map_def ..

lemma fun_map_eq_comp [simp]: "(f ↝ g) h = g ∘ h ∘ f"
  by (intro ext) (urule dep_fun_map_eq)

lemma fun_map_eq [simp]: "(f ↝ g) h x = g (h (f x))"
  unfolding fun_map_eq_comp by simp

lemma fun_map_id_eq_comp [simp]: "fun_map id = (∘)"
  by (intro ext) simp

lemma fun_map_id_eq_comp' [simp]: "(f ↝ id) h = h ∘ f"
  by (intro ext) simp

consts has_inverse_on :: "'a ⇒ 'b ⇒ 'c ⇒ bool"

definition "has_inverse_on_pred (P :: 'a ⇒ bool) ≡ in_codom_on P ∘ ((∘) (=))"
adhoc_overloading has_inverse_on ⇌ has_inverse_on_pred

lemma has_inverse_on_pred_eq_in_codom_on: "has_inverse_on P = in_codom_on P ∘ ((∘) (=))"
  unfolding has_inverse_on_pred_def by auto

lemma has_inverse_onI [intro]:
  assumes "P x"
  shows "has_inverse_on P f (f x)"
  using assms unfolding has_inverse_on_pred_def by auto

lemma has_inverse_on_if_pred_if_eq:
  assumes "y = f x"
  and "P x"
  shows "has_inverse_on P f y"
  using assms by auto

lemma has_inverse_onE [elim]:
  assumes "has_inverse_on P f y"
  obtains x where "P x" "y = f x"
  using assms unfolding has_inverse_on_pred_def by auto

context
  notes has_inverse_on_pred_eq_in_codom_on[simp]
begin

lemma has_inverse_on_bottom_eq [simp]: "has_inverse_on ⊥ = ⊥"
  by (urule in_codom_bottom_pred_eq_bottom)

lemma has_inverse_on_eq_pred_eq_eq_app [simp]: "has_inverse_on ((=) P) f = (=) (f P)"
  by (urule in_codom_on_eq_pred_eq)

lemma has_inverse_on_sup_eq_has_inverse_on_sup_has_inverse_on [simp]:
  "has_inverse_on (P ⊔ Q) = has_inverse_on P ⊔ has_inverse_on Q"
  supply ext[simp] by (urule in_codom_on_sup_pred_eq_in_codom_on_sup_in_codom_on)

end

definition "has_inverse ≡ has_inverse_on ⊤"

lemma has_inverse_eq_has_inverse_on_top: "has_inverse = has_inverse_on ⊤"
  unfolding has_inverse_def by simp

lemma has_inverse_eq_has_inverse_on_top_uhint [uhint]:
  assumes "P ≡ ⊤"
  shows "has_inverse ≡ has_inverse_on P"
  using assms by (simp add: has_inverse_eq_has_inverse_on_top)

lemma has_inverse_iff_has_inverse_on_top: "has_inverse f y ⟷ has_inverse_on ⊤ f y"
  by (simp add: has_inverse_eq_has_inverse_on_top)

lemma has_inverseI [intro]:
  assumes "y = f x"
  shows "has_inverse f y"
  using assms by (urule has_inverse_on_if_pred_if_eq) simp

lemma has_inverseE [elim]:
  assumes "has_inverse f y"
  obtains x where "y = f x"
  using assms by (urule (e) has_inverse_onE)

consts image :: "'a ⇒ 'b ⇒ 'c"

definition "image_pred (f :: 'a ⇒ 'b) (P :: 'a ⇒ bool) ≡ has_inverse_on P f"
adhoc_overloading image ⇌ image_pred

lemma image_pred_eq_has_inverse_on [simp]: "image f P = has_inverse_on P f"
  unfolding image_pred_def by simp

lemma image_pred_eq_has_inverse_on_uhint [uhint]:
  assumes "f ≡ f'"
  and "P ≡ P'"
  shows "image f P ≡ has_inverse_on P' f'"
  using assms by simp

definition "equaliser f g ≡ λx. f x = g x"

lemma equaliserI [intro]:
  assumes "f x = g x"
  shows "equaliser f g x"
  using assms unfolding equaliser_def by auto

lemma equaliserD [dest]:
  assumes "equaliser f g x"
  shows "f x = g x"
  using assms unfolding equaliser_def by auto

end