*To*: Thomas Sewell <Thomas.Sewell at nicta.com.au>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Error: Pending sort hypothesis*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Mon, 12 Oct 2009 17:32:49 +0200*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.22 (X11/20090605)

Hi Thomas, My hope was that ATP would find a proof based on the lemma "finite_imp_nat_seg_image_inj_on" that is, in some sense, the inverse of my lemma. In the meantime, I proved the lemma directly with induction over the finite set (no idea whether this is more elegant ;) ): -- "Finite sets have an injective mapping to an initial segments of the natural numbers" lemma finite_imp_inj_to_nat_seg: fixes A :: "'a set" assumes A: "finite A" obtains f::"'a \<Rightarrow> nat" and n::"nat" where "f`A = {i. i<n}" "inj_on f A" proof - from A have "\<exists>f (n::nat). f`A = {i. i<n} \<and> inj_on f A" proof (induct) case empty thus ?case by auto next case (insert x A) then obtain f and n::nat where IH: "f`A = {i. i<n}" "inj_on f A" by auto let ?fs = "f(x:=n)" from IH insert(2) have "?fs`(insert x A) = {i. i<Suc n}" "inj_on ?fs (insert x A)" apply - apply force apply simp apply (rule inj_onI) apply (auto dest: inj_onD split: split_if_asm) done thus ?case by blast qed with that show ?thesis by blast qed regards, Peter 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] Error: Pending sort hypothesis
- Next by Date: [isabelle] parametric typedef?
- 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