File ‹Tools/BNF/bnf_fp_n2m.ML›
signature BNF_FP_N2M =
sig
val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
(int * BNF_FP_Util.fp_result) list -> binding list -> (string * sort) list ->
typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
BNF_FP_Util.fp_result * local_theory
end;
structure BNF_FP_N2M : BNF_FP_N2M =
struct
open BNF_Def
open BNF_Util
open BNF_Comp
open BNF_FP_Util
open BNF_FP_Def_Sugar
open BNF_Tactics
open BNF_FP_N2M_Tactics
fun mk_arg_cong ctxt n t =
let
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
Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl))
|> Thm.close_derivation ⌂
end;
val cacheN = "cache"
fun mk_cacheN i = cacheN ^ string_of_int i ^ "_";
val cache_threshold = Attrib.setup_config_int \<^binding>‹bnf_n2m_cache_threshold› (K 200);
type cache = int * (term * thm) Typtab.table
val empty_cache = (0, Typtab.empty)
fun update_cache b0 TU t (cache as (i, tab), lthy) =
if size_of_term t < Config.get lthy cache_threshold then (t, (cache, lthy))
else
let
val b = Binding.prefix_name (mk_cacheN i) b0;
val ((c, thm), lthy') =
Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), t)) lthy
|>> apsnd snd;
in
(c, ((i + 1, Typtab.update (TU, (c, thm)) tab), lthy'))
end;
fun lookup_cache (SOME _) _ _ = NONE
| lookup_cache NONE TU ((_, tab), _) = Typtab.lookup tab TU |> Option.map fst;
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;
val timer = time (Timer.startRealTimer ());
val b_names = map Binding.name_of bs;
val b_name = mk_common_name b_names;
val b = Binding.name b_name;
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 = 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 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 fp_pre_bnfs = of_fp_res #pre_bnfs;
val fp_absTs = map #absT fp_absT_infos;
val fp_repTs = map #repT fp_absT_infos;
val fp_abss = map #abs fp_absT_infos;
val fp_reps = map #rep fp_absT_infos;
val fp_type_definitions = map #type_definition fp_absT_infos;
val absTs = map #absT absT_infos;
val repTs = map #repT absT_infos;
val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs;
val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs;
val abss = map #abs absT_infos;
val reps = map #rep absT_infos;
val abs_inverses = map #abs_inverse absT_infos;
val type_definitions = map #type_definition absT_infos;
val n = length bnfs;
val deads = fold (union (op =)) Dss resDs;
val As = subtract (op =) deads (map TFree resBs);
val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
val m = length As;
val live = m + n;
val (((Xs, Ys), Bs), names_lthy) = names_lthy
|> mk_TFrees n
||>> mk_TFrees n
||>> mk_TFrees m;
val allAs = As @ Xs;
val allBs = Bs @ Xs;
val phiTs = map2 mk_pred2T As Bs;
val thetaBs = As ~~ Bs;
val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs;
val fold_thetaAs = Xs ~~ fpTs;
val fold_thetaBs = Xs ~~ fpTs';
val pre_phiTs = map2 mk_pred2T fpTs fpTs';
val ((ctors, dtors), (xtor's, xtors)) =
let
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)) (case_fp fp ctors dtors))
end;
val absATs = map (domain_type o fastype_of) ctors;
val absBTs = map (Term.typ_subst_atomic thetaBs) absATs;
val xTs = map (domain_type o fastype_of) xtors;
val yTs = map (domain_type o fastype_of) xtor's;
val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
val fp_repAs = map2 mk_rep absATs fp_reps;
val fp_repBs = map2 mk_rep absBTs fp_reps;
val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
val sorted_theta = sort (int_ord o apply2 (Term.size_of_typ o fst)) (fpTs ~~ Xs)
val sorted_fpTs = map fst sorted_theta;
val nesting_bnfs = nesting_bnfs lthy
[[map (typ_subst_nonatomic_sorted (rev sorted_theta) o range_type o fastype_of) fp_repAs]]
allAs;
val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (fp_bnfs @ nesting_bnfs);
val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
|> mk_Frees' "R" phiTs
||>> mk_Frees "S" pre_phiTs
||>> mk_Frees "x" xTs
||>> mk_Frees "y" yTs;
val rels =
let
fun find_rel T As Bs = fp_or_nesting_bnfs
|> filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf)
|> find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))
|> Option.map (fn bnf =>
let val live = live_of_bnf bnf;
in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
|> the_default (HOLogic.eq_const T, 0);
fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
let
val (rel, live) = find_rel T Ts Us;
val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
val rels = map2 mk_rel Ts' Us';
in
Term.list_comb (rel, rels)
end
| mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
handle General.Subscript => HOLogic.eq_const T)
| mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
in
map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
end;
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) 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));
val rel_defs = map rel_def_of_bnf bnfs;
val rel_monos = map rel_mono_of_bnf bnfs;
fun cast castA castB pre_rel =
let
val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA)
(Term.subst_atomic_types fold_thetaBs castB);
in
fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs]
(castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0)))
end;
val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
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 inst = map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis);
in
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_tac fp abs_inverses rel_xtor_co_inducts_inst rel_defs
rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
lthy;
val map_id0s = no_refl (map map_id0_of_bnf bnfs);
val xtor_co_induct_thm =
(case fp of
Least_FP =>
let
val (Ps, names_lthy) = names_lthy
|> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
fun mk_Grp_id P =
let val T = domain_type (fastype_of P);
in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
val cts =
map (SOME o Thm.cterm_of names_lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
fun mk_fp_type_copy_thms thm = map (curry op RS thm)
@{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
fun mk_type_copy_thms thm = map (curry op RS thm)
@{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
in
infer_instantiate' names_lthy cts xtor_rel_co_induct
|> singleton (Proof_Context.export names_lthy lthy)
|> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
fp_or_nesting_rel_eqs)
|> funpow n (fn thm => thm RS spec)
|> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
|> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
maps mk_fp_type_copy_thms fp_type_definitions @
maps mk_type_copy_thms type_definitions)
|> unfold_thms lthy @{thms subset_iff mem_Collect_eq
atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
end
| Greatest_FP =>
let
val cts = NONE :: map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As);
in
infer_instantiate' lthy cts xtor_rel_co_induct
|> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
fp_or_nesting_rel_eqs)
|> funpow (2 * n) (fn thm => thm RS spec)
|> Conv.fconv_rule (Object_Logic.atomize lthy)
|> funpow n (fn thm => thm RS mp)
end);
val timer = time (timer "Nested-to-mutual (co)induction");
val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
val fold_strTs = map2 mk_co_algT fold_preTs Xs;
val resTs = map2 mk_co_algT fpTs Xs;
val fp_un_folds = of_fp_res #xtor_un_folds;
val ns = map (length o #Ts o snd) indexed_fp_ress;
fun force_fold i TU raw_un_fold =
let
val thy = Proof_Context.theory_of lthy;
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;
fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
val fold_pre_deads_only_Ts =
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 (fastype_of approx_un_fold))
|>> map subst
|> `(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 = 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_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)));
val thy = Proof_Context.theory_of lthy;
fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT;
fun mk_un_fold b_opt ss un_folds cache_lthy TU =
(case lookup_cache b_opt TU cache_lthy of
SOME t => ((t, Drule.dummy_thm), cache_lthy)
| NONE =>
let
val x = co_alg_argT TU;
val i = find_index (fn T => x = T) Xs;
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 TUfold);
fun mk_s TU' cache_lthy =
let
val i = find_index (fn T => co_alg_argT TU' = T) Xs;
val fp_abs = nth fp_abss i;
val fp_rep = nth fp_reps i;
val abs = nth abss i;
val rep = nth reps i;
val sF = co_alg_funT TU';
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 fold_preTs i;
val s = nth ss i;
in
if sF = F then (s, cache_lthy)
else if sF' = F then (mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s, cache_lthy)
else
let
val smapT = replicate live dummyT ---> mk_co_algT sF' F;
fun hidden_to_unit t =
Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
val smap = map_of_bnf (nth bnfs i)
|> force_typ names_lthy smapT
|> hidden_to_unit;
val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
fun mk_smap_arg T_to_U cache_lthy =
(if domain_type T_to_U = range_type T_to_U then
(HOLogic.id_const (domain_type T_to_U), cache_lthy)
else
mk_un_fold NONE ss un_folds cache_lthy T_to_U |>> fst);
val (smap_args, cache_lthy') = fold_map mk_smap_arg smap_argTs cache_lthy;
in
(mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep
(mk_co_comp s (Term.list_comb (smap, smap_args))), cache_lthy')
end
end;
val (args, cache_lthy) = fold_map mk_s TUs cache_lthy;
val t = Term.list_comb (TUfold, args);
in
(case b_opt of
NONE => update_cache b TU t cache_lthy |>> rpair Drule.dummy_thm
| SOME b => cache_lthy
|-> (fn cache =>
let
val S = HOLogic.mk_tupleT fold_strTs;
val s = HOLogic.mk_tuple ss;
val u = Const (\<^const_name>‹Let›, S --> (S --> TU) --> TU) $ s $ absdummy S t;
in
Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), u))
#>> apsnd snd ##> pair cache
end))
end);
val un_foldN = case_fp fp ctor_foldN dtor_unfoldN;
fun mk_un_folds (ss_names, lthy) =
let val ss = map2 (curry Free) ss_names fold_strTs;
in
fold2 (fn TU => fn b => fn ((un_folds, defs), cache_lthy) =>
mk_un_fold (SOME b) (map2 (curry Free) ss_names fold_strTs) un_folds cache_lthy TU
|>> (fn (f, d) => (f :: un_folds, d :: defs)))
resTs (map (Binding.suffix_name ("_" ^ un_foldN)) bs) (([], []), (empty_cache, lthy))
|>> map_prod rev rev
|>> pair ss
end;
val ((ss, (un_folds, un_fold_defs0)), (cache, (lthy, raw_lthy))) = lthy
|> (snd o Local_Theory.begin_nested)
|> Variable.add_fixes (mk_names n "s")
|> mk_un_folds
||> apsnd (`(Local_Theory.end_nested));
val un_fold_defs = map (unfold_thms raw_lthy @{thms Let_const}) un_fold_defs0;
val cache_defs = snd cache |> Typtab.dest |> map (snd o snd);
val phi = Proof_Context.export_morphism raw_lthy lthy;
val xtor_un_folds = map (head_of o Morphism.term phi) un_folds;
val xtor_un_fold_defs = map (Drule.abs_def o Morphism.thm phi) un_fold_defs;
val xtor_cache_defs = map (Drule.abs_def o Morphism.thm phi) cache_defs;
val xtor_un_folds' = map2 (fn raw => fn t =>
Const (fst (dest_Const t), fold_strTs ---> fastype_of raw))
un_folds xtor_un_folds;
val fp_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps
|> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
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 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;
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 un_folds xtors ss pre_fold_maps fp_abss fp_reps abss reps;
val fp_un_folds = map (mk_pointfree2 lthy) (of_fp_res #xtor_un_fold_thms);
val simps = flat [simp_thms, 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
|> (fn goal => Goal.prove_sorry raw_lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_xtor_un_fold_tac ctxt n simps cache_defs))
|> 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 ss 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 un_fold_defs map_arg_congs xtor_un_fold_o_maps
Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_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 xtor_cache_defs;
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 =
(case fp of
Least_FP =>
[(ctor_inductN, [xtor_co_induct_thm]),
(ctor_rel_inductN, [xtor_rel_co_induct])]
| Greatest_FP =>
[(dtor_coinductN, [xtor_co_induct_thm]),
(dtor_rel_coinductN, [xtor_rel_co_induct])])
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val notes =
(case fp of
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 =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss);
val lthy = lthy |> Config.get lthy bnf_internals
? snd o Local_Theory.notes (common_notes @ notes);
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_un_folds, xtor_co_recs = xtor_co_recs,
xtor_co_induct = xtor_co_induct_thm,
dtor_ctors = of_fp_res #dtor_ctors ,
ctor_dtors = of_fp_res #ctor_dtors ,
ctor_injects = of_fp_res #ctor_injects ,
dtor_injects = of_fp_res #dtor_injects ,
xtor_maps = of_fp_res #xtor_maps ,
xtor_map_unique = xtor_un_fold_unique_thm ,
xtor_setss = of_fp_res #xtor_setss ,
xtor_rels = of_fp_res #xtor_rels ,
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 ,
xtor_co_rec_o_maps = xtor_co_rec_o_map_thms ,
xtor_un_fold_transfers = xtor_un_fold_transfer_thms,
xtor_co_rec_transfers = xtor_co_rec_transfer_thms ,
xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
timer; (fp_res, lthy)
end;
end;