Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Exception using setup_lifting

view this post on Zulip Email Gateway (Sep 15 2021 at 08:14):

From: Robert Soeldner via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hello,

I'm currently exploring several graph representations and encountered an
unexpected exception using 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 the 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]

Would be great to receive some comments and potential suggestions on how to
overcome this issue.

Thank you in advance,
Robert

Last updated: Jan 04 2025 at 20:18 UTC