Re: [isabelle] Basic help with class and instantiation



Le Thu, 16 Aug 2012 10:34:58 +0200, Florian Haftmann <florian.haftmann-jNDFPZUTrfRoctOpMxdO53BFZrOObVGws0AfqQuZ5sE at public.gmane.org> a écrit:

Hi Yannick,

   instantiation int :: cls1
     begin
       definition df: "cls1_f n = f n"
       definition dg: "cls1_g n = g n"

without having really tried, I guess that the type of these definitions
is too general; try something like "cls1_f n = (f n :: int)".

	Florian



Florian, thanks for your reply,


I tried to add type annotations everywhere I could, which gave:

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

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

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

  declare [[show_types]] -- Testing
  declare [[show_consts]] -- Testing
  declare [[show_sorts]] -- Testing

  instantiation int :: cls1
    begin
      definition df: "(cls1_f (i::int)) = (f (i::int))"
      definition dg: "(cls1_g (n::nat)) = (g (n::nat))"
      instance proof
        have "(cls1_f (0::int)) = (f (0::int))" using df by simp -- Testing
        have "(cls1_g (0::nat)) = (g (0::nat))" using dg by simp -- Testing
        have "(f (g (0::nat))) = (g (0::nat))" by simp
        then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
          using df and dg by simp
      qed
    end


The result is the same. May be that's finally a bug, or else don't see why it can't unify the expression to be shown with the pending goal.

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

I wondered if this could be due to the absence of a universal quantification in the pending goal, but Isabelle is OK with this in other context, and there's no variables to Fix here. I will try something similar with a Locale, as a Class has similarities with a Locale, to see if it ends with the same.


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