src/HOL/Library/Function_Division.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 48188 dcfe2c92fc7c
child 58881 b9556a055632
permissions -rw-r--r--
more simplification rules on unary and binary minus
haftmann@48188
     1
(*  Title:      HOL/Library/Function_Division.thy
haftmann@48188
     2
    Author:     Florian Haftmann, TUM
haftmann@48188
     3
*)
haftmann@48188
     4
haftmann@48188
     5
header {* Pointwise instantiation of functions to division *}
haftmann@48188
     6
haftmann@48188
     7
theory Function_Division
haftmann@48188
     8
imports Function_Algebras
haftmann@48188
     9
begin
haftmann@48188
    10
haftmann@48188
    11
subsection {* Syntactic with division *}
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@48188
    18
definition "(f / 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
haftmann@48188
    32
text {*
haftmann@48188
    33
  Unfortunately, we cannot lift this operations to algebraic type
haftmann@48188
    34
  classes for division: being different from the constant
haftmann@48188
    35
  zero function @{term "f \<noteq> 0"} is too weak as precondition.
haftmann@48188
    36
  So we must introduce our own set of lemmas.
haftmann@48188
    37
*}
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
haftmann@48188
    57
text {* Feel free to extend this. *}
haftmann@48188
    58
haftmann@48188
    59
text {*
haftmann@48188
    60
  Another possibility would be a reformulation of the division type
haftmann@48188
    61
  classes to user a @{term zero_free} predicate rather than
haftmann@48188
    62
  a direct @{term "a \<noteq> 0"} condition.
haftmann@48188
    63
*}
haftmann@48188
    64
haftmann@48188
    65
end
haftmann@48188
    66