30 |
30 |
31 signature INDUCTIVE_PACKAGE = |
31 signature INDUCTIVE_PACKAGE = |
32 sig |
32 sig |
33 val quiet_mode: bool ref |
33 val quiet_mode: bool ref |
34 val unify_consts: Sign.sg -> term list -> term list -> term list * term list |
34 val unify_consts: Sign.sg -> term list -> term list -> term list * term list |
35 val get_inductive: theory -> string -> |
35 val get_inductive: theory -> string -> ({names: string list, coind: bool} * |
36 {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, |
36 {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
37 induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
37 intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option |
38 val print_inductives: theory -> unit |
38 val print_inductives: theory -> unit |
39 val mono_add_global: theory attribute |
39 val mono_add_global: theory attribute |
40 val mono_del_global: theory attribute |
40 val mono_del_global: theory attribute |
41 val get_monos: theory -> thm list |
41 val get_monos: theory -> thm list |
42 val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
42 val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
88 val print_inductives = InductiveData.print; |
88 val print_inductives = InductiveData.print; |
89 |
89 |
90 |
90 |
91 (* get and put data *) |
91 (* get and put data *) |
92 |
92 |
93 fun get_inductive thy name = |
93 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name); |
94 (case Symtab.lookup (fst (InductiveData.get thy), name) of |
|
95 Some info => info |
|
96 | None => error ("Unknown (co)inductive set " ^ quote name)); |
|
97 |
94 |
98 fun put_inductives names info thy = |
95 fun put_inductives names info thy = |
99 let |
96 let |
100 fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); |
97 fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); |
101 val tab_monos = foldl upd (InductiveData.get thy, names) |
98 val tab_monos = foldl upd (InductiveData.get thy, names) |
495 |
492 |
496 (* inductive_cases(_i) *) |
493 (* inductive_cases(_i) *) |
497 |
494 |
498 fun gen_inductive_cases prep_att prep_const prep_prop |
495 fun gen_inductive_cases prep_att prep_const prep_prop |
499 ((((name, raw_atts), raw_set), raw_props), comment) thy = |
496 ((((name, raw_atts), raw_set), raw_props), comment) thy = |
500 let |
497 let val sign = Theory.sign_of thy; |
501 val sign = Theory.sign_of thy; |
498 in (case get_inductive thy (prep_const sign raw_set) of |
502 |
499 None => error ("Unknown (co)inductive set " ^ quote name) |
503 val atts = map (prep_att thy) raw_atts; |
500 | Some (_, {elims, ...}) => |
504 val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set); |
501 let |
505 val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; |
502 val atts = map (prep_att thy) raw_atts; |
506 val thms = map (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops; |
503 val cprops = map |
507 in |
504 (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; |
508 thy |
505 val thms = map |
509 |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment) |
506 (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops; |
|
507 in |
|
508 thy |> IsarThy.have_theorems_i |
|
509 (((name, atts), map Thm.no_attributes thms), comment) |
|
510 end) |
510 end; |
511 end; |
511 |
512 |
512 val inductive_cases = |
513 val inductive_cases = |
513 gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; |
514 gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; |
514 |
515 |