equal
deleted
inserted
replaced
27 signature INDUCTIVE_PACKAGE = |
27 signature INDUCTIVE_PACKAGE = |
28 sig |
28 sig |
29 (*Insert definitions for the recursive sets, which |
29 (*Insert definitions for the recursive sets, which |
30 must *already* be declared as constants in parent theory!*) |
30 must *already* be declared as constants in parent theory!*) |
31 val add_inductive_i: bool -> term list * term -> |
31 val add_inductive_i: bool -> term list * term -> |
32 ((bstring * term) * theory attribute list) list -> |
32 ((bstring * term) * attribute list) list -> |
33 thm list * thm list * thm list * thm list -> theory -> theory * inductive_result |
33 thm list * thm list * thm list * thm list -> theory -> theory * inductive_result |
34 val add_inductive: string list * string -> |
34 val add_inductive: string list * string -> |
35 ((bstring * string) * Attrib.src list) list -> |
35 ((bstring * string) * Attrib.src list) list -> |
36 (thmref * Attrib.src list) list * (thmref * Attrib.src list) list * |
36 (thmref * Attrib.src list) list * (thmref * Attrib.src list) list * |
37 (thmref * Attrib.src list) list * (thmref * Attrib.src list) list -> |
37 (thmref * Attrib.src list) list * (thmref * Attrib.src list) list -> |
513 and mutual_induct = CP.remove_split mutual_induct_fsplit |
513 and mutual_induct = CP.remove_split mutual_induct_fsplit |
514 |
514 |
515 val ([induct', mutual_induct'], thy') = |
515 val ([induct', mutual_induct'], thy') = |
516 thy |
516 thy |
517 |> PureThy.add_thms [((co_prefix ^ "induct", induct), |
517 |> PureThy.add_thms [((co_prefix ^ "induct", induct), |
518 [case_names, Attrib.theory (InductAttrib.induct_set big_rec_name)]), |
518 [case_names, InductAttrib.induct_set big_rec_name]), |
519 (("mutual_induct", mutual_induct), [case_names])]; |
519 (("mutual_induct", mutual_induct), [case_names])]; |
520 in ((thy', induct'), mutual_induct') |
520 in ((thy', induct'), mutual_induct') |
521 end; (*of induction_rules*) |
521 end; (*of induction_rules*) |
522 |
522 |
523 val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct) |
523 val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct) |
535 thy2 |
535 thy2 |
536 |> IndCases.declare big_rec_name make_cases |
536 |> IndCases.declare big_rec_name make_cases |
537 |> PureThy.add_thms |
537 |> PureThy.add_thms |
538 [(("bnd_mono", bnd_mono), []), |
538 [(("bnd_mono", bnd_mono), []), |
539 (("dom_subset", dom_subset), []), |
539 (("dom_subset", dom_subset), []), |
540 (("cases", elim), [case_names, Attrib.theory (InductAttrib.cases_set big_rec_name)])] |
540 (("cases", elim), [case_names, InductAttrib.cases_set big_rec_name])] |
541 ||>> (PureThy.add_thmss o map Thm.no_attributes) |
541 ||>> (PureThy.add_thmss o map Thm.no_attributes) |
542 [("defs", defs), |
542 [("defs", defs), |
543 ("intros", intrs)]; |
543 ("intros", intrs)]; |
544 val (intrs'', thy4) = |
544 val (intrs'', thy4) = |
545 thy3 |
545 thy3 |
559 |
559 |
560 (*source version*) |
560 (*source version*) |
561 fun add_inductive (srec_tms, sdom_sum) intr_srcs |
561 fun add_inductive (srec_tms, sdom_sum) intr_srcs |
562 (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy = |
562 (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy = |
563 let |
563 let |
564 val intr_atts = map (map (Attrib.global_attribute thy) o snd) intr_srcs; |
564 val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs; |
565 val sintrs = map fst intr_srcs ~~ intr_atts; |
565 val sintrs = map fst intr_srcs ~~ intr_atts; |
566 val read = Sign.simple_read_term thy; |
566 val read = Sign.simple_read_term thy; |
567 val rec_tms = map (read Ind_Syntax.iT) srec_tms; |
567 val rec_tms = map (read Ind_Syntax.iT) srec_tms; |
568 val dom_sum = read Ind_Syntax.iT sdom_sum; |
568 val dom_sum = read Ind_Syntax.iT sdom_sum; |
569 val intr_tms = map (read propT o snd o fst) sintrs; |
569 val intr_tms = map (read propT o snd o fst) sintrs; |