[isabelle-dev] Typing problem in autogenerated axiom

Andreas Schropp schropp at in.tum.de
Sun Nov 29 18:19:18 CET 2009

Florian Haftmann wrote:
> Sort constraints on constants are just a pecularity of the parser (and
> can be changed internally, c.f. Sign.add_const_constraint), *not* a part
> of the logical foundation.  To understand, imagine you write down a
> "nonsense" term like "(x, y) = 0" ignoring the sort constraint ::zero on
> 0.  But this does not lead to problems since the only way to give
> "meaning" to this term is to instantiate it into theorems, where all
> relevant theorems involving 0 have a ::zero constraint.
> So, sort constraints are not relevant to definitions or constant
> signatures, but to theorems where they carry logical content.

I dont think this is (already) true for axiomatized constants.
If the HOL constant undefined :: 'a :: {HOL.type} (aka arbitrary) should 
witness only nonemptyness of HOL types,
then its sort constraint is important.

Perhaps this is debatable, as one can always prove nonemptyness of 
arbitrary types via hidden variables:

  metaex :: "('a::{} => prop) => prop"
  "metaex P == (!! Q. (!! x. PROP (P x) ==> PROP Q) ==> PROP Q)"

lemma meta_nonempty : "PROP metaex (% x::'a::{}. x == x)"
 unfolding metaex_def
 proof -
  fix Q
  assume H: "(!!x::'a. x == x ==> PROP Q)"
  have A: "y::'a::{} == y ==> PROP Q" by(rule H)
  have B: "y::'a::{} == y" by(rule Pure.reflexive)
  show "PROP Q" by(rule A[OF B])

> ------------------------------------------------------------------------
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list