*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*: Fri, 17 Aug 2012 20:50:59 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <op.wi47htqmule2fv@douda-yannick>*References*: <op.wiz568nrule2fv@douda-yannick> <op.wi4j9voqule2fv@douda-yannick> <502CB0B2.7040509@informatik.tu-muenchen.de> <op.wi4zq9zzule2fv@douda-yannick> <op.wi47htqmule2fv@douda-yannick>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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

Try this one: show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))" ^^^^^^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 the text, using CTRL/COMMAND hover.I often use it, but well, missed that. I did it again, and for cls1_f it says“'a::cls1 ⇒ 'a::cls1”, and for cls1_f it says “'nat ⇒ 'a::cls1”.So the type inference did not applied (while I was so much sure it did),and I have to understand why.

What could have been the way to solve the typeinference as I expected it to be? I see only one:definition df: "(cls1_f i) = (f i)" definition dg: "(cls1_g n) = (g n)" May be because that's just definitions? So I tried to replace the above with: fun cls1_f :: "int ⇒ int" where "(cls1_f i) = (f i)" fun cls1_g :: "nat ⇒ int" where "(cls1_g n) = (g n)"

So what happens here is that definition df: "(cls1_f i) = (f i)"

So here is the fun version of your example: 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)) = (cls1_g 0)" fun f :: "int ⇒ int" where "f i = i" fun g :: "nat ⇒ int" where "g n = (int n)" instantiation int :: cls1 begin print_context fun cls1_f_int where "cls1_f_int n = f n" fun cls1_g_int where "cls1_g_int n = g n" instance proof have "cls1_f 0 = f 0" by simp have "cls1_g 0 = g 0" by simp have "f (g 0) = g 0" by simp then show "cls1_f (cls1_g 0 :: int) = cls1_g 0" by simp qed end

Now ctrl/command + mouse‑hovering on cls1_f and cls1_g in: then show "(cls1_f (cls1_g 0)) = (cls1_g 0)" by simp… shows type inference applies in this case, as it says “int ⇒ int” and “nat⇒ int”. But unification does not works for another reason; it now complainsinstead: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)"… ends into the same similar issue as with Definition, but even worst,as adding a type annotation does not solve anything now.

Another trap here. This is how it works: abbreviation (input) f :: "int ⇒ int" where "f i ≡ i" abbreviation (input) g :: "nat ⇒ int" where "g n ≡ (int n)"

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)

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