[isabelle] fsp question-- supporting "natural" entry



Formal_Power_Series
has

lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d =
            fps_const (c * d)"

for scalar multiplication of c times fsp and it works but seems to require a conversion in the "shows" before entry. I would like to state

shows "(x::real)*(f::fsp)....."
or tacitly
shows "(x)*(f::fsp)....."

explicitly, but the parser objects.
In order to avoid continually digging around in the terms far removed in the heirarchy, is it appropriate to "overload" "*" ? Can I even do it to "*"? The documentation I am reading seems oriented to overloading classes/types.
And should I do it or not. i.e. are there dangers here?
In addition: since the fsp can have coefficients from rings other than real; how should I make sure that "x in (coefficient ring)" ? I am really open to alternatives to "overloading"; but I would really like equations far removed from the base to be expressible "naturally".

Ray

--
From the QED manifesto: https://www.cs.ru.nl/~freek/qed/qed.html
"
Mathematics is arguably the foremost creation of the human mind.
"





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