fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
authornipkow
Tue Mar 22 12:49:07 2011 +0100 (2011-03-22)
changeset 4205983f3dc509068
parent 42058 1eda69f0b9a8
child 42060 889d767ce5f4
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Mon Mar 21 21:10:29 2011 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Mar 22 12:49:07 2011 +0100
     1.3 @@ -261,6 +261,27 @@
     1.4  in [(@{const_syntax prod_case}, split_guess_names_tr')] end
     1.5  *}
     1.6  
     1.7 +(* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
     1.8 +   where Q is some bounded quantifier or set operator.
     1.9 +   Reason: the above prints as "Q p : A. case p of (x,y) \<Rightarrow> P x y"
    1.10 +   whereas we want "Q (x,y):A. P x y".
    1.11 +   Otherwise prevent eta-contraction.
    1.12 +*)
    1.13 +print_translation {*
    1.14 +let
    1.15 +  fun contract Q f ts =
    1.16 +    case ts of
    1.17 +      [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
    1.18 +      => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
    1.19 +    | _ => f ts;
    1.20 +  fun contract2 (Q,f) = (Q, contract Q f);
    1.21 +  val pairs =
    1.22 +    [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
    1.23 +     Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
    1.24 +     Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
    1.25 +     Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
    1.26 +in map contract2 pairs end
    1.27 +*}
    1.28  
    1.29  subsubsection {* Code generator setup *}
    1.30