*To*: Steve W <s.wong.731 at googlemail.com>*Subject*: Re: [isabelle] Problems with Real addition*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 21 Jan 2010 21:41:39 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <12d162d01001201951t1539db6eh6f8a791368d8eeec@mail.gmail.com>*References*: <12d162d01001201951t1539db6eh6f8a791368d8eeec@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

On Wed, Jan 20, 2010 at 7:51 PM, Steve W <s.wong.731 at googlemail.com> wrote: > I'm trying out addition in Real, but have run into some problems. Does > anyone know why the first example below doesn't work but the second does? Is > it a problem with the types? Hi Steve, This is not a problem with the types. It works exactly the same with type int or rat as it does with real. > axioms > ax : "F(t) = 0" > > lemma test: "EX x. F(x) + 1 ~= 0" > using ax > by auto You should realize that you are asking a lot of "auto" here, since proving this lemma requires it to guess a witness for the existential quantifier. The "auto" tactic can only guess witnesses in very limited circumstances. > axioms > ax : "F(t) = 0" > > lemma test: "EX x. F(x) + 0 = 0" > using ax > by auto Your second example happens to be one of the limited circumstances where auto *can* solve an existential. Simplification replaces "F(x) + 0" with "F(x)", leaving the subgoal "EX x. F(x) = 0" which just happens to match up perfectly with the rule "ax" that you provided. In general, you should only expect "auto" to solve existentials if they can be solved in one step by rule exI. Other tactics besides "auto" are better at solving existentials. For example, the "metis" tactic can solve your goal: lemma test: "EX x. F(x) + 1 ~= 0" using ax by (metis one_neq_zero add_0_left) The drawback with metis is that you need to supply all the other lemmas needed to solve the goal. In the end, it is often easiest to just provide the witness yourself: lemma test: "EX x. F(x) + 1 ~= 0" proof show "F(t) + 1 ~= 0" using ax by simp qed Hope this helps, - Brian

**References**:**[isabelle] Problems with Real addition***From:*Steve W

- Previous by Date: Re: [isabelle] Isabelle Proof in Papers
- Next by Date: [isabelle] MSCS Special Issue - Mechanization of Mathematics
- Previous by Thread: [isabelle] Problems with Real addition
- Next by Thread: [isabelle] Using Word, Map and Set in Haskabelle
- Cl-isabelle-users January 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list