*To*: Diego Marmsoler <marmsoler_diego at yahoo.it>*Subject*: Re: [isabelle] Datentypen in Isabelle*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 07 Nov 2012 16:57:39 +0100*Cc*: Isabelle <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <000201cdbcfb$4eb28d30$ec17a790$@yahoo.it>*References*: <000201cdbcfb$4eb28d30$ec17a790$@yahoo.it>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Dear Diego,

inductive_set CP ... typedef (open) program = "Pow CP" by auto

Hope this helps, Andreas

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

**References**:**[isabelle] Datentypen in Isabelle***From:*Diego Marmsoler

- Previous by Date: [isabelle] Datentypen in Isabelle
- Next by Date: [isabelle] New AFP entry: The independence of Tarski's Euclidean axiom
- Previous by Thread: [isabelle] Datentypen in Isabelle
- Next by Thread: [isabelle] New AFP entry: The independence of Tarski's Euclidean axiom
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list