src/HOL/ex/mesontest2.ML

 \  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
 \  (~product(x::'a,additive_identity,additive_identity)) --> False",
   meson_tac);
 ****************)
 
-(*5 inferences so far.  Searching to depth 5.  7.600 secs*)
+(*5 inferences so far.  Searching to depth 5.  16.8 secs*)
+(*Best-first: 14.9 secs*)
 val BOO011_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X Y. sum(X::'a,Y,add(X::'a,Y))) & \

 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
 \  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
 \  (~equal(inverse(additive_identity),multiplicative_identity)) --> False",
   meson_tac);
 
-(*4007 inferences so far.  Searching to depth 9.  74.220 secs*)
+(*4007 inferences so far.  Searching to depth 9.  166.5 secs*)
 val CAT001_3 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! Y X. equivalent(X::'a,Y) --> there_exists(X)) &       \

 \  (there_exists(compose(b::'a,h))) &       \
 \  (equal(compose(b::'a,h),compose(b::'a,g))) & \
 \  (~equal(h::'a,g)) --> False",
   meson_tac);
 
-(*43468 inferences so far.  Searching to depth 14.  401.13 secs*)
-(*245 inferences so far.  Searching to depth 7.  5.160 secs*)
+(*245 inferences so far.  Searching to depth 7.  11.6 secs*)
 val CAT003_3 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! Y X. equivalent(X::'a,Y) --> there_exists(X)) &       \

 \  (~equal(domain(a),d)) --> False",
   meson_tac);
 ****************)
 
 
