[isabelle] Interpretation with special cases



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
Description: This is a digitally signed message part.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.