Re: [isabelle] Datentypen in Isabelle



Dear Diego,

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 Isabelle2012:

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 type program.

Hope this helps,
Andreas

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:
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


--
Karlsruher Institut für Technologie
IPD Snelting

Dr. Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
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 MHonArc.