|
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 |