Email Gateway (Aug 18 2022 at 15:33): Email Gateway (Aug 18 2022 at 15:33):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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.
Email Gateway (Aug 18 2022 at 15:33):From: Tobias Nipkow <nipkow@in.tum.de>
This one is easy: for historical reasons certain basic constants are
unqualified. If you look into HOL.thy you'll find the keywords "global"
and "local" that control the naming. It is not advisable to use them
yourself.
Tobias
Email Gateway (Aug 18 2022 at 15:33):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Rafal,
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.
You might find the "Defs" table useful. E.g. try:
ML {* Defs.all_specifications_of (Theory.defs_of @{theory}) *}
Most if not all constants get registered in this table when they are defined (or introduced with the "axiomatization" command).
A more recent and in many ways more powerful approach is to use
ML {* Spec_Rules.get @{context} *}
The advantage of Spec_Rules is that it returns simplification rules for recursive functions rather than the raw definition, intro rules for (co)inductive predicates, etc.
I hope this helps.
Jasmin
Email Gateway (Aug 18 2022 at 15:34):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
I don't know for sure. I haven't ported my "Defs"-based code to "Spec_Rules" yet. Lukas uses "Spec_Rules" for the predicate compiler; maybe he has some insights to share.
I would definitely suggest you try with "Spec_Rules" first and use "Defs" as a fallback.
Jasmin
Email Gateway (Aug 18 2022 at 15:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rafal,
it depends what you actually aiming it. The Defs module represents the
proof theoretic aspect of definitions, i.e. constants which depend on
other constants. The Spec_Rules represent more the end-user view of
"initial specification".
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rafal,
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
signature.asc
Email Gateway (Aug 18 2022 at 15:34):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
What??
$ grep -l Spec_Rules ~/isabelle/src/HOL/Tools/{,/}
/Users/blanchet/isabelle/src/HOL/Tools/inductive.ML
/Users/blanchet/isabelle/src/HOL/Tools/old_primrec.ML
/Users/blanchet/isabelle/src/HOL/Tools/primrec.ML
/Users/blanchet/isabelle/src/HOL/Tools/recdef.ML
/Users/blanchet/isabelle/src/HOL/Tools/Function/function.ML
/Users/blanchet/isabelle/src/HOL/Tools/Function/size.ML
/Users/blanchet/isabelle/src/HOL/Tools/Nitpick/nitpick_hol.ML
/Users/blanchet/isabelle/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
I see primrec, recdef, and function/fun in there. Lukas's predicate compiler uses "Spec_Rules" to find equational specifications, so it must be working. Nitpick uses it already for the "(co)inductive" package and it's definitely working.
Cheers,
Jasmin
Email Gateway (Aug 18 2022 at 15:34):From: Gerwin Klein <gerwin.klein@nicta.com.au>
The difference may be because we're working on Isabelle 2009-1.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 15:34):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
On 23/06/10 18:05, Jasmin Blanchette wrote:
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.You might find the "Defs" table useful. E.g. try:
ML {* Defs.all_specifications_of (Theory.defs_of @{theory}) *}
Most if not all constants get registered in this table when they are
defined (or introduced with the "axiomatization" command).A more recent and in many ways more powerful approach is to use
ML {* Spec_Rules.get @{context} *}
That's amazing. I think it may be exactly what I've been looking for! I
really should have asked the list sooner rather than banging my head
against the wall for hours.
The advantage of Spec_Rules is that it returns simplification rules
for recursive functions rather than the raw definition, intro rules
for (co)inductive predicates, etc.
Is there any disadvantage you know of? For example, non-bizarre ways of
introducing constants that don't show up in this list?
I hope this helps.
Yes, it definitely does, thank you, Jasmin!
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 15:35):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
I've investigated Spec_Rules. It works as advertised for "definition"
and "constdefs", however the primrec/recdef/function/fun sadly do not
register their constants in this manner. I'll take a look at Defs now,
to see if those are workable.
Perhaps one day all packages will register with Spec_Rules? Who knows.
Still, for definitions and constdefs, this is already a step forward.
Cheers,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 15:35):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
I apologise, I failed to mention I'm on Isabelle 2009-1, working with on
the L4.verified repository. To me it looked like this:
[~/repos/l4.verified/isabelle]# rgrep -l Spec_Rules *
src/Pure/Isar/specification.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Isar/constdefs.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
Sorry. I'm glad Isabelle is, as usual, headed in the right direction.
Although as usual I'm a few steps behind.
I've finally hacked my way through the Defs interface. It was cryptic,
but consistent. Thank you for your help!
Sincerely,
Rafal Kolanski.
Last updated: Apr 26 2024 at 20:16 UTC