Email Gateway (Aug 19 2022 at 14:02): Email Gateway (Aug 19 2022 at 14:02):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
I am interested in a construction of the following structure:
type_synonym 'a trace = "nat => 'a"
type_synonym 'a A= "'a trace => bool"
type_synonym 'a 'b B= "'a trace => 'b trace => bool"
type_synonym 'a 'b 'c C= "'a trace => 'b trace => 'c trace => bool"
class myoperator =
fixes myop:: "'a => 'a"
I would like to get an instantiation for myoperator class
for the types ('a A), ('a 'b B), and ('a 'b 'c C), and to define
myop in all these cases.
More abstractly, I could also manage with using
'a::order instead of 'a trace.
So I would like to be able to define myop for
'a::order => bool
'a::order => 'b::order => bool
'a::order => 'b::order => 'c::order => bool
Best regards,
Viorel Preoteasa
Email Gateway (Aug 19 2022 at 14:02):From: Johannes Hölzl <hoelzl@in.tum.de>
If you use typedef instead of type_synonym you can instantiate the
myoperator type class. Then lift_definition + transfer could help you
translate the theorems on myop to theorems on functions.
Email Gateway (Aug 19 2022 at 14:02):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
I guess that you suggest to define
typedef 'a A= "{x :: 'a trace => bool . True}"
instantiation "A":: (type) myoperator
and then define myop on predicates via the bijection given by typedef.
With this approach I end up with 3 different names for functions
on 'a A, 'a 'b B, and 'a 'b 'c C.
I could define these functions right from the beginning because I do
not have theorems in myoperator. I just need a mechanism to have the
same symbol for all these functions.
Viorel
Email Gateway (Aug 19 2022 at 14:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Viorel,
If you do not care about the type system checks for type classes that Isabelle provides,
you can just use overloaded definitions, because your types A, B, and C do not overlap.
The most primitive form would be the following (where myop on A and C is the identity and
on B the negation).
consts myop :: "'a => 'a"
defs (overloaded) myop_A_def: "myop == %P :: 'a A. P"
defs (overloaded) myop_B_def: "myop == %P :: ('a, 'b) B. %s t. ~ P s t"
defs (overloaded) myop_C_def: "myop == %P :: ('a, 'b, 'c) C. P"
Note however that Isabelle does not enforce that myop is used only on defined types. For
example, "myop (3 :: int)" also type-checks.
If you want to use more advanced definition facilities (definition/function/...), you
should have a look at "context overloading ... begin" context blocks.
Best,
Andreas
Email Gateway (Aug 19 2022 at 14:06):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This is indeed preferred over low-level defs (overloaded).
Florian
signature.asc
Email Gateway (Aug 19 2022 at 14:18):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hi Andreas,
Thank you for your message.
On 03/24/2014 10:52 AM, Andreas Lochbihler wrote:
Hi Viorel,
If you do not care about the type system checks for type classes that
Isabelle provides, you can just use overloaded definitions, because
your types A, B, and C do not overlap. The most primitive form would
be the following (where myop on A and C is the identity and on B the
negation).consts myop :: "'a => 'a"
defs (overloaded) myop_A_def: "myop == %P :: 'a A. P"
defs (overloaded) myop_B_def: "myop == %P :: ('a, 'b) B. %s t. ~ P s t"
defs (overloaded) myop_C_def: "myop == %P :: ('a, 'b, 'c) C. P"Note however that Isabelle does not enforce that myop is used only on
defined types. For example, "myop (3 :: int)" also type-checks.
This is close to what I wanted, but I did not realize that this
will have a price. It is no longer possible to have the type inferred
from myop. If the class mechanism would work, then I could
axiomatize the properties of myop in the class.
If you want to use more advanced definition facilities
(definition/function/...), you should have a look at "context
overloading ... begin" context blocks.
Where can I find more information and examples about this mechanism?
Best regards,
Viorel
Best,
AndreasOn 19/03/14 17:25, Viorel Preoteasa wrote:
On 3/19/2014 3:55 PM, Johannes Hölzl wrote:
Am Mittwoch, den 19.03.2014, 14:58 +0200 schrieb Viorel Preoteasa:
I am interested in a construction of the following structure:
type_synonym 'a trace = "nat => 'a"
type_synonym 'a A= "'a trace => bool"
type_synonym 'a 'b B= "'a trace => 'b trace => bool"
type_synonym 'a 'b 'c C= "'a trace => 'b trace => 'c trace => bool"class myoperator =
fixes myop:: "'a => 'a"I would like to get an instantiation for myoperator class
for the types ('a A), ('a 'b B), and ('a 'b 'c C), and to define
myop in all these cases.More abstractly, I could also manage with using
'a::order instead of 'a trace.So I would like to be able to define myop for
'a::order => bool
'a::order => 'b::order => bool
'a::order => 'b::order => 'c::order => bool
If you use typedef instead of type_synonym you can instantiate the
myoperator type class. Then lift_definition + transfer could help you
translate the theorems on myop to theorems on functions.
I guess that you suggest to definetypedef 'a A= "{x :: 'a trace => bool . True}"
instantiation "A":: (type) myoperatorand then define myop on predicates via the bijection given by typedef.
With this approach I end up with 3 different names for functions
on 'a A, 'a 'b B, and 'a 'b 'c C.I could define these functions right from the beginning because I do
not have theorems in myoperator. I just need a mechanism to have the
same symbol for all these functions.Viorel
Email Gateway (Aug 19 2022 at 14:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Viorel,
The overloading target is documented in the isar-ref manual in section 5.8. It also works
without "context".
There are a number of examples usages in the HOL sources, e.g., in ~~/src/HOL/Nat and
~~/src/HOL/Algebra/Groups. Here's another example:
overloading
myop_A == "myop :: 'a A"
begin
definition myop_A :: "'a A" where "myop_A P = P"
end
Best,
Andreas
Last updated: May 06 2024 at 12:29 UTC