# Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...

```Hi René,

```
indeed the terms and the theorems should be in sync. I can not tell at the moment if both will be about Free's (monomorphic) or about Const's (polymorphic). This depends on fact whether the polymorphism is needed for 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 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'"

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

(* 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é

```
```
```
```

```

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