[isabelle] Error: Pending sort hypothesis



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.