Email Gateway (Aug 19 2022 at 16:14): Email Gateway (Aug 19 2022 at 16:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Clemens,
sorry for the delay.
On 16.10.2014 18:57, Clemens Ballarin wrote:
permanent_interpretation prefix: expr
where f = tWhat if expr contains where clauses? Sublocale distinguishes this (awkwardly) by slightly different syntax: "where" <term> "=" <term> within the expression vs. "where" <term> for the rewrite morphism.
This was my fault. The syntax (cf.
src/Tools/permanent_interpretation.ML) is
permanent_interpretation expr …
defining …
where …
permanent_interpretation prefix: expr
-- ‹with implicit mixin: f_def [symmetric]›This, I guess, refers to the original sublocale command, right?
In a locale context, yes.
I wonder whether we can come up with a syntax that permits both rewrite morphisms and definitions. Obviously one of the two kinds of equations would have to be turned around. Probably it would be more intuitive to reverse the notation of the rewrite morphisms.
Currently, definitions are orientated the other way round than bare
equations. Not sure what would fit best here.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:17):From: Jose Divasón <jose.divasonm@unirioja.es>
Dear all,
I was trying to demonstrate that any field is a euclidean (semi)ring. I
can't do it by means of subclasses, because they have different fixed
parameters:
class field = comm_ring_1 + inverse +
assumes field_inverse: "a ≠ 0 ⟹ inverse a * a = 1"
assumes field_divide_inverse: "a / b = a * inverse b"
class euclidean_semiring = semiring_div +
fixes euclidean_size :: "'a ⇒ nat"
fixes normalisation_factor :: "'a ⇒ 'a"
assumes .....
(subclass (in field) euclidean_ring)
So, I did it using sublocales (see the attached file).
sublocale field ⊆ field_is_euclidean_ring: euclidean_ring _ "λa b. if b = 0
then 0 else a/b" "λa b. if b = 0 then a else 0" _ _ _ "λi. if i = 0 then
0 else 1::nat" id
My problem is that, before such a sublocale I can execute functions defined
in the euclidean_ring class (such as gcd_eucl for naturals and integers).
On the contrary, after the sublocale those functions can't be executed
anymore. Maybe I'm not understanding properly how sublocales work.
The use of sublocales (and then, my problem) can be avoided creating a new
class fixing (and defining) the parameters presented in the euclidean_ring
class:
class field_euclidean = field + euclidean_ring +
assumes "euclidean_size = (λi. if i = 0 then 0 else 1::nat)"
and "normalisation_factor = id"
Nevertheless this is a bit unsatisfactory, because a new class has to be
introduced and I should instantiate each field to this new field_euclidean
class (although instances would be quite easy).
In the attached file there is my Isabelle theory (Foo.thy) with further
explanations.
Can this proof be done using sublocales without the loss of executability?
All suggestions are welcome.
Thanks,
Jose
Foo.zip
Email Gateway (Aug 19 2022 at 16:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jose,
So, I did it using sublocales (see the attached file).
you approach in principle is right.
The complications you encounter are due to the fact that the code
generator only accepts equations headed by logical constants (for
purpose of simple foundation) but syntactical constants stemming from
interpretations after definitions in locales are usually syntactic
abbreviations.
Find the solution in the attached theory.
In short steps:
Import "~~/src/Tools/Permanent_Interpretation" (this will later allow
to resolve the constant / abbreviation issue with minimal effort).
sublocale a ⊆ E is equivalent to context a begin … sublocale E … end
Substitute sublocale p: F by permanent_interpretation p?: F (logically
equivalent, but note the subtle change in semantics of prefixes, see below)
Note that locale expressions support also named instantiation rather
than positional one, which is superior in presence of many parameters
(see below – this is not required, but makes more clear whats going on)
Currently we are at
permanent_interpretation field_is_euclidean_ring?: euclidean_ring
where div = "λa b. if b = 0 then 0 else a/b"
and mod = "λa b. if b = 0 then a else 0"
and euclidean_size = "λi. if i = 0 then 0 else 1::nat"
and normalisation_factor = id
defining gcd_eucl = gcd_eucl
which essentially makes an appropriate constant definition and provides
a suitable mixin equation for the interpretation such that theorems are
properly folded.
That's it in the first instance.
Note that the unexpected »real« type is due to an implicit coercion.
I usually recommend to make interpretation prefixes mandatory (ie.
dropping the »?«).
Hope this helps,
Florian
Foo.thy
signature.asc
Email Gateway (Aug 19 2022 at 16:17):From: Clemens Ballarin <ballarin@in.tum.de>
It might be helpful to explain what permanent_interpretation does in terms a sublocale declaration and definitions.
Clemens
Email Gateway (Aug 19 2022 at 16:17):From: Jose Divasón <jose.divasonm@unirioja.es>
Thank you for the useful response.
Is there any feasible way to avoid that implicit coercion?
As far as I know, using permanent_interpretation gcd_eucl is now executable
but only over fields. Am I right?
I mean:
value "gcd_eucl (13::nat) (6::nat)"
Computes "field_class.gcd_eucl (real 13) (real 6)", which is unsatisfactory
for my purposes, because the gcd_eucl over reals is not the same as the
gcd_eucl over int or nat. I guess that now "euclidean_semiring.gcd_eucl"
has been hidden by the permanent_interpretation.
Thanks,
Jose
Email Gateway (Aug 19 2022 at 16:19):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jose,
Is there any feasible way to avoid that implicit coercion?
you can deactivate it using
declare [[coercion_enabled = false]]
to eliminate a potential source of confusion.
Computes "field_class.gcd_eucl (real 13) (real 6)", which is
unsatisfactory
for my purposes, because the gcd_eucl over reals is not the same as the
gcd_eucl over int or nat. I guess that now "euclidean_semiring.gcd_eucl"
has been hidden by the permanent_interpretation.
This is only a matter of name space. You may use
declare [[names_long]]
to have names always printed qualified, this might help in identifying
things which might have been shadowed.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:19):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
It might be helpful to explain what permanent_interpretation does in terms a sublocale declaration and definitions.
This is one item of my documentation dept.
Here a rough sketch:
permanent_interpretation prefix: expr
where f = t
One key property is that »t« is parsed in the (approximate) syntactic
context of expr (like mixin equations also). Let »t'« denote the
internalized term. Then we have:
definition
f_def: "f = t'"
permanent_interpretation prefix: expr
-- ‹with implicit mixin: f_def [symmetric]›
Note that the symmetric of f_def is directly integrated as mixin
equation into the resulting mixin morphisms – there is so separate proof
obligation.
That's it, in short words.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:20):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Florian,
Thanks for the feedback. Here are two quick questions:
permanent_interpretation prefix: expr
where f = t
What if expr contains where clauses? Sublocale distinguishes this (awkwardly) by slightly different syntax: "where" <term> "=" <term> within the expression vs. "where" <term> for the rewrite morphism.
One key property is that »t« is parsed in the (approximate) syntactic
context of expr (like mixin equations also). Let »t'« denote the
internalized term. Then we have:definition
f_def: "f = t'"permanent_interpretation prefix: expr
-- ‹with implicit mixin: f_def [symmetric]›
This, I guess, refers to the original sublocale command, right?
I wonder whether we can come up with a syntax that permits both rewrite morphisms and definitions. Obviously one of the two kinds of equations would have to be turned around. Probably it would be more intuitive to reverse the notation of the rewrite morphisms.
Clemens
Email Gateway (Aug 19 2022 at 16:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Clemens,
I like your idea of using more descriptive keywords here. Following
your suggestion, 'where' could be called 'unfolding' and replaced by
'folding' if we decide to turn the rewrite equations around. However,
the ing form tends to be used by the proof language for transformations
of the proof state, and 'unfolding' would even make the grammar
ambiguous. It will probably make more sense to settle for 'defines',
'unfolds' and 'folds'.
I agree in principle, but I am still uncertain what the preferred
orientation for mixin equations should be, except that there should only
be one orientation.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:33):From: Clemens Ballarin <ballarin@in.tum.de>
Well, I'm not sure. It really is a matter of fast whether you want to see them as rewrite rules or (pseudo-)definitions. I agree that it might be confusing, but I don't see that having both would be technically more difficult than having only 'folds'.
Clemens
Email Gateway (Aug 19 2022 at 16:35):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Florian,
I like your idea of using more descriptive keywords here. Following your suggestion, 'where' could be called 'unfolding' and replaced by 'folding' if we decide to turn the rewrite equations around. However, the ing form tends to be used by the proof language for transformations of the proof state, and 'unfolding' would even make the grammar ambiguous. It will probably make more sense to settle for 'defines', 'unfolds' and 'folds'.
Clemens
Email Gateway (Aug 19 2022 at 16:35):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Surely, there would not be any technical difficulty.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Clemens,
see now http://isabelle.in.tum.de/reports/Isabelle/rev/16d92d37a8a1 for
documentation stubs on permanent_interpretation.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:39):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Florian,
in the documentation, please note that the term 'mixing' needs explaining. My documentation only refers to rewrite morphisms not mixin equations. I use mixin only in the source code (but user don't normally read that).
Is there really a need for a new command? Wouldn't it make more sense to integrate the new functionality with 'interpretation' and 'sublocale'.
Clemens
Email Gateway (Aug 19 2022 at 16:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Clemens,
in the documentation, please note that the term 'mixing' needs
explaining. My documentation only refers to rewrite morphisms not mixin
equations. I use mixin only in the source code (but user don't normally
read that).
thanks for pointing that out. I will polish this further.
Is there really a need for a new command? Wouldn't it make more sense to integrate the new functionality with 'interpretation' and 'sublocale'.
There might be chances for something like
context
fixes …
assumes …
begin
permanent_interpretation …
end
to work some day. Anyway, I first have to conduct some experiments to
get an idea what the challenges are.
Cheers,
Florian
P. S. This has left the proper scope of isabelle-users already, so we
should continue the thread on isabelle-dev.
signature.asc
Email Gateway (Aug 19 2022 at 16:42):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Florian,
This looks interesting, but it's not clear to me what it would mean. I take that this is a makeshift context that cannot be entered again. Presumably the construct yields some sort of lifting?
Clemens
Email Gateway (Aug 19 2022 at 16:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The idea is that the context itself is embedded into a target again (for
simplicity, let us assume a locale as canonical candidate):
context foo
begin
…
context
fixes …
assumes P
begin
permanent_interpretation bar: bar …
end
…
end
So, technically speaking, this would establish a sublocale dependency
from bar to foo such that facts propagated from bar to foo gain
additional assumptions P.
It can be seen as a proper user-space pattern to avoid raw instantiation
of foundational facts bar… [OF …].
It is not clear to me whether that machinery can handle this out of the
box (or even properly), so this has to be figured out first.
Cheers,
Florian
signature.asc
Last updated: Apr 24 2024 at 08:20 UTC