[isabelle] partial_function shifts variable names in raw_induct
The induction rule that partial_function generates shifts the names of the function's
parameters in the quantifiers in the induction hypothesis (see below for an example). This
occurs in both Isabelle2013-1 and 2013 (I did not check how it was before). While these
names are logically insignificant, not shifting them would ease reading these rules,
especially, when I use meaningful names in the specification.
theory Scratch imports Main begin
partial_function (option) foo :: "int => string => string option"
where "foo number msg = (if number = 0 then Some msg else foo (number - 1) (tl msg))"
(* prints as:
[|foo number msg numbera.
!!msg b y. foo msg b = Some y ==> ?P msg b y;
(if number = 0 then Some msg else foo (number - 1) (tl msg)) =
Some numbera |]
==> ?P number msg numbera;
foo ?number ?msg = Some ?y |]
==> ?P ?number ?msg ?y
Note how the bound variable msg in the second line has type int, whereas b type string there.
In the same spirit, I doubt that numbera (of type string) is a good name for the result of
This archive was generated by a fusion of
Pipermail (Mailman edition) and