*Subject*: Re: [isabelle] Interpretation with special cases*From*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Date*: Mon, 25 May 2009 09:57:35 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200905251627.45020.tjm1983@gmail.com>*References*: <200905251627.45020.tjm1983@gmail.com>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Hi Tim,

proof show "\<exists>x y z :: real ^ 2. \<not> real_euclid.exact x y z \<and> \<not> real_euclid.exact y z x \<and> \<not> real_euclid.exact z x y" Regards, Andreas Tim McKenzie schrieb:

In the attached file, I define a locale called metric, and I prove interpretation real_euclid: metric distI also define a locale (based on metric) called non_exact_metric, and I try tobegin provinginterpretation real_euclid: non_exact_metric "dist:: [real^2, real^2] => real"Isabelle 2009 balks at the last show in the file, complaining "Local statementwill fail to refine any pending goal", even though I've specified that I onlywant to prove the interpretation for the two-dimensional case of dist. If Iremove the bit that specifies that ?x is of type real^2, then Isabelle happilyprocesses 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 <><

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

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