Email Gateway (Aug 19 2022 at 09:18): Email Gateway (Aug 19 2022 at 09:18):From: Diego Marmsoler <marmsoler_diego@yahoo.it>
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
Email Gateway (Aug 19 2022 at 09:18):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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 @.
Last updated: Apr 26 2024 at 01:06 UTC