*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Interpretation with special cases*From*: Tim McKenzie <tjm1983 at gmail.com>*Date*: Mon, 25 May 2009 16:27:40 +1200*User-agent*: KMail/1.11.2 (Linux/2.6.28-11-generic; KDE/4.2.2; i686; ; )

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

theory Metric imports Euclidean_Space begin locale metric = fixes d :: "'p \<Rightarrow> 'p \<Rightarrow> real" assumes zero_iff: "d x y = 0 \<longleftrightarrow> x = y" and triangle: "d x z \<le> d y x + d y z" definition (in metric) exact :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool" where "exact x y z \<equiv> d x z = d y x + d y z" locale non_exact_metric = metric + assumes non_exact: "\<exists>x y z. \<not> exact x y z \<and> \<not> exact y z x \<and> \<not> exact z x y" interpretation real_euclid: metric dist proof fix x y z show "dist x y = 0 \<longleftrightarrow> x = y" by simp from dist_triangle_alt show "dist x z \<le> dist y x + dist y z" by blast qed interpretation real_euclid: non_exact_metric "dist :: [real^2, real^2] \<Rightarrow> real" proof show "\<exists>x y z. \<not> real_euclid.exact x y z \<and> \<not> real_euclid.exact y z x \<and> \<not> real_euclid.exact z x y" proof let ?x = "0 :: real^2" show "\<exists>y z. \<not> real_euclid.exact ?x y z \<and> \<not> real_euclid.exact y z ?x \<and> \<not> real_euclid.exact z ?x y"

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Interpretation with special cases***From:*Andreas Lochbihler

**Re: [isabelle] Interpretation with special cases***From:*Brian Huffman

- Previous by Date: Re: [isabelle] problem with opening proof
- Next by Date: Re: [isabelle] Interpretation with special cases
- Previous by Thread: [isabelle] 2nd Cfp: PCC09
- 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