Re: [isabelle] Dependencies on constants




On 24/06/10 07:05, Jasmin Blanchette wrote:
Am 23.06.2010 um 18:44 schrieb Rafal Kolanski:

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.

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.

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.





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