# [isabelle] Datentypen in Isabelle

Hi,
I’ve a question regarding Datatypes in Isabelle/HOL. I want to define a new Datatype which is modeled as a set of tupels of traces where a trace is a list of some basic actions:
typedecl actions
type_synonym trace = "(actions list) × (actions list)"
type_synonym program = "trace set"
However I need to restrict the structure of the list: The list of action elements have to obey some constraints in order to be of type trace.
At the moment I define a normal set to state the constraints of a trace and all my theorems are stated with “P” of type “program” and include a separate assumption “P <= CP” in order
to make use of some properties elicited by the set CP. The set CP is defined as follows:
inductive_set
CP :: compensable_program
where
cp_skip: "([], []) ∈ CP" |
cp_error: "([!], []) ∈ CP" |
cp_a_base: "([Some a], [Some (inverse a)]) ∈ CP" |
cp_a_ind: "(p, pi) ∈ CP ⟹ (Some a # p, pi @ [Some (inverse a)]) ∈ CP"
This works fine, however it would be much nicer if I could define a Datatype CP instead of using the set CP. Hence I could state all the theorems simply as “P” of type “CP” without the assumption that “P” is a subset of CP.
Best,
Diego

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*