Email Gateway (Aug 19 2022 at 16:53): Email Gateway (Aug 19 2022 at 16:53):From: "W. Douglas Maurer" <maurer@gwu.edu>
I'm having problems using lattices. I know that any powerset is a
lattice, and therefore I ought to be able to use lattice operations
like \<sqinter>. I can certainly use \<inter> (the "cap" operation)
on elements of a powerset; thus I can write lemma rule9: "((C::int
set) \<inter> D) = (D \<inter> C)" by (rule Int_commute) where
\<inter> is replaced by cap. That works. But when I try the same
thing with lattice operations, like this: lemma rule11: "((C::int
set) \<sqinter> D) = (D \<sqinter> C)" by (rule INF_commute) where
\<sqinter> is replaced by the "square cap" operation, I get the
message "Inner lexical error -- Failed to parse prop". What else do I
need in order to get this to work? Thanks! -WDMaurer
Email Gateway (Aug 19 2022 at 16:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Douglas,
the typical infix syntax for lattice operations is no default part of
src/HOL/Main.thy. You can obtain it by importing theory
~~/src/HOL/Library/Lattice_Syntax
Hope this helps.
Florian
signature.asc
Last updated: Apr 20 2024 at 12:26 UTC