src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55966 972f0aa7091b
parent 55932 68c5104d2204
child 56484 c451cf8b29c8
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 22:15:01 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Mar 07 01:02:21 2014 +0100
     1.3 @@ -52,20 +52,20 @@
     1.4      fun of_fp_res get =
     1.5        map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
     1.6  
     1.7 -    fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
     1.8 -    fun co_swap pair = fp_case fp I swap pair;
     1.9 +    fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    1.10 +    fun co_swap pair = case_fp fp I swap pair;
    1.11      val mk_co_comp = HOLogic.mk_comp o co_swap;
    1.12 -    val co_productC = BNF_FP_Rec_Sugar_Util.fp_case fp @{type_name prod} @{type_name sum};
    1.13 +    val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum};
    1.14  
    1.15      val dest_co_algT = co_swap o dest_funT;
    1.16 -    val co_alg_argT = fp_case fp range_type domain_type;
    1.17 -    val co_alg_funT = fp_case fp domain_type range_type;
    1.18 -    val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
    1.19 -    val mk_map_co_product = fp_case fp mk_prod_map mk_map_sum;
    1.20 -    val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    1.21 -    val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
    1.22 -    val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
    1.23 -    val rewrite_comp_comp = fp_case fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
    1.24 +    val co_alg_argT = case_fp fp range_type domain_type;
    1.25 +    val co_alg_funT = case_fp fp domain_type range_type;
    1.26 +    val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
    1.27 +    val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum;
    1.28 +    val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    1.29 +    val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
    1.30 +    val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT;
    1.31 +    val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
    1.32  
    1.33      val fp_absT_infos = map #absT_info fp_sugars;
    1.34      val fp_bnfs = of_fp_res #bnfs;
    1.35 @@ -115,7 +115,7 @@
    1.36          val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
    1.37          val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
    1.38        in
    1.39 -        ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (fp_case fp ctors dtors))
    1.40 +        ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors))
    1.41        end;
    1.42  
    1.43      val absATs = map (domain_type o fastype_of) ctors;
    1.44 @@ -283,7 +283,7 @@
    1.45        end;
    1.46  
    1.47      fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
    1.48 -      fp_case fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
    1.49 +      case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
    1.50          (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
    1.51  
    1.52      fun mk_rec b_opt recs lthy TU =
    1.53 @@ -358,7 +358,7 @@
    1.54              fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
    1.55        end;
    1.56  
    1.57 -    val recN = fp_case fp ctor_recN dtor_corecN;
    1.58 +    val recN = case_fp fp ctor_recN dtor_corecN;
    1.59      fun mk_recs lthy =
    1.60        fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
    1.61          mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
    1.62 @@ -403,10 +403,10 @@
    1.63  
    1.64          val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
    1.65  
    1.66 -        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    1.67 +        val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    1.68            map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
    1.69            @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
    1.70 -        val rec_thms = fold_thms @ fp_case fp
    1.71 +        val rec_thms = fold_thms @ case_fp fp
    1.72            @{thms fst_convol map_prod_o_convol convol_o}
    1.73            @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
    1.74  
    1.75 @@ -415,7 +415,7 @@
    1.76          val map_thms = no_refl (maps (fn bnf =>
    1.77             let val map_comp0 = map_comp0_of_bnf bnf RS sym
    1.78             in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
    1.79 -          remove eq_thm_prop_untyped (fp_case fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
    1.80 +          remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
    1.81            (map2 (fn thm => fn bnf =>
    1.82              @{thm type_copy_map_comp0_undo} OF
    1.83                (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS