*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Basic help with class and instantiation*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Thu, 16 Aug 2012 15:58:11 +0200*Organization*: Ada @ Home*References*: <op.wiz568nrule2fv@douda-yannick> <op.wi4j9voqule2fv@douda-yannick> <502CB0B2.7040509@informatik.tu-muenchen.de>*User-agent*: Opera Mail/12.01 (Linux)

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

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

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

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

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

**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

- 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