Email Gateway (Aug 18 2022 at 15:24): Email Gateway (Aug 18 2022 at 15:24):From: Liam O'Reilly <Isabelle@liamoreilly.me.uk>
Hi,
I have recently migrated to Isabelle 2009. I have a Haskell code base that
produces Isabelle code automatically, however it does not produce Isar code.
Since the migration to Isabelle 2009, my instantiation of the Quotient class
does not work, where it used to work in 2008.
Could someone please help me with the code below and show me the new correct
syntax in plain Isabelle. Once this goes through then I will be able to
apply the same syntax to my Haskell code base (currently migrating the
codebase to Isar is far too much work and I don't have the time).
The error I get is on the defs line. The error is:
*** Clash of specifications "test.myType_sim_def" and
"test.eqv_MyType_inst.eqv_MyType_def" for constant "Quotient.eqv_class.eqv"
*** The error(s) above occurred in definition "myType_sim_def":
*** "x ~ y == eq x y"
*** At command "defs".
Any help will be most appreciated.
Thanks
Liam
The sample file I am working with is
theory test
imports Main "Quotient"
begin
datatype MyType = A | B
consts
eq :: "MyType => MyType => bool"
primrec "eq A y = (y = A)"
"eq B y = (y = B)"
instance MyType:: eqv
by (intro_classes)
defs (overloaded)
myType_sim_def : "eqv x y == (eq x y)"
instance MyType:: equiv
apply (intro_classes)
apply (unfold myType_sim_def)
apply (auto)
done
end
Email Gateway (Aug 18 2022 at 15:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Liam,
I have recently migrated to Isabelle 2009. I have a Haskell code base that
produces Isabelle code automatically, however it does not produce Isar code.
just a correction of terminology: you are producing Isar code, just
one which is not suitable for Isabelle 2009 any longer.
instance MyType:: eqv
by (intro_classes)defs (overloaded)
myType_sim_def : "eqv x y == (eq x y)"instance MyType:: equiv
apply (intro_classes)
apply (unfold myType_sim_def)
apply (auto)
done
You would translate this as follows (*):
instantiation MyType :: eqv
begin
definition
myType_sim_def: "(eqv :: MyType => MyType => bool) = (eq x y)"
instance by intro_classes
end
instance MyType :: equiv
apply (intro_classes)
apply (unfold myType_sim_def)
apply (auto)
done
Note that the type inside the definition is necessary in some situations
for disambiguation.
With the new infrastructure, you can also abolish the class eqv, putting
both operations and specifications in the same class (*):
class equiv =
fixes eqv :: "'a => 'a => bool"
assumes <whatever>
instantiation MyType :: equiv
begin
definition
myType_sim_def: "(eqv :: MyType => MyType => bool) = (eq x y)"
instance MyType :: equiv
apply (intro_classes)
apply (unfold myType_sim_def)
apply (auto)
done
Hope this helps,
Florian
(*) this text is not checked for typos
signature.asc
Email Gateway (Aug 18 2022 at 15:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Liam,
Thanks. That was exactly what I needed. I just could not work out or
find the correct syntax.
you can find syntax diagrams in the Isar reference manual. For type
classes there is also a dedicated tutorial.
Cheers,
Florian
signature.asc
Last updated: Apr 26 2024 at 16:20 UTC