*To*: René Thiemann <rene.thiemann at uibk.ac.at>, Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Thu, 13 Nov 2014 15:07:02 +0100*In-reply-to*: <5453C039.9010008@in.tum.de>*References*: <DD0DF2A3-DB63-463A-9B4A-29901389EF7E@uibk.ac.at> <6C845AD1-6EB9-494A-A5F8-E8E792BE1F4D@uibk.ac.at> <5453C039.9010008@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

It should be better with 1ae67039b14f. Dmitriy On 31.10.2014 18:00, Dmitriy Traytel wrote:

Hi René,indeed the terms and the theorems should be in sync. I can not tell atthe moment if both will be about Free's (monomorphic) or about Const's(polymorphic). This depends on fact whether the polymorphism is neededfor something internal or not. I'll have a closer look next week.Thanks for the report, Dmitriy On 31.10.2014 17:03, René Thiemann wrote:Short update:the behavior of BNF_LFP_Rec_Sugar.add_primrec_simple is alsoincompatible 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) $ (@{termConstructor} $ x), x))] lthyval _ = 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_simpleor add_primrecBest, 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 thedatatype_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) $ (@{termConstructor} $ x), x))] lthyval _ = 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 returnedinformation "info": it contains the newly defined constant "h" aswell as the simplification rules.However, the level between the constant and the simp-rules is not insync:- 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 toreturn"(Free f) (Constructor x) = x" as simp-rule? (I prefer to stay in the current context)The behavior is also different from similar commands likeLocal_Theory.define where thedefining 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:*René Thiemann

- Previous by Date: Re: [isabelle] Generic Contexts and Generic Data
- Next by Date: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- Previous by Thread: Re: [isabelle] primcorec error: Type unification failed
- Next by Thread: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- Cl-isabelle-users November 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