# [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.