[isabelle] simps_of_case does not preserve variable names



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.