Stream: General

Topic: Exception while using the lifting package

view this post on Zulip Robert Soeldner (Sep 12 2021 at 19:22):

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?

view this post on Zulip Robert Soeldner (Sep 15 2021 at 17:15):

This issue goes away moving from fmap to map.

view this post on Zulip Robert Soeldner (Sep 18 2021 at 19:55):

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 21 2024 at 12:33 UTC