[isabelle-dev] Default simprules for division in fields

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140404/cc37ddf3/attachment.sig>