Hongjian Jiang (Dec 15 2023 at 10:02): Hongjian Jiang (Dec 15 2023 at 10:02):Hi, all. I want to define a boolean algebra in Isabelle's class or locale, where the definition is a tuple (\sigma, a,[|_|], ⊥, ⊤, ⊔, ⊓, c ) where a is a set of predicates and ⊥, ⊤ \in a. The function [|_|] is a denotation: a -> 2^\sigma, like [|⊥|] = \emptyset, [|T|] = \sigma.
I found someone implemented it in Lean like
class Denotation (a : Type u) (\sigma : outParam (Type v)) where
denote : a → \sigma → Bool
So I try to rewrite it in Isabelle, but I found Isaeblle class can not support: Multiple type variables in class specification.
Any helps to define such a structure would be appreciated.
Mathias Fleury (Dec 15 2023 at 10:07):This is a limitation of the type system.
Mathias Fleury (Dec 15 2023 at 10:07):So you need to go to locales like done in HOL-Algebra https://isabelle.in.tum.de/library/HOL/HOL-Algebra/document.pdf
Last updated: Apr 27 2024 at 20:14 UTC