*To*: Tim McKenzie <tjm1983 at gmail.com>*Subject*: Re: [isabelle] Interpretation with special cases*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 25 May 2009 13:15:53 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200905251627.45020.tjm1983@gmail.com>*References*: <200905251627.45020.tjm1983@gmail.com>*Sender*: huffman.brian.c at gmail.com

Hi Tim, Running your proof script with "show sorts" enabled highlights exactly what the problem is. In your first "show" statement, the goal you have stated has a more general type than what you intended: "real^2" is replaced with "real ^ 'a". Since the more general statement still resolves with the original goal, Isar does not complain. Now Isabelle is expecting you to prove this new, more general goal, which of course is impossible. To fix the problem, just add a type annotation to the "show" statement to force x y and z to have type "real^2". interpretation real_euclid: non_exact_metric "dist :: [real^2, real^2] => real" proof (* the subgoal at this point is for type "real ^ 2" *) show "EX x y z. ~ real_euclid.exact x y z & ~ real_euclid.exact y z x & ~ real_euclid.exact z x y" (* the subgoal at this point is for type "real ^ 'a" *) proof let ?x = "0 :: real^2" show "EX y z. ~ real_euclid.exact ?x y z & ~ real_euclid.exact y z ?x & ~ real_euclid.exact z ?x y" I am actually surprised that no warning message is generated after the first "show", since you are adding a new type variable "'a" to the proof state that wasn't there before. I think there *should* be a warning message in this case, because inventing a new type variable is probably not what anyone would intend to do. - Brian On Sun, May 24, 2009 at 9:27 PM, Tim McKenzie <tjm1983 at gmail.com> wrote: > In the attached file, I define a locale called metric, and I prove > > interpretation real_euclid: metric dist > > I also define a locale (based on metric) called non_exact_metric, and I try to > begin proving > > interpretation real_euclid: non_exact_metric "dist:: [real^2, real^2] => real" > > Isabelle 2009 balks at the last show in the file, complaining "Local statement > will fail to refine any pending goal", even though I've specified that I only > want to prove the interpretation for the two-dimensional case of dist. If I > remove the bit that specifies that ?x is of type real^2, then Isabelle happily > processes the show command. I don't think I'd be able to finish the proof, > though, since one-dimensional Euclidean space doesn't satisfy non_exact. > > Can someone explain to me what's going on here? > > Tim > <>< >

**Follow-Ups**:**Re: [isabelle] Interpretation with special cases***From:*Tim McKenzie

**References**:**[isabelle] Interpretation with special cases***From:*Tim McKenzie

- Previous by Date: Re: [isabelle] Interpretation with special cases
- Next by Date: Re: [isabelle] Interpretation with special cases
- Previous by Thread: Re: [isabelle] Interpretation with special cases
- Next by Thread: Re: [isabelle] Interpretation with special cases
- Cl-isabelle-users May 2009 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