[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] "mode Element of ...", some questions...
Hi Adem,
there is a couple of solutions to your problem:
first, at global level (e.g. theorems) you can write
theorem
for x being Element of setA st x = 1 holds f(x) ...;
Inside proofs you can write
reconsider j = 1 as Element of setA;
f(j) = ...;
You can't use 'j' in theorems formulations because local constants can't
be imported to the library.
Another solution is to use
definition
let x, y be set;
assume x in y;
func In (x, y) -> Element of y equals
:: FUNCT_7:def 1
x;
end;
Having this, Mizar automatically knows that
In(1,setA) is Element of setA;
So you can formulate facts as
f(In(1,setA)) = ...;
I believe it helps.
Best regards
Artur
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. (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?
Thank you all and I always appreciate the group's help.
Regards,
Adem Ozyavas
Texas Tech University
==========================================================================
Artur Kornilowicz e-mail: arturk@math.uwb.edu.pl
Dept. of Programming and Formal Methods http://math.uwb.edu.pl/~arturk/
Institute of Computer Science tel. +48 (85) 745-7662
University of Bialystok fax. +48 (85) 745-7662
Sosnowa 64, 15-887 Bialystok, Poland