Re: [isabelle] Isabelle2014-RC0: add_assoc hidden, causes error, but proof passes
On 14-07-11 07:45, Florian Haftmann wrote:
There's "Groups.semigroup_add.add_assoc", followed in Groups.thy by
"hide_fact add_assoc". The "hide_fact" is new in Groups.thy and causes
an error in a proof.
this is a misunderstanding. The canonical name for associativity of
plus is now add.assoc, cf. NEWS.
The add_assoc you have stumbled over is just a device to bootstrap the
locale / type class hierarchy.
This shows cntl-clicking has its limitation as an educational tool,
where some of what I say here doesn't exactly fit anything, because I'm
talking about both the pre-RC0 install I have, and the 2014-RC0 install.
But, with this pre-RC0 Isabelle, I have these:
thm "add_assoc" (*[name "Groups.semigroup_add_class.add_assoc"]*)
All of those take me to
class semigroup_add = plus +
assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b
After doing a lot of grepping to find where the "add" of "add.assoc" is
defined, I finally decided it had to be the following, since it doesn't
show up anywhere else:
sublocale add!: semigroup plus
by default (fact add_assoc)
I could say it's obvious now, but it's not because I've read nothing
that tells me that "add!" defines "add" of "add.assoc". So, what's in
NEWS about "add.assoc" wouldn't have meant anything to me without a
little help about this.
Anyway, I kind of understanding the use of class with class, and that
class is a locale, and the use of locale with locale, but I haven't
understood the mixing of "locale" with "class" in Groups.thy, so if I
get a chance to work through Groups.thy, it could be I'll understand it
better with this knowledge.
This archive was generated by a fusion of
Pipermail (Mailman edition) and