Re: [isabelle] Basic help with class and instantiation



On Thu, 16 Aug 2012 16:44:43 +0200, Makarius <makarius at sketis.net> wrote:

Try this one:

   show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))"
                                  ^^^^^^

And yes, this solves the unification! (Makarius is a genius :-P )

Any of this three ones do:

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


The Prover IDE helped to expose the type of cls1_f and cls2_g in the text,
using CTRL/COMMAND hover.

I often use it, but well, missed that. I did it again, and for cls1_f it says “'a::cls1 ⇒ 'a::cls1”, and for cls1_f it says “'nat ⇒ 'a::cls1”.

So the type inference did not applied (while I was so much sure it did), and I have to understand why. What could have been the way to solve the type inference as I expected it to be? I see only one:

  definition df: "(cls1_f i) = (f i)"
  definition dg: "(cls1_g n) = (g n)"

May be because that's just definitions? So I tried to replace the above with:

  fun cls1_f :: "int ⇒ int"
    where "(cls1_f i) = (f i)"

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


Now ctrl/command + mouse‑hovering on cls1_f and cls1_g in:

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

… shows type inference applies in this case, as it says “int ⇒ int” and “nat ⇒ int”. But unification does not works for another reason; it now complains instead:

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

while before it was complaining:

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

The difference is the “local.” prefix.

Another attempt with:

  abbreviation "(cls1_f i) ≡ (f i)"
  abbreviation "(cls1_g n) ≡ (g n)"

… ends into the same similar issue as with Definition, but even worst, as adding a type annotation does not solve anything now.

Conclusion so far: Definition (and Abbreviation) do not provides hints for type inference, even if the Definition provides type annotations, and using fun/function, which provides hints for type inference, is not OK, as this create a plain new entity (of the same name, but still another entity), which cannot be unified with the expected one.

These are things to keep in mind about Isar.

Now to come back to an above comment I've made, which is “I often use it, but well, missed that” (talking about ctrl/command + mouse‑hovering over an item), may be an idea: show_types/consts/sorts, could still display something even when there is error to display. The Output pan did not show anything, as there was an error message instead, which replaced report messages. If both have been displayed together, may be I won't have missed it, as what's always displayed is less likely to be missed as I did.


By the way, is there a recommended way to submit bug reports (if that's
really one) about Isabelle?

As a rule of thumb there are hardly any bugs, only unexpected behaviour,

I believe the same (thus my doubts), and surprised myself to come to the bug hypothesis.

and that is best discussed on the mailing list.

OK


--
“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.