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