src/Tools/project_rule.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 33368 b1cf34f1855c
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     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;