Re: [mizar] How to search for a lemma?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Wed, Mar 05, 2003 at 12:19:14PM +0100, Freek Wiedijk wrote:

> I just spent an hour looking for a lemma that would give me
> 
>   for x,y being real number st x < y holds y - x > 0
> 
> Finally I gave up and used REAL_1:54 and REAL_1:36 with an
> intermediate step (y - x > x - x).
> 
> So my question is not so much what was the lemma that I
> needed, but how to find it myself.  Grzegorz (or someone else
> who knows), can you tell me how to do this with MML Query?

I am surprised that Grzegorz has not answered yet.  This is the type of
question that MML Query is meant to answer.

The fact that Freek is looking for involves the following constructors

	HIDDEN:mode 1 		set
	XREAL_0:attr 1 		real
	XREAL_0:func 5 		-  (binary)
	XREAL_0:pred 1 		<= 

and in addition number 0.  We query for the theorems in which these resources occur exactly
(i.e. no other resources occur)

exactly * ({hidden:mode 1, xreal_0:attr 1, xreal_0:pred 1, xreal_0:func 5, number 0}) | th

This was the idea behind MML Query, unfortunately at this very moment
it will give you an empty answer because something is broken in the implementation
and only Grzegorz would be able to help.


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr