[isabelle] Basic help with class and instantiation
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"
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and