Email Gateway (Aug 19 2022 at 12:43): Email Gateway (Aug 19 2022 at 12:43):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
I just tried the new simps_of_case conversion procedure, and so far, it works great except
for one thing: it does not preserve the names of variables that are bound in the cases,
but invents new ones. And therefore, I would like to ask for a new feature, namely that it
preserves them as far as possible. Here's an example:
datatype foo = Foo nat nat | Bar int
definition foo :: "foo => foo" where
"foo y = (case y of Foo n m => Bar (int n - int m) | Bar y => Foo (nat y) 0)"
simps_of_case foo_simps: foo_def
Now, foo.simps is the following:
"foo (Foo xa x) = Bar (int xa - int x)"
"foo (Bar x) = Foo (nat x) 0"
Here, n and m have been replaced by xa and x (but n and m are equally fresh) and the y by
x (y occured in the original theorem, but not in the final, so y could be resued too). I
would prefer if the names of the bound variables can be preserves, i.e.,:
"foo (Foo n m) = Bar (int n - in m)"
"foo (Bar y) = Bar (nat y) 0"
Best,
Andreas
Last updated: May 06 2024 at 12:29 UTC