Email Gateway (Aug 22 2022 at 18:11): Email Gateway (Aug 22 2022 at 18:11):From: Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
Greetings,
I am working with functions " fun :: ('a => 'b) => ( 'b :: ring) " and I
would like to reason about "substitutions" on them in the following sense:
I know that I will always be dealing with these functions as
lambda-abstractions, i.e. my function could be something like "/\ s. s x +
c · s y", and the substitution of "y" by the ring-element "d" in it would
be "/\ s. s x + c · d". In a very vague sense, the substitution is
performed over the syntax generated by the ring structure. That is, it will
respect the ring´s addition and multiplication and it will only replace
'a-variables by 'b-values.
Is it possible to implement these substitutions (of type "(('a =>'b)
=>('b::ring))=>(('a=>'b)
=>'b)")?
at the ML-level?
Email Gateway (Aug 22 2022 at 18:11):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
I suggest the following:
https://www.cs.york.ac.uk/circus/isabelle-utp/metalogic.html
There is a section for a meta-theory for substitution with a repository
link to the Isabelle sources.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 18:15):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Glad you find it useful.
Note that the core UTP theories is based on an expression language built
on a top of HOL (using lifting package). The expression language has a
strong syntactic flavor to mimic the UTP textbook notations.
I am not sure about what you want to do with UTP, but following my
experience (and also what any Isabelle expert will say): using HOL
directly, instead of lifting everything from HOL to a new expression
language, is more efficient for Isabelle backend tools and Isabelle tactics.
If what you like about UTP expressions is that they hide the state, then
you can always use for example syntax-translation package and have your
state hidden behind the expression while being more shallower than the
actual UTP.
Besides that, yes I do agree what York guys did with this UTP mechanization
is impressive.
Best wishes,
Yakoub
Last updated: Apr 25 2024 at 04:18 UTC