*To*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Basic help with class and instantiation*From*: Makarius <makarius at sketis.net>*Date*: Thu, 16 Aug 2012 16:44:43 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <op.wi4zq9zzule2fv@douda-yannick>*References*: <op.wiz568nrule2fv@douda-yannick> <op.wi4j9voqule2fv@douda-yannick> <502CB0B2.7040509@informatik.tu-muenchen.de> <op.wi4zq9zzule2fv@douda-yannick>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 result is the same. May be that's finally a bug, or else don't seewhy 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'sreally 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

**References**:**[isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Florian Haftmann

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Basic help with class and instantiation
- Next by Date: Re: [isabelle] Basic help with class and instantiation
- Previous by Thread: Re: [isabelle] Basic help with class and instantiation
- Next by Thread: Re: [isabelle] Basic help with class and instantiation
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list