CODEWITHSUNDEEP
abstractionisabelle
Zyzzyva
Zyzzyva

Reputation: 227

Is there an Isabelle equivalent to Haskell newtype?

I want to make a new datatype shaped like an old one, but (unlike using type_synonym) it should be recognized as distinct in other theories.

My motivating example: I'm making a stack datatype out of lists. I don't want my other theories to see my stacks as lists so I can enforce my own simplification rules on it, but the only solution I've found is the following:

datatype 'a stk = S "'a list"

...

primrec index_of' :: "'a list => 'a => nat option"
where "index_of' [] b = None"
    | "index_of' (a # as) b = (
          if b = a then Some 0 
          else case index_of' as b of Some n => Some (Suc n) | None => None)"

primrec index_of :: "'a stk => 'a => nat option"
where "index_of (S as) x = index_of' as x"

...

lemma [simp]: "index_of' del v = Some m ==> m <= n ==> 
                  index_of' (insert_at' del n v) v = Some m"
<proof>

lemma [simp]: "index_of del v = Some m ==> m <= n ==> 
                  index_of (insert_at del n v) v = Some m"
by (induction del, simp)

It works, but it means my stack theory is bloated and filled with way too much redundancy: every function has a second version stripping the constructor off, and every theorem has a second version (for which the proof is always by (induction del, simp), which strikes me as a sign I'm doing too much work somewhere).

Is there anything that would help here?

Upvotes: 1

Views: 195

Answers (1)

Joachim Breitner
Joachim Breitner

Reputation: 25763

You want to use typedef.

The declaration

typedef 'a stack = "{xs :: 'a list. True}" 
  morphisms list_of_stack as_stack
  by auto

introduces a new type, containing all lists, as well as functions between 'a stack and 'a list and a bunch of theorems. Here is selection of them (you can view all using show_theorems after the typedef command):

theorems:
  as_stack_cases: (⋀y. ?x = as_stack y ⟹ y ∈ {xs. True} ⟹ ?P) ⟹ ?P
  as_stack_inject: ?x ∈ {xs. True} ⟹ ?y ∈ {xs. True} ⟹ (as_stack ?x = as_stack ?y) = (?x = ?y)
  as_stack_inverse: ?y ∈ {xs. True} ⟹ list_of_stack (as_stack ?y) = ?y
  list_of_stack: list_of_stack ?x ∈ {xs. True}
  list_of_stack_inject: (list_of_stack ?x = list_of_stack ?y) = (?x = ?y)
  list_of_stack_inverse: as_stack (list_of_stack ?x) = ?x
  type_definition_stack: type_definition list_of_stack as_stack {xs. True}

The ?x ∈ {xs. True} assumptions are quite boring here, but you can specify a subset of all lists there, e.g. if your stacks are never empty, and ensure on the type level that the property holds for all types.

The type_definition_stack theorem is useful in conjunction with the lifting package. After the declaration

setup_lifting type_definition_stack

you can define functions on stacks by giving their definition in terms of lists, and also prove theorems involving stacks by proving their equivalent proposition in terms of lists; much easier than manually juggling with the conversion functions.

Upvotes: 3

Related Questions