src/HOL/Library/Function_Division.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 48188 dcfe2c92fc7c child 58881 b9556a055632 permissions -rw-r--r--
simpler proof
```     1 (*  Title:      HOL/Library/Function_Division.thy
```
```     2     Author:     Florian Haftmann, TUM
```
```     3 *)
```
```     4
```
```     5 header {* Pointwise instantiation of functions to division *}
```
```     6
```
```     7 theory Function_Division
```
```     8 imports Function_Algebras
```
```     9 begin
```
```    10
```
```    11 subsection {* Syntactic with division *}
```
```    12
```
```    13 instantiation "fun" :: (type, inverse) inverse
```
```    14 begin
```
```    15
```
```    16 definition "inverse f = inverse \<circ> f"
```
```    17
```
```    18 definition "(f / 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 {*
```
```    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 *}
```
```    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 {* Feel free to extend this. *}
```
```    58
```
```    59 text {*
```
```    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 *}
```
```    64
```
```    65 end
```
```    66
```