# HG changeset patch # User wenzelm # Date 1258138666 -3600 # Node ID ae9a2ea9a98995911fbf29ff80c6ada2a30949f4 # Parent 090288424d44bdf230d074d5561571b2c73ac242 inductive: eliminated obsolete kind; diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Nov 13 19:57:46 2009 +0100 @@ -569,9 +569,8 @@ thy3 |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global (serial ()) - {quiet_mode = false, verbose = false, kind = "", - alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false, - skip_mono = true, fork_mono = false} + {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name, + coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) (rep_set_names' ~~ recTs')) [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] @@ -1513,9 +1512,8 @@ thy10 |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global (serial ()) - {quiet_mode = #quiet config, verbose = false, kind = "", - alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false, - skip_mono = true, fork_mono = false} + {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name, + coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Nov 13 19:57:46 2009 +0100 @@ -156,9 +156,8 @@ thy0 |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global (serial ()) - {quiet_mode = #quiet config, verbose = false, kind = "", - alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true, - skip_mono = true, fork_mono = false} + {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name', + coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Nov 13 19:57:46 2009 +0100 @@ -175,9 +175,8 @@ thy1 |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global (serial ()) - {quiet_mode = #quiet config, verbose = false, kind = "", - alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false, - skip_mono = true, fork_mono = false} + {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name, + coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] ||> Sign.restore_naming thy1 diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Tools/Function/function_core.ML Fri Nov 13 19:57:46 2009 +0100 @@ -460,7 +460,6 @@ |> Inductive.add_inductive_i {quiet_mode = true, verbose = ! trace, - kind = "", alt_name = Binding.empty, coind = false, no_elim = false, diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 13 19:57:46 2009 +0100 @@ -355,9 +355,8 @@ thy |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global (serial ()) - {quiet_mode = false, verbose = false, kind = "", - alt_name = Binding.empty, coind = false, no_elim = false, - no_ind = false, skip_mono = false, fork_mono = false} + {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, + no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) pnames diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Tools/inductive.ML Fri Nov 13 19:57:46 2009 +0100 @@ -39,8 +39,8 @@ val inductive_cases_i: (Attrib.binding * term list) list -> local_theory -> thm list list * local_theory type inductive_flags = - {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding, - coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool} + {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, + no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool} val add_inductive_i: inductive_flags -> ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> @@ -71,7 +71,7 @@ term list -> (Attrib.binding * term) list -> thm list -> term list -> (binding * mixfix) list -> local_theory -> inductive_result * local_theory - val declare_rules: string -> binding -> bool -> bool -> string list -> + val declare_rules: binding -> bool -> bool -> string list -> thm list -> binding list -> Attrib.src list list -> (thm * string list) list -> thm -> local_theory -> thm list * thm list * thm * local_theory val add_ind_def: add_ind_def @@ -509,7 +509,8 @@ fun mk_ind_prem r = let - fun subst s = (case dest_predicate cs params s of + fun subst s = + (case dest_predicate cs params s of SOME (_, i, ys, (_, Ts)) => let val k = length Ts; @@ -520,10 +521,11 @@ HOLogic.mk_binop inductive_conj_name (list_comb (incr_boundvars k s, bs), P)) in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end - | NONE => (case s of - (t $ u) => (fst (subst t) $ fst (subst u), NONE) - | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE) - | _ => (s, NONE))); + | NONE => + (case s of + (t $ u) => (fst (subst t) $ fst (subst u), NONE) + | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE) + | _ => (s, NONE))); fun mk_prem s prems = (case subst s of @@ -618,16 +620,17 @@ SOME (_, i, ts, (Ts, Us)) => let val l = length Us; - val zs = map Bound (l - 1 downto 0) + val zs = map Bound (l - 1 downto 0); in list_abs (map (pair "z") Us, list_comb (p, make_bool_args' bs i @ make_args argTs ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us)))) end - | NONE => (case t of - t1 $ t2 => subst t1 $ subst t2 - | Abs (x, T, u) => Abs (x, T, subst u) - | _ => t)); + | NONE => + (case t of + t1 $ t2 => subst t1 $ subst t2 + | Abs (x, T, u) => Abs (x, T, subst u) + | _ => t)); (* transform an introduction rule into a conjunction *) (* [| p_i t; ... |] ==> p_j u *) @@ -698,8 +701,8 @@ list_comb (rec_const, params), preds, argTs, bs, xs) end; -fun declare_rules kind rec_binding coind no_ind cnames - intrs intr_bindings intr_atts elims raw_induct lthy = +fun declare_rules rec_binding coind no_ind cnames + intrs intr_bindings intr_atts elims raw_induct lthy = let val rec_name = Binding.name_of rec_binding; fun rec_qualified qualified = Binding.qualify qualified rec_name; @@ -716,7 +719,7 @@ val (intrs', lthy1) = lthy |> - LocalTheory.notes kind + LocalTheory.notes "" (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (Context_Rules.intro_query NONE)), @@ -724,16 +727,16 @@ map (hd o snd); val (((_, elims'), (_, [induct'])), lthy2) = lthy1 |> - LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> + LocalTheory.note "" ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> fold_map (fn (name, (elim, cases)) => - LocalTheory.note kind + LocalTheory.note "" ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"), [Attrib.internal (K (Rule_Cases.case_names cases)), Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.cases_pred name)), Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #> apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> - LocalTheory.note kind + LocalTheory.note "" ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); @@ -742,7 +745,7 @@ else let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in lthy2 |> - LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []), + LocalTheory.notes "" [((rec_qualified true (Binding.name "inducts"), []), inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), Attrib.internal (K (Rule_Cases.consumes 1)), @@ -751,8 +754,8 @@ in (intrs', elims', induct', lthy3) end; type inductive_flags = - {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding, - coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}; + {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, + no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}; type add_ind_def = inductive_flags -> @@ -760,8 +763,7 @@ term list -> (binding * mixfix) list -> local_theory -> inductive_result * local_theory; -fun add_ind_def - {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} +fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} cs intros monos params cnames_syn lthy = let val _ = null cnames_syn andalso error "No inductive predicates given"; @@ -797,7 +799,7 @@ prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def rec_preds_defs lthy1); - val (intrs', elims', induct, lthy2) = declare_rules kind rec_name coind no_ind + val (intrs', elims', induct, lthy2) = declare_rules rec_name coind no_ind cnames intrs intr_names intr_atts elims raw_induct lthy1; val result = @@ -817,7 +819,7 @@ (* external interfaces *) fun gen_add_inductive_i mk_def - (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}) + (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}) cnames_syn pnames spec monos lthy = let val thy = ProofContext.theory_of lthy; @@ -880,9 +882,8 @@ |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs; val (cs, ps) = chop (length cnames_syn) vars; val monos = Attrib.eval_thms lthy raw_monos; - val flags = {quiet_mode = false, verbose = verbose, kind = "", - alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, - skip_mono = false, fork_mono = not int}; + val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty, + coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int}; in lthy |> LocalTheory.set_group (serial ()) diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 19:57:46 2009 +0100 @@ -351,8 +351,8 @@ val (ind_info, thy3') = thy2 |> Inductive.add_inductive_global (serial ()) - {quiet_mode = false, verbose = false, kind = "", alt_name = Binding.empty, - coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} + {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, + no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} rlzpreds rlzparams (map (fn (rintr, intr) => ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), subst_atomic rlzpreds' (Logic.unvarify rintr))) diff -r 090288424d44 -r ae9a2ea9a989 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Nov 13 17:15:35 2009 +0000 +++ b/src/HOL/Tools/inductive_set.ML Fri Nov 13 19:57:46 2009 +0100 @@ -224,7 +224,7 @@ map (fn (x, ps) => let val U = HOLogic.dest_setT (fastype_of x); - val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x + val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x; in (cterm_of thy x, cterm_of thy (HOLogic.Collect_const U $ @@ -405,7 +405,7 @@ (**** definition of inductive sets ****) fun add_ind_set_def - {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} + {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} cs intros monos params cnames_syn lthy = let val thy = ProofContext.theory_of lthy; @@ -477,7 +477,7 @@ val monos' = map (to_pred [] (Context.Proof lthy)) monos; val ({preds, intrs, elims, raw_induct, ...}, lthy1) = Inductive.add_ind_def - {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty, + {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty, coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono, fork_mono = fork_mono} cs' intros' monos' params1 cnames_syn' lthy; @@ -505,7 +505,7 @@ (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps [def, mem_Collect_eq, split_conv]) 1)) in - lthy |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"), + lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"), [Attrib.internal (K pred_set_conv_att)]), [conv_thm]) |> snd end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2; @@ -519,7 +519,7 @@ val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct; val (intrs', elims', induct, lthy4) = - Inductive.declare_rules kind rec_name coind no_ind cnames + Inductive.declare_rules rec_name coind no_ind cnames (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts (map (fn th => (to_set [] (Context.Proof lthy3) th, map fst (fst (Rule_Cases.get th)))) elims)