# HG changeset patch # User traytel # Date 1460658582 -7200 # Node ID c50c764aab10f3b06bd471a891d320e8af9d47c1 # Parent 1ba3aacfa4d3b0f92bc92facc01f83027aa90372 n2m operates on (un)folds diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Basic_BNF_LFPs.thy --- a/src/HOL/Basic_BNF_LFPs.thy Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Basic_BNF_LFPs.thy Thu Apr 14 20:29:42 2016 +0200 @@ -62,6 +62,9 @@ lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (id_bnf \ g \ id_bnf))" unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) +lemma ctor_rec_transfer: "rel_fun (rel_fun (vimage2p id_bnf id_bnf R) S) (rel_fun R S) ctor_rec ctor_rec" + unfolding rel_fun_def vimage2p_def id_bnf_def ctor_rec_def by simp + lemma eq_fst_iff: "a = fst p \ (\b. p = (a, b))" by (cases p) auto diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Apr 14 20:29:42 2016 +0200 @@ -24,24 +24,22 @@ open BNF_Tactics open BNF_FP_N2M_Tactics -fun mk_prod_map f g = +fun mk_arg_cong ctxt n t = let - val ((fAT, fBT), fT) = `dest_funT (fastype_of f); - val ((gAT, gBT), gT) = `dest_funT (fastype_of g); + val Us = fastype_of t |> strip_typeN n |> fst; + val ((xs, ys), _) = ctxt + |> mk_Frees "x" Us + ||>> mk_Frees "y" Us; + val goal = Logic.list_implies (@{map 2} (curry mk_Trueprop_eq) xs ys, + mk_Trueprop_eq (list_comb (t, xs), list_comb (t, ys))); + val vars = Variable.add_free_names ctxt goal []; in - Const (@{const_name map_prod}, - fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g + Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => + HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl)) + |> Thm.close_derivation end; -fun mk_map_sum f g = - let - val ((fAT, fBT), fT) = `dest_funT (fastype_of f); - val ((gAT, gBT), gT) = `dest_funT (fastype_of g); - in - Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g - end; - -fun construct_mutualized_fp fp flat_mutual_cliques fpTs indexed_fp_ress bs resBs (resDs, Dss) bnfs +fun construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress bs resBs (resDs, Dss) bnfs (absT_infos : absT_info list) lthy = let val time = time lthy; @@ -54,22 +52,16 @@ fun of_fp_res get = map (uncurry nth o swap o apsnd get) indexed_fp_ress; 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 = case_fp fp @{type_name prod} @{type_name sum}; + val mk_co_comp = curry (HOLogic.mk_comp o co_swap); val dest_co_algT = co_swap o dest_funT; 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 = of_fp_res #absT_infos; val fp_bnfs = of_fp_res #bnfs; - val pre_bnfs = of_fp_res #pre_bnfs; + val fp_pre_bnfs = of_fp_res #pre_bnfs; val fp_absTs = map #absT fp_absT_infos; val fp_repTs = map #repT fp_absT_infos; @@ -93,8 +85,9 @@ val m = length As; val live = m + n; - val ((Xs, Bs), names_lthy) = names_lthy + val (((Xs, Ys), Bs), names_lthy) = names_lthy |> mk_TFrees n + ||>> mk_TFrees n ||>> mk_TFrees m; val allAs = As @ Xs; @@ -104,7 +97,6 @@ val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs; val fold_thetaAs = Xs ~~ fpTs; val fold_thetaBs = Xs ~~ fpTs'; - val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs; val pre_phiTs = map2 mk_pred2T fpTs fpTs'; val ((ctors, dtors), (xtor's, xtors)) = @@ -167,7 +159,7 @@ val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs; - val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs; + val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) fp_pre_bnfs; val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct) |> map (zero_var_indexes o unfold_thms lthy (id_apply :: rel_unfolds)); @@ -189,23 +181,26 @@ val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs); val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs; + fun mutual_instantiate ctxt inst = + let + val thetas = AList.group (op =) (mutual_cliques ~~ inst); + in + map2 (infer_instantiate ctxt o the o AList.lookup (op =) thetas) mutual_cliques + end; + val rel_xtor_co_inducts_inst = let val extract = case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb); val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts; - val thetas = - AList.group (op =) - (flat_mutual_cliques ~~ - map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis)); + val inst = map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis); in - map2 (infer_instantiate lthy o the o AList.lookup (op =) thetas) - flat_mutual_cliques rel_xtor_co_inducts + mutual_instantiate lthy inst rel_xtor_co_inducts end val xtor_rel_co_induct = mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys - xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts_inst rel_defs + xtors xtor's (mk_rel_xtor_co_induct_tac fp abs_inverses rel_xtor_co_inducts_inst rel_defs rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos) lthy; @@ -255,34 +250,21 @@ val timer = time (timer "Nested-to-mutual (co)induction"); val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs; - val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs; - val rec_strTs = map2 mk_co_algT rec_preTs Xs; + val fold_strTs = map2 mk_co_algT fold_preTs Xs; val resTs = map2 mk_co_algT fpTs Xs; - val ((rec_strs, rec_strs'), names_lthy) = names_lthy - |> mk_Frees' "s" rec_strTs; + val ((fold_strs, fold_strs'), names_lthy) = names_lthy + |> mk_Frees' "s" fold_strTs; - val xtor_co_recs = of_fp_res #xtor_co_recs; + val fp_un_folds = of_fp_res #xtor_un_folds; val ns = map (length o #Ts o snd) indexed_fp_ress; - fun foldT_of_recT recT = - let - val ((FTXs, Ys), TX) = strip_fun_type recT |>> map_split dest_co_algT; - val Zs = union op = Xs Ys; - fun subst (Type (C, Ts as [_, X])) = - if C = co_productC andalso member op = Zs X then X else Type (C, map subst Ts) - | subst (Type (C, Ts)) = Type (C, map subst Ts) - | subst T = T; - in - map2 (mk_co_algT o subst) FTXs Ys ---> TX - end; - - fun force_rec i TU raw_rec = + fun force_fold i TU raw_un_fold = let val thy = Proof_Context.theory_of lthy; - val approx_rec = raw_rec + val approx_un_fold = raw_un_fold |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU); val subst = Term.typ_subst_atomic fold_thetaAs; @@ -295,35 +277,35 @@ map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ sorted_fpTs))) fold_preTs'; val (mutual_clique, TUs) = - map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec))) + map_split dest_co_algT (binder_fun_types (fastype_of approx_un_fold)) |>> map subst - |> `(fn (_, Ys) => nth flat_mutual_cliques + |> `(fn (_, Ys) => nth mutual_cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs)) ||> uncurry (map2 mk_co_algT); - val cands = flat_mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs; + val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs; val js = find_indices (fn ((cl, cand), TU) => cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands; val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js; in - force_typ names_lthy (Tpats ---> TU) raw_rec + force_typ names_lthy (Tpats ---> TU) raw_un_fold end; fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t = 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 = + fun mk_un_fold b_opt un_folds lthy TU = let val thy = Proof_Context.theory_of lthy; val x = co_alg_argT TU; val i = find_index (fn T => x = T) Xs; - val TUrec = - (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of - NONE => force_rec i TU (nth xtor_co_recs i) + val TUfold = + (case find_first (fn f => body_fun_type (fastype_of f) = TU) un_folds of + NONE => force_fold i TU (nth fp_un_folds i) | SOME f => f); - val TUs = binder_fun_types (fastype_of TUrec); + val TUs = binder_fun_types (fastype_of TUfold); fun mk_s TU' = let @@ -338,8 +320,8 @@ val sF' = mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF handle Term.TYPE _ => sF; - val F = nth rec_preTs i; - val s = nth rec_strs i; + val F = nth fold_preTs i; + val s = nth fold_strs i; in if sF = F then s else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s @@ -356,131 +338,190 @@ (if domain_type T_to_U = range_type T_to_U then HOLogic.id_const (domain_type T_to_U) else - let - val (TY, (U, X)) = T_to_U |> dest_co_algT ||> dest_co_productT; - val T = mk_co_algT TY U; - fun mk_co_proj TU = - build_map lthy [] (fn TU => - let val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT in - if T1 = U then co_proj1_const TU - else mk_co_comp (mk_co_proj (co_swap (T1, U)), - co_proj1_const (co_swap (mk_co_productT T1 T2, T1))) - end) - TU; - fun default () = - mk_co_product (mk_co_proj (dest_funT T)) - (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X)))); - in - if can dest_co_productT TY then - mk_map_co_product (mk_co_proj (co_swap (dest_co_productT TY |> fst, U))) - (HOLogic.id_const X) - handle TYPE _ => default () (*N2M involving "prod" type*) - else - default () - end) + fst (fst (mk_un_fold NONE un_folds lthy T_to_U))); val smap_args = map mk_smap_arg smap_argTs; in mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep - (mk_co_comp (s, Term.list_comb (smap, smap_args))) + (mk_co_comp s (Term.list_comb (smap, smap_args))) end end; - val t = Term.list_comb (TUrec, map mk_s TUs); + val t = Term.list_comb (TUfold, map mk_s TUs); in (case b_opt of NONE => ((t, Drule.dummy_thm), lthy) | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), - fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd) + fold_rev Term.absfree fold_strs' t)) lthy |>> apsnd snd) end; - 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))) - resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy) + val foldN = case_fp fp ctor_foldN dtor_unfoldN; + fun mk_un_folds lthy = + fold2 (fn TU => fn b => fn ((un_folds, defs), lthy) => + mk_un_fold (SOME b) un_folds lthy TU |>> (fn (f, d) => (f :: un_folds, d :: defs))) + resTs (map (Binding.suffix_name ("_" ^ foldN)) bs) (([], []), lthy) |>> map_prod rev rev; - val ((raw_xtor_co_recs, raw_xtor_co_rec_defs), (lthy, raw_lthy)) = lthy + val ((raw_xtor_un_folds, raw_xtor_un_fold_defs), (lthy, raw_lthy)) = lthy |> Local_Theory.open_target |> snd - |> mk_recs + |> mk_un_folds ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism raw_lthy lthy; - val xtor_co_recs = map (Morphism.term phi) raw_xtor_co_recs; + val xtor_un_folds = map (Morphism.term phi) raw_xtor_un_folds; + val xtor_un_fold_defs = map (Morphism.thm phi) raw_xtor_un_fold_defs; + val xtor_un_folds' = map2 (fn raw => fn t => Const (fst (dest_Const t), fastype_of raw)) raw_xtor_un_folds xtor_un_folds; - val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps + val fp_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps |> maps (fn thm => [thm, thm RS rewrite_comp_comp]); - val xtor_co_rec_thms = + val un_folds = map (fn fold => Term.list_comb (fold, fold_strs)) raw_xtor_un_folds; + val fold_mapTs = co_swap (As @ fpTs, As @ Xs); + val pre_fold_maps = @{map 2} (fn Ds => uncurry (mk_map_of_bnf Ds) fold_mapTs) Dss bnfs + fun mk_pre_fold_maps fs = + map (fn mapx => Term.list_comb (mapx, map HOLogic.id_const As @ fs)) pre_fold_maps; + + val pre_map_defs = no_refl (map map_def_of_bnf bnfs); + val fp_map_defs = no_refl (map map_def_of_bnf fp_pre_bnfs); + val map_defs = pre_map_defs @ fp_map_defs; + val pre_rel_defs = no_refl (map rel_def_of_bnf bnfs); + val fp_rel_defs = no_refl (map rel_def_of_bnf fp_pre_bnfs); + val rel_defs = pre_rel_defs @ fp_rel_defs; + fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs}) + |> (fn thm => [thm, thm RS rewrite_comp_comp]); + val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions; + val pre_Rep_o_Abss = maps mk_Rep_o_Abs type_definitions; + val Rep_o_Abss = fp_Rep_o_Abss @ pre_Rep_o_Abss; + + val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs)); + val simp_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: + @{thms id_apply comp_id id_comp}; + + val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of; + + 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_or_nesting_bnfs) @ + 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 + rewrite_comp_comp) + type_definitions bnfs); + + val xtor_un_fold_thms = let - val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_xtor_co_recs; - val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs); - val pre_rec_maps = - map2 (fn Ds => fn bnf => - Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf, - map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs)) - Dss bnfs; - + val pre_fold_maps = mk_pre_fold_maps un_folds; fun mk_goals f xtor s smap fp_abs fp_rep abs rep = let - val lhs = mk_co_comp (f, xtor); - val rhs = mk_co_comp (s, smap); + val lhs = mk_co_comp f xtor; + val rhs = mk_co_comp s smap; in HOLogic.mk_eq (lhs, mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs)) fp_abs fp_rep abs rep rhs) end; - val goals = @{map 8} mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps; - - val pre_map_defs = no_refl (map map_def_of_bnf bnfs); - val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs); - - val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs)); - - val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms); - - 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 @ case_fp fp - @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod} - @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)}; - - val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of; + val goals = @{map 8} mk_goals un_folds xtors fold_strs pre_fold_maps fp_abss fp_reps abss reps; - 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_or_nesting_bnfs) @ - 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 - rewrite_comp_comp) - type_definitions bnfs); + val fp_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_un_fold_thms); - fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs}) - |> (fn thm => [thm, thm RS rewrite_comp_comp]); - - val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions; - val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions; - - fun tac {context = ctxt, prems = _} = - unfold_thms_tac ctxt (flat [rec_thms, raw_xtor_co_rec_defs, pre_map_defs, - fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, - Rep_o_Abss]) THEN - CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) bnfs; + val simps = flat [simp_thms, raw_xtor_un_fold_defs, map_defs, fp_un_folds, + fp_un_fold_o_maps, map_thms, Rep_o_Abss]; in Library.foldr1 HOLogic.mk_conj goals |> HOLogic.mk_Trueprop - |> fold_rev Logic.all rec_strs - |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac) + |> fold_rev Logic.all fold_strs + |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal + (fn {context = ctxt, prems = _} => mk_xtor_un_fold_tac ctxt n simps)) |> Thm.close_derivation |> Morphism.thm phi |> split_conj_thm |> map (fn thm => thm RS @{thm comp_eq_dest}) end; + val xtor_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps + |> maps (fn thm => [thm, thm RS rewrite_comp_comp]); + val xtor_un_fold_unique_thm = + let + val (fs, _) = names_lthy |> mk_Frees "f" resTs; + val fold_maps = mk_pre_fold_maps fs; + fun mk_prem f s mapx xtor fp_abs fp_rep abs rep = + let + val lhs = mk_co_comp f xtor; + val rhs = mk_co_comp s mapx; + in + mk_Trueprop_eq (lhs, + mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs)) + fp_abs fp_rep abs rep rhs) + end; + val prems = @{map 8} mk_prem fs fold_strs fold_maps xtors fp_abss fp_reps abss reps; + val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 (curry HOLogic.mk_eq) fs un_folds)); + val vars = Variable.add_free_names raw_lthy concl []; + val fp_un_fold_uniques0 = of_fp_res (split_conj_thm o #xtor_un_fold_unique) + |> map (Drule.zero_var_indexes o unfold_thms lthy fp_map_defs); + val names = fp_un_fold_uniques0 + |> map (Thm.concl_of #> HOLogic.dest_Trueprop + #> HOLogic.dest_eq #> fst #> dest_Var #> fst); + val inst = names ~~ map (Thm.cterm_of lthy) fs; + val fp_un_fold_uniques = mutual_instantiate lthy inst fp_un_fold_uniques0; + val map_arg_congs = + map (fn bnf => mk_arg_cong lthy (live_of_bnf bnf) (map_of_bnf bnf) + |> unfold_thms lthy (pre_map_defs @ simp_thms)) nesting_bnfs; + in + Goal.prove_sorry raw_lthy vars prems concl + (mk_xtor_un_fold_unique_tac fp raw_xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps + Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs) + |> Thm.close_derivation + |> case_fp fp I (fn thm => thm OF replicate n sym) + |> Morphism.thm phi + end; + + val ABs = As ~~ Bs; + val XYs = Xs ~~ Ys; + val ABphiTs = @{map 2} mk_pred2T As Bs; + val XYphiTs = @{map 2} mk_pred2T Xs Ys; + + val ((ABphis, XYphis), _) = names_lthy + |> mk_Frees "R" ABphiTs + ||>> mk_Frees "S" XYphiTs; + + val pre_rels = @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ Xs) (Bs @ Ys)) Dss bnfs; + + val ns = map (fn i => length (filter (fn c => i = c) mutual_cliques)) mutual_cliques; + + val map_transfers = map (funpow live (fn thm => thm RS @{thm rel_funD}) + #> unfold_thms lthy pre_rel_defs) + (map map_transfer_of_bnf bnfs); + val fp_un_fold_transfers = map2 (fn n => funpow n (fn thm => thm RS @{thm rel_funD}) + #> unfold_thms lthy fp_rel_defs) + ns (of_fp_res #xtor_un_fold_transfers); + val pre_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions; + val fp_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) fp_type_definitions; + val Abs_transfers = pre_Abs_transfers @ fp_Abs_transfers; + + fun tac {context = ctxt, prems = _} = + mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers + map_transfers Abs_transfers fp_or_nesting_rel_eqs; + + val xtor_un_fold_transfer_thms = + mk_xtor_co_iter_transfer_thms fp pre_rels XYphis XYphis rels ABphis + xtor_un_folds' (map (subst_atomic_types (ABs @ XYs)) xtor_un_folds') tac lthy; + + val timer = time (timer "Nested-to-mutual (co)iteration"); + + val xtor_maps = of_fp_res #xtor_maps; + val xtor_rels = of_fp_res #xtor_rels; + fun mk_Ts Cs = map (typ_subst_atomic (As ~~ Cs)) fpTs; + val phi = Local_Theory.target_morphism lthy; + val export = map (Morphism.term phi); + val ((xtor_co_recs, (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, + xtor_co_rec_transfer_thms)), lthy) = lthy + |> derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) bnfs + (export xtors) (export xtor_un_folds) + xtor_un_fold_unique_thm xtor_un_fold_thms xtor_un_fold_transfer_thms xtor_maps xtor_rels + (@{map 2} (curry (SOME o @{apply 2} (morph_absT_info phi))) fp_absT_infos absT_infos); + val timer = time (timer "Nested-to-mutual (co)recursion"); val common_notes = @@ -496,8 +537,8 @@ val notes = (case fp of - Least_FP => [(ctor_recN, xtor_co_rec_thms)] - | Greatest_FP => [(dtor_corecN, xtor_co_rec_thms)]) + Least_FP => [(ctor_foldN, xtor_un_fold_thms)] + | Greatest_FP => [(dtor_unfoldN, xtor_un_fold_thms)]) |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => @@ -512,23 +553,24 @@ val fp_res = ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos, dtors = dtors, ctors = ctors, - xtor_un_folds = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs, + xtor_un_folds = xtor_un_folds, xtor_co_recs = xtor_co_recs, xtor_co_induct = xtor_co_induct_thm, dtor_ctors = of_fp_res #dtor_ctors (*too general types*), ctor_dtors = of_fp_res #ctor_dtors (*too general types*), ctor_injects = of_fp_res #ctor_injects (*too general types*), dtor_injects = of_fp_res #dtor_injects (*too general types*), xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), - xtor_map_unique = TrueI (*wrong*), + xtor_map_unique = xtor_un_fold_unique_thm (*wrong*), xtor_setss = of_fp_res #xtor_setss (*too general types and terms*), xtor_rels = of_fp_res #xtor_rels (*too general types and terms*), - xtor_un_fold_thms = xtor_co_rec_thms (*wrong*), - xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*), - xtor_un_fold_unique = TrueI (*too general types and terms*), - xtor_co_rec_unique = TrueI (*wrong*), - xtor_un_fold_o_maps = fp_rec_o_maps (*wrong*), - xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*), - xtor_un_fold_transfers = [], xtor_co_rec_transfers = [], + xtor_un_fold_thms = xtor_un_fold_thms, + xtor_co_rec_thms = xtor_co_rec_thms, + xtor_un_fold_unique = xtor_un_fold_unique_thm, + xtor_co_rec_unique = xtor_co_rec_unique_thm, + xtor_un_fold_o_maps = fp_un_fold_o_maps (*wrong*), + xtor_co_rec_o_maps = xtor_co_rec_o_map_thms (*wrong*), + xtor_un_fold_transfers = xtor_un_fold_transfer_thms, + xtor_co_rec_transfers = xtor_co_rec_transfer_thms (*wrong*), xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []} |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); in diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Thu Apr 14 20:29:42 2016 +0200 @@ -7,8 +7,14 @@ signature BNF_FP_N2M_TACTICS = sig - val mk_rel_xtor_co_induct_tactic: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> + val mk_rel_xtor_co_induct_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic + val mk_xtor_un_fold_unique_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> + thm list -> thm list -> thm list -> thm list -> thm list -> + {context: Proof.context, prems: thm list} -> tactic + val mk_xtor_un_fold_tac: Proof.context -> int -> thm list -> tactic + val mk_xtor_un_fold_transfer_tac: Proof.context -> int -> thm list -> thm list -> thm list -> + thm list -> thm list -> thm list -> tactic end; structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS = @@ -20,7 +26,7 @@ val vimage2p_unfolds = o_apply :: @{thms vimage2p_def}; -fun mk_rel_xtor_co_induct_tactic fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0 +fun mk_rel_xtor_co_induct_tac fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0 nesting_rel_monos0 {context = ctxt, prems = raw_C_IHs} = let val nesting_rel_eqs = @{thms prod.rel_eq sum.rel_eq} @ nesting_rel_eqs0; @@ -54,4 +60,36 @@ co_inducts) end; +fun mk_xtor_un_fold_unique_tac fp xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps + Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs {context = ctxt, prems} = + unfold_thms_tac ctxt xtor_un_fold_defs THEN + HEADGOAL (REPEAT_DETERM o FIRST' [hyp_subst_tac_thin true ctxt, rtac ctxt refl, + rtac ctxt conjI, + rtac ctxt @{thm arg_cong2[of _ _ _ _ "op o", OF refl]}, + rtac ctxt @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}, + resolve_tac ctxt map_arg_congs, + resolve_tac ctxt fp_un_fold_uniques THEN_ALL_NEW case_fp fp (K all_tac) (rtac ctxt sym), + SELECT_GOAL (CHANGED (unfold_thms_tac ctxt (flat [simp_thms, map_thms, map_defs, + xtor_un_fold_defs, xtor_un_fold_o_maps, Rep_o_Abss, prems])))]); + +fun mk_xtor_un_fold_tac ctxt n simps = + unfold_thms_tac ctxt simps THEN + CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) (1 upto n); + +fun mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers + map_transfers Abs_transfers fp_or_nesting_rel_eqs = + let + val unfold = SELECT_GOAL (unfold_thms_tac ctxt fp_or_nesting_rel_eqs); + in + unfold_thms_tac ctxt (xtor_un_fold_defs @ rel_defs) THEN + HEADGOAL (CONJ_WRAP' + (fn thm => EVERY' [REPEAT_DETERM_N n o rtac ctxt rel_funI, rtac ctxt thm THEN_ALL_NEW + REPEAT_DETERM o (FIRST' [assume_tac ctxt, rtac ctxt @{thm id_transfer}, + rtac ctxt @{thm rel_funD[OF rel_funD[OF comp_transfer]]}, + resolve_tac ctxt fp_un_fold_transfers, resolve_tac ctxt map_transfers, + resolve_tac ctxt Abs_transfers, rtac ctxt @{thm vimage2p_rel_fun}, + unfold THEN' rtac ctxt @{thm vimage2p_rel_fun}])]) + fp_un_fold_transfers) + end; + end; diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Apr 14 20:29:42 2016 +0200 @@ -200,7 +200,9 @@ thm list -> thm list -> thm list val derive_xtor_co_recs: BNF_Util.fp_kind -> binding list -> (typ list -> typ list) -> (typ list list * typ list) -> BNF_Def.bnf list -> term list -> term list -> - thm -> thm list -> thm list -> thm list -> thm list -> local_theory -> + thm -> thm list -> thm list -> thm list -> thm list -> + (BNF_Comp.absT_info * BNF_Comp.absT_info) option list -> + local_theory -> (term list * (thm list * thm * thm list * thm list)) * local_theory val fixpoint_bnf: (binding -> binding) -> @@ -624,19 +626,65 @@ #> Syntax.check_term ctxt #> singleton (Variable.polymorphic ctxt); -fun mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique_thm map_id0s = - (xtor_un_fold_unique_thm OF - map (fn thm => case_fp fp - (mk_trans @{thm id_o} - (mk_sym (thm RS @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]}))) - (mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) - @{thm trans[OF id_o o_id[symmetric]]})) - map_id0s) - |> split_conj_thm |> map mk_sym; +fun absT_info_encodeT thy (SOME (src : absT_info, dst : absT_info)) src_absT = + let + val src_repT = mk_repT (#absT src) (#repT src) src_absT; + val dst_absT = mk_absT thy (#repT dst) (#absT dst) src_repT; + in + dst_absT + end + | absT_info_encodeT _ NONE T = T; + +fun absT_info_decodeT thy = absT_info_encodeT thy o Option.map swap; + +fun absT_info_encode thy fp (opt as SOME (src : absT_info, dst : absT_info)) t = + let + val co_alg_funT = case_fp fp domain_type range_type; + fun co_swap pair = case_fp fp I swap pair; + val mk_co_comp = curry (HOLogic.mk_comp o co_swap); + val mk_co_abs = case_fp fp mk_abs mk_rep; + val mk_co_rep = case_fp fp mk_rep mk_abs; + val co_abs = case_fp fp #abs #rep; + val co_rep = case_fp fp #rep #abs; + val src_absT = co_alg_funT (fastype_of t); + val dst_absT = absT_info_encodeT thy opt src_absT; + val co_src_abs = mk_co_abs src_absT (co_abs src); + val co_dst_rep = mk_co_rep dst_absT (co_rep dst); + in + mk_co_comp (mk_co_comp t co_src_abs) co_dst_rep + end + | absT_info_encode _ _ NONE t = t; + +fun absT_info_decode thy fp = absT_info_encode thy fp o Option.map swap; + +fun mk_xtor_un_fold_xtor_thms ctxt fp un_folds xtors xtor_un_fold_unique map_id0s + absT_info_opts = + let + val thy = Proof_Context.theory_of ctxt; + fun mk_goal un_fold = + let + val rhs = list_comb (un_fold, @{map 2} (absT_info_encode thy fp) absT_info_opts xtors); + val T = range_type (fastype_of rhs); + in + HOLogic.mk_eq (HOLogic.id_const T, rhs) + end; + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map mk_goal un_folds)); + fun mk_inverses NONE = [] + | mk_inverses (SOME (src, dst)) = + [#type_definition dst RS @{thm type_definition.Abs_inverse[OF _ UNIV_I]}, + #type_definition src RS @{thm type_definition.Rep_inverse}]; + val inverses = maps mk_inverses absT_info_opts; + in + Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} => + mk_xtor_un_fold_xtor_tac ctxt xtor_un_fold_unique map_id0s inverses) + |> split_conj_thm |> map mk_sym + end; fun derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) pre_bnfs xtors0 un_folds0 - xtor_un_fold_unique xtor_un_folds xtor_un_fold_transfers xtor_maps xtor_rels lthy = + xtor_un_fold_unique xtor_un_folds xtor_un_fold_transfers xtor_maps xtor_rels + absT_info_opts lthy = let + val thy = Proof_Context.theory_of lthy; fun co_swap pair = case_fp fp I swap pair; val mk_co_comp = curry (HOLogic.mk_comp o co_swap); fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); @@ -645,6 +693,7 @@ val co_proj1_const = case_fp fp fst_const (uncurry Inl_const o dest_sumT) o co_alg_funT; val co_proj2_const = case_fp fp snd_const (uncurry Inr_const o dest_sumT) o co_alg_funT; val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT); + val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp}; val n = length pre_bnfs; val live = live_of_bnf (hd pre_bnfs); @@ -677,7 +726,8 @@ val TFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Ts)) Dss pre_bnfs; - val xtors = @{map 3} (force_typ names_lthy oo mk_co_algT) TFTs Ts xtors0; + val TFTs' = @{map 2} (absT_info_decodeT thy) absT_info_opts TFTs; + val xtors = @{map 3} (force_typ names_lthy oo mk_co_algT) TFTs' Ts xtors0; val ids = map HOLogic.id_const As; val co_rec_Xs = @{map 2} mk_co_productT Ts Xs; @@ -693,12 +743,13 @@ val (((co_rec_ss, fs), xs), names_lthy) = names_lthy |> mk_Frees "s" co_rec_argTs ||>> mk_Frees "f" co_rec_resTs - ||>> mk_Frees "x" (case_fp fp TFTs Xs); + ||>> mk_Frees "x" (case_fp fp TFTs' Xs); val co_rec_strs = - @{map 3} (fn xtor => fn s => fn mapx => - mk_co_product (mk_co_comp xtor (list_comb (mapx, ids @ co_proj1s))) s) - xtors co_rec_ss co_rec_maps; + @{map 4} (fn xtor => fn s => fn mapx => fn absT_info_opt => + mk_co_product (mk_co_comp (absT_info_encode thy fp absT_info_opt xtor) + (list_comb (mapx, ids @ co_proj1s))) s) + xtors co_rec_ss co_rec_maps absT_info_opts; val theta = Xs ~~ co_rec_Xs; val co_rec_un_folds = map (subst_atomic_types theta) un_folds; @@ -730,7 +781,9 @@ val co_rec_defs = map (fn def => mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) co_rec_def_frees; - val xtor_un_fold_xtor_thms = mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique map_id0s; + val xtor_un_fold_xtor_thms = + mk_xtor_un_fold_xtor_thms lthy fp (map (Term.subst_atomic_types (Xs ~~ Ts)) un_folds) + xtors xtor_un_fold_unique map_id0s absT_info_opts; val co_rec_id_thms = let @@ -741,8 +794,8 @@ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms xtor_un_fold_unique xtor_un_folds map_comps) - |> Thm.close_derivation - |> split_conj_thm + |> Thm.close_derivation + |> split_conj_thm end; val co_rec_app_ss = map (fn co_rec => list_comb (co_rec, co_rec_ss)) co_recs; @@ -754,14 +807,16 @@ case_fp fp @{thm convol_expand_snd} @{thm case_sum_expand_Inr_pointfree}) co_rec_id_thms; val xtor_co_rec_thms = let - fun mk_goal co_rec s mapx xtor x = + fun mk_goal co_rec s mapx xtor x absT_info_opt = let val lhs = mk_co_app co_rec xtor x; - val rhs = mk_co_app s (list_comb (mapx, ids @ co_products)) x; + val rhs = mk_co_app s + (list_comb (mapx, ids @ co_products) |> absT_info_decode thy fp absT_info_opt) x; in mk_Trueprop_eq (lhs, rhs) end; - val goals = @{map 5} mk_goal co_rec_app_ss co_rec_ss co_rec_maps_rev xtors xs; + val goals = + @{map 6} mk_goal co_rec_app_ss co_rec_ss co_rec_maps_rev xtors xs absT_info_opts; in map2 (fn goal => fn un_fold => Variable.add_free_names lthy goal [] @@ -777,28 +832,38 @@ thm RS case_fp fp @{thm convol_expand_snd'} @{thm case_sum_expand_Inr'}) co_rec_id_thms; val xtor_co_rec_unique_thm = let - fun mk_prem f s mapx xtor = + fun mk_prem f s mapx xtor absT_info_opt = let val lhs = mk_co_comp f xtor; - val rhs = mk_co_comp s (list_comb (mapx, ids @ co_product_fs)); + val rhs = mk_co_comp s (list_comb (mapx, ids @ co_product_fs)) + |> absT_info_decode thy fp absT_info_opt; in mk_Trueprop_eq (co_swap (lhs, rhs)) end; - val prems = @{map 4} mk_prem fs co_rec_ss co_rec_maps_rev xtors; + val prems = @{map 5} mk_prem fs co_rec_ss co_rec_maps_rev xtors absT_info_opts; val concl = @{map 2} (curry HOLogic.mk_eq) fs co_rec_app_ss |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop; val goal = Logic.list_implies (prems, concl); val vars = Variable.add_free_names lthy goal []; + fun mk_inverses NONE = [] + | mk_inverses (SOME (src, dst)) = + [#type_definition dst RS @{thm type_copy_Rep_o_Abs} RS rewrite_comp_comp, + #type_definition src RS @{thm type_copy_Abs_o_Rep}]; + val inverses = maps mk_inverses absT_info_opts; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs - co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s) + co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s inverses) |> Thm.close_derivation end; - val xtor_co_rec_o_map_thms = mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm - (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms) - sym_map_comp0s map_cong0s; + val xtor_co_rec_o_map_thms = if forall is_none absT_info_opts + then + mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm + (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms) + sym_map_comp0s map_cong0s + else + replicate n refl (* FIXME *); val ABphiTs = @{map 2} mk_pred2T As Bs; val XYphiTs = @{map 2} mk_pred2T Xs Ys; @@ -807,24 +872,29 @@ |> mk_Frees "R" ABphiTs ||>> mk_Frees "S" XYphiTs; - val pre_rels = - @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ co_rec_Xs) (Bs @ co_rec_Ys)) Dss pre_bnfs; - val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop - #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb) - #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of - #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T')) - Ts Us xtor_un_fold_transfers; - - fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs - xtor_un_fold_transfers map_transfers xtor_rels; - - val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum; - val rec_phis = - map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis; - - val xtor_co_rec_transfer_thms = - mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis - co_recs (map (subst_atomic_types (ABs @ XYs)) co_recs) tac lthy; + val xtor_co_rec_transfer_thms = if forall is_none absT_info_opts + then + let + val pre_rels = + @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ co_rec_Xs) (Bs @ co_rec_Ys)) Dss pre_bnfs; + val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop + #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb) + #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of + #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T')) + Ts Us xtor_un_fold_transfers; + + fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs + xtor_un_fold_transfers map_transfers xtor_rels; + + val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum; + val rec_phis = + map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis; + in + mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis + co_recs (map (subst_atomic_types (ABs @ XYs)) co_recs) tac lthy + end + else + replicate n TrueI (* FIXME *); val notes = [(case_fp fp ctor_recN dtor_corecN, xtor_co_rec_thms), diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Tools/BNF/bnf_fp_util_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML Thu Apr 14 20:29:42 2016 +0200 @@ -8,6 +8,7 @@ signature BNF_FP_UTIL_TACTICS = sig +val mk_xtor_un_fold_xtor_tac: Proof.context -> thm -> thm list -> thm list -> tactic val mk_xtor_co_rec_id_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> tactic val mk_xtor_co_rec_tac: Proof.context -> thm -> thm list -> thm list -> tactic val mk_xtor_co_rec_unique_tac: Proof.context -> BNF_Util.fp_kind -> thm list -> thm list -> thm -> @@ -23,22 +24,32 @@ open BNF_Tactics open BNF_Util +fun mk_xtor_un_fold_xtor_tac ctxt xtor_un_fold_unique map_id0s inverses = + HEADGOAL (rtac ctxt xtor_un_fold_unique THEN_ALL_NEW rtac ctxt ext) THEN + unfold_thms_tac ctxt (@{thms o_apply id_o o_id} @ map_id0s @ inverses) THEN + ALLGOALS (rtac ctxt refl); + +fun mk_conj_arg_congN 1 = @{thm DEADID.rel_mono_strong} + | mk_conj_arg_congN n = mk_conj_arg_congN (n - 1) RSN (2, @{thm arg_cong2[of _ _ _ _ "op \"]}); + fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps = - unfold_thms_tac ctxt (map mk_sym xtor_un_fold_xtors) THEN - HEADGOAL (rtac ctxt xtor_un_fold_unique THEN_ALL_NEW EVERY' [rtac ctxt ext, - SELECT_GOAL (unfold_thms_tac ctxt - (o_apply :: @{thms fst_convol' id_o sum.case} @ map_comps @ xtor_un_folds)), - rtac ctxt refl]); + HEADGOAL (rtac ctxt (mk_conj_arg_congN (length xtor_un_fold_xtors) RS iffD1 OF + (map (fn thm => @{thm DEADID.rel_cong} OF [refl, thm]) xtor_un_fold_xtors)) THEN' + rtac ctxt xtor_un_fold_unique THEN_ALL_NEW EVERY' [rtac ctxt ext, + SELECT_GOAL (unfold_thms_tac ctxt + (o_apply :: @{thms fst_convol' id_o sum.case} @ map_comps @ xtor_un_folds)), + rtac ctxt refl]); fun mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms = unfold_thms_tac ctxt (un_fold :: @{thms o_apply sum.case snd_convol' case_sum_o_inj(2)} @ co_rec_defs @ co_rec_expand_thms) THEN HEADGOAL (rtac ctxt refl); -fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps = +fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps + inverses = unfold_thms_tac ctxt (co_rec_defs @ co_rec_expand's) THEN HEADGOAL (EVERY' [rtac ctxt un_fold_unique]) THEN - unfold_thms_tac ctxt (map_ids @ map_comps @ case_fp fp + unfold_thms_tac ctxt (map_ids @ map_comps @ inverses @ case_fp fp @{thms id_o o_id convol_o fst_convol o_assoc[symmetric]} @{thms id_o o_id o_case_sum case_sum_o_inj(1) o_assoc}) THEN ALLGOALS (etac ctxt (case_fp fp diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 14 20:29:42 2016 +0200 @@ -2585,7 +2585,7 @@ |> derive_xtor_co_recs Greatest_FP external_bs mk_Ts (Dss, resDs) bnfs (export dtors) (export unfolds) dtor_unfold_unique_thm dtor_unfold_thms dtor_unfold_transfer_thms - dtor_Jmap_thms dtor_Jrel_thms; + dtor_Jmap_thms dtor_Jrel_thms (replicate n NONE); val timer = time (timer "recursor"); diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 14 20:29:42 2016 +0200 @@ -1847,7 +1847,8 @@ lthy) = lthy |> derive_xtor_co_recs Least_FP external_bs mk_Ts (Dss, resDs) bnfs (export ctors) (export folds) - ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms; + ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms + (replicate n NONE); val timer = time (timer "recursor"); diff -r 1ba3aacfa4d3 -r c50c764aab10 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Apr 22 15:34:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Apr 14 20:29:42 2016 +0200 @@ -28,7 +28,8 @@ |> morph_ctr_sugar (Morphism.typ_morphism "BNF" Logic.unvarifyT_global $> Morphism.term_morphism "BNF" (Term.map_types Logic.unvarifyT_global)); -fun trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct = +fun trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map + xtor_rel_induct ctor_rec_transfer = let val xtors = [Const (@{const_name xtor}, fpT --> fpT)]; val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))]; @@ -44,7 +45,8 @@ xtor_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms, xtor_un_fold_unique = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm, xtor_un_fold_o_maps = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map], - xtor_un_fold_transfers = [], xtor_co_rec_transfers = [], + xtor_un_fold_transfers = [ctor_rec_transfer], + xtor_co_rec_transfers = [ctor_rec_transfer], xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []} end; @@ -62,6 +64,7 @@ val xtor_rel = @{thm xtor_rel[of "rel_sum R1 R2" for R1 R2]}; val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_sum g1 g2" for g1 g2]}; val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_sum R1 R2" for R1 R2]}; + val ctor_rec_transfer = @{thm ctor_rec_transfer[of "rel_sum R1 R2" for R1 R2]}; in {T = fpT, BT = fpBT, @@ -69,7 +72,8 @@ fp = Least_FP, fp_res_index = 0, fp_res = - trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct, + trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct + ctor_rec_transfer, pre_bnf = ID_bnf (*wrong*), fp_bnf = fp_bnf, absT_info = trivial_absT_info_of fpT, @@ -132,6 +136,7 @@ val xtor_rel = @{thm xtor_rel[of "rel_prod R1 R2" for R1 R2]}; val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_prod g1 g2" for g1 g2]}; val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_prod R1 R2" for R1 R2]}; + val ctor_rec_transfer = @{thm ctor_rec_transfer[of "rel_prod R1 R2" for R1 R2]}; in {T = fpT, BT = fpBT, @@ -139,7 +144,8 @@ fp = Least_FP, fp_res_index = 0, fp_res = - trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct, + trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct + ctor_rec_transfer, pre_bnf = ID_bnf (*wrong*), fp_bnf = fp_bnf, absT_info = trivial_absT_info_of fpT,