[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] quite some questions about functions


Hi Ad[ae]m :-),

On Mon, 12 May 2008, Adam Naumowicz wrote:


On Mon, 12 May 2008, Ozyavas, Adem wrote:
3) Is there any method/tool to know what the current thesis is at any point of proof? 

definition
 func exp -> Function of COMPLEX, COMPLEX means
 :Def18:
 for z being Element of COMPLEX holds it.z=Sum(z ExpSeq);
 existence
 proof
   deffunc U(Element of COMPLEX) = Sum($1 ExpSeq);
   consider f being Function of COMPLEX, COMPLEX such that
A1: for x being Element of COMPLEX holds f.x = U(x) from FUNCT_2:sch 4;
   take f;
   thus thesis by A1;
 end;
 uniqueness
 proof
 ...
Fortunately Josef has added such functionality to his XML rendering of Mizar articles. Just run Mizar on an article and then view the *.xml file created in an XML-supporting web browser - you should be able to click on some items to see the thesis at certain proof steps.
Or, if it is an existing MML article like in this case, just go to: http://mmlquery.mizar.org/mml/current/sin_cos.html#D18 . Clicking on the 'existence' keyword will show you the existence condition, and clicking on the followng 'proof' keyword will expand the proof, where the ':: thesis:' after each natural deduction step can again be clicked on.
If it is a new article (not yet in MML), either use the method Adam described, or you can also paste the article into http://octopi.mizar.org/~mptp/MizAR.html and press the Send button. 

Josef