# HG changeset patch
# User blanchet
# Date 1284027883 -7200
# Node ID 194014eb4f9f04e6402a11e9e1968be2d2dac56e
# Parent  65903ec4e8e868cd146f9ca3b4149854863b1a65
replace two slow "metis" proofs with faster proofs

diff -r 65903ec4e8e8 -r 194014eb4f9f src/HOL/Metis_Examples/BigO.thy
--- a/src/HOL/Metis_Examples/BigO.thy	Wed Sep 08 19:22:37 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy	Thu Sep 09 12:24:43 2010 +0200
@@ -253,10 +253,9 @@
   apply (rule abs_triangle_ineq)
   apply (metis add_nonneg_nonneg)
   apply (rule add_mono)
-using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]] 
-(*Found by SPASS; SLOW*)
-apply (metis le_maxI2 linorder_linear linorder_not_le min_max.sup_absorb1 mult_le_cancel_right order_trans)
-apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
+using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
+  apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
+  apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
 done
 
 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]]
@@ -619,9 +618,25 @@
    prefer 2 
    apply simp
   apply (simp add: mult_assoc [symmetric] abs_mult)
-  (*couldn't get this proof without the step above; SLOW*)
-  apply (metis mult_assoc abs_ge_zero mult_left_mono)
-done
+  (* couldn't get this proof without the step above *)
+proof -
+  fix g :: "'b \<Rightarrow> 'a" and d :: 'a
+  assume A1: "c \<noteq> (0\<Colon>'a)"
+  assume A2: "\<forall>x\<Colon>'b. \<bar>g x\<bar> \<le> d * \<bar>f x\<bar>"
+  have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse)
+  have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff)
+  have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive)
+  hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis
+  hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less)
+  have "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar>"
+    using A2 by metis
+  hence F4: "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>"
+    using F3 by metis
+  hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^isub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^isub>7 (u * v))\<bar>)"
+    by (metis comm_mult_left_mono)
+  thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
+    using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
+qed
 
 
 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]]