*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 18:45:19 +0200*Organization*: Ada @ Home*References*: <op.wiz568nrule2fv@douda-yannick> <op.wi4j9voqule2fv@douda-yannick> <502CB0B2.7040509@informatik.tu-muenchen.de> <op.wi4zq9zzule2fv@douda-yannick>*User-agent*: Opera Mail/12.01 (Linux)

On Thu, 16 Aug 2012 16:44:43 +0200, Makarius <makarius at sketis.net> wrote:

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

And yes, this solves the unification! (Makarius is a genius :-P ) 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)"

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

definition df: "(cls1_f i) = (f i)" definition dg: "(cls1_g n) = (g n)"

fun cls1_f :: "int ⇒ int" where "(cls1_f i) = (f i)" fun cls1_g :: "nat ⇒ int" where "(cls1_g n) = (g n)" Now ctrl/command + mouse‑hovering on cls1_f and cls1_g in: then show "(cls1_f (cls1_g 0)) = (cls1_g 0)" by simp

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. Another attempt with: abbreviation "(cls1_f i) ≡ (f i)" abbreviation "(cls1_g n) ≡ (g n)"

These are things to keep in mind about Isar.

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.

OK -- “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:*Yannick Duchêne (Hibou57)

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

**Re: [isabelle] Basic help with class and instantiation***From:*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