Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...

Email Gateway (Aug 19 2022 at 16:14):

From: René Thiemann <rene.thiemann@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é

Email Gateway (Aug 19 2022 at 16:14):

From: René Thiemann <rene.thiemann@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é

Email Gateway (Aug 19 2022 at 16:14):

From: Dmitriy Traytel <traytel@in.tum.de>
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

Email Gateway (Aug 19 2022 at 16:39):

From: Dmitriy Traytel <traytel@in.tum.de>
It should be better with 1ae67039b14f.

Dmitriy

Email Gateway (Aug 19 2022 at 16:39):

From: René Thiemann <rene.thiemann@uibk.ac.at>

It should be better with 1ae67039b14f.

Thanks, works perfectly now.

René

Last updated: Nov 21 2024 at 12:39 UTC