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