Theory Functions_Restrict

✐‹creator "Kevin Kappelmann"›
theory Functions_Restrict
  imports HOL_Basics_Base
begin

consts fun_restrict :: "'a ⇒ 'b ⇒ 'a"

bundle fun_restrict_syntax
begin
notation fun_restrict (‹(_)↾(⇘_⇙)› [1000])
end

definition "fun_restrict_pred f P x ≡ if P x then f x else undefined"
adhoc_overloading fun_restrict ⇌ fun_restrict_pred

context
  includes fun_restrict_syntax
begin

lemma fun_restrict_eq [simp]:
  assumes "P x"
  shows "f↾⇘P⇙ x = f x"
  using assms unfolding fun_restrict_pred_def by auto

lemma fun_restrict_eq_if_not [simp]:
  assumes "¬(P x)"
  shows "f↾⇘P⇙ x = undefined"
  using assms unfolding fun_restrict_pred_def by auto

lemma fun_restrict_eq_if: "f↾⇘P⇙ x = (if P x then f x else undefined)"
  by auto

lemma fun_restrict_cong [cong]:
  assumes "P = P'"
  and "⋀x. P' x ⟹ f x = g x"
  shows "f↾⇘P⇙ = g↾⇘P'⇙"
  using assms by (intro ext) (auto simp: fun_restrict_eq_if)

end


end