# HG changeset patch # User blanchet # Date 1275658982 -7200 # Node ID f1734f3e91050fe9cb89c192b7e5fa89c0d10160 # Parent 664d3110beb2da56e8ca6b34f03f56e738bd6436# Parent a1807bf72f760299da70bd8d6ff6368bf089b6a4 merged diff -r 664d3110beb2 -r f1734f3e9105 src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Fri Jun 04 11:31:33 2010 +0200 +++ b/src/HOL/Metis_Examples/BigO.thy Fri Jun 04 15:43:02 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\ diff -r 664d3110beb2 -r f1734f3e9105 src/HOL/Metis_Examples/set.thy --- a/src/HOL/Metis_Examples/set.thy Fri Jun 04 11:31:33 2010 +0200 +++ b/src/HOL/Metis_Examples/set.thy Fri Jun 04 15:43:02 2010 +0200 @@ -21,242 +21,164 @@ (*multiple versions of this example*) lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof (neg_clausify) -fix x -assume 0: "Y \ X \ X = Y \ Z" -assume 1: "Z \ X \ X = Y \ Z" -assume 2: "(\ Y \ X \ \ Z \ X \ Y \ x) \ X \ Y \ Z" -assume 3: "(\ Y \ X \ \ Z \ X \ Z \ x) \ X \ Y \ Z" -assume 4: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" -assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" -have 6: "sup Y Z = X \ Y \ X" - by (metis 0) -have 7: "sup Y Z = X \ Z \ X" - by (metis 1) -have 8: "\X3. sup Y Z = X \ X \ X3 \ \ Y \ X3 \ \ Z \ X3" - by (metis 5) -have 9: "Y \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 2) -have 10: "Z \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 3) -have 11: "sup Y Z \ X \ \ X \ x \ \ Y \ X \ \ Z \ X" - by (metis 4) -have 12: "Z \ X" - by (metis Un_upper2 7) -have 13: "\X3. sup Y Z = X \ X \ sup X3 Z \ \ Y \ sup X3 Z" - by (metis 8 Un_upper2) -have 14: "Y \ X" - by (metis Un_upper1 6) -have 15: "Z \ x \ sup Y Z \ X \ \ Y \ X" - by (metis 10 12) -have 16: "Y \ x \ sup Y Z \ X \ \ Y \ X" - by (metis 9 12) -have 17: "sup Y Z \ X \ \ X \ x \ \ Y \ X" - by (metis 11 12) -have 18: "sup Y Z \ X \ \ X \ x" - by (metis 17 14) -have 19: "Z \ x \ sup Y Z \ X" - by (metis 15 14) -have 20: "Y \ x \ sup Y Z \ X" - by (metis 16 14) -have 21: "sup Y Z = X \ X \ sup Y Z" - by (metis 13 Un_upper1) -have 22: "sup Y Z = X \ \ sup Y Z \ X" - by (metis equalityI 21) -have 23: "sup Y Z = X \ \ Z \ X \ \ Y \ X" - by (metis 22 Un_least) -have 24: "sup Y Z = X \ \ Y \ X" - by (metis 23 12) -have 25: "sup Y Z = X" - by (metis 24 14) -have 26: "\X3. X \ X3 \ \ Z \ X3 \ \ Y \ X3" - by (metis Un_least 25) -have 27: "Y \ x" - by (metis 20 25) -have 28: "Z \ x" - by (metis 19 25) -have 29: "\ X \ x" - by (metis 18 25) -have 30: "X \ x \ \ Y \ x" - by (metis 26 28) -have 31: "X \ x" - by (metis 30 27) -show "False" - by (metis 31 29) +proof - + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>1 \ x\<^isub>2" by (metis Un_commute Un_upper2) + have F2a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) + have F2: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq) + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume AA1: "Y \ Z \ X" + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + moreover + { assume AAA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) + hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1) } + moreover + { assume "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + moreover + { assume AAA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) + hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by blast } + moreover + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis qed sledgehammer_params [isar_proof, isar_shrink_factor = 2] lemma (*equal_union: *) - "(X = Y \ Z) = - (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof (neg_clausify) -fix x -assume 0: "Y \ X \ X = Y \ Z" -assume 1: "Z \ X \ X = Y \ Z" -assume 2: "(\ Y \ X \ \ Z \ X \ Y \ x) \ X \ Y \ Z" -assume 3: "(\ Y \ X \ \ Z \ X \ Z \ x) \ X \ Y \ Z" -assume 4: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" -assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" -have 6: "sup Y Z = X \ Y \ X" - by (metis 0) -have 7: "Y \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 2) -have 8: "sup Y Z \ X \ \ X \ x \ \ Y \ X \ \ Z \ X" - by (metis 4) -have 9: "\X3. sup Y Z = X \ X \ sup X3 Z \ \ Y \ sup X3 Z" - by (metis 5 Un_upper2) -have 10: "Z \ x \ sup Y Z \ X \ \ Y \ X" - by (metis 3 Un_upper2) -have 11: "sup Y Z \ X \ \ X \ x \ \ Y \ X" - by (metis 8 Un_upper2) -have 12: "Z \ x \ sup Y Z \ X" - by (metis 10 Un_upper1) -have 13: "sup Y Z = X \ X \ sup Y Z" - by (metis 9 Un_upper1) -have 14: "sup Y Z = X \ \ Z \ X \ \ Y \ X" - by (metis equalityI 13 Un_least) -have 15: "sup Y Z = X" - by (metis 14 1 6) -have 16: "Y \ x" - by (metis 7 Un_upper2 Un_upper1 15) -have 17: "\ X \ x" - by (metis 11 Un_upper1 15) -have 18: "X \ x" - by (metis Un_least 15 12 15 16) -show "False" - by (metis 18 17) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +proof - + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) + { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume AAA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "Y \ Z \ X \ X \ Y \ Z" + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1 Un_subset_iff) } + moreover + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } + moreover + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + moreover + { assume AA1: "Y \ X \ Y \ Z \ X" + { assume "\ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + moreover + { assume "Y \ Z \ X \ X \ Y \ Z" + hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis qed sledgehammer_params [isar_proof, isar_shrink_factor = 3] lemma (*equal_union: *) - "(X = Y \ Z) = - (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof (neg_clausify) -fix x -assume 0: "Y \ X \ X = Y \ Z" -assume 1: "Z \ X \ X = Y \ Z" -assume 2: "(\ Y \ X \ \ Z \ X \ Y \ x) \ X \ Y \ Z" -assume 3: "(\ Y \ X \ \ Z \ X \ Z \ x) \ X \ Y \ Z" -assume 4: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" -assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" -have 6: "Z \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 3) -have 7: "\X3. sup Y Z = X \ X \ sup X3 Z \ \ Y \ sup X3 Z" - by (metis 5 Un_upper2) -have 8: "Y \ x \ sup Y Z \ X \ \ Y \ X" - by (metis 2 Un_upper2) -have 9: "Z \ x \ sup Y Z \ X" - by (metis 6 Un_upper2 Un_upper1) -have 10: "sup Y Z = X \ \ sup Y Z \ X" - by (metis equalityI 7 Un_upper1) -have 11: "sup Y Z = X" - by (metis 10 Un_least 1 0) -have 12: "Z \ x" - by (metis 9 11) -have 13: "X \ x" - by (metis Un_least 11 12 8 Un_upper1 11) -show "False" - by (metis 13 4 Un_upper2 Un_upper1 11) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +proof - + have F1a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq) + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } + moreover + { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) qed -(*Example included in TPHOLs paper*) - sledgehammer_params [isar_proof, isar_shrink_factor = 4] lemma (*equal_union: *) - "(X = Y \ Z) = - (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -proof (neg_clausify) -fix x -assume 0: "Y \ X \ X = Y \ Z" -assume 1: "Z \ X \ X = Y \ Z" -assume 2: "(\ Y \ X \ \ Z \ X \ Y \ x) \ X \ Y \ Z" -assume 3: "(\ Y \ X \ \ Z \ X \ Z \ x) \ X \ Y \ Z" -assume 4: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" -assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" -have 6: "sup Y Z \ X \ \ X \ x \ \ Y \ X \ \ Z \ X" - by (metis 4) -have 7: "Z \ x \ sup Y Z \ X \ \ Y \ X" - by (metis 3 Un_upper2) -have 8: "Z \ x \ sup Y Z \ X" - by (metis 7 Un_upper1) -have 9: "sup Y Z = X \ \ Z \ X \ \ Y \ X" - by (metis equalityI 5 Un_upper2 Un_upper1 Un_least) -have 10: "Y \ x" - by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0) -have 11: "X \ x" - by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10) -show "False" - by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0) -qed + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" +proof - + have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) + { assume "\ Y \ X" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + moreover + { assume AA1: "Y \ X \ Y \ Z \ X" + { assume "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_subset_iff Un_upper2) +qed -declare [[ atp_problem_prefix = "set__equal_union" ]] +sledgehammer_params [isar_proof, isar_shrink_factor = 1] + lemma (*equal_union: *) - "(X = Y \ Z) = - (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" -(*One shot proof: hand-reduced. Metis can't do the full proof any more.*) + "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) +lemma "(X = Y \ Z) = (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))" +by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym) -declare [[ atp_problem_prefix = "set__equal_inter" ]] -lemma "(X = Y \ Z) = - (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))" -by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset) - -declare [[ atp_problem_prefix = "set__fixedpoint" ]] -lemma fixedpoint: - "\!x. f (g x) = x \ \!y. g (f y) = y" +lemma fixedpoint: "\!x. f (g x) = x \ \!y. g (f y) = y" by metis -lemma (*fixedpoint:*) - "\!x. f (g x) = x \ \!y. g (f y) = y" -proof (neg_clausify) -fix x xa -assume 0: "f (g x) = x" -assume 1: "\y. y = x \ f (g y) \ y" -assume 2: "\x. g (f (xa x)) = xa x \ g (f x) \ x" -assume 3: "\x. g (f x) \ x \ xa x \ x" -have 4: "\X1. g (f X1) \ X1 \ g x \ X1" - by (metis 3 1 2) -show "False" - by (metis 4 0) +lemma (* fixedpoint: *) "\!x. f (g x) = x \ \!y. g (f y) = y" +proof - + assume "\!x\'a. f (g x) = x" + thus "\!y\'b. g (f y) = y" by metis qed -declare [[ atp_problem_prefix = "set__singleton_example" ]] -lemma (*singleton_example_2:*) +lemma (* singleton_example_2: *) "\x \ S. \S \ x \ \z. S \ {z}" by (metis Set.subsetI Union_upper insertCI set_eq_subset) - --{*found by SPASS*} -lemma (*singleton_example_2:*) +lemma (* singleton_example_2: *) "\x \ S. \S \ x \ \z. S \ {z}" by (metis Set.subsetI Union_upper insert_iff set_eq_subset) lemma singleton_example_2: "\x \ S. \S \ x \ \z. S \ {z}" -proof (neg_clausify) -assume 0: "\x. \ S \ {x}" -assume 1: "\x. x \ S \ \S \ x" -have 2: "\X3. X3 = \S \ \ X3 \ \S \ X3 \ S" - by (metis set_eq_subset 1) -have 3: "\X3. S \ insert (\S) X3" - by (metis insert_iff Set.subsetI Union_upper 2 Set.subsetI) -show "False" - by (metis 3 0) +proof - + assume "\x \ S. \S \ x" + hence "\x\<^isub>1. x\<^isub>1 \ \S \ x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis set_eq_subset) + hence "\x\<^isub>1. x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis Union_upper) + hence "\x\<^isub>1\('a \ bool) \ bool. \S \ x\<^isub>1 \ S \ x\<^isub>1" by (metis subsetI) + hence "\x\<^isub>1\('a \ bool) \ bool. S \ insert (\S) x\<^isub>1" by (metis insert_iff) + thus "\z. S \ {z}" by metis qed - - text {* From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages 293-314. *} -declare [[ atp_problem_prefix = "set__Bledsoe_Fung" ]] -(*Notes: 1, the numbering doesn't completely agree with the paper. -2, we must rename set variables to avoid type clashes.*) +(* Notes: (1) The numbering doesn't completely agree with the paper. + (2) We must rename set variables to avoid type clashes. *) lemma "\B. (\x \ B. x \ (0::int))" "D \ F \ \G. \A \ G. \B \ F. A \ B" "P a \ \A. (\x \ A. P x) \ (\y. y \ A)" @@ -265,13 +187,13 @@ "P (f b) \ \s A. (\x \ A. P x) \ f s \ A" "\A. a \ A" "(\C. (0, 0) \ C \ (\x y. (x, y) \ C \ (Suc x, Suc y) \ C) \ (n, m) \ C) \ Q n \ Q m" -apply (metis all_not_in_conv)+ -apply (metis mem_def) -apply (metis insertCI singletonE zless_le) -apply (metis Collect_def Collect_mem_eq) -apply (metis Collect_def Collect_mem_eq) -apply (metis DiffE) -apply (metis pair_in_Id_conv) -done + apply (metis all_not_in_conv) + apply (metis all_not_in_conv) + apply (metis mem_def) + apply (metis less_int_def singleton_iff) + apply (metis mem_def) + apply (metis mem_def) + apply (metis all_not_in_conv) +by (metis pair_in_Id_conv) end diff -r 664d3110beb2 -r f1734f3e9105 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 04 11:31:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 04 15:43:02 2010 +0200 @@ -409,9 +409,10 @@ (substs' |> map (fn (x, y) => Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ Syntax.string_of_term ctxt (term_of y))))); - in cterm_instantiate substs' i_th - handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg) - end; + in cterm_instantiate substs' i_th end + handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg) + | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^ + "\n(Perhaps you want to try \"metisFT\".)") (* INFERENCE RULE: RESOLVE *) diff -r 664d3110beb2 -r f1734f3e9105 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 04 11:31:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 04 15:43:02 2010 +0200 @@ -28,8 +28,11 @@ val neg_clausify_setup = Method.setup @{binding neg_clausify} - (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)) - "conversion of goal to negated conjecture clauses" + (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac) + o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \ + \rerun Sledgehammer to obtain a direct \ + \proof")) + "conversion of goal to negated conjecture clauses (legacy)" (** Attribute for converting a theorem into clauses **) @@ -41,7 +44,9 @@ end)) val clausify_setup = - Attrib.setup @{binding clausify} parse_clausify_attribute + Attrib.setup @{binding clausify} + (parse_clausify_attribute + o tap (fn _ => legacy_feature "Old 'clausify' attribute")) "conversion of theorem to clauses" (** Sledgehammer commands **) @@ -226,7 +231,7 @@ let val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) - val _ = kill_atps () (* race w.r.t. other Sledgehammer invocations *) + val _ = kill_atps () val _ = priority "Sledgehammering..." val _ = app (start_prover_thread params birth_time death_time i n relevance_override minimize_command @@ -249,8 +254,10 @@ in case subgoal_count state of 0 => priority "No subgoal!" - | n => priority (#2 (minimize_theorems (get_params thy override_params) i n - state name_thms_pairs)) + | n => + (kill_atps (); + priority (#2 (minimize_theorems (get_params thy override_params) i n + state name_thms_pairs))) end val sledgehammerN = "sledgehammer" diff -r 664d3110beb2 -r f1734f3e9105 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 04 11:31:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 04 15:43:02 2010 +0200 @@ -487,8 +487,8 @@ fun decode_lines ctxt full_types tfrees lines = fst (fold_map (decode_line full_types tfrees) lines ctxt) -fun aint_inference _ (Definition _) = true - | aint_inference t (Inference (_, t', _)) = not (t aconv t') +fun aint_actual_inference _ (Definition _) = true + | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t') (* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) @@ -510,7 +510,7 @@ if is_only_type_information t then map (replace_deps_in_line (num, [])) lines (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (aint_inference t) lines of + else case take_prefix (aint_actual_inference t) lines of (_, []) => lines (*no repetition of proof line*) | (pre, Inference (num', _, _) :: post) => pre @ map (replace_deps_in_line (num', [num])) post @@ -523,7 +523,7 @@ if is_only_type_information t then Inference (num, t, deps) :: lines (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (aint_inference t) lines of + else case take_prefix (aint_actual_inference t) lines of (* FIXME: Doesn't this code risk conflating proofs involving different types?? *) (_, []) => Inference (num, t, deps) :: lines @@ -539,8 +539,8 @@ and delete_dep num lines = fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) [] -(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly, - removing the offending lines often does the trick. *) +(* ATPs sometimes reuse free variable names in the strangest ways. Removing + offending lines often does the trick. *) fun is_bad_free frees (Free x) = not (member (op =) frees x) | is_bad_free _ _ = false @@ -549,8 +549,8 @@ $ t1 $ t2)) = (t1 aconv t2) | is_trivial_formula t = false -fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) = - (j, line :: lines) +fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) = + (j, line :: map (replace_deps_in_line (num, [])) lines) | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees (Inference (num, t, deps)) (j, lines) = (j + 1, @@ -639,6 +639,9 @@ fun smart_case_split [] facts = ByMetis facts | smart_case_split proofs facts = CaseSplit (proofs, facts) +val indent_size = 2 +val no_label = ("", ~1) + val raw_prefix = "X" val assum_prefix = "A" val fact_prefix = "F" @@ -677,16 +680,12 @@ map2 (step_for_line thm_names) (length lines downto 1) lines end -val indent_size = 2 -val no_label = ("", ~1) - -fun no_show qs = not (member (op =) qs Show) - (* When redirecting proofs, we keep information about the labels seen so far in the "backpatches" data structure. The first component indicates which facts should be associated with forthcoming proof steps. The second component is a - pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and - "drop_ls" are those that should be dropped in a case split. *) + pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should + become assumptions and "drop_ls" are the labels that should be dropped in a + case split. *) type backpatches = (label * facts) list * (label list * label list) fun used_labels_of_step (Have (_, _, _, by)) = @@ -731,8 +730,15 @@ fun redirect_proof thy conjecture_shape hyp_ts concl_t proof = let + (* The first pass outputs those steps that are independent of the negated + conjecture. The second pass flips the proof by contradiction to obtain a + direct proof, introducing case splits when an inference depends on + several facts that depend on the negated conjecture. *) + fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape) val concl_ls = map (pair raw_prefix) (List.last conjecture_shape) - fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape) + val canonicalize_labels = + map (fn l => if member (op =) concl_ls l then hd concl_ls else l) + #> distinct (op =) fun first_pass ([], contra) = ([], contra) | first_pass ((step as Fix _) :: proof, contra) = first_pass (proof, contra) |>> cons step @@ -740,15 +746,19 @@ first_pass (proof, contra) |>> cons step | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) = if member (op =) concl_ls l then - first_pass (proof, contra ||> cons step) + first_pass (proof, contra ||> l = hd concl_ls ? cons step) else first_pass (proof, contra) |>> cons (Assume (l, find_hyp num)) - | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof, - contra) = - if exists (member (op =) (fst contra)) ls then - first_pass (proof, contra |>> cons l ||> cons step) - else - first_pass (proof, contra) |>> cons step + | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = + let + val ls = canonicalize_labels ls + val step = Have (qs, l, t, ByMetis (ls, ss)) + in + if exists (member (op =) (fst contra)) ls then + first_pass (proof, contra |>> cons l ||> cons step) + else + first_pass (proof, contra) |>> cons step + end | first_pass _ = raise Fail "malformed proof" val (proof_top, (contra_ls, contra_proof)) = first_pass (proof, (concl_ls, [])) @@ -756,23 +766,23 @@ fun backpatch_labels patches ls = fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) fun second_pass end_qs ([], assums, patches) = - ([Have (end_qs, no_label, - if length assums < length concl_ls then - clause_for_literals thy (map (negate_term thy o fst) assums) - else - concl_t, + ([Have (end_qs, no_label, concl_t, ByMetis (backpatch_labels patches (map snd assums)))], patches) | second_pass end_qs (Assume (l, t) :: proof, assums, patches) = second_pass end_qs (proof, (t, l) :: assums, patches) | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums, patches) = if member (op =) (snd (snd patches)) l andalso + not (member (op =) (fst (snd patches)) l) andalso not (AList.defined (op =) (fst patches) l) then second_pass end_qs (proof, assums, patches ||> apsnd (append ls)) else (case List.partition (member (op =) contra_ls) ls of ([contra_l], co_ls) => - if no_show qs then + if member (op =) qs Show then + second_pass end_qs (proof, assums, + patches |>> cons (contra_l, (co_ls, ss))) + else second_pass end_qs (proof, assums, patches |>> cons (contra_l, (l :: co_ls, ss))) @@ -781,9 +791,6 @@ else Have (qs, l, negate_term thy t, ByMetis (backpatch_label patches l))) - else - second_pass end_qs (proof, assums, - patches |>> cons (contra_l, (co_ls, ss))) | (contra_ls as _ :: _, co_ls) => let val proofs = @@ -801,7 +808,11 @@ ||> apsnd (union (op =) drop_ls)) |> fst |> SOME end) contra_ls - val facts = (co_ls, []) + val (assumes, facts) = + if member (op =) (fst (snd patches)) l then + ([Assume (l, negate_term thy t)], (l :: co_ls, ss)) + else + ([], (co_ls, ss)) in (case join_proofs proofs of SOME (l, t, proofs, proof_tail) => @@ -812,6 +823,7 @@ [Have (case_split_qualifiers proofs @ end_qs, no_label, concl_t, smart_case_split proofs facts)], patches) + |>> append assumes end | _ => raise Fail "malformed proof") | second_pass _ _ = raise Fail "malformed proof" @@ -914,9 +926,11 @@ fun string_for_proof ctxt i n = let - fun fix_print_mode f = - Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) f + fun fix_print_mode f x = + setmp_CRITICAL show_no_free_types true + (setmp_CRITICAL show_types true + (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) + (print_mode_value ())) f)) x fun do_indent ind = replicate_string (ind * indent_size) " " fun do_free (s, T) = maybe_quote s ^ " :: " ^ diff -r 664d3110beb2 -r f1734f3e9105 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jun 04 11:31:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jun 04 15:43:02 2010 +0200 @@ -91,7 +91,8 @@ end val subscript = implode o map (prefix "\<^isub>") o explode -val nat_subscript = subscript o string_of_int +fun nat_subscript n = + n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript fun plain_string_from_xml_tree t = Buffer.empty |> XML.add_content t |> Buffer.content