tune signatures
authorblanchet
Mon Apr 29 13:52:14 2013 +0200 (2013-04-29)
changeset 51815efacb9b99865
parent 51814 8b89afea27e7
child 51816 5f1dec4297da
tune signatures
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:47:46 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:52:14 2013 +0200
     1.3 @@ -7,14 +7,13 @@
     1.4  
     1.5  signature BNF_FP_DEF_SUGAR =
     1.6  sig
     1.7 -  val derive_induct_fold_rec_thms_for_types: int -> BNF_Def.BNF list -> thm -> thm list ->
     1.8 -    thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
     1.9 -    typ list list list -> int list list -> int list -> term list list -> term list list ->
    1.10 -    term list list -> term list list list -> thm list list -> term list -> term list -> thm list ->
    1.11 -    thm list -> Proof.context ->
    1.12 +  val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> thm -> thm list -> thm list ->
    1.13 +    BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list -> typ list list list ->
    1.14 +    int list list -> int list -> term list list -> term list list -> term list list -> term list
    1.15 +    list list -> thm list list -> term list -> term list -> thm list -> thm list -> Proof.context ->
    1.16      (thm * thm list * Args.src list) * (thm list list * Args.src list)
    1.17        * (thm list list * Args.src list)
    1.18 -  val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context -> int ->
    1.19 +  val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context ->
    1.20      BNF_Def.BNF list -> thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list ->
    1.21      BNF_Def.BNF list -> typ list -> typ list -> typ list -> int list list -> int list list ->
    1.22      int list -> term list -> term list list -> term list list -> term list list list list ->
    1.23 @@ -199,10 +198,12 @@
    1.24      val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
    1.25    in Term.list_comb (rel, map build_arg Ts') end;
    1.26  
    1.27 -fun derive_induct_fold_rec_thms_for_types nn pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
    1.28 +fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
    1.29      nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
    1.30      fold_defs rec_defs lthy =
    1.31    let
    1.32 +    val nn = length pre_bnfs;
    1.33 +
    1.34      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.35      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    1.36      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
    1.37 @@ -352,11 +353,13 @@
    1.38       (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
    1.39    end;
    1.40  
    1.41 -fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs dtor_coinduct
    1.42 +fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy pre_bnfs dtor_coinduct
    1.43      dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs
    1.44      As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
    1.45      unfolds corecs unfold_defs corec_defs lthy =
    1.46    let
    1.47 +    val nn = length pre_bnfs;
    1.48 +
    1.49      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.50      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
    1.51      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
    1.52 @@ -529,7 +532,8 @@
    1.53              dtor_corec_thms pre_map_defs ctr_defss;
    1.54  
    1.55          fun prove goal tac =
    1.56 -          Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
    1.57 +          Goal.prove_sorry lthy [] [] goal (tac o #context)
    1.58 +          |> Thm.close_derivation;
    1.59  
    1.60          val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
    1.61          val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
    1.62 @@ -1208,7 +1212,7 @@
    1.63          val ((induct_thm, induct_thms, induct_attrs),
    1.64               (fold_thmss, fold_attrs),
    1.65               (rec_thmss, rec_attrs)) =
    1.66 -          derive_induct_fold_rec_thms_for_types nn pre_bnfs fp_induct fp_fold_thms fp_rec_thms
    1.67 +          derive_induct_fold_rec_thms_for_types pre_bnfs fp_induct fp_fold_thms fp_rec_thms
    1.68              nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
    1.69              fold_defs rec_defs lthy;
    1.70  
    1.71 @@ -1240,7 +1244,7 @@
    1.72               (disc_unfold_thmss, disc_corec_thmss, disc_corec_like_attrs),
    1.73               (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_corec_like_iff_attrs),
    1.74               (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) =
    1.75 -          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs fp_induct
    1.76 +          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy pre_bnfs fp_induct
    1.77              fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As
    1.78              kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
    1.79              unfolds corecs unfold_defs corec_defs lthy;