Dear everyone, John Harrison pointed out to me that the following query was posted on the hol-info mailing list (I'm subscribed to that list but often just delete the messages without looking, sorry about that. So I missed this):
>6) I am very curious about Mizar Light and would like to convert >my exercise to Mizar Light. I found the Mizar Light sources as >well Freek's paper on Mizar Light. However, at first glance it >seemed as if the syntax for Mizar Light given in the paper is >quite different from what I saw in the source. So... what is the >current status of the project? There have been three experiments that I called "Mizar Light". However, after some soal searching I decided to rename the third thing from "Mizar Light III" to "miz3", so please don't call this third version Mizar Light anymore... :-) 1. The first thing is described in a TPHOLs paper from 2001, <http://www.cs.ru.nl/~freek/mizar/miz.pdf>. _Conceptually,_ I still _really_ like this, but ergonomically it's completely unusable, because of all the quotes and brackets, and because it's really hard to debug proofs. The Mizar proof Lm1: P implies P proof assume P; hence P; end; becomes in this framework: let lm1 = prove (`P ==> P`, ASSUME_A(0,`P:bool`) THEN THUS(`P:bool`) (BY [0][]));; 2. The second version never has been published about, but is part of the HOL Light distribution, it is in the sub-directory "Mizarlight". It is an attempt to make the first version more ergonomic, while still keeping the property that a proof is just ocaml code, so without having a separate "Mizar parser". In this system the above proof becomes: let lm1 = theorem "P ==> P" [assume "P"; hence "P"];; 3. And then there's my recent "miz3" system, which is my current best effort, and which (very similar to John Harrison's "Mizar mode") _does_ have a separate parser that allows one to get really close to Mizar syntax. It's described in the recent paper <http://www.cs.ru.nl/~freek/miz3/miz3.pdf>, and the system can be downloaded as <http://www.cs.ru.nl/~freek/miz3/miz3.tar.gz>. In this system the example is: let lm1 = thm `; let P be bool; thus P ==> P proof assume P; thus P; end`;; (In miz3 all variables have to be bound, either in the formula or in the context, hence the "let" at the start. Also in miz3 "then" is implicit, hence the "thus" instead of the "hence".) I hope this clears things up. I guess the poster might have been confused between the first and second, or second and third version of the thing? Ah yes, and if someone would like help with using miz3, just mail me! Freek ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
