inductive: eliminated obsolete kind;
authorwenzelm
Fri Nov 13 19:57:46 2009 +0100 (2009-11-13)
changeset 33669ae9a2ea9a989
parent 33668 090288424d44
child 33670 02b7738aef6a
inductive: eliminated obsolete kind;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -569,9 +569,8 @@
     1.4        thy3
     1.5        |> Sign.map_naming Name_Space.conceal
     1.6        |> Inductive.add_inductive_global (serial ())
     1.7 -          {quiet_mode = false, verbose = false, kind = "",
     1.8 -           alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
     1.9 -           skip_mono = true, fork_mono = false}
    1.10 +          {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
    1.11 +           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
    1.12            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    1.13               (rep_set_names' ~~ recTs'))
    1.14            [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    1.15 @@ -1513,9 +1512,8 @@
    1.16        thy10
    1.17        |> Sign.map_naming Name_Space.conceal
    1.18        |> Inductive.add_inductive_global (serial ())
    1.19 -          {quiet_mode = #quiet config, verbose = false, kind = "",
    1.20 -           alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
    1.21 -           skip_mono = true, fork_mono = false}
    1.22 +          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    1.23 +           coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
    1.24            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.25            (map dest_Free rec_fns)
    1.26            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
     2.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 17:15:35 2009 +0000
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 19:57:46 2009 +0100
     2.3 @@ -156,9 +156,8 @@
     2.4        thy0
     2.5        |> Sign.map_naming Name_Space.conceal
     2.6        |> Inductive.add_inductive_global (serial ())
     2.7 -          {quiet_mode = #quiet config, verbose = false, kind = "",
     2.8 -            alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
     2.9 -            skip_mono = true, fork_mono = false}
    2.10 +          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
    2.11 +            coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
    2.12            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    2.13            (map dest_Free rec_fns)
    2.14            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
     3.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 17:15:35 2009 +0000
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 19:57:46 2009 +0100
     3.3 @@ -175,9 +175,8 @@
     3.4        thy1
     3.5        |> Sign.map_naming Name_Space.conceal
     3.6        |> Inductive.add_inductive_global (serial ())
     3.7 -          {quiet_mode = #quiet config, verbose = false, kind = "",
     3.8 -           alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
     3.9 -           skip_mono = true, fork_mono = false}
    3.10 +          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    3.11 +           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
    3.12            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
    3.13            (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    3.14        ||> Sign.restore_naming thy1
     4.1 --- a/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 17:15:35 2009 +0000
     4.2 +++ b/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 19:57:46 2009 +0100
     4.3 @@ -460,7 +460,6 @@
     4.4        |> Inductive.add_inductive_i
     4.5            {quiet_mode = true,
     4.6              verbose = ! trace,
     4.7 -            kind = "",
     4.8              alt_name = Binding.empty,
     4.9              coind = false,
    4.10              no_elim = false,
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 17:15:35 2009 +0000
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 19:57:46 2009 +0100
     5.3 @@ -355,9 +355,8 @@
     5.4                thy
     5.5                |> Sign.map_naming Name_Space.conceal
     5.6                |> Inductive.add_inductive_global (serial ())
     5.7 -                {quiet_mode = false, verbose = false, kind = "",
     5.8 -                  alt_name = Binding.empty, coind = false, no_elim = false,
     5.9 -                  no_ind = false, skip_mono = false, fork_mono = false}
    5.10 +                {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
    5.11 +                  no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    5.12                  (map (fn (s, T) =>
    5.13                    ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
    5.14                  pnames
     6.1 --- a/src/HOL/Tools/inductive.ML	Fri Nov 13 17:15:35 2009 +0000
     6.2 +++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 19:57:46 2009 +0100
     6.3 @@ -39,8 +39,8 @@
     6.4    val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
     6.5      thm list list * local_theory
     6.6    type inductive_flags =
     6.7 -    {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
     6.8 -     coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
     6.9 +    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
    6.10 +      no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
    6.11    val add_inductive_i:
    6.12      inductive_flags -> ((binding * typ) * mixfix) list ->
    6.13      (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
    6.14 @@ -71,7 +71,7 @@
    6.15      term list -> (Attrib.binding * term) list -> thm list ->
    6.16      term list -> (binding * mixfix) list ->
    6.17      local_theory -> inductive_result * local_theory
    6.18 -  val declare_rules: string -> binding -> bool -> bool -> string list ->
    6.19 +  val declare_rules: binding -> bool -> bool -> string list ->
    6.20      thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
    6.21      thm -> local_theory -> thm list * thm list * thm * local_theory
    6.22    val add_ind_def: add_ind_def
    6.23 @@ -509,7 +509,8 @@
    6.24  
    6.25      fun mk_ind_prem r =
    6.26        let
    6.27 -        fun subst s = (case dest_predicate cs params s of
    6.28 +        fun subst s =
    6.29 +          (case dest_predicate cs params s of
    6.30              SOME (_, i, ys, (_, Ts)) =>
    6.31                let
    6.32                  val k = length Ts;
    6.33 @@ -520,10 +521,11 @@
    6.34                    HOLogic.mk_binop inductive_conj_name
    6.35                      (list_comb (incr_boundvars k s, bs), P))
    6.36                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
    6.37 -          | NONE => (case s of
    6.38 -              (t $ u) => (fst (subst t) $ fst (subst u), NONE)
    6.39 -            | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
    6.40 -            | _ => (s, NONE)));
    6.41 +          | NONE =>
    6.42 +              (case s of
    6.43 +                (t $ u) => (fst (subst t) $ fst (subst u), NONE)
    6.44 +              | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
    6.45 +              | _ => (s, NONE)));
    6.46  
    6.47          fun mk_prem s prems =
    6.48            (case subst s of
    6.49 @@ -618,16 +620,17 @@
    6.50          SOME (_, i, ts, (Ts, Us)) =>
    6.51            let
    6.52              val l = length Us;
    6.53 -            val zs = map Bound (l - 1 downto 0)
    6.54 +            val zs = map Bound (l - 1 downto 0);
    6.55            in
    6.56              list_abs (map (pair "z") Us, list_comb (p,
    6.57                make_bool_args' bs i @ make_args argTs
    6.58                  ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
    6.59            end
    6.60 -      | NONE => (case t of
    6.61 -          t1 $ t2 => subst t1 $ subst t2
    6.62 -        | Abs (x, T, u) => Abs (x, T, subst u)
    6.63 -        | _ => t));
    6.64 +      | NONE =>
    6.65 +          (case t of
    6.66 +            t1 $ t2 => subst t1 $ subst t2
    6.67 +          | Abs (x, T, u) => Abs (x, T, subst u)
    6.68 +          | _ => t));
    6.69  
    6.70      (* transform an introduction rule into a conjunction  *)
    6.71      (*   [| p_i t; ... |] ==> p_j u                       *)
    6.72 @@ -698,8 +701,8 @@
    6.73      list_comb (rec_const, params), preds, argTs, bs, xs)
    6.74    end;
    6.75  
    6.76 -fun declare_rules kind rec_binding coind no_ind cnames
    6.77 -      intrs intr_bindings intr_atts elims raw_induct lthy =
    6.78 +fun declare_rules rec_binding coind no_ind cnames
    6.79 +    intrs intr_bindings intr_atts elims raw_induct lthy =
    6.80    let
    6.81      val rec_name = Binding.name_of rec_binding;
    6.82      fun rec_qualified qualified = Binding.qualify qualified rec_name;
    6.83 @@ -716,7 +719,7 @@
    6.84  
    6.85      val (intrs', lthy1) =
    6.86        lthy |>
    6.87 -      LocalTheory.notes kind
    6.88 +      LocalTheory.notes ""
    6.89          (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
    6.90            map (fn th => [([th],
    6.91             [Attrib.internal (K (Context_Rules.intro_query NONE)),
    6.92 @@ -724,16 +727,16 @@
    6.93        map (hd o snd);
    6.94      val (((_, elims'), (_, [induct'])), lthy2) =
    6.95        lthy1 |>
    6.96 -      LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    6.97 +      LocalTheory.note "" ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    6.98        fold_map (fn (name, (elim, cases)) =>
    6.99 -        LocalTheory.note kind
   6.100 +        LocalTheory.note ""
   6.101            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
   6.102              [Attrib.internal (K (Rule_Cases.case_names cases)),
   6.103               Attrib.internal (K (Rule_Cases.consumes 1)),
   6.104               Attrib.internal (K (Induct.cases_pred name)),
   6.105               Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
   6.106          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
   6.107 -      LocalTheory.note kind
   6.108 +      LocalTheory.note ""
   6.109          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
   6.110            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   6.111  
   6.112 @@ -742,7 +745,7 @@
   6.113        else
   6.114          let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
   6.115            lthy2 |>
   6.116 -          LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
   6.117 +          LocalTheory.notes "" [((rec_qualified true (Binding.name "inducts"), []),
   6.118              inducts |> map (fn (name, th) => ([th],
   6.119                [Attrib.internal (K ind_case_names),
   6.120                 Attrib.internal (K (Rule_Cases.consumes 1)),
   6.121 @@ -751,8 +754,8 @@
   6.122    in (intrs', elims', induct', lthy3) end;
   6.123  
   6.124  type inductive_flags =
   6.125 -  {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
   6.126 -   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
   6.127 +  {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
   6.128 +    no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
   6.129  
   6.130  type add_ind_def =
   6.131    inductive_flags ->
   6.132 @@ -760,8 +763,7 @@
   6.133    term list -> (binding * mixfix) list ->
   6.134    local_theory -> inductive_result * local_theory;
   6.135  
   6.136 -fun add_ind_def
   6.137 -    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
   6.138 +fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
   6.139      cs intros monos params cnames_syn lthy =
   6.140    let
   6.141      val _ = null cnames_syn andalso error "No inductive predicates given";
   6.142 @@ -797,7 +799,7 @@
   6.143           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   6.144             rec_preds_defs lthy1);
   6.145  
   6.146 -    val (intrs', elims', induct, lthy2) = declare_rules kind rec_name coind no_ind
   6.147 +    val (intrs', elims', induct, lthy2) = declare_rules rec_name coind no_ind
   6.148        cnames intrs intr_names intr_atts elims raw_induct lthy1;
   6.149  
   6.150      val result =
   6.151 @@ -817,7 +819,7 @@
   6.152  (* external interfaces *)
   6.153  
   6.154  fun gen_add_inductive_i mk_def
   6.155 -    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
   6.156 +    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
   6.157      cnames_syn pnames spec monos lthy =
   6.158    let
   6.159      val thy = ProofContext.theory_of lthy;
   6.160 @@ -880,9 +882,8 @@
   6.161        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
   6.162      val (cs, ps) = chop (length cnames_syn) vars;
   6.163      val monos = Attrib.eval_thms lthy raw_monos;
   6.164 -    val flags = {quiet_mode = false, verbose = verbose, kind = "",
   6.165 -      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
   6.166 -      skip_mono = false, fork_mono = not int};
   6.167 +    val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
   6.168 +      coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
   6.169    in
   6.170      lthy
   6.171      |> LocalTheory.set_group (serial ())
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 17:15:35 2009 +0000
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 19:57:46 2009 +0100
     7.3 @@ -351,8 +351,8 @@
     7.4  
     7.5      val (ind_info, thy3') = thy2 |>
     7.6        Inductive.add_inductive_global (serial ())
     7.7 -        {quiet_mode = false, verbose = false, kind = "", alt_name = Binding.empty,
     7.8 -          coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
     7.9 +        {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
    7.10 +          no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    7.11          rlzpreds rlzparams (map (fn (rintr, intr) =>
    7.12            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
    7.13             subst_atomic rlzpreds' (Logic.unvarify rintr)))
     8.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 17:15:35 2009 +0000
     8.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 19:57:46 2009 +0100
     8.3 @@ -224,7 +224,7 @@
     8.4    map (fn (x, ps) =>
     8.5      let
     8.6        val U = HOLogic.dest_setT (fastype_of x);
     8.7 -      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
     8.8 +      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
     8.9      in
    8.10        (cterm_of thy x,
    8.11         cterm_of thy (HOLogic.Collect_const U $
    8.12 @@ -405,7 +405,7 @@
    8.13  (**** definition of inductive sets ****)
    8.14  
    8.15  fun add_ind_set_def
    8.16 -    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    8.17 +    {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    8.18      cs intros monos params cnames_syn lthy =
    8.19    let
    8.20      val thy = ProofContext.theory_of lthy;
    8.21 @@ -477,7 +477,7 @@
    8.22      val monos' = map (to_pred [] (Context.Proof lthy)) monos;
    8.23      val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
    8.24        Inductive.add_ind_def
    8.25 -        {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
    8.26 +        {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
    8.27            coind = coind, no_elim = no_elim, no_ind = no_ind,
    8.28            skip_mono = skip_mono, fork_mono = fork_mono}
    8.29          cs' intros' monos' params1 cnames_syn' lthy;
    8.30 @@ -505,7 +505,7 @@
    8.31              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
    8.32                [def, mem_Collect_eq, split_conv]) 1))
    8.33          in
    8.34 -          lthy |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    8.35 +          lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    8.36              [Attrib.internal (K pred_set_conv_att)]),
    8.37                [conv_thm]) |> snd
    8.38          end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
    8.39 @@ -519,7 +519,7 @@
    8.40      val (intr_names, intr_atts) = split_list (map fst intros);
    8.41      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
    8.42      val (intrs', elims', induct, lthy4) =
    8.43 -      Inductive.declare_rules kind rec_name coind no_ind cnames
    8.44 +      Inductive.declare_rules rec_name coind no_ind cnames
    8.45          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    8.46          (map (fn th => (to_set [] (Context.Proof lthy3) th,
    8.47             map fst (fst (Rule_Cases.get th)))) elims)