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



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.