Re: [mizar] consider

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

Hi Freek,

> > So in more than a half of the relevant cases, the linking
> > would be "immediately" useful.
>
> Thanks very much for investigating this!  Maybe this will
> help me eventually get my wish that I can use "then" after
> a consider...

Good luck :-)).

> - Do these counts include "assume that" and "let ... such
>  that" and so on?

No. The "usefullness ratio" would not be so impressive with them, so I did 
not want to publish the aggregate statistics ;-). This is probably because 
"assume", "suppose", etc., are skeleton items, so they are stated "when 
the thesis requires it" and not necessarily "when they are really needed 
to justify something". Additionally, "assume" with one statement is 
linkable already now.

> - If you only look at considers that have just one statement
>  inside (so you can't be confused about what the "then"
>  refers to), then how many are there then?  Is this easy
>  to find out?

Just add the subcondition "and (last() = 2)" somewhere in Consider.pl - 
e.g. after "(position() > 1)". There are 15234 such one-statement consider 
items, so it is actually the most useful case for linkage.

> So the considers that do not get a reference to the statement
> in the consider immediately after, they are generally
> followed by a "take" or a "set" or something like that?

To get the immediate following sibling, use '//Consider/following-sibling::*[1]' as 
the XPath expression in Consider.pl:

Proposition: 21429 (10008 linkable, so 11421 not)
Consider: 7151     (2463 linkable, so 4688 not)
Reconsider: 6311   (2578 linkable, so 3733 not)
Take: 4220
Conclusion: 2992   (2329 linkable, so 663 not) 
Now: 1555
IterEquality: 1372 (could be linkable, but not measured now)
Set: 1350
DefPred: 566
Assume: 495
PerCasesReasoning: 268
Let: 228
DefFunc: 218
Given: 6


Josef