Theory Functions_Inverse

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Inverse›
theory Functions_Inverse
  imports
    Functions_Injective
    Binary_Relations_Function_Evaluation
begin

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

overloading
  inverse_on_pred ≡ "inverse_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool"
begin
  definition "inverse_on_pred P f g ≡ ∀x : P. g (f x) = x"
end

lemma inverse_onI [intro]:
  assumes "⋀x. P x ⟹ g (f x) = x"
  shows "inverse_on P f g"
  unfolding inverse_on_pred_def using assms by blast

lemma inverse_onD:
  assumes "inverse_on P f g"
  and "P x"
  shows "g (f x) = x"
  using assms unfolding inverse_on_pred_def by blast

lemma injective_on_if_inverse_on:
  assumes inv: "inverse_on (P :: 'a ⇒ bool) (f :: 'a ⇒ 'b) (g :: 'b ⇒ 'a)"
  shows "injective_on P f"
proof (rule injective_onI)
  fix x x'
  assume Px: "P x" and Px': "P x'" and f_x_eq_f_x': "f x = f x'"
  from inv have "x = g (f x)" using Px by (intro inverse_onD[symmetric])
  also have "... = g (f x')" by (simp only: f_x_eq_f_x')
  also have "... = x'" using inv Px' by (intro inverse_onD)
  finally show "x = x'" .
qed

lemma inverse_on_compI:
  fixes P :: "'a ⇒ bool" and P' :: "'b ⇒ bool"
  and f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a" and f' :: "'b ⇒ 'c" and g' :: "'c ⇒ 'b"
  assumes "inverse_on P f g"
  and "inverse_on P' f' g'"
  and "(P ⇛⇩m P') f"
  shows "inverse_on P (f' ∘ f) (g ∘ g')"
  using assms by (intro inverse_onI) (auto dest!: inverse_onD)

consts inverse :: "'a ⇒ 'b ⇒ bool"

overloading
  inverse ≡ "inverse :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool"
begin
  definition "(inverse :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool) ≡ inverse_on (⊤ :: 'a ⇒ bool)"
end

lemma inverse_eq_inverse_on:
  "(inverse :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool) = inverse_on (⊤ :: 'a ⇒ bool)"
  unfolding inverse_def ..

lemma inverse_eq_inverse_on_uhint [uhint]:
  assumes "P ≡  ⊤ :: 'a ⇒ bool"
  shows "inverse :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool ≡ inverse_on P"
  using assms by (simp add: inverse_eq_inverse_on)

lemma inverseI [intro]:
  assumes "⋀x. g (f x) = x"
  shows "inverse f g"
  using assms by (urule inverse_onI)

lemma inverseD:
  assumes "inverse f g"
  shows "g (f x) = x"
  using assms by (urule (d) inverse_onD where chained = insert) simp_all

lemma inverse_on_if_inverse:
  fixes P :: "'a ⇒ bool" and f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a"
  assumes "inverse f g"
  shows "inverse_on P f g"
  using assms by (intro inverse_onI) (blast dest: inverseD)

lemma right_unique_eq_app_if_injective:
  assumes "injective f"
  shows "right_unique (λy x. y = f x)"
  using assms by (auto dest: injectiveD)

lemma inverse_eval_eq_app_if_injective:
  assumes "injective f"
  shows "inverse f (eval (λy x. y = f x))"
  by (urule inverseI eval_eq_if_right_unique_onI right_unique_eq_app_if_injective)+
  (use assms in simp_all)

lemma inverse_if_injectiveE:
  assumes "injective (f :: 'a ⇒ 'b)"
  obtains g :: "'b ⇒ 'a" where "inverse f g"
  using assms inverse_eval_eq_app_if_injective by blast


end