equal
deleted
inserted
replaced
72 val fp_bnfs = of_fp_res #bnfs; |
72 val fp_bnfs = of_fp_res #bnfs; |
73 val pre_bnfs = map #pre_bnf fp_sugars; |
73 val pre_bnfs = map #pre_bnf fp_sugars; |
74 val nesting_bnfss = |
74 val nesting_bnfss = |
75 map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars; |
75 map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars; |
76 val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss; |
76 val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss; |
77 val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss); |
77 val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (flat fp_or_nesting_bnfss); |
78 |
78 |
79 val fp_absTs = map #absT fp_absT_infos; |
79 val fp_absTs = map #absT fp_absT_infos; |
80 val fp_repTs = map #repT fp_absT_infos; |
80 val fp_repTs = map #repT fp_absT_infos; |
81 val fp_abss = map #abs fp_absT_infos; |
81 val fp_abss = map #abs fp_absT_infos; |
82 val fp_reps = map #rep fp_absT_infos; |
82 val fp_reps = map #rep fp_absT_infos; |
137 ||>> mk_Frees "y" yTs; |
137 ||>> mk_Frees "y" yTs; |
138 |
138 |
139 val rels = |
139 val rels = |
140 let |
140 let |
141 fun find_rel T As Bs = fp_or_nesting_bnfss |
141 fun find_rel T As Bs = fp_or_nesting_bnfss |
142 |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf)) |
142 |> map (filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf)) |
143 |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))) |
143 |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))) |
144 |> Option.map (fn bnf => |
144 |> Option.map (fn bnf => |
145 let val live = live_of_bnf bnf; |
145 let val live = live_of_bnf bnf; |
146 in (mk_rel live As Bs (rel_of_bnf bnf), live) end) |
146 in (mk_rel live As Bs (rel_of_bnf bnf), live) end) |
147 |> the_default (HOLogic.eq_const T, 0); |
147 |> the_default (HOLogic.eq_const T, 0); |
189 let |
189 let |
190 val extract = |
190 val extract = |
191 case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb); |
191 case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb); |
192 val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts; |
192 val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts; |
193 val thetas = AList.group (op =) |
193 val thetas = AList.group (op =) |
194 (mutual_cliques ~~ map (pairself (certify lthy)) (raw_phis ~~ pre_phis)); |
194 (mutual_cliques ~~ map (apply2 (certify lthy)) (raw_phis ~~ pre_phis)); |
195 in |
195 in |
196 map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas) |
196 map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas) |
197 mutual_cliques rel_xtor_co_inducts |
197 mutual_cliques rel_xtor_co_inducts |
198 end |
198 end |
199 |
199 |
284 |
284 |
285 val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs); |
285 val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs); |
286 |
286 |
287 val fold_pre_deads_only_Ts = |
287 val fold_pre_deads_only_Ts = |
288 map (typ_subst_nonatomic_sorted (map (rpair dummyT) |
288 map (typ_subst_nonatomic_sorted (map (rpair dummyT) |
289 (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs'; |
289 (As @ sort (int_ord o apply2 Term.size_of_typ) fpTs))) fold_preTs'; |
290 |
290 |
291 val (mutual_clique, TUs) = |
291 val (mutual_clique, TUs) = |
292 map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec))) |
292 map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec))) |
293 |>> map subst |
293 |>> map subst |
294 |> `(fn (_, Ys) => |
294 |> `(fn (_, Ys) => |
437 @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id}; |
437 @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id}; |
438 val rec_thms = fold_thms @ case_fp fp |
438 val rec_thms = fold_thms @ case_fp fp |
439 @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod} |
439 @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod} |
440 @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)}; |
440 @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)}; |
441 |
441 |
442 val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of; |
442 val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of; |
443 |
443 |
444 val map_thms = no_refl (maps (fn bnf => |
444 val map_thms = no_refl (maps (fn bnf => |
445 let val map_comp0 = map_comp0_of_bnf bnf RS sym |
445 let val map_comp0 = map_comp0_of_bnf bnf RS sym |
446 in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) |
446 in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) |
447 fp_or_nesting_bnfs) @ |
447 fp_or_nesting_bnfs) @ |