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 ..

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

bundle comp_syntax begin notation comp (infixl "∘" 55) end
bundle no_comp_syntax begin no_notation comp (infixl "∘" 55) end
unbundle comp_syntax

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"

bundle dep_fun_map_syntax begin
syntax
  "_fun_map" :: "('a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('b ⇒ 'c) ⇒
    ('a ⇒ 'd)" ("(_) ↝ (_)" [41, 40] 40)
  "_dep_fun_map" :: "idt ⇒ ('a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('b ⇒ 'c) ⇒
    ('a ⇒ 'd)" ("'(_/ : / _') ↝ (_)" [41, 41, 40] 40)
end
bundle no_dep_fun_map_syntax begin
no_syntax
  "_fun_map" :: "('a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('b ⇒ 'c) ⇒
    ('a ⇒ 'd)" ("(_) ↝ (_)" [41, 40] 40)
  "_dep_fun_map" :: "idt ⇒ ('a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('b ⇒ 'c) ⇒
    ('a ⇒ 'd)" ("'(_/ : / _') ↝ (_)" [41, 41, 40] 40)
end
unbundle dep_fun_map_syntax
translations
  "f ↝ g" ⇌ "CONST fun_map f g"
  "(x : f) ↝ g" ⇌ "CONST dep_fun_map f (λx. g)"

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) f ≡ in_codom_on P ((=) ∘ f)"
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)

end