Re: [isabelle] Possible unsoundness in axclass mechanism
On Wed, 14 Sep 2005, Tom Ridge wrote:
> theory False = Main:
> axclass blurg < type
> blurg: "! x. x ~= x"
> lemma l: "(x ~= (x::'a::blurg)) ==> False"
> lemma "False"
> apply(rule l[of "x"])
> apply(simp only: blurg)
> Is this supposed to happen? I thought declaring an axclass was supposed
> to be a conservative extension.
Yes, it is even a definitional one in the strict sense. The above merely
proves False under the assumption of "! x. x ~= x", i.e. False again.
The system warns you about that additional hypotheses, but does not print
it by default. Try ML "set show_hyps" to see more details.
This archive was generated by a fusion of
Pipermail (Mailman edition) and