Re: [isabelle] Interpretation with special cases



Hi Tim,

Running your proof script with "show sorts" enabled highlights exactly
what the problem is. In your first "show" statement, the goal you have
stated has a more general type than what you intended: "real^2" is
replaced with "real ^ 'a". Since the more general statement still
resolves with the original goal, Isar does not complain. Now Isabelle
is expecting you to prove this new, more general goal, which of course
is impossible. To fix the problem, just add a type annotation to the
"show" statement to force x y and z to have type "real^2".

interpretation real_euclid: non_exact_metric "dist :: [real^2, real^2] => real"
proof
(* the subgoal at this point is for type "real ^ 2" *)
  show "EX x y z.
    ~ real_euclid.exact x y z &
    ~ real_euclid.exact y z x &
    ~ real_euclid.exact z x y"
(* the subgoal at this point is for type "real ^ 'a" *)
  proof
    let ?x = "0 :: real^2"
    show "EX y z.
      ~ real_euclid.exact ?x y z &
      ~ real_euclid.exact y z ?x &
      ~ real_euclid.exact z ?x y"

I am actually surprised that no warning message is generated after the
first "show", since you are adding a new type variable "'a" to the
proof state that wasn't there before. I think there *should* be a
warning message in this case, because inventing a new type variable is
probably not what anyone would intend to do.

- Brian


On Sun, May 24, 2009 at 9:27 PM, Tim McKenzie <tjm1983 at gmail.com> wrote:
> 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.