You can use algebra_simps for everything up to and including rings. Field_simps
is separate because it can rearrange your formula dramatically by multiplying
with all the denominators - you don't always want that.
Tobias
On 07/04/2014 03:11, Thomas Sewell wrote:
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?
Cheers,
Thomas.
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?
Tobias
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.
Larry
On 4 Apr 2014, at 15:08, Florian Haftmann
florian.haftm...@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.
Maybe
lemma divide_minus_left [field_simps]: (-a) / b = - (a / b)
lemma divide_minus_right [field_simps]: a / - b = - (a / b)”
instead?
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
