Email Gateway (Aug 18 2022 at 13:57): Email Gateway (Aug 18 2022 at 13:57):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Is there an example in the HOL sources of defining a function from a
single valued relation. I want to specify the equations of the
function as simp rules, and also be able to go back and forth from
relational statements to equivalent functional statements.
Thanks for any pointers that could save me time figuring out how to do this.
Randy
Email Gateway (Aug 18 2022 at 13:57):From: Lawrence Paulson <lp15@cam.ac.uk>
You could look at the definition of the finite set fold functional in
the file Finite_Set.thy. There is also an associated paper: http://www.cl.cam.ac.uk/~lp15/papers/Reports/TPHOLs05.pdf
Larry
Last updated: Nov 21 2024 at 12:39 UTC