[isabelle-dev] Typing problem in autogenerated axiom
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Mon Nov 30 08:16:56 CET 2009
> 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
Indeed it is the other way round: the meta theory of HOL (also the
minimal HOL of Pure) demands non-emptiness of types. Postulating an
unspecified constants of an arbitrary type is always admissible.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091130/60fee5d4/attachment.sig>
More information about the isabelle-dev
mailing list