Re: [isabelle] Interpretation with special cases



Hi Tim,

if you turn on "show types" in Isabelle, you see that the goal in your interpretation proof for real_euclid : non_exact_metric after the first "proof" command still contains the type "real ^ 2" for the existentially quantified x y z.

Your show statement however replaces this type constraint with "real ^ 'a" because this is the most general type that can be inferred for the proposition to be shown. Since this type is more general than the typing for the actual goal to be shown, Isabelle does not complain. Hence, inside your second proof, the type for ?x should be "real ^ 'a" with 'a being now fixed.

The solution is to include a type constraint already in the first show statement:

interpretation real_euclid: non_exact_metric "dist :: [real2, real2] \<Rightarrow> real"
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 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
<><







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