balance tuples that represent curried functions
authorblanchet
Fri Mar 07 01:02:21 2014 +0100 (2014-03-07)
changeset 55966972f0aa7091b
parent 55965 0c2c61a87a7d
child 55967 5dadc93ff3df
child 55971 7644d63e8c3f
balance tuples that represent curried functions
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_GFP.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_util.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 22:15:01 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Fri Mar 07 01:02:21 2014 +0100
     1.3 @@ -28,12 +28,6 @@
     1.4  lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
     1.5  by simp
     1.6  
     1.7 -lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
     1.8 -by clarify
     1.9 -
    1.10 -lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
    1.11 -by auto
    1.12 -
    1.13  lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
    1.14  unfolding comp_def fun_eq_iff by simp
    1.15  
    1.16 @@ -58,9 +52,6 @@
    1.17  "case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
    1.18  by auto
    1.19  
    1.20 -lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.21 -by simp
    1.22 -
    1.23  lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
    1.24  by blast
    1.25  
    1.26 @@ -76,9 +67,6 @@
    1.27    fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
    1.28  qed
    1.29  
    1.30 -lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.31 -by (cases s) auto
    1.32 -
    1.33  lemma case_sum_if:
    1.34  "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    1.35  by simp
     2.1 --- a/src/HOL/BNF_GFP.thy	Thu Mar 06 22:15:01 2014 +0100
     2.2 +++ b/src/HOL/BNF_GFP.thy	Fri Mar 07 01:02:21 2014 +0100
     2.3 @@ -21,6 +21,12 @@
     2.4  Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
     2.5  *}
     2.6  
     2.7 +lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
     2.8 +by simp
     2.9 +
    2.10 +lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    2.11 +by (cases s) auto
    2.12 +
    2.13  lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    2.14  by (erule notE, rule TrueI)
    2.15  
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Mar 06 22:15:01 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Mar 07 01:02:21 2014 +0100
     3.3 @@ -365,7 +365,7 @@
     3.4    end;
     3.5  
     3.6  (*avoid "'a itself" arguments in corecursors*)
     3.7 -fun repair_nullary_single_ctr [[]] = [[@{typ unit}]]
     3.8 +fun repair_nullary_single_ctr [[]] = [[HOLogic.unitT]]
     3.9    | repair_nullary_single_ctr Tss = Tss;
    3.10  
    3.11  fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
    3.12 @@ -479,7 +479,7 @@
    3.13          (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
    3.14             map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
    3.15                 mk_case_absumprod ctor_rec_absT rep fs
    3.16 -                 (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
    3.17 +                 (map (mk_tuple_balanced o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
    3.18               ctor_rec_absTs reps fss xssss)))
    3.19      end;
    3.20  
    3.21 @@ -978,7 +978,7 @@
    3.22      val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts);
    3.23  
    3.24      val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
    3.25 -    val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
    3.26 +    val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
    3.27  
    3.28      val fp_eqs =
    3.29        map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
    3.30 @@ -1196,7 +1196,7 @@
    3.31                fun mk_map_thm ctr_def' cxIn =
    3.32                  fold_thms lthy [ctr_def']
    3.33                    (unfold_thms lthy (o_apply :: pre_map_def ::
    3.34 -                       (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map @
    3.35 +                       (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sumprod_thms_map @
    3.36                         abs_inverses)
    3.37                       (cterm_instantiate_pos (nones @ [SOME cxIn])
    3.38                          (if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong)))
    3.39 @@ -1205,7 +1205,7 @@
    3.40                fun mk_set_thm fp_set_thm ctr_def' cxIn =
    3.41                  fold_thms lthy [ctr_def']
    3.42                    (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @
    3.43 -                       (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set @
    3.44 +                       (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @
    3.45                         abs_inverses)
    3.46                       (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
    3.47                  |> singleton (Proof_Context.export names_lthy no_defs_lthy);
    3.48 @@ -1221,7 +1221,7 @@
    3.49                fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
    3.50                  fold_thms lthy ctr_defs'
    3.51                    (unfold_thms lthy (pre_rel_def :: abs_inverse ::
    3.52 -                       (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel @
    3.53 +                       (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
    3.54                         @{thms vimage2p_def Inl_Inr_False})
    3.55                       (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
    3.56                  |> postproc
    3.57 @@ -1396,7 +1396,7 @@
    3.58          abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
    3.59          ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
    3.60        |> wrap_types_etc
    3.61 -      |> fp_case fp derive_note_induct_recs_thms_for_types
    3.62 +      |> case_fp fp derive_note_induct_recs_thms_for_types
    3.63             derive_note_coinduct_corecs_thms_for_types;
    3.64  
    3.65      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 22:15:01 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Mar 07 01:02:21 2014 +0100
     4.3 @@ -7,9 +7,9 @@
     4.4  
     4.5  signature BNF_FP_DEF_SUGAR_TACTICS =
     4.6  sig
     4.7 -  val sum_prod_thms_map: thm list
     4.8 -  val sum_prod_thms_set: thm list
     4.9 -  val sum_prod_thms_rel: thm list
    4.10 +  val sumprod_thms_map: thm list
    4.11 +  val sumprod_thms_set: thm list
    4.12 +  val sumprod_thms_rel: thm list
    4.13  
    4.14    val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
    4.15      thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
    4.16 @@ -37,12 +37,12 @@
    4.17  val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
    4.18  val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
    4.19  
    4.20 -val sum_prod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
    4.21 -val sum_prod_thms_set =
    4.22 +val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
    4.23 +val sumprod_thms_set =
    4.24    @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
    4.25        Union_Un_distrib image_iff o_apply map_prod_simp
    4.26        mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
    4.27 -val sum_prod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply};
    4.28 +val sumprod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply};
    4.29  
    4.30  fun hhf_concl_conv cv ctxt ct =
    4.31    (case Thm.term_of ct of
    4.32 @@ -87,13 +87,13 @@
    4.33  
    4.34  val rec_unfold_thms =
    4.35    @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
    4.36 -      case_unit_Unity} @ sum_prod_thms_map;
    4.37 +      case_unit_Unity} @ sumprod_thms_map;
    4.38  
    4.39  fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
    4.40    unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
    4.41      pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
    4.42  
    4.43 -val corec_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
    4.44 +val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
    4.45  
    4.46  fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
    4.47    let
    4.48 @@ -121,7 +121,7 @@
    4.49      pre_set_defs =
    4.50    HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    4.51      SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @
    4.52 -      sum_prod_thms_set)),
    4.53 +      sumprod_thms_set)),
    4.54      solve_prem_prem_tac ctxt]) (rev kks)));
    4.55  
    4.56  fun mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps pre_set_defs m k
    4.57 @@ -153,7 +153,7 @@
    4.58      (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
    4.59    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
    4.60    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
    4.61 -    sels @ sum_prod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
    4.62 +    sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
    4.63    (atac ORELSE' REPEAT o etac conjE THEN'
    4.64       full_simp_tac
    4.65         (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 22:15:01 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Mar 07 01:02:21 2014 +0100
     5.3 @@ -52,20 +52,20 @@
     5.4      fun of_fp_res get =
     5.5        map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
     5.6  
     5.7 -    fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
     5.8 -    fun co_swap pair = fp_case fp I swap pair;
     5.9 +    fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    5.10 +    fun co_swap pair = case_fp fp I swap pair;
    5.11      val mk_co_comp = HOLogic.mk_comp o co_swap;
    5.12 -    val co_productC = BNF_FP_Rec_Sugar_Util.fp_case fp @{type_name prod} @{type_name sum};
    5.13 +    val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum};
    5.14  
    5.15      val dest_co_algT = co_swap o dest_funT;
    5.16 -    val co_alg_argT = fp_case fp range_type domain_type;
    5.17 -    val co_alg_funT = fp_case fp domain_type range_type;
    5.18 -    val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
    5.19 -    val mk_map_co_product = fp_case fp mk_prod_map mk_map_sum;
    5.20 -    val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    5.21 -    val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
    5.22 -    val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
    5.23 -    val rewrite_comp_comp = fp_case fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
    5.24 +    val co_alg_argT = case_fp fp range_type domain_type;
    5.25 +    val co_alg_funT = case_fp fp domain_type range_type;
    5.26 +    val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
    5.27 +    val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum;
    5.28 +    val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    5.29 +    val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
    5.30 +    val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT;
    5.31 +    val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
    5.32  
    5.33      val fp_absT_infos = map #absT_info fp_sugars;
    5.34      val fp_bnfs = of_fp_res #bnfs;
    5.35 @@ -115,7 +115,7 @@
    5.36          val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
    5.37          val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
    5.38        in
    5.39 -        ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (fp_case fp ctors dtors))
    5.40 +        ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors))
    5.41        end;
    5.42  
    5.43      val absATs = map (domain_type o fastype_of) ctors;
    5.44 @@ -283,7 +283,7 @@
    5.45        end;
    5.46  
    5.47      fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
    5.48 -      fp_case fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
    5.49 +      case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
    5.50          (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
    5.51  
    5.52      fun mk_rec b_opt recs lthy TU =
    5.53 @@ -358,7 +358,7 @@
    5.54              fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
    5.55        end;
    5.56  
    5.57 -    val recN = fp_case fp ctor_recN dtor_corecN;
    5.58 +    val recN = case_fp fp ctor_recN dtor_corecN;
    5.59      fun mk_recs lthy =
    5.60        fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
    5.61          mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
    5.62 @@ -403,10 +403,10 @@
    5.63  
    5.64          val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
    5.65  
    5.66 -        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    5.67 +        val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    5.68            map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
    5.69            @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
    5.70 -        val rec_thms = fold_thms @ fp_case fp
    5.71 +        val rec_thms = fold_thms @ case_fp fp
    5.72            @{thms fst_convol map_prod_o_convol convol_o}
    5.73            @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
    5.74  
    5.75 @@ -415,7 +415,7 @@
    5.76          val map_thms = no_refl (maps (fn bnf =>
    5.77             let val map_comp0 = map_comp0_of_bnf bnf RS sym
    5.78             in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
    5.79 -          remove eq_thm_prop_untyped (fp_case fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
    5.80 +          remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
    5.81            (map2 (fn thm => fn bnf =>
    5.82              @{thm type_copy_map_comp0_undo} OF
    5.83                (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Mar 06 22:15:01 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Mar 07 01:02:21 2014 +0100
     6.3 @@ -101,7 +101,7 @@
     6.4      xs ([], ([], []));
     6.5  
     6.6  fun key_of_fp_eqs fp fpTs fp_eqs =
     6.7 -  Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
     6.8 +  Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
     6.9  
    6.10  fun get_indices callers t =
    6.11    callers
    6.12 @@ -191,7 +191,7 @@
    6.13  
    6.14      val ctr_Tsss = map (map binder_types) ctr_Tss;
    6.15      val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
    6.16 -    val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
    6.17 +    val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
    6.18  
    6.19      val ns = map length ctr_Tsss;
    6.20      val kss = map (fn n => 1 upto n) ns;
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Thu Mar 06 22:15:01 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Fri Mar 07 01:02:21 2014 +0100
     7.3 @@ -10,7 +10,7 @@
     7.4  sig
     7.5    datatype fp_kind = Least_FP | Greatest_FP
     7.6  
     7.7 -  val fp_case: fp_kind -> 'a -> 'a -> 'a
     7.8 +  val case_fp: fp_kind -> 'a -> 'a -> 'a
     7.9  
    7.10    val flat_rec_arg_args: 'a list list -> 'a list
    7.11  
    7.12 @@ -48,8 +48,8 @@
    7.13  
    7.14  datatype fp_kind = Least_FP | Greatest_FP;
    7.15  
    7.16 -fun fp_case Least_FP l _ = l
    7.17 -  | fp_case Greatest_FP _ g = g;
    7.18 +fun case_fp Least_FP l _ = l
    7.19 +  | case_fp Greatest_FP _ g = g;
    7.20  
    7.21  fun flat_rec_arg_args xss =
    7.22    (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
    7.23 @@ -107,8 +107,8 @@
    7.24  fun mk_co_rec thy fp fpT Cs t =
    7.25    let
    7.26      val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last;
    7.27 -    val fpT0 = fp_case fp prebody body;
    7.28 -    val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs);
    7.29 +    val fpT0 = case_fp fp prebody body;
    7.30 +    val Cs0 = distinct (op =) (map (case_fp fp body_type domain_type) f_Cs);
    7.31      val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
    7.32    in
    7.33      Term.subst_TVars rho t
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 22:15:01 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 01:02:21 2014 +0100
     8.3 @@ -128,7 +128,7 @@
     8.4    val split_conj_prems: int -> thm -> thm
     8.5  
     8.6    val mk_sumTN: typ list -> typ
     8.7 -  val mk_sumTN_balanced: typ list -> typ
     8.8 +  val mk_sumprodT_balanced: typ list list -> typ
     8.9  
    8.10    val mk_proj: typ -> int -> int -> term
    8.11  
    8.12 @@ -143,7 +143,7 @@
    8.13  
    8.14    val mk_Inl: typ -> term -> term
    8.15    val mk_Inr: typ -> term -> term
    8.16 -  val mk_InN: typ list -> term -> int -> term
    8.17 +  val mk_tuple_balanced: term list -> term
    8.18    val mk_absumprod: typ -> term -> int -> int -> term list -> term
    8.19  
    8.20    val dest_sumT: typ -> typ * typ
    8.21 @@ -155,7 +155,6 @@
    8.22    val mk_If: term -> term -> term -> term
    8.23    val mk_union: term * term -> term
    8.24  
    8.25 -  val mk_sumEN: int -> thm
    8.26    val mk_absumprodE: thm -> int list -> thm
    8.27  
    8.28    val mk_sum_caseN: int -> int -> thm
    8.29 @@ -331,7 +330,7 @@
    8.30  val selN = "sel"
    8.31  val sel_corecN = selN ^ "_" ^ corecN
    8.32  
    8.33 -fun co_prefix fp = (if fp = Greatest_FP then "co" else "");
    8.34 +fun co_prefix fp = case_fp fp "" "co";
    8.35  
    8.36  fun add_components_of_typ (Type (s, Ts)) =
    8.37      cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts
    8.38 @@ -343,16 +342,20 @@
    8.39  
    8.40  val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
    8.41  
    8.42 -(* TODO: move something like this to "HOLogic"? *)
    8.43 -fun dest_tupleT 0 @{typ unit} = []
    8.44 -  | dest_tupleT 1 T = [T]
    8.45 -  | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
    8.46 +fun dest_tupleT_balanced 0 @{typ unit} = []
    8.47 +  | dest_tupleT_balanced n T = Balanced_Tree.dest HOLogic.dest_prodT n T;
    8.48  
    8.49 -fun dest_absumprodT absT repT n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o mk_repT absT repT;
    8.50 +fun dest_absumprodT absT repT n ms =
    8.51 +  map2 dest_tupleT_balanced ms o dest_sumTN_balanced n o mk_repT absT repT;
    8.52  
    8.53  val mk_sumTN = Library.foldr1 mk_sumT;
    8.54  val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
    8.55  
    8.56 +fun mk_tupleT_balanced [] = HOLogic.unitT
    8.57 +  | mk_tupleT_balanced Ts = Balanced_Tree.make HOLogic.mk_prodT Ts;
    8.58 +
    8.59 +val mk_sumprodT_balanced = mk_sumTN_balanced o map mk_tupleT_balanced;
    8.60 +
    8.61  fun mk_proj T n k =
    8.62    let val (binders, _) = strip_typeN n T in
    8.63      fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1))
    8.64 @@ -371,11 +374,7 @@
    8.65  fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
    8.66  fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
    8.67  
    8.68 -fun mk_InN [_] t 1 = t
    8.69 -  | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
    8.70 -  | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
    8.71 -  | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
    8.72 -
    8.73 +(* FIXME: reuse "mk_inj" in function package *)
    8.74  fun mk_InN_balanced sum_T n t k =
    8.75    let
    8.76      fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
    8.77 @@ -390,9 +389,12 @@
    8.78      |> repair_types sum_T
    8.79    end;
    8.80  
    8.81 +fun mk_tuple_balanced [] = HOLogic.unit
    8.82 +  | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts;
    8.83 +
    8.84  fun mk_absumprod absT abs0 n k ts =
    8.85    let val abs = mk_abs absT abs0;
    8.86 -  in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (HOLogic.mk_tuple ts) k end;
    8.87 +  in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (mk_tuple_balanced ts) k end;
    8.88  
    8.89  fun mk_case_sum (f, g) =
    8.90    let
    8.91 @@ -434,24 +436,26 @@
    8.92        if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
    8.93    in split limit 1 th end;
    8.94  
    8.95 -fun mk_sumEN 1 = @{thm one_pointE}
    8.96 -  | mk_sumEN 2 = @{thm sumE}
    8.97 -  | mk_sumEN n =
    8.98 -    (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
    8.99 -      replicate n (impI RS allI);
   8.100 -
   8.101  fun mk_obj_sumEN_balanced n =
   8.102    Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
   8.103      (replicate n asm_rl);
   8.104  
   8.105 -fun mk_tupled_allIN 0 = @{thm unit_all_impI}
   8.106 -  | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
   8.107 -  | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
   8.108 -  | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
   8.109 +fun mk_tupled_allIN_balanced 0 = @{thm unit_all_impI}
   8.110 +  | mk_tupled_allIN_balanced n =
   8.111 +    let
   8.112 +      val (tfrees, _) = BNF_Util.mk_TFrees n @{context};
   8.113 +      val T = mk_tupleT_balanced tfrees;
   8.114 +    in
   8.115 +      @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
   8.116 +      |> Drule.instantiate' [SOME (ctyp_of @{theory} T)] []
   8.117 +      |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
   8.118 +      |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
   8.119 +      |> Thm.varifyT_global
   8.120 +    end;
   8.121  
   8.122  fun mk_absumprodE type_definition ms =
   8.123    let val n = length ms in
   8.124 -    mk_obj_sumEN_balanced n OF map mk_tupled_allIN ms RS
   8.125 +    mk_obj_sumEN_balanced n OF map mk_tupled_allIN_balanced ms RS
   8.126        (type_definition RS @{thm type_copy_obj_one_point_absE})
   8.127    end;
   8.128  
   8.129 @@ -519,16 +523,16 @@
   8.130      map_cong0s =
   8.131    let
   8.132      val n = length sym_map_comps;
   8.133 -    val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
   8.134 -    val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
   8.135 -    val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   8.136 +    val rewrite_comp_comp2 = case_fp fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
   8.137 +    val rewrite_comp_comp = case_fp fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
   8.138 +    val map_cong_passive_args1 = replicate m (case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   8.139      val map_cong_active_args1 = replicate n (if is_rec
   8.140 -      then fp_case fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
   8.141 +      then case_fp fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
   8.142        else refl);
   8.143 -    val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
   8.144 +    val map_cong_passive_args2 = replicate m (case_fp fp @{thm comp_id} @{thm id_comp} RS fun_cong);
   8.145      val map_cong_active_args2 = replicate n (if is_rec
   8.146 -      then fp_case fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
   8.147 -      else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   8.148 +      then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
   8.149 +      else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   8.150      fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
   8.151      val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
   8.152      val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
   8.153 @@ -543,7 +547,7 @@
   8.154            (mk_trans rewrite1 (mk_sym rewrite2)))
   8.155        xtor_maps xtor_un_folds rewrite1s rewrite2s;
   8.156    in
   8.157 -    split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems)
   8.158 +    split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   8.159    end;
   8.160  
   8.161  fun mk_strong_coinduct_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 06 22:15:01 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Mar 07 01:02:21 2014 +0100
     9.3 @@ -821,7 +821,7 @@
     9.4      val ctr_specss = map #ctr_specs corec_specs;
     9.5      val corec_args = hd corecs
     9.6        |> fst o split_last o binder_types o fastype_of
     9.7 -      |> map (fn T => if range_type T = @{typ bool}
     9.8 +      |> map (fn T => if range_type T = HOLogic.boolT
     9.9            then Abs (Name.uu_, domain_type T, @{term False})
    9.10            else Const (@{const_name undefined}, T))
    9.11        |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
    9.12 @@ -1227,9 +1227,9 @@
    9.13                             split_last (map_filter I ctr_conds_argss_opt) ||> snd
    9.14                           else
    9.15                             Const (@{const_name Code.abort}, @{typ String.literal} -->
    9.16 -                               (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
    9.17 +                               (HOLogic.unitT --> body_type fun_T) --> body_type fun_T) $
    9.18                               HOLogic.mk_literal fun_name $
    9.19 -                             absdummy @{typ unit} (incr_boundvars 1 lhs)
    9.20 +                             absdummy HOLogic.unitT (incr_boundvars 1 lhs)
    9.21                             |> pair (map_filter I ctr_conds_argss_opt))
    9.22                           |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
    9.23                      in
    10.1 --- a/src/HOL/Tools/BNF/bnf_gfp_util.ML	Thu Mar 06 22:15:01 2014 +0100
    10.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML	Fri Mar 07 01:02:21 2014 +0100
    10.3 @@ -12,6 +12,7 @@
    10.4    val dest_listT: typ -> typ
    10.5  
    10.6    val mk_Cons: term -> term -> term
    10.7 +  val mk_InN: typ list -> term -> int -> term
    10.8    val mk_Shift: term -> term -> term
    10.9    val mk_Succ: term -> term -> term
   10.10    val mk_Times: term * term -> term
   10.11 @@ -36,18 +37,25 @@
   10.12    val mk_InN_Field: int -> int -> thm
   10.13    val mk_InN_inject: int -> int -> thm
   10.14    val mk_InN_not_InM: int -> int -> thm
   10.15 +  val mk_sumEN: int -> thm
   10.16  end;
   10.17  
   10.18  structure BNF_GFP_Util : BNF_GFP_UTIL =
   10.19  struct
   10.20  
   10.21  open BNF_Util
   10.22 +open BNF_FP_Util
   10.23  
   10.24  val mk_append = HOLogic.mk_binop @{const_name append};
   10.25  
   10.26  fun mk_equiv B R =
   10.27    Const (@{const_name equiv}, fastype_of B --> fastype_of R --> HOLogic.boolT) $ B $ R;
   10.28  
   10.29 +fun mk_InN [_] t 1 = t
   10.30 +  | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
   10.31 +  | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
   10.32 +  | mk_InN Ts t _ = raise TYPE ("mk_InN", Ts, [t]);
   10.33 +
   10.34  fun mk_Sigma (A, B) =
   10.35    let
   10.36      val AT = fastype_of A;
   10.37 @@ -160,6 +168,12 @@
   10.38    | mk_InN_inject 2 2 = @{thm Inr_inject}
   10.39    | mk_InN_inject n m = @{thm Inr_inject} RS mk_InN_inject (n - 1) (m - 1);
   10.40  
   10.41 +fun mk_sumEN 1 = @{thm one_pointE}
   10.42 +  | mk_sumEN 2 = @{thm sumE}
   10.43 +  | mk_sumEN n =
   10.44 +    (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
   10.45 +      replicate n (impI RS allI);
   10.46 +
   10.47  fun mk_specN 0 thm = thm
   10.48    | mk_specN n thm = mk_specN (n - 1) (thm RS spec);
   10.49  
    11.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Mar 06 22:15:01 2014 +0100
    11.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Mar 07 01:02:21 2014 +0100
    11.3 @@ -120,7 +120,7 @@
    11.4      val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1);
    11.5  
    11.6      fun apply_comps n kk =
    11.7 -      mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit}) (nth callers kk);
    11.8 +      mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk);
    11.9  
   11.10      val callssss =
   11.11        map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks)))