[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] "mode Element of ...", some questions...
On Tue, 20 Oct 2009, Ozyavas, Adem wrote:
Dear All,
I would like to ask a question but before that please let me present the following Mizar fragment:
definition
func setA -> set equals
{k where k is Element of NAT: k < 15};
correctness;
end;
definition
let e be Element of setA;
func f(e) -> Element of setA means
...
end;
f(1) = ...;
::>*103 (Unknown Functor)
1 is Element of setA;
::> *4 (This inference is not accepted)
My questions are
(1) how to make Mizar accept "1 is Element of setA"? I checked the MML for "mode Element of ..." examples and could not find anything that could help me.
As '1' is a numeral and not a 'regular' functor, you cannot redefine it,
or register new attributes for it.
(2) This relates to the Question (1). How can I make sure that 1 is known to be an Element of setA so that 103 error does not occur?
But you can always use a 'permissive' definition of f(), so that it
accepts all 'Element of NAT', but is meaningful only for these in 'setA',
e.g.
definition
let e be Element of NAT;
assume e in setA;
:: or e < 15
func f(e) -> Element of setA means
...
end;
Then f(1) is a perfectly legal expression;
Best,
Adam Naumowicz
=======================================================================
Dept. of Programming and Formal Methods Fax: +48(85)7457662
Institute of Informatics Tel: +48(85)7457559 (office)
University of Bialystok E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
=======================================================================