# [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 =
fixes
cls1_x :: "'a" and
cls1_f :: "'a ⇒ 'a" and
cls1_g :: "nat ⇒ 'a"
assumes
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
begin
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
qed
end

`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.*