tuning
authorblanchet
Mon Apr 29 13:47:46 2013 +0200 (2013-04-29)
changeset 518148b89afea27e7
parent 51813 ca201253e7bb
child 51815 efacb9b99865
tuning
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:42:54 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:47:46 2013 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4      val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
     1.5    in Term.list_comb (rel, map build_arg Ts') end;
     1.6  
     1.7 -fun derive_induct_fold_rec_thms_for_types nn pre_bnfs fp_induct fp_fold_thms fp_rec_thms
     1.8 +fun derive_induct_fold_rec_thms_for_types nn pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
     1.9      nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
    1.10      fold_defs rec_defs lthy =
    1.11    let
    1.12 @@ -286,7 +286,7 @@
    1.13  
    1.14          val kksss = map (map (map (fst o snd) o #2)) raw_premss;
    1.15  
    1.16 -        val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.17 +        val ctor_induct' = ctor_induct OF (map mk_sumEN_tupled_balanced mss);
    1.18  
    1.19          val thm =
    1.20            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.21 @@ -333,11 +333,11 @@
    1.22          val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
    1.23  
    1.24          val fold_tacss =
    1.25 -          map2 (map o mk_rec_like_tac pre_map_defs [] nesting_map_ids'' fold_defs) fp_fold_thms
    1.26 +          map2 (map o mk_rec_like_tac pre_map_defs [] nesting_map_ids'' fold_defs) ctor_fold_thms
    1.27              ctr_defss;
    1.28          val rec_tacss =
    1.29            map2 (map o mk_rec_like_tac pre_map_defs nested_map_comp's
    1.30 -            (nested_map_ids'' @ nesting_map_ids'') rec_defs) fp_rec_thms ctr_defss;
    1.31 +            (nested_map_ids'' @ nesting_map_ids'') rec_defs) ctor_rec_thms ctr_defss;
    1.32  
    1.33          fun prove goal tac =
    1.34            Goal.prove_sorry lthy [] [] goal (tac o #context)
    1.35 @@ -352,10 +352,10 @@
    1.36       (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
    1.37    end;
    1.38  
    1.39 -fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs fp_induct
    1.40 -    fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As kss mss
    1.41 -    ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress unfolds corecs
    1.42 -    unfold_defs corec_defs lthy =
    1.43 +fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs dtor_coinduct
    1.44 +    dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs
    1.45 +    As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
    1.46 +    unfolds corecs unfold_defs corec_defs lthy =
    1.47    let
    1.48      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.49      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
    1.50 @@ -449,7 +449,7 @@
    1.51            |> Drule.zero_var_indexes
    1.52            |> `(conj_dests nn);
    1.53        in
    1.54 -        (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
    1.55 +        (postproc nn (prove dtor_coinduct goal), postproc nn (prove dtor_strong_induct strong_goal))
    1.56        end;
    1.57  
    1.58      fun mk_coinduct_concls ms discs ctrs =
    1.59 @@ -522,11 +522,11 @@
    1.60  
    1.61          val unfold_tacss =
    1.62            map3 (map oo mk_corec_like_tac unfold_defs [] [] nesting_map_ids'' [])
    1.63 -            fp_fold_thms pre_map_defs ctr_defss;
    1.64 +            dtor_unfold_thms pre_map_defs ctr_defss;
    1.65          val corec_tacss =
    1.66            map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
    1.67                (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
    1.68 -            fp_rec_thms pre_map_defs ctr_defss;
    1.69 +            dtor_corec_thms pre_map_defs ctr_defss;
    1.70  
    1.71          fun prove goal tac =
    1.72            Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;