[isabelle-dev] Typing problem in autogenerated axiom

[Andreas Schropp]

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
>