Re: [isabelle] Basic help with class and instantiation



After Lars Noschinski's suggestion, I added (already posted, but never shown up in the thread, so I'm re‑posting it)

  declare [[show_types]]
  declare [[show_consts]]
  declare [[show_sorts]]

… before the Instantiation

Moving the cursor after “instance proof”, the Output pan of jEdit/Isabelle, shows this:

  proof (state): step 1

  goal (1 subgoal):
   1. cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat)
  constants:
    TYPE(int) :: int itself
    cls1_class :: int itself ⇒ prop
    prop :: prop ⇒ prop
    0∷nat :: nat
    cls1_g :: nat ⇒ int
    cls1_f :: int ⇒ int
    op = :: int ⇒ int ⇒ bool
    Trueprop :: bool ⇒ prop
    op ⟹ :: prop ⇒ prop ⇒ prop

Types seems correctly applied/inferred. I attempted to replace

  then show "(cls1_f (cls1_g 0)) = (cls1_g 0)"

with

  then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"

… but this solved nothing.

At this stage, as I have no idea, I wonder if it's me who is missing something, or else if my assumption that this should be OK is right, and so, that this would be an error from Isabelle. This would not be proving something which is wrong, but failing to allow to prove something which is right; which in turn is not the worst, but annoying. That doubts are blocking for me (I can't avoid thinking about this topic).


Le Tue, 14 Aug 2012 01:29:22 +0200, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> a écrit:

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.