author blanchet Mon Jan 30 17:15:59 2012 +0100 (2012-01-30) changeset 46369 9ac0c64ad8e7 parent 46368 ded0390eceae child 46370 b3e53dd6f10a
example tuning
```     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.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.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.37 +              comm_semiring_1_class.normalizing_semiring_rules(24))
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.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.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.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.250 -done
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.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.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.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
```