Re: [isabelle] Strange eta-expansion on induction



The induct method itself does not eta-contract or expand. It merely uses
primitives, in particular resolution, which in turn uses higher-order
unification. And higher-order unification does indeed eta-expand. In
certain situations. This is intentionally not fixed and you should not
expect or rely on a particular behaviour. That is, you may have to
ensure eta-contraction yourself if some part of your proof method is
sensitive to it.

Tobias

Am 01/03/2012 18:53, schrieb Peter Lammich:
> 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.