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?
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.