# HG changeset patch # User blanchet # Date 1394150541 -3600 # Node ID 972f0aa7091b0c647c4e744e7ca2ebf53619a484 # Parent 0c2c61a87a7d9c585690c9088e79520a083a8709 balance tuples that represent curried functions diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/BNF_FP_Base.thy Fri Mar 07 01:02:21 2014 +0100 @@ -28,12 +28,6 @@ lemma unit_all_impI: "(P () \ Q ()) \ \x. P x \ Q x" by simp -lemma prod_all_impI: "(\x y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" -by clarify - -lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" -by auto - lemma pointfree_idE: "f \ g = id \ f (g x) = x" unfolding comp_def fun_eq_iff by simp @@ -58,9 +52,6 @@ "case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p" by auto -lemma one_pointE: "\\x. s = x \ P\ \ P" -by simp - lemma obj_one_pointE: "\x. s = x \ P \ P" by blast @@ -76,9 +67,6 @@ fix x from assms show "s = f x \ P" by (cases x) auto qed -lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" -by (cases s) auto - lemma case_sum_if: "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)" by simp diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/BNF_GFP.thy --- a/src/HOL/BNF_GFP.thy Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/BNF_GFP.thy Fri Mar 07 01:02:21 2014 +0100 @@ -21,6 +21,12 @@ Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj} *} +lemma one_pointE: "\\x. s = x \ P\ \ P" +by simp + +lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" +by (cases s) auto + lemma not_TrueE: "\ True \ P" by (erule notE, rule TrueI) diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Mar 07 01:02:21 2014 +0100 @@ -365,7 +365,7 @@ end; (*avoid "'a itself" arguments in corecursors*) -fun repair_nullary_single_ctr [[]] = [[@{typ unit}]] +fun repair_nullary_single_ctr [[]] = [[HOLogic.unitT]] | repair_nullary_single_ctr Tss = Tss; fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts = @@ -479,7 +479,7 @@ (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss => mk_case_absumprod ctor_rec_absT rep fs - (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss)) + (map (mk_tuple_balanced o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss)) ctor_rec_absTs reps fss xssss))) end; @@ -978,7 +978,7 @@ val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts); val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss; - val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; + val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs; @@ -1196,7 +1196,7 @@ fun mk_map_thm ctr_def' cxIn = fold_thms lthy [ctr_def'] (unfold_thms lthy (o_apply :: pre_map_def :: - (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map @ + (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sumprod_thms_map @ abs_inverses) (cterm_instantiate_pos (nones @ [SOME cxIn]) (if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong))) @@ -1205,7 +1205,7 @@ fun mk_set_thm fp_set_thm ctr_def' cxIn = fold_thms lthy [ctr_def'] (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @ - (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set @ + (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @ abs_inverses) (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) |> singleton (Proof_Context.export names_lthy no_defs_lthy); @@ -1221,7 +1221,7 @@ fun mk_rel_thm postproc ctr_defs' cxIn cyIn = fold_thms lthy ctr_defs' (unfold_thms lthy (pre_rel_def :: abs_inverse :: - (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel @ + (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ @{thms vimage2p_def Inl_Inr_False}) (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm)) |> postproc @@ -1396,7 +1396,7 @@ abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) |> wrap_types_etc - |> fp_case fp derive_note_induct_recs_thms_for_types + |> case_fp fp derive_note_induct_recs_thms_for_types derive_note_coinduct_corecs_thms_for_types; val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Mar 07 01:02:21 2014 +0100 @@ -7,9 +7,9 @@ signature BNF_FP_DEF_SUGAR_TACTICS = sig - val sum_prod_thms_map: thm list - val sum_prod_thms_set: thm list - val sum_prod_thms_rel: thm list + val sumprod_thms_map: thm list + val sumprod_thms_set: thm list + val sumprod_thms_rel: thm list val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> @@ -37,12 +37,12 @@ val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; -val sum_prod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; -val sum_prod_thms_set = +val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; +val sumprod_thms_set = @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff Union_Un_distrib image_iff o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; -val sum_prod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply}; +val sumprod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply}; fun hhf_concl_conv cv ctxt ct = (case Thm.term_of ct of @@ -87,13 +87,13 @@ val rec_unfold_thms = @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv - case_unit_Unity} @ sum_prod_thms_map; + case_unit_Unity} @ sumprod_thms_map; fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl); -val corec_unfold_thms = @{thms id_def} @ sum_prod_thms_map; +val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map; fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt = let @@ -121,7 +121,7 @@ pre_set_defs = HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @ - sum_prod_thms_set)), + sumprod_thms_set)), solve_prem_prem_tac ctxt]) (rev kks))); fun mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps pre_set_defs m k @@ -153,7 +153,7 @@ (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN' SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN' SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor :: - sels @ sum_prod_thms_rel @ @{thms o_apply vimage2p_def})) THEN' + sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN' (atac ORELSE' REPEAT o etac conjE THEN' full_simp_tac (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN' diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Mar 07 01:02:21 2014 +0100 @@ -52,20 +52,20 @@ fun of_fp_res get = map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars; - fun mk_co_algT T U = fp_case fp (T --> U) (U --> T); - fun co_swap pair = fp_case fp I swap pair; + fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); + fun co_swap pair = case_fp fp I swap pair; val mk_co_comp = HOLogic.mk_comp o co_swap; - val co_productC = BNF_FP_Rec_Sugar_Util.fp_case fp @{type_name prod} @{type_name sum}; + val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum}; val dest_co_algT = co_swap o dest_funT; - val co_alg_argT = fp_case fp range_type domain_type; - val co_alg_funT = fp_case fp domain_type range_type; - val mk_co_product = curry (fp_case fp mk_convol mk_case_sum); - val mk_map_co_product = fp_case fp mk_prod_map mk_map_sum; - val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd); - val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT); - val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT; - val rewrite_comp_comp = fp_case fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp}; + val co_alg_argT = case_fp fp range_type domain_type; + val co_alg_funT = case_fp fp domain_type range_type; + val mk_co_product = curry (case_fp fp mk_convol mk_case_sum); + val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum; + val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd); + val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT); + val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT; + val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp}; val fp_absT_infos = map #absT_info fp_sugars; val fp_bnfs = of_fp_res #bnfs; @@ -115,7 +115,7 @@ val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors); val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors); in - ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (fp_case fp ctors dtors)) + ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors)) end; val absATs = map (domain_type o fastype_of) ctors; @@ -283,7 +283,7 @@ end; fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t = - fp_case fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep)) + case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep)) (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t))); fun mk_rec b_opt recs lthy TU = @@ -358,7 +358,7 @@ fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd) end; - val recN = fp_case fp ctor_recN dtor_corecN; + val recN = case_fp fp ctor_recN dtor_corecN; fun mk_recs lthy = fold2 (fn TU => fn b => fn ((recs, defs), lthy) => mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs))) @@ -403,10 +403,10 @@ val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms); - val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: + val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @ @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id}; - val rec_thms = fold_thms @ fp_case fp + val rec_thms = fold_thms @ case_fp fp @{thms fst_convol map_prod_o_convol convol_o} @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum}; @@ -415,7 +415,7 @@ val map_thms = no_refl (maps (fn bnf => let val map_comp0 = map_comp0_of_bnf bnf RS sym in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @ - remove eq_thm_prop_untyped (fp_case fp @{thm comp_assoc[symmetric]} @{thm comp_assoc}) + remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc}) (map2 (fn thm => fn bnf => @{thm type_copy_map_comp0_undo} OF (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Mar 07 01:02:21 2014 +0100 @@ -101,7 +101,7 @@ xs ([], ([], [])); fun key_of_fp_eqs fp fpTs fp_eqs = - Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs); + Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs); fun get_indices callers t = callers @@ -191,7 +191,7 @@ val ctr_Tsss = map (map binder_types) ctr_Tss; val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss; - val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; + val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; val ns = map length ctr_Tsss; val kss = map (fn n => 1 upto n) ns; diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 07 01:02:21 2014 +0100 @@ -10,7 +10,7 @@ sig datatype fp_kind = Least_FP | Greatest_FP - val fp_case: fp_kind -> 'a -> 'a -> 'a + val case_fp: fp_kind -> 'a -> 'a -> 'a val flat_rec_arg_args: 'a list list -> 'a list @@ -48,8 +48,8 @@ datatype fp_kind = Least_FP | Greatest_FP; -fun fp_case Least_FP l _ = l - | fp_case Greatest_FP _ g = g; +fun case_fp Least_FP l _ = l + | case_fp Greatest_FP _ g = g; fun flat_rec_arg_args xss = (* FIXME (once the old datatype package is phased out): The first line below gives the preferred @@ -107,8 +107,8 @@ fun mk_co_rec thy fp fpT Cs t = let val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last; - val fpT0 = fp_case fp prebody body; - val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs); + val fpT0 = case_fp fp prebody body; + val Cs0 = distinct (op =) (map (case_fp fp body_type domain_type) f_Cs); val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs); in Term.subst_TVars rho t diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 07 01:02:21 2014 +0100 @@ -128,7 +128,7 @@ val split_conj_prems: int -> thm -> thm val mk_sumTN: typ list -> typ - val mk_sumTN_balanced: typ list -> typ + val mk_sumprodT_balanced: typ list list -> typ val mk_proj: typ -> int -> int -> term @@ -143,7 +143,7 @@ val mk_Inl: typ -> term -> term val mk_Inr: typ -> term -> term - val mk_InN: typ list -> term -> int -> term + val mk_tuple_balanced: term list -> term val mk_absumprod: typ -> term -> int -> int -> term list -> term val dest_sumT: typ -> typ * typ @@ -155,7 +155,6 @@ val mk_If: term -> term -> term -> term val mk_union: term * term -> term - val mk_sumEN: int -> thm val mk_absumprodE: thm -> int list -> thm val mk_sum_caseN: int -> int -> thm @@ -331,7 +330,7 @@ val selN = "sel" val sel_corecN = selN ^ "_" ^ corecN -fun co_prefix fp = (if fp = Greatest_FP then "co" else ""); +fun co_prefix fp = case_fp fp "" "co"; fun add_components_of_typ (Type (s, Ts)) = cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts @@ -343,16 +342,20 @@ val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; -(* TODO: move something like this to "HOLogic"? *) -fun dest_tupleT 0 @{typ unit} = [] - | dest_tupleT 1 T = [T] - | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T'; +fun dest_tupleT_balanced 0 @{typ unit} = [] + | dest_tupleT_balanced n T = Balanced_Tree.dest HOLogic.dest_prodT n T; -fun dest_absumprodT absT repT n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o mk_repT absT repT; +fun dest_absumprodT absT repT n ms = + map2 dest_tupleT_balanced ms o dest_sumTN_balanced n o mk_repT absT repT; val mk_sumTN = Library.foldr1 mk_sumT; val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; +fun mk_tupleT_balanced [] = HOLogic.unitT + | mk_tupleT_balanced Ts = Balanced_Tree.make HOLogic.mk_prodT Ts; + +val mk_sumprodT_balanced = mk_sumTN_balanced o map mk_tupleT_balanced; + fun mk_proj T n k = let val (binders, _) = strip_typeN n T in fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1)) @@ -371,11 +374,7 @@ fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT)); fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; -fun mk_InN [_] t 1 = t - | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t - | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) - | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t])); - +(* FIXME: reuse "mk_inj" in function package *) fun mk_InN_balanced sum_T n t k = let fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t @@ -390,9 +389,12 @@ |> repair_types sum_T end; +fun mk_tuple_balanced [] = HOLogic.unit + | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts; + fun mk_absumprod absT abs0 n k ts = let val abs = mk_abs absT abs0; - in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (HOLogic.mk_tuple ts) k end; + in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (mk_tuple_balanced ts) k end; fun mk_case_sum (f, g) = let @@ -434,24 +436,26 @@ if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th; in split limit 1 th end; -fun mk_sumEN 1 = @{thm one_pointE} - | mk_sumEN 2 = @{thm sumE} - | mk_sumEN n = - (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF - replicate n (impI RS allI); - fun mk_obj_sumEN_balanced n = Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) (replicate n asm_rl); -fun mk_tupled_allIN 0 = @{thm unit_all_impI} - | mk_tupled_allIN 1 = @{thm impI[THEN allI]} - | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*) - | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step}; +fun mk_tupled_allIN_balanced 0 = @{thm unit_all_impI} + | mk_tupled_allIN_balanced n = + let + val (tfrees, _) = BNF_Util.mk_TFrees n @{context}; + val T = mk_tupleT_balanced tfrees; + in + @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]} + |> Drule.instantiate' [SOME (ctyp_of @{theory} T)] [] + |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]} + |> (fn thm => impI RS funpow n (fn th => allI RS th) thm) + |> Thm.varifyT_global + end; fun mk_absumprodE type_definition ms = let val n = length ms in - mk_obj_sumEN_balanced n OF map mk_tupled_allIN ms RS + mk_obj_sumEN_balanced n OF map mk_tupled_allIN_balanced ms RS (type_definition RS @{thm type_copy_obj_one_point_absE}) end; @@ -519,16 +523,16 @@ map_cong0s = let val n = length sym_map_comps; - val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; - val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; - val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong); + val rewrite_comp_comp2 = case_fp fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; + val rewrite_comp_comp = case_fp fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; + val map_cong_passive_args1 = replicate m (case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong); val map_cong_active_args1 = replicate n (if is_rec - then fp_case fp @{thm convol_o} @{thm o_case_sum} RS fun_cong + then case_fp fp @{thm convol_o} @{thm o_case_sum} RS fun_cong else refl); - val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong); + val map_cong_passive_args2 = replicate m (case_fp fp @{thm comp_id} @{thm id_comp} RS fun_cong); val map_cong_active_args2 = replicate n (if is_rec - then fp_case fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id} - else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong); + then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id} + else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong); fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s; val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1; val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; @@ -543,7 +547,7 @@ (mk_trans rewrite1 (mk_sym rewrite2))) xtor_maps xtor_un_folds rewrite1s rewrite2s; in - split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems) + split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems) end; fun mk_strong_coinduct_thm coind rel_eqs rel_monos mk_vimage2p ctxt = diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Mar 07 01:02:21 2014 +0100 @@ -821,7 +821,7 @@ val ctr_specss = map #ctr_specs corec_specs; val corec_args = hd corecs |> fst o split_last o binder_types o fastype_of - |> map (fn T => if range_type T = @{typ bool} + |> map (fn T => if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False}) else Const (@{const_name undefined}, T)) |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss @@ -1227,9 +1227,9 @@ split_last (map_filter I ctr_conds_argss_opt) ||> snd else Const (@{const_name Code.abort}, @{typ String.literal} --> - (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ + (HOLogic.unitT --> body_type fun_T) --> body_type fun_T) $ HOLogic.mk_literal fun_name $ - absdummy @{typ unit} (incr_boundvars 1 lhs) + absdummy HOLogic.unitT (incr_boundvars 1 lhs) |> pair (map_filter I ctr_conds_argss_opt)) |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) in diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_gfp_util.ML --- a/src/HOL/Tools/BNF/bnf_gfp_util.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML Fri Mar 07 01:02:21 2014 +0100 @@ -12,6 +12,7 @@ val dest_listT: typ -> typ val mk_Cons: term -> term -> term + val mk_InN: typ list -> term -> int -> term val mk_Shift: term -> term -> term val mk_Succ: term -> term -> term val mk_Times: term * term -> term @@ -36,18 +37,25 @@ val mk_InN_Field: int -> int -> thm val mk_InN_inject: int -> int -> thm val mk_InN_not_InM: int -> int -> thm + val mk_sumEN: int -> thm end; structure BNF_GFP_Util : BNF_GFP_UTIL = struct open BNF_Util +open BNF_FP_Util val mk_append = HOLogic.mk_binop @{const_name append}; fun mk_equiv B R = Const (@{const_name equiv}, fastype_of B --> fastype_of R --> HOLogic.boolT) $ B $ R; +fun mk_InN [_] t 1 = t + | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t + | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) + | mk_InN Ts t _ = raise TYPE ("mk_InN", Ts, [t]); + fun mk_Sigma (A, B) = let val AT = fastype_of A; @@ -160,6 +168,12 @@ | mk_InN_inject 2 2 = @{thm Inr_inject} | mk_InN_inject n m = @{thm Inr_inject} RS mk_InN_inject (n - 1) (m - 1); +fun mk_sumEN 1 = @{thm one_pointE} + | mk_sumEN 2 = @{thm sumE} + | mk_sumEN n = + (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF + replicate n (impI RS allI); + fun mk_specN 0 thm = thm | mk_specN n thm = mk_specN (n - 1) (thm RS spec); diff -r 0c2c61a87a7d -r 972f0aa7091b src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Mar 06 22:15:01 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Mar 07 01:02:21 2014 +0100 @@ -120,7 +120,7 @@ val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1); fun apply_comps n kk = - mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit}) (nth callers kk); + mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk); val callssss = map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks)))