Re: [isabelle] Possible unsoundness in axclass mechanism
Tom Ridge wrote:
Declaring an axclass IS a conservative extension. Actually, the theorem
"False" (lets call it L2) you see in your example theory is not the
theorem you actually get. When you finish your proof of L2 Isabelle
theory False = Main:
axclass blurg < type
blurg: "! x. x ~= x"
lemma l: "(x ~= (x::'a::blurg)) ==> 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.
### Pending sort hypotheses: blurg
This means that there are further hypotheses in your theorem L2 which
you don't see but which are nevertheless there. The specific hypothesis
in L2 says that there must exist a type 'a which is an instance of the
axiomatic type class blurg. Since you will never be able to exhibit such
a type, the hypothesis in L2 can never be discharged to result in a
hypotheses-free "False" theorem.
In order to check if your theorem contains such a meta-hypothesis you
have to use the ML level (as far as I know), for example:
This will result in the following output:
val it = "False" [.] : Thm.thm
The notation [.] tells you that there are further hypotheses hidden in
To make sort hypotheses explicit like normal assumptions in Isabelle you
would probably need (existential) type quantification.
-- Steven Obua
This archive was generated by a fusion of
Pipermail (Mailman edition) and