*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Fri, 31 Oct 2014 17:03:35 +0100*In-reply-to*: <DD0DF2A3-DB63-463A-9B4A-29901389EF7E@uibk.ac.at>*References*: <DD0DF2A3-DB63-463A-9B4A-29901389EF7E@uibk.ac.at>

Short update: the behavior of BNF_LFP_Rec_Sugar.add_primrec_simple is also incompatible to the one of Primrec.add_primrec_simple, the latter has the expected behavior as Local_Theory.define: datatype someType = Constructor nat local_setup {* fn lthy => let val x = Free ("x", @{typ nat}) val fT = @{typ "someType => nat"} val (new,lthy) = Primrec.add_primrec_simple [((Binding.name "f", fT), NoSyn)] [HOLogic.mk_Trueprop (HOLogic.mk_eq (Free ("f",fT) $ (@{term Constructor} $ x), x))] lthy val _ = Output.urgent_message (@{make_string} new) in lthy end *} produces ("f", ([Free ("f", "someType ⇒ nat")], ["f (Constructor ?x) = ?x" [.]])) Moreover, it does not depend on whether one uses add_primrec_simple or add_primrec Best, René > Am 31.10.2014 um 16:03 schrieb René Thiemann <rene.thiemann at uibk.ac.at>: > > Dear all, > > I'm currently working with the Isabelle/ML-interface of the datatype_new command, where I'm defining some functions as follows: > > theory Scratch > imports Main > begin > datatype_new someType = Constructor nat > > (* primrec "f (Constructor x) = x" *) > > local_setup {* > fn lthy => > let > val x = Free ("x", @{typ nat}) > val fT = @{typ "someType => nat"} > val (info,lthy) = BNF_LFP_Rec_Sugar.add_primrec_simple [((Binding.name "f", fT), NoSyn)] > [HOLogic.mk_Trueprop (HOLogic.mk_eq (Free ("f",fT) $ (@{term Constructor} $ x), x))] lthy > val _ = Output.urgent_message (@{make_string} info) > in > lthy > end > *} > > (* output: (["f"], ([Free ("f", "someType ⇒ nat")], ([[0]], [["Scratch.f (Constructor x) = x"]]))) *) > > Whereas the primrec command indeed generates the intended function, I noticed some inconvenience in the returned > information "info": it contains the newly defined constant "h" as well as the simplification rules. > However, the level between the constant and the simp-rules is not in sync: > - the constant is still some free variable "Free 'f'" > - the simp-rules already speak about the global constant "Const (Scratch.f)" > > Is this the intended behavior? Or wouldn't it be more sensibly to return > "(Free f) (Constructor x) = x" as simp-rule? > (I prefer to stay in the current context) > > The behavior is also different from similar commands like Local_Theory.define where the > defining equation speaks about "Free g", and not about "Const (Scratch.g)" > > (* definition g :: nat => nat where "g = % x. x" *) > > local_setup {* > fn lthy => > let > val x = Free ("x", @{typ nat}) > val gT = @{typ "nat => nat"} > val (info,lthy) = Local_Theory.define ((Binding.name "g", NoSyn), ((Binding.name "g_def", []), > (lambda x x))) lthy > val _ = Output.urgent_message (@{make_string} info) > in > lthy > end > *} > > (* output: (Free ("g", "nat ⇒ nat"), ("local.g_def", "g ≡ λx. x" [.])) *) > > Best regards, > René >

**Follow-Ups**:**Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...***From:*Dmitriy Traytel

**References**:**[isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...***From:*René Thiemann

- Previous by Date: Re: [isabelle] Case-combinator allows qualified names for bound variables
- Next by Date: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- Previous by Thread: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- Next by Thread: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list