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: Jun 20 2024 at 12:31 UTC