Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?



2012-08-10 12:22 Johannes Hölzl:
Am Freitag, den 10.08.2012, 12:08 +0200 schrieb Christoph LANGE:
2012-08-10 10:15 Brian Huffman:
by (rule less_imp_le)

…

Generally, when similar situations occur in future: Is there any
documentation of such rules?  In the manuals that come with Isabelle I
didn't find anything.

The theories are documented in
   http://isabelle.in.tum.de/dist/library/HOL/Orderings.html

but this is neither searchable nor very readable.

Thanks! Grepping the *.thy source files has been very useful for me so far. Actually the only reason why I ended up in the ML sources was that in the theory sources there was a lot of "noise" from this rule being _applied_, so I just overlooked the lemma.

There are two better methods:

Thanks a lot – very helpful. As a newbie, obviously, I knew neither of them.

  * use find_theorems
      like: find_theorems "_ > _ ==> _ >= _"
                           ^
I think here it expects a numeric argument as said below; didn't work without.

…
    General rule: give a list of constants and not more:
      find_theorems (200) "_ > _" "_ >= _" name: Ord
    (the (200) tells find theorem to list the first 200 results)

BTW in the documentation find_theorems is only mentioned in prog-prove.pdf (just searched all files with pdfgrep), and there it says:

--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---
Command find_theorems searches for specific theorems in the current theory.
Search criteria include pattern matching on terms and on names. For details
see the Isabelle/Isar Reference Manual [4].
--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---

… but the reference manual does't mention it.

Generally, I had no idea that one can apply _any_ theorem using (rule name_of_theorem). This wasn't obvious to me, and instead I had thought that "rules" are something special that's built in at the level of "a calculus for a logic".

  * use sledgehammer:

      lemma "(x::real) > 0 --> x >= 0"
        sledgehammer

    This will now try to find a proof for this.
    The proof will contain the necessary lemmas.

Excellent, very helpful too!

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Building & Exploring Web Based Environments.  Seville, Spain, 27 Jan–
  1 Feb 2013.  Deadline 2 Sep.  http://iaria.org/conferences2013/WEB13.html





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.