(* Title: HOL/Library/Function_Division.thy Author: Florian Haftmann, TUM
*)
section \<open>Pointwise instantiation of functions to division\<close>
theory Function_Division imports Function_Algebras begin
subsection \<open>Syntactic with division\<close>
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)" 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\<open>
Unfortunately, we cannot lift this operations to algebraic type classesfor division: being different from the constant
zero function\<^term>\<open>f \<noteq> 0\<close> is too weak as precondition.
So we must introduce our own set of lemmas. \<close>
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\<open>Feel free to extend this.\<close>
text\<open>
Another possibility would be a reformulation of the division type classesto user a \<^term>\<open>zero_free\<close> predicate rather than
a direct \<^term>\<open>a \<noteq> 0\<close> condition. \<close>
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
