[isabelle] Goal.prove automatically produces schematic type variables



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
+ m"};
val th = Goal.prove @{context} [] [] eq (K (Simplifier.asm_full_simp_tac
@{context} 1))
*}

Output is:
val th = "(1::'a) + - inverse (2::'a) + (m::'a) = inverse (2::'a) + m": thm

Best,
Bohua



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