Re: [isabelle] Interpretation with special cases



Thanks Brian and Andreas for your excellent explanations. I think I
understand the problem now, and I've also found out how to turn on
"show types" and "show sorts" in Proof General, so I should be able to
diagnose similar problems in future.

Tim
<><

2009/5/26 Brian Huffman <brianh at cs.pdx.edu>:
> 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





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