Re: [isabelle] Error: Pending sort hypothesis



I am surprised you got any answer from sledgehammer, I failed.
Unfortunately the proof you got is not a real proof: the ATPs are give a
problem with some type information omitted for efficiency reasons. This
allows them sometimes to find proofs that do not replay in Isabelle
because of typing problems. Yours is most likely of that kind.

The development version has a Settings item ATP: Full Types that gives
the ATPs the full type information which you can try in such situations.
It will avoid these unsound proofs but also reduces the success rate of
the ATPs. In you example I am sceptical that the ATPs will find a real
proof because of the non-trivial witnesses required.

Tobias

Peter 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.