Re: [isabelle] Basic help with class and instantiation



On Thu, 16 Aug 2012, Yannick Duchêne (Hibou57) wrote:

Try this one:

  show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))"
                                 ^^^^^^
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)"

Yes. In this context the argument type of cls1_g is always nat, so there is no need for that constraint.


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.

There is something like a standard portfolio of getting confused with type inference. I will try harder next time to provide some visual clues in the Prover IDE markup about such situations, so that errors are easier to understand, or avoided in the first place.


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)"

There is no fundamental difference of 'definition' vs. 'fun', only an accidental one: 'definition' (like 'abbreviation') allows a short form where the defined entity is not explicitly bound but just mentioned in the proper place on the LHS of the defining equation. You can call that feature a bug, but I usually use neither of these meaningless words. It is just a convenience to write short definitions, even if it can lead to slightly different situations concerning type-inference.

So what happens here is that

  definition df: "(cls1_f i) = (f i)"

refers to a particilar instance of the overloaded constant cls1_f for type int, because that is special in the instantiation context. The context is also responsible for exchanging that instance internally with a formal parameter cls1_f_int that needs to be defined here for the sake of the instantiation. The 'print_context' command right after 'instantiation' tells that story in extreme brevity.

So here is the fun version of your example:

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

print_context

fun cls1_f_int where "cls1_f_int n = f n"
fun cls1_g_int where "cls1_g_int n = g n"

instance
proof
  have "cls1_f 0 = f 0" by simp
  have "cls1_g 0 = g 0" by simp
  have "f (g 0) = g 0" by simp
  then show "cls1_f (cls1_g 0 :: int) = cls1_g 0" by simp
qed

end


Another obvious improvement of the Prover IDE would be to turn the print_context above into some kind of template for the consecutive text.


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.

You've just fallen on you nose by defining unrelated cls1_f and cls2_g. See the fun clauses above, with cls1_f_int and cls2_g_int.



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.

Another trap here.  This is how it works:

abbreviation (input) f :: "int ⇒ int" where "f i ≡ i"
abbreviation (input) g :: "nat ⇒ int" where "g n ≡ (int n)"

Abbreviations try to be smart folding back by default, but the first line can do that indefinitely, so an attempt to print something integer will loop later on.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.