[isabelle] Error: Pending sort hypothesis

Hi all,

I wanted to prove the following 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
  (* Here, Isabelle sais: No subgoals
  However, when finnishing the proof: *)
  (* 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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.