1.1 --- a/src/HOL/IsaMakefile	Wed Jul 04 13:08:44 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jul 05 13:24:09 2012 +0200
     1.3 @@ -458,7 +458,8 @@
     1.4    Library/FinFun.thy Library/FinFun_Syntax.thy Library/Float.thy	\
     1.5    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
     1.6    Library/FrechetDeriv.thy Library/FuncSet.thy				\
     1.7 -  Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\
     1.8 +  Library/Function_Algebras.thy Library/Function_Division.thy		\
     1.9 +  Library/Fundamental_Theorem_Algebra.thy				\
    1.10    Library/Glbs.thy Library/Indicator_Function.thy			\
    1.11    Library/Infinite_Set.thy Library/Inner_Product.thy			\
    1.12    Library/Kleene_Algebra.thy Library/LaTeXsugar.thy			\

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Function_Division.thy	Thu Jul 05 13:24:09 2012 +0200
     2.3 @@ -0,0 +1,66 @@
     2.4 +(*  Title:      HOL/Library/Function_Division.thy
     2.5 +    Author:     Florian Haftmann, TUM
     2.6 +*)
     2.7 +
     2.8 +header {* Pointwise instantiation of functions to division *}
     2.9 +
    2.10 +theory Function_Division
    2.11 +imports Function_Algebras
    2.12 +begin
    2.13 +
    2.14 +subsection {* Syntactic with division *}
    2.15 +
    2.16 +instantiation "fun" :: (type, inverse) inverse
    2.17 +begin
    2.18 +
    2.19 +definition "inverse f = inverse \<circ> f"
    2.20 +
    2.21 +definition "(f / g) = (\<lambda>x. f x / g x)"
    2.22 +
    2.23 +instance ..
    2.24 +
    2.25 +end
    2.26 +
    2.27 +lemma inverse_fun_apply [simp]:
    2.28 +  "inverse f x = inverse (f x)"
    2.29 +  by (simp add: inverse_fun_def)
    2.30 +
    2.31 +lemma divide_fun_apply [simp]:
    2.32 +  "(f / g) x = f x / g x"
    2.33 +  by (simp add: divide_fun_def)
    2.34 +
    2.35 +text {*
    2.36 +  Unfortunately, we cannot lift this operations to algebraic type
    2.37 +  classes for division: being different from the constant
    2.38 +  zero function @{term "f \<noteq> 0"} is too weak as precondition.
    2.39 +  So we must introduce our own set of lemmas.
    2.40 +*}
    2.41 +
    2.42 +abbreviation zero_free :: "('b \<Rightarrow> 'a::field) \<Rightarrow> bool" where
    2.43 +  "zero_free f \<equiv> \<not> (\<exists>x. f x = 0)"
    2.44 +
    2.45 +lemma fun_left_inverse:
    2.46 +  fixes f :: "'b \<Rightarrow> 'a::field"
    2.47 +  shows "zero_free f \<Longrightarrow> inverse f * f = 1"
    2.48 +  by (simp add: fun_eq_iff)
    2.49 +
    2.50 +lemma fun_right_inverse:
    2.51 +  fixes f :: "'b \<Rightarrow> 'a::field"
    2.52 +  shows "zero_free f \<Longrightarrow> f * inverse f = 1"
    2.53 +  by (simp add: fun_eq_iff)
    2.54 +
    2.55 +lemma fun_divide_inverse:
    2.56 +  fixes f g :: "'b \<Rightarrow> 'a::field"
    2.57 +  shows "f / g = f * inverse g"
    2.58 +  by (simp add: fun_eq_iff divide_inverse)
    2.59 +
    2.60 +text {* Feel free to extend this. *}
    2.61 +
    2.62 +text {*
    2.63 +  Another possibility would be a reformulation of the division type
    2.64 +  classes to user a @{term zero_free} predicate rather than
    2.65 +  a direct @{term "a \<noteq> 0"} condition.
    2.66 +*}
    2.67 +
    2.68 +end
    2.69 +

     3.1 --- a/src/HOL/Library/Library.thy	Wed Jul 04 13:08:44 2012 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Thu Jul 05 13:24:09 2012 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4    Fraction_Field
     3.5    FrechetDeriv
     3.6    FuncSet
     3.7 -  Function_Algebras
     3.8 +  Function_Division
     3.9    Fundamental_Theorem_Algebra
    3.10    Indicator_Function
    3.11    Infinite_Set