Re: [isabelle-dev] Default simprules for division in fields

2014-04-06 Thread Thomas Sewell
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

Re: [isabelle-dev] Default simprules for division in fields

2014-04-06 Thread Tobias Nipkow
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

[isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Lawrence Paulson
The theory Fields.thy declares the following simprules: lemma divide_minus_left [simp]: (-a) / b = - (a / b) lemma divide_minus_right [simp]: a / - b = - (a / b)” The idea is that extracting the minus sign yields a good normal form. But it seems that sometimes this works in the opposite

Re: [isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Florian Haftmann
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

Re: [isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Lawrence Paulson
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

Re: [isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Tobias Nipkow
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

Re: [isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Florian Haftmann
Florian, can you give an example where previously field_simps was too weak but with the two additional rules it works? Well, your example seems to indicate that even field_simps is too strong as declaration. Florian Tobias On 04/04/2014 17:37, Lawrence Paulson wrote: A very

Re: [isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Lawrence Paulson
I wasn’t aware of this detail. But for people who use field_simps explicitly, it neutralises the effect of removing those two as default simprules. Larry On 4 Apr 2014, at 17:09, Tobias Nipkow nip...@in.tum.de wrote: Florian, can you give an example where previously field_simps was too weak

Re: [isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Tobias Nipkow
Florian, I was confused and you may well be right: if those two rules are no longer simp rules, it looks like field_simps no longer does its job properly. Most likely they should be added there as you suggested. Tobias On 04/04/2014 16:08, Florian Haftmann wrote: lemma divide_minus_left

Re: [isabelle-dev] Default simprules for division in fields

2014-04-04 Thread Tobias Nipkow
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. I don't think it is a good policy to ask for comments on a change and