Email Gateway (Apr 23 2025 at 18:28): Email Gateway (Apr 23 2025 at 18:28):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
here's an issue that has been bugging me for years: in methods like
"cases", "induct", and "induction" that take a rule and instantiations
for that rule, it seems that type inference is first run for the
instantiations separately and the results are then plugged into the rule.
This can lead to problems, e.g. the following does not work:
lemma
fixes P :: "int ⇒ bool"
shows "P a"
proof (cases a 0 rule: linorder_cases)
exception THM 0 raised (line 756 of "drule.ML"):
infer_instantiate_types: type int of variable ?y
cannot be unified with type 'a of term 0
(?x < ?y ⟹ ?P) ⟹
(?x = ?y ⟹ ?P) ⟹ (?y < ?x ⟹ ?P) ⟹ ?P
There is an easy workaround, of course:
proof (cases a "0::int" rule: linorder_cases)
However, I remember that I was quite puzzled when I first encountered
this. Perhaps it would be worth investigating whether this can be made
more robust. I can e.g. write
thm linorder_cases[of a 0]
just fine, so it must be possible to plug in the instantiations first an
then do the type inference. I tried to do it myself but didn't get very far.
Cheers,
Manuel
Last updated: May 06 2025 at 08:28 UTC