[isabelle-dev] Default simprules for division in fields

[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 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.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.
>>>> 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-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev