1.1 --- a/src/HOL/Metis_Examples/Big_O.thy Fri Nov 18 11:47:12 2011 +0100
1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy Fri Nov 18 11:47:12 2011 +0100
1.3 @@ -10,36 +10,31 @@
1.4 theory Big_O
1.5 imports
1.6 "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
1.7 - Main
1.8 "~~/src/HOL/Library/Function_Algebras"
1.9 "~~/src/HOL/Library/Set_Algebras"
1.10 begin
1.11
1.12 -declare [[metis_new_skolemizer]]
1.13 -
1.14 subsection {* Definitions *}
1.15
1.16 -definition bigo :: "('a => 'b::{linordered_idom,number_ring}) => ('a => 'b) set" ("(1O'(_'))") where
1.17 - "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
1.18 +definition bigo :: "('a => 'b\<Colon>{linordered_idom,number_ring}) => ('a => 'b) set" ("(1O'(_'))") where
1.19 + "O(f\<Colon>('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}"
1.20
1.21 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_pos_const" ]]
1.22 -lemma bigo_pos_const: "(EX (c::'a::linordered_idom).
1.23 - ALL x. (abs (h x)) <= (c * (abs (f x))))
1.24 - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
1.25 - apply auto
1.26 - apply (case_tac "c = 0", simp)
1.27 - apply (rule_tac x = "1" in exI, simp)
1.28 - apply (rule_tac x = "abs c" in exI, auto)
1.29 - apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult)
1.30 - done
1.31 +lemma bigo_pos_const:
1.32 + "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
1.33 + \<forall>x. (abs (h x)) <= (c * (abs (f x))))
1.34 + = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
1.35 +by (metis (hide_lams, no_types) abs_ge_zero
1.36 + comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral
1.37 + mult_nonpos_nonneg not_leE order_trans zero_less_one)
1.38
1.39 (*** Now various verions with an increasing shrink factor ***)
1.40
1.41 sledgehammer_params [isar_proof, isar_shrink_factor = 1]
1.42
1.43 -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
1.44 - ALL x. (abs (h x)) <= (c * (abs (f x))))
1.45 - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
1.46 +lemma
1.47 + "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
1.48 + \<forall>x. (abs (h x)) <= (c * (abs (f x))))
1.49 + = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
1.50 apply auto
1.51 apply (case_tac "c = 0", simp)
1.52 apply (rule_tac x = "1" in exI, simp)
1.53 @@ -67,9 +62,10 @@
1.54
1.55 sledgehammer_params [isar_proof, isar_shrink_factor = 2]
1.56
1.57 -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
1.58 - ALL x. (abs (h x)) <= (c * (abs (f x))))
1.59 - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
1.60 +lemma
1.61 + "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
1.62 + \<forall>x. (abs (h x)) <= (c * (abs (f x))))
1.63 + = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
1.64 apply auto
1.65 apply (case_tac "c = 0", simp)
1.66 apply (rule_tac x = "1" in exI, simp)
1.67 @@ -89,9 +85,10 @@
1.68
1.69 sledgehammer_params [isar_proof, isar_shrink_factor = 3]
1.70
1.71 -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
1.72 - ALL x. (abs (h x)) <= (c * (abs (f x))))
1.73 - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
1.74 +lemma
1.75 + "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
1.76 + \<forall>x. (abs (h x)) <= (c * (abs (f x))))
1.77 + = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
1.78 apply auto
1.79 apply (case_tac "c = 0", simp)
1.80 apply (rule_tac x = "1" in exI, simp)
1.81 @@ -108,9 +105,10 @@
1.82
1.83 sledgehammer_params [isar_proof, isar_shrink_factor = 4]
1.84
1.85 -lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
1.86 - ALL x. (abs (h x)) <= (c * (abs (f x))))
1.87 - = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
1.88 +lemma
1.89 + "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
1.90 + \<forall>x. (abs (h x)) <= (c * (abs (f x))))
1.91 + = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
1.92 apply auto
1.93 apply (case_tac "c = 0", simp)
1.94 apply (rule_tac x = "1" in exI, simp)
1.95 @@ -127,142 +125,109 @@
1.96
1.97 sledgehammer_params [isar_proof, isar_shrink_factor = 1]
1.98
1.99 -lemma bigo_alt_def: "O(f) =
1.100 - {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
1.101 +lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c & (\<forall>x. abs (h x) <= c * abs (f x)))}"
1.102 by (auto simp add: bigo_def bigo_pos_const)
1.103
1.104 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_elt_subset" ]]
1.105 -lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
1.106 - apply (auto simp add: bigo_alt_def)
1.107 - apply (rule_tac x = "ca * c" in exI)
1.108 - apply (rule conjI)
1.109 - apply (rule mult_pos_pos)
1.110 +lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) <= O(g)"
1.111 +apply (auto simp add: bigo_alt_def)
1.112 +apply (rule_tac x = "ca * c" in exI)
1.113 +apply (rule conjI)
1.114 + apply (rule mult_pos_pos)
1.115 apply (assumption)+
1.116 -(*sledgehammer*)
1.117 - apply (rule allI)
1.118 - apply (drule_tac x = "xa" in spec)+
1.119 - apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
1.120 - apply (erule order_trans)
1.121 - apply (simp add: mult_ac)
1.122 - apply (rule mult_left_mono, assumption)
1.123 - apply (rule order_less_imp_le, assumption)
1.124 -done
1.125 +(* sledgehammer *)
1.126 +apply (rule allI)
1.127 +apply (drule_tac x = "xa" in spec)+
1.128 +apply (subgoal_tac "ca * abs (f xa) <= ca * (c * abs (g xa))")
1.129 + apply (metis comm_semiring_1_class.normalizing_semiring_rules(19)
1.130 + comm_semiring_1_class.normalizing_semiring_rules(7) order_trans)
1.131 +by (metis mult_le_cancel_left_pos)
1.132
1.133 -
1.134 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_refl" ]]
1.135 lemma bigo_refl [intro]: "f : O(f)"
1.136 apply (auto simp add: bigo_def)
1.137 by (metis mult_1 order_refl)
1.138
1.139 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_zero" ]]
1.140 lemma bigo_zero: "0 : O(g)"
1.141 apply (auto simp add: bigo_def func_zero)
1.142 by (metis mult_zero_left order_refl)
1.143
1.144 -lemma bigo_zero2: "O(%x.0) = {%x.0}"
1.145 - by (auto simp add: bigo_def)
1.146 +lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
1.147 +by (auto simp add: bigo_def)
1.148
1.149 lemma bigo_plus_self_subset [intro]:
1.150 "O(f) \<oplus> O(f) <= O(f)"
1.151 - apply (auto simp add: bigo_alt_def set_plus_def)
1.152 - apply (rule_tac x = "c + ca" in exI)
1.153 - apply auto
1.154 - apply (simp add: ring_distribs func_plus)
1.155 - apply (blast intro:order_trans abs_triangle_ineq add_mono elim:)
1.156 -done
1.157 +apply (auto simp add: bigo_alt_def set_plus_def)
1.158 +apply (rule_tac x = "c + ca" in exI)
1.159 +apply auto
1.160 +apply (simp add: ring_distribs func_plus)
1.161 +by (metis order_trans abs_triangle_ineq add_mono)
1.162
1.163 lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
1.164 - apply (rule equalityI)
1.165 - apply (rule bigo_plus_self_subset)
1.166 - apply (rule set_zero_plus2)
1.167 - apply (rule bigo_zero)
1.168 -done
1.169 +by (metis bigo_plus_self_subset bigo_zero set_eq_subset set_zero_plus2)
1.170
1.171 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
1.172 - apply (rule subsetI)
1.173 - apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
1.174 - apply (subst bigo_pos_const [symmetric])+
1.175 - apply (rule_tac x =
1.176 - "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
1.177 - apply (rule conjI)
1.178 - apply (rule_tac x = "c + c" in exI)
1.179 - apply (clarsimp)
1.180 - apply (auto)
1.181 +apply (rule subsetI)
1.182 +apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
1.183 +apply (subst bigo_pos_const [symmetric])+
1.184 +apply (rule_tac x = "\<lambda>n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
1.185 +apply (rule conjI)
1.186 + apply (rule_tac x = "c + c" in exI)
1.187 + apply clarsimp
1.188 + apply auto
1.189 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
1.190 - apply (erule_tac x = xa in allE)
1.191 - apply (erule order_trans)
1.192 - apply (simp)
1.193 + apply (metis mult_2 order_trans)
1.194 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
1.195 + apply (erule order_trans)
1.196 + apply (simp add: ring_distribs)
1.197 + apply (rule mult_left_mono)
1.198 + apply (simp add: abs_triangle_ineq)
1.199 + apply (simp add: order_less_le)
1.200 + apply (rule mult_nonneg_nonneg)
1.201 + apply auto
1.202 +apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
1.203 +apply (rule conjI)
1.204 + apply (rule_tac x = "c + c" in exI)
1.205 + apply auto
1.206 + apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
1.207 + apply (metis order_trans semiring_mult_2)
1.208 + apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
1.209 apply (erule order_trans)
1.210 apply (simp add: ring_distribs)
1.211 - apply (rule mult_left_mono)
1.212 - apply (simp add: abs_triangle_ineq)
1.213 - apply (simp add: order_less_le)
1.214 - apply (rule mult_nonneg_nonneg)
1.215 - apply auto
1.216 - apply (rule_tac x = "%n. if (abs (f n)) < abs (g n) then x n else 0"
1.217 - in exI)
1.218 - apply (rule conjI)
1.219 - apply (rule_tac x = "c + c" in exI)
1.220 - apply auto
1.221 - apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
1.222 - apply (erule_tac x = xa in allE)
1.223 - apply (erule order_trans)
1.224 - apply (simp)
1.225 - apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
1.226 - apply (erule order_trans)
1.227 - apply (simp add: ring_distribs)
1.228 - apply (rule mult_left_mono)
1.229 - apply (rule abs_triangle_ineq)
1.230 - apply (simp add: order_less_le)
1.231 -apply (metis abs_not_less_zero even_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
1.232 -done
1.233 + apply (metis abs_triangle_ineq mult_le_cancel_left_pos)
1.234 +by (metis abs_ge_zero abs_of_pos zero_le_mult_iff)
1.235
1.236 -lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
1.237 - apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
1.238 - apply (erule order_trans)
1.239 - apply simp
1.240 - apply (auto del: subsetI simp del: bigo_plus_idemp)
1.241 -done
1.242 +lemma bigo_plus_subset2 [intro]: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> A \<oplus> B <= O(f)"
1.243 +by (metis bigo_plus_idemp set_plus_mono2)
1.244
1.245 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq" ]]
1.246 -lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==>
1.247 - O(f + g) = O(f) \<oplus> O(g)"
1.248 - apply (rule equalityI)
1.249 - apply (rule bigo_plus_subset)
1.250 - apply (simp add: bigo_alt_def set_plus_def func_plus)
1.251 - apply clarify
1.252 -(*sledgehammer*)
1.253 - apply (rule_tac x = "max c ca" in exI)
1.254 - apply (rule conjI)
1.255 - apply (metis Orderings.less_max_iff_disj)
1.256 - apply clarify
1.257 - apply (drule_tac x = "xa" in spec)+
1.258 - apply (subgoal_tac "0 <= f xa + g xa")
1.259 - apply (simp add: ring_distribs)
1.260 - apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
1.261 - apply (subgoal_tac "abs(a xa) + abs(b xa) <=
1.262 - max c ca * f xa + max c ca * g xa")
1.263 - apply (blast intro: order_trans)
1.264 +lemma bigo_plus_eq: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. 0 <= g x \<Longrightarrow> O(f + g) = O(f) \<oplus> O(g)"
1.265 +apply (rule equalityI)
1.266 +apply (rule bigo_plus_subset)
1.267 +apply (simp add: bigo_alt_def set_plus_def func_plus)
1.268 +apply clarify
1.269 +(* sledgehammer *)
1.270 +apply (rule_tac x = "max c ca" in exI)
1.271 +apply (rule conjI)
1.272 + apply (metis less_max_iff_disj)
1.273 +apply clarify
1.274 +apply (drule_tac x = "xa" in spec)+
1.275 +apply (subgoal_tac "0 <= f xa + g xa")
1.276 + apply (simp add: ring_distribs)
1.277 + apply (subgoal_tac "abs (a xa + b xa) <= abs (a xa) + abs (b xa)")
1.278 + apply (subgoal_tac "abs (a xa) + abs (b xa) <=
1.279 + max c ca * f xa + max c ca * g xa")
1.280 + apply (metis order_trans)
1.281 defer 1
1.282 - apply (rule abs_triangle_ineq)
1.283 - apply (metis add_nonneg_nonneg)
1.284 - apply (rule add_mono)
1.285 -using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
1.286 - apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
1.287 - apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
1.288 -done
1.289 + apply (metis abs_triangle_ineq)
1.290 + apply (metis add_nonneg_nonneg)
1.291 +apply (rule add_mono)
1.292 + apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
1.293 +by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
1.294
1.295 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]]
1.296 -lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
1.297 - f : O(g)"
1.298 - apply (auto simp add: bigo_def)
1.299 +lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
1.300 +apply (auto simp add: bigo_def)
1.301 (* Version 1: one-line proof *)
1.302 - apply (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult)
1.303 - done
1.304 +by (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult)
1.305
1.306 -lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
1.307 - f : O(g)"
1.308 +lemma "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
1.309 apply (auto simp add: bigo_def)
1.310 (* Version 2: structured proof *)
1.311 proof -
1.312 @@ -270,32 +235,11 @@
1.313 thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
1.314 qed
1.315
1.316 -text{*So here is the easier (and more natural) problem using transitivity*}
1.317 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
1.318 -lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
1.319 -apply (auto simp add: bigo_def)
1.320 -(* Version 1: one-line proof *)
1.321 -by (metis abs_ge_self abs_mult order_trans)
1.322 +lemma bigo_bounded: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= g x \<Longrightarrow> f : O(g)"
1.323 +apply (erule bigo_bounded_alt [of f 1 g])
1.324 +by (metis mult_1)
1.325
1.326 -text{*So here is the easier (and more natural) problem using transitivity*}
1.327 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
1.328 -lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
1.329 - apply (auto simp add: bigo_def)
1.330 -(* Version 2: structured proof *)
1.331 -proof -
1.332 - assume "\<forall>x. f x \<le> c * g x"
1.333 - thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
1.334 -qed
1.335 -
1.336 -lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==>
1.337 - f : O(g)"
1.338 - apply (erule bigo_bounded_alt [of f 1 g])
1.339 - apply simp
1.340 -done
1.341 -
1.342 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded2" ]]
1.343 -lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
1.344 - f : lb +o O(g)"
1.345 +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.346 apply (rule set_minus_imp_plus)
1.347 apply (rule bigo_bounded)
1.348 apply (auto simp add: diff_minus fun_Compl_def func_plus)
1.349 @@ -308,19 +252,17 @@
1.350 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.351 qed
1.352
1.353 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs" ]]
1.354 -lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
1.355 +lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
1.356 apply (unfold bigo_def)
1.357 apply auto
1.358 by (metis mult_1 order_refl)
1.359
1.360 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs2" ]]
1.361 -lemma bigo_abs2: "f =o O(%x. abs(f x))"
1.362 +lemma bigo_abs2: "f =o O(\<lambda>x. abs(f x))"
1.363 apply (unfold bigo_def)
1.364 apply auto
1.365 by (metis mult_1 order_refl)
1.366
1.367 -lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
1.368 +lemma bigo_abs3: "O(f) = O(\<lambda>x. abs(f x))"
1.369 proof -
1.370 have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
1.371 have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
1.372 @@ -328,16 +270,15 @@
1.373 thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
1.374 qed
1.375
1.376 -lemma bigo_abs4: "f =o g +o O(h) ==>
1.377 - (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
1.378 +lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
1.379 apply (drule set_plus_imp_minus)
1.380 apply (rule set_minus_imp_plus)
1.381 apply (subst fun_diff_def)
1.382 proof -
1.383 assume a: "f - g : O(h)"
1.384 - have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
1.385 + have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs(abs (f x) - abs (g x)))"
1.386 by (rule bigo_abs2)
1.387 - also have "... <= O(%x. abs (f x - g x))"
1.388 + also have "... <= O(\<lambda>x. abs (f x - g x))"
1.389 apply (rule bigo_elt_subset)
1.390 apply (rule bigo_bounded)
1.391 apply force
1.392 @@ -351,45 +292,43 @@
1.393 done
1.394 also have "... <= O(h)"
1.395 using a by (rule bigo_elt_subset)
1.396 - finally show "(%x. abs (f x) - abs (g x)) : O(h)".
1.397 + finally show "(\<lambda>x. abs (f x) - abs (g x)) : O(h)".
1.398 qed
1.399
1.400 -lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)"
1.401 +lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs(f x)) =o O(g)"
1.402 by (unfold bigo_def, auto)
1.403
1.404 -lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
1.405 +lemma bigo_elt_subset2 [intro]: "f : g +o O(h) \<Longrightarrow> O(f) <= O(g) \<oplus> O(h)"
1.406 proof -
1.407 assume "f : g +o O(h)"
1.408 also have "... <= O(g) \<oplus> O(h)"
1.409 by (auto del: subsetI)
1.410 - also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
1.411 + also have "... = O(\<lambda>x. abs(g x)) \<oplus> O(\<lambda>x. abs(h x))"
1.412 apply (subst bigo_abs3 [symmetric])+
1.413 apply (rule refl)
1.414 done
1.415 - also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
1.416 + also have "... = O((\<lambda>x. abs(g x)) + (\<lambda>x. abs(h x)))"
1.417 by (rule bigo_plus_eq [symmetric], auto)
1.418 finally have "f : ...".
1.419 then have "O(f) <= ..."
1.420 by (elim bigo_elt_subset)
1.421 - also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
1.422 + also have "... = O(\<lambda>x. abs(g x)) \<oplus> O(\<lambda>x. abs(h x))"
1.423 by (rule bigo_plus_eq, auto)
1.424 finally show ?thesis
1.425 by (simp add: bigo_abs3 [symmetric])
1.426 qed
1.427
1.428 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult" ]]
1.429 lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
1.430 apply (rule subsetI)
1.431 apply (subst bigo_def)
1.432 apply (auto simp del: abs_mult mult_ac
1.433 simp add: bigo_alt_def set_times_def func_times)
1.434 -(*sledgehammer*)
1.435 +(* sledgehammer *)
1.436 apply (rule_tac x = "c * ca" in exI)
1.437 apply(rule allI)
1.438 apply(erule_tac x = x in allE)+
1.439 apply(subgoal_tac "c * ca * abs(f x * g x) =
1.440 (c * abs(f x)) * (ca * abs(g x))")
1.441 -using [[ sledgehammer_problem_prefix = "BigO__bigo_mult_simpler" ]]
1.442 prefer 2
1.443 apply (metis mult_assoc mult_left_commute
1.444 abs_of_pos mult_left_commute
1.445 @@ -400,14 +339,12 @@
1.446 abs_mult has just been done *)
1.447 by (metis abs_ge_zero mult_mono')
1.448
1.449 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult2" ]]
1.450 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
1.451 apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
1.452 -(*sledgehammer*)
1.453 +(* sledgehammer *)
1.454 apply (rule_tac x = c in exI)
1.455 apply clarify
1.456 apply (drule_tac x = x in spec)
1.457 -using [[ sledgehammer_problem_prefix = "BigO__bigo_mult2_simpler" ]]
1.458 (*sledgehammer [no luck]*)
1.459 apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
1.460 apply (simp add: mult_ac)
1.461 @@ -415,36 +352,33 @@
1.462 apply (rule abs_ge_zero)
1.463 done
1.464
1.465 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult3" ]]
1.466 -lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
1.467 +lemma bigo_mult3: "f : O(h) \<Longrightarrow> g : O(j) \<Longrightarrow> f * g : O(h * j)"
1.468 by (metis bigo_mult set_rev_mp set_times_intro)
1.469
1.470 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult4" ]]
1.471 -lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
1.472 +lemma bigo_mult4 [intro]:"f : k +o O(h) \<Longrightarrow> g * f : (g * k) +o O(g * h)"
1.473 by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
1.474
1.475 -
1.476 -lemma bigo_mult5: "ALL x. f x ~= 0 ==>
1.477 - O(f * g) <= (f::'a => ('b::{linordered_field,number_ring})) *o O(g)"
1.478 +lemma bigo_mult5: "\<forall>x. f x ~= 0 \<Longrightarrow>
1.479 + O(f * g) <= (f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
1.480 proof -
1.481 - assume a: "ALL x. f x ~= 0"
1.482 + assume a: "\<forall>x. f x ~= 0"
1.483 show "O(f * g) <= f *o O(g)"
1.484 proof
1.485 fix h
1.486 assume h: "h : O(f * g)"
1.487 - then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
1.488 + then have "(\<lambda>x. 1 / (f x)) * h : (\<lambda>x. 1 / f x) *o O(f * g)"
1.489 by auto
1.490 - also have "... <= O((%x. 1 / f x) * (f * g))"
1.491 + also have "... <= O((\<lambda>x. 1 / f x) * (f * g))"
1.492 by (rule bigo_mult2)
1.493 - also have "(%x. 1 / f x) * (f * g) = g"
1.494 + also have "(\<lambda>x. 1 / f x) * (f * g) = g"
1.495 apply (simp add: func_times)
1.496 apply (rule ext)
1.497 apply (simp add: a h nonzero_divide_eq_eq mult_ac)
1.498 done
1.499 - finally have "(%x. (1::'b) / f x) * h : O(g)".
1.500 - then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
1.501 + finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
1.502 + then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
1.503 by auto
1.504 - also have "f * ((%x. (1::'b) / f x) * h) = h"
1.505 + also have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) = h"
1.506 apply (simp add: func_times)
1.507 apply (rule ext)
1.508 apply (simp add: a h nonzero_divide_eq_eq mult_ac)
1.509 @@ -453,34 +387,32 @@
1.510 qed
1.511 qed
1.512
1.513 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult6" ]]
1.514 -lemma bigo_mult6: "ALL x. f x ~= 0 ==>
1.515 - O(f * g) = (f::'a => ('b::{linordered_field,number_ring})) *o O(g)"
1.516 +lemma bigo_mult6: "\<forall>x. f x ~= 0 \<Longrightarrow>
1.517 + O(f * g) = (f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
1.518 by (metis bigo_mult2 bigo_mult5 order_antisym)
1.519
1.520 (*proof requires relaxing relevance: 2007-01-25*)
1.521 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult7" ]]
1.522 declare bigo_mult6 [simp]
1.523 -lemma bigo_mult7: "ALL x. f x ~= 0 ==>
1.524 - O(f * g) <= O(f::'a => ('b::{linordered_field,number_ring})) \<otimes> O(g)"
1.525 -(*sledgehammer*)
1.526 +lemma bigo_mult7: "\<forall>x. f x ~= 0 \<Longrightarrow>
1.527 + O(f * g) <= O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
1.528 +(* sledgehammer *)
1.529 apply (subst bigo_mult6)
1.530 apply assumption
1.531 apply (rule set_times_mono3)
1.532 apply (rule bigo_refl)
1.533 done
1.534 - declare bigo_mult6 [simp del]
1.535
1.536 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult8" ]]
1.537 - declare bigo_mult7[intro!]
1.538 -lemma bigo_mult8: "ALL x. f x ~= 0 ==>
1.539 - O(f * g) = O(f::'a => ('b::{linordered_field,number_ring})) \<otimes> O(g)"
1.540 +declare bigo_mult6 [simp del]
1.541 +declare bigo_mult7 [intro!]
1.542 +
1.543 +lemma bigo_mult8: "\<forall>x. f x ~= 0 \<Longrightarrow>
1.544 + O(f * g) = O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
1.545 by (metis bigo_mult bigo_mult7 order_antisym_conv)
1.546
1.547 -lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
1.548 +lemma bigo_minus [intro]: "f : O(g) \<Longrightarrow> - f : O(g)"
1.549 by (auto simp add: bigo_def fun_Compl_def)
1.550
1.551 -lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
1.552 +lemma bigo_minus2: "f : g +o O(h) \<Longrightarrow> -f : -g +o O(h)"
1.553 apply (rule set_minus_imp_plus)
1.554 apply (drule set_plus_imp_minus)
1.555 apply (drule bigo_minus)
1.556 @@ -490,7 +422,7 @@
1.557 lemma bigo_minus3: "O(-f) = O(f)"
1.558 by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
1.559
1.560 -lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
1.561 +lemma bigo_plus_absorb_lemma1: "f : O(g) \<Longrightarrow> f +o O(g) <= O(g)"
1.562 proof -
1.563 assume a: "f : O(g)"
1.564 show "f +o O(g) <= O(g)"
1.565 @@ -508,7 +440,7 @@
1.566 qed
1.567 qed
1.568
1.569 -lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
1.570 +lemma bigo_plus_absorb_lemma2: "f : O(g) \<Longrightarrow> O(g) <= f +o O(g)"
1.571 proof -
1.572 assume a: "f : O(g)"
1.573 show "O(g) <= f +o O(g)"
1.574 @@ -522,23 +454,22 @@
1.575 qed
1.576 qed
1.577
1.578 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_absorb" ]]
1.579 -lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
1.580 +lemma bigo_plus_absorb [simp]: "f : O(g) \<Longrightarrow> f +o O(g) = O(g)"
1.581 by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff)
1.582
1.583 -lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
1.584 +lemma bigo_plus_absorb2 [intro]: "f : O(g) \<Longrightarrow> A <= O(g) \<Longrightarrow> f +o A <= O(g)"
1.585 apply (subgoal_tac "f +o A <= f +o O(g)")
1.586 apply force+
1.587 done
1.588
1.589 -lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
1.590 +lemma bigo_add_commute_imp: "f : g +o O(h) \<Longrightarrow> g : f +o O(h)"
1.591 apply (subst set_minus_plus [symmetric])
1.592 apply (subgoal_tac "g - f = - (f - g)")
1.593 apply (erule ssubst)
1.594 apply (rule bigo_minus)
1.595 apply (subst set_minus_plus)
1.596 apply assumption
1.597 - apply (simp add: diff_minus add_ac)
1.598 + apply (simp add: diff_minus add_ac)
1.599 done
1.600
1.601 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
1.602 @@ -546,67 +477,60 @@
1.603 apply (erule bigo_add_commute_imp)+
1.604 done
1.605
1.606 -lemma bigo_const1: "(%x. c) : O(%x. 1)"
1.607 +lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)"
1.608 by (auto simp add: bigo_def mult_ac)
1.609
1.610 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const2" ]]
1.611 -lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
1.612 +lemma (*bigo_const2 [intro]:*) "O(\<lambda>x. c) <= O(\<lambda>x. 1)"
1.613 by (metis bigo_const1 bigo_elt_subset)
1.614
1.615 -lemma bigo_const2 [intro]: "O(%x. c::'b::{linordered_idom,number_ring}) <= O(%x. 1)"
1.616 -(* "thus" had to be replaced by "show" with an explicit reference to "F1" *)
1.617 +lemma bigo_const2 [intro]: "O(\<lambda>x. c\<Colon>'b\<Colon>{linordered_idom,number_ring}) <= O(\<lambda>x. 1)"
1.618 proof -
1.619 - have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
1.620 - show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset)
1.621 + have "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
1.622 + thus "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis bigo_elt_subset)
1.623 qed
1.624
1.625 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const3" ]]
1.626 -lemma bigo_const3: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> (%x. 1) : O(%x. c)"
1.627 +lemma bigo_const3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> (\<lambda>x. 1) : O(\<lambda>x. c)"
1.628 apply (simp add: bigo_def)
1.629 by (metis abs_eq_0 left_inverse order_refl)
1.630
1.631 -lemma bigo_const4: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> O(%x. 1) <= O(%x. c)"
1.632 +lemma bigo_const4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> O(\<lambda>x. 1) <= O(\<lambda>x. c)"
1.633 by (rule bigo_elt_subset, rule bigo_const3, assumption)
1.634
1.635 -lemma bigo_const [simp]: "(c::'a::{linordered_field,number_ring}) ~= 0 ==>
1.636 - O(%x. c) = O(%x. 1)"
1.637 +lemma bigo_const [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
1.638 + O(\<lambda>x. c) = O(\<lambda>x. 1)"
1.639 by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
1.640
1.641 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult1" ]]
1.642 -lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
1.643 +lemma bigo_const_mult1: "(\<lambda>x. c * f x) : O(f)"
1.644 apply (simp add: bigo_def abs_mult)
1.645 by (metis le_less)
1.646
1.647 -lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
1.648 +lemma bigo_const_mult2: "O(\<lambda>x. c * f x) <= O(f)"
1.649 by (rule bigo_elt_subset, rule bigo_const_mult1)
1.650
1.651 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult3" ]]
1.652 -lemma bigo_const_mult3: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> f : O(%x. c * f x)"
1.653 - apply (simp add: bigo_def)
1.654 -(*sledgehammer [no luck]*)
1.655 - apply (rule_tac x = "abs(inverse c)" in exI)
1.656 - apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
1.657 +lemma bigo_const_mult3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> f : O(\<lambda>x. c * f x)"
1.658 +apply (simp add: bigo_def)
1.659 +(* sledgehammer *)
1.660 +apply (rule_tac x = "abs(inverse c)" in exI)
1.661 +apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
1.662 apply (subst left_inverse)
1.663 -apply (auto )
1.664 -done
1.665 +by auto
1.666
1.667 -lemma bigo_const_mult4: "(c::'a::{linordered_field,number_ring}) ~= 0 ==>
1.668 - O(f) <= O(%x. c * f x)"
1.669 +lemma bigo_const_mult4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
1.670 + O(f) <= O(\<lambda>x. c * f x)"
1.671 by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
1.672
1.673 -lemma bigo_const_mult [simp]: "(c::'a::{linordered_field,number_ring}) ~= 0 ==>
1.674 - O(%x. c * f x) = O(f)"
1.675 +lemma bigo_const_mult [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
1.676 + O(\<lambda>x. c * f x) = O(f)"
1.677 by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
1.678
1.679 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult5" ]]
1.680 -lemma bigo_const_mult5 [simp]: "(c::'a::{linordered_field,number_ring}) ~= 0 ==>
1.681 - (%x. c) *o O(f) = O(f)"
1.682 +lemma bigo_const_mult5 [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
1.683 + (\<lambda>x. c) *o O(f) = O(f)"
1.684 apply (auto del: subsetI)
1.685 apply (rule order_trans)
1.686 apply (rule bigo_mult2)
1.687 apply (simp add: func_times)
1.688 apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
1.689 - apply (rule_tac x = "%y. inverse c * x y" in exI)
1.690 + apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
1.691 apply (rename_tac g d)
1.692 apply safe
1.693 apply (rule_tac [2] ext)
1.694 @@ -633,13 +557,11 @@
1.695 using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
1.696 qed
1.697
1.698 -
1.699 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]]
1.700 -lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
1.701 +lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
1.702 apply (auto intro!: subsetI
1.703 simp add: bigo_def elt_set_times_def func_times
1.704 simp del: abs_mult mult_ac)
1.705 -(*sledgehammer*)
1.706 +(* sledgehammer *)
1.707 apply (rule_tac x = "ca * (abs c)" in exI)
1.708 apply (rule allI)
1.709 apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
1.710 @@ -651,23 +573,23 @@
1.711 apply(simp add: mult_ac)
1.712 done
1.713
1.714 -lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
1.715 +lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
1.716 proof -
1.717 assume "f =o O(g)"
1.718 - then have "(%x. c) * f =o (%x. c) *o O(g)"
1.719 + then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"
1.720 by auto
1.721 - also have "(%x. c) * f = (%x. c * f x)"
1.722 + also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"
1.723 by (simp add: func_times)
1.724 - also have "(%x. c) *o O(g) <= O(g)"
1.725 + also have "(\<lambda>x. c) *o O(g) <= O(g)"
1.726 by (auto del: subsetI)
1.727 finally show ?thesis .
1.728 qed
1.729
1.730 -lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
1.731 +lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f(k x)) =o O(\<lambda>x. g(k x))"
1.732 by (unfold bigo_def, auto)
1.733
1.734 -lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o
1.735 - O(%x. h(k x))"
1.736 +lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o
1.737 + O(\<lambda>x. h(k x))"
1.738 apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
1.739 func_plus)
1.740 apply (erule bigo_compose1)
1.741 @@ -675,9 +597,9 @@
1.742
1.743 subsection {* Setsum *}
1.744
1.745 -lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==>
1.746 - EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
1.747 - (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
1.748 +lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
1.749 + \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) <= c * (h x y) \<Longrightarrow>
1.750 + (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
1.751 apply (auto simp add: bigo_def)
1.752 apply (rule_tac x = "abs c" in exI)
1.753 apply (subst abs_of_nonneg) back back
1.754 @@ -691,61 +613,50 @@
1.755 apply (blast intro: order_trans mult_right_mono abs_ge_self)
1.756 done
1.757
1.758 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum1" ]]
1.759 -lemma bigo_setsum1: "ALL x y. 0 <= h x y ==>
1.760 - EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
1.761 - (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
1.762 - apply (rule bigo_setsum_main)
1.763 -(*sledgehammer*)
1.764 - apply force
1.765 - apply clarsimp
1.766 - apply (rule_tac x = c in exI)
1.767 - apply force
1.768 -done
1.769 +lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
1.770 + \<exists>c. \<forall>x y. abs (f x y) <= c * (h x y) \<Longrightarrow>
1.771 + (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
1.772 +by (metis (no_types) bigo_setsum_main)
1.773
1.774 -lemma bigo_setsum2: "ALL y. 0 <= h y ==>
1.775 - EX c. ALL y. abs(f y) <= c * (h y) ==>
1.776 - (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
1.777 +lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
1.778 + \<exists>c. \<forall>y. abs(f y) <= c * (h y) \<Longrightarrow>
1.779 + (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
1.780 by (rule bigo_setsum1, auto)
1.781
1.782 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum3" ]]
1.783 -lemma bigo_setsum3: "f =o O(h) ==>
1.784 - (%x. SUM y : A x. (l x y) * f(k x y)) =o
1.785 - O(%x. SUM y : A x. abs(l x y * h(k x y)))"
1.786 - apply (rule bigo_setsum1)
1.787 - apply (rule allI)+
1.788 - apply (rule abs_ge_zero)
1.789 - apply (unfold bigo_def)
1.790 - apply (auto simp add: abs_mult)
1.791 -(*sledgehammer*)
1.792 - apply (rule_tac x = c in exI)
1.793 - apply (rule allI)+
1.794 - apply (subst mult_left_commute)
1.795 - apply (rule mult_left_mono)
1.796 - apply (erule spec)
1.797 - apply (rule abs_ge_zero)
1.798 -done
1.799 +lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
1.800 + (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
1.801 + O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
1.802 +apply (rule bigo_setsum1)
1.803 + apply (rule allI)+
1.804 + apply (rule abs_ge_zero)
1.805 +apply (unfold bigo_def)
1.806 +apply (auto simp add: abs_mult)
1.807 +(* sledgehammer *)
1.808 +apply (rule_tac x = c in exI)
1.809 +apply (rule allI)+
1.810 +apply (subst mult_left_commute)
1.811 +apply (rule mult_left_mono)
1.812 + apply (erule spec)
1.813 +by (rule abs_ge_zero)
1.814
1.815 -lemma bigo_setsum4: "f =o g +o O(h) ==>
1.816 - (%x. SUM y : A x. l x y * f(k x y)) =o
1.817 - (%x. SUM y : A x. l x y * g(k x y)) +o
1.818 - O(%x. SUM y : A x. abs(l x y * h(k x y)))"
1.819 - apply (rule set_minus_imp_plus)
1.820 - apply (subst fun_diff_def)
1.821 - apply (subst setsum_subtractf [symmetric])
1.822 - apply (subst right_diff_distrib [symmetric])
1.823 - apply (rule bigo_setsum3)
1.824 - apply (subst fun_diff_def [symmetric])
1.825 - apply (erule set_plus_imp_minus)
1.826 -done
1.827 +lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
1.828 + (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
1.829 + (\<lambda>x. SUM y : A x. l x y * g(k x y)) +o
1.830 + O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
1.831 +apply (rule set_minus_imp_plus)
1.832 +apply (subst fun_diff_def)
1.833 +apply (subst setsum_subtractf [symmetric])
1.834 +apply (subst right_diff_distrib [symmetric])
1.835 +apply (rule bigo_setsum3)
1.836 +apply (subst fun_diff_def [symmetric])
1.837 +by (erule set_plus_imp_minus)
1.838
1.839 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum5" ]]
1.840 -lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==>
1.841 - ALL x. 0 <= h x ==>
1.842 - (%x. SUM y : A x. (l x y) * f(k x y)) =o
1.843 - O(%x. SUM y : A x. (l x y) * h(k x y))"
1.844 - apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) =
1.845 - (%x. SUM y : A x. abs((l x y) * h(k x y)))")
1.846 +lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
1.847 + \<forall>x. 0 <= h x \<Longrightarrow>
1.848 + (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
1.849 + O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
1.850 + apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
1.851 + (\<lambda>x. SUM y : A x. abs((l x y) * h(k x y)))")
1.852 apply (erule ssubst)
1.853 apply (erule bigo_setsum3)
1.854 apply (rule ext)
1.855 @@ -754,11 +665,11 @@
1.856 apply (metis abs_of_nonneg zero_le_mult_iff)
1.857 done
1.858
1.859 -lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
1.860 - ALL x. 0 <= h x ==>
1.861 - (%x. SUM y : A x. (l x y) * f(k x y)) =o
1.862 - (%x. SUM y : A x. (l x y) * g(k x y)) +o
1.863 - O(%x. SUM y : A x. (l x y) * h(k x y))"
1.864 +lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
1.865 + \<forall>x. 0 <= h x \<Longrightarrow>
1.866 + (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
1.867 + (\<lambda>x. SUM y : A x. (l x y) * g(k x y)) +o
1.868 + O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
1.869 apply (rule set_minus_imp_plus)
1.870 apply (subst fun_diff_def)
1.871 apply (subst setsum_subtractf [symmetric])
1.872 @@ -771,50 +682,39 @@
1.873
1.874 subsection {* Misc useful stuff *}
1.875
1.876 -lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
1.877 +lemma bigo_useful_intro: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow>
1.878 A \<oplus> B <= O(f)"
1.879 apply (subst bigo_plus_idemp [symmetric])
1.880 apply (rule set_plus_mono2)
1.881 apply assumption+
1.882 done
1.883
1.884 -lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
1.885 +lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)"
1.886 apply (subst bigo_plus_idemp [symmetric])
1.887 apply (rule set_plus_intro)
1.888 apply assumption+
1.889 done
1.890
1.891 -lemma bigo_useful_const_mult: "(c::'a::{linordered_field,number_ring}) ~= 0 ==>
1.892 - (%x. c) * f =o O(h) ==> f =o O(h)"
1.893 +lemma bigo_useful_const_mult: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
1.894 + (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"
1.895 apply (rule subsetD)
1.896 - apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
1.897 + apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) <= O(h)")
1.898 apply assumption
1.899 apply (rule bigo_const_mult6)
1.900 - apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
1.901 + apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)")
1.902 apply (erule ssubst)
1.903 apply (erule set_times_intro2)
1.904 apply (simp add: func_times)
1.905 done
1.906
1.907 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_fix" ]]
1.908 -lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
1.909 +lemma bigo_fix: "(\<lambda>x. f ((x\<Colon>nat) + 1)) =o O(\<lambda>x. h(x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow>
1.910 f =o O(h)"
1.911 - apply (simp add: bigo_alt_def)
1.912 -(*sledgehammer*)
1.913 - apply clarify
1.914 - apply (rule_tac x = c in exI)
1.915 - apply safe
1.916 - apply (case_tac "x = 0")
1.917 -apply (metis abs_ge_zero abs_zero order_less_le split_mult_pos_le)
1.918 - apply (subgoal_tac "x = Suc (x - 1)")
1.919 - apply metis
1.920 - apply simp
1.921 - done
1.922 -
1.923 +apply (simp add: bigo_alt_def)
1.924 +by (metis abs_ge_zero abs_mult abs_of_pos abs_zero not0_implies_Suc)
1.925
1.926 lemma bigo_fix2:
1.927 - "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==>
1.928 - f 0 = g 0 ==> f =o g +o O(h)"
1.929 + "(\<lambda>x. f ((x\<Colon>nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow>
1.930 + f 0 = g 0 \<Longrightarrow> f =o g +o O(h)"
1.931 apply (rule set_minus_imp_plus)
1.932 apply (rule bigo_fix)
1.933 apply (subst fun_diff_def)
1.934 @@ -826,23 +726,23 @@
1.935
1.936 subsection {* Less than or equal to *}
1.937
1.938 -definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
1.939 - "f <o g == (%x. max (f x - g x) 0)"
1.940 +definition lesso :: "('a => 'b\<Colon>linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
1.941 + "f <o g == (\<lambda>x. max (f x - g x) 0)"
1.942
1.943 -lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
1.944 +lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= abs (f x) \<Longrightarrow>
1.945 g =o O(h)"
1.946 apply (unfold bigo_def)
1.947 apply clarsimp
1.948 apply (blast intro: order_trans)
1.949 done
1.950
1.951 -lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
1.952 +lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= f x \<Longrightarrow>
1.953 g =o O(h)"
1.954 apply (erule bigo_lesseq1)
1.955 apply (blast intro: abs_ge_self order_trans)
1.956 done
1.957
1.958 -lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
1.959 +lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= f x \<Longrightarrow>
1.960 g =o O(h)"
1.961 apply (erule bigo_lesseq2)
1.962 apply (rule allI)
1.963 @@ -850,8 +750,8 @@
1.964 apply (erule spec)+
1.965 done
1.966
1.967 -lemma bigo_lesseq4: "f =o O(h) ==>
1.968 - ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
1.969 +lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
1.970 + \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= abs (f x) \<Longrightarrow>
1.971 g =o O(h)"
1.972 apply (erule bigo_lesseq1)
1.973 apply (rule allI)
1.974 @@ -859,23 +759,15 @@
1.975 apply (erule spec)+
1.976 done
1.977
1.978 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso1" ]]
1.979 -lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
1.980 +lemma bigo_lesso1: "\<forall>x. f x <= g x \<Longrightarrow> f <o g =o O(h)"
1.981 apply (unfold lesso_def)
1.982 -apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
1.983 -proof -
1.984 - assume "(\<lambda>x. max (f x - g x) 0) = 0"
1.985 - thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero)
1.986 -next
1.987 - show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)"
1.988 - apply (unfold func_zero)
1.989 - apply (rule ext)
1.990 - by (simp split: split_max)
1.991 -qed
1.992 +apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
1.993 + apply (metis bigo_zero)
1.994 +by (metis (lam_lifting, no_types) func_zero le_fun_def le_iff_diff_le_0
1.995 + min_max.sup_absorb2 order_eq_iff)
1.996
1.997 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso2" ]]
1.998 -lemma bigo_lesso2: "f =o g +o O(h) ==>
1.999 - ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
1.1000 +lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
1.1001 + \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow>
1.1002 k <o g =o O(h)"
1.1003 apply (unfold lesso_def)
1.1004 apply (rule bigo_lesseq4)
1.1005 @@ -885,33 +777,15 @@
1.1006 apply (rule allI)
1.1007 apply (subst fun_diff_def)
1.1008 apply (erule thin_rl)
1.1009 -(*sledgehammer*)
1.1010 - apply (case_tac "0 <= k x - g x")
1.1011 -(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
1.1012 - le_max_iff_disj min_max.le_supE min_max.sup_absorb2
1.1013 - min_max.sup_commute) *)
1.1014 -proof -
1.1015 - fix x :: 'a
1.1016 - assume "\<forall>x\<Colon>'a. k x \<le> f x"
1.1017 - hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2)
1.1018 - assume "(0\<Colon>'b) \<le> k x - g x"
1.1019 - hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2)
1.1020 - have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less)
1.1021 - have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj)
1.1022 - hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE)
1.1023 - hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute)
1.1024 - hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2)
1.1025 - thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute)
1.1026 -next
1.1027 - show "\<And>x\<Colon>'a.
1.1028 - \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
1.1029 - \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
1.1030 - by (metis abs_ge_zero le_cases min_max.sup_absorb2)
1.1031 -qed
1.1032 +(* sledgehammer *)
1.1033 +apply (case_tac "0 <= k x - g x")
1.1034 + apply (metis (hide_lams, no_types) abs_le_iff add_le_imp_le_right diff_minus le_less
1.1035 + le_max_iff_disj min_max.le_supE min_max.sup_absorb2
1.1036 + min_max.sup_commute)
1.1037 +by (metis abs_ge_zero le_cases min_max.sup_absorb2)
1.1038
1.1039 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3" ]]
1.1040 -lemma bigo_lesso3: "f =o g +o O(h) ==>
1.1041 - ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
1.1042 +lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
1.1043 + \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow>
1.1044 f <o k =o O(h)"
1.1045 apply (unfold lesso_def)
1.1046 apply (rule bigo_lesseq4)
1.1047 @@ -920,20 +794,19 @@
1.1048 apply (rule le_maxI2)
1.1049 apply (rule allI)
1.1050 apply (subst fun_diff_def)
1.1051 -apply (erule thin_rl)
1.1052 -(*sledgehammer*)
1.1053 + apply (erule thin_rl)
1.1054 + (* sledgehammer *)
1.1055 apply (case_tac "0 <= f x - k x")
1.1056 - apply (simp)
1.1057 + apply simp
1.1058 apply (subst abs_of_nonneg)
1.1059 apply (drule_tac x = x in spec) back
1.1060 -using [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3_simpler" ]]
1.1061 -apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
1.1062 -apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
1.1063 + apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
1.1064 + apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
1.1065 apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
1.1066 done
1.1067
1.1068 -lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::{linordered_field,number_ring}) ==>
1.1069 - g =o h +o O(k) ==> f <o h =o O(k)"
1.1070 +lemma bigo_lesso4: "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field,number_ring}) \<Longrightarrow>
1.1071 + g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"
1.1072 apply (unfold lesso_def)
1.1073 apply (drule set_plus_imp_minus)
1.1074 apply (drule bigo_abs5) back
1.1075 @@ -946,9 +819,7 @@
1.1076 split: split_max abs_split)
1.1077 done
1.1078
1.1079 -declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso5" ]]
1.1080 -lemma bigo_lesso5: "f <o g =o O(h) ==>
1.1081 - EX C. ALL x. f x <= g x + C * abs(h x)"
1.1082 +lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * abs(h x)"
1.1083 apply (simp only: lesso_def bigo_alt_def)
1.1084 apply clarsimp
1.1085 apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)