*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Fri, 31 Oct 2014 16:03:45 +0100

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:*René Thiemann

- Previous by Date: [isabelle] Case-combinator allows qualified names for bound variables
- Next by Date: Re: [isabelle] Case-combinator allows qualified names for bound variables
- Previous by Thread: Re: [isabelle] Case-combinator allows qualified names for bound variables
- 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