[isabelle-dev] Typing problem in autogenerated axiom
Andreas Schropp
schropp at in.tum.de
Mon Nov 30 13:27:44 CET 2009
Florian Haftmann wrote:
>> 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.
>
Yes, but why is undefined only declared for HOL types then?
This is of course only one halve of the truth: sort constraints don't
matter in the kernel and thus undefined can be used on any type, but not
"officially" by users.
And more generally: why does axiomatization not do the strip_sorts
normalization?
All this leads to strangeness in the HOL->ZF translation, where I have
to introduce a fake constant in ZF to be the image of undefined on
non-HOL-types.
> Florian
>
>
More information about the isabelle-dev
mailing list