Email Gateway (Aug 19 2022 at 12:34): Email Gateway (Aug 19 2022 at 12:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi,
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.
Andreas
Last updated: Apr 25 2024 at 12:23 UTC