src/Tools/project_rule.ML
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 33368 b1cf34f1855c
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     1 (*  Title:      Tools/project_rule.ML
     2     Author:     Makarius
     3 
     4 Transform mutual rule:
     5 
     6   HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
     7 
     8 into projection:
     9 
    10   xi:Ai ==> HH ==> Pi xi
    11 *)
    12 
    13 signature PROJECT_RULE_DATA =
    14 sig
    15   val conjunct1: thm
    16   val conjunct2: thm
    17   val mp: thm
    18 end;
    19 
    20 signature PROJECT_RULE =
    21 sig
    22   val project: Proof.context -> int -> thm -> thm
    23   val projects: Proof.context -> int list -> thm -> thm list
    24   val projections: Proof.context -> thm -> thm list
    25 end;
    26 
    27 functor Project_Rule(Data: PROJECT_RULE_DATA): PROJECT_RULE =
    28 struct
    29 
    30 fun conj1 th = th RS Data.conjunct1;
    31 fun conj2 th = th RS Data.conjunct2;
    32 fun imp th = th RS Data.mp;
    33 
    34 fun projects ctxt is raw_rule =
    35   let
    36     fun proj 1 th = the_default th (try conj1 th)
    37       | proj k th = proj (k - 1) (conj2 th);
    38     fun prems k th =
    39       (case try imp th of
    40         NONE => (k, th)
    41       | SOME th' => prems (k + 1) th');
    42     val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
    43     fun result i =
    44       rule
    45       |> proj i
    46       |> prems 0 |-> (fn k =>
    47         Thm.permute_prems 0 (~ k)
    48         #> singleton (Variable.export ctxt' ctxt)
    49         #> Drule.zero_var_indexes
    50         #> Rule_Cases.save raw_rule
    51         #> Rule_Cases.add_consumes k);
    52   in map result is end;
    53 
    54 fun project ctxt i th = hd (projects ctxt [i] th);
    55 
    56 fun projections ctxt raw_rule =
    57   let
    58     fun projs k th =
    59       (case try conj2 th of
    60         NONE => k
    61       | SOME th' => projs (k + 1) th');
    62     val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
    63   in projects ctxt (1 upto projs 1 rule) raw_rule end;
    64 
    65 end;