Re: [isabelle] Dependencies on constants



Hi Rafal,

> Also, a simpler issue: for some reason I can't figure out the rules
> about fully-qualified names of constants in theorems. E.g. if I make a
> definition "zulu" in theory Deps, @{const zulu} comes back as:
>   Const ("Dependencies.zulu", "nat \<Rightarrow> bool") : term
> but if I ask about "False" it comes back with:
>   Const ("False", "bool") : term
> What's more, HOL.False does not exist as a constant.
> I'm confused about the rules for when I can count on a fully-qualified
> name and when not. Can you offer any advice?

the rules in the strictest sense are not fixed;  introducing new named
entities happens through ML functions in Pure/General/name_space.ML

val declare: bool -> naming -> binding -> Name_Space.T -> string *
Name_Space.T

Here "binding" is a name hint which is expanded to a full name according
to a policy set by a "naming";  the resulting full name and the updated
name space are returned.

val define: bool -> naming -> binding * 'a -> Name_Space.T * 'a
Symtab.table -> string * Name_Space.T * 'a Symtab.table

Usually the name space is coupled with a table which contains entry data
for the newly defined named entity.

Hope this helps,
	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

Attachment: signature.asc
Description: OpenPGP digital signature



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