use record instead of big tuple
authorblanchet
Mon Apr 29 16:50:01 2013 +0200 (2013-04-29)
changeset 518199df935196be9
parent 51818 517f232e867d
child 51821 8bbc5fd78cd2
child 51823 38996458bc5c
use record instead of big tuple
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 15:47:42 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 16:50:01 2013 +0200
     1.3 @@ -8,8 +8,15 @@
     1.4  signature BNF_CTR_SUGAR =
     1.5  sig
     1.6    type ctr_wrap_result =
     1.7 -    term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
     1.8 -    thm list list
     1.9 +    {discs: term list,
    1.10 +     selss: term list list,
    1.11 +     exhaust: thm,
    1.12 +     injects: thm list,
    1.13 +     distincts: thm list,
    1.14 +     case_thms: thm list,
    1.15 +     disc_thmss: thm list list,
    1.16 +     discIs: thm list,
    1.17 +     sel_thmss: thm list list};
    1.18  
    1.19    val rep_compat_prefix: string
    1.20  
    1.21 @@ -37,8 +44,15 @@
    1.22  open BNF_Ctr_Sugar_Tactics
    1.23  
    1.24  type ctr_wrap_result =
    1.25 -  term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
    1.26 -  thm list list;
    1.27 +  {discs: term list,
    1.28 +   selss: term list list,
    1.29 +   exhaust: thm,
    1.30 +   injects: thm list,
    1.31 +   distincts: thm list,
    1.32 +   case_thms: thm list,
    1.33 +   disc_thmss: thm list list,
    1.34 +   discIs: thm list,
    1.35 +   sel_thmss: thm list list};
    1.36  
    1.37  val rep_compat_prefix = "new";
    1.38  
    1.39 @@ -671,14 +685,15 @@
    1.40            [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
    1.41            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.42        in
    1.43 -        ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
    1.44 -          sel_thmss),
    1.45 -          lthy
    1.46 -          |> not rep_compat ?
    1.47 -             (Local_Theory.declaration {syntax = false, pervasive = true}
    1.48 +        ({discs = discs, selss = selss, exhaust = exhaust_thm, injects = inject_thms,
    1.49 +          distincts = distinct_thms, case_thms = case_thms, disc_thmss = disc_thmss,
    1.50 +          discIs = discI_thms, sel_thmss = sel_thmss},
    1.51 +         lthy
    1.52 +         |> not rep_compat ?
    1.53 +            (Local_Theory.declaration {syntax = false, pervasive = true}
    1.54                 (fn phi => Case_Translation.register
    1.55 -                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
    1.56 -          |> Local_Theory.notes (notes' @ notes) |> snd)
    1.57 +                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
    1.58 +         |> Local_Theory.notes (notes' @ notes) |> snd)
    1.59        end;
    1.60    in
    1.61      (goalss, after_qed, lthy')
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 15:47:42 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 16:50:01 2013 +0200
     2.3 @@ -8,21 +8,21 @@
     2.4  signature BNF_FP =
     2.5  sig
     2.6    type fp_result =
     2.7 -    {bnfs : BNF_Def.BNF list,
     2.8 -     dtors : term list,
     2.9 -     ctors : term list,
    2.10 -     folds : term list,
    2.11 -     recs : term list,
    2.12 -     induct : thm,
    2.13 -     strong_induct : thm,
    2.14 -     dtor_ctors : thm list,
    2.15 -     ctor_dtors : thm list,
    2.16 -     ctor_injects : thm list,
    2.17 -     map_thms : thm list,
    2.18 -     set_thmss : thm list list,
    2.19 -     rel_thms : thm list,
    2.20 -     fold_thms : thm list,
    2.21 -     rec_thms : thm list}
    2.22 +    {bnfs: BNF_Def.BNF list,
    2.23 +     dtors: term list,
    2.24 +     ctors: term list,
    2.25 +     folds: term list,
    2.26 +     recs: term list,
    2.27 +     induct: thm,
    2.28 +     strong_induct: thm,
    2.29 +     dtor_ctors: thm list,
    2.30 +     ctor_dtors: thm list,
    2.31 +     ctor_injects: thm list,
    2.32 +     map_thms: thm list,
    2.33 +     set_thmss: thm list list,
    2.34 +     rel_thms: thm list,
    2.35 +     fold_thms: thm list,
    2.36 +     rec_thms: thm list}
    2.37  
    2.38    val time: Timer.real_timer -> string -> Timer.real_timer
    2.39  
    2.40 @@ -168,21 +168,21 @@
    2.41  open BNF_Util
    2.42  
    2.43  type fp_result =
    2.44 -  {bnfs : BNF_Def.BNF list,
    2.45 -   dtors : term list,
    2.46 -   ctors : term list,
    2.47 -   folds : term list,
    2.48 -   recs : term list,
    2.49 -   induct : thm,
    2.50 -   strong_induct : thm,
    2.51 -   dtor_ctors : thm list,
    2.52 -   ctor_dtors : thm list,
    2.53 -   ctor_injects : thm list,
    2.54 -   map_thms : thm list,
    2.55 -   set_thmss : thm list list,
    2.56 -   rel_thms : thm list,
    2.57 -   fold_thms : thm list,
    2.58 -   rec_thms : thm list};
    2.59 +  {bnfs: BNF_Def.BNF list,
    2.60 +   dtors: term list,
    2.61 +   ctors: term list,
    2.62 +   folds: term list,
    2.63 +   recs: term list,
    2.64 +   induct: thm,
    2.65 +   strong_induct: thm,
    2.66 +   dtor_ctors: thm list,
    2.67 +   ctor_dtors: thm list,
    2.68 +   ctor_injects: thm list,
    2.69 +   map_thms: thm list,
    2.70 +   set_thmss: thm list list,
    2.71 +   rel_thms: thm list,
    2.72 +   fold_thms: thm list,
    2.73 +   rec_thms: thm list};
    2.74  
    2.75  val timing = true;
    2.76  fun time timer msg = (if timing
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 15:47:42 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 16:50:01 2013 +0200
     3.3 @@ -369,12 +369,12 @@
     3.4  
     3.5      val fp_b_names = map base_name_of_typ fpTs;
     3.6  
     3.7 -    val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress;
     3.8 -    val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress;
     3.9 -    val exhaust_thms = map #3 ctr_wrap_ress;
    3.10 -    val disc_thmsss = map #7 ctr_wrap_ress;
    3.11 -    val discIss = map #8 ctr_wrap_ress;
    3.12 -    val sel_thmsss = map #9 ctr_wrap_ress;
    3.13 +    val discss = map (map (mk_disc_or_sel As) o #discs) ctr_wrap_ress;
    3.14 +    val selsss = map (map (map (mk_disc_or_sel As)) o #selss) ctr_wrap_ress;
    3.15 +    val exhausts = map #exhaust ctr_wrap_ress;
    3.16 +    val disc_thmsss = map #disc_thmss ctr_wrap_ress;
    3.17 +    val discIss = map #discIs ctr_wrap_ress;
    3.18 +    val sel_thmsss = map #sel_thmss ctr_wrap_ress;
    3.19  
    3.20      val (((rs, us'), vs'), names_lthy) =
    3.21        lthy
    3.22 @@ -440,7 +440,7 @@
    3.23          fun prove dtor_coinduct' goal =
    3.24            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    3.25              mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
    3.26 -              exhaust_thms ctr_defss disc_thmsss sel_thmsss)
    3.27 +              exhausts ctr_defss disc_thmsss sel_thmsss)
    3.28            |> singleton (Proof_Context.export names_lthy lthy)
    3.29            |> Thm.close_derivation;
    3.30  
    3.31 @@ -1202,8 +1202,8 @@
    3.32  
    3.33      (* TODO: Add map, sets, rel simps *)
    3.34      val mk_simp_thmss =
    3.35 -      map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
    3.36 -        injects @ distincts @ cases @ rec_likes @ fold_likes);
    3.37 +      map3 (fn {injects, distincts, case_thms, ...} => fn rec_likes => fn fold_likes =>
    3.38 +        injects @ distincts @ case_thms @ rec_likes @ fold_likes);
    3.39  
    3.40      fun derive_and_note_induct_fold_rec_thms_for_types
    3.41          (((ctrss, xsss, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =