Re: [isabelle] mutual recdefs



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.

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.

- Brian

On Friday 10 March 2006 09:22, Peter Sewell wrote:
> Another naive question: I'd like to define several mutually recursive
> functions, eg (roughly) as is_val and is_exp in the example below.
> Looking in the tutorial I only see single examples - how would this be
> most nicely done?  (Presumably I could make a new disjoint sum type
> and work over that, but that seems ugly - though some plumbing of size
> functions is going to be needed somewhere.)
>
> ta,
> Peter
>
>
> 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"
>
> and C =
>    Ctx_pairL "exp"
>
>  | Ctx_pairR "exp"
>  | Ctx_appL "exp"
>  | Ctx_appR "exp"
>
> and Jop =
>    JO_red "exp*exp"
> and judgement =
>    judgement_Jop "Jop"
>
> consts is_val :: "exp => bool"
> is_C :: "C => bool"
> is_Jop :: "Jop => bool"
> is_exp :: "exp => bool"
> recdef is_val "measure (% x . size x)"
> "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"
> recdef is_C "measure (% x . size x)"
> "is_C (Ctx_pairL ( exp ) ) = (((is_exp exp)))"
> "is_C (Ctx_pairR ( val ) ) = (((is_val val)))"
> "is_C (Ctx_appL ( exp ) ) = (((is_exp exp)))"
> "is_C (Ctx_appR ( val ) ) = (((is_val val)))"
> recdef is_Jop "measure (% x . size x)"
> "is_Jop (JO_red ( e , e' ) ) = (((is_exp e) & (is_exp e')))"
> recdef is_exp "measure (% x . size x)"
> "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.