Email Gateway (Nov 28 2020 at 21:29): Email Gateway (Nov 28 2020 at 21:29):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Hope everyone is doing fine, and that this email is not much too long
for the list standards.
I've gathered some minor observations/suggestions concerning the logic
ZF and the ZF-Constructible session. I hope they are of some use to make
the sources more coherent, especially since we are getting closer to RCs
season.
ZF
The names "lepoll_imp_Card_le" and "well_ord_lepoll_imp_Card_le"
seem to be a slight typo, since the relevant term is "cardinal", not
"Card".
I noted that the precedence of some binders that output a set (big
union "UN", big intersection "INT" and "Lamda") is too low to work
well with equality (for instance,
"Z=⋃i∈J. X(i)"
does not parse).
Very early in the development, some alternative names were set for
the definitions of some terms (notably "The", "Image", "If", which
are called "the_def", "image_def", "if_def", resp., instead of the
default capitalized versions). This is a bit misleading. The
associated lemmas are also stated in lower case.
ZF-Constructible
A better name for "separation_closed" would be "Collect_closed" (as
other similar closure lemmas; in this case, it states that the model
M is closed under the term "Collect").
Two nameless lemmas in ZF-Constructible.Formula are declared [simp].
Appropriate names could be "sats_Member_iff" and "sats_Equal_iff".
In the same spirit, I would suggest "obase_exists" -->
"obase_closed" in theory Rank. In the same file, some text comments
refer to undefined terms "oB" and "om" that might be "obase" and
"omap", instead.
One of the main results in Rank.thy (right after well_ord_abs) does
not have a name. It is not quite an "ordertype_abs", because it
doesn't relate the absolute and relative versions of that concept. A
possible name follows from the text comments right before its
statement: "ordertypes_are_absolute". (Incidentally, I have a proof
of a proper "ordertype_abs", but it is not in good shape right now.)
"pred_set_abs" in ZF-Constructible.Wellorderings holds in the weaker
locale M_trans.
The theorem name "L_axioms.range_type" clashes with a similar
"func.range_type". Perhaps it would be better to have
"L_axioms.range_fm_type" (since we are typing the term "range_fm").
However, there are great many theorems that seem to follow the same
naming convention.
Perhaps there is a better name for "Relative.M_trans.nonempty" (like
"M_zero" or "zero_into_M").
I'm including a patch (output of "hg diff") with most of the suggested
changes, except the last items in each list (applying them would have
global consequences in both sessions). The changes seem not to affect
any theory below ZF (builds are all successful).
Best wishes,
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
patch
Email Gateway (Nov 29 2020 at 12:20):From: Makarius <makarius@sketis.net>
The low precedence of binders is commonplace in Isabelle syntax, thus you
often need parentheses around them.
Changing that would probably mess up many things: you can try it out by
changing the analogous syntax in HOL set theory notation and see what happens
in AFP, for example.
Makarius
Email Gateway (Nov 29 2020 at 12:34):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 29/11/20 a las 09:19, Makarius escribió:
As far as I experimented, it seems not to be an issue all of the
Isabelle/ZF sessions bundled with Isabelle (though I didn't check
against the few /other/ ZF entries in the AFP).
But, indeed, I also consider this item to be "low priority" :-).
Email Gateway (Nov 29 2020 at 12:49):From: Makarius <makarius@sketis.net>
This merely means you don't see the problem, because there are very few
applications of Isabelle/ZF.
Makarius
Email Gateway (Nov 30 2020 at 10:32):From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks for your comments. I’m always glad to hear about duplicate and unnecessary hypotheses, and these days we certainly frown upon nameless top-level theorems. On the other hand, it’s well-established in Isabelle that all variable binding constructions should be explicitly bracketed. I will take a look at the other suggestions too. Many thanks again for your interest in Isabelle/ZF!
Larry
Last updated: Jan 04 2025 at 20:18 UTC