# Theory Function_Division

```(*  Title:      HOL/Library/Function_Division.thy
Author:     Florian Haftmann, TUM
*)

section ‹Pointwise instantiation of functions to division›

theory Function_Division
imports Function_Algebras
begin

subsection ‹Syntactic with division›

instantiation "fun" :: (type, inverse) inverse
begin

definition "inverse f = inverse ∘ f"

definition "f div g = (λx. f x / g x)"

instance ..

end

lemma inverse_fun_apply [simp]:
"inverse f x = inverse (f x)"

lemma divide_fun_apply [simp]:
"(f / g) x = f x / g x"

text ‹
Unfortunately, we cannot lift this operations to algebraic type
classes for division: being different from the constant
zero function \<^term>‹f ≠ 0› is too weak as precondition.
So we must introduce our own set of lemmas.
›

abbreviation zero_free :: "('b ⇒ 'a::field) ⇒ bool" where
"zero_free f ≡ ¬ (∃x. f x = 0)"

lemma fun_left_inverse:
fixes f :: "'b ⇒ 'a::field"
shows "zero_free f ⟹ inverse f * f = 1"

lemma fun_right_inverse:
fixes f :: "'b ⇒ 'a::field"
shows "zero_free f ⟹ f * inverse f = 1"

lemma fun_divide_inverse:
fixes f g :: "'b ⇒ 'a::field"
shows "f / g = f * inverse g"