[isabelle] Dependencies on constants



Dear Isabelle Gurus,

I am trying to find all theorems in a bunch of theories that don't (deeply) depend on a set of theorems in another bunch of theories.

Where I am completely lost is the definitions of constants. If I ask Isabelle, constant definitions do not depend on anything. That is, asking for the theorem dependencies of *_def usually results in nothing.
However, they do depend on other constants used in their definition.

For example, False_def involves use of "==" "False" and "All", so I argue that in my situation False_def depends on the definitions of "==" and "All". If those definitions exist in theories which I've tagged, then I should tag False_def as well and anything that uses the constant "False".

What I want is some way of discovering (even really slowly) "this is the first occurrence of a given constant; before this theorem it did not exist before". In the case of "False" this would be HOL.False_def. I realise that the concept of "before" may be problematic in a parallel environment, but although theories may be processed in parallel, I believe they still need to be put together in a specific order. The _def theorem for a definition cannot be successfully processed after a theorem that uses the definition's constant. If I could get a list of theorems in the order that they were defined/accepted/processed instead of alphabetically, I'd be able to pull it off.

I am not looking for elegance for now. Only: can this be done?

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?

I thank you in advance for any hints. Perhaps if I make this work, we can create a useful tool for automatically identifying generic lemmas. It may also improve the feature set of find_theorems.

Sincerely,

Rafal Kolanski.





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