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.