# Re: [isabelle] A constant become a free variable

On Wed, 4 Dec 2013, Yannick Duchêne (Hibou57) wrote:

`On the last line of the simple lemma proof, at “from 4 show "t1 ≅ t2"
``by (simp add: 3)”, if I move the mouse cursor over “≅” while Ctrl is
``pressed, I get a tool‑tip which tells me it's a fixed variable as well
``as a free variable. Surprising, as to me it's a fixed variable, but I
``don't mind more. More disturbing, is what I see in the Output pan when I
``move the caret to the end of the same line ; it displays “t1 ≅ t2” and
``if I move the mouse cursor over it while Ctrl is pressed, it says it's a
``free variable, and just a free variable, and it draws the “≅” in blue
``instead of black. Why does it become a free variable in the Output pan ?
`

`I don't see an actual constant in the example, although a fixed variable
``is better understood as "local constant".
`

`The PIDE markup seen in the input or output represents certain aspects of
``the formal processing by the prover. This sometimes exposes more internal
``details than make sense to the user. It needs some further refinements,
``but that is part of the concept: more and more useful markup information
``is provided and rendered -- this is a continuous process over the years.
`

`As a question aside, is there a more explicit way to substitute the
``second “t1” in 4 using the equivalence from 3 ? I feel I already came a
``similar question one year ago, but I'm not able to remember what I did
`

lemma (in unification) l1: "t1 = t2 ⟹ t1 ≅ t2"
proof -
assume 1: "t1 = t2"
have 2: "t1 = t2 ⟹ t1 ≡ t2" by (fact HOL.eq_reflection[of t1 t2])
have 3: "t1 ≡ t2" by (fact 2[OF 1])
have 4: "t1 ≅ t1" by (fact self[of t1])
from 4 show "t1 ≅ t2" by (simp add: 3)
qed

`The use of Pure equality and HOL.eq_reflection looks a bit strange: you
``should bever need that in HOL applications, unless some old forms are
``somehow ported.
`

`A more imminent proof just normalizes wrt. "t1 = t2" and the solves via
``reflexivity ("self"):
`
lemma (in unification) "t1 = t2 ⟹ t1 ≅ t2"
by (simp add: self)

`More explicit reasoning can be done by calculations in Isar, but its
``substitution steps will always replace all occurrences of the subterm in
``question (according to the standard policy of Larry's implementation of
``Huet). Going from "t1 ≅ t1" to "t1 ≅ t2" is not immediate in this
``scheme.
`

`Maybe some experts on hand-crafted substitution can point out frequently
``used patterns, without too much "term surgery".
`
Makarius

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