--- 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 \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> 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 \<longleftrightarrow> (\<exists>b. p = (a, b))"
by (cases p) auto
--- 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
--- 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;
--- 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),
--- 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 \<and>"]});
+
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
--- 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");
--- 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");
--- 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,