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