--- a/src/HOL/Nominal/nominal_inductive.ML Fri Oct 05 22:00:13 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Oct 05 22:00:15 2007 +0200
@@ -148,7 +148,7 @@
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
val induct_cases = map fst (fst (RuleCases.get (the
- (Induct.lookup_inductS ctxt (hd names)))));
+ (Induct.lookup_inductP ctxt (hd names)))));
val raw_induct' = Logic.unvarify (prop_of raw_induct);
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
--- a/src/HOL/Tools/function_package/fundef_package.ML Fri Oct 05 22:00:13 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Oct 05 22:00:15 2007 +0200
@@ -73,7 +73,7 @@
|> addsmps "psimps" [] psimps
||> fold_option (snd oo addsmps "simps" []) trsimps
||>> note_theorem ((qualify "pinduct",
- [Attrib.internal (K (Induct.induct_set ""))]), simple_pinducts)
+ [Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
||>> note_theorem ((qualify "termination", []), [termination])
||> (snd o note_theorem ((qualify "cases", []), [cases]))
||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
--- a/src/HOL/Tools/inductive_package.ML Fri Oct 05 22:00:13 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Fri Oct 05 22:00:15 2007 +0200
@@ -433,7 +433,7 @@
error (Pretty.string_of (Pretty.block
[Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
- val elims = Induct.find_casesS ctxt prop;
+ val elims = Induct.find_casesP ctxt prop;
val cprop = Thm.cterm_of thy prop;
val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
@@ -679,7 +679,7 @@
if coind then
(raw_induct, [RuleCases.case_names [rec_name],
RuleCases.case_conclusion (rec_name, intr_names),
- RuleCases.consumes 1, Induct.coinduct_set (hd cnames)])
+ RuleCases.consumes 1, Induct.coinduct_pred (hd cnames)])
else if no_ind orelse length cnames > 1 then
(raw_induct, [ind_case_names, RuleCases.consumes 0])
else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
@@ -698,7 +698,7 @@
LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
[Attrib.internal (K (RuleCases.case_names cases)),
Attrib.internal (K (RuleCases.consumes 1)),
- Attrib.internal (K (Induct.cases_set name)),
+ Attrib.internal (K (Induct.cases_pred name)),
Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
@@ -712,7 +712,7 @@
inducts |> map (fn (name, th) => ([th],
[Attrib.internal (K ind_case_names),
Attrib.internal (K (RuleCases.consumes 1)),
- Attrib.internal (K (Induct.induct_set name))])))] |> snd
+ Attrib.internal (K (Induct.induct_pred name))])))] |> snd
end
in (intrs', elims', induct', ctxt3) end;
--- a/src/HOL/Tools/typedef_package.ML Fri Oct 05 22:00:13 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML Fri Oct 05 22:00:15 2007 +0200
@@ -176,11 +176,11 @@
((Rep_name ^ "_inject", make Rep_inject), []),
((Abs_name ^ "_inject", abs_inject), []),
((Rep_name ^ "_cases", make Rep_cases),
- [RuleCases.case_names [Rep_name], Induct.cases_set full_name]),
+ [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
((Abs_name ^ "_cases", make Abs_cases),
[RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
((Rep_name ^ "_induct", make Rep_induct),
- [RuleCases.case_names [Rep_name], Induct.induct_set full_name]),
+ [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
((Abs_name ^ "_induct", make Abs_induct),
[RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
||> Sign.parent_path;
--- a/src/Tools/induct.ML Fri Oct 05 22:00:13 2007 +0200
+++ b/src/Tools/induct.ML Fri Oct 05 22:00:15 2007 +0200
@@ -18,32 +18,33 @@
(*rule declarations*)
val vars_of: term -> term list
val dest_rules: Proof.context ->
- {type_cases: (string * thm) list, set_cases: (string * thm) list,
- type_induct: (string * thm) list, set_induct: (string * thm) list,
- type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
+ {type_cases: (string * thm) list, pred_cases: (string * thm) list,
+ type_induct: (string * thm) list, pred_induct: (string * thm) list,
+ type_coinduct: (string * thm) list, pred_coinduct: (string * thm) list}
val print_rules: Proof.context -> unit
val lookup_casesT: Proof.context -> string -> thm option
- val lookup_casesS: Proof.context -> string -> thm option
+ val lookup_casesP: Proof.context -> string -> thm option
val lookup_inductT: Proof.context -> string -> thm option
- val lookup_inductS: Proof.context -> string -> thm option
+ val lookup_inductP: Proof.context -> string -> thm option
val lookup_coinductT: Proof.context -> string -> thm option
- val lookup_coinductS: Proof.context -> string -> thm option
+ val lookup_coinductP: Proof.context -> string -> thm option
val find_casesT: Proof.context -> typ -> thm list
- val find_casesS: Proof.context -> term -> thm list
+ val find_casesP: Proof.context -> term -> thm list
val find_inductT: Proof.context -> typ -> thm list
- val find_inductS: Proof.context -> term -> thm list
+ val find_inductP: Proof.context -> term -> thm list
val find_coinductT: Proof.context -> typ -> thm list
- val find_coinductS: Proof.context -> term -> thm list
+ val find_coinductP: Proof.context -> term -> thm list
val cases_type: string -> attribute
- val cases_set: string -> attribute
+ val cases_pred: string -> attribute
val induct_type: string -> attribute
- val induct_set: string -> attribute
+ val induct_pred: string -> attribute
val coinduct_type: string -> attribute
- val coinduct_set: string -> attribute
+ val coinduct_pred: string -> attribute
val casesN: string
val inductN: string
val coinductN: string
val typeN: string
+ val predN: string
val setN: string
(*proof methods*)
val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
@@ -130,33 +131,33 @@
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
val extend = I;
- fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
- ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
- ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
- (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
- (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
+ fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
+ ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
+ ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)),
+ (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)),
+ (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2)));
);
val get_local = Induct.get o Context.Proof;
fun dest_rules ctxt =
- let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
+ let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
{type_cases = NetRules.rules casesT,
- set_cases = NetRules.rules casesS,
+ pred_cases = NetRules.rules casesP,
type_induct = NetRules.rules inductT,
- set_induct = NetRules.rules inductS,
+ pred_induct = NetRules.rules inductP,
type_coinduct = NetRules.rules coinductT,
- set_coinduct = NetRules.rules coinductS}
+ pred_coinduct = NetRules.rules coinductP}
end;
fun print_rules ctxt =
- let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
+ let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
[pretty_rules ctxt "coinduct type:" coinductT,
- pretty_rules ctxt "coinduct set:" coinductS,
+ pretty_rules ctxt "coinduct pred:" coinductP,
pretty_rules ctxt "induct type:" inductT,
- pretty_rules ctxt "induct set:" inductS,
+ pretty_rules ctxt "induct pred:" inductP,
pretty_rules ctxt "cases type:" casesT,
- pretty_rules ctxt "cases set:" casesS]
+ pretty_rules ctxt "cases pred:" casesP]
|> Pretty.chunks |> Pretty.writeln
end;
@@ -169,22 +170,22 @@
(* access rules *)
val lookup_casesT = lookup_rule o #1 o #1 o get_local;
-val lookup_casesS = lookup_rule o #2 o #1 o get_local;
+val lookup_casesP = lookup_rule o #2 o #1 o get_local;
val lookup_inductT = lookup_rule o #1 o #2 o get_local;
-val lookup_inductS = lookup_rule o #2 o #2 o get_local;
+val lookup_inductP = lookup_rule o #2 o #2 o get_local;
val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
-val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
+val lookup_coinductP = lookup_rule o #2 o #3 o get_local;
fun find_rules which how ctxt x =
map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
val find_casesT = find_rules (#1 o #1) encode_type;
-val find_casesS = find_rules (#2 o #1) I;
+val find_casesP = find_rules (#2 o #1) I;
val find_inductT = find_rules (#1 o #2) encode_type;
-val find_inductS = find_rules (#2 o #2) I;
+val find_inductP = find_rules (#2 o #2) I;
val find_coinductT = find_rules (#1 o #3) encode_type;
-val find_coinductS = find_rules (#2 o #3) I;
+val find_coinductP = find_rules (#2 o #3) I;
@@ -200,11 +201,11 @@
fun map3 f (x, y, z) = (x, y, f z);
fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
-fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
+fun add_casesP rule x = map1 (apsnd (NetRules.insert rule)) x;
fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
-fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
+fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x;
fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
-fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
+fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x;
fun consumes0 x = RuleCases.consumes_default 0 x;
fun consumes1 x = RuleCases.consumes_default 1 x;
@@ -212,11 +213,11 @@
in
val cases_type = mk_att add_casesT consumes0;
-val cases_set = mk_att add_casesS consumes1;
+val cases_pred = mk_att add_casesP consumes1;
val induct_type = mk_att add_inductT consumes0;
-val induct_set = mk_att add_inductS consumes1;
+val induct_pred = mk_att add_inductP consumes1;
val coinduct_type = mk_att add_coinductT consumes0;
-val coinduct_set = mk_att add_coinductS consumes1;
+val coinduct_pred = mk_att add_coinductP consumes1;
end;
@@ -229,6 +230,7 @@
val coinductN = "coinduct";
val typeN = "type";
+val predN = "pred";
val setN = "set";
local
@@ -237,19 +239,21 @@
Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
Scan.lift (Args.$$$ k) >> K "";
-fun attrib add_type add_set =
- Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
+fun attrib add_type add_pred = Attrib.syntax
+ (spec typeN Args.tyname >> add_type ||
+ spec predN Args.const >> add_pred ||
+ spec setN Args.const >> add_pred);
-val cases_att = attrib cases_type cases_set;
-val induct_att = attrib induct_type induct_set;
-val coinduct_att = attrib coinduct_type coinduct_set;
+val cases_att = attrib cases_type cases_pred;
+val induct_att = attrib induct_type induct_pred;
+val coinduct_att = attrib coinduct_type coinduct_pred;
in
val attrib_setup = Attrib.add_attributes
- [(casesN, cases_att, "declaration of cases rule for type or set"),
- (inductN, induct_att, "declaration of induction rule for type or set"),
- (coinductN, coinduct_att, "declaration of coinduction rule for type or set")];
+ [(casesN, cases_att, "declaration of cases rule for type or predicate/set"),
+ (inductN, induct_att, "declaration of induction rule for type or predicate/set"),
+ (coinductN, coinduct_att, "declaration of coinduction rule for type or predicate/set")];
end;
@@ -314,7 +318,7 @@
(*
rule selection scheme:
cases - default case split
- `x:A` cases ... - set cases
+ `A t` cases ... - predicate/set cases
cases t - type cases
... cases ... r - explicit rule
*)
@@ -324,8 +328,8 @@
fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t)
| get_casesT _ _ = [];
-fun get_casesS ctxt (fact :: _) = find_casesS ctxt (Thm.concl_of fact)
- | get_casesS _ _ = [];
+fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact)
+ | get_casesP _ _ = [];
in
@@ -345,7 +349,7 @@
(case opt_rule of
SOME r => Seq.single (inst_rule r)
| NONE =>
- (get_casesS ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
+ (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
|> tap (trace_rules ctxt casesN)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
in
@@ -551,7 +555,7 @@
(*
rule selection scheme:
- `x:A` induct ... - set induction
+ `A x` induct ... - predicate/set induction
induct x - type induction
... induct ... r - explicit rule
*)
@@ -563,8 +567,8 @@
|> map (find_inductT ctxt o Term.fastype_of)) [[]]
|> filter_out (forall PureThy.is_internal);
-fun get_inductS ctxt (fact :: _) = map single (find_inductS ctxt (Thm.concl_of fact))
- | get_inductS _ _ = [];
+fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
+ | get_inductP _ _ = [];
in
@@ -589,7 +593,7 @@
(case opt_rule of
SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
| NONE =>
- (get_inductS ctxt facts @
+ (get_inductP ctxt facts @
map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
|> map_filter (RuleCases.mutual_rule ctxt)
|> tap (trace_rules ctxt inductN o map #2)
@@ -627,7 +631,7 @@
(*
rule selection scheme:
- goal "x:A" coinduct ... - set coinduction
+ goal "A x" coinduct ... - predicate/set coinduction
coinduct x - type coinduction
coinduct ... r - explicit rule
*)
@@ -637,7 +641,10 @@
fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t)
| get_coinductT _ _ = [];
-fun get_coinductS ctxt goal = find_coinductS ctxt (Logic.strip_assums_concl goal);
+fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
+
+fun main_prop_of th =
+ if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
in
@@ -649,14 +656,14 @@
fun inst_rule r =
if null inst then `RuleCases.get r
- else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r
+ else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r
|> pair (RuleCases.get r);
fun ruleq goal =
(case opt_rule of
SOME r => Seq.single (inst_rule r)
| NONE =>
- (get_coinductS ctxt goal @ get_coinductT ctxt inst)
+ (get_coinductP ctxt goal @ get_coinductT ctxt inst)
|> tap (trace_rules ctxt coinductN)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
in
@@ -693,14 +700,15 @@
(case get (Context.proof_of context) name of SOME x => x
| NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
-fun rule get_type get_set =
+fun rule get_type get_pred =
named_rule typeN Args.tyname get_type ||
- named_rule setN Args.const get_set ||
+ named_rule predN Args.const get_pred ||
+ named_rule setN Args.const get_pred ||
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
-val cases_rule = rule lookup_casesT lookup_casesS >> single_rule;
-val induct_rule = rule lookup_inductT lookup_inductS;
-val coinduct_rule = rule lookup_coinductT lookup_coinductS >> single_rule;
+val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
+val induct_rule = rule lookup_inductT lookup_inductP;
+val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule;
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
@@ -714,7 +722,7 @@
fun unless_more_args scan = Scan.unless (Scan.lift
((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
- Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
+ Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
Args.and_list1 (Scan.repeat (unless_more_args free))) [];
@@ -755,8 +763,8 @@
val setup =
attrib_setup #>
Method.add_methods
- [(casesN, cases_meth, "case analysis on types or sets"),
- (inductN, induct_meth, "induction on types or sets"),
- (coinductN, coinduct_meth, "coinduction on types or sets")];
+ [(casesN, cases_meth, "case analysis on types or predicates/sets"),
+ (inductN, induct_meth, "induction on types or predicates/sets"),
+ (coinductN, coinduct_meth, "coinduction on types or predicates/sets")];
end;
--- a/src/ZF/Tools/inductive_package.ML Fri Oct 05 22:00:13 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Oct 05 22:00:15 2007 +0200
@@ -506,7 +506,7 @@
val ([induct', mutual_induct'], thy') =
thy
|> PureThy.add_thms [((co_prefix ^ "induct", induct),
- [case_names, Induct.induct_set big_rec_name]),
+ [case_names, Induct.induct_pred big_rec_name]),
(("mutual_induct", mutual_induct), [case_names])];
in ((thy', induct'), mutual_induct')
end; (*of induction_rules*)
@@ -528,7 +528,7 @@
|> PureThy.add_thms
[(("bnd_mono", bnd_mono), []),
(("dom_subset", dom_subset), []),
- (("cases", elim), [case_names, Induct.cases_set big_rec_name])]
+ (("cases", elim), [case_names, Induct.cases_pred big_rec_name])]
||>> (PureThy.add_thmss o map Thm.no_attributes)
[("defs", defs),
("intros", intrs)];