src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
changeset 49126 1bbd7a37fc29
parent 49125 5fc5211cf104
child 49127 f7326a0d7f19
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 15:51:32 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 16:17:22 2012 +0200
     1.3 @@ -107,21 +107,22 @@
     1.4  
     1.5      val eqs = map dest_TFree Bs ~~ sum_prod_TsBs;
     1.6  
     1.7 -    val ((raw_flds, raw_unfs, fld_unfs, unf_flds), lthy') = fp_bnf construct bs eqs lthy;
     1.8 +    val ((raw_unfs, raw_flds, unf_flds, fld_unfs, fld_injects), lthy') =
     1.9 +      fp_bnf construct bs eqs lthy;
    1.10  
    1.11 -    fun mk_fld_or_unf get_foldedT Ts t =
    1.12 +    fun mk_unf_or_fld get_foldedT Ts t =
    1.13        let val Type (_, Ts0) = get_foldedT (fastype_of t) in
    1.14          Term.subst_atomic_types (Ts0 ~~ Ts) t
    1.15        end;
    1.16  
    1.17 -    val mk_fld = mk_fld_or_unf range_type;
    1.18 -    val mk_unf = mk_fld_or_unf domain_type;
    1.19 +    val mk_unf = mk_unf_or_fld domain_type;
    1.20 +    val mk_fld = mk_unf_or_fld range_type;
    1.21  
    1.22 +    val unfs = map (mk_unf As) raw_unfs;
    1.23      val flds = map (mk_fld As) raw_flds;
    1.24 -    val unfs = map (mk_unf As) raw_unfs;
    1.25  
    1.26 -    fun wrap_type ((((((((T, fld), unf), fld_unf), unf_fld), ctr_names), ctr_Tss), disc_names),
    1.27 -        sel_namess) no_defs_lthy =
    1.28 +    fun wrap_type (((((((((T, fld), unf), fld_unf), unf_fld), fld_inject), ctr_names), ctr_Tss),
    1.29 +        disc_names), sel_namess) no_defs_lthy =
    1.30        let
    1.31          val n = length ctr_names;
    1.32          val ks = 1 upto n;
    1.33 @@ -178,11 +179,15 @@
    1.34          fun exhaust_tac {context = ctxt, ...} =
    1.35            mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
    1.36  
    1.37 -        (* ### *)
    1.38 +        val inject_tacss =
    1.39 +          map2 (fn 0 => K []
    1.40 +                 | _ => fn ctr_def => [fn {context = ctxt, ...} =>
    1.41 +                     mk_inject_tac ctxt ctr_def fld_inject])
    1.42 +            ms ctr_defs;
    1.43 +
    1.44 +        (*###*)
    1.45          fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
    1.46  
    1.47 -        val inject_tacss = map (fn 0 => [] | _ => [cheat_tac]) ms;
    1.48 -
    1.49          val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
    1.50  
    1.51          val case_tacs = map (K cheat_tac) ks;
    1.52 @@ -193,8 +198,8 @@
    1.53        end;
    1.54    in
    1.55      lthy'
    1.56 -    |> fold wrap_type (Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ ctr_namess ~~ ctr_Tsss ~~
    1.57 -      disc_namess ~~ sel_namesss)
    1.58 +    |> fold wrap_type (Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ctr_namess ~~
    1.59 +      ctr_Tsss ~~ disc_namess ~~ sel_namesss)
    1.60    end;
    1.61  
    1.62  fun data_cmd info specs lthy =