Hi, I'm trying to leverage `fmap`

and create a new type with a restriction, but with this code

```
typedef Assets = "{assets. (∀ t v. fmlookup assets t = Some v ⟶ v > 0)} :: ((Token, nat) fmap) set"
proof
show "fmempty ∈ {assets. (∀ t v. fmlookup assets t = Some v ⟶ v > 0)}"
by auto
qed
setup_lifting type_definition_Assets
```

I have the following error on the last command

```
exception THM 1 raised (line 1872 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))
```

Is it possible to create a typedef of a typedef?

I vaguely remember having had problems myself when trying something like this, and I cannot offer you a direct solution.

That said, it might make sense in your case to define the assets type differently. Spontaneously, I see the following two options:

- Assets are defined as finite maps that map to positive integers (thus excluding 0). This would be the straightforward solution, in my opinion, but it might require you to define the type of positive integers first, which might involve quite a bit of work.
- Assets are defined as those (total) functions from tokens to natural numbers which map only a finite number of tokens to something greater than zero. The idea would be to use
`0`

as representing absence of a mapping. You should then define accessor functions that hide this implementation trick.

By the way, the Isabelle convention is to have type names start with lower case letters.

Last updated: Nov 11 2024 at 01:24 UTC