[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: strict
On Tue, 9 Jan 2007, Jesse Alama wrote:
You don't have to worry about proving "strictness" with your
definition -
if you define your functor using an "aggregate" structure term
explicitely enumerating all selectors, like
doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #),
then the "strict" attribute is added automatically. This is why the
definition of "strict" has a special meaning which is automatically
defined separately for all structures - and it is added to the XML
presentation even if it's not present in the actual miz/abs file.
I'm afraid that's not what I see: I have the definition
definition
func F2 -> doubleLoopStr equals
doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
coherence;
end;
and then the theorem
theorem F2 is strict;
but "This inference is not accepted". There's nothing wrong with the
definition in the sense that it is accepted without errors. What
might be going on here?
Make sure that it's not just the error explanation appended at the end of
the file that makes you think that the theorem is not accepted - add a
new-line after the theorem - I've just prepared a test file and already
started to worry as it seemed not accepted at first glance ;-))))
Here's my file - the statement _IS_ accepted:
----------------------------------------------------
environ
vocabularies TESTER,BINOP_1,VECTSP_1;
notations TARSKI,SUBSET_1,BINOP_1,VECTSP_1;
constructors BINOP_1,VECTSP_1;
begin
definition
func add2 -> BinOp of {0,1} means contradiction;
correctness;
::> *4
func prod2 -> BinOp of {0,1} means contradiction;
correctness;
::> *4
func unit2 -> Element of {0,1} means contradiction;
correctness;
::> *4
func zero2 -> Element of {0,1} means contradiction;
correctness;
::> *4
end;
definition
func F2 -> doubleLoopStr equals
doubleLoopStr(#{0,1},add2,prod2,unit2,zero2#);
coherence;
end;
theorem
F2 is strict;
::> 4: This inference is not accepted
--------------------------------------------
BTW: it's better to state such properties of F2 as functorial
registrations rather than theorems - this way they could be used
automatically by the checker when one would import your registrations.
Best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================