Customized datatype

Question

I am trying to create a datatype with rules, so to speak, and I am unsure where to start (assuming it is possible!).

For example, I have a datatype, a pair (kind, value) defined as a record. I would like to define another datatype on top of it, a set of such records, with three rules: (1) the set is finite (2) at least one such a record must be in the set (3) only one record of each kind can be in the set

So, if I define them as:

datatype akind = k1 | k2 | k3
record apair =
  kind :: akind
  val :: nat

type_synonym aset = "apair set"

I would like to be able to limit aset such that s1, s2 are not "legal" aset, and s3 is.

define s1 :: aset where "s1 = {}"
define s2 :: aset where "s2 = {(k1, 1), (k1, 2)}
define s3 :: aset where "s3 = {(k1, 1), (k3, 3)}

How can I achieve this? I have definitely hit a block on this one. Thank you in advance!

Answer 1

In Isabelle/HOL, you can derive types from other types with a lot of freedom either by picking subsets of the type or by constructing quotient types. From your description, it sounds like you want to do something like the first, for which there is the typedef command. (This would not be called “datatype” in the Isabelle/HOL sense. “datatypes” are “algebraic data types”, i.e., fancy kinds of (possibly infinitary) trees.)

So, one would start out with an existing type that is a “superset” of what one wants to have. In your instance, I would say, we're talking about partial functions from akind to nat with the requirement that at least one kind is set to a value. (I'll glance over the requirement of finiteness as akind has finitely many members anyways.) So, we'll embed into akind ⇒ (nat option).

Coming up with a set expressing the requirements

One starts out by expressing the type as a set on the base type:

datatype akind = k1 | k2 | k3

definition aset_set :: "(akind ⇒ (nat option)) set" where 
  ‹aset_set ≡ {asg. ∃k. asg k ≠ None}›

We can now check that your first example indeed is not in this set, while the third one is. (And the second one is ruled out by using functions as a base.)

lemma example_no_asg:
  ‹(λk. None)
    ∉ aset_set›
  unfolding aset_set_def by auto

lemma example_asg:
  ‹(λk. case k of
       k1 ⇒ Some 1
     | k3 ⇒ Some 3
     | _ ⇒ None)
    ∈ aset_set›
  unfolding aset_set_def by (simp, meson akind.simps(7))

Deriving a type from a set

The second lemma shows that the set is non-empty. This is the only requirement we need to derive a new type from it. (In HOL, types must be non-empty!)

typedef aset = aset_set
  using example_asg by blast

So, all done! What this does under the hood, is:

• register a new type aset,
• introduce Abs_aset:: (akind ⇒ nat option) ⇒ aset to “cast” functions as type members and
• introduce Rep_aset:: aset ⇒ akind ⇒ nat option to get the function representing the type member.

The pair of abstraction / representation functions is connected via some facts that allow you to go ”in circles” between the two views, as long as you stay within the aset_set we defined, in particular:

• Rep_aset_inverse: Abs_aset (Rep_aset ?x) = ?x
• Abs_aset_inverse: ?y ∈ aset_set ⟹ Rep_aset (Abs_aset ?y) = ?y
• For the others, examine find_theorems Rep_aset!

Working with derived types

We can now come up with the kinds of definitions we want by translating back and forth through Rep_aset / Abs_aset and prove properties through their facts.

For instance, we might want to define a value_of function to obtain the value associated with an akind and an update function to change it. We can prove useful properties on them:

definition value_of :: ‹aset ⇒ akind ⇒ nat option› where
  ‹value_of asg ≡ Rep_aset asg›

definition update :: ‹aset ⇒ akind ⇒ nat ⇒ aset› where
  ‹update asg k n ≡ Abs_aset ((Rep_aset asg)(k := Some n))›

lemma ‹value_of (update asg k v) k = Some v›
  unfolding value_of_def update_def
  by (metis (mono_tags, lifting) Abs_aset_inverse CollectI aset_set_def fun_upd_same option.simps(3))

Why it might not help as much as one wants

The nice thing about types is to rule out bogus “values.“ The Abs/Rep approach means that, whenever they appear, definitions might be meaningless. Nothing stops us from “defining” an unsafe function to remove assignments:

definition undefine :: ‹aset ⇒ akind ⇒ aset› where
  ‹undefine asg k ≡ Abs_aset ((Rep_aset asg)(k := None))› 

Clearly, this definition seems to allow us to construct empty assignments---which we assumed to have ruled out in aset_set! The trick here is that the axiomatization will not allow us to prove the facts we might desire:

lemma ‹value_of (undefine asg k1) k1 = None›
  unfolding value_of_def undefine_def sledgehammer (*no proof found. phew!*) oops

So, one has to keep the “invariants” in mind to come up with definitions that lead to anything nice to be provable.

Alternatives

In general, I recommend to only use typedef as a last resort. Whenever you can express your models directly with existing types (or datatype combinations thereof), your life will be much nicer.

Maybe, the invariant can just be carried around as a fact in the proofs where you really need it?

A middle ground is to use the quotient_type and just make redundant type members equal. For the example, one could start out with non-empty lists of key-value pairs and define an equivalence that only considers the first assignment appearing. However, this post already is getting quite long---so I'll leave it at this side-remark.