[isabelle-dev] Default simprules for division in fields

[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 then say
that you will push it half a day later. I for one am not convinced by the
utility of the change.

1. Your changeset shows quite a number of proofs where the rules need to be
added by hand but in all of HOL there is only one proof where divide_minus_left
is removed. Hence the current setup seems to work not that badly.

2. I see little difference between a normal form where "/" is pulled out and one
where "-" is. You may have to deal with one more case if "-" is pulled out. But
can you give an example where pulling "/" out is a big win over "-"?

Tobias

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