Thanks, John! I'll fiddle with the miz3 term `set' and book up in the Mizar literature. This is excellent:
Yes, this may be the core problem: the default built-in miz3 prover doesn't know much about sets, and may not know that, say, the formulas S = {x | P x} and !x. x IN S <=> P x are equivalent, as you might have expected. There is a standard HOL Light tactic called SET_TAC that does some preprocessing of set operations and then calls MESON. It would certainly be possible to change the default miz3 prover to do something similar. Thanks! That really helps my faith in HOL Light. That would be great if you or Freek could make this improvement. You are probably going to hit quite a few such restrictions as you are using miz3 pretty heavily, and it may make sense for us to improve the default miz3 prover as you hit these issues rather than have you work around them. However, I am a bit short of time to work on it right now so I can't promise to fix these shortcomings myself in the short term. Can we make a deal? If I code up the Hilbert plane geometry part of my paper (18+ pages), can you fix it by the time I'm done? I think it would be easy to modify my worked-around code if you fix it by then. -- Best, Bill ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info