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"]*)
  thm "Groups.semigroup_add.add_assoc"
  thm "Groups.semigroup_add_class.add_assoc"

All of those take me to

 line 152:
class semigroup_add = plus +
assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"

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:

line 156:
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 MHonArc.