19 co_induct: thm, |
19 co_induct: thm, |
20 strong_co_induct: thm, |
20 strong_co_induct: thm, |
21 un_fold_thmss: thm list list, |
21 un_fold_thmss: thm list list, |
22 co_rec_thmss: thm list list}; |
22 co_rec_thmss: thm list list}; |
23 |
23 |
24 val fp_sugar_of: local_theory -> string -> fp_sugar option |
24 val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar |
|
25 val fp_sugar_of: Proof.context -> string -> fp_sugar option |
25 |
26 |
26 val exists_subtype_in: typ list -> typ -> bool |
27 val exists_subtype_in: typ list -> typ -> bool |
27 val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c |
28 val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c |
28 val mk_fp_iter: bool -> typ list -> typ list -> term list -> term list * typ list |
29 val mk_fp_iter: bool -> typ list -> typ list -> term list -> term list * typ list |
29 val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term |
30 val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term |
1253 val spec = |
1254 val spec = |
1254 mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)), |
1255 mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)), |
1255 mk_iter_body no_defs_lthy fpTs ctor_iter fss xsss); |
1256 mk_iter_body no_defs_lthy fpTs ctor_iter fss xsss); |
1256 in (binding, spec) end; |
1257 in (binding, spec) end; |
1257 |
1258 |
1258 val iter_infos = [(foldN, fp_fold, fold_only), (recN, fp_rec, rec_only)]; |
1259 val binding_specs = |
1259 val (bindings, specs) = map generate_iter iter_infos |> split_list; |
1260 map generate_iter [(foldN, fp_fold, fold_only), (recN, fp_rec, rec_only)]; |
1260 |
1261 |
1261 val ((csts, defs), (lthy', lthy)) = no_defs_lthy |
1262 val ((csts, defs), (lthy', lthy)) = no_defs_lthy |
1262 |> apfst split_list o fold_map2 (fn b => fn spec => |
1263 |> apfst split_list o fold_map (fn (b, spec) => |
1263 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
1264 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
1264 #>> apsnd snd) bindings specs |
1265 #>> apsnd snd) binding_specs |
1265 ||> `Local_Theory.restore; |
1266 ||> `Local_Theory.restore; |
1266 |
1267 |
1267 val phi = Proof_Context.export_morphism lthy lthy'; |
1268 val phi = Proof_Context.export_morphism lthy lthy'; |
1268 |
1269 |
1269 val [fold_def, rec_def] = map (Morphism.thm phi) defs; |
1270 val [fold_def, rec_def] = map (Morphism.thm phi) defs; |
1284 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)), |
1285 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)), |
1285 mk_coiter_body no_defs_lthy cs ns cpss f_sum_prod_Ts f_Tsss cqssss cfssss |
1286 mk_coiter_body no_defs_lthy cs ns cpss f_sum_prod_Ts f_Tsss cqssss cfssss |
1286 dtor_coiter); |
1287 dtor_coiter); |
1287 in (binding, spec) end; |
1288 in (binding, spec) end; |
1288 |
1289 |
1289 val coiter_infos = [(unfoldN, fp_fold, unfold_only), (corecN, fp_rec, corec_only)]; |
1290 val binding_specs = |
1290 val (bindings, specs) = map generate_coiter coiter_infos |> split_list; |
1291 map generate_coiter [(unfoldN, fp_fold, unfold_only), (corecN, fp_rec, corec_only)]; |
1291 |
1292 |
1292 val ((csts, defs), (lthy', lthy)) = no_defs_lthy |
1293 val ((csts, defs), (lthy', lthy)) = no_defs_lthy |
1293 |> apfst split_list o fold_map2 (fn b => fn spec => |
1294 |> apfst split_list o fold_map (fn (b, spec) => |
1294 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
1295 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
1295 #>> apsnd snd) bindings specs |
1296 #>> apsnd snd) binding_specs |
1296 ||> `Local_Theory.restore; |
1297 ||> `Local_Theory.restore; |
1297 |
1298 |
1298 val phi = Proof_Context.export_morphism lthy lthy'; |
1299 val phi = Proof_Context.export_morphism lthy lthy'; |
1299 |
1300 |
1300 val [unfold_def, corec_def] = map (Morphism.thm phi) defs; |
1301 val [unfold_def, corec_def] = map (Morphism.thm phi) defs; |