[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))"

thm foo.raw_induct

(* 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 the computation.


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