src/HOL/Tools/inductive_realizer.ML
changeset 46219 426ed18eba43
parent 45839 43a5b86bc102
child 46708 b138dee7bed3
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Jan 14 20:05:58 2012 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 14 21:16:15 2012 +0100
     1.3 @@ -88,8 +88,9 @@
     1.4            val u = list_comb (t, map Bound (i - 1 downto 0))
     1.5          in 
     1.6            if member (op =) vs a then
     1.7 -            list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
     1.8 -          else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
     1.9 +            fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u)
    1.10 +          else
    1.11 +            fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u)
    1.12          end
    1.13    | gen_rvar _ t = t;
    1.14  
    1.15 @@ -164,24 +165,25 @@
    1.16                  let
    1.17                    val prem' :: prems' = prems;
    1.18                    val U = Extraction.etype_of thy vs [] prem';
    1.19 -                in if U = Extraction.nullT
    1.20 +                in
    1.21 +                  if U = Extraction.nullT
    1.22                    then fun_of (Free (x, T) :: ts)
    1.23                      (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
    1.24                      (Free (x, T) :: args) (x :: r :: used) prems'
    1.25                    else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
    1.26                      (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
    1.27                  end
    1.28 -              else (case strip_type T of
    1.29 +              else
    1.30 +                (case strip_type T of
    1.31                    (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
    1.32                      let
    1.33                        val fx = Free (x, Ts ---> T1);
    1.34                        val fr = Free (r, Ts ---> T2);
    1.35                        val bs = map Bound (length Ts - 1 downto 0);
    1.36 -                      val t = list_abs (map (pair "z") Ts,
    1.37 -                        HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
    1.38 -                    in fun_of (fx :: ts) (fr :: rts) (t::args)
    1.39 -                      (x :: r :: used) prems
    1.40 -                    end
    1.41 +                      val t =
    1.42 +                        fold_rev (Term.abs o pair "z") Ts
    1.43 +                          (HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)));
    1.44 +                    in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end
    1.45                  | (Ts, U) => fun_of (Free (x, T) :: ts)
    1.46                      (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
    1.47                      (Free (x, T) :: args) (x :: r :: used) prems)
    1.48 @@ -439,13 +441,16 @@
    1.49          val T' = Extraction.etype_of thy (vs @ Ps) [] p;
    1.50          val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
    1.51          val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
    1.52 -        val r = if null Ps then Extraction.nullt
    1.53 -          else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
    1.54 -            (if dummy then
    1.55 -               [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
    1.56 -             else []) @
    1.57 -            map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
    1.58 -            [Bound (length prems)]));
    1.59 +        val r =
    1.60 +          if null Ps then Extraction.nullt
    1.61 +          else
    1.62 +            fold_rev (Term.abs o pair "x") Ts
    1.63 +              (list_comb (Const (case_name, T),
    1.64 +                (if dummy then
    1.65 +                   [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
    1.66 +                 else []) @
    1.67 +                map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
    1.68 +                [Bound (length prems)]));
    1.69          val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
    1.70          val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
    1.71          val rews = map mk_meta_eq case_thms;