src/HOL/Library/Function_Division.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 60500 903bb1495239
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned references
     1 (*  Title:      HOL/Library/Function_Division.thy
     2     Author:     Florian Haftmann, TUM
     3 *)
     4 
     5 section \<open>Pointwise instantiation of functions to division\<close>
     6 
     7 theory Function_Division
     8 imports Function_Algebras
     9 begin
    10 
    11 subsection \<open>Syntactic with division\<close>
    12 
    13 instantiation "fun" :: (type, inverse) inverse
    14 begin
    15 
    16 definition "inverse f = inverse \<circ> f"
    17 
    18 definition "f div g = (\<lambda>x. f x / g x)"
    19 
    20 instance ..
    21 
    22 end
    23 
    24 lemma inverse_fun_apply [simp]:
    25   "inverse f x = inverse (f x)"
    26   by (simp add: inverse_fun_def)
    27 
    28 lemma divide_fun_apply [simp]:
    29   "(f / g) x = f x / g x"
    30   by (simp add: divide_fun_def)
    31 
    32 text \<open>
    33   Unfortunately, we cannot lift this operations to algebraic type
    34   classes for division: being different from the constant
    35   zero function @{term "f \<noteq> 0"} is too weak as precondition.
    36   So we must introduce our own set of lemmas.
    37 \<close>
    38 
    39 abbreviation zero_free :: "('b \<Rightarrow> 'a::field) \<Rightarrow> bool" where
    40   "zero_free f \<equiv> \<not> (\<exists>x. f x = 0)"
    41 
    42 lemma fun_left_inverse:
    43   fixes f :: "'b \<Rightarrow> 'a::field"
    44   shows "zero_free f \<Longrightarrow> inverse f * f = 1"
    45   by (simp add: fun_eq_iff)
    46 
    47 lemma fun_right_inverse:
    48   fixes f :: "'b \<Rightarrow> 'a::field"
    49   shows "zero_free f \<Longrightarrow> f * inverse f = 1"
    50   by (simp add: fun_eq_iff)
    51 
    52 lemma fun_divide_inverse:
    53   fixes f g :: "'b \<Rightarrow> 'a::field"
    54   shows "f / g = f * inverse g"
    55   by (simp add: fun_eq_iff divide_inverse)
    56 
    57 text \<open>Feel free to extend this.\<close>
    58 
    59 text \<open>
    60   Another possibility would be a reformulation of the division type
    61   classes to user a @{term zero_free} predicate rather than
    62   a direct @{term "a \<noteq> 0"} condition.
    63 \<close>
    64 
    65 end