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