Ant S. (Mar 24 2026 at 10:59): Ant S. (Mar 24 2026 at 10:59):I'm trying out a trivial proof as follows (ripped from Midlands Grad School'25): consider a typeclass representing partial orders, total orders, and lattices. It is quite easy to prove that a total order is a lattice i.e. subclass (in total_order) lattice. I already have this proof
Say, I want to show that the ints form a lattice. While auto would just reduce this proof to proving that for any two elements there exists a supremum and an infimum (which is always one of the two elements), I noticed that would be unnecessary. Consider that I prove that the ints form a total order (i.e. interpretation ints_to: total_order "less_eq :: int ⇒ int ⇒ bool"). How can I use the fact that total_order is a subclass of lattice to finish the proof, without having to explicitly write out the sup/inf cases?
Maximilian Schäffeler (Mar 24 2026 at 11:18):You should have fact called ints_to.lattice_axioms at your disposal, right? In this specific case, apply rule/ standard / unfold_locales might also work directly.
Ant S. (Mar 24 2026 at 11:24):Yeah, that's exactly what I was looking for
How do I find all of the theorems generated from an interpretation or a subclass?
Maximilian Schäffeler (Mar 24 2026 at 11:37):You can add the command print_theorems after other commands in your theory file and check which theorems were produced. It might be insightful to also check after function or datatype definitions.
Ant S. (Mar 24 2026 at 11:38):this is exactly what I needed, thanks!
Last updated: Mar 25 2026 at 02:29 UTC