transfer rule for bounded_linear of blinfun

--- a/src/HOL/Limits.thy	Tue Dec 22 21:58:27 2015 +0100
+++ b/src/HOL/Limits.thy	Wed Dec 23 14:36:45 2015 +0100
@@ -827,18 +827,6 @@
     by (rule Zfun_imp_Zfun)
 qed
 
-lemma (in bounded_bilinear) flip:
-  "bounded_bilinear (\<lambda>x y. y ** x)"
-  apply standard
-  apply (rule add_right)
-  apply (rule add_left)
-  apply (rule scaleR_right)
-  apply (rule scaleR_left)
-  apply (subst mult.commute)
-  using bounded
-  apply blast
-  done
-
 lemma (in bounded_bilinear) Bfun_prod_Zfun:
   assumes f: "Bfun f F"
   assumes g: "Zfun g F"

--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Dec 22 21:58:27 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Dec 23 14:36:45 2015 +0100
@@ -594,17 +594,26 @@
 
 subsection \<open>concrete bounded linear functions\<close>
 
-lemma bounded_linear_bounded_bilinear_blinfun_applyI: --"TODO: transfer rule!"
-  assumes n: "bounded_bilinear (\<lambda>i x. (blinfun_apply (f x) i))"
-  shows "bounded_linear f"
-proof (unfold_locales, safe intro!: blinfun_eqI)
-  fix i
-  interpret bounded_bilinear "\<lambda>i x. f x i" by fact
-  show "f (x + y) i = (f x + f y) i" "f (r *\<^sub>R x) i = (r *\<^sub>R f x) i" for r x y
-    by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
-  from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
-    by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq assms ac_simps)
-qed
+lemma transfer_bounded_bilinear_bounded_linearI:
+  assumes "g = (\<lambda>i x. (blinfun_apply (f i) x))"
+  shows "bounded_bilinear g = bounded_linear f"
+proof
+  assume "bounded_bilinear g"
+  then interpret bounded_bilinear f by (simp add: assms)
+  show "bounded_linear f"
+  proof (unfold_locales, safe intro!: blinfun_eqI)
+    fix i
+    show "f (x + y) i = (f x + f y) i" "f (r *\<^sub>R x) i = (r *\<^sub>R f x) i" for r x y
+      by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
+    from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
+      by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq ac_simps)
+  qed
+qed (auto simp: assms intro!: blinfun.comp)
+
+lemma transfer_bounded_bilinear_bounded_linear[transfer_rule]:
+  "(rel_fun (rel_fun op = (pcr_blinfun op = op =)) op =) bounded_bilinear bounded_linear"
+  by (auto simp: pcr_blinfun_def cr_blinfun_def rel_fun_def OO_def
+    intro!: transfer_bounded_bilinear_bounded_linearI)
 
 context bounded_bilinear
 begin
@@ -614,14 +623,14 @@
 declare prod_left.rep_eq[simp]
 
 lemma bounded_linear_prod_left[bounded_linear]: "bounded_linear prod_left"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_axioms)
+  by transfer (rule flip)
 
 lift_definition prod_right::"'a \<Rightarrow> 'b \<Rightarrow>\<^sub>L 'c" is "(\<lambda>a b. prod a b)"
   by (rule bounded_linear_right)
 declare prod_right.rep_eq[simp]
 
 lemma bounded_linear_prod_right[bounded_linear]: "bounded_linear prod_right"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: flip)
+  by transfer (rule bounded_bilinear_axioms)
 
 end
 
@@ -678,8 +687,7 @@
 declare blinfun_inner_right.rep_eq[simp]
 
 lemma bounded_linear_blinfun_inner_right[bounded_linear]: "bounded_linear blinfun_inner_right"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
-    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_inner])
+  by transfer (rule bounded_bilinear_inner)
 
 
 lift_definition blinfun_inner_left::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "\<lambda>x y. y \<bullet> x"
@@ -687,7 +695,7 @@
 declare blinfun_inner_left.rep_eq[simp]
 
 lemma bounded_linear_blinfun_inner_left[bounded_linear]: "bounded_linear blinfun_inner_left"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_inner)
+  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
 
 
 lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "op *\<^sub>R"
@@ -695,8 +703,7 @@
 declare blinfun_scaleR_right.rep_eq[simp]
 
 lemma bounded_linear_blinfun_scaleR_right[bounded_linear]: "bounded_linear blinfun_scaleR_right"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
-    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_scaleR])
+  by transfer (rule bounded_bilinear_scaleR)
 
 
 lift_definition blinfun_scaleR_left::"'a::real_normed_vector \<Rightarrow> real \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y *\<^sub>R x"
@@ -704,7 +711,7 @@
 lemmas [simp] = blinfun_scaleR_left.rep_eq
 
 lemma bounded_linear_blinfun_scaleR_left[bounded_linear]: "bounded_linear blinfun_scaleR_left"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_scaleR)
+  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
 
 
 lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "op *"
@@ -712,8 +719,7 @@
 declare blinfun_mult_right.rep_eq[simp]
 
 lemma bounded_linear_blinfun_mult_right[bounded_linear]: "bounded_linear blinfun_mult_right"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
-    (auto simp: bounded_bilinear.flip[OF bounded_bilinear_mult])
+  by transfer (rule bounded_bilinear_mult)
 
 
 lift_definition blinfun_mult_left::"'a::real_normed_algebra \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y * x"
@@ -721,6 +727,6 @@
 lemmas [simp] = blinfun_mult_left.rep_eq
 
 lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
-  by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_mult)
+  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
 
 end

--- a/src/HOL/Real_Vector_Spaces.thy	Tue Dec 22 21:58:27 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 23 14:36:45 2015 +0100
@@ -1435,6 +1435,43 @@
   "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
 by (simp add: diff_left diff_right)
 
+lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
+  apply standard
+  apply (rule add_right)
+  apply (rule add_left)
+  apply (rule scaleR_right)
+  apply (rule scaleR_left)
+  apply (subst mult.commute)
+  using bounded
+  apply blast
+  done
+
+lemma comp1:
+  assumes "bounded_linear g"
+  shows "bounded_bilinear (\<lambda>x. op ** (g x))"
+proof unfold_locales
+  interpret g: bounded_linear g by fact
+  show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
+    "\<And>a b b'. g a ** (b + b') = g a ** b + g a ** b'"
+    "\<And>r a b. g (r *\<^sub>R a) ** b = r *\<^sub>R (g a ** b)"
+    "\<And>a r b. g a ** (r *\<^sub>R b) = r *\<^sub>R (g a ** b)"
+    by (auto simp: g.add add_left add_right g.scaleR scaleR_left scaleR_right)
+  from g.nonneg_bounded nonneg_bounded
+  obtain K L
+  where nn: "0 \<le> K" "0 \<le> L"
+    and K: "\<And>x. norm (g x) \<le> norm x * K"
+    and L: "\<And>a b. norm (a ** b) \<le> norm a * norm b * L"
+    by auto
+  have "norm (g a ** b) \<le> norm a * K * norm b * L" for a b
+    by (auto intro!:  order_trans[OF K] order_trans[OF L] mult_mono simp: nn)
+  then show "\<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K"
+    by (auto intro!: exI[where x="K * L"] simp: ac_simps)
+qed
+
+lemma comp:
+  "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_bilinear (\<lambda>x y. f x ** g y)"
+  by (rule bounded_bilinear.flip[OF bounded_bilinear.comp1[OF bounded_bilinear.flip[OF comp1]]])
+
 end
 
 lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"