Email Gateway (Apr 11 2024 at 14:55): Email Gateway (Apr 11 2024 at 14:55):From: Tobias Nipkow <nipkow@in.tum.de>
In theory Groups, the followingh pattern is used to define algebraic structures:
class semigroup_add = plus +
assumes add_assoc [algebra_simps, ...]:
"(a + b) + c = a + (b + c)"
begin
...
end
hide_fact add_assoc
Can somebody remind me why add_assoc is hidden? The motivation for this question
is some proof manipulation work where the proof internally contains an instance
of add_assoc (which was obtained via algebra_simps, which is not hidden). But
when creating some proof text, the name Groups.semigroup_add_class.add_assoc
does not work because of the hide_fact:
Inaccessible fact: "Groups.semigroup_add_class.add_assoc"
What should the proof text use to access such a hidden thm (assuming that the
reason for hiding it is valid)? No, algebra_simps(1) is not an option, that name
is not contained in the proof we start from.
Tobias
Email Gateway (Apr 11 2024 at 15:12):From: Manuel Eberl <manuel@pruvisto.org>
I cannot comment on why it is done that way, but the usual way to refer
to this theorem is "add.assoc".
Generally I've been bitten quite a few times by inaccessible facts, so I
try to avoid it these days. The only case where it might potentially
make sense is when you prove a theorem by first proving a strictly more
restrictive version of it first as a lemma. But even there I don't
really hide it usually.
Manuel
Email Gateway (Apr 11 2024 at 17:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Tobias,
In theory Groups, the followingh pattern is used to define algebraic
structures:class semigroup_add = plus +
assumes add_assoc [algebra_simps, ...]:
"(a + b) + c = a + (b + c)"
begin
...
endhide_fact add_assoc
Can somebody remind me why add_assoc is hidden?
as Manuel already indicated, the motivation was to promote the use of
_.assoc etc. and hence establish some kind of »canonicity« for the many
variants that have emerged over time.
The motivation for this
question is some proof manipulation work where the proof internally
contains an instance of add_assoc (which was obtained via algebra_simps,
which is not hidden). But when creating some proof text, the name
Groups.semigroup_add_class.add_assoc does not work because of the
hide_fact:Inaccessible fact: "Groups.semigroup_add_class.add_assoc"
It would be interesting to understand why the machinery prefers the
hidden name and does not come up with add.assoc.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Apr 11 2024 at 18:39):From: Tobias Nipkow <nipkow@in.tum.de>
Florian,
As I wrote, the proof uses a thm from algebra_simps, but in there, the thm has
the hidden name. Thus, if you really want to hide the name, you must make sure
that that version of the thm is completely inaccessible: add.assoc should go
into those named thms like algebra_simps, and similarly for the other hidden
facts in Groups (and elsewhere).
Tobias
Email Gateway (Apr 13 2024 at 07:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Tobias,
see now
https://isabelle.sketis.net/repos/isabelle/rev/5ed992c47cdc
where the »dotted« variants are used in fact collections uniformly.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Apr 15 2024 at 06:53):From: Tobias Nipkow <nipkow@in.tum.de>
Thank you, Florian!
Tobias
Last updated: May 05 2024 at 01:11 UTC