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