Re: [isabelle] Possible unsoundness in axclass mechanism



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.

T

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 tells you:

### 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:

ML {*
 thm "L2"
*}

This will result in the following output:

val it = "False" [.] : Thm.thm

The notation [.] tells you that there are further hypotheses hidden in the theorem.

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 MHonArc.