src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 49682 f57af1c46f99
parent 49681 aa66ea552357
child 49683 78a3d5006cf1
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 02 01:00:18 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 02 01:00:18 2012 +0200
     1.3 @@ -113,8 +113,6 @@
     1.4      Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
     1.5    | _ => replicate n false);
     1.6  
     1.7 -fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
     1.8 -
     1.9  fun tack z_name (c, u) f =
    1.10    let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
    1.11      Term.lambda z (mk_sum_case (Term.lambda u u, Term.lambda c (f $ c)) $ z)
    1.12 @@ -546,7 +544,7 @@
    1.13              val cxIns = map2 (mk_cIn I) tuple_xs ks;
    1.14              val cyIns = map2 (mk_cIn B_ify) tuple_ys ks;
    1.15  
    1.16 -            fun mk_map_thm ctr_def' xs cxIn =
    1.17 +            fun mk_map_thm ctr_def' cxIn =
    1.18                fold_thms lthy [ctr_def']
    1.19                  (unfold_thms lthy (pre_map_def ::
    1.20                       (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
    1.21 @@ -554,21 +552,21 @@
    1.22                        (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
    1.23                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
    1.24  
    1.25 -            fun mk_set_thm fp_set_thm ctr_def' xs cxIn =
    1.26 +            fun mk_set_thm fp_set_thm ctr_def' cxIn =
    1.27                fold_thms lthy [ctr_def']
    1.28                  (unfold_thms lthy (pre_set_defs @ nested_set_natural's @ nesting_set_natural's @
    1.29                       (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
    1.30                     (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
    1.31                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
    1.32  
    1.33 -            fun mk_set_thms fp_set_thm = map3 (mk_set_thm fp_set_thm) ctr_defs' xss cxIns;
    1.34 +            fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns;
    1.35  
    1.36 -            val map_thms = map3 mk_map_thm ctr_defs' xss cxIns;
    1.37 +            val map_thms = map2 mk_map_thm ctr_defs' cxIns;
    1.38              val set_thmss = map mk_set_thms fp_set_thms;
    1.39  
    1.40 -            val rel_infos = (ctr_defs' ~~ xss ~~ cxIns, ctr_defs' ~~ yss ~~ cyIns);
    1.41 +            val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
    1.42  
    1.43 -            fun mk_rel_thm postproc ctr_defs' xs cxIn ys cyIn =
    1.44 +            fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
    1.45                fold_thms lthy ctr_defs'
    1.46                   (unfold_thms lthy (pre_rel_def :: (if lfp then [] else [dtor_ctor]) @
    1.47                        sum_prod_thms_rel)
    1.48 @@ -576,14 +574,14 @@
    1.49                |> postproc
    1.50                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
    1.51  
    1.52 -            fun mk_rel_inject_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
    1.53 -              mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] xs cxIn ys cyIn;
    1.54 +            fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
    1.55 +              mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
    1.56  
    1.57              val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
    1.58  
    1.59 -            fun mk_half_rel_distinct_thm (((xctr_def', xs), cxIn), ((yctr_def', ys), cyIn)) =
    1.60 +            fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
    1.61                mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
    1.62 -                xs cxIn ys cyIn;
    1.63 +                cxIn cyIn;
    1.64  
    1.65              fun mk_other_half_rel_distinct_thm thm =
    1.66                flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
    1.67 @@ -824,26 +822,24 @@
    1.68                fold_rev (fold_rev Logic.all) (xs :: fss)
    1.69                  (mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
    1.70  
    1.71 -            fun build_rec_like frec_likes maybe_tick (T, U) =
    1.72 +            fun build_rec_like frec_likes (T, U) =
    1.73                if T = U then
    1.74                  id_const T
    1.75                else
    1.76                  (case find_index (curry (op =) T) fpTs of
    1.77 -                  ~1 => build_map (build_rec_like frec_likes maybe_tick) T U
    1.78 -                | kk => maybe_tick (nth us kk) (nth frec_likes kk));
    1.79 +                  ~1 => build_map (build_rec_like frec_likes) T U
    1.80 +                | kk => nth frec_likes kk);
    1.81  
    1.82 -            fun mk_U maybe_mk_prodT =
    1.83 -              typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
    1.84 +            val mk_U = typ_subst (map2 pair fpTs Cs);
    1.85  
    1.86 -            fun intr_rec_likes frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
    1.87 +            fun intr_rec_likes frec_likes maybe_cons (x as Free (_, T)) =
    1.88                if exists_fp_subtype T then
    1.89 -                maybe_cons x [build_rec_like frec_likes (K I) (T, mk_U (K I) T) $ x]
    1.90 +                maybe_cons x [build_rec_like frec_likes (T, mk_U T) $ x]
    1.91                else
    1.92                  [x];
    1.93  
    1.94 -            val gxsss = map (map (maps (intr_rec_likes gfolds (K I) (K I) (K I)))) xsss;
    1.95 -            val hxsss =
    1.96 -              map (map (maps (intr_rec_likes hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
    1.97 +            val gxsss = map (map (maps (intr_rec_likes gfolds (K I)))) xsss;
    1.98 +            val hxsss = map (map (maps (intr_rec_likes hrecs cons))) xsss;
    1.99  
   1.100              val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
   1.101              val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;