[isabelle-dev] Default simprules for division in fields

[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 direction, because there are situations where we want to extract the division operator.

It would be a mistake to reorient the simprules, but I am suggesting that they should not be declared as simprules with either orientation. Because only fields are affected, the compatibility issues are relatively minor (and always can be fixed by inserting one of the simprules in the appropriate part of a proof). I played around with this yesterday and managed to build most of the analysis-oriented developments. Now the question is whether to go ahead with this change. I attach a patch.

Larry
-------------- next part --------------
A non-text attachment was scrubbed...
Name: divide_minus_left.patch
Type: application/octet-stream
Size: 16500 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140404/d160408e/attachment-0001.obj>