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
 haftmann@48188 ` 1` ```(* Title: HOL/Library/Function_Division.thy ``` haftmann@48188 ` 2` ``` Author: Florian Haftmann, TUM ``` haftmann@48188 ` 3` ```*) ``` haftmann@48188 ` 4` haftmann@48188 ` 5` ```header {* 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` haftmann@48188 ` 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@48188 ` 18` ```definition "(f / 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` haftmann@48188 ` 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. ``` haftmann@48188 ` 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` haftmann@48188 ` 57` ```text {* Feel free to extend this. *} ``` haftmann@48188 ` 58` haftmann@48188 ` 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. ``` haftmann@48188 ` 63` ```*} ``` haftmann@48188 ` 64` haftmann@48188 ` 65` ```end ``` haftmann@48188 ` 66`