[isabelle-dev] Default simprules for division in fields

[Tobias Nipkow]

On 04/04/2014 18:10, Florian Haftmann wrote:
>> 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.

Which example? I didn't give one...

Tobias

> Florian
> 
>> 
>> 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
>>
>