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



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 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'"
- 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é








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