--- a/src/HOL/Nominal/nominal_datatype.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 01 15:24:45 2009 +0100
@@ -62,10 +62,10 @@
in
-fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
+fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
fun mk_case_names_exhausts descr new =
- map (RuleCases.case_names o exhaust_cases descr o #1)
+ map (Rule_Cases.case_names o exhaust_cases descr o #1)
(filter (fn ((_, (name, _, _))) => name mem_string new) descr);
end;
@@ -153,7 +153,7 @@
fun projections rule =
Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
- |> map (Drule.standard #> RuleCases.save rule);
+ |> map (Drule.standard #> Rule_Cases.save rule);
val supp_prod = thm "supp_prod";
val fresh_prod = thm "fresh_prod";
--- a/src/HOL/Nominal/nominal_induct.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Sun Nov 01 15:24:45 2009 +0100
@@ -7,7 +7,7 @@
sig
val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
- thm list -> int -> RuleCases.cases_tactic
+ thm list -> int -> Rule_Cases.cases_tactic
val nominal_induct_method: (Proof.context -> Proof.method) context_parser
end =
struct
@@ -31,9 +31,9 @@
fun inst_mutual_rule ctxt insts avoiding rules =
let
- val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
+ val (nconcls, joined_rule) = Rule_Cases.strict_mutual_rule ctxt rules;
val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
- val (cases, consumes) = RuleCases.get joined_rule;
+ val (cases, consumes) = Rule_Cases.get joined_rule;
val l = length rules;
val _ =
@@ -93,12 +93,12 @@
split_all_tuples
#> rename_params_rule true
(map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
- fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
+ fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
in
(fn i => fn st =>
rules
|> inst_mutual_rule ctxt insts avoiding
- |> RuleCases.consume (flat defs) facts
+ |> Rule_Cases.consume (flat defs) facts
|> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
(CONJUNCTS (ALLGOALS
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Nov 01 15:24:45 2009 +0100
@@ -158,7 +158,7 @@
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
- val induct_cases = map fst (fst (RuleCases.get (the
+ val induct_cases = map fst (fst (Rule_Cases.get (the
(Induct.lookup_inductP ctxt (hd names)))));
val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
@@ -547,7 +547,7 @@
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
- val ind_case_names = RuleCases.case_names induct_cases;
+ val ind_case_names = Rule_Cases.case_names induct_cases;
val induct_cases' = Inductive.partition_rules' raw_induct
(intrs ~~ induct_cases);
val thss' = map (map atomize_intr) thss;
@@ -558,9 +558,9 @@
(thsss ~~ elims ~~ cases_prems ~~ cases_prems');
val strong_induct =
if length names > 1 then
- (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
+ (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
else (strong_raw_induct RSN (2, rev_mp),
- [ind_case_names, RuleCases.consumes 1]);
+ [ind_case_names, Rule_Cases.consumes 1]);
val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
((rec_qualified (Binding.name "strong_induct"),
map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
@@ -572,12 +572,12 @@
LocalTheory.note Thm.generatedK
((rec_qualified (Binding.name "strong_inducts"),
[Attrib.internal (K ind_case_names),
- Attrib.internal (K (RuleCases.consumes 1))]),
+ Attrib.internal (K (Rule_Cases.consumes 1))]),
strong_inducts) |> snd |>
LocalTheory.notes Thm.generatedK (map (fn ((name, elim), (_, cases)) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
- [Attrib.internal (K (RuleCases.case_names (map snd cases))),
- Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
+ [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
+ Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
(strong_cases ~~ induct_cases')) |> snd
end)
(map (map (rulify_term thy #> rpair [])) vc_compat)
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Nov 01 15:24:45 2009 +0100
@@ -164,7 +164,7 @@
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
- val induct_cases = map fst (fst (RuleCases.get (the
+ val induct_cases = map fst (fst (Rule_Cases.get (the
(Induct.lookup_inductP ctxt (hd names)))));
val induct_cases' = if null induct_cases then replicate (length intrs) ""
else induct_cases;
@@ -449,7 +449,7 @@
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
- val ind_case_names = RuleCases.case_names induct_cases;
+ val ind_case_names = Rule_Cases.case_names induct_cases;
val induct_cases' = Inductive.partition_rules' raw_induct
(intrs ~~ induct_cases);
val thss' = map (map atomize_intr) thss;
@@ -458,9 +458,9 @@
mk_ind_proof ctxt thss' |> Inductive.rulify;
val strong_induct =
if length names > 1 then
- (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
+ (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
else (strong_raw_induct RSN (2, rev_mp),
- [ind_case_names, RuleCases.consumes 1]);
+ [ind_case_names, Rule_Cases.consumes 1]);
val (induct_name, inducts_name) =
case alt_name of
NONE => (rec_qualified (Binding.name "strong_induct"),
@@ -477,7 +477,7 @@
LocalTheory.note Thm.generatedK
((inducts_name,
[Attrib.internal (K ind_case_names),
- Attrib.internal (K (RuleCases.consumes 1))]),
+ Attrib.internal (K (Rule_Cases.consumes 1))]),
strong_inducts) |> snd
end)
(map (map (rulify_term thy #> rpair [])) vc_compat)
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Nov 01 15:24:45 2009 +0100
@@ -203,10 +203,10 @@
in
-fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
+fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
fun mk_case_names_exhausts descr new =
- map (RuleCases.case_names o exhaust_cases descr o #1)
+ map (Rule_Cases.case_names o exhaust_cases descr o #1)
(filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
end;
@@ -328,7 +328,7 @@
[((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
val unnamed_rules = map (fn induct =>
- ((Binding.empty, [induct]), [RuleCases.inner_rule, Induct.induct_type ""]))
+ ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
(Library.drop (length dt_names, inducts));
in
thy9
--- a/src/HOL/Tools/Function/function.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML Sun Nov 01 15:24:45 2009 +0100
@@ -98,12 +98,12 @@
psimp_attribs psimps
||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
||>> note_theorem ((qualify "pinduct",
- [Attrib.internal (K (RuleCases.case_names cnames)),
- Attrib.internal (K (RuleCases.consumes 1)),
+ [Attrib.internal (K (Rule_Cases.case_names cnames)),
+ Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
||>> note_theorem ((qualify "termination", []), [termination])
||> (snd o note_theorem ((qualify "cases",
- [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
+ [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
@@ -153,7 +153,7 @@
|> add_simps I "simps" simp_attribs tsimps |> snd
|> note_theorem
((qualify "induct",
- [Attrib.internal (K (RuleCases.case_names case_names))]),
+ [Attrib.internal (K (Rule_Cases.case_names case_names))]),
tinduct) |> snd
end
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Nov 01 15:24:45 2009 +0100
@@ -2332,7 +2332,7 @@
in mk_casesrule lthy' pred nparams intros end
val cases_rules = map mk_cases preds
val cases =
- map (fn case_rule => RuleCases.Case {fixes = [],
+ map (fn case_rule => Rule_Cases.Case {fixes = [],
assumes = [("", Logic.strip_imp_prems case_rule)],
binds = [], cases = []}) cases_rules
val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
--- a/src/HOL/Tools/inductive.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Nov 01 15:24:45 2009 +0100
@@ -693,15 +693,15 @@
val rec_name = Binding.name_of rec_binding;
fun rec_qualified qualified = Binding.qualify qualified rec_name;
val intr_names = map Binding.name_of intr_bindings;
- val ind_case_names = RuleCases.case_names intr_names;
+ val ind_case_names = Rule_Cases.case_names intr_names;
val induct =
if coind then
- (raw_induct, [RuleCases.case_names [rec_name],
- RuleCases.case_conclusion (rec_name, intr_names),
- RuleCases.consumes 1, Induct.coinduct_pred (hd cnames)])
+ (raw_induct, [Rule_Cases.case_names [rec_name],
+ Rule_Cases.case_conclusion (rec_name, intr_names),
+ Rule_Cases.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]);
+ (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
+ else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
val (intrs', ctxt1) =
ctxt |>
@@ -716,8 +716,8 @@
LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
fold_map (fn (name, (elim, cases)) =>
LocalTheory.note kind ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
- [Attrib.internal (K (RuleCases.case_names cases)),
- Attrib.internal (K (RuleCases.consumes 1)),
+ [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 (ContextRules.elim_query NONE))]), [elim]) #>
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
@@ -732,7 +732,7 @@
LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
inducts |> map (fn (name, th) => ([th],
[Attrib.internal (K ind_case_names),
- Attrib.internal (K (RuleCases.consumes 1)),
+ Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.induct_pred name))])))] |> snd
end
in (intrs', elims', induct', ctxt3) end;
--- a/src/HOL/Tools/inductive_set.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML Sun Nov 01 15:24:45 2009 +0100
@@ -343,7 +343,7 @@
Simplifier.full_simplify (HOL_basic_ss addsimprocs
[to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
eta_contract_thm (is_pred pred_arities) |>
- RuleCases.save thm
+ Rule_Cases.save thm
end;
val to_pred_att = Thm.rule_attribute o to_pred;
@@ -374,7 +374,7 @@
Thm.instantiate ([], insts) |>
Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
- RuleCases.save thm
+ Rule_Cases.save thm
end;
val to_set_att = Thm.rule_attribute o to_set;
@@ -522,7 +522,7 @@
Inductive.declare_rules kind rec_name coind no_ind cnames
(map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof ctxt3) th,
- map fst (fst (RuleCases.get th)))) elims)
+ map fst (fst (Rule_Cases.get th)))) elims)
raw_induct' ctxt3
in
({intrs = intrs', elims = elims', induct = induct,
--- a/src/HOL/Tools/old_primrec.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML Sun Nov 01 15:24:45 2009 +0100
@@ -237,8 +237,8 @@
val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
in
induct
- |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
- |> RuleCases.save induct
+ |> Rule_Cases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
+ |> Rule_Cases.save induct
end;
local
--- a/src/HOL/Tools/record.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/record.ML Sun Nov 01 15:24:45 2009 +0100
@@ -1553,7 +1553,7 @@
(* attributes *)
-fun case_names_fields x = RuleCases.case_names ["fields"] x;
+fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
fun induct_type_global name = [case_names_fields, Induct.induct_type name];
fun cases_type_global name = [case_names_fields, Induct.cases_type name];
--- a/src/HOL/Tools/split_rule.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML Sun Nov 01 15:24:45 2009 +0100
@@ -118,7 +118,7 @@
fst (fold_rev complete_split_rule_var vars (rl, xs))
|> remove_internal_split
|> Drule.standard
- |> RuleCases.save rl
+ |> Rule_Cases.save rl
end;
@@ -138,7 +138,7 @@
|> fold_index one_goal xss
|> Simplifier.full_simplify split_rule_ss
|> Drule.standard
- |> RuleCases.save rl
+ |> Rule_Cases.save rl
end;
--- a/src/HOL/Tools/typedef.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/typedef.ML Sun Nov 01 15:24:45 2009 +0100
@@ -152,13 +152,13 @@
((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
- [RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
+ [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
- [RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
+ [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
- [RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
+ [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
- [RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
+ [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
||> Sign.parent_path;
val info = {rep_type = oldT, abs_type = newT,
Rep_name = full Rep_name, Abs_name = full Abs_name,
--- a/src/Pure/Isar/attrib.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Nov 01 15:24:45 2009 +0100
@@ -287,15 +287,15 @@
"rename bound variables in abstractions" #>
setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
setup (Binding.name "folded") folded "folded definitions" #>
- setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes)
+ setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
"number of consumed facts" #>
- setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names)
+ setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
"named rule cases" #>
setup (Binding.name "case_conclusion")
- (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion)
+ (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
"named conclusion of rule cases" #>
setup (Binding.name "params")
- (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params)
+ (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
"named rule parameters" #>
setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
"result put into standard form (legacy)" #>
--- a/src/Pure/Isar/obtain.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Sun Nov 01 15:24:45 2009 +0100
@@ -222,7 +222,7 @@
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
- val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
+ val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
val m = length vars;
val n = length params;
val _ = m <= n orelse err "More variables than parameters in obtained rule" rule;
--- a/src/Pure/Isar/proof.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/proof.ML Sun Nov 01 15:24:45 2009 +0100
@@ -387,7 +387,7 @@
fun no_goal_cases st = map (rpair NONE) (goals st);
fun goal_cases st =
- RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
+ Rule_Cases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
fun apply_method current_context meth state =
let
--- a/src/Pure/Isar/proof_context.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Nov 01 15:24:45 2009 +0100
@@ -112,9 +112,9 @@
val add_assms_i: Assumption.export ->
(Thm.binding * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
- val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
- val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
- val get_case: Proof.context -> string -> string option list -> RuleCases.T
+ val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
+ val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
+ val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
@@ -169,7 +169,7 @@
syntax: LocalSyntax.T, (*local syntax*)
consts: Consts.T * Consts.T, (*local/global consts*)
facts: Facts.T, (*local facts*)
- cases: (string * (RuleCases.T * bool)) list}; (*named case contexts*)
+ cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*)
fun make_ctxt (mode, naming, syntax, consts, facts, cases) =
Ctxt {mode = mode, naming = naming, syntax = syntax,
@@ -1150,13 +1150,13 @@
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
| replace [] ys = ys
| replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
- val RuleCases.Case {fixes, assumes, binds, cases} = c;
+ val Rule_Cases.Case {fixes, assumes, binds, cases} = c;
val fixes' = replace fxs fixes;
val binds' = map drop_schematic binds;
in
if null (fold (Term.add_tvarsT o snd) fixes []) andalso
null (fold (fold Term.add_vars o snd) assumes []) then
- RuleCases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
+ Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
else error ("Illegal schematic variable(s) in case " ^ quote name)
end;
@@ -1172,9 +1172,9 @@
fun case_result c ctxt =
let
- val RuleCases.Case {fixes, ...} = c;
+ val Rule_Cases.Case {fixes, ...} = c;
val (ts, ctxt') = ctxt |> fold_map fix fixes;
- val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
+ val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
in
ctxt'
|> bind_terms (map drop_schematic binds)
@@ -1292,7 +1292,7 @@
fun pretty_cases ctxt =
let
fun add_case (_, (_, false)) = I
- | add_case (name, (c as RuleCases.Case {fixes, ...}, true)) =
+ | add_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
cons (name, (fixes, case_result c ctxt));
val cases = fold add_case (cases_of ctxt) [];
in
--- a/src/Pure/Isar/rule_cases.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML Sun Nov 01 15:24:45 2009 +0100
@@ -47,7 +47,7 @@
val strict_mutual_rule: Proof.context -> thm list -> int list * thm
end;
-structure RuleCases: RULE_CASES =
+structure Rule_Cases: RULE_CASES =
struct
(** cases **)
@@ -379,5 +379,5 @@
end;
-structure Basic_Rule_Cases: BASIC_RULE_CASES = RuleCases;
+structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
open Basic_Rule_Cases;
--- a/src/Pure/Isar/rule_insts.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Sun Nov 01 15:24:45 2009 +0100
@@ -177,7 +177,7 @@
else
T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
in
- Drule.instantiate insts thm |> RuleCases.save thm
+ Drule.instantiate insts thm |> Rule_Cases.save thm
end;
fun read_instantiate_mixed' ctxt (args, concl_args) thm =
--- a/src/Pure/Isar/specification.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/specification.ML Sun Nov 01 15:24:45 2009 +0100
@@ -318,7 +318,7 @@
end;
val atts = map (Attrib.internal o K)
- [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
+ [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];
val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = [((Binding.empty, atts), [(thesis, [])])];
--- a/src/Tools/induct.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Tools/induct.ML Sun Nov 01 15:24:45 2009 +0100
@@ -216,8 +216,8 @@
fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
-val consumes0 = RuleCases.consumes_default 0;
-val consumes1 = RuleCases.consumes_default 1;
+val consumes0 = Rule_Cases.consumes_default 0;
+val consumes1 = Rule_Cases.consumes_default 1;
in
@@ -344,10 +344,10 @@
val thy = ProofContext.theory_of ctxt;
fun inst_rule r =
- if null insts then `RuleCases.get r
+ if null insts then `Rule_Cases.get r
else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
|> maps (prep_inst ctxt align_left I)
- |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
+ |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r);
val ruleq =
(case opt_rule of
@@ -359,9 +359,9 @@
in
fn i => fn st =>
ruleq
- |> Seq.maps (RuleCases.consume [] facts)
+ |> Seq.maps (Rule_Cases.consume [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
- CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases)
+ CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases)
(Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
end;
@@ -483,7 +483,7 @@
in Logic.list_implies (map rename_asm As, C) end;
val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
- in [RuleCases.save thm thm'] end
+ in [Rule_Cases.save thm thm'] end
| special_rename_params _ _ ths = ths;
@@ -570,7 +570,7 @@
((fn [] => NONE | ts => List.last ts) #>
(fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
find_inductT ctxt)) [[]]
- |> filter_out (forall RuleCases.is_inner_rule);
+ |> filter_out (forall Rule_Cases.is_inner_rule);
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
| get_inductP _ _ = [];
@@ -583,29 +583,29 @@
val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
fun inst_rule (concls, r) =
- (if null insts then `RuleCases.get r
+ (if null insts then `Rule_Cases.get r
else (align_left "Rule has fewer conclusions than arguments given"
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
|> maps (prep_inst ctxt align_right (atomize_term thy))
- |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
+ |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
|> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
val ruleq =
(case opt_rule of
- SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
+ SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
| NONE =>
(get_inductP ctxt facts @
map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
- |> map_filter (RuleCases.mutual_rule ctxt)
+ |> map_filter (Rule_Cases.mutual_rule ctxt)
|> tap (trace_rules ctxt inductN o map #2)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
fun rule_cases rule =
- RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule);
+ Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule);
in
(fn i => fn st =>
ruleq
- |> Seq.maps (RuleCases.consume (flat defs) facts)
+ |> Seq.maps (Rule_Cases.consume (flat defs) facts)
|> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
(CONJUNCTS (ALLGOALS
@@ -643,7 +643,7 @@
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;
+ if Rule_Cases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
in
@@ -652,9 +652,9 @@
val thy = ProofContext.theory_of ctxt;
fun inst_rule r =
- if null inst then `RuleCases.get r
+ if null inst then `Rule_Cases.get r
else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
- |> pair (RuleCases.get r);
+ |> pair (Rule_Cases.get r);
fun ruleq goal =
(case opt_rule of
@@ -666,12 +666,12 @@
in
SUBGOAL_CASES (fn (goal, i) => fn st =>
ruleq goal
- |> Seq.maps (RuleCases.consume [] facts)
+ |> Seq.maps (Rule_Cases.consume [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
guess_instance ctxt rule i st
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
- CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
+ CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases)
(Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
end;
--- a/src/Tools/induct_tacs.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Tools/induct_tacs.ML Sun Nov 01 15:24:45 2009 +0100
@@ -86,9 +86,9 @@
val argss = map (map (Option.map induct_var)) varss;
val rule =
(case opt_rules of
- SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
+ SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
| NONE =>
- (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
+ (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
(_, rule) :: _ => rule
| [] => raise THM ("No induction rules", 0, [])));
--- a/src/Tools/project_rule.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Tools/project_rule.ML Sun Nov 01 15:24:45 2009 +0100
@@ -47,8 +47,8 @@
Thm.permute_prems 0 (~ k)
#> singleton (Variable.export ctxt' ctxt)
#> Drule.zero_var_indexes
- #> RuleCases.save raw_rule
- #> RuleCases.add_consumes k);
+ #> Rule_Cases.save raw_rule
+ #> Rule_Cases.add_consumes k);
in map result is end;
fun project ctxt i th = hd (projects ctxt [i] th);
--- a/src/ZF/Tools/inductive_package.ML Fri Oct 30 18:33:21 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sun Nov 01 15:24:45 2009 +0100
@@ -66,7 +66,7 @@
val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
- val case_names = RuleCases.case_names intr_names;
+ val case_names = Rule_Cases.case_names intr_names;
(*recT and rec_params should agree for all mutually recursive components*)
val rec_hds = map head_of rec_tms;