tuned internal interfaces: flags record, added kind for results;
authorwenzelm
Tue Oct 02 22:23:26 2007 +0200 (2007-10-02)
changeset 24815f7093e90f36c
parent 24814 0384f48a806e
child 24816 2d0fa8f31804
tuned internal interfaces: flags record, added kind for results;
tuned;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Oct 02 22:23:24 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 02 22:23:26 2007 +0200
     1.3 @@ -38,7 +38,8 @@
     1.4      Proof.context -> thm list list * local_theory
     1.5    val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
     1.6      Proof.context -> thm list list * local_theory
     1.7 -  val add_inductive_i: bool -> bstring -> bool -> bool -> bool ->
     1.8 +  val add_inductive_i:
     1.9 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.10      ((string * typ) * mixfix) list ->
    1.11      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.12        local_theory -> inductive_result * local_theory
    1.13 @@ -46,7 +47,8 @@
    1.14      (string * string option * mixfix) list ->
    1.15      ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
    1.16      local_theory -> inductive_result * local_theory
    1.17 -  val add_inductive_global: bool -> bstring -> bool -> bool -> bool ->
    1.18 +  val add_inductive_global:
    1.19 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.20      ((string * typ) * mixfix) list -> (string * typ) list ->
    1.21      ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
    1.22    val arities_of: thm -> (string * int) list
    1.23 @@ -61,12 +63,12 @@
    1.24  sig
    1.25    include BASIC_INDUCTIVE_PACKAGE
    1.26    type add_ind_def
    1.27 -  val declare_rules: bstring -> bool -> bool -> string list ->
    1.28 +  val declare_rules: string -> bstring -> bool -> bool -> string list ->
    1.29      thm list -> bstring list -> Attrib.src list list -> (thm * string list) list ->
    1.30      thm -> local_theory -> thm list * thm list * thm * local_theory
    1.31    val add_ind_def: add_ind_def
    1.32    val gen_add_inductive_i: add_ind_def ->
    1.33 -    bool -> bstring -> bool -> bool -> bool ->
    1.34 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.35      ((string * typ) * mixfix) list ->
    1.36      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.37        local_theory -> inductive_result * local_theory
    1.38 @@ -86,10 +88,6 @@
    1.39  
    1.40  (** theory context references **)
    1.41  
    1.42 -val mono_name = "Orderings.mono";
    1.43 -val gfp_name = "FixedPoint.gfp";
    1.44 -val lfp_name = "FixedPoint.lfp";
    1.45 -
    1.46  val inductive_forall_name = "HOL.induct_forall";
    1.47  val inductive_forall_def = thm "induct_forall_def";
    1.48  val inductive_conj_name = "HOL.induct_conj";
    1.49 @@ -198,9 +196,6 @@
    1.50  fun message s = if ! quiet_mode then () else writeln s;
    1.51  fun clean_message s = if ! quick_and_dirty then () else message s;
    1.52  
    1.53 -val note_theorems = LocalTheory.notes Thm.theoremK;
    1.54 -val note_theorem = LocalTheory.note Thm.theoremK;
    1.55 -
    1.56  fun coind_prefix true = "co"
    1.57    | coind_prefix false = "";
    1.58  
    1.59 @@ -325,7 +320,7 @@
    1.60   (message "  Proving monotonicity ...";
    1.61    Goal.prove ctxt [] []   (*NO quick_and_dirty here!*)
    1.62      (HOLogic.mk_Trueprop
    1.63 -      (Const (mono_name, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    1.64 +      (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    1.65      (fn _ => EVERY [rtac monoI 1,
    1.66        REPEAT (resolve_tac [le_funI, le_boolI'] 1),
    1.67        REPEAT (FIRST
    1.68 @@ -462,7 +457,7 @@
    1.69      val facts = args |> map (fn ((a, atts), props) =>
    1.70        ((a, map (prep_att thy) atts),
    1.71          map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
    1.72 -  in lthy |> note_theorems facts |>> map snd end;
    1.73 +  in lthy |> LocalTheory.notes Thm.theoremK facts |>> map snd end;
    1.74  
    1.75  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    1.76  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    1.77 @@ -594,7 +589,7 @@
    1.78  fun mk_ind_def alt_name coind cs intr_ts monos
    1.79        params cnames_syn ctxt =
    1.80    let
    1.81 -    val fp_name = if coind then gfp_name else lfp_name;
    1.82 +    val fp_name = if coind then @{const_name FixedPoint.gfp} else @{const_name FixedPoint.lfp};
    1.83  
    1.84      val argTs = fold (fn c => fn Ts => Ts @
    1.85        (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];
    1.86 @@ -676,7 +671,7 @@
    1.87      list_comb (rec_const, params), preds, argTs, bs, xs)
    1.88    end;
    1.89  
    1.90 -fun declare_rules rec_name coind no_ind cnames intrs intr_names intr_atts
    1.91 +fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts
    1.92        elims raw_induct ctxt =
    1.93    let
    1.94      val ind_case_names = RuleCases.case_names intr_names;
    1.95 @@ -691,29 +686,29 @@
    1.96  
    1.97      val (intrs', ctxt1) =
    1.98        ctxt |>
    1.99 -      note_theorems
   1.100 +      LocalTheory.notes kind
   1.101          (map (NameSpace.qualified rec_name) intr_names ~~
   1.102           intr_atts ~~ map (fn th => [([th],
   1.103             [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
   1.104        map (hd o snd);
   1.105      val (((_, elims'), (_, [induct'])), ctxt2) =
   1.106        ctxt1 |>
   1.107 -      note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
   1.108 +      LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
   1.109        fold_map (fn (name, (elim, cases)) =>
   1.110 -        note_theorem ((NameSpace.qualified (Sign.base_name name) "cases",
   1.111 +        LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
   1.112            [Attrib.internal (K (RuleCases.case_names cases)),
   1.113             Attrib.internal (K (RuleCases.consumes 1)),
   1.114             Attrib.internal (K (InductAttrib.cases_set name)),
   1.115             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
   1.116          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
   1.117 -      note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
   1.118 +      LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
   1.119          map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   1.120  
   1.121      val ctxt3 = if no_ind orelse coind then ctxt2 else
   1.122        let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
   1.123        in
   1.124          ctxt2 |>
   1.125 -        note_theorems [((NameSpace.qualified rec_name "inducts", []),
   1.126 +        LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []),
   1.127            inducts |> map (fn (name, th) => ([th],
   1.128              [Attrib.internal (K ind_case_names),
   1.129               Attrib.internal (K (RuleCases.consumes 1)),
   1.130 @@ -721,13 +716,14 @@
   1.131        end
   1.132    in (intrs', elims', induct', ctxt3) end;
   1.133  
   1.134 -type add_ind_def = bool -> bstring -> bool -> bool -> bool ->
   1.135 +type add_ind_def =
   1.136 +  {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
   1.137    term list -> ((string * Attrib.src list) * term) list -> thm list ->
   1.138    term list -> (string * mixfix) list ->
   1.139    local_theory -> inductive_result * local_theory
   1.140  
   1.141 -fun add_ind_def verbose alt_name coind no_elim no_ind cs
   1.142 -    intros monos params cnames_syn ctxt =
   1.143 +fun add_ind_def {verbose, kind, alt_name, coind, no_elim, no_ind}
   1.144 +    cs intros monos params cnames_syn ctxt =
   1.145    let
   1.146      val _ =
   1.147        if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
   1.148 @@ -757,7 +753,7 @@
   1.149           prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def
   1.150             rec_preds_defs ctxt1);
   1.151  
   1.152 -    val (intrs', elims', induct, ctxt2) = declare_rules rec_name coind no_ind
   1.153 +    val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
   1.154        cnames intrs intr_names intr_atts elims raw_induct ctxt1;
   1.155  
   1.156      val names = map #1 cnames_syn;
   1.157 @@ -780,7 +776,7 @@
   1.158  
   1.159  (* external interfaces *)
   1.160  
   1.161 -fun gen_add_inductive_i mk_def verbose alt_name coind no_elim no_ind
   1.162 +fun gen_add_inductive_i mk_def (flags as {verbose, kind, alt_name, coind, no_elim, no_ind})
   1.163      cnames_syn pnames pre_intros monos ctxt =
   1.164    let
   1.165      val thy = ProofContext.theory_of ctxt;
   1.166 @@ -831,10 +827,9 @@
   1.167  
   1.168      val intros = map (close_rule ##> expand abbrevs') pre_intros';
   1.169    in
   1.170 -    ctxt |>
   1.171 -    mk_def verbose alt_name coind no_elim no_ind cs intros monos
   1.172 -      params cnames_syn'' ||>
   1.173 -    fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs''
   1.174 +    ctxt
   1.175 +    |> mk_def flags cs intros monos params cnames_syn''
   1.176 +    ||> fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs''
   1.177    end;
   1.178  
   1.179  fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
   1.180 @@ -844,14 +839,16 @@
   1.181      val (cs, ps) = chop (length cnames_syn) vars;
   1.182      val intrs = map (apsnd the_single) specs;
   1.183      val monos = Attrib.eval_thms lthy raw_monos;
   1.184 -  in gen_add_inductive_i mk_def verbose "" coind false false cs (map fst ps) intrs monos lthy end;
   1.185 +    val flags = {verbose = verbose, kind = Thm.theoremK, alt_name = "",
   1.186 +      coind = coind, no_elim = false, no_ind = false};
   1.187 +  in gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos lthy end;
   1.188  
   1.189  val add_inductive_i = gen_add_inductive_i add_ind_def;
   1.190  val add_inductive = gen_add_inductive add_ind_def;
   1.191  
   1.192 -fun add_inductive_global verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos =
   1.193 +fun add_inductive_global flags cnames_syn pnames pre_intros monos =
   1.194    TheoryTarget.init NONE #>
   1.195 -  add_inductive_i verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos #>
   1.196 +  add_inductive_i flags cnames_syn pnames pre_intros monos #>
   1.197    (fn (_, lthy) =>
   1.198      (#2 (the_inductive (LocalTheory.target_of lthy)
   1.199        (LocalTheory.target_name lthy (fst (fst (hd cnames_syn))))),
     2.1 --- a/src/HOL/Tools/inductive_set_package.ML	Tue Oct 02 22:23:24 2007 +0200
     2.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Tue Oct 02 22:23:26 2007 +0200
     2.3 @@ -11,7 +11,8 @@
     2.4    val to_set_att: thm list -> attribute
     2.5    val to_pred_att: thm list -> attribute
     2.6    val pred_set_conv_att: attribute
     2.7 -  val add_inductive_i: bool -> bstring -> bool -> bool -> bool ->
     2.8 +  val add_inductive_i:
     2.9 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    2.10      ((string * typ) * mixfix) list ->
    2.11      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    2.12        local_theory -> InductivePackage.inductive_result * local_theory
    2.13 @@ -25,13 +26,8 @@
    2.14  structure InductiveSetPackage: INDUCTIVE_SET_PACKAGE =
    2.15  struct
    2.16  
    2.17 -val note_theorem = LocalTheory.note Thm.theoremK;
    2.18 -
    2.19 -
    2.20  (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
    2.21  
    2.22 -val subset_antisym = thm "subset_antisym";
    2.23 -
    2.24  val collect_mem_simproc =
    2.25    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
    2.26      fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
    2.27 @@ -50,7 +46,7 @@
    2.28                        SOME (Goal.prove (Simplifier.the_context ss) [] []
    2.29                          (Const ("==", T --> T --> propT) $ S $ S')
    2.30                          (K (EVERY
    2.31 -                          [rtac eq_reflection 1, rtac subset_antisym 1,
    2.32 +                          [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
    2.33                             rtac subsetI 1, dtac CollectD 1, simp,
    2.34                             rtac subsetI 1, rtac CollectI 1, simp])))
    2.35                      end
    2.36 @@ -403,8 +399,8 @@
    2.37  
    2.38  (**** definition of inductive sets ****)
    2.39  
    2.40 -fun add_ind_set_def verbose alt_name coind no_elim no_ind cs
    2.41 -    intros monos params cnames_syn ctxt =
    2.42 +fun add_ind_set_def {verbose, kind, alt_name, coind, no_elim, no_ind}
    2.43 +    cs intros monos params cnames_syn ctxt =
    2.44    let
    2.45      val thy = ProofContext.theory_of ctxt;
    2.46      val {set_arities, pred_arities, to_pred_simps, ...} =
    2.47 @@ -466,8 +462,10 @@
    2.48      val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn;
    2.49      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
    2.50      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    2.51 -      InductivePackage.add_ind_def verbose "" coind
    2.52 -        no_elim no_ind cs' intros' monos' params1 cnames_syn' ctxt;
    2.53 +      InductivePackage.add_ind_def {verbose = verbose, kind = kind,
    2.54 +          alt_name = "",  (* FIXME pass alt_name (!?) *)
    2.55 +          coind = coind, no_elim = no_elim, no_ind = no_ind}
    2.56 +        cs' intros' monos' params1 cnames_syn' ctxt;
    2.57  
    2.58      (* define inductive sets using previously defined predicates *)
    2.59      val (defs, ctxt2) = LocalTheory.defs Thm.internalK
    2.60 @@ -489,7 +487,7 @@
    2.61              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
    2.62                [def, mem_Collect_eq, split_conv]) 1))
    2.63          in
    2.64 -          ctxt |> note_theorem ((s ^ "p_" ^ s ^ "_eq",
    2.65 +          ctxt |> LocalTheory.note kind ((s ^ "p_" ^ s ^ "_eq",
    2.66              [Attrib.internal (K pred_set_conv_att)]),
    2.67                [conv_thm]) |> snd
    2.68          end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
    2.69 @@ -501,7 +499,7 @@
    2.70      val (intr_names, intr_atts) = split_list (map fst intros);
    2.71      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
    2.72      val (intrs', elims', induct, ctxt4) =
    2.73 -      InductivePackage.declare_rules rec_name coind no_ind cnames
    2.74 +      InductivePackage.declare_rules kind rec_name coind no_ind cnames
    2.75        (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
    2.76        (map (fn th => (to_set [] (Context.Proof ctxt3) th,
    2.77           map fst (fst (RuleCases.get th)))) elims)