Re: [isabelle] Datentypen in Isabelle
at the moment, program is just a type abbreviation, not a type constructor.
Hence, you can use all functions on sets for programs, e.g., membership,
subsets, bounded quantification. When you want to restrict the type of programs
to those sets of traces from CP, you have to model program as a type of its own,
i.e., you must define all the set operations you need on the new type. It is up
to you to decide whether this is worth the effort. Here's how you would do it in
inductive_set CP ...
typedef (open) program = "Pow CP" by auto
This defines the new type program. It is inhabited by all sets of traces all of
which are in CP. The function Abs_program constructs from an arbitrary set of
traces the program that inhabits type program, Rep_program unpacks a program
into the set of traces. For sets of traces not all of which are in CP,
Abs_program is unspecified. Since you make assumptions about the sets of traces
that are programs, you cannot define program via datatype.
The new lifting facility might help you in transferring and working with the
Hope this helps,
PS: The rule cp_a_base in CP's definition is redundant, because it is a special
case of cp_a_ind with cp_skip for the premise and simplification for @.
Am 07.11.2012 16:19, schrieb Diego Marmsoler:
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:
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:
CP :: compensable_program
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.
Karlsruher Institut für Technologie
Dr. Andreas Lochbihler
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and