Stream: Beginner Questions

Topic: Is it possible to create a typedef of a typedef?

Hernán Rajchert (Mar 09 2023 at 04:26):

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?

Wolfgang Jeltsch (Jun 04 2023 at 23:08):

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: Apr 25 2024 at 01:08 UTC