Re: [isabelle] all Re: [Fwd: Re: Qualified name for Set.insert]



On Mon, 27 Jul 2009, Christian Sternagel wrote:

I think a related issue is that it is not possible to use the identifier 'all', e.g., I wanted to have the list function

primrec all :: "('a => bool) => 'a list => bool"
where "all p [] = True"
   | "all p (x#xs) = (p x \<and> all p xs)"

The definition ran through... however, at some later point I tried to use a formula of the form "!!x. ?P x" and there I got a type error. Would this problem also be solved if the internal constant for `!!' would be qualified... or is it a different problem?

P.S.: is there some workaround that lets me use the function name 'all'?

The Pure quantifier is called "all" internally -- this is a global name with "non-authentic" syntax. This means there is no way to use that base name in some user theory -- neither name space accesses nor notation can be modified later without breakdown.

While we have worked hard to reduce the number of (historical) global constants like this for HOL (and the process is not really finished yet), this is even harder for Pure. So global names are likely to persist there for > 10 more years.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.