equal
deleted
inserted
replaced
204 |
204 |
205 val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) |
205 val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) |
206 |> map prop_of |
206 |> map prop_of |
207 |> map Logic.strip_horn |
207 |> map Logic.strip_horn |
208 |> split_list |
208 |> split_list |
209 |>> map (map strip_params_prems_concl) |
209 |>> (map o map) strip_params_prems_concl |
210 |
210 |
211 val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss) |
211 val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss) |
212 in |
212 in |
213 Goal.prove_multi lthy'' [] prems main_concls |
213 Goal.prove_multi lthy'' [] prems main_concls |
214 (fn {prems:thm list, context} => |
214 (fn {prems:thm list, context} => |
312 fun rawify_bnds bnds = |
312 fun rawify_bnds bnds = |
313 map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds |
313 map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds |
314 |
314 |
315 fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys) |
315 fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys) |
316 in |
316 in |
317 map (map (map rawify_bclause)) bclauses |
317 (map o map o map) rawify_bclause bclauses |
318 end |
318 end |
319 *} |
319 *} |
320 |
320 |
321 |
321 |
322 ML {* |
322 ML {* |
388 |> map dest_TFree |
388 |> map dest_TFree |
389 |
389 |
390 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names |
390 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names |
391 |
391 |
392 val raw_cns_info = all_dtyp_constrs_types descr sorts |
392 val raw_cns_info = all_dtyp_constrs_types descr sorts |
393 val raw_constrs = map (map (fn (c, _, _, _) => c)) raw_cns_info |
393 val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info |
394 |
394 |
395 val raw_inject_thms = flat (map #inject dtinfos) |
395 val raw_inject_thms = flat (map #inject dtinfos) |
396 val raw_distinct_thms = flat (map #distinct dtinfos) |
396 val raw_distinct_thms = flat (map #distinct dtinfos) |
397 val raw_induct_thm = #induct dtinfo |
397 val raw_induct_thm = #induct dtinfo |
398 val raw_induct_thms = #inducts dtinfo |
398 val raw_induct_thms = #inducts dtinfo |
628 val lthy9a = |
628 val lthy9a = |
629 if get_STEPS lthy > 26 |
629 if get_STEPS lthy > 26 |
630 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
630 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
631 else raise TEST lthy9 |
631 else raise TEST lthy9 |
632 |
632 |
633 val qtrms = map (map #qconst) qconstrs_infos |
633 val qtrms = (map o map) #qconst qconstrs_infos |
634 val qbns = map #qconst qbns_info |
634 val qbns = map #qconst qbns_info |
635 val qfvs = map #qconst qfvs_info |
635 val qfvs = map #qconst qfvs_info |
636 val qfv_bns = map #qconst qfv_bns_info |
636 val qfv_bns = map #qconst qfv_bns_info |
637 val qalpha_bns = map #qconst qalpha_bns_info |
637 val qalpha_bns = map #qconst qalpha_bns_info |
638 val qperm_bns = map #qconst qperm_bns_info |
638 val qperm_bns = map #qconst qperm_bns_info |
858 ML {* |
858 ML {* |
859 fun prepare_bclauses dt_strs thy = |
859 fun prepare_bclauses dt_strs thy = |
860 let |
860 let |
861 val annos_bclauses = |
861 val annos_bclauses = |
862 get_cnstrs dt_strs |
862 get_cnstrs dt_strs |
863 |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) |
863 |> (map o map) (fn (_, antys, _, bns) => (map fst antys, bns)) |
864 |
864 |
865 fun prep_binder env bn_str = |
865 fun prep_binder env bn_str = |
866 case (Syntax.read_term_global thy bn_str) of |
866 case (Syntax.read_term_global thy bn_str) of |
867 Free (x, _) => (NONE, index_lookup env x) |
867 Free (x, _) => (NONE, index_lookup env x) |
868 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
868 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
883 val env = indexify annos (* for every label, associate the index *) |
883 val env = indexify annos (* for every label, associate the index *) |
884 in |
884 in |
885 map (prep_bclause env) bclause_strs |
885 map (prep_bclause env) bclause_strs |
886 end |
886 end |
887 in |
887 in |
888 (map (map prep_bclauses) annos_bclauses, thy) |
888 ((map o map) prep_bclauses annos_bclauses, thy) |
889 end |
889 end |
890 *} |
890 *} |
891 |
891 |
892 text {* |
892 text {* |
893 adds an empty binding clause for every argument |
893 adds an empty binding clause for every argument |
907 ML {* |
907 ML {* |
908 fun complete dt_strs bclauses = |
908 fun complete dt_strs bclauses = |
909 let |
909 let |
910 val args = |
910 val args = |
911 get_cnstrs dt_strs |
911 get_cnstrs dt_strs |
912 |> map (map (fn (_, antys, _, _) => length antys)) |
912 |> (map o map) (fn (_, antys, _, _) => length antys) |
913 |
913 |
914 fun complt n bcs = |
914 fun complt n bcs = |
915 let |
915 let |
916 fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) |
916 fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) |
917 in |
917 in |