[isabelle] normalization method introduces schematic type variables in HOL/Word types



I found that normalisation introduces fresh type variables when the word type from HOL-Word occurs in the goal statement. Here is a tiny example:

theory Scratch imports "~~/src/HOL/Word/Word" begin

lemma "(2 + 3 :: 4 word) = 3 + 2"
  using [[show_consts, show_sorts]]
apply normalization

Before the call to normalization, there are no type variables in the goal state. The normalization method turns the goal into the following:

uint (Word.Word (snd (divmod_int (uint (Word.Word 3) + uint (Word.Word 2)) 4294967296))) =
uint (Word.Word (snd (divmod_int (uint (Word.Word 2) + uint (Word.Word 3)) 4294967296)))

The unexpected thing is that each occurrence of Word.Word now has a different type with a schematic type variable, i.e., Word.Word :: int => ?'a word, Word.Word :: int => ?'b word, etc. Correspondingly, every occurrence of uint also has a type variable in there. All the new type variables have sort {}. Consequently, I cannot use many of the other methods like simp that do not like such schematic type variables.

Why does normalization introduce these type variables at all? Is this intended? How can I disable this feature or is this inherent to NBE?

Cheers,
Andreas




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