Experimenting with different representations and the lifting package, the following code

```
type_synonym 'i graph_rep = "'i fset × 'i fset × ('i,'i) fmap × ('i,'i) fmap"
typedef 'i graph =
"{(nodes, edges, src, trg) :: 'i graph_rep |
nodes edges src trg. fmdom src |⊆| edges ∧ fmran src |⊆| nodes ∧ fmdom trg |⊆| edges ∧ fmran trg |⊆| nodes
}"
apply (rule exI[where x = "(fempty, fempty, fmempty, fmempty)"])
by simp
setup_lifting type_definition_graph
```

produces an unexpected output:

```
exception THM 1 raised (line 1828 of "thm.ML"):
dest_state
Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T) [Quotient R Abs Rep T]
```

Is this a known behavior?

This issue goes away moving from `fmap`

to `map`

.

In general, it looks like `Finite_Maps`

can't be used with subtypes,

```
typedef 'a A = "{a :: ('a,'a) fmap. True}"
by simp
setup_lifting type_definition_A
```

yields the following exception

```
exception THM 1 raised (line 1828 of "thm.ML"):
dest_state
Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T) [Quotient R Abs Rep T]
```

Any idea how to further debug this?

Last updated: Dec 07 2023 at 08:19 UTC