author paulson Mon, 06 May 1996 10:44:43 +0200 changeset 1720 4d34973672d6 parent 1719 8b677c7e18bc child 1721 445654b6cb95
Updated timings; more theorems can be proved
 src/HOL/ex/mesontest2.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/mesontest2.ML	Mon May 06 10:39:54 1996 +0200
+++ b/src/HOL/ex/mesontest2.ML	Mon May 06 10:44:43 1996 +0200
@@ -1,5 +1,5 @@
(* Courtesy John Harrison
-   HOL can parse them in Prod.thy, regarding arguments as tuples
+  \$Id\$
Changed numeric constants e.g. 0, 1, 2... to num0, num1, num2...
*)

@@ -118,6 +118,7 @@
* TOP005-2    139.8    Lemma 1e [Wick & McCune, 1989]
*)

+(*Prod.thy instead of HOL.thy to regard arguments as tuples*)
fun prove (s,tac) = prove_goal Prod.thy s (fn [] => [tac]);

val meson_tac = safe_meson_tac 1;
@@ -488,7 +489,6 @@
\  (~defined(a::'a,b)) --> False",
meson_tac);

-(****************ABOVE FIVE MINUTES
(*15290 inferences so far.  Searching to depth 12.  1649.59 secs*)
(*82895 inferences so far.  Searching to depth 13.  1999.820 secs*)
val CAT018_1 = prove
@@ -527,7 +527,6 @@
\  (defined(b::'a,c)) &     \
\  (~defined(a::'a,compose(b::'a,c))) --> False",
meson_tac);
-****************)

(* 896 inferences so far.  Searching to depth 8.  18.92 secs*)
(*1118 inferences so far.  Searching to depth 8.  13.480 secs*)
@@ -1010,7 +1009,7 @@
meson_tac);
****************)

-(****************ABOVE FIVE MINUTES
+(*0 inferences so far.  Searching to depth 0. 2.1 secs*)
val GEO079_1 = prove
("(! U V W X Y Z. right_angle(U::'a,V,W) & right_angle(X::'a,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &       \
\  (! U V W X Y Z. congruent(U::'a,V,W,X,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &        \
@@ -1019,7 +1018,6 @@
\  (trapezoid(a::'a,b,c,d)) &       \
\  (~eq(a::'a,c,b,c,a,d)) --> False",
meson_tac);
-****************)

(****************ABOVE FIVE MINUTES
val GRP001_1 = prove
@@ -1553,7 +1551,7 @@
\  (! Value. ~value(xor(xor(xor(xor(truth::'a,falsity),falsity),truth),falsity),Value)) --> False",
meson_tac);

-(****************ABOVE FIVE MINUTES
+(*19116 inferences so far.  Searching to depth 16. 186.2 secs*)
val MSC006_1 = prove
("(! Y X Z. p(X::'a,Y) & p(Y::'a,Z) --> p(X::'a,Z)) &      \
\  (! Y X Z. q(X::'a,Y) & q(Y::'a,Z) --> q(X::'a,Z)) &      \
@@ -1562,7 +1560,6 @@
\  (~p(a::'a,b)) &  \
\  (~q(c::'a,d)) --> False",
meson_tac);
-****************)

(*1713 inferences so far.  Searching to depth 10.  41.0 secs*)
val NUM001_1 = prove
@@ -2407,8 +2404,7 @@
\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,l) & less_than(a(X),a(predecessor(X))))) --> False",
meson_tac);

-(*2343 inferences so far.  Searching to depth 8
-Process time (incl GC): 53.8 secs*)
+(*2343 inferences so far.  Searching to depth 8.  53.8 secs*)
val PRV006_1 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2438,8 +2434,7 @@
\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,i) & less_than(a(X),a(predecessor(X))))) --> False",
meson_tac);

-(*86 inferences so far.  Searching to depth 14
-Process time (incl GC): 2.2 secs*)
+(*86 inferences so far.  Searching to depth 14.  2.2 secs*)
val PRV009_1 = prove
("(! Y X. less_or_equal(X::'a,Y) | less(Y::'a,X)) &   \
\  (less(j::'a,i)) &        \
@@ -2452,8 +2447,7 @@
\  (~less_or_equal(a(p),a(q))) --> False",
meson_tac);

