# HG changeset patch
# User paulson
# Date 831372283 -7200
# Node ID 4d34973672d60e90e7a9be0e2ed2f52403b5319b
# Parent  8b677c7e18bc5e1a3126a894bdbcea329ec1cbf6
Updated timings; more theorems can be proved

diff -r 8b677c7e18bc -r 4d34973672d6 src/HOL/ex/mesontest2.ML
--- 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 @@
 \  (~equal(multiply(multiply(associator(a::'a,a,b),a),associator(a::'a,a,b)),additive_identity)) --> False",
   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 @@
 \  (~equal(associator(x::'a,x,y),additive_identity)) --> False",
   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. sum(X::'a,additive_identity,X)) &  \
 \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
@@ -2753,8 +2741,7 @@
 \  (~equal(b::'a,additive_identity)) --> False",
   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 @@
 \  (~sum(l::'a,n,additive_identity)) --> False",
   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 @@
 \  (~equal(negate(add(c::'a,negate(add(negate(b),a)))),a)) --> False",
   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 @@
 \  (~equal(negate(add(e::'a,multiply(k::'a,add(d::'a,negate(add(d::'a,negate(e))))))),negate(e))) --> False",
   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)) &    \