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.