[isabelle] Strange eta-expansion on induction



Hi,

[Referring to Isabelle-2011-1]

I recently encountered a quite strange behavior of the induct method. It
seems to arbitrarily eta-expand its subgoals under certain conditions
(If the induction variable is nested inside higher-order context ???).

In the boiled-down example below, the first induct method fully
eta-expands its subgoals. In the second induct-method, the subgoals are
not eta-expanded, but the generated cases are. That is, on apply-style
scripts, you see eta-contracted goals, and when switching to ISAR, using
case-commands, you get eta-expanded goals.

Is this behavior somehow documented? Can I switch it off? 
In my concrete application, it kills my simplifier setup, as the
simplifier applies rules inside the eta-expanded terms that I do not
expect to be applied there.

Regards,
  Peter


--------------------------------------

declare [[eta_contract = false ]] (* Configure pretty-printer not to
eta-contract on pretty-printing *)

consts
  f :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
  i :: "('a list \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b
\<Rightarrow> bool)"

lemma "f (i xs s)"
  apply (induct xs)   (* Subgoals are fully eta-expanded here *)
  print_cases (* Cases are eta-expanded, too*)
  oops

lemma "f (i xs s)"
  apply (induct xs arbitrary: s) (* Subgoals are *NOT* eta-expanded here
*)
  print_cases  (* Cases are eta-expanded *)
  oops







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