Re: [isabelle] mutual recdefs



Brian Huffman writes:
>You could actually define these functions together using primrec: Since 
>recursive calls are only made on subterms, you don't really need the full 
>power of recdef.

that's true in this case, indeed.

>However, using primrec is complicated by the fact that you have used product 
>types as arguments to your constructors. This is actually an instance of 
>indirect recursion, which means you would be required to additionally define 
>several extra constants which take the product types as arguments. If you 
>change your datatype definitions so that the constructors have two separate 
>arguments instead of a pair, then primrec should work just fine.

But that seems not to be.  As far as I can tell it's impossible to 
define multiple mutually-recursive functions over the same types, eg the

  is_val :: "exp => bool"
  is_exp :: "exp => bool"

in the example below, using either primrec or recdef.  Is that really the case?
Clearly I could encode, with something like

  is_val_is_exp :: "exp => (bool * bool) "

and Tom Ridge points out that I can then prove lemmas characterising
the projections of that that look like my original definition.  
But I don't want to do that encoding unless I have to...

thanks,
Peter




(* here is_val and is_exp define two sub-grammars of the free exp *)
theory Out = Main:
types ident = "string"
datatype 
exp = 
   Exp_ident "ident"
 | Exp_unit 
 | Exp_pair "exp" "exp"
 | Exp_fun "ident" "exp"
 | Exp_app "exp" "exp"
 | Exp_foo "exp"

consts
is_val :: "exp => bool"
is_exp :: "exp => bool"

primrec
"is_val ((Exp_ident x)) = (True)"
"is_val (Exp_unit) = (True)"
"is_val ((Exp_pair exp exp')) = (((is_val exp) & (is_val exp')))"
"is_val ((Exp_fun x exp)) = (((is_exp exp)))"
"is_val ((Exp_app exp exp')) = False"
"is_val ((Exp_foo val)) = False"

"is_exp ((Exp_ident x)) = (True)"
"is_exp (Exp_unit) = (True)"
"is_exp ((Exp_pair exp exp')) = (((is_exp exp) & (is_exp exp')))"
"is_exp ((Exp_fun x exp)) = (((is_exp exp)))"
"is_exp ((Exp_app exp exp')) = (((is_exp exp) & (is_exp exp')))"
"is_exp ((Exp_foo val)) = (((is_val val)))"






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