Define sometimes requires eta-expanded recursive calls

[xrchz]

val _ = Hol_datatype`
  foo = C1 | C2 of foo list`

(* fails *)
val foo_def = Define`
  (foo f x C1 = x) ∧
  (foo f x (C2 ls) = FOLDL (foo f) x ls)`

(* succeeds *)
val foo'_def = tDefine "foo'"`
  (foo' f x C1 = x) ∧
  (foo' f x (C2 ls) = FOLDL (λx. foo' f x) x ls)`(
WF_REL_TAC `measure (foo_size o SND o SND)` THEN
Induct THEN SRW_TAC[][definition"foo_size_def"] THEN
RES_TAC THEN DECIDE_TAC)

val foo'_nice_def = SIMP_RULE (srw_ss()++boolSimps.ETA_ss) [] foo'_def

(* for comparison, this works *)
val bar_def = tDefine "bar"`
  (bar C1 = [F]) ∧
  (bar (C2 ls) = FLAT (MAP bar ls))`(
WF_REL_TAC `measure foo_size` THEN
Induct THEN SRW_TAC[][definition"foo_size_def"] THEN
RES_TAC THEN DECIDE_TAC)

It would be nice if Define could try various amounts of eta-expansion before "failure in internal translation to tupled format", and also clean up the resulting theorems.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.