1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 19:57:50 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 19:58:09 2012 +0200
     1.3 @@ -67,7 +67,6 @@
     1.4        | A :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy A)));
     1.5  
     1.6      (* TODO: use sort constraints on type args *)
     1.7 -    (* TODO: use mixfix *)
     1.8  
     1.9      val N = length specs;
    1.10  
    1.11 @@ -122,7 +121,7 @@
    1.12      val eqs = map dest_TFree Bs ~~ sum_prod_TsBs;
    1.13  
    1.14      val ((raw_unfs, raw_flds, unf_flds, fld_unfs, fld_injects), lthy') =
    1.15 -      fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs As' eqs lthy;
    1.16 +      fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs mixfixes As' eqs lthy;
    1.17  
    1.18      val timer = time (Timer.startRealTimer ());
    1.19  
    1.20 @@ -137,8 +136,8 @@
    1.21      val unfs = map (mk_unf As) raw_unfs;
    1.22      val flds = map (mk_fld As) raw_flds;
    1.23  
    1.24 -    fun pour_sugar_on_type ((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
    1.25 -        ctr_binders), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
    1.26 +    fun pour_sugar_on_type (((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
    1.27 +        ctr_binders), ctr_mixfixes), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
    1.28        let
    1.29          val n = length ctr_binders;
    1.30          val ks = 1 upto n;
    1.31 @@ -165,9 +164,9 @@
    1.32            fold_rev Term.lambda (fs @ [v]) (mk_sum_caseN (uncurry_fs fs xss) $ (unf $ v));
    1.33  
    1.34          val (((raw_ctrs, raw_ctr_defs), (raw_case, raw_case_def)), (lthy', lthy)) = no_defs_lthy
    1.35 -          |> apfst split_list o fold_map2 (fn b => fn rhs =>
    1.36 -               Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
    1.37 -             ctr_binders ctr_rhss
    1.38 +          |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
    1.39 +               Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
    1.40 +             ctr_binders ctr_mixfixes ctr_rhss
    1.41            ||>> (Local_Theory.define ((case_binder, NoSyn), ((Thm.def_binding case_binder, []),
    1.42               case_rhs)) #>> apsnd snd)
    1.43            ||> `Local_Theory.restore;
    1.44 @@ -250,7 +249,7 @@
    1.45  
    1.46      val lthy'' =
    1.47        fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
    1.48 -        ctr_binderss ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) lthy'
    1.49 +        ctr_binderss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) lthy';
    1.50  
    1.51      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
    1.52        (if gfp then "co" else "") ^ "datatype"));

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 19:57:50 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 19:58:09 2012 +0200
     2.3 @@ -98,11 +98,12 @@
     2.4  
     2.5    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
     2.6  
     2.7 -  val fp_bnf: (binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
     2.8 -    local_theory -> 'a) ->
     2.9 -    binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> 'a
    2.10 -  val fp_bnf_cmd: (binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
    2.11 -    local_theory -> 'a) ->
    2.12 +  val fp_bnf: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
    2.13 +    BNF_Def.BNF list -> local_theory -> 'a) ->
    2.14 +    binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
    2.15 +    local_theory -> 'a
    2.16 +  val fp_bnf_cmd: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
    2.17 +    BNF_Def.BNF list -> local_theory -> 'a) ->
    2.18      binding list * (string list * string list) -> local_theory -> 'a
    2.19  end;
    2.20  
    2.21 @@ -259,7 +260,7 @@
    2.22  fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
    2.23    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
    2.24  
    2.25 -fun mk_fp_bnf timer construct bs resBs sort lhss bnfs deadss livess unfold lthy =
    2.26 +fun mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs deadss livess unfold lthy =
    2.27    let
    2.28      val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
    2.29      fun qualify i bind =
    2.30 @@ -289,14 +290,14 @@
    2.31  
    2.32      val timer = time (timer "Normalization & sealing of BNFs");
    2.33  
    2.34 -    val res = construct bs resDs Dss bnfs'' lthy'';
    2.35 +    val res = construct bs mixfixes resDs Dss bnfs'' lthy'';
    2.36  
    2.37      val timer = time (timer "FP construction in total");
    2.38    in
    2.39      res
    2.40    end;
    2.41  
    2.42 -fun fp_bnf construct bs resBs eqs lthy =
    2.43 +fun fp_bnf construct bs mixfixes resBs eqs lthy =
    2.44    let
    2.45      val timer = time (Timer.startRealTimer ());
    2.46      val (lhss, rhss) = split_list eqs;
    2.47 @@ -305,7 +306,7 @@
    2.48        (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
    2.49          (empty_unfold, lthy));
    2.50    in
    2.51 -    mk_fp_bnf timer construct bs resBs sort lhss bnfs Dss Ass unfold lthy'
    2.52 +    mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs Dss Ass unfold lthy'
    2.53    end;
    2.54  
    2.55  fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
    2.56 @@ -318,7 +319,7 @@
    2.57          (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
    2.58          bs raw_bnfs (empty_unfold, lthy));
    2.59    in
    2.60 -    mk_fp_bnf timer construct bs [] sort lhss bnfs Dss Ass unfold lthy'
    2.61 +    mk_fp_bnf timer construct bs (map (K NoSyn) bs) [] sort lhss bnfs Dss Ass unfold lthy'
    2.62    end;
    2.63  
    2.64  end;

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 05 19:57:50 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 05 19:58:09 2012 +0200
     3.3 @@ -9,8 +9,9 @@
     3.4  
     3.5  signature BNF_GFP =
     3.6  sig
     3.7 -  val bnf_gfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
     3.8 -    local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
     3.9 +  val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
    3.10 +    BNF_Def.BNF list -> local_theory ->
    3.11 +    (term list * term list * thm list * thm list * thm list) * local_theory
    3.12  end;
    3.13  
    3.14  structure BNF_GFP : BNF_GFP =
    3.15 @@ -52,7 +53,7 @@
    3.16       ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    3.17  
    3.18  (*all bnfs have the same lives*)
    3.19 -fun bnf_gfp bs resDs Dss_insts bnfs lthy =
    3.20 +fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy =
    3.21    let
    3.22      val timer = time (Timer.startRealTimer ());
    3.23  
    3.24 @@ -1830,9 +1831,9 @@
    3.25  
    3.26      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
    3.27        lthy
    3.28 -      |> fold_map3 (fn b => fn car_final => fn in_car_final =>
    3.29 -        typedef false NONE (b, params, NoSyn) car_final NONE
    3.30 -          (EVERY' [rtac exI, rtac in_car_final] 1)) bs car_finals in_car_final_thms
    3.31 +      |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
    3.32 +        typedef false NONE (b, params, mx) car_final NONE
    3.33 +          (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
    3.34        |>> apsnd split_list o split_list;
    3.35  
    3.36      val Ts = map (fn name => Type (name, params')) T_names;

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 05 19:57:50 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 05 19:58:09 2012 +0200
     4.3 @@ -8,8 +8,9 @@
     4.4  
     4.5  signature BNF_LFP =
     4.6  sig
     4.7 -  val bnf_lfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
     4.8 -    local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
     4.9 +  val bnf_lfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
    4.10 +    BNF_Def.BNF list -> local_theory ->
    4.11 +    (term list * term list * thm list * thm list * thm list) * local_theory
    4.12  end;
    4.13  
    4.14  structure BNF_LFP : BNF_LFP =
    4.15 @@ -23,7 +24,7 @@
    4.16  open BNF_LFP_Tactics
    4.17  
    4.18  (*all bnfs have the same lives*)
    4.19 -fun bnf_lfp bs resDs Dss_insts bnfs lthy =
    4.20 +fun bnf_lfp bs mixfixes resDs Dss_insts bnfs lthy =
    4.21    let
    4.22      val timer = time (Timer.startRealTimer ());
    4.23      val live = live_of_bnf (hd bnfs);
    4.24 @@ -927,9 +928,9 @@
    4.25  
    4.26      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
    4.27        lthy
    4.28 -      |> fold_map2 (fn b => fn car_init => typedef true NONE (b, params, NoSyn) car_init NONE
    4.29 +      |> fold_map3 (fn b => fn mx => fn car_init => typedef true NONE (b, params, mx) car_init NONE
    4.30            (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
    4.31 -            rtac alg_init_thm] 1)) bs car_inits
    4.32 +            rtac alg_init_thm] 1)) bs mixfixes car_inits
    4.33        |>> apsnd split_list o split_list;
    4.34  
    4.35      val Ts = map (fn name => Type (name, params')) T_names;