src/HOL/Library/Function_Division.thy
 author nipkow Tue Sep 22 14:31:22 2015 +0200 (2015-09-22) changeset 61225 1a690dce8cfc parent 60500 903bb1495239 child 69593 3dda49e08b9d permissions -rw-r--r--
tuned references
 haftmann@48188 ` 1` ```(* Title: HOL/Library/Function_Division.thy ``` haftmann@48188 ` 2` ``` Author: Florian Haftmann, TUM ``` haftmann@48188 ` 3` ```*) ``` haftmann@48188 ` 4` wenzelm@60500 ` 5` ```section \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` wenzelm@60500 ` 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 \ f" ``` haftmann@48188 ` 17` haftmann@60429 ` 18` ```definition "f div g = (\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` wenzelm@60500 ` 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 \ 0"} is too weak as precondition. ``` haftmann@48188 ` 36` ``` So we must introduce our own set of lemmas. ``` wenzelm@60500 ` 37` ```\ ``` haftmann@48188 ` 38` haftmann@48188 ` 39` ```abbreviation zero_free :: "('b \ 'a::field) \ bool" where ``` haftmann@48188 ` 40` ``` "zero_free f \ \ (\x. f x = 0)" ``` haftmann@48188 ` 41` haftmann@48188 ` 42` ```lemma fun_left_inverse: ``` haftmann@48188 ` 43` ``` fixes f :: "'b \ 'a::field" ``` haftmann@48188 ` 44` ``` shows "zero_free f \ 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 \ 'a::field" ``` haftmann@48188 ` 49` ``` shows "zero_free f \ 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 \ '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` wenzelm@60500 ` 57` ```text \Feel free to extend this.\ ``` haftmann@48188 ` 58` wenzelm@60500 ` 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 \ 0"} condition. ``` wenzelm@60500 ` 63` ```\ ``` haftmann@48188 ` 64` haftmann@48188 ` 65` ```end ```