Email Gateway (Aug 22 2022 at 10:37): Email Gateway (Aug 22 2022 at 10:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I wonder whether there is any support for parametricity for records in Isabelle/HOL. In
particular, suppose I have a record
record 'a test = test :: "'a => 'a list"
Then, I would like to get a relator
rel_test_ext ::
"('a => 'b => bool) => ('m1 => 'm2 => bool)
=> ('a, 'm1) test_ext => ('b, 'm2) test => bool"
and appropriate parametricity rules for the constants generated by the record command. For
example,
test_parametric: "(rel_test_ext A B ==> A ==> list_all2 A) test test"
Do I have to derive the setup manually or is there some tool support available?
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:38):From: "traytel@in.tum.de" <traytel@in.tum.de>
Hi Andreas,
there is a command in the making that will lift BNFs through typedefs (given that the predicate is closed under map functions). Since records are type copies this will give you the relator. Proving parametricity of selectors would be then a next step.
Dmitriy
Email Gateway (Aug 22 2022 at 10:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
That's good to hear. I am looking forward to trying this new command. In the meantime,
I'll just define the relator myself.
How do you plan to handle the extensibility of records? Do you lift the BNF over the _ext
types and use normal composition or do you plan to introduce constants for _scheme, too?
This might also affect the selector issue in my other thread
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00109.html
Best,
Andreas
Last updated: Apr 26 2024 at 01:06 UTC