*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Error: Pending sort hypothesis*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Mon, 12 Oct 2009 15:08:46 +1100*Cc*: Peter Lammich <peter.lammich at uni-muenster.de>*In-reply-to*: <4AD21C82.6040203@in.tum.de>*References*: <4ACFA37E.7000600@uni-muenster.de> <4AD21C82.6040203@in.tum.de>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Hi Peter.

Yours, Thomas. lemma fixes A :: "'a set" assumes finA: "finite A" obtains f::"'a => nat" and n::"nat" where "f`A = {i. i<n}" "inj_on f A" proof - obtain xs where dist: "distinct xs" and A: "A = set xs" using finite_distinct_list[OF finA] by auto

obtain f where f_def: "f == inv g o Inl" .. have inj_g: "inj g" unfolding g_def apply (rule inj_onI) apply (auto simp: nth_eq_iff_index_eq[OF dist] split: split_if_asm) done have f_i: "!!i. i < length xs ==> f (xs ! i) = i" unfolding f_def apply (cut_tac x=i in inv_f_f[OF inj_g]) apply (clarsimp simp: g_def) done have f_im: "f ` A = {i. i < length xs}" apply safe apply (clarsimp simp: A in_set_conv_nth f_i) apply (simp add: A) apply (rule image_eqI[OF sym], erule f_i) apply simp done have f_inj: "inj_on f A" apply (rule inj_onI) apply (auto simp: A in_set_conv_nth f_i) done show ?thesis using prems f_im f_inj by auto qed Tobias Nipkow wrote:

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

**Follow-Ups**:**Re: [isabelle] Error: Pending sort hypothesis***From:*Tobias Nipkow

**Re: [isabelle] Error: Pending sort hypothesis***From:*Peter Lammich

**References**:**[isabelle] Error: Pending sort hypothesis***From:*Peter Lammich

**Re: [isabelle] Error: Pending sort hypothesis***From:*Tobias Nipkow

- Previous by Date: [isabelle] default implementations for type classes
- Next by Date: Re: [isabelle] documentation
- Previous by Thread: Re: [isabelle] Error: Pending sort hypothesis
- Next by Thread: Re: [isabelle] Error: Pending sort hypothesis
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list