Re: [mizar] How to properly do inductive sets in Mizar?

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

On Wed, 7 Aug 2002, Freek Wiedijk wrote:

> >you can use the "Knaster" scheme
> 
> The scheme that I proved using "Knaster" was (of course this
> is only part of the induction principle: maybe it should have
> a different name):
> 
>   scheme Inductive
>     {A() -> non empty set, P[set,set]}:
>    ex X being Subset of A() st
>     for x being Element of A() holds x in X iff P[x,X]
>   provided
>    for x,X,X' being set st X c= X' & P[x,X] holds P[x,X']
> 
> Is something like this already in the library?  If so: how
> should I have found it?


If you were sure enough, that Knaster has to be used for this, you can 
simply grep *.miz for "Knaster" - this gave me (suprisingly) no results, 
so there is no theorem or scheme in MML using the Knaster scheme so far.

Unfortunately, the proof of Knaster is not too long, so grepping e.g. for 
all theorems from the article KNASTER might be necessary too.

Grep is not bad, but I repeat what I have written earlier: the proof 
presentation is quite important and e.g. having such possibilities in 
Query ("find all theorems (in)directly using theorem "Foo", etc.) would be 
even better. 

Also, Mizar now lacks theorem proving tools, that could be of some help 
when MML contains some generalization of what you are looking for. 

Josef