[isabelle] A constant become a free variable



Planning to rework an SML application I did three years ago, I wanted to have a start trying something in a sample theory, attached to this message and pasted below in case the attachment disappears.

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 ?

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 (I'm seasoned with Isabelle).

-----%<---------->%-----

theory Sample
imports Main
begin

  typedecl atom;
  typedecl variable;

  datatype "term" =
    Any                  ("ε")
  | Atom atom            ("α")
  | Variable variable    ("υ")
  | Compound "term list" ("ω")
  ;

  locale unification =
    fixes
      unifies :: "[term, term] ⇒ bool"       (infix "≅" 500) and
      "interpretation" :: "variable ⇒ term"  ("⊢")
    assumes
      self: "t ≅ t" and
      comm: "t1 ≅ t2 ⟷ t2 ≅ t1" and
      inter: "(υ v) ≅ t ⟷ (⊢ v) ≅ t" and
      rec: "(ω (t1 # r1)) ≅ (ω (t2 # r2)) ⟷ t1 ≅ t2 ∧ (ω r1) ≅ (ω r2)"
  ;

  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
  ;

end

-----%<---------->%-----

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Attachment: Sample.thy
Description: Binary data



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