Email Gateway (Aug 22 2022 at 19:26): Email Gateway (Aug 22 2022 at 19:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
in the context of
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-March/msg00017.html
(Conflicting rules in default simps vs. algebraic rule collections) I
revisited existing *_simps collections particulary in the HOL theories,
with the following insights:
Collections mult_compare_simps and unit_simps seem to be never used
neither in the distro nor the AFP and hence I would suggest to remove them.
There is the well-established chain ac_simps ⊆ algebra_simps ⊆
field_simps, which is also referenced in tutorials:
There are two somehow irregular variants:
divide_simps with more aggressive rewrites than field_simps wrt.
case distinctions
sign_simps introducing potential case splits on signs; this is
indeed quite old stuff dating back to at least 2f4be6844f7c in 2007,
which seems to have escaped any modernization or systematization so far,
but is used in a couple of places.
The rules in both these surely have their purpose, and it would be a
good idea to make them available more prominently.
So far my current thoughts on that:
a) The traditional chain is extended: ac_simps ⊆ algebra_simps ⊆
field_simps ⊆ field_split_simps, where field_split_simps adds the
potential case-splitting rules now in divide_simps and sign_simps.
b) I am a little bit uncomfortable with the well-established name
field_simps, though:
* Most of its rules do not apply to fields but to the weaker
division_ring (which does not sound so odd for German speakers used to
think about »Körper« and »Schiefkörper«).
* My original motivation was to find a collection to store some rules
about (partial) division in rings, and it is somehow strange that the
formally fitting collection is named after fields.
Hence suggestions for a better naming for field_simps and
field_split_simps are welcome.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
After a second study, I recognized that the whole story is a little bit
more involved.
Concerning ac_simps ⊆ algebra_simps ⊆ field_simps – this inclusion does
just not hold:
a) ac_simps contains all kind of AC-rules (coprime, min, max, inf, sup,
…), but algebra_simps only those for + and *.
b) field_simps is no superset of algebra_simps, and in some sense they
work against each other:
algebra_simps: (a + b) * c = a * c + b * c
but not: (a + b) / c = a / c + b / c
field_simps: a / c + b / c = (a + b) / c
It will need some further rounds of thinking to understand where to go
from here.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
After a third study and conversation with Tobias and Fabian, the
situation presents itself as follows:
a) algebra_simps and field_simps are deliberately designed to provide
some kind of decision procedure based on simp rules and ought stay »as
they are« both in naming and content.
b) Currently, sign_simps is an ad-hoc collection consisting of
algebra_simps plus
lemma zero_less_mult_iff [sign_simps]:
"0 < a * b ⟷ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0"
lemma mult_less_0_iff [sign_simps]:
"a * b < 0 ⟷ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b"
c) An intermediate post-release step is to turn sign_simps into a proper
collection consisting solely of
lemma zero_less_mult_iff [sign_simps]:
"0 < a * b ⟷ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0"
lemma mult_less_0_iff [sign_simps]:
"a * b < 0 ⟷ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b"
and also
lemma zero_le_mult_iff [sign_simps]:
"0 ≤ a * b ⟷ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0"
lemma mult_le_0_iff [sign_simps]:
"a * b ≤ 0 ⟷ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b"
d) The specific property of sign_simps and divide_simps is that goals
may be split. Maybe this can be developed into a schema where each
algebra_simps and field_simps are accompanied by splitting variants,
making sign_simps and divide_simp. This needs to be discussed.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:42):From: Lawrence Paulson <lp15@cam.ac.uk>
The purpose of divide_simps is to eliminate division from arithmetic expressions in equations and inequalities. I introduced it in order to simplify the results of differentiation but it seems to have many other applications.
Larry
Email Gateway (Aug 22 2022 at 19:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
the following tableaux shows that each rule in divide_simps corresponds
to one or two rules from field_simps; the key difference is that rules
in field_simps do not split goals whereas divide_simps does.
thm divide_simps(1) field_simps(21)
thm divide_simps(2) field_simps(26)
thm divide_simps(3) field_simps(27)
thm divide_simps(4) field_simps(29)
thm divide_simps(5) field_simps(28)
thm divide_simps(6) field_simps(30)
thm divide_simps(7) field_simps(31)
thm divide_simps(8) field_simps(23)
thm divide_simps(9) field_simps(22)
thm divide_simps(10) field_simps(24)
thm divide_simps(11) field_simps(25)
thm divide_simps(12) field_simps(32) field_simps(35)
thm divide_simps(13) field_simps(36) field_simps(38)
thm divide_simps(14) field_simps(33) field_simps(34)
thm divide_simps(15) field_simps(37) field_simps(39)
thm divide_simps(16) field_simps(40) field_simps(41)
thm divide_simps(17) field_simps(46) field_simps(47)
thm divide_simps(18) field_simps(42) field_simps(43)
thm divide_simps(19) field_simps(44) field_simps(45)
Hence I am still in favour to arrange everything as follows
| conservative | splitting
for rings | algebra_simps | algebra_split_simps
for fields | field_simps | field_split_simps
where field_split_simps would be the successor of divide_simps, and
sign_simps be obsolete.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:59):From: Tobias Nipkow <nipkow@in.tum.de>
I support this change because the new names reflect the relationship to the
popular algebra_simps and field_simps and indicate that splitting may happen.
Tobias
smime.p7s
Last updated: Apr 25 2024 at 08:20 UTC