1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/project_rule.ML	Sat Feb 28 14:02:12 2009 +0100
     1.3 @@ -0,0 +1,65 @@
     1.4 +(*  Title:      Tools/project_rule.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Transform mutual rule:
     1.8 +
     1.9 +  HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
    1.10 +
    1.11 +into projection:
    1.12 +
    1.13 +  xi:Ai ==> HH ==> Pi xi
    1.14 +*)
    1.15 +
    1.16 +signature PROJECT_RULE_DATA =
    1.17 +sig
    1.18 +  val conjunct1: thm
    1.19 +  val conjunct2: thm
    1.20 +  val mp: thm
    1.21 +end;
    1.22 +
    1.23 +signature PROJECT_RULE =
    1.24 +sig
    1.25 +  val project: Proof.context -> int -> thm -> thm
    1.26 +  val projects: Proof.context -> int list -> thm -> thm list
    1.27 +  val projections: Proof.context -> thm -> thm list
    1.28 +end;
    1.29 +
    1.30 +functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
    1.31 +struct
    1.32 +
    1.33 +fun conj1 th = th RS Data.conjunct1;
    1.34 +fun conj2 th = th RS Data.conjunct2;
    1.35 +fun imp th = th RS Data.mp;
    1.36 +
    1.37 +fun projects ctxt is raw_rule =
    1.38 +  let
    1.39 +    fun proj 1 th = the_default th (try conj1 th)
    1.40 +      | proj k th = proj (k - 1) (conj2 th);
    1.41 +    fun prems k th =
    1.42 +      (case try imp th of
    1.43 +        NONE => (k, th)
    1.44 +      | SOME th' => prems (k + 1) th');
    1.45 +    val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
    1.46 +    fun result i =
    1.47 +      rule
    1.48 +      |> proj i
    1.49 +      |> prems 0 |-> (fn k =>
    1.50 +        Thm.permute_prems 0 (~ k)
    1.51 +        #> singleton (Variable.export ctxt' ctxt)
    1.52 +        #> Drule.zero_var_indexes
    1.53 +        #> RuleCases.save raw_rule
    1.54 +        #> RuleCases.add_consumes k);
    1.55 +  in map result is end;
    1.56 +
    1.57 +fun project ctxt i th = hd (projects ctxt [i] th);
    1.58 +
    1.59 +fun projections ctxt raw_rule =
    1.60 +  let
    1.61 +    fun projs k th =
    1.62 +      (case try conj2 th of
    1.63 +        NONE => k
    1.64 +      | SOME th' => projs (k + 1) th');
    1.65 +    val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
    1.66 +  in projects ctxt (1 upto projs 1 rule) raw_rule end;
    1.67 +
    1.68 +end;