Stream: Beginner Questions

Topic: Attach restriction to type

Hernán Rajchert (Oct 26 2022 at 13:32):

Is there a way to encode a restriction in a type, similar to what a "smart constructor" would do in Haskell/PureScript?

I would like to define a type like this

type_synonym TimeInterval = "POSIXTime × POSIXTime"

A function that may create it

fun createTimeInterval :: "POSIXTime ⇒ POSIXTime ⇒ TimeInterval option" where
  "createTimeInterval l r = (if l ≤ r then Some (l, r) else None)"

and then to carry this restriction, so that I don't have to add it to every lemma

fun validTimeInterval :: "TimeInterval ⇒ bool" where
  "validTimeInterval (l, r) = (l ≤ r)"

theorem inInterval_subset:
  "validTimeInterval a ⟹ inInterval a b = (tToSet a ⊆ bToSet b)"

I have the feeling that I might achieve this with locales, but not sure if this is the intended use case.

Jan van Brügge (Oct 26 2022 at 13:42):

You would do that with a subtype of TimeInterval, using typedef:

typedef ValidTimeInterval = "{ (x, y)::TimeInterval . x <= y }"

Then you can get the underlying type using the Rep_ValidTimeInterval function and the property is in the theorem Rep_ValidTimeInterval

Hernán Rajchert (Oct 26 2022 at 14:16):

Thanks! Will try it :)

Hernán Rajchert (Oct 26 2022 at 17:58):

It worked great in the proofs, now I need to figure out how to export code from it. I'm getting the following error, need to check how to define the code equation

 No code equations for Abs_ValidTimeInterval

Hernán Rajchert (Oct 26 2022 at 18:21):

Ah, just defining code_datatype Abs_ValidTimeInterval did the trick :D

Last updated: Dec 21 2024 at 16:20 UTC