Email Gateway (Mar 11 2024 at 03:30): Email Gateway (Mar 11 2024 at 03:30):From: Ian Hayes <Ian.Hayes@uq.edu.au>
We are trying to use/adapt the HOL/Hoare_Parallel theories, in
particular, RG_Syntax.
In those theories the state of a program is represented by a record.
A common requirement is for a relation that says that only the x field
of the state changes
i.e. all other fields remain the same.
If one only has two fields x and y, one can just explicitly say, y after
= y before,
but if there are many fields this become tedious.
Moreover we would like it to be generic and given an arbitrary record
type that has a field x
says that all fields other than x should be unchanged.
Or more generally, given a set of field names X, all fields other than
those in X do not change.
Can anyone give us pointers as to how to approach this?
For example, do records have any way of getting the names of the fields
of a record?
Or the set of their accessor functions?
Thanks in advance
Ian
Email Gateway (Mar 11 2024 at 08:51):From: Thomas Sewell <tals4@cam.ac.uk>
Hi Ian.
This issue has been seen before. I once considered defining some special syntax for equality modulo some fields, and decided it wasn't quite worth it. Here are some options to consider.
You could phrase your property about r1 and r2 as "∃ x2. r2 = r1⦇ x := x2 ⦈" (ASCII "? x2. r2 = r1(| x := x2 |)" in case something is wrong with unicode).
That existential form should work well if it ever ends up in your assumptions. Then r2 will be rewritten into an explicit update of r1 throughout your goal, and the equalities for other fields will be proven automatically.
To prove this goal, or any other kind of record equality, as a conclusion, you might want to make use of the ".equality" theorem created by the record package, e.g. if your state record is called "state", have a look at "state.equality".
For each field "x" of the record, the package creates an accessor constant (just called "x") and an updator called "x_update". If you want to try to define something generic for a list of field updates, you might want to try to define some combinator across the update functions.
You can't enumerate all of the fields/accessors of a record as an Isabelle object, since they don't necessarily have the same type. You can fetch them all as syntax in ML code, if you want. Have a look at the interface in src/HOL/Tools/record.ML . I'm not sure how helpful that is, though.
I hope at least one of those suggestions is useful.
More broadly, I think that it's a bug that the record package defines an accessor constant with the same name as the field. We don't really want a collection of constants with names like "x" living in the global context and conflicting with variable names. I think that there should be a single constant defined with a name like "x_field", and both the accessor and updator syntax should derive from that. There are some other advantages to having a single field constant, for instance, various proofs about field updates want to use field access to pick the obvious witness value, but in the current setup this requires code or user input to relate "x_update" to "x".
Good luck with it,
Thomas.
Email Gateway (Mar 11 2024 at 09:19):From: Alex Shkotin <alex.shkotin@gmail.com>
Hi Ian
Just in addition: consider using any kind of macro processing to simplify a
tedious work.
Alex
пн, 11 мар. 2024 г. в 06:30, Ian Hayes <Ian.Hayes@uq.edu.au>:
Last updated: Apr 28 2024 at 20:16 UTC