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
```     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>\<open>f \<noteq> 0\<close> 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>\<open>zero_free\<close> predicate rather than
```
```    62   a direct \<^term>\<open>a \<noteq> 0\<close> condition.
```
```    63 \<close>
```
```    64
```
```    65 end
```