[isabelle] primrec_new error: extra vars on RHS, option return type works



Hi,

I'm using `datatype_new` like this:

datatype_new hD = hEM | hS "hD fset"

I then get the `primrec_new` error, "Extra variables on the rhs", for this function:

primrec_new get_hS_FAILS :: "hD => hD fset" where
  "get_hS_FAILS hEM    = {||}"
 |"get_hS_FAILS (hS x) = x"

Fortunately, this function works for me, where I use `hD fset option` as the return type:

primrec_new opt_hS :: "hD => hD fset option" where
  "opt_hS hEM    = None"
 |"opt_hS (hS x) = Some x"

The end result is that I have to use three functions instead of the one.

Is there a simple fix for this? I attach the theory.

Thanks,
GB






theory i140123a
imports BNF (*"i"*)
begin

datatype_new hD = hEM | hS "hD fset"   

code_datatype hEM hS

(*ERROR: Extra variables on rhs: "(x::hD fset)".*)

primrec_new get_hS_FAILS :: "hD => hD fset" where
  "get_hS_FAILS hEM    = {||}"
 |"get_hS_FAILS (hS x) = x"
 
(*NOTE: Instead of one function, I have to use three, one of them being `the`.*)

primrec_new opt_hS :: "hD => hD fset option" where
  "opt_hS hEM    = None"
 |"opt_hS (hS x) = Some x"

abbreviation the_hS :: "hD => hD fset" where
  "the_hS x == the(opt_hS x)"
  
primrec_new get_hS :: "hD => hD fset" where
  "get_hS hEM    = {||}"
 |"get_hS (hS x) = the_hS(hS x)"
 
(*CHECK: I checked out my use of `primrec` using `list` instead of `fset`.*) 
 
datatype hD2 = hEM2 | hS2 "hD2 list" 

primrec get_hS2 :: "hD2 => hD2 list" where
  "get_hS2 hEM2    = []"
 |"get_hS2 (hS2 x) = x"
  
end


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