[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:
definition
metaex :: "('a::{} => prop) => prop"
where
"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])
qed
>
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> 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