example tuning
authorblanchet
Mon Jan 30 17:15:59 2012 +0100 (2012-01-30)
changeset 463699ac0c64ad8e7
parent 46368 ded0390eceae
child 46370 b3e53dd6f10a
example tuning
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Metis_Examples/Type_Encodings.thy
     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 17:15:59 2012 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 17:15:59 2012 +0100
     1.3 @@ -197,6 +197,7 @@
     1.4  apply clarify
     1.5  (* sledgehammer *)
     1.6  apply (rule_tac x = "max c ca" in exI)
     1.7 +
     1.8  apply (rule conjI)
     1.9   apply (metis less_max_iff_disj)
    1.10  apply clarify
    1.11 @@ -210,9 +211,8 @@
    1.12    defer 1
    1.13    apply (metis abs_triangle_ineq)
    1.14   apply (metis add_nonneg_nonneg)
    1.15 -apply (rule add_mono)
    1.16 - apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
    1.17 -by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
    1.18 +by (metis (no_types) add_mono le_maxI2 linorder_linear min_max.sup_absorb1
    1.19 +          mult_right_mono xt1(6))
    1.20  
    1.21  lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
    1.22  apply (auto simp add: bigo_def)
    1.23 @@ -234,15 +234,10 @@
    1.24  lemma bigo_bounded2: "\<forall>x. lb x <= f x \<Longrightarrow> \<forall>x. f x <= lb x + g x \<Longrightarrow> f : lb +o O(g)"
    1.25  apply (rule set_minus_imp_plus)
    1.26  apply (rule bigo_bounded)
    1.27 - apply (auto simp add: diff_minus fun_Compl_def func_plus)
    1.28 - prefer 2
    1.29 - apply (drule_tac x = x in spec)+
    1.30 - apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans)
    1.31 -proof -
    1.32 -  fix x :: 'a
    1.33 -  assume "\<forall>x. lb x \<le> f x"
    1.34 -  thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
    1.35 -qed
    1.36 + apply (metis add_le_cancel_left diff_add_cancel diff_self minus_apply
    1.37 +              comm_semiring_1_class.normalizing_semiring_rules(24))
    1.38 +by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
    1.39 +          comm_semiring_1_class.normalizing_semiring_rules(24))
    1.40  
    1.41  lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
    1.42  apply (unfold bigo_def)
    1.43 @@ -273,10 +268,8 @@
    1.44    also have "... <= O(\<lambda>x. abs (f x - g x))"
    1.45      apply (rule bigo_elt_subset)
    1.46      apply (rule bigo_bounded)
    1.47 -    apply force
    1.48 -    apply (rule allI)
    1.49 -    apply (rule abs_triangle_ineq3)
    1.50 -    done
    1.51 +     apply (metis abs_ge_zero)
    1.52 +    by (metis abs_triangle_ineq3)
    1.53    also have "... <= O(f - g)"
    1.54      apply (rule bigo_elt_subset)
    1.55      apply (subst fun_diff_def)
    1.56 @@ -296,9 +289,7 @@
    1.57    also have "... <= O(g) \<oplus> O(h)"
    1.58      by (auto del: subsetI)
    1.59    also have "... = O(\<lambda>x. abs(g x)) \<oplus> O(\<lambda>x. abs(h x))"
    1.60 -    apply (subst bigo_abs3 [symmetric])+
    1.61 -    apply (rule refl)
    1.62 -    done
    1.63 +    by (metis bigo_abs3)
    1.64    also have "... = O((\<lambda>x. abs(g x)) + (\<lambda>x. abs(h x)))"
    1.65      by (rule bigo_plus_eq [symmetric], auto)
    1.66    finally have "f : ...".
    1.67 @@ -310,39 +301,21 @@
    1.68      by (simp add: bigo_abs3 [symmetric])
    1.69  qed
    1.70  
    1.71 -lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
    1.72 -  apply (rule subsetI)
    1.73 -  apply (subst bigo_def)
    1.74 -  apply (auto simp del: abs_mult mult_ac
    1.75 -              simp add: bigo_alt_def set_times_def func_times)
    1.76 +lemma bigo_mult [intro]: "O(f) \<otimes> O(g) <= O(f * g)"
    1.77 +apply (rule subsetI)
    1.78 +apply (subst bigo_def)
    1.79 +apply (auto simp del: abs_mult mult_ac
    1.80 +            simp add: bigo_alt_def set_times_def func_times)
    1.81  (* sledgehammer *)
    1.82 -  apply (rule_tac x = "c * ca" in exI)
    1.83 -  apply(rule allI)
    1.84 -  apply(erule_tac x = x in allE)+
    1.85 -  apply(subgoal_tac "c * ca * abs(f x * g x) =
    1.86 -      (c * abs(f x)) * (ca * abs(g x))")
    1.87 -prefer 2
    1.88 -apply (metis mult_assoc mult_left_commute
    1.89 -  abs_of_pos mult_left_commute
    1.90 -  abs_mult mult_pos_pos)
    1.91 -  apply (erule ssubst)
    1.92 -  apply (subst abs_mult)
    1.93 -(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
    1.94 -   abs_mult has just been done *)
    1.95 -by (metis abs_ge_zero mult_mono')
    1.96 +apply (rule_tac x = "c * ca" in exI)
    1.97 +apply (rule allI)
    1.98 +apply (erule_tac x = x in allE)+
    1.99 +apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs(f x)) * (ca * abs (g x))")
   1.100 + apply (metis (no_types) abs_ge_zero abs_mult mult_mono')
   1.101 +by (metis mult_assoc mult_left_commute abs_of_pos mult_left_commute abs_mult)
   1.102  
   1.103  lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
   1.104 -  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
   1.105 -(* sledgehammer *)
   1.106 -  apply (rule_tac x = c in exI)
   1.107 -  apply clarify
   1.108 -  apply (drule_tac x = x in spec)
   1.109 -(*sledgehammer [no luck]*)
   1.110 -  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
   1.111 -  apply (simp add: mult_ac)
   1.112 -  apply (rule mult_left_mono, assumption)
   1.113 -  apply (rule abs_ge_zero)
   1.114 -done
   1.115 +by (metis bigo_mult bigo_refl set_times_mono3 subset_trans)
   1.116  
   1.117  lemma bigo_mult3: "f : O(h) \<Longrightarrow> g : O(j) \<Longrightarrow> f * g : O(h * j)"
   1.118  by (metis bigo_mult set_rev_mp set_times_intro)
   1.119 @@ -364,157 +337,101 @@
   1.120        by (rule bigo_mult2)
   1.121      also have "(\<lambda>x. 1 / f x) * (f * g) = g"
   1.122        apply (simp add: func_times)
   1.123 -      apply (rule ext)
   1.124 -      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
   1.125 -      done
   1.126 +      by (metis (lifting, no_types) a ext mult_ac(2) nonzero_divide_eq_eq)
   1.127      finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
   1.128      then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
   1.129        by auto
   1.130      also have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) = h"
   1.131        apply (simp add: func_times)
   1.132 -      apply (rule ext)
   1.133 -      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
   1.134 -      done
   1.135 +      by (metis (lifting, no_types) a eq_divide_imp ext
   1.136 +                comm_semiring_1_class.normalizing_semiring_rules(7))
   1.137      finally show "h : f *o O(g)".
   1.138    qed
   1.139  qed
   1.140  
   1.141 -lemma bigo_mult6: "\<forall>x. f x ~= 0 \<Longrightarrow>
   1.142 -    O(f * g) = (f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
   1.143 +lemma bigo_mult6:
   1.144 +"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = (f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
   1.145  by (metis bigo_mult2 bigo_mult5 order_antisym)
   1.146  
   1.147  (*proof requires relaxing relevance: 2007-01-25*)
   1.148  declare bigo_mult6 [simp]
   1.149  
   1.150 -lemma bigo_mult7: "\<forall>x. f x ~= 0 \<Longrightarrow>
   1.151 -    O(f * g) <= O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
   1.152 -(* sledgehammer *)
   1.153 -  apply (subst bigo_mult6)
   1.154 -  apply assumption
   1.155 -  apply (rule set_times_mono3)
   1.156 -  apply (rule bigo_refl)
   1.157 -done
   1.158 +lemma bigo_mult7:
   1.159 +"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<le> O(f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
   1.160 +by (metis bigo_refl bigo_mult6 set_times_mono3)
   1.161  
   1.162  declare bigo_mult6 [simp del]
   1.163  declare bigo_mult7 [intro!]
   1.164  
   1.165 -lemma bigo_mult8: "\<forall>x. f x ~= 0 \<Longrightarrow>
   1.166 -    O(f * g) = O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
   1.167 +lemma bigo_mult8:
   1.168 +"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
   1.169  by (metis bigo_mult bigo_mult7 order_antisym_conv)
   1.170  
   1.171  lemma bigo_minus [intro]: "f : O(g) \<Longrightarrow> - f : O(g)"
   1.172 -  by (auto simp add: bigo_def fun_Compl_def)
   1.173 +by (auto simp add: bigo_def fun_Compl_def)
   1.174  
   1.175  lemma bigo_minus2: "f : g +o O(h) \<Longrightarrow> -f : -g +o O(h)"
   1.176 -  apply (rule set_minus_imp_plus)
   1.177 -  apply (drule set_plus_imp_minus)
   1.178 -  apply (drule bigo_minus)
   1.179 -  apply (simp add: diff_minus)
   1.180 -done
   1.181 +by (metis (no_types) bigo_elt_subset bigo_minus bigo_mult4 bigo_refl
   1.182 +          comm_semiring_1_class.normalizing_semiring_rules(11) minus_mult_left
   1.183 +          set_plus_mono_b)
   1.184  
   1.185  lemma bigo_minus3: "O(-f) = O(f)"
   1.186 -  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
   1.187 +by (metis bigo_elt_subset bigo_minus bigo_refl equalityI minus_minus)
   1.188  
   1.189 -lemma bigo_plus_absorb_lemma1: "f : O(g) \<Longrightarrow> f +o O(g) <= O(g)"
   1.190 -proof -
   1.191 -  assume a: "f : O(g)"
   1.192 -  show "f +o O(g) <= O(g)"
   1.193 -  proof -
   1.194 -    have "f : O(f)" by auto
   1.195 -    then have "f +o O(g) <= O(f) \<oplus> O(g)"
   1.196 -      by (auto del: subsetI)
   1.197 -    also have "... <= O(g) \<oplus> O(g)"
   1.198 -    proof -
   1.199 -      from a have "O(f) <= O(g)" by (auto del: subsetI)
   1.200 -      thus ?thesis by (auto del: subsetI)
   1.201 -    qed
   1.202 -    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
   1.203 -    finally show ?thesis .
   1.204 -  qed
   1.205 -qed
   1.206 +lemma bigo_plus_absorb_lemma1: "f : O(g) \<Longrightarrow> f +o O(g) \<le> O(g)"
   1.207 +by (metis bigo_plus_idemp set_plus_mono3)
   1.208  
   1.209 -lemma bigo_plus_absorb_lemma2: "f : O(g) \<Longrightarrow> O(g) <= f +o O(g)"
   1.210 -proof -
   1.211 -  assume a: "f : O(g)"
   1.212 -  show "O(g) <= f +o O(g)"
   1.213 -  proof -
   1.214 -    from a have "-f : O(g)" by auto
   1.215 -    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
   1.216 -    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
   1.217 -    also have "f +o (-f +o O(g)) = O(g)"
   1.218 -      by (simp add: set_plus_rearranges)
   1.219 -    finally show ?thesis .
   1.220 -  qed
   1.221 -qed
   1.222 +lemma bigo_plus_absorb_lemma2: "f : O(g) \<Longrightarrow> O(g) \<le> f +o O(g)"
   1.223 +by (metis (no_types) bigo_minus bigo_plus_absorb_lemma1 right_minus
   1.224 +          set_plus_mono_b set_plus_rearrange2 set_zero_plus subsetI)
   1.225  
   1.226  lemma bigo_plus_absorb [simp]: "f : O(g) \<Longrightarrow> f +o O(g) = O(g)"
   1.227  by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff)
   1.228  
   1.229 -lemma bigo_plus_absorb2 [intro]: "f : O(g) \<Longrightarrow> A <= O(g) \<Longrightarrow> f +o A <= O(g)"
   1.230 -  apply (subgoal_tac "f +o A <= f +o O(g)")
   1.231 -  apply force+
   1.232 -done
   1.233 +lemma bigo_plus_absorb2 [intro]: "f : O(g) \<Longrightarrow> A <= O(g) \<Longrightarrow> f +o A \<le> O(g)"
   1.234 +by (metis bigo_plus_absorb set_plus_mono)
   1.235  
   1.236  lemma bigo_add_commute_imp: "f : g +o O(h) \<Longrightarrow> g : f +o O(h)"
   1.237 -  apply (subst set_minus_plus [symmetric])
   1.238 -  apply (subgoal_tac "g - f = - (f - g)")
   1.239 -  apply (erule ssubst)
   1.240 -  apply (rule bigo_minus)
   1.241 -  apply (subst set_minus_plus)
   1.242 -  apply assumption
   1.243 -  apply (simp add: diff_minus add_ac)
   1.244 -done
   1.245 +by (metis bigo_minus minus_diff_eq set_plus_imp_minus set_minus_plus)
   1.246  
   1.247  lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
   1.248 -  apply (rule iffI)
   1.249 -  apply (erule bigo_add_commute_imp)+
   1.250 -done
   1.251 +by (metis bigo_add_commute_imp)
   1.252  
   1.253  lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)"
   1.254  by (auto simp add: bigo_def mult_ac)
   1.255  
   1.256 -lemma (*bigo_const2 [intro]:*) "O(\<lambda>x. c) <= O(\<lambda>x. 1)"
   1.257 +lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<le> O(\<lambda>x. 1)"
   1.258  by (metis bigo_const1 bigo_elt_subset)
   1.259  
   1.260 -lemma bigo_const2 [intro]: "O(\<lambda>x. c\<Colon>'b\<Colon>{linordered_idom,number_ring}) <= O(\<lambda>x. 1)"
   1.261 -proof -
   1.262 -  have "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
   1.263 -  thus "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis bigo_elt_subset)
   1.264 -qed
   1.265 -
   1.266  lemma bigo_const3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> (\<lambda>x. 1) : O(\<lambda>x. c)"
   1.267  apply (simp add: bigo_def)
   1.268  by (metis abs_eq_0 left_inverse order_refl)
   1.269  
   1.270  lemma bigo_const4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> O(\<lambda>x. 1) <= O(\<lambda>x. c)"
   1.271 -by (rule bigo_elt_subset, rule bigo_const3, assumption)
   1.272 +by (metis bigo_elt_subset bigo_const3)
   1.273  
   1.274  lemma bigo_const [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
   1.275      O(\<lambda>x. c) = O(\<lambda>x. 1)"
   1.276 -by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   1.277 +by (metis bigo_const2 bigo_const4 equalityI)
   1.278  
   1.279  lemma bigo_const_mult1: "(\<lambda>x. c * f x) : O(f)"
   1.280 -  apply (simp add: bigo_def abs_mult)
   1.281 +apply (simp add: bigo_def abs_mult)
   1.282  by (metis le_less)
   1.283  
   1.284 -lemma bigo_const_mult2: "O(\<lambda>x. c * f x) <= O(f)"
   1.285 +lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<le> O(f)"
   1.286  by (rule bigo_elt_subset, rule bigo_const_mult1)
   1.287  
   1.288  lemma bigo_const_mult3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> f : O(\<lambda>x. c * f x)"
   1.289  apply (simp add: bigo_def)
   1.290 -(* sledgehammer *)
   1.291 -apply (rule_tac x = "abs(inverse c)" in exI)
   1.292 -apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
   1.293 -apply (subst left_inverse)
   1.294 -by auto
   1.295 +by (metis (no_types) abs_mult mult_assoc mult_1 order_refl left_inverse)
   1.296  
   1.297 -lemma bigo_const_mult4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
   1.298 -    O(f) <= O(\<lambda>x. c * f x)"
   1.299 -by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
   1.300 +lemma bigo_const_mult4:
   1.301 +"(c\<Colon>'a\<Colon>{linordered_field,number_ring}) \<noteq> 0 \<Longrightarrow> O(f) \<le> O(\<lambda>x. c * f x)"
   1.302 +by (metis bigo_elt_subset bigo_const_mult3)
   1.303  
   1.304  lemma bigo_const_mult [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
   1.305      O(\<lambda>x. c * f x) = O(f)"
   1.306 -by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   1.307 +by (metis equalityI bigo_const_mult2 bigo_const_mult4)
   1.308  
   1.309  lemma bigo_const_mult5 [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
   1.310      (\<lambda>x. c) *o O(f) = O(f)"
   1.311 @@ -563,48 +480,36 @@
   1.312    apply (rule mult_left_mono)
   1.313    apply (erule spec)
   1.314    apply simp
   1.315 -  apply(simp add: mult_ac)
   1.316 +  apply (simp add: mult_ac)
   1.317  done
   1.318  
   1.319  lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
   1.320 -proof -
   1.321 -  assume "f =o O(g)"
   1.322 -  then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"
   1.323 -    by auto
   1.324 -  also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"
   1.325 -    by (simp add: func_times)
   1.326 -  also have "(\<lambda>x. c) *o O(g) <= O(g)"
   1.327 -    by (auto del: subsetI)
   1.328 -  finally show ?thesis .
   1.329 -qed
   1.330 +by (metis bigo_const_mult1 bigo_elt_subset order_less_le psubsetD)
   1.331  
   1.332  lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f(k x)) =o O(\<lambda>x. g(k x))"
   1.333  by (unfold bigo_def, auto)
   1.334  
   1.335 -lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o
   1.336 -    O(\<lambda>x. h(k x))"
   1.337 -  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
   1.338 -      func_plus)
   1.339 -  apply (erule bigo_compose1)
   1.340 -done
   1.341 +lemma bigo_compose2:
   1.342 +"f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o O(\<lambda>x. h(k x))"
   1.343 +apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def func_plus)
   1.344 +by (erule bigo_compose1)
   1.345  
   1.346  subsection {* Setsum *}
   1.347  
   1.348  lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
   1.349      \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) <= c * (h x y) \<Longrightarrow>
   1.350        (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
   1.351 -  apply (auto simp add: bigo_def)
   1.352 -  apply (rule_tac x = "abs c" in exI)
   1.353 -  apply (subst abs_of_nonneg) back back
   1.354 -  apply (rule setsum_nonneg)
   1.355 -  apply force
   1.356 -  apply (subst setsum_right_distrib)
   1.357 -  apply (rule allI)
   1.358 -  apply (rule order_trans)
   1.359 -  apply (rule setsum_abs)
   1.360 -  apply (rule setsum_mono)
   1.361 -apply (blast intro: order_trans mult_right_mono abs_ge_self)
   1.362 -done
   1.363 +apply (auto simp add: bigo_def)
   1.364 +apply (rule_tac x = "abs c" in exI)
   1.365 +apply (subst abs_of_nonneg) back back
   1.366 + apply (rule setsum_nonneg)
   1.367 + apply force
   1.368 +apply (subst setsum_right_distrib)
   1.369 +apply (rule allI)
   1.370 +apply (rule order_trans)
   1.371 + apply (rule setsum_abs)
   1.372 +apply (rule setsum_mono)
   1.373 +by (metis abs_ge_self abs_mult_pos order_trans)
   1.374  
   1.375  lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
   1.376      \<exists>c. \<forall>x y. abs (f x y) <= c * (h x y) \<Longrightarrow>
   1.377 @@ -612,9 +517,10 @@
   1.378  by (metis (no_types) bigo_setsum_main)
   1.379  
   1.380  lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
   1.381 -    \<exists>c. \<forall>y. abs(f y) <= c * (h y) \<Longrightarrow>
   1.382 +    \<exists>c. \<forall>y. abs (f y) <= c * (h y) \<Longrightarrow>
   1.383        (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
   1.384 -by (rule bigo_setsum1, auto)
   1.385 +apply (rule bigo_setsum1)
   1.386 +by metis+
   1.387  
   1.388  lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
   1.389      (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
   1.390 @@ -624,13 +530,7 @@
   1.391   apply (rule abs_ge_zero)
   1.392  apply (unfold bigo_def)
   1.393  apply (auto simp add: abs_mult)
   1.394 -(* sledgehammer *)
   1.395 -apply (rule_tac x = c in exI)
   1.396 -apply (rule allI)+
   1.397 -apply (subst mult_left_commute)
   1.398 -apply (rule mult_left_mono)
   1.399 - apply (erule spec)
   1.400 -by (rule abs_ge_zero)
   1.401 +by (metis abs_ge_zero mult_left_commute mult_left_mono)
   1.402  
   1.403  lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
   1.404      (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
   1.405 @@ -641,22 +541,19 @@
   1.406  apply (subst setsum_subtractf [symmetric])
   1.407  apply (subst right_diff_distrib [symmetric])
   1.408  apply (rule bigo_setsum3)
   1.409 -apply (subst fun_diff_def [symmetric])
   1.410 -by (erule set_plus_imp_minus)
   1.411 +by (metis (lifting, no_types) fun_diff_def set_plus_imp_minus ext)
   1.412  
   1.413  lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
   1.414      \<forall>x. 0 <= h x \<Longrightarrow>
   1.415        (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
   1.416          O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
   1.417 -  apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
   1.418 +apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
   1.419        (\<lambda>x. SUM y : A x. abs((l x y) * h(k x y)))")
   1.420 -  apply (erule ssubst)
   1.421 -  apply (erule bigo_setsum3)
   1.422 -  apply (rule ext)
   1.423 -  apply (rule setsum_cong2)
   1.424 -  apply (thin_tac "f \<in> O(h)")
   1.425 -apply (metis abs_of_nonneg zero_le_mult_iff)
   1.426 -done
   1.427 + apply (erule ssubst)
   1.428 + apply (erule bigo_setsum3)
   1.429 +apply (rule ext)
   1.430 +apply (rule setsum_cong2)
   1.431 +by (metis abs_of_nonneg zero_le_mult_iff)
   1.432  
   1.433  lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
   1.434      \<forall>x. 0 <= h x \<Longrightarrow>
     2.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jan 30 17:15:59 2012 +0100
     2.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jan 30 17:15:59 2012 +0100
     2.3 @@ -67,7 +67,8 @@
     2.4        | tac (type_enc :: type_encs) st =
     2.5          st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
     2.6             |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
     2.7 -               THEN Metis_Tactic.metis_tac [type_enc] "combinators" ctxt ths 1
     2.8 +               THEN Metis_Tactic.metis_tac [type_enc]
     2.9 +                    ATP_Problem_Generate.combsN ctxt ths 1
    2.10                 THEN COND (has_fewer_prems 2) all_tac no_tac
    2.11                 THEN tac type_encs)
    2.12    in tac end