src/Provers/project_rule.ML
author wenzelm
Wed Apr 04 00:11:03 2007 +0200 (2007-04-04)
changeset 22578 b0eb5652f210
parent 22568 ed7aa5a350ef
permissions -rw-r--r--
removed obsolete sign_of/sign_of_thm;
     1 (*  Title:      Provers/project_rule.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Transform mutual rule:
     6   HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
     7 into projection:
     8   xi:Ai ==> HH ==> Pi xi
     9 *)
    10 
    11 signature PROJECT_RULE_DATA =
    12 sig
    13   val conjunct1: thm
    14   val conjunct2: thm
    15   val mp: thm
    16 end;
    17 
    18 signature PROJECT_RULE =
    19 sig
    20   val project: Proof.context -> int -> thm -> thm
    21   val projects: Proof.context -> int list -> thm -> thm list
    22   val projections: Proof.context -> thm -> thm list
    23 end;
    24 
    25 functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
    26 struct
    27 
    28 fun conj1 th = th RS Data.conjunct1;
    29 fun conj2 th = th RS Data.conjunct2;
    30 fun imp th = th RS Data.mp;
    31 
    32 fun projects ctxt is raw_rule =
    33   let
    34     fun proj 1 th = the_default th (try conj1 th)
    35       | proj k th = proj (k - 1) (conj2 th);
    36     fun prems k th =
    37       (case try imp th of
    38         NONE => (k, th)
    39       | SOME th' => prems (k + 1) th');
    40     val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
    41     fun result i =
    42       rule
    43       |> proj i
    44       |> prems 0 |-> (fn k =>
    45         Thm.permute_prems 0 (~ k)
    46         #> singleton (Variable.export ctxt' ctxt)
    47         #> Drule.zero_var_indexes
    48         #> RuleCases.save raw_rule
    49         #> RuleCases.add_consumes k);
    50   in map result is end;
    51 
    52 fun project ctxt i th = hd (projects ctxt [i] th);
    53 
    54 fun projections ctxt raw_rule =
    55   let
    56     fun projs k th =
    57       (case try conj2 th of
    58         NONE => k
    59       | SOME th' => projs (k + 1) th');
    60     val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
    61   in projects ctxt (1 upto projs 1 rule) raw_rule end;
    62 
    63 end;