[isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...



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.