10 sig |
10 sig |
11 val to_set_att: thm list -> attribute |
11 val to_set_att: thm list -> attribute |
12 val to_pred_att: thm list -> attribute |
12 val to_pred_att: thm list -> attribute |
13 val pred_set_conv_att: attribute |
13 val pred_set_conv_att: attribute |
14 val add_inductive_i: |
14 val add_inductive_i: |
15 {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring, |
15 InductivePackage.inductive_flags -> |
16 coind: bool, no_elim: bool, no_ind: bool} -> |
|
17 ((string * typ) * mixfix) list -> |
16 ((string * typ) * mixfix) list -> |
18 (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> |
17 (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> |
19 local_theory -> InductivePackage.inductive_result * local_theory |
18 local_theory -> InductivePackage.inductive_result * local_theory |
20 val add_inductive: bool -> bool -> (string * string option * mixfix) list -> |
19 val add_inductive: bool -> bool -> (string * string option * mixfix) list -> |
21 (string * string option * mixfix) list -> |
20 (string * string option * mixfix) list -> |
400 fun code_ind_att optmod = to_pred_att [] #> InductiveCodegen.add optmod NONE; |
399 fun code_ind_att optmod = to_pred_att [] #> InductiveCodegen.add optmod NONE; |
401 |
400 |
402 |
401 |
403 (**** definition of inductive sets ****) |
402 (**** definition of inductive sets ****) |
404 |
403 |
405 fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind} |
404 fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono} |
406 cs intros monos params cnames_syn ctxt = |
405 cs intros monos params cnames_syn ctxt = |
407 let |
406 let |
408 val thy = ProofContext.theory_of ctxt; |
407 val thy = ProofContext.theory_of ctxt; |
409 val {set_arities, pred_arities, to_pred_simps, ...} = |
408 val {set_arities, pred_arities, to_pred_simps, ...} = |
410 PredSetConvData.get (Context.Proof ctxt); |
409 PredSetConvData.get (Context.Proof ctxt); |
464 eta_contract (member op = cs' orf is_pred pred_arities))) intros; |
463 eta_contract (member op = cs' orf is_pred pred_arities))) intros; |
465 val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn; |
464 val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn; |
466 val monos' = map (to_pred [] (Context.Proof ctxt)) monos; |
465 val monos' = map (to_pred [] (Context.Proof ctxt)) monos; |
467 val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = |
466 val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = |
468 InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind, |
467 InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind, |
469 alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind} |
468 alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} |
470 cs' intros' monos' params1 cnames_syn' ctxt; |
469 cs' intros' monos' params1 cnames_syn' ctxt; |
471 |
470 |
472 (* define inductive sets using previously defined predicates *) |
471 (* define inductive sets using previously defined predicates *) |
473 val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK) |
472 val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK) |
474 (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []), |
473 (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []), |