Re: [isabelle] Possible unsoundness in axclass mechanism



Hi Tom,

> theory False = Main:
> 
> axclass blurg < type
>    blurg: "! x. x ~= x"
> 
> lemma l: "(x ~= (x::'a::blurg)) ==> False"
>    apply(simp)
>    done
> 
> lemma "False"
>    apply(rule l[of "x"])
>    apply(simp only: blurg)
>    apply(simp)
>    done

When finishing the questionable theorem you get the message

### Pending sort hypotheses: blurg

Sort hypotheses are additional hypotheses which state that certain type classes
must be consistent for the theorem to hold. So what you proved is actually "If
there is a type satisfying axiom blurg, then False".

Sort hypotheses are tracked by the system and are usually automatically resolved
my making use of proven instances for the axclasses. If there is no such
instance, this fails and you get the above warning.

You can get a list of unsolved sort hypotheses of a theorem by

ML {* extra_shyps (thm "thm_name") *}

So, what was your instance for "blurg" again?

Alex





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