# [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.