>>> One way to ameliorate this problem is to compose proofs lazily. >>> By that, I mean when you get to a step that's obvious to you, just cheat >>> (most proof assistants have some option to make a "tagged" theorem without >>> proof). >> >> Do you (or anyone) know if there is a way to do this in HOL Light? > > Looking at HOL Light's kernel briefly I think the only thing you can > do is call new_axiom a lot, which isn't exactly what you want, but > could work: make many new_axioms when you're cheating (you could write > a tactic that does this for use within a proof script), and check the > list of axioms to be sure you haven't cheated after you've filled > everything in.
This tactic already exists in HOL Light, and is called CHEAT_TAC. I occasionally use it to compose proofs lazily, but usually follow the mode recommended by Freek of proving everything properly (because I don't trust myself to cheat truthfully). Cheers, Joe ------------------------------------------------------------------------------ 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
