Use an equivalence relation to insantiate a class · Beginner Questions

Similar to my previous question, I have a Value datatype and an evalValue :: Environment => State => Value => int function.

I'm trying to instantiate the semigroup_add class for Value, but of course this is not true

Can I use valueEquiv and semigroup_add_value_equiv defined below to instantiate the semigroup_add class?

instantiation Value :: zero
begin
definition "zero_Value = Constant 0"
instance ..
end

instantiation Value :: one
begin
definition "one_Value = Constant 1"
instance ..
end

instantiation Value :: plus
begin

definition "plus_Value a b = AddValue a b"

instance ..
end

definition valueEquiv :: "Value ⇒ Value ⇒ bool" (infix ‹≡⇩v› 50) where
  "(a ≡⇩v b) ⟷  (∀env st. evalValue env st a = evalValue env st b)"

lemma semigroup_add_value_equiv : "a + b + c ≡⇩v a + (b + c)"
  by (simp add: valueEquiv_def plus_Value_def)


instantiation Value :: semigroup_add
begin
instance proof
  fix a b c :: Value
  show "(a + b) + c = a + (b + c)"
    (* Can I use the equivalence rule to solve this? *)
qed
end

Christian Pardillo Laursen (Feb 27 2023 at 09:56):

You might want to consider defining your Value type as a quotient type on the equivalence relation you give. This would give you the properties you desire from your type, abstracting away implementation details of how Values are stored.

Wolfgang Jeltsch (Feb 27 2023 at 13:53):

I was going to say the same. However, I think @Hernán Rajchert is interested in code extraction. How does code extraction work for quotient types? Is it possible to (easily) extract code that works with the underlying representations?

Hernán Rajchert (Feb 27 2023 at 15:00):

My knowledge of quotient types is limited, and I think it might make more sense for the AssocMap (in the previous question) than the Value type.

My idea of adding semigroup_add to Value was because I wanted to overload the numeral class (and also the arithmetic functions) to have a nicer syntax when I write my language expression in Isabelle. With the help of some abbreviations I was able to achieve the following syntax

abbreviation const :: "int ⇒ Value" (‹_⇩c› [1000] 1000)  where
  "(n)⇩c ≡ Constant n"

abbreviation addValue :: "[Value, Value] ⇒ Value" (infixl ‹+⇩v› 65)  where
  "a +⇩v b ≡ AddValue a b"

abbreviation subValue :: "[Value, Value] ⇒ Value" (infixl ‹-⇩v› 65)  where
  "a -⇩v b ≡ SubValue a b"

abbreviation mulValue :: "[Value, Value] ⇒ Value" (infixl ‹⋆⇩v› 70)  where
  "a ⋆⇩v b ≡ MulValue a b"

abbreviation divValue :: "Value ⇒ Value ⇒ Value" (infixl "(÷⇩v)" 70)  where
  "a ÷⇩v b ≡ DivValue a b"

abbreviation condValue :: "Observation ⇒ Value ⇒ Value ⇒ Value" (‹_ ?⇩v _ : _› [1000, 1000, 1000] 700) where
  "c ?⇩v t : f ≡ Cond c t f"

definition "v1 = Constant 3 +⇩v Constant 2"
definition "v2 = Constant 3 +⇩v Constant 2"
definition "v3 = 4⇩c -⇩v Constant 3"
definition "v4 = 4⇩c -⇩v 3⇩c"
definition "v5 = 6⇩c ÷⇩v 2⇩c"
definition "v6 = 6⇩c +⇩v 4⇩c ÷⇩v 2⇩c"
definition "v7 = (6⇩c +⇩v 4⇩c) ÷⇩v 2⇩c"
definition "v8 = TrueObs ?⇩v 4⇩c : 6⇩c"
definition "v9 = FalseObs ?⇩v 4⇩c : 6⇩c"
definition "v10 = TrueObs ?⇩v (4⇩c +⇩v 32⇩c) : 6⇩c"
definition "v11 = FalseObs ?⇩v (4⇩c +⇩v 2⇩c) : 6⇩c ⋆⇩v 2⇩c"

If I could define numeral, plus, minus,times and divide/inverse then I wouldn't need the abbreviations.

Note that Value and Observation are mutual recursive and so are evalValue and evalObservation. This raises three questions:

Wolfgang Jeltsch (Feb 27 2023 at 15:13):

At least for order relations there is a base class that contains only the relevant methods, like (<), but not properties. Maybe something like that also exists for (+). You may want to trace the superclass chains that start from semigroup_add back to the superclasses.

Wolfgang Jeltsch (Feb 27 2023 at 15:16):

You always define a quotient type based on a representation type, like you do for subtypes. If only your representation types are defined by multiple recursion, you’re fine.

Hernán Rajchert (Feb 27 2023 at 15:35):

Yes, the plus, minus and times could offer me the (+), (-) and (*) syntax override. The divide class offers me an infix div and the inverse_divide offers me / (which I don't think applies here because my Constant's are ints, so I cannot offer an inverse)

Maybe as a compromise, I can define the classes that doesn't involve properties for their syntax, use the sub_c abbreviation for Constants, and then have equivalence relations instead of equality relations. But this means I could never use the semigroup_add class, at most I could use the semigroup locale with an f that uses evalValue. Not sure if this would be useful or if it just complicates things.

Wolfgang Jeltsch (Feb 27 2023 at 16:01):

When just specifying, I would always opt for quotient types, I think. If quotient types work well with code extraction, I’d go for it also here, I guess. I haven’t looked at the details of your code, though.

Stream: Beginner Questions

Topic: Use an equivalence relation to insantiate a class