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"
>    apply(simp)
>    done
> 
> lemma "False"
>    apply(rule l[of "x"])
>    apply(simp only: blurg)
>    apply(simp)
>    done
> 
> end
> 
> 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.


	Makarius






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