--- a/src/Doc/Sugar/Sugar.thy Sat Aug 26 18:58:40 2017 +0200
+++ b/src/Doc/Sugar/Sugar.thy Mon Aug 28 18:27:21 2017 +0200
@@ -200,6 +200,24 @@
\showout @{thm split_paired_All[rename_abs _ l r]}
\end{quote}
+Sometimes Isabelle $\eta$-contracts terms, for example in the following definition:
+*}
+fun eta where
+"eta (x \<cdot> xs) = (\<forall>y \<in> set xs. x < y)"
+text{*
+\noindent
+If you now print the defining equation, the result is not what you hoped for:
+\begin{quote}
+\verb!@!\verb!{thm eta.simps}!\\
+\showout @{thm eta.simps}
+\end{quote}
+In such situations you can put the abstractions back by explicitly $\eta$-expanding upon output:
+\begin{quote}
+\verb!@!\verb!{thm (eta_expand z) eta.simps}!\\
+\showout @{thm (eta_expand z) eta.simps}
+\end{quote}
+Instead of a single variable \verb!z! you can give a whole list \verb!x y z!
+to perform multiple $\eta$-expansions.
\subsection{Inference rules}
--- a/src/HOL/Library/LaTeXsugar.thy Sat Aug 26 18:58:40 2017 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Mon Aug 28 18:27:21 2017 +0200
@@ -128,5 +128,31 @@
end
\<close>
+setup \<open>
+let
+
+fun eta_expand Ts t xs = case t of
+ Abs(x,T,t) =>
+ let val (t', xs') = eta_expand (T::Ts) t xs
+ in (Abs (x, T, t'), xs') end
+ | _ =>
+ let
+ val (a,ts) = strip_comb t (* assume a atomic *)
+ val (ts',xs') = fold_map (eta_expand Ts) ts xs
+ val t' = list_comb (a, ts');
+ val Bs = binder_types (fastype_of1 (Ts,t));
+ val n = Int.min (length Bs, length xs');
+ val bs = map Bound ((n - 1) downto 0);
+ val xBs = ListPair.zip (xs',Bs);
+ val xs'' = drop n xs';
+ val t'' = fold_rev Term.abs xBs (list_comb(t', bs))
+ in (t'', xs'') end
+
+val style_eta_expand =
+ (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs))
+
+in Term_Style.setup @{binding eta_expand} style_eta_expand end
+\<close>
+
end
(*>*)