Re: [mizar] Now I know why I cannot quote a theorem but the trouble remains

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

Hi:

I would like to thank Adam and Artur for prompt reply.  It was late into
the night and I did not see it myself for I needed the notation from 
POLYNOM1 too.

So I am now facing now a bigger trouble.  Have a look at this:

-------------------------------------------------------------------------------

environ

 vocabulary RLVECT_1, FINSEQ_1, VECTSP_1, LATTICES;
 notation SUBSET_1, STRUCT_0, RLVECT_1, VECTSP_1, FINSEQ_1, POLYNOM1, FVSUM_1;
 constructors MONOID_0, FVSUM_1, SIN_COS, POLYNOM5, WELLFND1, ALGSTR_1,
      POLYNOM2;
 clusters MONOID_0, POLYNOM4;
 theorems POLYNOM1, FVSUM_1;

begin

:: theorem :: POLYNOM1:23
 for L being non empty HGrStr, a being Element of the carrier of L,
     p, q being FinSequence of the carrier of L
  holds (p^q)*a = (p*a)^(q*a) by POLYNOM1:24;


:: theorem :: POLYNOM1:23
 for L being non empty HGrStr, a being Element of the carrier of L,
     p, q being FinSequence of the carrier of L
  holds a*(p^q) = (a*p)^(a*q) by POLYNOM1:23;
::>                            *4


::theorem :: FVSUM_1:92
   for K being Abelian add-associative right_zeroed
        right_complementable distributive(non empty doubleLoopStr),
     a being Element of the carrier of K,
     p being FinSequence of the carrier of K holds
   Sum(a*p) = a*(Sum p) by FVSUM_1:92;

::> 4: This inference is not accepted

-------------------------------------------------------------------------------

I need both notations from FVSUM1 and from POLYNOM1.  What am I supposed
to do?

This brings back the issue of Universal Resource Naming (URN).  I am
in favour of using Grzegorz's names from MML Query and I would put up
with writing something like this:

  URN(POLYNOM1:func 6,a,p^q)       instead of          a*(p^q)

  Sum URN(FVSUM_1:func 9,a,p)      instead of          Sum(a*p)

when I know what I want to say and Mizar would not let me.  All
library resources should be available in this way and it is not meant
only for the masochist types.

The first time that I have proposed introducing this was in late 70's
in some write-up and then more seriously in 1993 but probably there
were many before me.

Best,

PR


On Sat, Nov 29, 2003 at 10:07:37AM +0100, Artur Kornilowicz wrote:
> Piotr,
> put notation FVSUM_1 after POLYNOM_1. And see
> 
> definition
>  let L be non empty HGrStr,
>      a be Element of the carrier of L,
>      p be FinSequence of the carrier of L;
>  func a*p -> FinSequence of the carrier of L means
> :: POLYNOM1:def 2
>   dom it = dom p &
>   for i being set st i in dom p holds it/.i = a*(p/.i);
> end;
> 
> definition let K be non empty HGrStr;
>    let p be FinSequence of the carrier of K;
>    let a be Element of the carrier of K;
>   func a*p -> FinSequence of the carrier of K equals
> :: FVSUM_1:def 6
>   (a multfield)*p;
> end;
> 
> Artur
> 
> 
> On Sat, 29 Nov 2003, Piotr Rudnicki wrote:
> 
> > Hi:
> >
> > In the text below I am unable to quote a theorem. Why?

..  snap snap ...

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