# [isabelle] mutual recdefs

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.*