-(*1391 inferences so far.  Searching to depth 10. 118.03 secs*)
-(*1728 inferences so far.  Searching to depth 10.  33.520 secs*)
+(*1728 inferences so far.  Searching to depth 10.  74.1 secs*)
 val CAT007_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X Y. defined(X::'a,Y) --> product(X::'a,Y,compose(X::'a,Y))) &        \

 \  (! X Y Z. equal(X::'a,Y) --> equal(compose(X::'a,Z),compose(Y::'a,Z))) & \
 \  (equal(domain(a),codomain(b))) &     \
 \  (~defined(a::'a,b)) --> False",
   meson_tac);
 
-(*15290 inferences so far.  Searching to depth 12.  1649.59 secs*)
-(*82895 inferences so far.  Searching to depth 13.  1999.820 secs*)
+(*82895 inferences so far.  Searching to depth 13.  4770.8 secs*)
 val CAT018_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X Y. defined(X::'a,Y) --> product(X::'a,Y,compose(X::'a,Y))) &        \

 \  (defined(a::'a,b)) &     \
 \  (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*)
+(*1118 inferences so far.  Searching to depth 8.  30.0 secs*)
 val COL001_2 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X Y Z. equal(apply(apply(apply(s::'a,X),Y),Z),apply(apply(X::'a,Z),apply(Y::'a,Z)))) &        \

 \  (! D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) &  \
 \  (! X. equal(apply(apply(apply(s::'a,apply(b::'a,X)),i),apply(apply(s::'a,apply(b::'a,X)),i)),apply(x::'a,apply(apply(apply(s::'a,apply(b::'a,X)),i),apply(apply(s::'a,apply(b::'a,X)),i))))) &   \
 \  (! Y. ~equal(Y::'a,apply(combinator::'a,Y))) --> False",
   meson_tac);
 
-(*382 inferences so far.  Searching to depth 8.  7.8 secs*)
-(*500 inferences so far.  Searching to depth 8.  5.810 secs*)
+(*500 inferences so far.  Searching to depth 8.  14.9 secs*)
 val COL023_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X Y Z. equal(apply(apply(apply(b::'a,X),Y),Z),apply(X::'a,apply(Y::'a,Z)))) & \

 \  (! A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) &     \
 \  (! D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) &  \
 \  (! Y. ~equal(Y::'a,apply(combinator::'a,Y))) --> False",
   meson_tac);
 
-(*2423 inferences so far.  Searching to depth 10.  47.46 secs*)
-(*3018 inferences so far.  Searching to depth 10.  27.390 secs*)
+(*3018 inferences so far.  Searching to depth 10.  61.3 secs*)
 val COL032_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. equal(apply(m::'a,X),apply(X::'a,X))) &        \

 \  (~agreeable(a)) &    \
 \  (equal(c::'a,compose(a::'a,b))) --> False",
   meson_tac);
 ****************)
 
-(*13201 inferences so far.  Searching to depth 11.  473 secs*)
+(*13201 inferences so far.  Searching to depth 11.  489.0 secs*)
 val COL075_2 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! Y X. equal(apply(apply(k::'a,X),Y),X)) &      \

 \  (equal(n_right::'a,right_child_of(n))) & \
 \  (! Z. ~failure_node(Z::'a,or(empty::'a,empty))) --> False",
   meson_tac);
 ****************)
 
-(*179 inferences so far.  Searching to depth 7.  52.4 secs, mostly parsing*)
+(*179 inferences so far.  Searching to depth 7.  50.8 secs*)
 val GEO003_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X Y. between(X::'a,Y,X) --> equal(X::'a,Y)) &     \

 \  (equal(v::'a,reflection(u::'a,v))) & \
 \  (~equal(u::'a,v)) --> False",
   meson_tac);
 ****************)
 
-(*0 inferences so far.  Searching to depth 0. 2.1 secs*)
+(*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)) &        \
 \  (! V W U X. trapezoid(U::'a,V,W,X) --> parallel(V::'a,W,U,X)) &      \
 \  (! U V X Y. parallel(U::'a,V,X,Y) --> eq(X::'a,V,U,V,X,Y)) & \

 \  (product(a::'a,b,c)) &   \
 \  (~product(b::'a,a,c)) --> False",
   meson_tac);
 ****************)
 
-(*2386 inferences so far.  Searching to depth 11.  128 secs*)
+(*2386 inferences so far.  Searching to depth 11.  132.5 secs*)
 val GRP008_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. product(identity::'a,X,X)) &       \

 \  (! A. product(A::'a,inverse(A),identity)) &      \
 \  (! A. product(A::'a,identity,A)) &       \
 \  (! A. ~product(A::'a,a,identity)) --> False",
   meson_tac);
 
-(*47 inferences so far.  Searching to depth 11.  3.2 secs*)
+(*47 inferences so far.  Searching to depth 11.  2.5 secs*)
 val GRP034_4 = prove
  ("(! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
 \  (! X. product(identity::'a,X,X)) &       \
 \  (! X. product(X::'a,identity,X)) &       \
 \  (! X. product(X::'a,inverse(X),identity)) &      \

 \  (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) &        \
 \  (equal(a::'a,b)) &       \
 \  (~equal(multiply(c::'a,a),multiply(c::'a,b))) --> False",
   meson_tac);
 
-(*25559 inferences so far.  Searching to depth 19.  259.0 secs*)
+(*25559 inferences so far.  Searching to depth 19.  250.0 secs*)
 val GRP130_1_002 = prove
  ("(group_element(e_1)) &       \
 \  (group_element(e_2)) &       \
 \  (~equal(e_1::'a,e_2)) &  \
 \  (~equal(e_2::'a,e_1)) &  \

 \  (! J L K'. equal(J::'a,K') & less_equal(L::'a,J) --> less_equal(L::'a,K')) &     \
 \  (~less_equal(a::'a,a)) --> False",
   meson_tac);
 ****************)
 
-(*1063 inferences so far.  Searching to depth 20.  19.8 secs*)
+(*1063 inferences so far.  Searching to depth 20.  14.0 secs*)
 val LCL010_1 = prove
  ("(! X Y. is_a_theorem(equivalent(X::'a,Y)) & is_a_theorem(X) --> is_a_theorem(Y)) &       \
 \  (! X Z Y. is_a_theorem(equivalent(equivalent(X::'a,Y),equivalent(equivalent(X::'a,Z),equivalent(Z::'a,Y))))) &   \
 \  (~is_a_theorem(equivalent(equivalent(a::'a,b),equivalent(equivalent(c::'a,b),equivalent(a::'a,c))))) --> False",
   meson_tac);

 \  (! Y X. is_a_theorem(implies(implies(implies(X,Y),Y),implies(implies(Y,X),X)))) &    \
 \  (! Y X. is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X)))) &        \
 \  (~is_a_theorem(implies(implies(a,b),implies(implies(c,a),implies(c,b))))) --> False",
   meson_tac);
 
-(*667 inferences so far.  Searching to depth 9.  24.0 secs*)
+(*667 inferences so far.  Searching to depth 9.  19.3 secs*)
 val LCL143_1 = prove
  ("(! X. equal(X,X)) &  \
 \  (! Y X. equal(X,Y) --> equal(Y,X)) & \
 \  (! Y X Z. equal(X,Y) & equal(Y,Z) --> equal(X,Z)) &  \
 \  (! X. equal(implies(true,X),X)) &    \

 \  (! X Y. axiom(or(not(Y),X)) & theorem(Y) --> theorem(X)) &   \
 \  (! X Y Z. axiom(or(not(X),Y)) & theorem(or(not(Y),Z)) --> theorem(or(not(X),Z))) &   \
 \  (~theorem(or(not(not(or(p,q))),not(q)))) --> False",
   meson_tac);
 
-(*5849 inferences so far.  Searching to depth 12.  102.2 secs*)
+(*5849 inferences so far.  Searching to depth 12.  91.0 secs*)
 val LCL215_1 = prove
  ("(! A. axiom(or(not(or(A,A)),A))) &   \
 \  (! B A. axiom(or(not(A),or(B,A)))) & \
 \  (! B A. axiom(or(not(or(A,B)),or(B,A)))) &   \
 \  (! B A C. axiom(or(not(or(A,or(B,C))),or(B,or(A,C))))) &     \

 \  (! X Y. value(X::'a,falsity) & value(Y::'a,truth) --> value(xor(X::'a,Y),truth)) &       \
 \  (! X Y. value(X::'a,falsity) & value(Y::'a,falsity) --> value(xor(X::'a,Y),falsity)) &   \
 \  (! Value. ~value(xor(xor(xor(xor(truth::'a,falsity),falsity),truth),falsity),Value)) --> False",
   meson_tac);
 
-(*19116 inferences so far.  Searching to depth 16. 186.2 secs*)
+(*19116 inferences so far.  Searching to depth 16. 230.8 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)) &      \
 \  (! Y X. q(X::'a,Y) --> q(Y::'a,X)) & \
 \  (! X Y. p(X::'a,Y) | q(X::'a,Y)) &  \

 \  (~q(c::'a,d)) --> False",
   meson_tac);
 
 (*1713 inferences so far.  Searching to depth 10.  41.0 secs*)
 val NUM001_1 = prove
- ("(! A. equal(A::'a,A)) &  \
-\  (! B A C. equal(A::'a,B) & equal(B::'a,C) --> equal(A::'a,C)) &  \
-\  (! B A. equal(add(A::'a,B),add(B::'a,A))) &  \
-\  (! A B C. equal(add(A::'a,add(B::'a,C)),add(add(A::'a,B),C))) &  \
-\  (! B A. equal(subtract(add(A::'a,B),B),A)) &     \
-\  (! A B. equal(A::'a,subtract(add(A::'a,B),B))) &     \
-\  (! A C B. equal(add(subtract(A::'a,B),C),subtract(add(A::'a,C),B))) &        \
-\  (! A C B. equal(subtract(add(A::'a,B),C),add(subtract(A::'a,C),B))) &        \
+ ("(! A. equal(A::'a,A)) &                                                \
+\  (! B A C. equal(A::'a,B) & equal(B::'a,C) --> equal(A::'a,C)) &        \
+\  (! B A. equal(add(A::'a,B),add(B::'a,A))) &                            \
+\  (! A B C. equal(add(A::'a,add(B::'a,C)),add(add(A::'a,B),C))) &        \
+\  (! B A. equal(subtract(add(A::'a,B),B),A)) &                           \
+\  (! A B. equal(A::'a,subtract(add(A::'a,B),B))) &                       \
+\  (! A C B. equal(add(subtract(A::'a,B),C),subtract(add(A::'a,C),B))) &  \
+\  (! A C B. equal(subtract(add(A::'a,B),C),add(subtract(A::'a,C),B))) &  \
 \  (! A C B D. equal(A::'a,B) & equal(C::'a,add(A::'a,D)) --> equal(C::'a,add(B::'a,D))) &  \
 \  (! A C D B. equal(A::'a,B) & equal(C::'a,add(D::'a,A)) --> equal(C::'a,add(D::'a,B))) &  \
 \  (! A C B D. equal(A::'a,B) & equal(C::'a,subtract(A::'a,D)) --> equal(C::'a,subtract(B::'a,D))) &        \
 \  (! A C D B. equal(A::'a,B) & equal(C::'a,subtract(D::'a,A)) --> equal(C::'a,subtract(D::'a,B))) &        \
 \  (~equal(add(add(a::'a,b),c),add(a::'a,add(b::'a,c)))) --> False",
   meson_tac);
 
-(*20717 inferences so far.  Searching to depth 11.  165.0 secs*)
+(*20717 inferences so far.  Searching to depth 11.  208.5 secs*)
 val NUM021_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! A. equal(add(A::'a,num0),A)) &   \

 \  (~less(b::'a,a)) &       \
 \  (divides(c::'a,a)) &     \
 \  (! A. ~equal(successor(A),num0)) --> False",
   meson_tac);
 
-(*26320 inferences so far.  Searching to depth 10.  323.4 secs*)
+(*26320 inferences so far.  Searching to depth 10.  408.4 secs*)
 val NUM024_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! A. equal(add(A::'a,num0),A)) &   \

 \  (~function(z)) &     \
 \  (~equal(recursion_equation_functions(z),null_class)) --> False",
   meson_tac);
 ****************)
 
-(*4868 inferences so far.  Searching to depth 12.  79.7 secs*)
+(*4868 inferences so far.  Searching to depth 12.  67.8 secs*)
 val PLA002_1 = prove
  ("(! Situation1 Situation2. warm(Situation1) | cold(Situation2)) &    \
 \  (! Situation. at(a::'a,Situation) --> at(b::'a,walk(b::'a,Situation))) & \
 \  (! Situation. at(a::'a,Situation) --> at(b::'a,drive(b::'a,Situation))) &        \
 \  (! Situation. at(b::'a,Situation) --> at(a::'a,walk(a::'a,Situation))) & \

 \  (holds(empty::'a,s0)) &  \
 \  (! State. holds(clear(table),State)) &       \
 \  (! State. ~holds(on(a::'a,c),State)) --> False",
   meson_tac);
 
-(*13732 inferences so far.  Searching to depth 16.  168.5 secs*)
+(*13732 inferences so far.  Searching to depth 16.  150.8 secs*)
 val PLA022_1 = prove
  ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
 \  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
 \  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
 \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \

 \  (holds(empty::'a,s0)) &  \
 \  (! State. holds(clear(table),State)) &       \
 \  (! State. ~holds(and'(on(a::'a,c),on(c::'a,d)),State)) --> False",
   meson_tac);
 
-(*948 inferences so far.  Searching to depth 18.  19.4 secs*)
+(*948 inferences so far.  Searching to depth 18.  14.8 secs*)
 val PRV001_1 = prove
  ("(! X Y Z. q1(X::'a,Y,Z) & less_or_equal(X::'a,Y) --> q2(X::'a,Y,Z)) &    \
 \  (! X Y Z. q1(X::'a,Y,Z) --> less_or_equal(X::'a,Y) | q3(X::'a,Y,Z)) &   \
 \  (! Z X Y. q2(X::'a,Y,Z) --> q4(X::'a,Y,Y)) & \
 \  (! Z Y X. q3(X::'a,Y,Z) --> q4(X::'a,Y,X)) & \

 \  (label(boxc::'a,bananas)) &      \
 \  (contains(boxb::'a,apples)) &    \
 \  (~(contains(boxa::'a,bananas) & contains(boxc::'a,oranges))) --> False",
   meson_tac);
 
-(*35 inferences so far.  Searching to depth 5.  44.1 secs*)
+(*35 inferences so far.  Searching to depth 5.  36.5 secs*)
 val PUZ020_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! A B. equal(A::'a,B) --> equal(statement_by(A),statement_by(B))) &     \

 \  (product(b::'a,a,l)) &   \
 \  (product(c::'a,a,n)) &   \
 \  (~sum(l::'a,n,additive_identity)) --> False",
   meson_tac);
 
-(*8991 inferences so far.  Searching to depth 9.  325.8 secs*)
+(*8991 inferences so far.  Searching to depth 9.  300.9 secs*)
 val RNG041_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. sum(additive_identity::'a,X,X)) &  \

 \  (equal(negate(add(a::'a,negate(b))),c)) &        \
 \  (~equal(negate(add(c::'a,negate(add(b::'a,a)))),a)) --> False",
   meson_tac);
 ****************)
 
-(*6933 inferences so far.  Searching to depth 12.  88.9 secs*)
+(*6933 inferences so far.  Searching to depth 12.  75.7 secs*)
 val ROB013_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! Y X. equal(add(X::'a,Y),add(Y::'a,X))) &  \

 \  (! G H. equal(G::'a,H) --> equal(negate(G),negate(H))) & \
 \  (equal(negate(add(a::'a,b)),c)) &        \
 \  (~equal(negate(add(c::'a,negate(add(negate(b),a)))),a)) --> False",
   meson_tac);
 
-(*6614 inferences so far.  Searching to depth 11.  350.2 secs*)
+(*6614 inferences so far.  Searching to depth 11.  310.8 secs*)
 val ROB016_1 = prove
  ("(! X. equal(X::'a,X)) &  \
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! Y X. equal(add(X::'a,Y),add(Y::'a,X))) &  \