Re: [isabelle] Basic help with class and instantiation



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

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

Try this one:

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

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


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?

As a rule of thumb there are hardly any bugs, only unexpected behaviour,
and that is best discussed on the mailing list.


	Makarius


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