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"
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)
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
A more imminent proof just normalizes wrt. "t1 = t2" and the solves via
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
Maybe some experts on hand-crafted substitution can point out frequently
used patterns, without too much "term surgery".
This archive was generated by a fusion of
Pipermail (Mailman edition) and