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

It would be nice to get a compact proof. Here is a condensed version of Thomas's proof, getting rid of Inl/Inr: 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 let ?I = "{i. i<size xs}" def g == "%n. xs ! n" def f == "Inv ?I g" have inj_g: "inj_on g ?I" 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 : ?I ==> f (xs ! i) = i" unfolding f_def by (metis Inv_f_f g_def inj_g) have f_im: "f ` A = ?I" apply(auto simp add:A in_set_conv_nth f_i) apply (metis Collect_def f_i in_set_conv_nth rev_image_eqI mem_def) 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 I am sure this can be improved further. Tobias Thomas Sewell wrote: > Hi Peter. > > I agree with Tobias, it's highly unlikely that the automated theorem > provers will find an instantiation that solves your problem. I was > fiddling with your problem out of interest, and did find a proof, but > it's not especially elegant. The rule finite_distinct_list tells you > that a list exists which puts A in order, giving you (roughly) the > inverse of the function f you want. The problem is inverting back to f > since we don't have an injective function. To do this I had to extend > into the sum type to force injectivity - maybe someone can see an easier > way? > > 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 g where g_def: "g == (%n. if n < length xs then Inl (xs ! n) > else Inr n)" .. > > 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 >>> >>> >>> >> >> >

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

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

**Re: [isabelle] Error: Pending sort hypothesis***From:*Thomas Sewell

- Previous by Date: Re: [isabelle] default implementations for type classes
- Next by Date: Re: [isabelle] Error: Pending sort hypothesis
- 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