-(*222 inferences so far.  Searching to depth 8
-Process time (incl GC): 4.8 secs*)
+(*222 inferences so far.  Searching to depth 8.  4.8 secs*)
val PUZ012_1 = prove
("(! X. equal_fruits(X::'a,X)) &   \
\  (! X. equal_boxes(X::'a,X)) &    \
@@ -2475,8 +2469,7 @@
\  (~(contains(boxa::'a,bananas) & contains(boxc::'a,oranges))) --> False",
meson_tac);

-(*35 inferences so far.  Searching to depth 5
-Process time (incl GC): 44.1 secs*)
+(*35 inferences so far.  Searching to depth 5.  44.1 secs*)
val PUZ020_1 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2538,8 +2531,7 @@
meson_tac);
****************)

-(*621 inferences so far.  Searching to depth 18
-Process time (incl GC): 4.8 secs*)
+(*621 inferences so far.  Searching to depth 18.  4.8 secs*)
val PUZ029_1 = prove
("(! X. dances_on_tightropes(X) | eats_pennybuns(X) | old(X)) &      \
\  (! X. pig(X) & liable_to_giddiness(X) --> treated_with_respect(X)) & \
@@ -2606,8 +2598,7 @@
meson_tac);
****************)

-(*0 inferences so far.  Searching to depth 0
-Process time (incl GC): 7.6 secs*)
+(*0 inferences so far.  Searching to depth 0.  7.6 secs*)
val RNG011_5 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2646,8 +2637,7 @@
meson_tac);

-(*202 inferences so far.  Searching to depth 8
-Process time (incl GC): 7.4 secs*)
+(*202 inferences so far.  Searching to depth 8.  7.4 secs*)
val RNG023_6 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2680,8 +2670,7 @@
meson_tac);

-(*0 inferences so far.  Searching to depth 0
-Process time (incl GC): 7.4 secs*)
+(*0 inferences so far.  Searching to depth 0.  7.4 secs*)
val RNG028_2 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2718,8 +2707,7 @@
\  (~equal(multiply(multiply(cx::'a,multiply(cy::'a,cx)),cz),multiply(cx::'a,multiply(cy::'a,multiply(cx::'a,cz))))) --> False",
meson_tac);

-(*209 inferences so far.  Searching to depth 9
-Process time (incl GC): 16.3 secs*)
+(*209 inferences so far.  Searching to depth 9.  16.3 secs*)
val RNG038_2 = prove
\  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
@@ -2753,8 +2741,7 @@
meson_tac);

-(*2660 inferences so far.  Searching to depth 10
-Process time (incl GC): 100.5 secs*)
+(*2660 inferences so far.  Searching to depth 10.  100.5 secs*)
val RNG040_2 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2798,8 +2785,7 @@
meson_tac);

-(*8991 inferences so far.  Searching to depth 9
-Process time (incl GC): 325.8 secs*)
+(*8991 inferences so far.  Searching to depth 9.  325.8 secs*)
val RNG041_1 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2860,8 +2846,7 @@
meson_tac);
****************)

-(*6933 inferences so far.  Searching to depth 12
-Process time (incl GC): 88.9 secs*)
+(*6933 inferences so far.  Searching to depth 12.  88.9 secs*)
val ROB013_1 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2876,8 +2861,7 @@
meson_tac);

-(*6614 inferences so far.  Searching to depth 11
-Process time (incl GC): 350.2 secs*)
+(*6614 inferences so far.  Searching to depth 11.  350.2 secs*)
val ROB016_1 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2902,8 +2886,7 @@
meson_tac);

-(*14077 inferences so far.  Searching to depth 11
-Process time (incl GC): 561.3 secs*)
+(*14077 inferences so far.  Searching to depth 11.  561.3 secs*)
val ROB021_1 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -2939,8 +2922,7 @@
meson_tac);
****************)

-(*6450 inferences so far.  Searching to depth 14
-Process time (incl GC): 67.5 secs*)
+(*6450 inferences so far.  Searching to depth 14.  67.5 secs*)
val SET009_1 = prove
("(! Subset Element Superset. member(Element::'a,Subset) & subset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \
\  (! Superset Subset. subset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) &       \
@@ -3232,16 +3214,14 @@
meson_tac);
****************)

-(*13 inferences so far.  Searching to depth 8
-Process time (incl GC): 0.9 secs*)
+(*13 inferences so far.  Searching to depth 8.  0.9 secs*)
val SET046_5 = prove
("(! Y X. ~(element(X::'a,a) & element(X::'a,Y) & element(Y::'a,X))) &     \
\  (! X. element(X::'a,f(X)) | element(X::'a,a)) &     \
\  (! X. element(f(X),X) | element(X::'a,a)) --> False",
meson_tac);

