header {* 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 o f"
definition "(f / g) = (λx. f x / g x)"
instance ..
end
lemma inverse_fun_apply [simp]:
"inverse f x = inverse (f x)"
by (simp add: inverse_fun_def)
lemma divide_fun_apply [simp]:
"(f / g) x = f x / g x"
by (simp add: divide_fun_def)
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"
by (simp add: fun_eq_iff)
lemma fun_right_inverse:
fixes f :: "'b => 'a::field"
shows "zero_free f ==> f * inverse f = 1"
by (simp add: fun_eq_iff)
lemma fun_divide_inverse:
fixes f g :: "'b => 'a::field"
shows "f / g = f * inverse g"
by (simp add: fun_eq_iff divide_inverse)
text {* Feel free to extend this. *}
text {*
Another possibility would be a reformulation of the division type
classes to user a @{term zero_free} predicate rather than
a direct @{term "a ≠ 0"} condition.
*}
end