Re: [isabelle] Interpretation with special cases
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
interpretation real_euclid: non_exact_metric "dist :: [real2, real2]
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"
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and