Re: [isabelle] mutual recdefs



I think the only mutual recursion we currently support is for mutually
recursive datatypes. Mutual recursion in general is in the pipeline...

Below you find a higher-order encoding of mutual recursion. It avoids having
to mess around with pairs but requires its own tricks. I had never tried this
before and it was a valuable exercise.

Tobias

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_val2 :: "(exp => bool) => exp => bool"
is_exp :: "exp => bool"

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

recdef is_exp "measure size"
"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_val2 is_exp val"

(* The real thing: *)
constdefs is_val :: "exp => bool"
 "is_val == is_val2 is_exp"

(* Deriving the real eqns: *)
lemma [simp]:
 "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"
by(simp_all add:is_val_def)

(* A complication: the final is_exp rule is more complicated than one
may naively expect. *)
thm is_exp.simps(6)

lemma is_val2_cong:
 "(!!e'. size e' < size e ==> f e' = g e') ==> is_val2 f e = is_val2 g e"
by (induct e) simp_all

lemma is_exp_foo[simp]: "is_exp (Exp_foo e) = is_val e"
by(simp add:is_val_def measure_def inv_image_def is_val2_cong)

declare is_exp.simps(6)[simp del]





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