src/HOL/Library/LaTeXsugar.thy
changeset 66527 7ca69030a2af
parent 63935 aa1fe1103ab8
child 67386 998e01d6f8fd
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sun Aug 27 16:56:25 2017 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon Aug 28 18:27:16 2017 +0200
     1.3 @@ -128,5 +128,31 @@
     1.4  end
     1.5  \<close>
     1.6  
     1.7 +setup \<open>
     1.8 +let
     1.9 +
    1.10 +fun eta_expand Ts t xs = case t of
    1.11 +    Abs(x,T,t) =>
    1.12 +      let val (t', xs') = eta_expand (T::Ts) t xs
    1.13 +      in (Abs (x, T, t'), xs') end
    1.14 +  | _ =>
    1.15 +      let
    1.16 +        val (a,ts) = strip_comb t (* assume a atomic *)
    1.17 +        val (ts',xs') = fold_map (eta_expand Ts) ts xs
    1.18 +        val t' = list_comb (a, ts');
    1.19 +        val Bs = binder_types (fastype_of1 (Ts,t));
    1.20 +        val n = Int.min (length Bs, length xs');
    1.21 +        val bs = map Bound ((n - 1) downto 0);
    1.22 +        val xBs = ListPair.zip (xs',Bs);
    1.23 +        val xs'' = drop n xs';
    1.24 +        val t'' = fold_rev Term.abs xBs (list_comb(t', bs))
    1.25 +      in (t'', xs'') end
    1.26 +
    1.27 +val style_eta_expand =
    1.28 +  (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs))
    1.29 +
    1.30 +in Term_Style.setup @{binding eta_expand} style_eta_expand end
    1.31 +\<close>
    1.32 +
    1.33  end
    1.34  (*>*)