src/HOL/Product_Type.thy
changeset 42059 83f3dc509068
parent 41792 ff3cb0c418b7
child 42083 e1209fc7ecdc
equal deleted inserted replaced
42058:1eda69f0b9a8 42059:83f3dc509068
   259           end)
   259           end)
   260     | split_guess_names_tr' _ _ _ = raise Match;
   260     | split_guess_names_tr' _ _ _ = raise Match;
   261 in [(@{const_syntax prod_case}, split_guess_names_tr')] end
   261 in [(@{const_syntax prod_case}, split_guess_names_tr')] end
   262 *}
   262 *}
   263 
   263 
       
   264 (* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
       
   265    where Q is some bounded quantifier or set operator.
       
   266    Reason: the above prints as "Q p : A. case p of (x,y) \<Rightarrow> P x y"
       
   267    whereas we want "Q (x,y):A. P x y".
       
   268    Otherwise prevent eta-contraction.
       
   269 *)
       
   270 print_translation {*
       
   271 let
       
   272   fun contract Q f ts =
       
   273     case ts of
       
   274       [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
       
   275       => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
       
   276     | _ => f ts;
       
   277   fun contract2 (Q,f) = (Q, contract Q f);
       
   278   val pairs =
       
   279     [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
       
   280      Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
       
   281      Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
       
   282      Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
       
   283 in map contract2 pairs end
       
   284 *}
   264 
   285 
   265 subsubsection {* Code generator setup *}
   286 subsubsection {* Code generator setup *}
   266 
   287 
   267 code_type prod
   288 code_type prod
   268   (SML infix 2 "*")
   289   (SML infix 2 "*")