# Re: [isabelle] Error: Pending sort hypothesis

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)
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:
using finite_imp_nat_seg_image_inj_on
Now s/h finds the above proof.
Tobias
Lammich schrieb:
> Hi all,
>
> I wanted to prove the following lemma:
>
> lemma
> fixes A :: "'a set"
> assumes "finite A"
> obtains f::"'a => nat" and n::"nat" where
> "f`A = {i. i<n}"
> "inj_on f A"
>
> (* Sledgehammer found a proof: *)
> apply (metis finite finite_imageD id_apply inj_on_inverseI
> infinite_UNIV_char_0)
> (* Here, Isabelle sais: No subgoals
> However, when finnishing the proof: *)
> done
> (* I get the error:
> *** Pending sort hypotheses: {finite,semiring_char_0}
> *** At command "done".
> *)
>
> Ok, I wondered how to prove the theorem from the lemmas given to metis.
> But what is happening here behind the scenes, how do these
> typeclasses(?) enter the game?
>
> Regards,
> Peter
>
>

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