# HG changeset patch # User blanchet # Date 1272541311 -7200 # Node ID f91c7198281110151244aa1c581ae10dd5bf4ad3 # Parent 45c1870f234fba7857397b31b0ed8c291de8f5eb redo more Metis/Sledgehammer example diff -r 45c1870f234f -r f91c71982811 src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Thu Apr 29 12:21:20 2010 +0200 +++ b/src/HOL/Metis_Examples/BigO.thy Thu Apr 29 13:41:51 2010 +0200 @@ -23,7 +23,7 @@ apply (case_tac "c = 0", simp) apply (rule_tac x = "1" in exI, simp) apply (rule_tac x = "abs c" in exI, auto) - apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult) + apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult) done (*** Now various verions with an increasing shrink factor ***) @@ -37,64 +37,25 @@ apply (case_tac "c = 0", simp) apply (rule_tac x = "1" in exI, simp) apply (rule_tac x = "abs c" in exI, auto) -proof (neg_clausify) -fix c x -have 0: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * X2\ = \X2 * X1\" - by (metis abs_mult mult_commute) -have 1: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. - X1 \ (0\'a\linordered_idom) \ \X2\ * X1 = \X2 * X1\" - by (metis abs_mult_pos linorder_linear) -have 2: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. - \ (0\'a\linordered_idom) < X1 * X2 \ - \ (0\'a\linordered_idom) \ X2 \ \ X1 \ (0\'a\linordered_idom)" - by (metis linorder_not_less mult_nonneg_nonpos2) -assume 3: "\x\'b\type. - \(h\'b\type \ 'a\linordered_idom) x\ - \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) x\" -assume 4: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ - \ \c\'a\linordered_idom\ * \(f\'b\type \ 'a\linordered_idom) x\" -have 5: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ - \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) x\" - by (metis 4 abs_mult) -have 6: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. - \ X1 \ (0\'a\linordered_idom) \ X1 \ \X2\" - by (metis abs_ge_zero xt1(6)) -have 7: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. - X1 \ \X2\ \ (0\'a\linordered_idom) < X1" - by (metis not_leE 6) -have 8: "(0\'a\linordered_idom) < \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\" - by (metis 5 7) -have 9: "\X1\'a\linordered_idom. - \ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ \ X1 \ - (0\'a\linordered_idom) < X1" - by (metis 8 order_less_le_trans) -have 10: "(0\'a\linordered_idom) -< (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) (x\'b\type)\" - by (metis 3 9) -have 11: "\ (c\'a\linordered_idom) \ (0\'a\linordered_idom)" - by (metis abs_ge_zero 2 10) -have 12: "\X1\'a\linordered_idom. (c\'a\linordered_idom) * \X1\ = \X1 * c\" - by (metis mult_commute 1 11) -have 13: "\X1\'b\type. - - (h\'b\type \ 'a\linordered_idom) X1 - \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) X1\" - by (metis 3 abs_le_D2) -have 14: "\X1\'b\type. - - (h\'b\type \ 'a\linordered_idom) X1 - \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" - by (metis 0 12 13) -have 15: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * \X2\\ = \X1 * X2\" - by (metis abs_mult abs_mult_pos abs_ge_zero) -have 16: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. X1 \ \X2\ \ \ X1 \ X2" - by (metis xt1(6) abs_ge_self) -have 17: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \ \X1\ \ X2 \ X1 \ \X2\" - by (metis 16 abs_le_D1) -have 18: "\X1\'b\type. - (h\'b\type \ 'a\linordered_idom) X1 - \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" - by (metis 17 3 15) -show "False" - by (metis abs_le_iff 5 18 14) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have F1: "\x\<^isub>1\'a\linordered_idom. 0 \ \x\<^isub>1\" by (metis abs_ge_zero) + have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F3: "\x\<^isub>1 x\<^isub>3. x\<^isub>3 \ \h x\<^isub>1\ \ x\<^isub>3 \ c * \f x\<^isub>1\" by (metis A1 order_trans) + have F4: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" + by (metis abs_mult) + have F5: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" + by (metis abs_mult_pos) + hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = \1\ * x\<^isub>1" by (metis F2) + hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F2 abs_one) + hence "\x\<^isub>3. 0 \ \h x\<^isub>3\ \ \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis F3) + hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis F1) + hence "\x\<^isub>3. (0\'a) \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F5) + hence "\x\<^isub>3. (0\'a) \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F4) + hence "\x\<^isub>3. c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F1) + hence "\h x\ \ \c * f x\" by (metis A1) + thus "\h x\ \ \c\ * \f x\" by (metis F4) qed sledgehammer_params [shrink_factor = 2] @@ -106,36 +67,17 @@ apply (case_tac "c = 0", simp) apply (rule_tac x = "1" in exI, simp) apply (rule_tac x = "abs c" in exI, auto); -proof (neg_clausify) -fix c x -have 0: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * X2\ = \X2 * X1\" - by (metis abs_mult mult_commute) -assume 1: "\x\'b\type. - \(h\'b\type \ 'a\linordered_idom) x\ - \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) x\" -assume 2: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ - \ \c\'a\linordered_idom\ * \(f\'b\type \ 'a\linordered_idom) x\" -have 3: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ - \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) x\" - by (metis 2 abs_mult) -have 4: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. - \ X1 \ (0\'a\linordered_idom) \ X1 \ \X2\" - by (metis abs_ge_zero xt1(6)) -have 5: "(0\'a\linordered_idom) < \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\" - by (metis not_leE 4 3) -have 6: "(0\'a\linordered_idom) -< (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) (x\'b\type)\" - by (metis 1 order_less_le_trans 5) -have 7: "\X1\'a\linordered_idom. (c\'a\linordered_idom) * \X1\ = \X1 * c\" - by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute) -have 8: "\X1\'b\type. - - (h\'b\type \ 'a\linordered_idom) X1 - \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" - by (metis 0 7 abs_le_D2 1) -have 9: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \ \X1\ \ X2 \ X1 \ \X2\" - by (metis abs_ge_self xt1(6) abs_le_D1) -show "False" - by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F2: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" + by (metis abs_mult) + have "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_mult_pos abs_one) + hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis A1 abs_ge_zero order_trans) + hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c * f x\<^isub>3\" by (metis F2 abs_mult_pos) + hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero) + thus "\h x\ \ \c\ * \f x\" by (metis F2) qed sledgehammer_params [shrink_factor = 3] @@ -146,30 +88,17 @@ apply auto apply (case_tac "c = 0", simp) apply (rule_tac x = "1" in exI, simp) - apply (rule_tac x = "abs c" in exI, auto); -proof (neg_clausify) -fix c x -assume 0: "\x\'b\type. - \(h\'b\type \ 'a\linordered_idom) x\ - \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) x\" -assume 1: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ - \ \c\'a\linordered_idom\ * \(f\'b\type \ 'a\linordered_idom) x\" -have 2: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. - X1 \ \X2\ \ (0\'a\linordered_idom) < X1" - by (metis abs_ge_zero xt1(6) not_leE) -have 3: "\ (c\'a\linordered_idom) \ (0\'a\linordered_idom)" - by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0) -have 4: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * \X2\\ = \X1 * X2\" - by (metis abs_ge_zero abs_mult_pos abs_mult) -have 5: "\X1\'b\type. - (h\'b\type \ 'a\linordered_idom) X1 - \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" - by (metis 4 0 xt1(6) abs_ge_self abs_le_D1) -show "False" - by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff) + apply (rule_tac x = "abs c" in exI, auto) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F2: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" by (metis abs_mult_pos) + hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_one) + hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F2 A1 abs_ge_zero order_trans) + thus "\h x\ \ \c\ * \f x\" by (metis A1 abs_mult abs_ge_zero) qed - sledgehammer_params [shrink_factor = 4] lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). @@ -178,33 +107,18 @@ apply auto apply (case_tac "c = 0", simp) apply (rule_tac x = "1" in exI, simp) - apply (rule_tac x = "abs c" in exI, auto); -proof (neg_clausify) -fix c x (*sort/type constraint inserted by hand!*) -have 0: "\(X1\'a\linordered_idom) X2. \X1 * \X2\\ = \X1 * X2\" - by (metis abs_ge_zero abs_mult_pos abs_mult) -assume 1: "\A. \h A\ \ c * \f A\" -have 2: "\X1 X2. \ \X1\ \ X2 \ (0\'a) \ X2" - by (metis abs_ge_zero order_trans) -have 3: "\X1. (0\'a) \ c * \f X1\" - by (metis 1 2) -have 4: "\X1. c * \f X1\ = \c * f X1\" - by (metis 0 abs_of_nonneg 3) -have 5: "\X1. - h X1 \ c * \f X1\" - by (metis 1 abs_le_D2) -have 6: "\X1. - h X1 \ \c * f X1\" - by (metis 4 5) -have 7: "\X1. h X1 \ c * \f X1\" - by (metis 1 abs_le_D1) -have 8: "\X1. h X1 \ \c * f X1\" - by (metis 4 7) -assume 9: "\ \h x\ \ \c\ * \f x\" -have 10: "\ \h x\ \ \c * f x\" - by (metis abs_mult 9) -show "False" - by (metis 6 8 10 abs_leI) + apply (rule_tac x = "abs c" in exI, auto) +proof - + fix c :: 'a and x :: 'b + assume A1: "\x. \h x\ \ c * \f x\" + have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" + by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) + hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) + thus "\h x\ \ \c\ * \f x\" by (metis abs_mult) qed +sledgehammer_params [shrink_factor = 1] lemma bigo_alt_def: "O(f) = {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}" @@ -230,29 +144,13 @@ declare [[ atp_problem_prefix = "BigO__bigo_refl" ]] lemma bigo_refl [intro]: "f : O(f)" - apply(auto simp add: bigo_def) -proof (neg_clausify) -fix x -assume 0: "\xa. \ \f (x xa)\ \ xa * \f (x xa)\" -have 1: "\X2. X2 \ (1\'b) * X2 \ \ (1\'b) \ (1\'b)" - by (metis mult_le_cancel_right1 order_eq_iff) -have 2: "\X2. X2 \ (1\'b) * X2" - by (metis order_eq_iff 1) -show "False" - by (metis 0 2) -qed +apply (auto simp add: bigo_def) +by (metis class_semiring.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_zero" ]] lemma bigo_zero: "0 : O(g)" - apply (auto simp add: bigo_def func_zero) -proof (neg_clausify) -fix x -assume 0: "\xa. \ (0\'b) \ xa * \g (x xa)\" -have 1: "\ (0\'b) \ (0\'b)" - by (metis 0 mult_eq_0_iff) -show "False" - by (metis 1 linorder_neq_iff linorder_antisym_conv1) -qed +apply (auto simp add: bigo_def func_zero) +by (metis class_semiring.mul_0 order_refl) lemma bigo_zero2: "O(%x.0) = {%x.0}" apply (auto simp add: bigo_def) @@ -365,103 +263,36 @@ lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" apply (auto simp add: bigo_def) -(*Version 1: one-shot proof*) +(* Version 1: one-line proof *) apply (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult) done lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> - f : O(g)" - apply (auto simp add: bigo_def) -(*Version 2: single-step proof*) -proof (neg_clausify) -fix x -assume 0: "\x. f x \ c * g x" -assume 1: "\xa. \ f (x xa) \ xa * \g (x xa)\" -have 2: "\X3. c * g X3 = f X3 \ \ c * g X3 \ f X3" - by (metis 0 order_antisym_conv) -have 3: "\X3. \ f (x \X3\) \ \X3 * g (x \X3\)\" - by (metis 1 abs_mult) -have 4: "\X1 X3\'b\linordered_idom. X3 \ X1 \ X1 \ \X3\" - by (metis linorder_linear abs_le_D1) -have 5: "\X3::'b. \X3\ * \X3\ = X3 * X3" - by (metis abs_mult_self) -have 6: "\X3. \ X3 * X3 < (0\'b\linordered_idom)" - by (metis not_square_less_zero) -have 7: "\X1 X3::'b. \X1\ * \X3\ = \X3 * X1\" - by (metis abs_mult mult_commute) -have 8: "\X3::'b. X3 * X3 = \X3 * X3\" - by (metis abs_mult 5) -have 9: "\X3. X3 * g (x \X3\) \ f (x \X3\)" - by (metis 3 4) -have 10: "c * g (x \c\) = f (x \c\)" - by (metis 2 9) -have 11: "\X3::'b. \X3\ * \\X3\\ = \X3\ * \X3\" - by (metis abs_idempotent abs_mult 8) -have 12: "\X3::'b. \X3 * \X3\\ = \X3\ * \X3\" - by (metis mult_commute 7 11) -have 13: "\X3::'b. \X3 * \X3\\ = X3 * X3" - by (metis 8 7 12) -have 14: "\X3. X3 \ \X3\ \ X3 < (0\'b)" - by (metis abs_ge_self abs_le_D1 abs_if) -have 15: "\X3. X3 \ \X3\ \ \X3\ < (0\'b)" - by (metis abs_ge_self abs_le_D1 abs_if) -have 16: "\X3. X3 * X3 < (0\'b) \ X3 * \X3\ \ X3 * X3" - by (metis 15 13) -have 17: "\X3::'b. X3 * \X3\ \ X3 * X3" - by (metis 16 6) -have 18: "\X3. X3 \ \X3\ \ \ X3 < (0\'b)" - by (metis mult_le_cancel_left 17) -have 19: "\X3::'b. X3 \ \X3\" - by (metis 18 14) -have 20: "\ f (x \c\) \ \f (x \c\)\" - by (metis 3 10) -show "False" - by (metis 20 19) + f : O(g)" +apply (auto simp add: bigo_def) +(* Version 2: structured proof *) +proof - + assume "\x. f x \ c * g x" + thus "\c. \x. f x \ c * \g x\" by (metis abs_mult abs_ge_self order_trans) qed +text{*So here is the easier (and more natural) problem using transitivity*} +declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] +lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" +apply (auto simp add: bigo_def) +(* Version 1: one-line proof *) +by (metis abs_ge_self abs_mult order_trans) text{*So here is the easier (and more natural) problem using transitivity*} declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" apply (auto simp add: bigo_def) - (*Version 1: one-shot proof*) - apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less) - done - -text{*So here is the easier (and more natural) problem using transitivity*} -declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] -lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" - apply (auto simp add: bigo_def) -(*Version 2: single-step proof*) -proof (neg_clausify) -fix x -assume 0: "\A\'a\type. - (f\'a\type \ 'b\linordered_idom) A - \ (c\'b\linordered_idom) * (g\'a\type \ 'b\linordered_idom) A" -assume 1: "\A\'b\linordered_idom. - \ (f\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) A) - \ A * \(g\'a\type \ 'b\linordered_idom) (x A)\" -have 2: "\X2\'a\type. - \ (c\'b\linordered_idom) * (g\'a\type \ 'b\linordered_idom) X2 - < (f\'a\type \ 'b\linordered_idom) X2" - by (metis 0 linorder_not_le) -have 3: "\X2\'b\linordered_idom. - \ (f\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) \X2\) - \ \X2 * (g\'a\type \ 'b\linordered_idom) (x \X2\)\" - by (metis abs_mult 1) -have 4: "\X2\'b\linordered_idom. - \X2 * (g\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) \X2\)\ - < (f\'a\type \ 'b\linordered_idom) (x \X2\)" - by (metis 3 linorder_not_less) -have 5: "\X2\'b\linordered_idom. - X2 * (g\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) \X2\) - < (f\'a\type \ 'b\linordered_idom) (x \X2\)" - by (metis abs_less_iff 4) -show "False" - by (metis 2 5) +(* Version 2: structured proof *) +proof - + assume "\x. f x \ c * g x" + thus "\c. \x. f x \ c * \g x\" by (metis abs_mult abs_ge_self order_trans) qed - lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> f : O(g)" apply (erule bigo_bounded_alt [of f 1 g]) @@ -471,63 +302,37 @@ declare [[ atp_problem_prefix = "BigO__bigo_bounded2" ]] lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==> f : lb +o O(g)" - apply (rule set_minus_imp_plus) - apply (rule bigo_bounded) - apply (auto simp add: diff_minus fun_Compl_def func_plus) - prefer 2 - apply (drule_tac x = x in spec)+ - apply arith (*not clear that it's provable otherwise*) -proof (neg_clausify) -fix x -assume 0: "\y. lb y \ f y" -assume 1: "\ (0\'b) \ f x + - lb x" -have 2: "\X3. (0\'b) + X3 = X3" - by (metis diff_eq_eq right_minus_eq) -have 3: "\ (0\'b) \ f x - lb x" - by (metis 1 diff_minus) -have 4: "\ (0\'b) + lb x \ f x" - by (metis 3 le_diff_eq) -show "False" - by (metis 4 2 0) +apply (rule set_minus_imp_plus) +apply (rule bigo_bounded) + apply (auto simp add: diff_minus fun_Compl_def func_plus) + prefer 2 + apply (drule_tac x = x in spec)+ + apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) +proof - + fix x :: 'a + assume "\x. lb x \ f x" + thus "(0\'b) \ f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le) qed declare [[ atp_problem_prefix = "BigO__bigo_abs" ]] lemma bigo_abs: "(%x. abs(f x)) =o O(f)" - apply (unfold bigo_def) - apply auto -proof (neg_clausify) -fix x -assume 0: "\xa. \ \f (x xa)\ \ xa * \f (x xa)\" -have 1: "\X2. X2 \ (1\'b) * X2 \ \ (1\'b) \ (1\'b)" - by (metis mult_le_cancel_right1 order_eq_iff) -have 2: "\X2. X2 \ (1\'b) * X2" - by (metis order_eq_iff 1) -show "False" - by (metis 0 2) -qed +apply (unfold bigo_def) +apply auto +by (metis class_semiring.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]] lemma bigo_abs2: "f =o O(%x. abs(f x))" - apply (unfold bigo_def) - apply auto -proof (neg_clausify) -fix x -assume 0: "\xa. \ \f (x xa)\ \ xa * \f (x xa)\" -have 1: "\X2. X2 \ (1\'b) * X2 \ \ (1\'b) \ (1\'b)" - by (metis mult_le_cancel_right1 order_eq_iff) -have 2: "\X2. X2 \ (1\'b) * X2" - by (metis order_eq_iff 1) -show "False" - by (metis 0 2) -qed +apply (unfold bigo_def) +apply auto +by (metis class_semiring.mul_1 order_refl) lemma bigo_abs3: "O(f) = O(%x. abs(f x))" - apply (rule equalityI) - apply (rule bigo_elt_subset) - apply (rule bigo_abs2) - apply (rule bigo_elt_subset) - apply (rule bigo_abs) -done +proof - + have F1: "\v u. u \ O(v) \ O(u) \ O(v)" by (metis bigo_elt_subset) + have F2: "\u. (\R. \u R\) \ O(u)" by (metis bigo_abs) + have "\u. u \ O(\R. \u R\)" by (metis bigo_abs2) + thus "O(f) = O(\x. \f x\)" using F1 F2 by auto +qed lemma bigo_abs4: "f =o g +o O(h) ==> (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)" @@ -597,63 +402,9 @@ abs_mult mult_pos_pos) apply (erule ssubst) apply (subst abs_mult) -(*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has - just been done*) -proof (neg_clausify) -fix a c b ca x -assume 0: "(0\'b\linordered_idom) < (c\'b\linordered_idom)" -assume 1: "\(a\'a \ 'b\linordered_idom) (x\'a)\ -\ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" -assume 2: "\(b\'a \ 'b\linordered_idom) (x\'a)\ -\ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\" -assume 3: "\ \(a\'a \ 'b\linordered_idom) (x\'a)\ * - \(b\'a \ 'b\linordered_idom) x\ - \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\ * - ((ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\)" -have 4: "\c\'b\linordered_idom\ = c" - by (metis abs_of_pos 0) -have 5: "\X1\'b\linordered_idom. (c\'b\linordered_idom) * \X1\ = \c * X1\" - by (metis abs_mult 4) -have 6: "(0\'b\linordered_idom) = (1\'b\linordered_idom) \ -(0\'b\linordered_idom) < (1\'b\linordered_idom)" - by (metis abs_not_less_zero abs_one linorder_neqE_linordered_idom) -have 7: "(0\'b\linordered_idom) < (1\'b\linordered_idom)" - by (metis 6 one_neq_zero) -have 8: "\1\'b\linordered_idom\ = (1\'b\linordered_idom)" - by (metis abs_of_pos 7) -have 9: "\X1\'b\linordered_idom. (0\'b\linordered_idom) \ (c\'b\linordered_idom) * \X1\" - by (metis abs_ge_zero 5) -have 10: "\X1\'b\linordered_idom. X1 * (1\'b\linordered_idom) = X1" - by (metis mult_cancel_right2 mult_commute) -have 11: "\X1\'b\linordered_idom. \\X1\\ = \X1\ * \1\'b\linordered_idom\" - by (metis abs_mult abs_idempotent 10) -have 12: "\X1\'b\linordered_idom. \\X1\\ = \X1\" - by (metis 11 8 10) -have 13: "\X1\'b\linordered_idom. (0\'b\linordered_idom) \ \X1\" - by (metis abs_ge_zero 12) -have 14: "\ (0\'b\linordered_idom) - \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) (x\'a)\ \ -\ (0\'b\linordered_idom) \ \(b\'a \ 'b\linordered_idom) x\ \ -\ \b x\ \ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\ \ -\ \(a\'a \ 'b\linordered_idom) x\ \ c * \f x\" - by (metis 3 mult_mono) -have 15: "\ (0\'b\linordered_idom) \ \(b\'a \ 'b\linordered_idom) (x\'a)\ \ -\ \b x\ \ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\ \ -\ \(a\'a \ 'b\linordered_idom) x\ - \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" - by (metis 14 9) -have 16: "\ \(b\'a \ 'b\linordered_idom) (x\'a)\ - \ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\ \ -\ \(a\'a \ 'b\linordered_idom) x\ - \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" - by (metis 15 13) -have 17: "\ \(a\'a \ 'b\linordered_idom) (x\'a)\ - \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" - by (metis 16 2) -show 18: "False" - by (metis 17 1) -qed - +(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since + abs_mult has just been done *) +by (metis abs_ge_zero mult_mono') declare [[ atp_problem_prefix = "BigO__bigo_mult2" ]] lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)" @@ -672,7 +423,7 @@ declare [[ atp_problem_prefix = "BigO__bigo_mult3" ]] lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)" -by (metis bigo_mult set_times_intro subset_iff) +by (metis bigo_mult set_rev_mp set_times_intro) declare [[ atp_problem_prefix = "BigO__bigo_mult4" ]] lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)" @@ -809,40 +560,16 @@ by (metis bigo_const1 bigo_elt_subset); lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)"; -(*??FAILS because the two occurrences of COMBK have different polymorphic types -proof (neg_clausify) -assume 0: "\ O(COMBK (c\'b\linordered_idom)) \ O(COMBK (1\'b\linordered_idom))" -have 1: "COMBK (c\'b\linordered_idom) \ O(COMBK (1\'b\linordered_idom))" -apply (rule notI) -apply (rule 0 [THEN notE]) -apply (rule bigo_elt_subset) -apply assumption; -sorry - by (metis 0 bigo_elt_subset) loops?? -show "False" - by (metis 1 bigo_const1) +(* "thus" had to be replaced by "show" with an explicit reference to "F1" *) +proof - + have F1: "\u. (\Q. u) \ O(\Q. 1)" by (metis bigo_const1) + show "O(\x. c) \ O(\x. 1)" by (metis F1 bigo_elt_subset) qed -*) - apply (rule bigo_elt_subset) - apply (rule bigo_const1) -done declare [[ atp_problem_prefix = "BigO__bigo_const3" ]] lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" apply (simp add: bigo_def) -proof (neg_clausify) -assume 0: "(c\'a\linordered_field) \ (0\'a\linordered_field)" -assume 1: "\A\'a\linordered_field. \ (1\'a\linordered_field) \ A * \c\'a\linordered_field\" -have 2: "(0\'a\linordered_field) = \c\'a\linordered_field\ \ -\ (1\'a\linordered_field) \ (1\'a\linordered_field)" - by (metis 1 field_inverse) -have 3: "\c\'a\linordered_field\ = (0\'a\linordered_field)" - by (metis linorder_neq_iff linorder_antisym_conv1 2) -have 4: "(0\'a\linordered_field) = (c\'a\linordered_field)" - by (metis 3 abs_eq_0) -show "False" - by (metis 0 4) -qed +by (metis abs_eq_0 left_inverse order_refl) lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" by (rule bigo_elt_subset, rule bigo_const3, assumption) @@ -854,15 +581,7 @@ declare [[ atp_problem_prefix = "BigO__bigo_const_mult1" ]] lemma bigo_const_mult1: "(%x. c * f x) : O(f)" apply (simp add: bigo_def abs_mult) -proof (neg_clausify) -fix x -assume 0: "\xa\'b\linordered_idom. - \ \c\'b\linordered_idom\ * - \(f\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) xa)\ - \ xa * \f (x xa)\" -show "False" - by (metis linorder_neq_iff linorder_antisym_conv1 0) -qed +by (metis le_less) lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)" by (rule bigo_elt_subset, rule bigo_const_mult1) @@ -870,7 +589,7 @@ declare [[ atp_problem_prefix = "BigO__bigo_const_mult3" ]] lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)" apply (simp add: bigo_def) -(*sledgehammer [no luck]*); +(*sledgehammer [no luck]*) apply (rule_tac x = "abs(inverse c)" in exI) apply (simp only: abs_mult [symmetric] mult_assoc [symmetric]) apply (subst left_inverse) @@ -1132,15 +851,17 @@ declare [[ atp_problem_prefix = "BigO__bigo_lesso1" ]] lemma bigo_lesso1: "ALL x. f x <= g x ==> f x. max (f x - g x) 0) = 0" + thus "(\x. max (f x - g x) 0) \ O(h)" by (metis bigo_zero) +next + show "\x\'a. f x \ g x \ (\x\'a. max (f x - g x) (0\'b)) = (0\'a \ 'b)" apply (unfold func_zero) apply (rule ext) - apply (simp split: split_max) -done - + by (simp split: split_max) +qed declare [[ atp_problem_prefix = "BigO__bigo_lesso2" ]] lemma bigo_lesso2: "f =o g +o O(h) ==> @@ -1156,8 +877,9 @@ apply (erule thin_rl) (*sledgehammer*); apply (case_tac "0 <= k x - g x") - prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*) - apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.sup_absorb1 min_max.sup_commute) +(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less + le_max_iff_disj min_max.le_supE min_max.sup_absorb2 + min_max.sup_commute) *) proof (neg_clausify) fix x assume 0: "\A. k A \ f A" @@ -1177,6 +899,11 @@ by (metis 5 abs_minus_commute 7 min_max.sup_commute 6) show "False" by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8) +next + show "\x\'a. + \\x\'a. (0\'b) \ k x; \x\'a. k x \ f x; \ (0\'b) \ k x - g x\ + \ max (k x - g x) (0\'b) \ \f x - g x\" + by (metis abs_ge_zero le_cases min_max.sup_absorb2) qed declare [[ atp_problem_prefix = "BigO__bigo_lesso3" ]]