Email Gateway (Aug 22 2022 at 12:31): Email Gateway (Aug 22 2022 at 12:31):From: Bohua Zhan <bzhan@mit.edu>
This behavior is very strange to me. Example (in Isabelle2016-RC0):
theory Test
imports Rat
begin
declare [[show_types]]
ML {*
val eq = @{prop "(1::('a::linordered_field)) + - inverse 2 = inverse 2"};
val th = Goal.prove @{context} [] [] eq (K (Simplifier.asm_full_simp_tac
@{context} 1))
*}
This produces:
val th = "(1::?'a) + - inverse (2::?'a) = inverse (2::?'a)": thm
The free type variable is automatically converted to schematic type
variable in the resulting theorem. Why is this? How can I keep the original
free type variable?
Interestingly this is no longer the case if there is a free variable
present:
ML {*
val eq = @{prop "(1::('a::linordered_field)) + - inverse 2 + m = inverse 2
Output is:
val th = "(1::'a) + - inverse (2::'a) + (m::'a) = inverse (2::'a) + m": thm
Best,
Bohua
Email Gateway (Aug 22 2022 at 12:31):From: Makarius <makarius@sketis.net>
This is a consequence of Hindley-Milner polymorphism wrt. to the local
context. See also section 6.1 of the "implementation" manual, which
contains further explanations and some abstract examples.
If anything is still unclear after reading that, we should continue the
discussion here. These concepts are very important in Isabelle after
1999. Further discussion of difficulties also helps to improve the
manual.
Makarius
Last updated: Apr 19 2024 at 01:05 UTC