[isabelle-dev] Default simprules for division in fields
thomas.sewell at nicta.com.au
Mon Apr 7 03:11:59 CEST 2014
This makes me realise that I may have been misunderstanding field_simps.
I've been using it as a replacement after ring_simps disappeared a while
ago. It always struck me as odd, since I'm nearly always in a word type,
which is a ring but not a field.
Is it just a coincidence that field_simps usually does what I want?
On 05/04/14 03:09, Tobias Nipkow wrote:
> I set up field_simps to yield a decision procedure for field equality, provided
> all denominators can be proved to be 0. Hence I am sceptical if adding new rules
> to it is a good idea. Florian, can you give an example where previously
> field_simps was too weak but with the two additional rules it works?
> On 04/04/2014 17:37, Lawrence Paulson wrote:
>> A very good idea, which reduces the impact of the change on existing proofs. I am trying it out now.
>> Seeing no objections, I am quite likely to push this change later today.
>> On 4 Apr 2014, at 15:08, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>>> lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
>>>> lemma divide_minus_right [simp]: "a / - b = - (a / b)”
>>>> It would be a mistake to reorient the simprules, but I am suggesting that they should not be declared as simprules with either orientation.
>>>> lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)"
>>>> lemma divide_minus_right [field_simps]: "a / - b = - (a / b)”
>>> PGP available:
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev