src/HOL/Tools/inductive.ML
changeset 33669 ae9a2ea9a989
parent 33666 e49bfeb0d822
child 33670 02b7738aef6a
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -39,8 +39,8 @@
     1.4    val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
     1.5      thm list list * local_theory
     1.6    type inductive_flags =
     1.7 -    {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
     1.8 -     coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
     1.9 +    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
    1.10 +      no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
    1.11    val add_inductive_i:
    1.12      inductive_flags -> ((binding * typ) * mixfix) list ->
    1.13      (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
    1.14 @@ -71,7 +71,7 @@
    1.15      term list -> (Attrib.binding * term) list -> thm list ->
    1.16      term list -> (binding * mixfix) list ->
    1.17      local_theory -> inductive_result * local_theory
    1.18 -  val declare_rules: string -> binding -> bool -> bool -> string list ->
    1.19 +  val declare_rules: binding -> bool -> bool -> string list ->
    1.20      thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
    1.21      thm -> local_theory -> thm list * thm list * thm * local_theory
    1.22    val add_ind_def: add_ind_def
    1.23 @@ -509,7 +509,8 @@
    1.24  
    1.25      fun mk_ind_prem r =
    1.26        let
    1.27 -        fun subst s = (case dest_predicate cs params s of
    1.28 +        fun subst s =
    1.29 +          (case dest_predicate cs params s of
    1.30              SOME (_, i, ys, (_, Ts)) =>
    1.31                let
    1.32                  val k = length Ts;
    1.33 @@ -520,10 +521,11 @@
    1.34                    HOLogic.mk_binop inductive_conj_name
    1.35                      (list_comb (incr_boundvars k s, bs), P))
    1.36                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
    1.37 -          | NONE => (case s of
    1.38 -              (t $ u) => (fst (subst t) $ fst (subst u), NONE)
    1.39 -            | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
    1.40 -            | _ => (s, NONE)));
    1.41 +          | NONE =>
    1.42 +              (case s of
    1.43 +                (t $ u) => (fst (subst t) $ fst (subst u), NONE)
    1.44 +              | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
    1.45 +              | _ => (s, NONE)));
    1.46  
    1.47          fun mk_prem s prems =
    1.48            (case subst s of
    1.49 @@ -618,16 +620,17 @@
    1.50          SOME (_, i, ts, (Ts, Us)) =>
    1.51            let
    1.52              val l = length Us;
    1.53 -            val zs = map Bound (l - 1 downto 0)
    1.54 +            val zs = map Bound (l - 1 downto 0);
    1.55            in
    1.56              list_abs (map (pair "z") Us, list_comb (p,
    1.57                make_bool_args' bs i @ make_args argTs
    1.58                  ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
    1.59            end
    1.60 -      | NONE => (case t of
    1.61 -          t1 $ t2 => subst t1 $ subst t2
    1.62 -        | Abs (x, T, u) => Abs (x, T, subst u)
    1.63 -        | _ => t));
    1.64 +      | NONE =>
    1.65 +          (case t of
    1.66 +            t1 $ t2 => subst t1 $ subst t2
    1.67 +          | Abs (x, T, u) => Abs (x, T, subst u)
    1.68 +          | _ => t));
    1.69  
    1.70      (* transform an introduction rule into a conjunction  *)
    1.71      (*   [| p_i t; ... |] ==> p_j u                       *)
    1.72 @@ -698,8 +701,8 @@
    1.73      list_comb (rec_const, params), preds, argTs, bs, xs)
    1.74    end;
    1.75  
    1.76 -fun declare_rules kind rec_binding coind no_ind cnames
    1.77 -      intrs intr_bindings intr_atts elims raw_induct lthy =
    1.78 +fun declare_rules rec_binding coind no_ind cnames
    1.79 +    intrs intr_bindings intr_atts elims raw_induct lthy =
    1.80    let
    1.81      val rec_name = Binding.name_of rec_binding;
    1.82      fun rec_qualified qualified = Binding.qualify qualified rec_name;
    1.83 @@ -716,7 +719,7 @@
    1.84  
    1.85      val (intrs', lthy1) =
    1.86        lthy |>
    1.87 -      LocalTheory.notes kind
    1.88 +      LocalTheory.notes ""
    1.89          (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
    1.90            map (fn th => [([th],
    1.91             [Attrib.internal (K (Context_Rules.intro_query NONE)),
    1.92 @@ -724,16 +727,16 @@
    1.93        map (hd o snd);
    1.94      val (((_, elims'), (_, [induct'])), lthy2) =
    1.95        lthy1 |>
    1.96 -      LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    1.97 +      LocalTheory.note "" ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    1.98        fold_map (fn (name, (elim, cases)) =>
    1.99 -        LocalTheory.note kind
   1.100 +        LocalTheory.note ""
   1.101            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
   1.102              [Attrib.internal (K (Rule_Cases.case_names cases)),
   1.103               Attrib.internal (K (Rule_Cases.consumes 1)),
   1.104               Attrib.internal (K (Induct.cases_pred name)),
   1.105               Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
   1.106          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
   1.107 -      LocalTheory.note kind
   1.108 +      LocalTheory.note ""
   1.109          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
   1.110            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   1.111  
   1.112 @@ -742,7 +745,7 @@
   1.113        else
   1.114          let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
   1.115            lthy2 |>
   1.116 -          LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
   1.117 +          LocalTheory.notes "" [((rec_qualified true (Binding.name "inducts"), []),
   1.118              inducts |> map (fn (name, th) => ([th],
   1.119                [Attrib.internal (K ind_case_names),
   1.120                 Attrib.internal (K (Rule_Cases.consumes 1)),
   1.121 @@ -751,8 +754,8 @@
   1.122    in (intrs', elims', induct', lthy3) end;
   1.123  
   1.124  type inductive_flags =
   1.125 -  {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
   1.126 -   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
   1.127 +  {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
   1.128 +    no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
   1.129  
   1.130  type add_ind_def =
   1.131    inductive_flags ->
   1.132 @@ -760,8 +763,7 @@
   1.133    term list -> (binding * mixfix) list ->
   1.134    local_theory -> inductive_result * local_theory;
   1.135  
   1.136 -fun add_ind_def
   1.137 -    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
   1.138 +fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
   1.139      cs intros monos params cnames_syn lthy =
   1.140    let
   1.141      val _ = null cnames_syn andalso error "No inductive predicates given";
   1.142 @@ -797,7 +799,7 @@
   1.143           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   1.144             rec_preds_defs lthy1);
   1.145  
   1.146 -    val (intrs', elims', induct, lthy2) = declare_rules kind rec_name coind no_ind
   1.147 +    val (intrs', elims', induct, lthy2) = declare_rules rec_name coind no_ind
   1.148        cnames intrs intr_names intr_atts elims raw_induct lthy1;
   1.149  
   1.150      val result =
   1.151 @@ -817,7 +819,7 @@
   1.152  (* external interfaces *)
   1.153  
   1.154  fun gen_add_inductive_i mk_def
   1.155 -    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
   1.156 +    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
   1.157      cnames_syn pnames spec monos lthy =
   1.158    let
   1.159      val thy = ProofContext.theory_of lthy;
   1.160 @@ -880,9 +882,8 @@
   1.161        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
   1.162      val (cs, ps) = chop (length cnames_syn) vars;
   1.163      val monos = Attrib.eval_thms lthy raw_monos;
   1.164 -    val flags = {quiet_mode = false, verbose = verbose, kind = "",
   1.165 -      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
   1.166 -      skip_mono = false, fork_mono = not int};
   1.167 +    val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
   1.168 +      coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
   1.169    in
   1.170      lthy
   1.171      |> LocalTheory.set_group (serial ())