Stub theory for division on functionals.

--- a/src/HOL/IsaMakefile	Wed Jul 04 13:08:44 2012 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 05 13:24:09 2012 +0200
@@ -458,7 +458,8 @@
   Library/FinFun.thy Library/FinFun_Syntax.thy Library/Float.thy	\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
   Library/FrechetDeriv.thy Library/FuncSet.thy				\
-  Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\
+  Library/Function_Algebras.thy Library/Function_Division.thy		\
+  Library/Fundamental_Theorem_Algebra.thy				\
   Library/Glbs.thy Library/Indicator_Function.thy			\
   Library/Infinite_Set.thy Library/Inner_Product.thy			\
   Library/Kleene_Algebra.thy Library/LaTeXsugar.thy			\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Function_Division.thy	Thu Jul 05 13:24:09 2012 +0200
@@ -0,0 +1,66 @@
+(*  Title:      HOL/Library/Function_Division.thy
+    Author:     Florian Haftmann, TUM
+*)
+
+header {* Pointwise instantiation of functions to division *}
+
+theory Function_Division
+imports Function_Algebras
+begin
+
+subsection {* Syntactic with division *}
+
+instantiation "fun" :: (type, inverse) inverse
+begin
+
+definition "inverse f = inverse \<circ> f"
+
+definition "(f / g) = (\<lambda>x. f x / g x)"
+
+instance ..
+
+end
+
+lemma inverse_fun_apply [simp]:
+  "inverse f x = inverse (f x)"
+  by (simp add: inverse_fun_def)
+
+lemma divide_fun_apply [simp]:
+  "(f / g) x = f x / g x"
+  by (simp add: divide_fun_def)
+
+text {*
+  Unfortunately, we cannot lift this operations to algebraic type
+  classes for division: being different from the constant
+  zero function @{term "f \<noteq> 0"} is too weak as precondition.
+  So we must introduce our own set of lemmas.
+*}
+
+abbreviation zero_free :: "('b \<Rightarrow> 'a::field) \<Rightarrow> bool" where
+  "zero_free f \<equiv> \<not> (\<exists>x. f x = 0)"
+
+lemma fun_left_inverse:
+  fixes f :: "'b \<Rightarrow> 'a::field"
+  shows "zero_free f \<Longrightarrow> inverse f * f = 1"
+  by (simp add: fun_eq_iff)
+
+lemma fun_right_inverse:
+  fixes f :: "'b \<Rightarrow> 'a::field"
+  shows "zero_free f \<Longrightarrow> f * inverse f = 1"
+  by (simp add: fun_eq_iff)
+
+lemma fun_divide_inverse:
+  fixes f g :: "'b \<Rightarrow> 'a::field"
+  shows "f / g = f * inverse g"
+  by (simp add: fun_eq_iff divide_inverse)
+
+text {* Feel free to extend this. *}
+
+text {*
+  Another possibility would be a reformulation of the division type
+  classes to user a @{term zero_free} predicate rather than
+  a direct @{term "a \<noteq> 0"} condition.
+*}
+
+end
+

--- a/src/HOL/Library/Library.thy	Wed Jul 04 13:08:44 2012 +0200
+++ b/src/HOL/Library/Library.thy	Thu Jul 05 13:24:09 2012 +0200
@@ -20,7 +20,7 @@
   Fraction_Field
   FrechetDeriv
   FuncSet
-  Function_Algebras
+  Function_Division
   Fundamental_Theorem_Algebra
   Indicator_Function
   Infinite_Set