# HG changeset patch
# User paulson
# Date 1503948800 -3600
# Node ID 6e50b550adf5a72d86c3dbbf1d181c79774eba2f
# Parent  65c3c8fc83e4a7b9519dca1447c58824a3560579# Parent  e2249cd6df67db38e45945f5abd55ea7286de5a0
merged

diff -r e2249cd6df67 -r 6e50b550adf5 src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Mon Aug 28 20:33:08 2017 +0100
+++ b/src/Doc/Sugar/Sugar.thy	Mon Aug 28 20:33:20 2017 +0100
@@ -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}
 
diff -r e2249cd6df67 -r 6e50b550adf5 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Mon Aug 28 20:33:08 2017 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Mon Aug 28 20:33:20 2017 +0100
@@ -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
 (*>*)