src/HOL/Library/Function_Division.thy
 author haftmann Tue Feb 19 19:44:10 2013 +0100 (2013-02-19) changeset 51188 9b5bf1a9a710 parent 48188 dcfe2c92fc7c child 58881 b9556a055632 permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
1 (*  Title:      HOL/Library/Function_Division.thy
2     Author:     Florian Haftmann, TUM
3 *)
5 header {* Pointwise instantiation of functions to division *}
7 theory Function_Division
8 imports Function_Algebras
9 begin
11 subsection {* Syntactic with division *}
13 instantiation "fun" :: (type, inverse) inverse
14 begin
16 definition "inverse f = inverse \<circ> f"
18 definition "(f / g) = (\<lambda>x. f x / g x)"
20 instance ..
22 end
24 lemma inverse_fun_apply [simp]:
25   "inverse f x = inverse (f x)"
26   by (simp add: inverse_fun_def)
28 lemma divide_fun_apply [simp]:
29   "(f / g) x = f x / g x"
30   by (simp add: divide_fun_def)
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 *}
39 abbreviation zero_free :: "('b \<Rightarrow> 'a::field) \<Rightarrow> bool" where
40   "zero_free f \<equiv> \<not> (\<exists>x. f x = 0)"
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)
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)
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)
57 text {* Feel free to extend this. *}
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 *}
65 end