src/HOL/Tools/inductive_package.ML
changeset 11628 e57a6e51715e
parent 11502 e80a712982e1
child 11682 d9063229b4a1
equal deleted inserted replaced
11627:abf9cda4a4d2 11628:e57a6e51715e
    47   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    47   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    48     -> theory -> theory
    48     -> theory -> theory
    49   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    49   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    50     -> theory -> theory
    50     -> theory -> theory
    51   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    51   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    52     theory attribute list -> ((bstring * term) * theory attribute list) list ->
    52     ((bstring * term) * theory attribute list) list ->
    53       thm list -> thm list -> theory -> theory *
    53       thm list -> thm list -> theory -> theory *
    54       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    54       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    55        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    55        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    56   val add_inductive: bool -> bool -> string list -> Args.src list ->
    56   val add_inductive: bool -> bool -> string list ->
    57     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    57     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    58       (xstring * Args.src list) list -> theory -> theory *
    58       (xstring * Args.src list) list -> theory -> theory *
    59       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    59       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    60        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    60        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    61   val setup: (theory -> theory) list
    61   val setup: (theory -> theory) list
   739     val mono = prove_mono setT fp_fun monos thy'
   739     val mono = prove_mono setT fp_fun monos thy'
   740 
   740 
   741   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   741   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   742 
   742 
   743 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   743 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   744     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   744     intros monos con_defs thy params paramTs cTs cnames induct_cases =
   745   let
   745   let
   746     val _ =
   746     val _ =
   747       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   747       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   748         commas_quote cnames) else ();
   748         commas_quote cnames) else ();
   749 
   749 
   770     val (thy2, intrs') =
   770     val (thy2, intrs') =
   771       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   771       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   772     val (thy3, ([intrs'', elims'], [induct'])) =
   772     val (thy3, ([intrs'', elims'], [induct'])) =
   773       thy2
   773       thy2
   774       |> PureThy.add_thmss
   774       |> PureThy.add_thmss
   775         [(("intros", intrs'), atts),
   775         [(("intros", intrs'), []),
   776           (("elims", elims), [RuleCases.consumes 1])]
   776           (("elims", elims), [RuleCases.consumes 1])]
   777       |>>> PureThy.add_thms
   777       |>>> PureThy.add_thms
   778         [((coind_prefix coind ^ "induct", rulify induct),
   778         [((coind_prefix coind ^ "induct", rulify induct),
   779          [RuleCases.case_names induct_cases,
   779          [RuleCases.case_names induct_cases,
   780           RuleCases.consumes 1])]
   780           RuleCases.consumes 1])]
   797   (case Library.try f t of
   797   (case Library.try f t of
   798     Some x => x
   798     Some x => x
   799   | None => error (msg ^ Sign.string_of_term sign t));
   799   | None => error (msg ^ Sign.string_of_term sign t));
   800 
   800 
   801 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   801 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   802     atts pre_intros monos con_defs thy =
   802     pre_intros monos con_defs thy =
   803   let
   803   let
   804     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   804     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   805     val sign = Theory.sign_of thy;
   805     val sign = Theory.sign_of thy;
   806 
   806 
   807     (*parameters should agree for all mutually recursive components*)
   807     (*parameters should agree for all mutually recursive components*)
   820       thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   820       thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   821     val intros = map (check_rule save_sign cs) pre_intros;
   821     val intros = map (check_rule save_sign cs) pre_intros;
   822     val induct_cases = map (#1 o #1) intros;
   822     val induct_cases = map (#1 o #1) intros;
   823 
   823 
   824     val (thy1, result as {elims, induct, ...}) =
   824     val (thy1, result as {elims, induct, ...}) =
   825       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   825       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
   826         con_defs thy params paramTs cTs cnames induct_cases;
   826         con_defs thy params paramTs cTs cnames induct_cases;
   827     val thy2 = thy1
   827     val thy2 = thy1
   828       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   828       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   829       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
   829       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
   830   in (thy2, result) end;
   830   in (thy2, result) end;
   831 
   831 
   832 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   832 fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
   833   let
   833   let
   834     val sign = Theory.sign_of thy;
   834     val sign = Theory.sign_of thy;
   835     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   835     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   836 
   836 
   837     val atts = map (Attrib.global_attribute thy) srcs;
       
   838     val intr_names = map (fst o fst) intro_srcs;
   837     val intr_names = map (fst o fst) intro_srcs;
   839     fun read_rule s = Thm.read_cterm sign (s, propT)
   838     fun read_rule s = Thm.read_cterm sign (s, propT)
   840       handle ERROR => error ("The error(s) above occurred for " ^ s);
   839       handle ERROR => error ("The error(s) above occurred for " ^ s);
   841     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   840     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   842     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   841     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   845     val ((thy', con_defs), monos) = thy
   844     val ((thy', con_defs), monos) = thy
   846       |> IsarThy.apply_theorems raw_monos
   845       |> IsarThy.apply_theorems raw_monos
   847       |> apfst (IsarThy.apply_theorems raw_con_defs);
   846       |> apfst (IsarThy.apply_theorems raw_con_defs);
   848   in
   847   in
   849     add_inductive_i verbose false "" coind false false cs'
   848     add_inductive_i verbose false "" coind false false cs'
   850       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   849       ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   851   end;
   850   end;
   852 
   851 
   853 
   852 
   854 
   853 
   855 (** package setup **)
   854 (** package setup **)
   865 
   864 
   866 (* outer syntax *)
   865 (* outer syntax *)
   867 
   866 
   868 local structure P = OuterParse and K = OuterSyntax.Keyword in
   867 local structure P = OuterParse and K = OuterSyntax.Keyword in
   869 
   868 
   870 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   869 fun mk_ind coind (((sets, intrs), monos), con_defs) =
   871   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
   870   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos con_defs;
   872 
   871 
   873 fun ind_decl coind =
   872 fun ind_decl coind =
   874   (Scan.repeat1 P.term --| P.marg_comment) --
   873   (Scan.repeat1 P.term --| P.marg_comment) --
   875   (P.$$$ "intros" |--
   874   (P.$$$ "intros" |--
   876     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   875     P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   877   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   876   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   878   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   877   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   879   >> (Toplevel.theory o mk_ind coind);
   878   >> (Toplevel.theory o mk_ind coind);
   880 
   879 
   881 val inductiveP =
   880 val inductiveP =