author blanchet Fri, 24 Feb 2012 11:23:36 +0100 changeset 46644 bd03e0890699 parent 46643 a88bccd2b567 child 46645 573aff6b9b0a
rephrase some slow "metis" calls
--- a/src/HOL/Metis_Examples/Big_O.thy	Fri Feb 24 11:23:35 2012 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Feb 24 11:23:36 2012 +0100
@@ -100,7 +100,7 @@
have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
-  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
qed

sledgehammer_params [isar_proof, isar_shrink_factor = 4]
@@ -211,8 +211,9 @@
defer 1
apply (metis abs_triangle_ineq)
-by (metis (no_types) add_mono le_maxI2 linorder_linear min_max.sup_absorb1
-          mult_right_mono xt1(6))
+ apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
+by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)

lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
@@ -383,7 +384,8 @@

lemma bigo_plus_absorb_lemma2: "f : O(g) \<Longrightarrow> O(g) \<le> f +o O(g)"
by (metis (no_types) bigo_minus bigo_plus_absorb_lemma1 right_minus
-          set_plus_mono_b set_plus_rearrange2 set_zero_plus subsetI)
+          set_plus_mono set_plus_rearrange2 set_zero_plus subsetD subset_refl
+          subset_trans)

lemma bigo_plus_absorb [simp]: "f : O(g) \<Longrightarrow> f +o O(g) = O(g)"
by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff)
@@ -669,31 +671,29 @@
apply (erule thin_rl)
(* sledgehammer *)
apply (case_tac "0 <= k x - g x")
- apply (metis (hide_lams, no_types) abs_le_iff add_le_imp_le_right diff_minus le_less
-          le_max_iff_disj min_max.le_supE min_max.sup_absorb2
-          min_max.sup_commute)
+ apply (metis (lifting) abs_le_D1 linorder_linear min_diff_distrib_left
+          min_max.inf_absorb1 min_max.inf_absorb2 min_max.sup_absorb1)
by (metis abs_ge_zero le_cases min_max.sup_absorb2)

lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
\<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow>
f <o k =o O(h)"
-  apply (unfold lesso_def)
-  apply (rule bigo_lesseq4)
+apply (unfold lesso_def)
+apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
-  apply (rule allI)
-  apply (rule le_maxI2)
-  apply (rule allI)
-  apply (subst fun_diff_def)
-  apply (erule thin_rl)
-  (* sledgehammer *)
-  apply (case_tac "0 <= f x - k x")
-  apply simp
-  apply (subst abs_of_nonneg)
+ apply (rule allI)
+ apply (rule le_maxI2)
+apply (rule allI)
+apply (subst fun_diff_def)
+apply (erule thin_rl)
+(* sledgehammer *)
+apply (case_tac "0 <= f x - k x")
+ apply simp
+ apply (subst abs_of_nonneg)
apply (drule_tac x = x in spec) back
apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))