blanchet@50127: (* Title: HOL/Codatatype/Tools/bnf_fp_sugar.ML blanchet@50127: Author: Jasmin Blanchette, TU Muenchen blanchet@50127: Copyright 2012 blanchet@50127: blanchet@50404: Sugared datatype and codatatype constructions. blanchet@50127: *) blanchet@50127: blanchet@50127: signature BNF_FP_SUGAR = blanchet@50127: sig blanchet@50312: val datatyp: bool -> blanchet@50323: (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list -> blanchet@50323: BNF_Def.BNF list -> local_theory -> blanchet@50352: (term list * term list * term list * term list * thm * thm list * thm list * thm list * blanchet@50352: thm list * thm list) * local_theory) -> blanchet@50313: bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) * blanchet@50312: (binding * typ) list) * (binding * term) list) * mixfix) list) list -> blanchet@50312: local_theory -> local_theory blanchet@50323: val parse_datatype_cmd: bool -> blanchet@50323: (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list -> blanchet@50323: BNF_Def.BNF list -> local_theory -> blanchet@50352: (term list * term list * term list * term list * thm * thm list * thm list * thm list * blanchet@50352: thm list * thm list) * local_theory) -> blanchet@50323: (local_theory -> local_theory) parser blanchet@50127: end; blanchet@50127: blanchet@50127: structure BNF_FP_Sugar : BNF_FP_SUGAR = blanchet@50127: struct blanchet@50127: blanchet@50134: open BNF_Util blanchet@50134: open BNF_Wrap blanchet@50229: open BNF_Def blanchet@50134: open BNF_FP_Util blanchet@50138: open BNF_FP_Sugar_Tactics blanchet@50134: blanchet@50315: val simp_attrs = @{attributes [simp]}; blanchet@50315: blanchet@50385: fun split_list10 xs = blanchet@50281: (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs, blanchet@50385: map #9 xs, map #10 xs); blanchet@50229: blanchet@50357: fun resort_tfree S (TFree (s, _)) = TFree (s, S); blanchet@50357: blanchet@50229: fun typ_subst inst (T as Type (s, Ts)) = blanchet@50229: (case AList.lookup (op =) inst T of blanchet@50229: NONE => Type (s, map (typ_subst inst) Ts) blanchet@50229: | SOME T' => T') blanchet@50229: | typ_subst inst T = the_default T (AList.lookup (op =) inst T); blanchet@50220: blanchet@50312: val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)); blanchet@50217: blanchet@50215: fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); blanchet@50215: fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; blanchet@50217: fun mk_uncurried2_fun f xss = blanchet@50215: mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss); blanchet@50215: blanchet@50248: fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v)); blanchet@50248: blanchet@50248: fun tack z_name (c, v) f = blanchet@50288: let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in blanchet@50288: Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z) blanchet@50288: end; blanchet@50229: blanchet@50139: fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; blanchet@50134: blanchet@50313: fun merge_type_arg T T' = if T = T' then T else cannot_merge_types (); blanchet@50134: blanchet@50313: fun merge_type_args (As, As') = blanchet@50313: if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types (); blanchet@50134: blanchet@50136: fun type_args_constrained_of (((cAs, _), _), _) = cAs; blanchet@50351: fun type_binding_of (((_, b), _), _) = b; blanchet@50196: fun mixfix_of ((_, mx), _) = mx; blanchet@50136: fun ctr_specs_of (_, ctr_specs) = ctr_specs; blanchet@50134: blanchet@50301: fun disc_of ((((disc, _), _), _), _) = disc; blanchet@50301: fun ctr_of ((((_, ctr), _), _), _) = ctr; blanchet@50301: fun args_of (((_, args), _), _) = args; blanchet@50301: fun defaults_of ((_, ds), _) = ds; blanchet@50196: fun ctr_mixfix_of (_, mx) = mx; blanchet@50134: blanchet@50323: fun define_datatype prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs) blanchet@50313: no_defs_lthy0 = blanchet@50127: let blanchet@50313: (* TODO: sanity checks on arguments *) blanchet@50313: blanchet@50301: val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes" blanchet@50293: else (); blanchet@50293: blanchet@50382: val nn = length specs; blanchet@50376: val fp_bs = map type_binding_of specs; blanchet@50376: val fp_common_name = mk_common_name fp_bs; blanchet@50134: blanchet@50313: fun prepare_type_arg (ty, c) = blanchet@50313: let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in blanchet@50313: TFree (s, prepare_constraint no_defs_lthy0 c) blanchet@50313: end; blanchet@50134: blanchet@50313: val Ass0 = map (map prepare_type_arg o type_args_constrained_of) specs; blanchet@50313: val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0; blanchet@50313: val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0; blanchet@50134: blanchet@50385: val ((Bs, Cs), no_defs_lthy) = blanchet@50313: no_defs_lthy0 blanchet@50313: |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As blanchet@50382: |> mk_TFrees nn blanchet@50385: ||>> mk_TFrees nn; blanchet@50313: blanchet@50313: (* TODO: cleaner handling of fake contexts, without "background_theory" *) blanchet@50313: (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a blanchet@50313: locale and shadows an existing global type*) blanchet@50313: val fake_thy = blanchet@50313: Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy blanchet@50351: (type_binding_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs; blanchet@50313: val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy; blanchet@50134: blanchet@50197: fun mk_fake_T b = blanchet@50136: Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))), blanchet@50313: unsorted_As); blanchet@50136: blanchet@50317: val fake_Ts = map mk_fake_T fp_bs; blanchet@50136: blanchet@50196: val mixfixes = map mixfix_of specs; blanchet@50134: blanchet@50317: val _ = (case duplicates Binding.eq_name fp_bs of [] => () blanchet@50134: | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); blanchet@50134: blanchet@50136: val ctr_specss = map ctr_specs_of specs; blanchet@50134: blanchet@50351: val disc_bindingss = map (map disc_of) ctr_specss; blanchet@50351: val ctr_bindingss = blanchet@50317: map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of)) blanchet@50317: fp_bs ctr_specss; blanchet@50136: val ctr_argsss = map (map args_of) ctr_specss; blanchet@50196: val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss; blanchet@50134: blanchet@50351: val sel_bindingsss = map (map (map fst)) ctr_argsss; blanchet@50313: val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; blanchet@50301: val raw_sel_defaultsss = map (map defaults_of) ctr_specss; blanchet@50301: blanchet@50323: val (As :: _) :: fake_ctr_Tsss = blanchet@50313: burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0); blanchet@50313: blanchet@50313: val _ = (case duplicates (op =) unsorted_As of [] => () blanchet@50313: | A :: _ => error ("Duplicate type parameter " ^ blanchet@50313: quote (Syntax.string_of_typ no_defs_lthy A))); blanchet@50313: blanchet@50198: val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss []; blanchet@50313: val _ = (case subtract (op =) (map dest_TFree As) rhs_As' of blanchet@50180: [] => () blanchet@50357: | A' :: _ => error ("Extra type variable on right-hand side: " ^ blanchet@50219: quote (Syntax.string_of_typ no_defs_lthy (TFree A')))); blanchet@50180: blanchet@50219: fun eq_fpT (T as Type (s, Us)) (Type (s', Us')) = blanchet@50161: s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^ blanchet@50161: quote (Syntax.string_of_typ fake_lthy T))) blanchet@50219: | eq_fpT _ _ = false; blanchet@50161: blanchet@50219: fun freeze_fp (T as Type (s, Us)) = blanchet@50313: (case find_index (eq_fpT T) fake_Ts of ~1 => Type (s, map freeze_fp Us) | j => nth Bs j) blanchet@50219: | freeze_fp T = T; blanchet@50134: blanchet@50312: val ctr_TsssBs = map (map (map freeze_fp)) fake_ctr_Tsss; blanchet@50312: val ctr_sum_prod_TsBs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssBs; blanchet@50134: blanchet@50313: val fp_eqs = blanchet@50313: map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs; blanchet@50136: blanchet@50352: val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, fp_induct, unf_flds, fld_unfs, fld_injects, blanchet@50222: fp_iter_thms, fp_rec_thms), lthy)) = blanchet@50323: fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0; blanchet@50136: blanchet@50378: fun add_nesty_bnf_names Us = blanchet@50241: let blanchet@50241: fun add (Type (s, Ts)) ss = blanchet@50241: let val (needs, ss') = fold_map add Ts ss in blanchet@50241: if exists I needs then (true, insert (op =) s ss') else (false, ss') blanchet@50241: end blanchet@50378: | add T ss = (member (op =) Us T, ss); blanchet@50241: in snd oo add end; blanchet@50241: blanchet@50378: fun nesty_bnfs Us = blanchet@50378: map_filter (bnf_of lthy) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_TsssBs []); blanchet@50378: blanchet@50378: val nesting_bnfs = nesty_bnfs As; blanchet@50378: val nested_bnfs = nesty_bnfs Bs; blanchet@50241: blanchet@50182: val timer = time (Timer.startRealTimer ()); blanchet@50182: blanchet@50191: fun mk_unf_or_fld get_T Ts t = blanchet@50191: let val Type (_, Ts0) = get_T (fastype_of t) in blanchet@50139: Term.subst_atomic_types (Ts0 ~~ Ts) t blanchet@50136: end; blanchet@50136: blanchet@50141: val mk_unf = mk_unf_or_fld domain_type; blanchet@50141: val mk_fld = mk_unf_or_fld range_type; blanchet@50139: blanchet@50218: val unfs = map (mk_unf As) unfs0; blanchet@50218: val flds = map (mk_fld As) flds0; blanchet@50136: blanchet@50216: val fpTs = map (domain_type o fastype_of) unfs; blanchet@50377: blanchet@50377: val exists_fp_subtype = exists_subtype (member (op =) fpTs); blanchet@50377: blanchet@50312: val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs; blanchet@50218: val ns = map length ctr_Tsss; blanchet@50227: val kss = map (fn n => 1 upto n) ns; blanchet@50218: val mss = map (map length) ctr_Tsss; blanchet@50218: val Css = map2 replicate ns Cs; blanchet@50218: blanchet@50229: fun mk_iter_like Ts Us t = blanchet@50134: let blanchet@50351: val (bindings, body) = strip_type (fastype_of t); blanchet@50351: val (f_Us, prebody) = split_last bindings; blanchet@50225: val Type (_, Ts0) = if lfp then prebody else body; blanchet@50225: val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us); blanchet@50191: in blanchet@50229: Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t blanchet@50191: end; blanchet@50191: blanchet@50225: val fp_iters as fp_iter1 :: _ = map (mk_iter_like As Cs) fp_iters0; blanchet@50225: val fp_recs as fp_rec1 :: _ = map (mk_iter_like As Cs) fp_recs0; blanchet@50225: blanchet@50227: val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1))); blanchet@50227: val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1))); blanchet@50219: blanchet@50271: val ((iter_only as (gss, _, _), rec_only as (hss, _, _)), blanchet@50291: (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))) = blanchet@50223: if lfp then blanchet@50223: let blanchet@50223: val y_Tsss = blanchet@50270: map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type) blanchet@50227: ns mss fp_iter_fun_Ts; blanchet@50223: val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css; blanchet@50219: blanchet@50223: val ((gss, ysss), _) = blanchet@50223: lthy blanchet@50223: |> mk_Freess "f" g_Tss blanchet@50223: ||>> mk_Freesss "x" y_Tsss; blanchet@50289: val yssss = map (map (map single)) ysss; blanchet@50289: blanchet@50289: fun dest_rec_prodT (T as Type (@{type_name prod}, Us as [_, U])) = blanchet@50289: if member (op =) Cs U then Us else [T] blanchet@50289: | dest_rec_prodT T = [T]; blanchet@50219: blanchet@50223: val z_Tssss = blanchet@50289: map3 (fn n => fn ms => map2 (map dest_rec_prodT oo dest_tupleT) ms o blanchet@50270: dest_sumTN_balanced n o domain_type) ns mss fp_rec_fun_Ts; blanchet@50223: val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css; blanchet@50223: blanchet@50313: val hss = map2 (map2 retype_free) h_Tss gss; blanchet@50313: val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss; blanchet@50289: val (zssss_tl, _) = blanchet@50223: lthy blanchet@50289: |> mk_Freessss "y" (map (map (map tl)) z_Tssss); blanchet@50289: val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl; blanchet@50225: in blanchet@50289: (((gss, g_Tss, yssss), (hss, h_Tss, zssss)), blanchet@50291: ([], [], [], (([], []), ([], [])), (([], []), ([], [])))) blanchet@50225: end blanchet@50223: else blanchet@50225: let blanchet@50236: (*avoid "'a itself" arguments in coiterators and corecursors*) blanchet@50236: val mss' = map (fn [0] => [1] | ms => ms) mss; blanchet@50236: blanchet@50290: val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_predT) ns Cs; blanchet@50191: blanchet@50291: fun zip_predss_getterss qss fss = maps (op @) (qss ~~ fss); blanchet@50230: blanchet@50291: fun zip_preds_predsss_gettersss [] [qss] [fss] = zip_predss_getterss qss fss blanchet@50291: | zip_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) = blanchet@50291: p :: zip_predss_getterss qss fss @ zip_preds_predsss_gettersss ps qsss fsss; blanchet@50289: blanchet@50289: fun mk_types maybe_dest_sumT fun_Ts = blanchet@50227: let blanchet@50227: val f_sum_prod_Ts = map range_type fun_Ts; blanchet@50270: val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; blanchet@50290: val f_Tssss = blanchet@50290: map3 (fn C => map2 (map (map (curry (op -->) C) o maybe_dest_sumT) oo dest_tupleT)) blanchet@50290: Cs mss' f_prod_Tss; blanchet@50290: val q_Tssss = blanchet@50290: map (map (map (fn [_] => [] | [_, C] => [mk_predT (domain_type C)]))) f_Tssss; blanchet@50291: val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; blanchet@50290: in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end; blanchet@50226: blanchet@50290: val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts; blanchet@50226: blanchet@50290: val ((((Free (z, _), cs), pss), gssss), _) = blanchet@50225: lthy blanchet@50248: |> yield_singleton (mk_Frees "z") dummyT blanchet@50248: ||>> mk_Frees "a" Cs blanchet@50226: ||>> mk_Freess "p" p_Tss blanchet@50290: ||>> mk_Freessss "g" g_Tssss; blanchet@50290: val rssss = map (map (map (fn [] => []))) r_Tssss; blanchet@50289: blanchet@50289: fun dest_corec_sumT (T as Type (@{type_name sum}, Us as [_, U])) = blanchet@50289: if member (op =) Cs U then Us else [T] blanchet@50289: | dest_corec_sumT T = [T]; blanchet@50289: blanchet@50290: val (s_Tssss, h_sum_prod_Ts, h_Tssss, ph_Tss) = mk_types dest_corec_sumT fp_rec_fun_Ts; blanchet@50225: blanchet@50313: val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss; blanchet@50290: val ((sssss, hssss_tl), _) = blanchet@50290: lthy blanchet@50290: |> mk_Freessss "q" s_Tssss blanchet@50290: ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss); blanchet@50290: val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl; blanchet@50226: blanchet@50227: val cpss = map2 (fn c => map (fn p => p $ c)) cs pss; blanchet@50227: blanchet@50291: fun mk_preds_getters_join [] [cf] = cf blanchet@50291: | mk_preds_getters_join [cq] [cf, cf'] = blanchet@50291: mk_If cq (mk_Inl (fastype_of cf') cf) (mk_Inr (fastype_of cf) cf'); blanchet@50291: blanchet@50290: fun mk_terms qssss fssss = blanchet@50227: let blanchet@50291: val pfss = map3 zip_preds_predsss_gettersss pss qssss fssss; blanchet@50290: val cqssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs qssss; blanchet@50289: val cfssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs fssss; blanchet@50291: val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss; blanchet@50291: in (pfss, cqfsss) end; blanchet@50225: in blanchet@50227: ((([], [], []), ([], [], [])), blanchet@50290: ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)), blanchet@50290: (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))) blanchet@50225: end; blanchet@50225: blanchet@50385: fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec), blanchet@50385: fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss), blanchet@50385: disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = blanchet@50191: let blanchet@50216: val unfT = domain_type (fastype_of fld); blanchet@50225: val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; blanchet@50270: val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts; blanchet@50149: val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss; blanchet@50139: blanchet@50385: val ((((u, fs), xss), v'), _) = blanchet@50219: no_defs_lthy blanchet@50216: |> yield_singleton (mk_Frees "u") unfT blanchet@50191: ||>> mk_Frees "f" case_Ts blanchet@50385: ||>> mk_Freess "x" ctr_Tss blanchet@50385: ||>> yield_singleton (Variable.variant_fixes) (Binding.name_of fp_b); blanchet@50385: blanchet@50385: val v = Free (v', fpT); blanchet@50136: blanchet@50144: val ctr_rhss = blanchet@50271: map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $ blanchet@50271: mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss; blanchet@50136: blanchet@50351: val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b; blanchet@50144: blanchet@50149: val case_rhs = blanchet@50270: fold_rev Term.lambda (fs @ [v]) blanchet@50270: (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (unf $ v)); blanchet@50144: blanchet@50216: val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy blanchet@50184: |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => blanchet@50317: Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd) blanchet@50351: (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss) blanchet@50136: ||> `Local_Theory.restore; blanchet@50136: blanchet@50136: val phi = Proof_Context.export_morphism lthy lthy'; blanchet@50136: blanchet@50136: val ctr_defs = map (Morphism.thm phi) raw_ctr_defs; blanchet@50145: val case_def = Morphism.thm phi raw_case_def; blanchet@50145: blanchet@50218: val ctrs0 = map (Morphism.term phi) raw_ctrs; blanchet@50218: val casex0 = Morphism.term phi raw_case; blanchet@50218: blanchet@50218: val ctrs = map (mk_ctr As) ctrs0; blanchet@50136: blanchet@50150: fun exhaust_tac {context = ctxt, ...} = blanchet@50138: let blanchet@50150: val fld_iff_unf_thm = blanchet@50150: let blanchet@50150: val goal = blanchet@50150: fold_rev Logic.all [u, v] blanchet@50150: (mk_Trueprop_eq (HOLogic.mk_eq (v, fld $ u), HOLogic.mk_eq (unf $ v, u))); blanchet@50150: in blanchet@50150: Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => blanchet@50216: mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unfT, fpT]) blanchet@50191: (certify lthy fld) (certify lthy unf) fld_unf unf_fld) blanchet@50150: |> Thm.close_derivation blanchet@50150: |> Morphism.thm phi blanchet@50150: end; blanchet@50150: blanchet@50150: val sumEN_thm' = blanchet@50150: Local_Defs.unfold lthy @{thms all_unit_eq} blanchet@50270: (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) [] blanchet@50270: (mk_sumEN_balanced n)) blanchet@50150: |> Morphism.thm phi; blanchet@50138: in blanchet@50176: mk_exhaust_tac ctxt n ctr_defs fld_iff_unf_thm sumEN_thm' blanchet@50138: end; blanchet@50136: blanchet@50141: val inject_tacss = blanchet@50220: map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} => blanchet@50220: mk_inject_tac ctxt ctr_def fld_inject]) ms ctr_defs; blanchet@50141: blanchet@50142: val half_distinct_tacss = blanchet@50142: map (map (fn (def, def') => fn {context = ctxt, ...} => blanchet@50142: mk_half_distinct_tac ctxt fld_inject [def, def'])) (mk_half_pairss ctr_defs); blanchet@50142: blanchet@50145: val case_tacs = blanchet@50145: map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} => blanchet@50145: mk_case_tac ctxt n k m case_def ctr_def unf_fld) ks ms ctr_defs; blanchet@50136: blanchet@50136: val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs]; blanchet@50149: blanchet@50302: fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) = blanchet@50149: let blanchet@50223: val fpT_to_C = fpT --> C; blanchet@50214: blanchet@50230: fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) = blanchet@50230: let blanchet@50230: val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C; blanchet@50351: val binding = Binding.suffix_name ("_" ^ suf) fp_b; blanchet@50230: val spec = blanchet@50351: mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)), blanchet@50230: Term.list_comb (fp_iter_like, blanchet@50270: map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)); blanchet@50351: in (binding, spec) end; blanchet@50230: blanchet@50315: val iter_like_infos = blanchet@50230: [(iterN, fp_iter, iter_only), blanchet@50230: (recN, fp_rec, rec_only)]; blanchet@50230: blanchet@50351: val (bindings, specs) = map generate_iter_like iter_like_infos |> split_list; blanchet@50230: blanchet@50230: val ((csts, defs), (lthy', lthy)) = no_defs_lthy blanchet@50216: |> apfst split_list o fold_map2 (fn b => fn spec => blanchet@50214: Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) blanchet@50351: #>> apsnd snd) bindings specs blanchet@50214: ||> `Local_Theory.restore; blanchet@50216: blanchet@50216: val phi = Proof_Context.export_morphism lthy lthy'; blanchet@50216: blanchet@50230: val [iter_def, rec_def] = map (Morphism.thm phi) defs; blanchet@50216: blanchet@50230: val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts; blanchet@50149: in blanchet@50385: ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy) blanchet@50149: end; blanchet@50149: blanchet@50302: fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) = blanchet@50225: let blanchet@50225: val B_to_fpT = C --> fpT; blanchet@50225: blanchet@50291: fun mk_preds_getterss_join c n cps sum_prod_T cqfss = blanchet@50291: Term.lambda c (mk_IfN sum_prod_T cps blanchet@50291: (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n))); blanchet@50290: blanchet@50291: fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqfsss), (f_sum_prod_Ts, blanchet@50289: pf_Tss))) = blanchet@50226: let blanchet@50226: val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT; blanchet@50351: val binding = Binding.suffix_name ("_" ^ suf) fp_b; blanchet@50226: val spec = blanchet@50351: mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)), blanchet@50226: Term.list_comb (fp_iter_like, blanchet@50291: map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss)); blanchet@50351: in (binding, spec) end; blanchet@50225: blanchet@50315: val coiter_like_infos = blanchet@50230: [(coiterN, fp_iter, coiter_only), blanchet@50230: (corecN, fp_rec, corec_only)]; blanchet@50227: blanchet@50351: val (bindings, specs) = map generate_coiter_like coiter_like_infos |> split_list; blanchet@50226: blanchet@50226: val ((csts, defs), (lthy', lthy)) = no_defs_lthy blanchet@50225: |> apfst split_list o fold_map2 (fn b => fn spec => blanchet@50225: Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) blanchet@50351: #>> apsnd snd) bindings specs blanchet@50225: ||> `Local_Theory.restore; blanchet@50225: blanchet@50225: val phi = Proof_Context.export_morphism lthy lthy'; blanchet@50225: blanchet@50226: val [coiter_def, corec_def] = map (Morphism.thm phi) defs; blanchet@50225: blanchet@50226: val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts; blanchet@50225: in blanchet@50385: ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def), blanchet@50385: lthy) blanchet@50225: end; blanchet@50301: blanchet@50302: fun wrap lthy = blanchet@50302: let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in blanchet@50351: wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss, blanchet@50302: sel_defaultss))) lthy blanchet@50302: end; blanchet@50302: blanchet@50302: val define_iter_likes = if lfp then define_iter_rec else define_coiter_corec; blanchet@50134: in blanchet@50302: ((wrap, define_iter_likes), lthy') blanchet@50134: end; blanchet@50182: blanchet@50241: val pre_map_defs = map map_def_of_bnf pre_bnfs; blanchet@50357: val pre_set_defss = map set_defs_of_bnf pre_bnfs; blanchet@50383: val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs; blanchet@50378: val nesting_map_ids = map map_id_of_bnf nesting_bnfs; blanchet@50241: blanchet@50408: fun mk_map live Ts Us t = blanchet@50441: let blanchet@50441: val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last blanchet@50441: in blanchet@50229: Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t blanchet@50229: end; blanchet@50229: blanchet@50396: fun build_map build_arg (T as Type (s, Ts)) (U as Type (_, Us)) = blanchet@50249: let blanchet@50407: val bnf = the (bnf_of lthy s); blanchet@50408: val live = live_of_bnf bnf; blanchet@50408: val mapx = mk_map live Ts Us (map_of_bnf bnf); blanchet@50408: val TUs = map dest_funT (fst (strip_typeN live (fastype_of mapx))); blanchet@50249: val args = map build_arg TUs; blanchet@50249: in Term.list_comb (mapx, args) end; blanchet@50249: blanchet@50385: fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _, blanchet@50352: iter_defs, rec_defs), lthy) = blanchet@50217: let blanchet@50385: val (((phis, phis'), vs'), names_lthy) = blanchet@50385: lthy blanchet@50385: |> mk_Frees' "P" (map mk_predT fpTs) blanchet@50385: ||>> Variable.variant_fixes (map Binding.name_of fp_bs); blanchet@50385: blanchet@50385: val vs = map2 (curry Free) vs' fpTs; blanchet@50385: blanchet@50377: fun mk_sets_nested bnf = blanchet@50377: let blanchet@50377: val Type (T_name, Us) = T_of_bnf bnf; blanchet@50377: val lives = lives_of_bnf bnf; blanchet@50377: val sets = sets_of_bnf bnf; blanchet@50377: fun mk_set U = blanchet@50377: (case find_index (curry (op =) U) lives of blanchet@50377: ~1 => Term.dummy blanchet@50377: | i => nth sets i); blanchet@50377: in blanchet@50377: (T_name, map mk_set Us) blanchet@50377: end; blanchet@50377: blanchet@50377: val setss_nested = map mk_sets_nested nested_bnfs; blanchet@50377: blanchet@50352: val (induct_thms, induct_thm) = blanchet@50352: let blanchet@50377: fun mk_set Ts t = blanchet@50377: let val Type (_, Ts0) = domain_type (fastype_of t) in blanchet@50377: Term.subst_atomic_types (Ts0 ~~ Ts) t blanchet@50377: end; blanchet@50377: blanchet@50390: fun mk_raw_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) = blanchet@50376: (case find_index (curry (op =) T) fpTs of blanchet@50377: ~1 => blanchet@50377: (case AList.lookup (op =) setss_nested T_name of blanchet@50377: NONE => [] blanchet@50377: | SOME raw_sets0 => blanchet@50377: let blanchet@50377: val (Ts, raw_sets) = blanchet@50377: split_list (filter (exists_fp_subtype o fst) (Ts0 ~~ raw_sets0)); blanchet@50377: val sets = map (mk_set Ts0) raw_sets; blanchet@50377: val (ys, names_lthy') = names_lthy |> mk_Frees s Ts; blanchet@50390: val xysets = map (pair x) (ys ~~ sets); blanchet@50390: val ppremss = map (mk_raw_prem_prems names_lthy') ys; blanchet@50377: in blanchet@50390: flat (map2 (map o apfst o cons) xysets ppremss) blanchet@50377: end) blanchet@50391: | i => [([], (i + 1, x))]) blanchet@50390: | mk_raw_prem_prems _ _ = []; blanchet@50357: blanchet@50393: fun close_prem_prem xs t = blanchet@50393: fold_rev Logic.all (map Free (drop (nn + length xs) blanchet@50393: (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t; blanchet@50377: blanchet@50393: fun mk_prem_prem xs (xysets, (j, x)) = blanchet@50393: close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) => blanchet@50391: HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets, blanchet@50391: HOLogic.mk_Trueprop (nth phis (j - 1) $ x))); blanchet@50390: blanchet@50387: fun mk_raw_prem phi ctr ctr_Ts = blanchet@50377: let blanchet@50377: val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; blanchet@50391: val pprems = maps (mk_raw_prem_prems names_lthy') xs; blanchet@50393: in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end; blanchet@50357: blanchet@50391: fun mk_prem (xs, raw_pprems, concl) = blanchet@50393: fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl)); blanchet@50383: blanchet@50404: val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss; blanchet@50404: blanchet@50376: val goal = blanchet@50387: Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, blanchet@50383: HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj blanchet@50383: (map2 (curry (op $)) phis vs))); blanchet@50383: blanchet@50444: val kksss = map (map (map (fst o snd) o #2)) raw_premss; blanchet@50383: blanchet@50383: val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); blanchet@50357: blanchet@50357: val induct_thm = blanchet@50376: Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => blanchet@50444: mk_induct_tac ctxt ns mss kksss (flat ctr_defss) fld_induct' blanchet@50404: nested_set_natural's pre_set_defss) blanchet@50383: |> singleton (Proof_Context.export names_lthy lthy) blanchet@50352: in blanchet@50382: `(conj_dests nn) induct_thm blanchet@50352: end; blanchet@50216: blanchet@50217: val (iter_thmss, rec_thmss) = blanchet@50222: let blanchet@50352: val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; blanchet@50352: val giters = map (lists_bmoc gss) iters; blanchet@50352: val hrecs = map (lists_bmoc hss) recs; blanchet@50352: blanchet@50227: fun mk_goal_iter_like fss fiter_like xctr f xs fxs = blanchet@50222: fold_rev (fold_rev Logic.all) (xs :: fss) blanchet@50227: (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs))); blanchet@50216: blanchet@50249: fun build_call fiter_likes maybe_tick (T, U) = blanchet@50249: if T = U then blanchet@50383: id_const T blanchet@50249: else blanchet@50249: (case find_index (curry (op =) T) fpTs of blanchet@50249: ~1 => build_map (build_call fiter_likes maybe_tick) T U blanchet@50249: | j => maybe_tick (nth vs j) (nth fiter_likes j)); blanchet@50248: blanchet@50289: fun mk_U maybe_mk_prodT = blanchet@50289: typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs); blanchet@50229: blanchet@50357: fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) = blanchet@50229: if member (op =) fpTs T then blanchet@50248: maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x] blanchet@50377: else if exists_fp_subtype T then blanchet@50289: [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x] blanchet@50229: else blanchet@50229: [x]; blanchet@50229: blanchet@50357: val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss; blanchet@50357: val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss; blanchet@50219: blanchet@50227: val goal_iterss = map5 (map4 o mk_goal_iter_like gss) giters xctrss gss xsss gxsss; blanchet@50227: val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss; blanchet@50219: blanchet@50218: val iter_tacss = blanchet@50378: map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms blanchet@50378: ctr_defss; blanchet@50218: val rec_tacss = blanchet@50378: map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms blanchet@50378: ctr_defss; blanchet@50217: in blanchet@50291: (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) blanchet@50220: goal_iterss iter_tacss, blanchet@50291: map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) blanchet@50220: goal_recss rec_tacss) blanchet@50217: end; blanchet@50216: blanchet@50352: val common_notes = blanchet@50382: (if nn > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else []) blanchet@50352: |> map (fn (thmN, thms, attrs) => blanchet@50352: ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])])); blanchet@50352: blanchet@50241: val notes = blanchet@50357: [(inductN, map single induct_thms, []), (* FIXME: attribs *) blanchet@50357: (itersN, iter_thmss, simp_attrs), blanchet@50315: (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)] blanchet@50315: |> maps (fn (thmN, thmss, attrs) => blanchet@50217: map2 (fn b => fn thms => blanchet@50315: ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), blanchet@50317: [(thms, [])])) fp_bs thmss); blanchet@50217: in blanchet@50352: lthy |> Local_Theory.notes (common_notes @ notes) |> snd blanchet@50217: end; blanchet@50217: blanchet@50385: fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss, blanchet@50385: discIss, sel_thmsss, coiter_defs, corec_defs), lthy) = blanchet@50227: let blanchet@50387: val (vs', _) = blanchet@50385: lthy blanchet@50385: |> Variable.variant_fixes (map Binding.name_of fp_bs); blanchet@50385: blanchet@50385: val vs = map2 (curry Free) vs' fpTs; blanchet@50385: blanchet@50352: val (coinduct_thms, coinduct_thm) = blanchet@50352: let blanchet@50352: val coinduct_thm = fp_induct; blanchet@50352: in blanchet@50382: `(conj_dests nn) coinduct_thm blanchet@50352: end; blanchet@50227: blanchet@50227: val (coiter_thmss, corec_thmss) = blanchet@50227: let blanchet@50352: val z = the_single zs; blanchet@50352: val gcoiters = map (lists_bmoc pgss) coiters; blanchet@50352: val hcorecs = map (lists_bmoc phss) corecs; blanchet@50352: blanchet@50247: fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not); blanchet@50227: blanchet@50291: fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' = blanchet@50227: fold_rev (fold_rev Logic.all) ([c] :: pfss) blanchet@50247: (Logic.list_implies (seq_conds mk_goal_cond n k cps, blanchet@50291: mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs')))); blanchet@50227: blanchet@50249: fun build_call fiter_likes maybe_tack (T, U) = blanchet@50249: if T = U then blanchet@50383: id_const T blanchet@50249: else blanchet@50249: (case find_index (curry (op =) U) fpTs of blanchet@50249: ~1 => build_map (build_call fiter_likes maybe_tack) T U blanchet@50249: | j => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j)); blanchet@50248: blanchet@50289: fun mk_U maybe_mk_sumT = blanchet@50289: typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs); blanchet@50227: blanchet@50357: fun intr_calls fiter_likes maybe_mk_sumT maybe_tack cqf = blanchet@50291: let val T = fastype_of cqf in blanchet@50291: if exists_subtype (member (op =) Cs) T then blanchet@50291: build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf blanchet@50291: else blanchet@50291: cqf blanchet@50291: end; blanchet@50247: blanchet@50357: val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss; blanchet@50357: val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss; blanchet@50227: blanchet@50227: val goal_coiterss = blanchet@50291: map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss crgsss'; blanchet@50248: val goal_corecss = blanchet@50291: map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss'; blanchet@50228: blanchet@50228: val coiter_tacss = blanchet@50378: map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs blanchet@50241: ctr_defss; blanchet@50248: val corec_tacss = blanchet@50378: map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs blanchet@50248: ctr_defss; blanchet@50227: in blanchet@50291: (map2 (map2 (fn goal => fn tac => blanchet@50291: Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation)) blanchet@50228: goal_coiterss coiter_tacss, blanchet@50291: map2 (map2 (fn goal => fn tac => blanchet@50291: Skip_Proof.prove lthy [] [] goal (tac o #context) blanchet@50291: |> Local_Defs.unfold lthy @{thms sum_case_if} |> Thm.close_derivation)) blanchet@50248: goal_corecss corec_tacss) blanchet@50227: end; blanchet@50227: blanchet@50281: fun mk_disc_coiter_like_thms [_] = K [] blanchet@50281: | mk_disc_coiter_like_thms thms = map2 (curry (op RS)) thms; blanchet@50281: blanchet@50281: val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss; blanchet@50281: val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss; blanchet@50281: blanchet@50282: fun mk_sel_coiter_like_thm coiter_like_thm sel0 sel_thm = blanchet@50281: let blanchet@50282: val (domT, ranT) = dest_funT (fastype_of sel0); blanchet@50281: val arg_cong' = blanchet@50281: Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT]) blanchet@50282: [NONE, NONE, SOME (certify lthy sel0)] arg_cong blanchet@50282: |> Thm.varifyT_global; blanchet@50281: val sel_thm' = sel_thm RSN (2, trans); blanchet@50281: in blanchet@50282: coiter_like_thm RS arg_cong' RS sel_thm' blanchet@50281: end; blanchet@50281: blanchet@50281: val sel_coiter_thmsss = blanchet@50281: map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss; blanchet@50281: val sel_corec_thmsss = blanchet@50282: map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss; blanchet@50281: blanchet@50357: val common_notes = blanchet@50382: (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else []) blanchet@50357: |> map (fn (thmN, thms, attrs) => blanchet@50357: ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])])); blanchet@50357: blanchet@50227: val notes = blanchet@50357: [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *) blanchet@50357: (coitersN, coiter_thmss, []), blanchet@50315: (disc_coitersN, disc_coiter_thmss, []), blanchet@50315: (sel_coitersN, map flat sel_coiter_thmsss, []), blanchet@50315: (corecsN, corec_thmss, []), blanchet@50315: (disc_corecsN, disc_corec_thmss, []), blanchet@50315: (sel_corecsN, map flat sel_corec_thmsss, [])] blanchet@50315: |> maps (fn (thmN, thmss, attrs) => blanchet@50281: map_filter (fn (_, []) => NONE | (b, thms) => blanchet@50315: SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), blanchet@50317: [(thms, [])])) (fp_bs ~~ thmss)); blanchet@50227: in blanchet@50376: lthy |> Local_Theory.notes (common_notes @ notes) |> snd blanchet@50227: end; blanchet@50227: blanchet@50302: fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) = blanchet@50385: fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10 blanchet@50302: blanchet@50219: val lthy' = lthy blanchet@50385: |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ blanchet@50385: fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~ blanchet@50385: ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) blanchet@50302: |>> split_list |> wrap_types_and_define_iter_likes blanchet@50352: |> (if lfp then derive_induct_iter_rec_thms_for_types blanchet@50352: else derive_coinduct_coiter_corec_thms_for_types); blanchet@50182: blanchet@50182: val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ blanchet@50223: (if lfp then "" else "co") ^ "datatype")); blanchet@50127: in blanchet@50323: timer; lthy' blanchet@50127: end; blanchet@50127: blanchet@50313: val datatyp = define_datatype (K I) (K I) (K I); blanchet@50312: blanchet@50313: val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term; blanchet@50134: blanchet@50344: val parse_binding_colon = Parse.binding --| @{keyword ":"}; blanchet@50351: val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding; blanchet@50134: blanchet@50127: val parse_ctr_arg = blanchet@50344: @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} || blanchet@50351: (Parse.typ >> pair no_binding); blanchet@50127: blanchet@50301: val parse_defaults = blanchet@50301: @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"}; blanchet@50301: blanchet@50127: val parse_single_spec = blanchet@50127: Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- blanchet@50134: (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding -- blanchet@50301: Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix)); blanchet@50127: blanchet@50293: val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec; blanchet@50293: blanchet@50323: fun parse_datatype_cmd lfp construct = parse_datatype >> datatype_cmd lfp construct; blanchet@50127: blanchet@50127: end;