src/HOL/Product_Type.thy
changeset 42247 12fe41a92cd5
parent 42083 e1209fc7ecdc
child 42284 326f57825e1a
equal deleted inserted replaced
42246:8f798ba04393 42247:12fe41a92cd5
   230 *}
   230 *}
   231 
   231 
   232 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
   232 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
   233 typed_print_translation {*
   233 typed_print_translation {*
   234 let
   234 let
   235   fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
   235   fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
   236     | split_guess_names_tr' _ T [Abs (x, xT, t)] =
   236     | split_guess_names_tr' T [Abs (x, xT, t)] =
   237         (case (head_of t) of
   237         (case (head_of t) of
   238           Const (@{const_syntax prod_case}, _) => raise Match
   238           Const (@{const_syntax prod_case}, _) => raise Match
   239         | _ =>
   239         | _ =>
   240           let 
   240           let 
   241             val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   241             val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   243             val (x', t'') = atomic_abs_tr' (x, xT, t');
   243             val (x', t'') = atomic_abs_tr' (x, xT, t');
   244           in
   244           in
   245             Syntax.const @{syntax_const "_abs"} $
   245             Syntax.const @{syntax_const "_abs"} $
   246               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   246               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   247           end)
   247           end)
   248     | split_guess_names_tr' _ T [t] =
   248     | split_guess_names_tr' T [t] =
   249         (case head_of t of
   249         (case head_of t of
   250           Const (@{const_syntax prod_case}, _) => raise Match
   250           Const (@{const_syntax prod_case}, _) => raise Match
   251         | _ =>
   251         | _ =>
   252           let
   252           let
   253             val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   253             val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   255             val (x', t'') = atomic_abs_tr' ("x", xT, t');
   255             val (x', t'') = atomic_abs_tr' ("x", xT, t');
   256           in
   256           in
   257             Syntax.const @{syntax_const "_abs"} $
   257             Syntax.const @{syntax_const "_abs"} $
   258               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   258               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   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)"
   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.
   265    where Q is some bounded quantifier or set operator.