1(* Title: HOL/Tools/BNF/bnf_fp_n2m.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Copyright 2013 4 5Flattening of nested to mutual (co)recursion. 6*) 7 8signature BNF_FP_N2M = 9sig 10 val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list -> 11 (int * BNF_FP_Util.fp_result) list -> binding list -> (string * sort) list -> 12 typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 13 BNF_FP_Util.fp_result * local_theory 14end; 15 16structure BNF_FP_N2M : BNF_FP_N2M = 17struct 18 19open BNF_Def 20open BNF_Util 21open BNF_Comp 22open BNF_FP_Util 23open BNF_FP_Def_Sugar 24open BNF_Tactics 25open BNF_FP_N2M_Tactics 26 27fun mk_arg_cong ctxt n t = 28 let 29 val Us = fastype_of t |> strip_typeN n |> fst; 30 val ((xs, ys), _) = ctxt 31 |> mk_Frees "x" Us 32 ||>> mk_Frees "y" Us; 33 val goal = Logic.list_implies (@{map 2} (curry mk_Trueprop_eq) xs ys, 34 mk_Trueprop_eq (list_comb (t, xs), list_comb (t, ys))); 35 val vars = Variable.add_free_names ctxt goal []; 36 in 37 Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => 38 HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl)) 39 |> Thm.close_derivation \<^here> 40 end; 41 42val cacheN = "cache" 43fun mk_cacheN i = cacheN ^ string_of_int i ^ "_"; 44val cache_threshold = Attrib.setup_config_int \<^binding>\<open>bnf_n2m_cache_threshold\<close> (K 200); 45type cache = int * (term * thm) Typtab.table 46val empty_cache = (0, Typtab.empty) 47fun update_cache b0 TU t (cache as (i, tab), lthy) = 48 if size_of_term t < Config.get lthy cache_threshold then (t, (cache, lthy)) 49 else 50 let 51 val b = Binding.prefix_name (mk_cacheN i) b0; 52 val ((c, thm), lthy') = 53 Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), t)) lthy 54 |>> apsnd snd; 55 in 56 (c, ((i + 1, Typtab.update (TU, (c, thm)) tab), lthy')) 57 end; 58 59fun lookup_cache (SOME _) _ _ = NONE 60 | lookup_cache NONE TU ((_, tab), _) = Typtab.lookup tab TU |> Option.map fst; 61 62fun construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress bs resBs (resDs, Dss) bnfs 63 (absT_infos : absT_info list) lthy = 64 let 65 val time = time lthy; 66 val timer = time (Timer.startRealTimer ()); 67 68 val b_names = map Binding.name_of bs; 69 val b_name = mk_common_name b_names; 70 val b = Binding.name b_name; 71 72 fun of_fp_res get = map (uncurry nth o swap o apsnd get) indexed_fp_ress; 73 fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); 74 fun co_swap pair = case_fp fp I swap pair; 75 val mk_co_comp = curry (HOLogic.mk_comp o co_swap); 76 77 val dest_co_algT = co_swap o dest_funT; 78 val co_alg_argT = case_fp fp range_type domain_type; 79 val co_alg_funT = case_fp fp domain_type range_type; 80 val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp}; 81 82 val fp_absT_infos = of_fp_res #absT_infos; 83 val fp_bnfs = of_fp_res #bnfs; 84 val fp_pre_bnfs = of_fp_res #pre_bnfs; 85 86 val fp_absTs = map #absT fp_absT_infos; 87 val fp_repTs = map #repT fp_absT_infos; 88 val fp_abss = map #abs fp_absT_infos; 89 val fp_reps = map #rep fp_absT_infos; 90 val fp_type_definitions = map #type_definition fp_absT_infos; 91 92 val absTs = map #absT absT_infos; 93 val repTs = map #repT absT_infos; 94 val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs; 95 val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs; 96 val abss = map #abs absT_infos; 97 val reps = map #rep absT_infos; 98 val abs_inverses = map #abs_inverse absT_infos; 99 val type_definitions = map #type_definition absT_infos; 100 101 val n = length bnfs; 102 val deads = fold (union (op =)) Dss resDs; 103 val As = subtract (op =) deads (map TFree resBs); 104 val names_lthy = fold Variable.declare_typ (As @ deads) lthy; 105 val m = length As; 106 val live = m + n; 107 108 val (((Xs, Ys), Bs), names_lthy) = names_lthy 109 |> mk_TFrees n 110 ||>> mk_TFrees n 111 ||>> mk_TFrees m; 112 113 val allAs = As @ Xs; 114 val allBs = Bs @ Xs; 115 val phiTs = map2 mk_pred2T As Bs; 116 val thetaBs = As ~~ Bs; 117 val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs; 118 val fold_thetaAs = Xs ~~ fpTs; 119 val fold_thetaBs = Xs ~~ fpTs'; 120 val pre_phiTs = map2 mk_pred2T fpTs fpTs'; 121 122 val ((ctors, dtors), (xtor's, xtors)) = 123 let 124 val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors); 125 val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors); 126 in 127 ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors)) 128 end; 129 130 val absATs = map (domain_type o fastype_of) ctors; 131 val absBTs = map (Term.typ_subst_atomic thetaBs) absATs; 132 val xTs = map (domain_type o fastype_of) xtors; 133 val yTs = map (domain_type o fastype_of) xtor's; 134 135 val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss; 136 val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss; 137 val fp_repAs = map2 mk_rep absATs fp_reps; 138 val fp_repBs = map2 mk_rep absBTs fp_reps; 139 140 val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single); 141 val sorted_theta = sort (int_ord o apply2 (Term.size_of_typ o fst)) (fpTs ~~ Xs) 142 val sorted_fpTs = map fst sorted_theta; 143 144 val nesting_bnfs = nesting_bnfs lthy 145 [[map (typ_subst_nonatomic_sorted (rev sorted_theta) o range_type o fastype_of) fp_repAs]] 146 allAs; 147 val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (fp_bnfs @ nesting_bnfs); 148 149 val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy 150 |> mk_Frees' "R" phiTs 151 ||>> mk_Frees "S" pre_phiTs 152 ||>> mk_Frees "x" xTs 153 ||>> mk_Frees "y" yTs; 154 155 val rels = 156 let 157 fun find_rel T As Bs = fp_or_nesting_bnfs 158 |> filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf) 159 |> find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)) 160 |> Option.map (fn bnf => 161 let val live = live_of_bnf bnf; 162 in (mk_rel live As Bs (rel_of_bnf bnf), live) end) 163 |> the_default (HOLogic.eq_const T, 0); 164 165 fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) = 166 let 167 val (rel, live) = find_rel T Ts Us; 168 val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T; 169 val rels = map2 mk_rel Ts' Us'; 170 in 171 Term.list_comb (rel, rels) 172 end 173 | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As) 174 handle General.Subscript => HOLogic.eq_const T) 175 | mk_rel _ _ = raise Fail "fpTs contains schematic type variables"; 176 in 177 map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs' 178 end; 179 180 val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs; 181 182 val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) fp_pre_bnfs; 183 val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct) 184 |> map (zero_var_indexes o unfold_thms lthy (id_apply :: rel_unfolds)); 185 186 val rel_defs = map rel_def_of_bnf bnfs; 187 val rel_monos = map rel_mono_of_bnf bnfs; 188 189 fun cast castA castB pre_rel = 190 let 191 val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA) 192 (Term.subst_atomic_types fold_thetaBs castB); 193 in 194 fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs] 195 (castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0))) 196 end; 197 198 val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs; 199 val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs; 200 201 val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs); 202 val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs; 203 204 fun mutual_instantiate ctxt inst = 205 let 206 val thetas = AList.group (op =) (mutual_cliques ~~ inst); 207 in 208 map2 (infer_instantiate ctxt o the o AList.lookup (op =) thetas) mutual_cliques 209 end; 210 211 val rel_xtor_co_inducts_inst = 212 let 213 val extract = 214 case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb); 215 val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts; 216 val inst = map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis); 217 in 218 mutual_instantiate lthy inst rel_xtor_co_inducts 219 end 220 221 val xtor_rel_co_induct = 222 mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys 223 xtors xtor's (mk_rel_xtor_co_induct_tac fp abs_inverses rel_xtor_co_inducts_inst rel_defs 224 rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos) 225 lthy; 226 227 val map_id0s = no_refl (map map_id0_of_bnf bnfs); 228 229 val xtor_co_induct_thm = 230 (case fp of 231 Least_FP => 232 let 233 val (Ps, names_lthy) = names_lthy 234 |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs); 235 fun mk_Grp_id P = 236 let val T = domain_type (fastype_of P); 237 in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end; 238 val cts = 239 map (SOME o Thm.cterm_of names_lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps); 240 fun mk_fp_type_copy_thms thm = map (curry op RS thm) 241 @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep}; 242 fun mk_type_copy_thms thm = map (curry op RS thm) 243 @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs}; 244 in 245 infer_instantiate' names_lthy cts xtor_rel_co_induct 246 |> singleton (Proof_Context.export names_lthy lthy) 247 |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ 248 fp_or_nesting_rel_eqs) 249 |> funpow n (fn thm => thm RS spec) 250 |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s) 251 |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id 252 Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @ 253 maps mk_fp_type_copy_thms fp_type_definitions @ 254 maps mk_type_copy_thms type_definitions) 255 |> unfold_thms lthy @{thms subset_iff mem_Collect_eq 256 atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]} 257 end 258 | Greatest_FP => 259 let 260 val cts = NONE :: map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As); 261 in 262 infer_instantiate' lthy cts xtor_rel_co_induct 263 |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ 264 fp_or_nesting_rel_eqs) 265 |> funpow (2 * n) (fn thm => thm RS spec) 266 |> Conv.fconv_rule (Object_Logic.atomize lthy) 267 |> funpow n (fn thm => thm RS mp) 268 end); 269 270 val timer = time (timer "Nested-to-mutual (co)induction"); 271 272 val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs; 273 274 val fold_strTs = map2 mk_co_algT fold_preTs Xs; 275 val resTs = map2 mk_co_algT fpTs Xs; 276 277 val fp_un_folds = of_fp_res #xtor_un_folds; 278 val ns = map (length o #Ts o snd) indexed_fp_ress; 279 280 fun force_fold i TU raw_un_fold = 281 let 282 val thy = Proof_Context.theory_of lthy; 283 284 val approx_un_fold = raw_un_fold 285 |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU); 286 val subst = Term.typ_subst_atomic fold_thetaAs; 287 288 fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT; 289 val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs; 290 291 val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs); 292 293 val fold_pre_deads_only_Ts = 294 map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ sorted_fpTs))) fold_preTs'; 295 296 val (mutual_clique, TUs) = 297 map_split dest_co_algT (binder_fun_types (fastype_of approx_un_fold)) 298 |>> map subst 299 |> `(fn (_, Ys) => nth mutual_cliques 300 (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs)) 301 ||> uncurry (map2 mk_co_algT); 302 val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs; 303 val js = find_indices (fn ((cl, cand), TU) => 304 cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands; 305 val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js; 306 in 307 force_typ names_lthy (Tpats ---> TU) raw_un_fold 308 end; 309 310 fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t = 311 case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep)) 312 (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t))); 313 314 val thy = Proof_Context.theory_of lthy; 315 fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT; 316 317 fun mk_un_fold b_opt ss un_folds cache_lthy TU = 318 (case lookup_cache b_opt TU cache_lthy of 319 SOME t => ((t, Drule.dummy_thm), cache_lthy) 320 | NONE => 321 let 322 val x = co_alg_argT TU; 323 val i = find_index (fn T => x = T) Xs; 324 val TUfold = 325 (case find_first (fn f => body_fun_type (fastype_of f) = TU) un_folds of 326 NONE => force_fold i TU (nth fp_un_folds i) 327 | SOME f => f); 328 329 val TUs = binder_fun_types (fastype_of TUfold); 330 331 fun mk_s TU' cache_lthy = 332 let 333 val i = find_index (fn T => co_alg_argT TU' = T) Xs; 334 val fp_abs = nth fp_abss i; 335 val fp_rep = nth fp_reps i; 336 val abs = nth abss i; 337 val rep = nth reps i; 338 val sF = co_alg_funT TU'; 339 val sF' = 340 mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF 341 handle Term.TYPE _ => sF; 342 val F = nth fold_preTs i; 343 val s = nth ss i; 344 in 345 if sF = F then (s, cache_lthy) 346 else if sF' = F then (mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s, cache_lthy) 347 else 348 let 349 val smapT = replicate live dummyT ---> mk_co_algT sF' F; 350 fun hidden_to_unit t = 351 Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t; 352 val smap = map_of_bnf (nth bnfs i) 353 |> force_typ names_lthy smapT 354 |> hidden_to_unit; 355 val smap_argTs = strip_typeN live (fastype_of smap) |> fst; 356 fun mk_smap_arg T_to_U cache_lthy = 357 (if domain_type T_to_U = range_type T_to_U then 358 (HOLogic.id_const (domain_type T_to_U), cache_lthy) 359 else 360 mk_un_fold NONE ss un_folds cache_lthy T_to_U |>> fst); 361 val (smap_args, cache_lthy') = fold_map mk_smap_arg smap_argTs cache_lthy; 362 in 363 (mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep 364 (mk_co_comp s (Term.list_comb (smap, smap_args))), cache_lthy') 365 end 366 end; 367 val (args, cache_lthy) = fold_map mk_s TUs cache_lthy; 368 val t = Term.list_comb (TUfold, args); 369 in 370 (case b_opt of 371 NONE => update_cache b TU t cache_lthy |>> rpair Drule.dummy_thm 372 | SOME b => cache_lthy 373 |-> (fn cache => 374 let 375 val S = HOLogic.mk_tupleT fold_strTs; 376 val s = HOLogic.mk_tuple ss; 377 val u = Const (\<^const_name>\<open>Let\<close>, S --> (S --> TU) --> TU) $ s $ absdummy S t; 378 in 379 Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), u)) 380 #>> apsnd snd ##> pair cache 381 end)) 382 end); 383 384 val un_foldN = case_fp fp ctor_foldN dtor_unfoldN; 385 fun mk_un_folds (ss_names, lthy) = 386 let val ss = map2 (curry Free) ss_names fold_strTs; 387 in 388 fold2 (fn TU => fn b => fn ((un_folds, defs), cache_lthy) => 389 mk_un_fold (SOME b) (map2 (curry Free) ss_names fold_strTs) un_folds cache_lthy TU 390 |>> (fn (f, d) => (f :: un_folds, d :: defs))) 391 resTs (map (Binding.suffix_name ("_" ^ un_foldN)) bs) (([], []), (empty_cache, lthy)) 392 |>> map_prod rev rev 393 |>> pair ss 394 end; 395 val ((ss, (un_folds, un_fold_defs0)), (cache, (lthy, raw_lthy))) = lthy 396 |> Local_Theory.open_target |> snd 397 |> Variable.add_fixes (mk_names n "s") 398 |> mk_un_folds 399 ||> apsnd (`(Local_Theory.close_target)); 400 401 val un_fold_defs = map (unfold_thms raw_lthy @{thms Let_const}) un_fold_defs0; 402 403 val cache_defs = snd cache |> Typtab.dest |> map (snd o snd); 404 405 val phi = Proof_Context.export_morphism raw_lthy lthy; 406 407 val xtor_un_folds = map (head_of o Morphism.term phi) un_folds; 408 val xtor_un_fold_defs = map (Drule.abs_def o Morphism.thm phi) un_fold_defs; 409 val xtor_cache_defs = map (Drule.abs_def o Morphism.thm phi) cache_defs; 410 val xtor_un_folds' = map2 (fn raw => fn t => 411 Const (fst (dest_Const t), fold_strTs ---> fastype_of raw)) 412 un_folds xtor_un_folds; 413 414 val fp_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps 415 |> maps (fn thm => [thm, thm RS rewrite_comp_comp]); 416 417 val fold_mapTs = co_swap (As @ fpTs, As @ Xs); 418 val pre_fold_maps = @{map 2} (fn Ds => uncurry (mk_map_of_bnf Ds) fold_mapTs) Dss bnfs 419 fun mk_pre_fold_maps fs = 420 map (fn mapx => Term.list_comb (mapx, map HOLogic.id_const As @ fs)) pre_fold_maps; 421 422 val pre_map_defs = no_refl (map map_def_of_bnf bnfs); 423 val fp_map_defs = no_refl (map map_def_of_bnf fp_pre_bnfs); 424 val map_defs = pre_map_defs @ fp_map_defs; 425 val pre_rel_defs = no_refl (map rel_def_of_bnf bnfs); 426 val fp_rel_defs = no_refl (map rel_def_of_bnf fp_pre_bnfs); 427 val rel_defs = pre_rel_defs @ fp_rel_defs; 428 fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs}) 429 |> (fn thm => [thm, thm RS rewrite_comp_comp]); 430 val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions; 431 val pre_Rep_o_Abss = maps mk_Rep_o_Abs type_definitions; 432 val Rep_o_Abss = fp_Rep_o_Abss @ pre_Rep_o_Abss; 433 434 val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs)); 435 val simp_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: 436 @{thms id_apply comp_id id_comp}; 437 438 val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of; 439 440 val map_thms = no_refl (maps (fn bnf => 441 let val map_comp0 = map_comp0_of_bnf bnf RS sym 442 in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) 443 fp_or_nesting_bnfs) @ 444 remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc}) 445 (map2 (fn thm => fn bnf => 446 @{thm type_copy_map_comp0_undo} OF 447 (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS 448 rewrite_comp_comp) 449 type_definitions bnfs); 450 451 val xtor_un_fold_thms = 452 let 453 val pre_fold_maps = mk_pre_fold_maps un_folds; 454 fun mk_goals f xtor s smap fp_abs fp_rep abs rep = 455 let 456 val lhs = mk_co_comp f xtor; 457 val rhs = mk_co_comp s smap; 458 in 459 HOLogic.mk_eq (lhs, 460 mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs)) 461 fp_abs fp_rep abs rep rhs) 462 end; 463 464 val goals = 465 @{map 8} mk_goals un_folds xtors ss pre_fold_maps fp_abss fp_reps abss reps; 466 467 val fp_un_folds = map (mk_pointfree2 lthy) (of_fp_res #xtor_un_fold_thms); 468 469 val simps = flat [simp_thms, un_fold_defs, map_defs, fp_un_folds, 470 fp_un_fold_o_maps, map_thms, Rep_o_Abss]; 471 in 472 Library.foldr1 HOLogic.mk_conj goals 473 |> HOLogic.mk_Trueprop 474 |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal 475 (fn {context = ctxt, prems = _} => mk_xtor_un_fold_tac ctxt n simps cache_defs)) 476 |> Thm.close_derivation \<^here> 477 |> Morphism.thm phi 478 |> split_conj_thm 479 |> map (fn thm => thm RS @{thm comp_eq_dest}) 480 end; 481 482 val xtor_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps 483 |> maps (fn thm => [thm, thm RS rewrite_comp_comp]); 484 val xtor_un_fold_unique_thm = 485 let 486 val (fs, _) = names_lthy |> mk_Frees "f" resTs; 487 val fold_maps = mk_pre_fold_maps fs; 488 fun mk_prem f s mapx xtor fp_abs fp_rep abs rep = 489 let 490 val lhs = mk_co_comp f xtor; 491 val rhs = mk_co_comp s mapx; 492 in 493 mk_Trueprop_eq (lhs, 494 mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs)) 495 fp_abs fp_rep abs rep rhs) 496 end; 497 val prems = @{map 8} mk_prem fs ss fold_maps xtors fp_abss fp_reps abss reps; 498 val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 499 (map2 (curry HOLogic.mk_eq) fs un_folds)); 500 val vars = Variable.add_free_names raw_lthy concl []; 501 val fp_un_fold_uniques0 = of_fp_res (split_conj_thm o #xtor_un_fold_unique) 502 |> map (Drule.zero_var_indexes o unfold_thms lthy fp_map_defs); 503 val names = fp_un_fold_uniques0 504 |> map (Thm.concl_of #> HOLogic.dest_Trueprop 505 #> HOLogic.dest_eq #> fst #> dest_Var #> fst); 506 val inst = names ~~ map (Thm.cterm_of lthy) fs; 507 val fp_un_fold_uniques = mutual_instantiate lthy inst fp_un_fold_uniques0; 508 val map_arg_congs = 509 map (fn bnf => mk_arg_cong lthy (live_of_bnf bnf) (map_of_bnf bnf) 510 |> unfold_thms lthy (pre_map_defs @ simp_thms)) nesting_bnfs; 511 in 512 Goal.prove_sorry raw_lthy vars prems concl 513 (mk_xtor_un_fold_unique_tac fp un_fold_defs map_arg_congs xtor_un_fold_o_maps 514 Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs) 515 |> Thm.close_derivation \<^here> 516 |> case_fp fp I (fn thm => thm OF replicate n sym) 517 |> Morphism.thm phi 518 end; 519 520 val ABs = As ~~ Bs; 521 val XYs = Xs ~~ Ys; 522 val ABphiTs = @{map 2} mk_pred2T As Bs; 523 val XYphiTs = @{map 2} mk_pred2T Xs Ys; 524 525 val ((ABphis, XYphis), _) = names_lthy 526 |> mk_Frees "R" ABphiTs 527 ||>> mk_Frees "S" XYphiTs; 528 529 val pre_rels = @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ Xs) (Bs @ Ys)) Dss bnfs; 530 531 val ns = map (fn i => length (filter (fn c => i = c) mutual_cliques)) mutual_cliques; 532 533 val map_transfers = map (funpow live (fn thm => thm RS @{thm rel_funD}) 534 #> unfold_thms lthy pre_rel_defs) 535 (map map_transfer_of_bnf bnfs); 536 val fp_un_fold_transfers = map2 (fn n => funpow n (fn thm => thm RS @{thm rel_funD}) 537 #> unfold_thms lthy fp_rel_defs) 538 ns (of_fp_res #xtor_un_fold_transfers); 539 val pre_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions; 540 val fp_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) fp_type_definitions; 541 val Abs_transfers = pre_Abs_transfers @ fp_Abs_transfers; 542 543 fun tac {context = ctxt, prems = _} = 544 mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers 545 map_transfers Abs_transfers fp_or_nesting_rel_eqs xtor_cache_defs; 546 547 val xtor_un_fold_transfer_thms = 548 mk_xtor_co_iter_transfer_thms fp pre_rels XYphis XYphis rels ABphis 549 xtor_un_folds' (map (subst_atomic_types (ABs @ XYs)) xtor_un_folds') tac lthy; 550 551 val timer = time (timer "Nested-to-mutual (co)iteration"); 552 553 val xtor_maps = of_fp_res #xtor_maps; 554 val xtor_rels = of_fp_res #xtor_rels; 555 fun mk_Ts Cs = map (typ_subst_atomic (As ~~ Cs)) fpTs; 556 val phi = Local_Theory.target_morphism lthy; 557 val export = map (Morphism.term phi); 558 val ((xtor_co_recs, (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, 559 xtor_co_rec_transfer_thms)), lthy) = lthy 560 |> derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) bnfs 561 (export xtors) (export xtor_un_folds) 562 xtor_un_fold_unique_thm xtor_un_fold_thms xtor_un_fold_transfer_thms xtor_maps xtor_rels 563 (@{map 2} (curry (SOME o @{apply 2} (morph_absT_info phi))) fp_absT_infos absT_infos); 564 565 val timer = time (timer "Nested-to-mutual (co)recursion"); 566 567 val common_notes = 568 (case fp of 569 Least_FP => 570 [(ctor_inductN, [xtor_co_induct_thm]), 571 (ctor_rel_inductN, [xtor_rel_co_induct])] 572 | Greatest_FP => 573 [(dtor_coinductN, [xtor_co_induct_thm]), 574 (dtor_rel_coinductN, [xtor_rel_co_induct])]) 575 |> map (fn (thmN, thms) => 576 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); 577 578 val notes = 579 (case fp of 580 Least_FP => [(ctor_foldN, xtor_un_fold_thms)] 581 | Greatest_FP => [(dtor_unfoldN, xtor_un_fold_thms)]) 582 |> map (apsnd (map single)) 583 |> maps (fn (thmN, thmss) => 584 map2 (fn b => fn thms => 585 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) 586 bs thmss); 587 588 val lthy = lthy |> Config.get lthy bnf_internals 589 ? snd o Local_Theory.notes (common_notes @ notes); 590 591 (* These results are half broken. This is deliberate. We care only about those fields that are 592 used by "primrec", "primcorecursive", and "datatype_compat". *) 593 val fp_res = 594 ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos, 595 dtors = dtors, ctors = ctors, 596 xtor_un_folds = xtor_un_folds, xtor_co_recs = xtor_co_recs, 597 xtor_co_induct = xtor_co_induct_thm, 598 dtor_ctors = of_fp_res #dtor_ctors (*too general types*), 599 ctor_dtors = of_fp_res #ctor_dtors (*too general types*), 600 ctor_injects = of_fp_res #ctor_injects (*too general types*), 601 dtor_injects = of_fp_res #dtor_injects (*too general types*), 602 xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), 603 xtor_map_unique = xtor_un_fold_unique_thm (*wrong*), 604 xtor_setss = of_fp_res #xtor_setss (*too general types and terms*), 605 xtor_rels = of_fp_res #xtor_rels (*too general types and terms*), 606 xtor_un_fold_thms = xtor_un_fold_thms, 607 xtor_co_rec_thms = xtor_co_rec_thms, 608 xtor_un_fold_unique = xtor_un_fold_unique_thm, 609 xtor_co_rec_unique = xtor_co_rec_unique_thm, 610 xtor_un_fold_o_maps = fp_un_fold_o_maps (*wrong*), 611 xtor_co_rec_o_maps = xtor_co_rec_o_map_thms (*wrong*), 612 xtor_un_fold_transfers = xtor_un_fold_transfer_thms, 613 xtor_co_rec_transfers = xtor_co_rec_transfer_thms (*wrong*), 614 xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []} 615 |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); 616 in 617 timer; (fp_res, lthy) 618 end; 619 620end; 621