Re: [isabelle] Error: Pending sort hypothesis



Tobias Nipkow wrote:
> It turns out that your intuition was right: sledgehammer can prove the
> theorem, with a little help. This is the resulting proof (to go into the
> library):
>
> lemma finite_imp_inj_to_nat_seg:
>   "finite A ==> EX f n::nat. f`A = {i. i<n} & inj_on f A"
> by (metis bij_betw_Inv bij_betw_def finite_imp_nat_seg_image_inj_on)
>
>   
Is there any rule of thumb when to use EX and when to use obtains for
theorems (from a good-style viewpoint, not from the ATP viewpoint)?
Note that metis can also prove the theorem in obtains-style.

regards,
  Peter

> For a start, notice the formulation in terms of EX rather than
> "obtains", which s/h seems to prefer. But still, s/h does not find a
> proof. You need to tell it to use finite_imp_nat_seg_image_inj_on:
>
>   






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