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 2024 at 16:22 UTC