# HG changeset patch # User blanchet # Date 1275656930 -7200 # Node ID c2a44bc874f9d106e2772b87ee242f1f64ccd72f # Parent d77250dd24162116a16e4b21fc7fa4c7b9123e4b redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs diff -r d77250dd2416 -r c2a44bc874f9 src/HOL/Metis_Examples/set.thy --- a/src/HOL/Metis_Examples/set.thy Fri Jun 04 14:08:23 2010 +0200 +++ b/src/HOL/Metis_Examples/set.thy Fri Jun 04 15:08:50 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