[isabelle] Basic help with class and instantiation

Hi all,

I must miss something obvious, I can't get a simple sample class instatiation working, and that's many hours I try to guess, but failed, thus this message.

Here is the sample:

  class cls1 =
      cls1_x :: "'a" and
      cls1_f :: "'a ⇒ 'a" and
      cls1_g :: "nat ⇒ 'a"
      cls1_fg_prop: "(cls1_f (cls1_g 0)) = (cls1_g 0)"

  fun f :: "int ⇒ int" where
    "f i = i"

  fun g :: "nat ⇒ int" where
    "g n = (int n)"

  instantiation int :: cls1
      definition df: "cls1_f n = f n"
      definition dg: "cls1_g n = g n"
      instance proof
        have "cls1_f 0 = f 0" unfolding df by simp -- #1
        have "cls1_g 0 = g 0" unfolding dg by simp -- #2
        have "f (g 0) = g 0" by simp               -- #3
        then show "cls1_f (cls1_g 0) = cls1_g 0"   -- #4
          unfolding df and dg by simp

Cls1 is just for testing, it does not pretend to be useful in any way. F and g, are supposed to play the role of cls1_f and cls1_g, respectively.

In the instantiation, putting the cursor on Show, which is underlined in red, Isabelle insist on complaining:

  Local statement will fail to refine any pending goal
  Failed attempt to solve goal by exported rule:
  cls1_f (cls1_g 0) = cls1_g 0

However, putting the cursor right after Instance Proof, Isabelle says:

  proof (state): step 1
  goal (1 subgoal):
   1. cls1_f (cls1_g 0) = cls1_g 0

… which is exactly what's in the expression to be shown.

Line #1 and #2 are for testing, after this failure, and both are OK. Hovering the cursor above cls1_f and cls1_g in line #1 and #2, says they are cls1_class.cls1_f and cls1_class.cls1_g, which makes Isabelle's complains even less clear to me.

Line #3 is OK too.

So what's wrong? Must be obvious, but honestly, I completely miss it.

P.S. By the way, what's the name of the default proof method Isabelle uses in Instance Proof? Does not seems to be unfold_classes (as there is an unfold_locales method) or any similar names I've tested.

“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

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