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.
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
Thanks! Will try it :)
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
Ah, just defining code_datatype Abs_ValidTimeInterval
did the trick :D
Last updated: Dec 07 2024 at 16:22 UTC