# HG changeset patch # User blanchet # Date 1275482415 -7200 # Node ID 06c7a2f231fec44481a97eb90649b6e79110b996 # Parent 42268dc7d6c47f4dabbdb5fb438e92ef72ea7f05 kill another neg_clausify proof diff -r 42268dc7d6c4 -r 06c7a2f231fe src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Wed Jun 02 14:35:52 2010 +0200 +++ b/src/HOL/Metis_Examples/BigO.thy Wed Jun 02 14:40:15 2010 +0200 @@ -880,25 +880,18 @@ (* 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" -have 1: "\(X1\'b\linordered_idom) X2. \ max X1 X2 < X1" - by (metis linorder_not_less le_maxI1) (*sort inserted by hand*) -assume 2: "(0\'b) \ k x - g x" -have 3: "\ k x - g x < (0\'b)" - by (metis 2 linorder_not_less) -have 4: "\X1 X2. min X1 (k X2) \ f X2" - by (metis min_max.inf_le2 min_max.le_inf_iff min_max.le_iff_inf 0) -have 5: "\g x - f x\ = f x - g x" - by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.inf_commute 4 linorder_not_le min_max.le_iff_inf 3 diff_less_0_iff_less linorder_not_less) -have 6: "max (0\'b) (k x - g x) = k x - g x" - by (metis min_max.le_iff_sup 2) -assume 7: "\ max (k x - g x) (0\'b) \ \f x - g x\" -have 8: "\ k x - g x \ f x - g x" - 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) +proof - + fix x :: 'a + assume "\x\'a. k x \ f x" + hence F1: "\x\<^isub>1\'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2) + assume "(0\'b) \ k x - g x" + hence F2: "max (0\'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2) + have F3: "\x\<^isub>1\'b. x\<^isub>1 \ \x\<^isub>1\" by (metis abs_le_iff le_less) + have "\(x\<^isub>2\'b) x\<^isub>1\'b. max x\<^isub>1 x\<^isub>2 \ x\<^isub>2 \ max x\<^isub>1 x\<^isub>2 \ x\<^isub>1" by (metis le_less le_max_iff_disj) + hence "\(x\<^isub>3\'b) (x\<^isub>2\'b) x\<^isub>1\'b. x\<^isub>1 - x\<^isub>2 \ x\<^isub>3 - x\<^isub>2 \ x\<^isub>3 \ x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE) + hence "k x - g x \ f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute) + hence "k x - g x \ \f x - g x\" by (metis F3 le_max_iff_disj min_max.sup_absorb2) + thus "max (k x - g x) (0\'b) \ \f x - g x\" by (metis F2 min_max.sup_commute) next show "\x\'a. \\x\'a. (0\'b) \ k x; \x\'a. k x \ f x; \ (0\'b) \ k x - g x\