--- a/src/Provers/project_rule.ML Tue Jun 13 23:41:31 2006 +0200
+++ b/src/Provers/project_rule.ML Tue Jun 13 23:41:34 2006 +0200
@@ -17,8 +17,9 @@
signature PROJECT_RULE =
sig
- val project: thm -> int -> thm
- val projections: thm -> thm list
+ val project: Proof.context -> int -> thm -> thm
+ val projects: Proof.context -> int list -> thm -> thm list
+ val projections: Proof.context -> thm -> thm list
end;
functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
@@ -28,9 +29,7 @@
fun conj2 th = th RS Data.conjunct2;
fun imp th = th RS Data.mp;
-val freeze = Drule.zero_var_indexes #> Drule.freeze_all;
-
-fun project rule i =
+fun projects ctxt is raw_rule =
let
fun proj 1 th = the_default th (try conj1 th)
| proj k th = proj (k - 1) (conj2 th);
@@ -38,24 +37,27 @@
(case try imp th of
NONE => (k, th)
| SOME th' => prems (k + 1) th');
- in
- rule
- |> freeze
- |> proj i
- |> prems 0 |-> (fn k =>
- Thm.permute_prems 0 (~ k)
- #> Drule.standard'
- #> RuleCases.save rule
- #> RuleCases.add_consumes k)
- end;
+ val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;
+ fun result i =
+ rule
+ |> proj i
+ |> prems 0 |-> (fn k =>
+ Thm.permute_prems 0 (~ k)
+ #> ProofContext.export ctxt' ctxt
+ #> Drule.zero_var_indexes
+ #> RuleCases.save raw_rule
+ #> RuleCases.add_consumes k);
+ in map result is end;
-fun projections rule =
+fun project ctxt i th = hd (projects ctxt [i] th);
+
+fun projections ctxt raw_rule =
let
fun projs k th =
(case try conj2 th of
NONE => k
| SOME th' => projs (k + 1) th');
- val n = projs 1 (freeze rule);
- in map (project rule) (1 upto n) end;
+ val ([rule], _) = ProofContext.import true [raw_rule] ctxt;
+ in projects ctxt (1 upto projs 1 rule) raw_rule end;
end;