-(*33 inferences so far.  Searching to depth 9
-Process time (incl GC): 3.0 secs*)
+(*33 inferences so far.  Searching to depth 9.  3.0 secs*)
val SET047_5 = prove
("(! X Z Y. set_equal(X::'a,Y) & element(Z::'a,X) --> element(Z::'a,Y)) &  \
\  (! Y Z X. set_equal(X::'a,Y) & element(Z::'a,Y) --> element(Z::'a,X)) &  \
@@ -3251,16 +3231,14 @@
\  (~(set_equal(b::'a,a) & set_equal(a::'a,b))) --> False",
meson_tac);

-(*311 inferences so far.  Searching to depth 12
-Process time (incl GC): 2.0 secs*)
+(*311 inferences so far.  Searching to depth 12.  2.0 secs*)
val SYN034_1 = prove
("(! A. p(A::'a,a) | p(A::'a,f(A))) & \
\  (! A. p(A::'a,a) | p(f(A),A)) & \
\  (! A B. ~(p(A::'a,B) & p(B::'a,A) & p(B::'a,a))) --> False",
meson_tac);

-(*30 inferences so far.  Searching to depth 6
-Process time (incl GC): 2.8 secs*)
+(*30 inferences so far.  Searching to depth 6.  2.8 secs*)
val SYN071_1 = prove
("(! X. equal(X::'a,X)) &  \
\  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
@@ -3286,8 +3264,7 @@
meson_tac);
****************)

-(*398 inferences so far.  Searching to depth 12
-Process time (incl GC): 6.8 secs*)
+(*398 inferences so far.  Searching to depth 12.  6.8 secs*)
val SYN352_1 = prove
("(f(a::'a,b)) &   \
\  (! X Y. f(X::'a,Y) --> f(b::'a,z(X::'a,Y)) | f(Y::'a,z(X::'a,Y))) &     \
@@ -3298,8 +3275,7 @@
\  (! X Y. f(X::'a,Y) --> f(X::'a,z(X::'a,Y)) | f(Y::'a,z(X::'a,Y))) --> False",
meson_tac);

-(*5336 inferences so far.  Searching to depth 15
-Process time (incl GC): 80.9 secs*)
+(*5336 inferences so far.  Searching to depth 15.  80.9 secs*)
val TOP001_2 = prove
("(! Vf U. element_of_set(U::'a,union_of_members(Vf)) --> element_of_set(U::'a,f1(Vf::'a,U))) &    \
\  (! U Vf. element_of_set(U::'a,union_of_members(Vf)) --> element_of_collection(f1(Vf::'a,U),Vf)) &    \
@@ -3316,8 +3292,7 @@
\  (~subset_sets(union_of_members(top_of_basis(f)),cx)) --> False",
meson_tac);

-(*0 inferences so far.  Searching to depth 0
-Process time (incl GC): 0.3 secs*)
+(*0 inferences so far.  Searching to depth 0.  0.3 secs*)
val TOP002_2 = prove
("(! Vf U. element_of_collection(U::'a,top_of_basis(Vf)) | element_of_set(f11(Vf::'a,U),U)) & \
\  (! X. ~element_of_set(X::'a,empty_set)) &        \
@@ -3442,8 +3417,7 @@
meson_tac);
****************)

-(*0 inferences so far.  Searching to depth 0
-Process time (incl GC): 8.2 secs*)
+(*0 inferences so far.  Searching to depth 0.  8.2 secs*)
val TOP004_2 = prove
("(! U Uu1 Vf. element_of_set(U::'a,Uu1) & element_of_collection(Uu1::'a,Vf) --> element_of_set(U::'a,union_of_members(Vf))) &     \
\  (! Vf X. basis(X::'a,Vf) --> equal_sets(union_of_members(Vf),X)) &       \
@@ -3468,8 +3442,7 @@
\  (! U V. ~element_of_collection(intersection_of_sets(U::'a,V),top_of_basis(f))) --> False",
meson_tac);

-(*53777 inferences so far.  Searching to depth 20
-Process time (incl GC): 1089.3 secs*)
+(*53777 inferences so far.  Searching to depth 20.  1089.3 secs*)
val TOP005_2 = prove
("(! Vf U. element_of_set(U::'a,union_of_members(Vf)) --> element_of_set(U::'a,f1(Vf::'a,U))) &    \
\  (! U Vf. element_of_set(U::'a,union_of_members(Vf)) --> element_of_collection(f1(Vf::'a,U),Vf)) &    \```