tuned Induct interface: prefer pred'' over set'';
authorwenzelm
Fri Oct 05 22:00:15 2007 +0200 (2007-10-05)
changeset 24861cc669ca5f382
parent 24860 ceb634874e0c
child 24862 6b7258da912b
tuned Induct interface: prefer pred'' over set'';
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/typedef_package.ML
src/Tools/induct.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Oct 05 22:00:13 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Oct 05 22:00:15 2007 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     1.5            commas_quote xs));
     1.6      val induct_cases = map fst (fst (RuleCases.get (the
     1.7 -      (Induct.lookup_inductS ctxt (hd names)))));
     1.8 +      (Induct.lookup_inductP ctxt (hd names)))));
     1.9      val raw_induct' = Logic.unvarify (prop_of raw_induct);
    1.10      val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
    1.11        HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Oct 05 22:00:13 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Oct 05 22:00:15 2007 +0200
     2.3 @@ -73,7 +73,7 @@
     2.4              |> addsmps "psimps" [] psimps
     2.5              ||> fold_option (snd oo addsmps "simps" []) trsimps
     2.6              ||>> note_theorem ((qualify "pinduct",
     2.7 -                                [Attrib.internal (K (Induct.induct_set ""))]), simple_pinducts)
     2.8 +                                [Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
     2.9              ||>> note_theorem ((qualify "termination", []), [termination])
    2.10              ||> (snd o note_theorem ((qualify "cases", []), [cases]))
    2.11              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 05 22:00:13 2007 +0200
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 05 22:00:15 2007 +0200
     3.3 @@ -433,7 +433,7 @@
     3.4        error (Pretty.string_of (Pretty.block
     3.5          [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
     3.6  
     3.7 -    val elims = Induct.find_casesS ctxt prop;
     3.8 +    val elims = Induct.find_casesP ctxt prop;
     3.9  
    3.10      val cprop = Thm.cterm_of thy prop;
    3.11      val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
    3.12 @@ -679,7 +679,7 @@
    3.13        if coind then
    3.14          (raw_induct, [RuleCases.case_names [rec_name],
    3.15            RuleCases.case_conclusion (rec_name, intr_names),
    3.16 -          RuleCases.consumes 1, Induct.coinduct_set (hd cnames)])
    3.17 +          RuleCases.consumes 1, Induct.coinduct_pred (hd cnames)])
    3.18        else if no_ind orelse length cnames > 1 then
    3.19          (raw_induct, [ind_case_names, RuleCases.consumes 0])
    3.20        else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
    3.21 @@ -698,7 +698,7 @@
    3.22          LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
    3.23            [Attrib.internal (K (RuleCases.case_names cases)),
    3.24             Attrib.internal (K (RuleCases.consumes 1)),
    3.25 -           Attrib.internal (K (Induct.cases_set name)),
    3.26 +           Attrib.internal (K (Induct.cases_pred name)),
    3.27             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    3.28          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    3.29        LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
    3.30 @@ -712,7 +712,7 @@
    3.31            inducts |> map (fn (name, th) => ([th],
    3.32              [Attrib.internal (K ind_case_names),
    3.33               Attrib.internal (K (RuleCases.consumes 1)),
    3.34 -             Attrib.internal (K (Induct.induct_set name))])))] |> snd
    3.35 +             Attrib.internal (K (Induct.induct_pred name))])))] |> snd
    3.36        end
    3.37    in (intrs', elims', induct', ctxt3) end;
    3.38  
     4.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Oct 05 22:00:13 2007 +0200
     4.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Oct 05 22:00:15 2007 +0200
     4.3 @@ -176,11 +176,11 @@
     4.4                  ((Rep_name ^ "_inject", make Rep_inject), []),
     4.5                  ((Abs_name ^ "_inject", abs_inject), []),
     4.6                  ((Rep_name ^ "_cases", make Rep_cases),
     4.7 -                  [RuleCases.case_names [Rep_name], Induct.cases_set full_name]),
     4.8 +                  [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
     4.9                  ((Abs_name ^ "_cases", make Abs_cases),
    4.10                    [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
    4.11                  ((Rep_name ^ "_induct", make Rep_induct),
    4.12 -                  [RuleCases.case_names [Rep_name], Induct.induct_set full_name]),
    4.13 +                  [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
    4.14                  ((Abs_name ^ "_induct", make Abs_induct),
    4.15                    [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
    4.16              ||> Sign.parent_path;
     5.1 --- a/src/Tools/induct.ML	Fri Oct 05 22:00:13 2007 +0200
     5.2 +++ b/src/Tools/induct.ML	Fri Oct 05 22:00:15 2007 +0200
     5.3 @@ -18,32 +18,33 @@
     5.4    (*rule declarations*)
     5.5    val vars_of: term -> term list
     5.6    val dest_rules: Proof.context ->
     5.7 -    {type_cases: (string * thm) list, set_cases: (string * thm) list,
     5.8 -      type_induct: (string * thm) list, set_induct: (string * thm) list,
     5.9 -      type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
    5.10 +    {type_cases: (string * thm) list, pred_cases: (string * thm) list,
    5.11 +      type_induct: (string * thm) list, pred_induct: (string * thm) list,
    5.12 +      type_coinduct: (string * thm) list, pred_coinduct: (string * thm) list}
    5.13    val print_rules: Proof.context -> unit
    5.14    val lookup_casesT: Proof.context -> string -> thm option
    5.15 -  val lookup_casesS: Proof.context -> string -> thm option
    5.16 +  val lookup_casesP: Proof.context -> string -> thm option
    5.17    val lookup_inductT: Proof.context -> string -> thm option
    5.18 -  val lookup_inductS: Proof.context -> string -> thm option
    5.19 +  val lookup_inductP: Proof.context -> string -> thm option
    5.20    val lookup_coinductT: Proof.context -> string -> thm option
    5.21 -  val lookup_coinductS: Proof.context -> string -> thm option
    5.22 +  val lookup_coinductP: Proof.context -> string -> thm option
    5.23    val find_casesT: Proof.context -> typ -> thm list
    5.24 -  val find_casesS: Proof.context -> term -> thm list
    5.25 +  val find_casesP: Proof.context -> term -> thm list
    5.26    val find_inductT: Proof.context -> typ -> thm list
    5.27 -  val find_inductS: Proof.context -> term -> thm list
    5.28 +  val find_inductP: Proof.context -> term -> thm list
    5.29    val find_coinductT: Proof.context -> typ -> thm list
    5.30 -  val find_coinductS: Proof.context -> term -> thm list
    5.31 +  val find_coinductP: Proof.context -> term -> thm list
    5.32    val cases_type: string -> attribute
    5.33 -  val cases_set: string -> attribute
    5.34 +  val cases_pred: string -> attribute
    5.35    val induct_type: string -> attribute
    5.36 -  val induct_set: string -> attribute
    5.37 +  val induct_pred: string -> attribute
    5.38    val coinduct_type: string -> attribute
    5.39 -  val coinduct_set: string -> attribute
    5.40 +  val coinduct_pred: string -> attribute
    5.41    val casesN: string
    5.42    val inductN: string
    5.43    val coinductN: string
    5.44    val typeN: string
    5.45 +  val predN: string
    5.46    val setN: string
    5.47    (*proof methods*)
    5.48    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    5.49 @@ -130,33 +131,33 @@
    5.50       (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
    5.51       (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
    5.52    val extend = I;
    5.53 -  fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
    5.54 -      ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
    5.55 -    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
    5.56 -      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
    5.57 -      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
    5.58 +  fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
    5.59 +      ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
    5.60 +    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)),
    5.61 +      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)),
    5.62 +      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2)));
    5.63  );
    5.64  
    5.65  val get_local = Induct.get o Context.Proof;
    5.66  
    5.67  fun dest_rules ctxt =
    5.68 -  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
    5.69 +  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
    5.70      {type_cases = NetRules.rules casesT,
    5.71 -     set_cases = NetRules.rules casesS,
    5.72 +     pred_cases = NetRules.rules casesP,
    5.73       type_induct = NetRules.rules inductT,
    5.74 -     set_induct = NetRules.rules inductS,
    5.75 +     pred_induct = NetRules.rules inductP,
    5.76       type_coinduct = NetRules.rules coinductT,
    5.77 -     set_coinduct = NetRules.rules coinductS}
    5.78 +     pred_coinduct = NetRules.rules coinductP}
    5.79    end;
    5.80  
    5.81  fun print_rules ctxt =
    5.82 -  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
    5.83 +  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
    5.84     [pretty_rules ctxt "coinduct type:" coinductT,
    5.85 -    pretty_rules ctxt "coinduct set:" coinductS,
    5.86 +    pretty_rules ctxt "coinduct pred:" coinductP,
    5.87      pretty_rules ctxt "induct type:" inductT,
    5.88 -    pretty_rules ctxt "induct set:" inductS,
    5.89 +    pretty_rules ctxt "induct pred:" inductP,
    5.90      pretty_rules ctxt "cases type:" casesT,
    5.91 -    pretty_rules ctxt "cases set:" casesS]
    5.92 +    pretty_rules ctxt "cases pred:" casesP]
    5.93      |> Pretty.chunks |> Pretty.writeln
    5.94    end;
    5.95  
    5.96 @@ -169,22 +170,22 @@
    5.97  (* access rules *)
    5.98  
    5.99  val lookup_casesT = lookup_rule o #1 o #1 o get_local;
   5.100 -val lookup_casesS = lookup_rule o #2 o #1 o get_local;
   5.101 +val lookup_casesP = lookup_rule o #2 o #1 o get_local;
   5.102  val lookup_inductT = lookup_rule o #1 o #2 o get_local;
   5.103 -val lookup_inductS = lookup_rule o #2 o #2 o get_local;
   5.104 +val lookup_inductP = lookup_rule o #2 o #2 o get_local;
   5.105  val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
   5.106 -val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
   5.107 +val lookup_coinductP = lookup_rule o #2 o #3 o get_local;
   5.108  
   5.109  
   5.110  fun find_rules which how ctxt x =
   5.111    map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
   5.112  
   5.113  val find_casesT = find_rules (#1 o #1) encode_type;
   5.114 -val find_casesS = find_rules (#2 o #1) I;
   5.115 +val find_casesP = find_rules (#2 o #1) I;
   5.116  val find_inductT = find_rules (#1 o #2) encode_type;
   5.117 -val find_inductS = find_rules (#2 o #2) I;
   5.118 +val find_inductP = find_rules (#2 o #2) I;
   5.119  val find_coinductT = find_rules (#1 o #3) encode_type;
   5.120 -val find_coinductS = find_rules (#2 o #3) I;
   5.121 +val find_coinductP = find_rules (#2 o #3) I;
   5.122  
   5.123  
   5.124  
   5.125 @@ -200,11 +201,11 @@
   5.126  fun map3 f (x, y, z) = (x, y, f z);
   5.127  
   5.128  fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
   5.129 -fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
   5.130 +fun add_casesP rule x = map1 (apsnd (NetRules.insert rule)) x;
   5.131  fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
   5.132 -fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
   5.133 +fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x;
   5.134  fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
   5.135 -fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
   5.136 +fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x;
   5.137  
   5.138  fun consumes0 x = RuleCases.consumes_default 0 x;
   5.139  fun consumes1 x = RuleCases.consumes_default 1 x;
   5.140 @@ -212,11 +213,11 @@
   5.141  in
   5.142  
   5.143  val cases_type = mk_att add_casesT consumes0;
   5.144 -val cases_set = mk_att add_casesS consumes1;
   5.145 +val cases_pred = mk_att add_casesP consumes1;
   5.146  val induct_type = mk_att add_inductT consumes0;
   5.147 -val induct_set = mk_att add_inductS consumes1;
   5.148 +val induct_pred = mk_att add_inductP consumes1;
   5.149  val coinduct_type = mk_att add_coinductT consumes0;
   5.150 -val coinduct_set = mk_att add_coinductS consumes1;
   5.151 +val coinduct_pred = mk_att add_coinductP consumes1;
   5.152  
   5.153  end;
   5.154  
   5.155 @@ -229,6 +230,7 @@
   5.156  val coinductN = "coinduct";
   5.157  
   5.158  val typeN = "type";
   5.159 +val predN = "pred";
   5.160  val setN = "set";
   5.161  
   5.162  local
   5.163 @@ -237,19 +239,21 @@
   5.164    Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   5.165    Scan.lift (Args.$$$ k) >> K "";
   5.166  
   5.167 -fun attrib add_type add_set =
   5.168 -  Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
   5.169 +fun attrib add_type add_pred = Attrib.syntax
   5.170 + (spec typeN Args.tyname >> add_type ||
   5.171 +  spec predN Args.const >> add_pred ||
   5.172 +  spec setN Args.const >> add_pred);
   5.173  
   5.174 -val cases_att = attrib cases_type cases_set;
   5.175 -val induct_att = attrib induct_type induct_set;
   5.176 -val coinduct_att = attrib coinduct_type coinduct_set;
   5.177 +val cases_att = attrib cases_type cases_pred;
   5.178 +val induct_att = attrib induct_type induct_pred;
   5.179 +val coinduct_att = attrib coinduct_type coinduct_pred;
   5.180  
   5.181  in
   5.182  
   5.183  val attrib_setup = Attrib.add_attributes
   5.184 - [(casesN, cases_att, "declaration of cases rule for type or set"),
   5.185 -  (inductN, induct_att, "declaration of induction rule for type or set"),
   5.186 -  (coinductN, coinduct_att, "declaration of coinduction rule for type or set")];
   5.187 + [(casesN, cases_att, "declaration of cases rule for type or predicate/set"),
   5.188 +  (inductN, induct_att, "declaration of induction rule for type or predicate/set"),
   5.189 +  (coinductN, coinduct_att, "declaration of coinduction rule for type or predicate/set")];
   5.190  
   5.191  end;
   5.192  
   5.193 @@ -314,7 +318,7 @@
   5.194  (*
   5.195    rule selection scheme:
   5.196            cases         - default case split
   5.197 -    `x:A` cases ...     - set cases
   5.198 +    `A t` cases ...     - predicate/set cases
   5.199            cases t       - type cases
   5.200      ...   cases ... r   - explicit rule
   5.201  *)
   5.202 @@ -324,8 +328,8 @@
   5.203  fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t)
   5.204    | get_casesT _ _ = [];
   5.205  
   5.206 -fun get_casesS ctxt (fact :: _) = find_casesS ctxt (Thm.concl_of fact)
   5.207 -  | get_casesS _ _ = [];
   5.208 +fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact)
   5.209 +  | get_casesP _ _ = [];
   5.210  
   5.211  in
   5.212  
   5.213 @@ -345,7 +349,7 @@
   5.214        (case opt_rule of
   5.215          SOME r => Seq.single (inst_rule r)
   5.216        | NONE =>
   5.217 -          (get_casesS ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
   5.218 +          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
   5.219            |> tap (trace_rules ctxt casesN)
   5.220            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   5.221    in
   5.222 @@ -551,7 +555,7 @@
   5.223  
   5.224  (*
   5.225    rule selection scheme:
   5.226 -    `x:A` induct ...     - set induction
   5.227 +    `A x` induct ...     - predicate/set induction
   5.228            induct x       - type induction
   5.229      ...   induct ... r   - explicit rule
   5.230  *)
   5.231 @@ -563,8 +567,8 @@
   5.232      |> map (find_inductT ctxt o Term.fastype_of)) [[]]
   5.233    |> filter_out (forall PureThy.is_internal);
   5.234  
   5.235 -fun get_inductS ctxt (fact :: _) = map single (find_inductS ctxt (Thm.concl_of fact))
   5.236 -  | get_inductS _ _ = [];
   5.237 +fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   5.238 +  | get_inductP _ _ = [];
   5.239  
   5.240  in
   5.241  
   5.242 @@ -589,7 +593,7 @@
   5.243        (case opt_rule of
   5.244          SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
   5.245        | NONE =>
   5.246 -          (get_inductS ctxt facts @
   5.247 +          (get_inductP ctxt facts @
   5.248              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
   5.249            |> map_filter (RuleCases.mutual_rule ctxt)
   5.250            |> tap (trace_rules ctxt inductN o map #2)
   5.251 @@ -627,7 +631,7 @@
   5.252  
   5.253  (*
   5.254    rule selection scheme:
   5.255 -    goal "x:A" coinduct ...   - set coinduction
   5.256 +    goal "A x" coinduct ...   - predicate/set coinduction
   5.257                 coinduct x     - type coinduction
   5.258                 coinduct ... r - explicit rule
   5.259  *)
   5.260 @@ -637,7 +641,10 @@
   5.261  fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t)
   5.262    | get_coinductT _ _ = [];
   5.263  
   5.264 -fun get_coinductS ctxt goal = find_coinductS ctxt (Logic.strip_assums_concl goal);
   5.265 +fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
   5.266 +
   5.267 +fun main_prop_of th =
   5.268 +  if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
   5.269  
   5.270  in
   5.271  
   5.272 @@ -649,14 +656,14 @@
   5.273  
   5.274      fun inst_rule r =
   5.275        if null inst then `RuleCases.get r
   5.276 -      else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r
   5.277 +      else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r
   5.278          |> pair (RuleCases.get r);
   5.279  
   5.280      fun ruleq goal =
   5.281        (case opt_rule of
   5.282          SOME r => Seq.single (inst_rule r)
   5.283        | NONE =>
   5.284 -          (get_coinductS ctxt goal @ get_coinductT ctxt inst)
   5.285 +          (get_coinductP ctxt goal @ get_coinductT ctxt inst)
   5.286            |> tap (trace_rules ctxt coinductN)
   5.287            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   5.288    in
   5.289 @@ -693,14 +700,15 @@
   5.290        (case get (Context.proof_of context) name of SOME x => x
   5.291        | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
   5.292  
   5.293 -fun rule get_type get_set =
   5.294 +fun rule get_type get_pred =
   5.295    named_rule typeN Args.tyname get_type ||
   5.296 -  named_rule setN Args.const get_set ||
   5.297 +  named_rule predN Args.const get_pred ||
   5.298 +  named_rule setN Args.const get_pred ||
   5.299    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   5.300  
   5.301 -val cases_rule = rule lookup_casesT lookup_casesS >> single_rule;
   5.302 -val induct_rule = rule lookup_inductT lookup_inductS;
   5.303 -val coinduct_rule = rule lookup_coinductT lookup_coinductS >> single_rule;
   5.304 +val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
   5.305 +val induct_rule = rule lookup_inductT lookup_inductP;
   5.306 +val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule;
   5.307  
   5.308  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
   5.309  
   5.310 @@ -714,7 +722,7 @@
   5.311  
   5.312  fun unless_more_args scan = Scan.unless (Scan.lift
   5.313    ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
   5.314 -    Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
   5.315 +    Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
   5.316  
   5.317  val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   5.318    Args.and_list1 (Scan.repeat (unless_more_args free))) [];
   5.319 @@ -755,8 +763,8 @@
   5.320  val setup =
   5.321    attrib_setup #>
   5.322    Method.add_methods
   5.323 -    [(casesN, cases_meth, "case analysis on types or sets"),
   5.324 -     (inductN, induct_meth, "induction on types or sets"),
   5.325 -     (coinductN, coinduct_meth, "coinduction on types or sets")];
   5.326 +    [(casesN, cases_meth, "case analysis on types or predicates/sets"),
   5.327 +     (inductN, induct_meth, "induction on types or predicates/sets"),
   5.328 +     (coinductN, coinduct_meth, "coinduction on types or predicates/sets")];
   5.329  
   5.330  end;
     6.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Oct 05 22:00:13 2007 +0200
     6.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Oct 05 22:00:15 2007 +0200
     6.3 @@ -506,7 +506,7 @@
     6.4       val ([induct', mutual_induct'], thy') =
     6.5         thy
     6.6         |> PureThy.add_thms [((co_prefix ^ "induct", induct),
     6.7 -             [case_names, Induct.induct_set big_rec_name]),
     6.8 +             [case_names, Induct.induct_pred big_rec_name]),
     6.9             (("mutual_induct", mutual_induct), [case_names])];
    6.10      in ((thy', induct'), mutual_induct')
    6.11      end;  (*of induction_rules*)
    6.12 @@ -528,7 +528,7 @@
    6.13      |> PureThy.add_thms
    6.14        [(("bnd_mono", bnd_mono), []),
    6.15         (("dom_subset", dom_subset), []),
    6.16 -       (("cases", elim), [case_names, Induct.cases_set big_rec_name])]
    6.17 +       (("cases", elim), [case_names, Induct.cases_pred big_rec_name])]
    6.18      ||>> (PureThy.add_thmss o map Thm.no_attributes)
    6.19          [("defs", defs),
    6.20           ("intros", intrs)];