rephrase some slow "metis" calls
authorblanchet
Fri Feb 24 11:23:36 2012 +0100 (2012-02-24)
changeset 46644bd03e0890699
parent 46643 a88bccd2b567
child 46645 573aff6b9b0a
rephrase some slow "metis" calls
src/HOL/Metis_Examples/Big_O.thy
     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Fri Feb 24 11:23:35 2012 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Feb 24 11:23:36 2012 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4    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)
     1.5    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)
     1.6    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)
     1.7 -  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
     1.8 +  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
     1.9  qed
    1.10  
    1.11  sledgehammer_params [isar_proof, isar_shrink_factor = 4]
    1.12 @@ -211,8 +211,9 @@
    1.13    defer 1
    1.14    apply (metis abs_triangle_ineq)
    1.15   apply (metis add_nonneg_nonneg)
    1.16 -by (metis (no_types) add_mono le_maxI2 linorder_linear min_max.sup_absorb1
    1.17 -          mult_right_mono xt1(6))
    1.18 +apply (rule add_mono)
    1.19 + apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
    1.20 +by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
    1.21  
    1.22  lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
    1.23  apply (auto simp add: bigo_def)
    1.24 @@ -383,7 +384,8 @@
    1.25  
    1.26  lemma bigo_plus_absorb_lemma2: "f : O(g) \<Longrightarrow> O(g) \<le> f +o O(g)"
    1.27  by (metis (no_types) bigo_minus bigo_plus_absorb_lemma1 right_minus
    1.28 -          set_plus_mono_b set_plus_rearrange2 set_zero_plus subsetI)
    1.29 +          set_plus_mono set_plus_rearrange2 set_zero_plus subsetD subset_refl
    1.30 +          subset_trans)
    1.31  
    1.32  lemma bigo_plus_absorb [simp]: "f : O(g) \<Longrightarrow> f +o O(g) = O(g)"
    1.33  by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff)
    1.34 @@ -669,31 +671,29 @@
    1.35  apply (erule thin_rl)
    1.36  (* sledgehammer *)
    1.37  apply (case_tac "0 <= k x - g x")
    1.38 - apply (metis (hide_lams, no_types) abs_le_iff add_le_imp_le_right diff_minus le_less
    1.39 -          le_max_iff_disj min_max.le_supE min_max.sup_absorb2
    1.40 -          min_max.sup_commute)
    1.41 + apply (metis (lifting) abs_le_D1 linorder_linear min_diff_distrib_left
    1.42 +          min_max.inf_absorb1 min_max.inf_absorb2 min_max.sup_absorb1)
    1.43  by (metis abs_ge_zero le_cases min_max.sup_absorb2)
    1.44  
    1.45  lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
    1.46      \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow>
    1.47        f <o k =o O(h)"
    1.48 -  apply (unfold lesso_def)
    1.49 -  apply (rule bigo_lesseq4)
    1.50 +apply (unfold lesso_def)
    1.51 +apply (rule bigo_lesseq4)
    1.52    apply (erule set_plus_imp_minus)
    1.53 -  apply (rule allI)
    1.54 -  apply (rule le_maxI2)
    1.55 -  apply (rule allI)
    1.56 -  apply (subst fun_diff_def)
    1.57 -  apply (erule thin_rl)
    1.58 -  (* sledgehammer *)
    1.59 -  apply (case_tac "0 <= f x - k x")
    1.60 -  apply simp
    1.61 -  apply (subst abs_of_nonneg)
    1.62 + apply (rule allI)
    1.63 + apply (rule le_maxI2)
    1.64 +apply (rule allI)
    1.65 +apply (subst fun_diff_def)
    1.66 +apply (erule thin_rl)
    1.67 +(* sledgehammer *)
    1.68 +apply (case_tac "0 <= f x - k x")
    1.69 + apply simp
    1.70 + apply (subst abs_of_nonneg)
    1.71    apply (drule_tac x = x in spec) back
    1.72    apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))
    1.73   apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
    1.74 -apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
    1.75 -done
    1.76 +by (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
    1.77  
    1.78  lemma bigo_lesso4:
    1.79    "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field,number_ring}) \<Longrightarrow>