tuning -- avoided unreadable true/false all over the place for LFP/GFP
authorblanchet
Tue May 28 21:17:48 2013 +0200 (2013-05-28)
changeset 5220721026c312cc3
parent 52206 6fa21e5a57c3
child 52208 ff8725b21a43
tuning -- avoided unreadable true/false all over the place for LFP/GFP
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_util.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 20:00:29 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 21:17:48 2013 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    type fp_sugar =
     1.6      {T: typ,
     1.7 -     lfp: bool,
     1.8 +     fp: BNF_FP_Util.fp_kind,
     1.9       index: int,
    1.10       pre_bnfs: BNF_Def.bnf list,
    1.11       fp_res: BNF_FP_Util.fp_result,
    1.12 @@ -27,11 +27,11 @@
    1.13  
    1.14    val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
    1.15    val exists_subtype_in: typ list -> typ -> bool
    1.16 -  val mk_co_iter: theory -> bool -> typ -> typ list -> term -> term
    1.17 +  val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
    1.18    val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
    1.19    val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
    1.20 -  val mk_un_fold_co_rec_prelims: bool -> typ list -> typ list -> int list -> int list list ->
    1.21 -    term list -> term list -> Proof.context ->
    1.22 +  val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
    1.23 +    int list list -> term list -> term list -> Proof.context ->
    1.24      (term list * term list * ((term list list * typ list list * term list list list)
    1.25         * (term list list * typ list list * term list list list)) option
    1.26       * (term list * term list list
    1.27 @@ -71,14 +71,14 @@
    1.28      * (thm list list * thm list list * Args.src list)
    1.29      * (thm list list * thm list list * Args.src list)
    1.30  
    1.31 -  val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list list ->
    1.32 -      binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.33 -      local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.34 +  val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.35 +      binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    1.36 +      BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.37      (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
    1.38        ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    1.39          mixfix) list) list ->
    1.40      local_theory -> local_theory
    1.41 -  val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list ->
    1.42 +  val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.43        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    1.44        BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    1.45      (local_theory -> local_theory) parser
    1.46 @@ -97,7 +97,7 @@
    1.47  
    1.48  type fp_sugar =
    1.49    {T: typ,
    1.50 -   lfp: bool,
    1.51 +   fp: fp_kind,
    1.52     index: int,
    1.53     pre_bnfs: bnf list,
    1.54     fp_res: fp_result,
    1.55 @@ -110,14 +110,15 @@
    1.56     un_fold_thmss: thm list list,
    1.57     co_rec_thmss: thm list list};
    1.58  
    1.59 -fun eq_fp_sugar ({T = T1, lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
    1.60 -    {T = T2, lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
    1.61 -  T1 = T2 andalso lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
    1.62 +fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
    1.63 +    {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
    1.64 +  T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
    1.65  
    1.66 -fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds, co_recs,
    1.67 -    co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} =
    1.68 -  {T = Morphism.typ phi T, lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    1.69 -   fp_res = morph_fp_result phi fp_res, ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
    1.70 +fun morph_fp_sugar phi {T, fp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds,
    1.71 +    co_recs, co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} =
    1.72 +  {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi)
    1.73 +   pre_bnfs, fp_res = morph_fp_result phi fp_res,
    1.74 +   ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
    1.75     ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds,
    1.76     co_recs = map (Morphism.term phi) co_recs, co_induct = Morphism.thm phi co_induct,
    1.77     strong_co_induct = Morphism.thm phi strong_co_induct,
    1.78 @@ -138,11 +139,11 @@
    1.79    Local_Theory.declaration {syntax = false, pervasive = true}
    1.80      (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
    1.81  
    1.82 -fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs
    1.83 +fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs
    1.84      co_induct strong_co_induct un_fold_thmss co_rec_thmss lthy =
    1.85    (0, lthy)
    1.86    |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
    1.87 -    register_fp_sugar s {T = T, lfp = lfp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res,
    1.88 +    register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res,
    1.89        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs,
    1.90        co_induct = co_induct, strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss,
    1.91        co_rec_thmss = co_rec_thmss} lthy)) Ts
    1.92 @@ -220,22 +221,22 @@
    1.93  val mk_ctor = mk_ctor_or_dtor range_type;
    1.94  val mk_dtor = mk_ctor_or_dtor domain_type;
    1.95  
    1.96 -fun mk_co_iter thy lfp fpT Cs t =
    1.97 +fun mk_co_iter thy fp fpT Cs t =
    1.98    let
    1.99      val (bindings, body) = strip_type (fastype_of t);
   1.100      val (f_Cs, prebody) = split_last bindings;
   1.101 -    val fpT0 = if lfp then prebody else body;
   1.102 -    val Cs0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Cs);
   1.103 +    val fpT0 = if fp = Least_FP then prebody else body;
   1.104 +    val Cs0 = distinct (op =) (map (if fp = Least_FP then body_type else domain_type) f_Cs);
   1.105      val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
   1.106    in
   1.107      Term.subst_TVars rho t
   1.108    end;
   1.109  
   1.110 -fun mk_co_iters thy lfp fpTs Cs ts0 =
   1.111 +fun mk_co_iters thy fp fpTs Cs ts0 =
   1.112    let
   1.113      val nn = length fpTs;
   1.114      val (fpTs0, Cs0) =
   1.115 -      map ((not lfp ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0
   1.116 +      map ((fp = Greatest_FP ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0
   1.117        |> split_list;
   1.118      val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs);
   1.119    in
   1.120 @@ -348,17 +349,17 @@
   1.121      ((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy)
   1.122    end;
   1.123  
   1.124 -fun mk_un_fold_co_rec_prelims lfp fpTs Cs ns mss fp_folds0 fp_recs0 lthy =
   1.125 +fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss fp_folds0 fp_recs0 lthy =
   1.126    let
   1.127      val thy = Proof_Context.theory_of lthy;
   1.128  
   1.129 -    val (fp_fold_fun_Ts, fp_folds) = mk_co_iters thy lfp fpTs Cs fp_folds0
   1.130 +    val (fp_fold_fun_Ts, fp_folds) = mk_co_iters thy fp fpTs Cs fp_folds0
   1.131        |> `(mk_fp_iter_fun_types o hd);
   1.132 -    val (fp_rec_fun_Ts, fp_recs) = mk_co_iters thy lfp fpTs Cs fp_recs0
   1.133 +    val (fp_rec_fun_Ts, fp_recs) = mk_co_iters thy fp fpTs Cs fp_recs0
   1.134        |> `(mk_fp_iter_fun_types o hd);
   1.135  
   1.136      val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
   1.137 -      if lfp then
   1.138 +      if fp = Least_FP then
   1.139          mk_fold_rec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
   1.140          |>> (rpair NONE o SOME)
   1.141        else
   1.142 @@ -513,11 +514,12 @@
   1.143  
   1.144      val [fold_def, rec_def] = map (Morphism.thm phi) defs;
   1.145  
   1.146 -    val [foldx, recx] = map (mk_co_iter thy true fpT Cs o Morphism.term phi) csts;
   1.147 +    val [foldx, recx] = map (mk_co_iter thy Least_FP fpT Cs o Morphism.term phi) csts;
   1.148    in
   1.149      ((foldx, recx, fold_def, rec_def), lthy')
   1.150    end;
   1.151  
   1.152 +(* TODO: merge with above function? *)
   1.153  fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs Cs dtor_unfold
   1.154      dtor_corec lthy0 =
   1.155    let
   1.156 @@ -550,7 +552,7 @@
   1.157  
   1.158      val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
   1.159  
   1.160 -    val [unfold, corec] = map (mk_co_iter thy false fpT Cs o Morphism.term phi) csts;
   1.161 +    val [unfold, corec] = map (mk_co_iter thy Greatest_FP fpT Cs o Morphism.term phi) csts;
   1.162    in
   1.163      ((unfold, corec, unfold_def, corec_def), lthy')
   1.164    end ;
   1.165 @@ -984,13 +986,15 @@
   1.166       (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
   1.167    end;
   1.168  
   1.169 -fun define_co_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
   1.170 +fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
   1.171      (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
   1.172    let
   1.173      (* TODO: sanity checks on arguments *)
   1.174  
   1.175 -    val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
   1.176 -      else ();
   1.177 +    val _ = if fp = Greatest_FP andalso no_dests then
   1.178 +        error "Cannot define destructor-less codatatypes"
   1.179 +      else
   1.180 +        ();
   1.181  
   1.182      fun qualify mandatory fp_b_name =
   1.183        Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
   1.184 @@ -1134,7 +1138,7 @@
   1.185      val mss = map (map length) ctr_Tsss;
   1.186  
   1.187      val ((fp_folds, fp_recs, fold_rec_args_types, unfold_corec_args_types), lthy) =
   1.188 -      mk_un_fold_co_rec_prelims lfp fpTs Cs ns mss fp_folds0 fp_recs0 lthy;
   1.189 +      mk_un_fold_co_rec_prelims fp fpTs Cs ns mss fp_folds0 fp_recs0 lthy;
   1.190  
   1.191      fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
   1.192              fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
   1.193 @@ -1244,7 +1248,7 @@
   1.194                val nones = replicate live NONE;
   1.195  
   1.196                val ctor_cong =
   1.197 -                if lfp then
   1.198 +                if fp = Least_FP then
   1.199                    Drule.dummy_thm
   1.200                  else
   1.201                    let val ctor' = mk_ctor Bs ctor in
   1.202 @@ -1252,7 +1256,7 @@
   1.203                    end;
   1.204  
   1.205                fun mk_cIn ify =
   1.206 -                certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
   1.207 +                certify lthy o (fp = Greatest_FP ? curry (op $) (map_types ify ctor)) oo
   1.208                  mk_InN_balanced (ify ctr_sum_prod_T) n;
   1.209  
   1.210                val cxIns = map2 (mk_cIn I) tuple_xs ks;
   1.211 @@ -1261,15 +1265,15 @@
   1.212                fun mk_map_thm ctr_def' cxIn =
   1.213                  fold_thms lthy [ctr_def']
   1.214                    (unfold_thms lthy (pre_map_def ::
   1.215 -                       (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
   1.216 +                       (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
   1.217                       (cterm_instantiate_pos (nones @ [SOME cxIn])
   1.218 -                        (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
   1.219 +                        (if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong)))
   1.220                  |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.221  
   1.222                fun mk_set_thm fp_set_thm ctr_def' cxIn =
   1.223                  fold_thms lthy [ctr_def']
   1.224                    (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
   1.225 -                       (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
   1.226 +                       (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set)
   1.227                       (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
   1.228                  |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.229  
   1.230 @@ -1283,7 +1287,7 @@
   1.231                fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
   1.232                  fold_thms lthy ctr_defs'
   1.233                     (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
   1.234 -                        (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
   1.235 +                        (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel)
   1.236                        (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
   1.237                  |> postproc
   1.238                  |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.239 @@ -1326,7 +1330,7 @@
   1.240        in
   1.241          (wrap_ctrs
   1.242           #> derive_maps_sets_rels
   1.243 -         ##>> (if lfp then define_fold_rec (the fold_rec_args_types)
   1.244 +         ##>> (if fp = Least_FP then define_fold_rec (the fold_rec_args_types)
   1.245             else define_unfold_corec (the unfold_corec_args_types)) mk_binding fpTs Cs fp_fold fp_rec
   1.246           #> massage_res, lthy')
   1.247        end;
   1.248 @@ -1370,7 +1374,7 @@
   1.249        in
   1.250          lthy
   1.251          |> Local_Theory.notes (common_notes @ notes) |> snd
   1.252 -        |> register_fp_sugars true pre_bnfs fp_res ctr_defss ctr_sugars folds recs induct_thm
   1.253 +        |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars folds recs induct_thm
   1.254            induct_thm fold_thmss rec_thmss
   1.255        end;
   1.256  
   1.257 @@ -1429,8 +1433,8 @@
   1.258        in
   1.259          lthy
   1.260          |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
   1.261 -        |> register_fp_sugars false pre_bnfs fp_res ctr_defss ctr_sugars unfolds corecs coinduct_thm
   1.262 -          strong_coinduct_thm unfold_thmss corec_thmss
   1.263 +        |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars unfolds corecs
   1.264 +          coinduct_thm strong_coinduct_thm unfold_thmss corec_thmss
   1.265        end;
   1.266  
   1.267      val lthy' = lthy
   1.268 @@ -1440,11 +1444,11 @@
   1.269          mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
   1.270          raw_sel_defaultsss)
   1.271        |> wrap_types_etc
   1.272 -      |> (if lfp then derive_and_note_induct_fold_rec_thms_for_types
   1.273 +      |> (if fp = Least_FP then derive_and_note_induct_fold_rec_thms_for_types
   1.274            else derive_and_note_coinduct_unfold_corec_thms_for_types);
   1.275  
   1.276      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
   1.277 -      datatype_word lfp));
   1.278 +      datatype_word fp));
   1.279    in
   1.280      timer; lthy'
   1.281    end;
   1.282 @@ -1496,6 +1500,6 @@
   1.283  
   1.284  val parse_co_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
   1.285  
   1.286 -fun parse_co_datatype_cmd lfp construct_fp = parse_co_datatype >> co_datatype_cmd lfp construct_fp;
   1.287 +fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
   1.288  
   1.289  end;
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue May 28 20:00:29 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue May 28 21:17:48 2013 +0200
     2.3 @@ -8,6 +8,8 @@
     2.4  
     2.5  signature BNF_FP_UTIL =
     2.6  sig
     2.7 +  datatype fp_kind = Least_FP | Greatest_FP
     2.8 +
     2.9    type fp_result =
    2.10      {Ts: typ list,
    2.11       bnfs: BNF_Def.bnf list,
    2.12 @@ -118,7 +120,7 @@
    2.13    val mk_dtor_set_inductN: int -> string
    2.14    val mk_set_inductN: int -> string
    2.15  
    2.16 -  val datatype_word: bool -> string
    2.17 +  val datatype_word: fp_kind -> string
    2.18  
    2.19    val base_name_of_typ: typ -> string
    2.20    val mk_common_name: string list -> string
    2.21 @@ -176,6 +178,8 @@
    2.22  open BNF_Def
    2.23  open BNF_Util
    2.24  
    2.25 +datatype fp_kind = Least_FP | Greatest_FP;
    2.26 +
    2.27  type fp_result =
    2.28    {Ts: typ list,
    2.29     bnfs: BNF_Def.bnf list,
    2.30 @@ -318,7 +322,7 @@
    2.31  val sel_unfoldN = selN ^ "_" ^ unfoldN
    2.32  val sel_corecN = selN ^ "_" ^ corecN
    2.33  
    2.34 -fun datatype_word lfp = (if lfp then "" else "co") ^ "datatype";
    2.35 +fun datatype_word fp = (if fp = Greatest_FP then "co" else "") ^ "datatype";
    2.36  
    2.37  fun add_components_of_typ (Type (s, Ts)) =
    2.38      fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue May 28 20:00:29 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue May 28 21:17:48 2013 +0200
     3.3 @@ -3122,6 +3122,6 @@
     3.4  
     3.5  val _ =
     3.6    Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     3.7 -    (parse_co_datatype_cmd false construct_gfp);
     3.8 +    (parse_co_datatype_cmd Greatest_FP construct_gfp);
     3.9  
    3.10  end;
     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Tue May 28 20:00:29 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Tue May 28 21:17:48 2013 +0200
     4.3 @@ -1866,6 +1866,6 @@
     4.4  
     4.5  val _ =
     4.6    Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
     4.7 -    (parse_co_datatype_cmd true construct_lfp);
     4.8 +    (parse_co_datatype_cmd Least_FP construct_lfp);
     4.9  
    4.10  end;