restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
authorhaftmann
Tue Oct 13 09:21:21 2015 +0200 (2015-10-13)
changeset 61425fb95d06fb21f
parent 61424 c3658c18b7bc
child 61426 d53db136e8fd
restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Tue Oct 13 09:21:15 2015 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Oct 13 09:21:21 2015 +0200
     1.3 @@ -353,6 +353,47 @@
     1.4    in [(@{const_syntax case_prod}, K case_prod_guess_names_tr')] end
     1.5  \<close>
     1.6  
     1.7 +text \<open>reconstruct pattern from (nested) @{const case_prod}s,
     1.8 +  avoiding eta-contraction of body; required for enclosing "let",
     1.9 +  if "let" does not avoid eta-contraction, which has been observed to occur\<close>
    1.10 +
    1.11 +print_translation \<open>
    1.12 +  let
    1.13 +    fun case_prod_tr' [Abs (x, T, t as (Abs abs))] =
    1.14 +          (* case_prod (\<lambda>x y. t) \<Rightarrow> \<lambda>(x, y) t *)
    1.15 +          let
    1.16 +            val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
    1.17 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
    1.18 +          in
    1.19 +            Syntax.const @{syntax_const "_abs"} $
    1.20 +              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.21 +          end
    1.22 +      | case_prod_tr' [Abs (x, T, (s as Const (@{const_syntax case_prod}, _) $ t))] =
    1.23 +          (* case_prod (\<lambda>x. (case_prod (\<lambda>y z. t))) \<Rightarrow> \<lambda>(x, y, z). t *)
    1.24 +          let
    1.25 +            val Const (@{syntax_const "_abs"}, _) $
    1.26 +              (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' =
    1.27 +                case_prod_tr' [t];
    1.28 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
    1.29 +          in
    1.30 +            Syntax.const @{syntax_const "_abs"} $
    1.31 +              (Syntax.const @{syntax_const "_pattern"} $ x' $
    1.32 +                (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
    1.33 +          end
    1.34 +      | case_prod_tr' [Const (@{const_syntax case_prod}, _) $ t] =
    1.35 +          (* case_prod (case_prod (\<lambda>x y z. t)) \<Rightarrow> \<lambda>((x, y), z). t *)
    1.36 +          case_prod_tr' [(case_prod_tr' [t])]
    1.37 +            (* inner case_prod_tr' creates next pattern *)
    1.38 +      | case_prod_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
    1.39 +          (* case_prod (\<lambda>pttrn z. t) \<Rightarrow> \<lambda>(pttrn, z). t *)
    1.40 +          let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
    1.41 +            Syntax.const @{syntax_const "_abs"} $
    1.42 +              (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
    1.43 +          end
    1.44 +      | case_prod_tr' _ = raise Match;
    1.45 +  in [(@{const_syntax case_prod}, K case_prod_tr')] end
    1.46 +\<close>
    1.47 +
    1.48  
    1.49  subsubsection \<open>Code generator setup\<close>
    1.50