Vladimir Timashov wrote: > I have some problem with proving in HOL4.
> I have some subgoal: > -- 1 <= i - 1 > ------------------------------------ > 0. ... > 1. 1 <= i > 2. ... > 3. ... > 4. ... > 5. ... > : goalstack > So it seems to be trivial but I can't find the way to prove it in > HOL. Could anybody help me with this please? What tactic should I > use? Or may be I should inform HOL in some way to use assumption #1? Which theory are you working in? In particular, I don't know what constant you're trying to write with the symbol --. In HOL4, the unary negation is written with ~ (the tilde character), mimicking what is done in SML. If you were trying to prove ``1 <= i ==> ~1 <= i - 1`` the appropriate tactic would depend on whether you were in the integers or reals. For the reals, I'd recommend: SRW_TAC [realSimps.REAL_ARITH_ss][] For the integers: intLib.ARITH_TAC There should be an analogue of REAL_ARITH_ss for the integers, but I haven't written it yet. Michael. ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
